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
( cod i1 = c & cod i2 = c ) by A1, Def18;
then A3: (0,1) --> (i1,i2) is Injections_family of c,{0,1} by Th65;
c is_a_coproduct_wrt (0,1) --> (i1,i2) by A1, Th79;
then d is_a_coproduct_wrt f * ((0,1) --> (i1,i2)) by A2, A3, Th74;
then d is_a_coproduct_wrt (0,1) --> ((f (*) i1),(f (*) i2)) by Th15;
hence d is_a_coproduct_wrt f (*) i1,f (*) i2 by Th79; :: thesis: verum