let I be set ; :: thesis: for C being Category
for c, d being Object of C
for F being Injections_family of c,I
for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds
c,d are_isomorphic
let C be Category; :: thesis: for c, d being Object of C
for F being Injections_family of c,I
for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds
c,d are_isomorphic
let c, d be Object of C; :: thesis: for F being Injections_family of c,I
for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds
c,d are_isomorphic
let F be Injections_family of c,I; :: thesis: for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds
c,d are_isomorphic
let F9 be Injections_family of d,I; :: thesis: ( c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 implies c,d are_isomorphic )
assume that
A1: c is_a_coproduct_wrt F and
A2: d is_a_coproduct_wrt F9 and
A3: doms F = doms F9 ; :: thesis: c,d are_isomorphic
doms F9 = doms F9 ;
then consider fg being Morphism of C such that
fg in Hom (d,d) and
A4: for k being Morphism of C st k in Hom (d,d) holds
( ( for x being set st x in I holds
k * (F9 /. x) = F9 /. x ) iff fg = k ) by A2, Def18;
consider f being Morphism of C such that
A5: f in Hom (c,d) and
A6: for k being Morphism of C st k in Hom (c,d) holds
( ( for x being set st x in I holds
k * (F /. x) = F9 /. x ) iff f = k ) by A1, A3, Def18;
thus Hom (c,d) <> {} by A5; :: according to CAT_1:def 14 :: thesis: ex b₁ being Morphism of c,d st b₁ is invertible
reconsider f = f as Morphism of c,d by A5, CAT_1:def 4;
A7: dom f = c by A5, CAT_1:1;

A8: now

set k = id c;
thus id c in Hom (c,c) by CAT_1:26; :: thesis: for x being set st x in I holds
(id c) * (F /. x) = F /. x
let x be set ; :: thesis: ( x in I implies (id c) * (F /. x) = F /. x )
assume x in I ; :: thesis: (id c) * (F /. x) = F /. x
then cod (F /. x) = c by Th67;
hence (id c) * (F /. x) = F /. x by CAT_1:21; :: thesis: verum

end;

A9: now

set k = id d;
thus id d in Hom (d,d) by CAT_1:26; :: thesis: for x being set st x in I holds
(id d) * (F9 /. x) = F9 /. x
let x be set ; :: thesis: ( x in I implies (id d) * (F9 /. x) = F9 /. x )
assume x in I ; :: thesis: (id d) * (F9 /. x) = F9 /. x
then cod (F9 /. x) = d by Th67;
hence (id d) * (F9 /. x) = F9 /. x by CAT_1:21; :: thesis: verum

end;

doms F = doms F ;
then consider gf being Morphism of C such that
gf in Hom (c,c) and
A10: for k being Morphism of C st k in Hom (c,c) holds
( ( for x being set st x in I holds
k * (F /. x) = F /. x ) iff gf = k ) by A1, Def18;
consider g being Morphism of C such that
A11: g in Hom (d,c) and
A12: for k being Morphism of C st k in Hom (d,c) holds
( ( for x being set st x in I holds
k * (F9 /. x) = F /. x ) iff g = k ) by A2, A3, Def18;
take f ; :: thesis: f is invertible
take g ; :: according to CAT_1:def 9 :: thesis: ( dom g = cod f & cod g = dom f & f * g = id (cod f) & g * f = id (dom f) )
A13: cod f = d by A5, CAT_1:1;
hence ( dom g = cod f & cod g = dom f ) by A11, A7, CAT_1:1; :: thesis: ( f * g = id (cod f) & g * f = id (dom f) )
A14: dom g = d by A11, CAT_1:1;
A15: cod g = c by A11, CAT_1:1;

now

( cod (f * g) = d & dom (f * g) = d ) by A13, A14, A7, A15, CAT_1:17;
hence f * g in Hom (d,d) ; :: thesis: for x being set st x in I holds
(f * g) * (F9 /. x) = F9 /. x
let x be set ; :: thesis: ( x in I implies (f * g) * (F9 /. x) = F9 /. x )
assume A16: x in I ; :: thesis: (f * g) * (F9 /. x) = F9 /. x
then cod (F9 /. x) = d by Th67;
hence (f * g) * (F9 /. x) = f * (g * (F9 /. x)) by A14, A7, A15, CAT_1:18
.= f * (F /. x) by A11, A12, A16
.= F9 /. x by A5, A6, A16 ;
:: thesis: verum

end;

hence f * g = fg by A4
.= id (cod f) by A13, A4, A9 ;
:: thesis: g * f = id (dom f)

now

( cod (g * f) = c & dom (g * f) = c ) by A13, A14, A7, A15, CAT_1:17;
hence g * f in Hom (c,c) ; :: thesis: for x being set st x in I holds
(g * f) * (F /. x) = F /. x
let x be set ; :: thesis: ( x in I implies (g * f) * (F /. x) = F /. x )
assume A17: x in I ; :: thesis: (g * f) * (F /. x) = F /. x
then cod (F /. x) = c by Th67;
hence (g * f) * (F /. x) = g * (f * (F /. x)) by A13, A14, A7, CAT_1:18
.= g * (F9 /. x) by A5, A6, A17
.= F /. x by A11, A12, A17 ;
:: thesis: verum

end;

hence g * f = gf by A10
.= id (dom f) by A7, A8, A10 ;
:: thesis: verum