let C be Category; :: thesis: for c, d being Object of C
for i1, i2, f being Morphism of C 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, f being Morphism of C 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, f be Morphism of C; :: 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, Def19;
then A3: 0 ,1 --> i1,i2 is Injections_family of c,{0 ,1} by Th70;
c is_a_coproduct_wrt 0 ,1 --> i1,i2 by A1, Th85;
then d is_a_coproduct_wrt f * (0 ,1 --> i1,i2) by A2, A3, Th80;
then d is_a_coproduct_wrt 0 ,1 --> (f * i1),(f * i2) by Th19;
hence d is_a_coproduct_wrt f * i1,f * i2 by Th85; :: thesis: verum