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
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;
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;
reconsider f = f as Morphism of c,d by A5, CAT_1:def 5;
A7: dom f = c by A5, CAT_1:1;
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;
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;
reconsider g = g as Morphism of d,c by A11, CAT_1:def 5;
take f ; :: according to CAT_1:def 20 :: thesis: f is invertible
thus ( Hom (c,d) <> {} & Hom (d,c) <> {} ) by A11, A5; :: according to CAT_1:def 16 :: thesis: ex b₁ being Morphism of d,c st
( f * b₁ = id d & b₁ * f = id c )
take g ; :: thesis: ( f * g = id d & g * f = id c )
A13: cod f = d by A5, CAT_1:1;
A14: dom g = d by A11, CAT_1:1;
A15: cod g = c by A11, CAT_1:1;
thus f * g = f (*) g by A11, A5, CAT_1:def 13
.= fg by A4, A16
.= id d by A4, A9 ; :: thesis: g * f = id c
thus g * f = g (*) f by A11, A5, CAT_1:def 13
.= gf by A10, A18
.= id c by A8, A10 ; :: thesis: verum