let C be Category; :: thesis: for c, d being Object of C
for i1, i2, j1, j2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & d is_a_coproduct_wrt j1,j2 & dom i1 = dom j1 & dom i2 = dom j2 holds
c,d are_isomorphic
let c, d be Object of C; :: thesis: for i1, i2, j1, j2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & d is_a_coproduct_wrt j1,j2 & dom i1 = dom j1 & dom i2 = dom j2 holds
c,d are_isomorphic
let i1, i2, j1, j2 be Morphism of C; :: thesis: ( c is_a_coproduct_wrt i1,i2 & d is_a_coproduct_wrt j1,j2 & dom i1 = dom j1 & dom i2 = dom j2 implies c,d are_isomorphic )
assume that
A1: c is_a_coproduct_wrt i1,i2 and
A2: d is_a_coproduct_wrt j1,j2 and
A3: ( dom i1 = dom j1 & dom i2 = dom j2 ) ; :: thesis: c,d are_isomorphic
set I = {0,1};
set F = (0,1) --> (i1,i2);
set F9 = (0,1) --> (j1,j2);
A4: ( c is_a_coproduct_wrt (0,1) --> (i1,i2) & d is_a_coproduct_wrt (0,1) --> (j1,j2) ) by A1, A2, Th85;
( cod j1 = d & cod j2 = d ) by A2, Def19;
then A5: (0,1) --> (j1,j2) is Injections_family of d,{0,1} by Th70;
( cod i1 = c & cod i2 = c ) by A1, Def19;
then A6: (0,1) --> (i1,i2) is Injections_family of c,{0,1} by Th70;
doms ((0,1) --> (i1,i2)) = (0,1) --> ((dom j1),(dom j2)) by A3, Th10
.= doms ((0,1) --> (j1,j2)) by Th10 ;
hence c,d are_isomorphic by A6, A5, A4, Th78; :: thesis: verum