let C be Cocartesian_category; :: thesis: C is with_finite_coproduct
A1: [0] C is initial by Def27;
for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 )

proof

let a, b be Object of C; :: thesis: ex c being Object of C ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 )
take a + b ; :: thesis: ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = a + b & cod i2 = a + b & a + b is_a_coproduct_wrt i1,i2 )
take in1 a,b ; :: thesis: ex i2 being Morphism of C st
( dom (in1 a,b) = a & dom i2 = b & cod (in1 a,b) = a + b & cod i2 = a + b & a + b is_a_coproduct_wrt in1 a,b,i2 )
take in2 a,b ; :: thesis: ( dom (in1 a,b) = a & dom (in2 a,b) = b & cod (in1 a,b) = a + b & cod (in2 a,b) = a + b & a + b is_a_coproduct_wrt in1 a,b, in2 a,b )
thus ( dom (in1 a,b) = a & dom (in2 a,b) = b & cod (in1 a,b) = a + b & cod (in2 a,b) = a + b & a + b is_a_coproduct_wrt in1 a,b, in2 a,b ) by Def27, Th64, Th65; :: thesis: verum

end;

hence C is with_finite_coproduct by A1, Th46; :: thesis: verum