let C be Cocartesian_category; :: thesis: C is with_finite_coproduct
A1: 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 Def26, Th59, Th60; :: thesis: verum

end;

EmptyMS C is initial by Def26;
hence C is with_finite_coproduct by A1, Th44; :: thesis: verum