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 Def27;
hence ( dom (in2 a,b) = b & cod (in2 a,b) = a + b ) by Def27, CAT_3:def 19; :: thesis: verum