theorem :: CAT_4:64

for C being Cocartesian_category holds C is with_finite_coproduct