let C be Cocartesian_category; :: thesis: for a, b being Object of C holds
( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b )
let a, b be Object of C; :: thesis: ( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b )
set i1 = the Incl1 of C . (a,b);
set i2 = the Incl2 of C . (a,b);
a + b is_a_coproduct_wrt the Incl1 of C . (a,b), the Incl2 of C . (a,b) by Def26;
hence ( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b ) by Def26; :: thesis: verum