Implication Details

Assumptions: extensive

Conclusions: disjoint finite coproducts

Reason: This is Prop. 2.6 in Introduction to extensive and distributive categories.