let C be Cocartesian_category; 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; ( 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; verum