let C be Category; :: thesis: for c, d being Object of C
for i1, i2 being Morphism of C
for f being Morphism of c,d st c is_a_coproduct_wrt i1,i2 & dom f = c & cod f = d & f is invertible holds
d is_a_coproduct_wrt f (*) i1,f (*) i2
let c, d be Object of C; :: thesis: for i1, i2 being Morphism of C
for f being Morphism of c,d st c is_a_coproduct_wrt i1,i2 & dom f = c & cod f = d & f is invertible holds
d is_a_coproduct_wrt f (*) i1,f (*) i2
let i1, i2 be Morphism of C; :: thesis: for f being Morphism of c,d st c is_a_coproduct_wrt i1,i2 & dom f = c & cod f = d & f is invertible holds
d is_a_coproduct_wrt f (*) i1,f (*) i2
let f be Morphism of c,d; :: thesis: ( c is_a_coproduct_wrt i1,i2 & dom f = c & cod f = d & f is invertible implies d is_a_coproduct_wrt f (*) i1,f (*) i2 )
assume that
A1: c is_a_coproduct_wrt i1,i2 and
A2: ( dom f = c & cod f = d & f is invertible ) ; :: thesis: d is_a_coproduct_wrt f (*) i1,f (*) i2
c is_a_coproduct_wrt (0,{0}) --> (i1,i2) by A1, Th79;
then d is_a_coproduct_wrt f * ((0,{0}) --> (i1,i2)) by A2, Th74;
then d is_a_coproduct_wrt (0,{0}) --> ((f (*) i1),(f (*) i2)) by Th15;
hence d is_a_coproduct_wrt f (*) i1,f (*) i2 by Th79; :: thesis: verum