let I be set ; :: thesis: for C being Category
for c, d being Object of
for F being Projections_family of c,I
for F' being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F' & cods F = cods F' holds
c,d are_isomorphic
let C be Category; :: thesis: for c, d being Object of
for F being Projections_family of c,I
for F' being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F' & cods F = cods F' holds
c,d are_isomorphic
let c, d be Object of ; :: thesis: for F being Projections_family of c,I
for F' being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F' & cods F = cods F' holds
c,d are_isomorphic
let F be Projections_family of c,I; :: thesis: for F' being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F' & cods F = cods F' holds
c,d are_isomorphic
let F' be Projections_family of d,I; :: thesis: ( c is_a_product_wrt F & d is_a_product_wrt F' & cods F = cods F' implies c,d are_isomorphic )
assume that
A1: c is_a_product_wrt F and
A2: d is_a_product_wrt F' and
A3: cods F = cods F' ; :: thesis: c,d are_isomorphic
cods F' = cods F' ;
then consider gf being Morphism of such that
gf in Hom d,d and
A4: for k being Morphism of st k in Hom d,d holds
( ( for x being set st x in I holds
(F' /. x) * k = F' /. x ) iff gf = k ) by A2, Def15;
consider f being Morphism of such that
A5: f in Hom d,c and
A6: for k being Morphism of st k in Hom d,c holds
( ( for x being set st x in I holds
(F /. x) * k = F' /. x ) iff f = k ) by A1, A3, Def15;
cods F = cods F ;
then consider fg being Morphism of such that
fg in Hom c,c and
A7: for k being Morphism of st k in Hom c,c holds
( ( for x being set st x in I holds
(F /. x) * k = F /. x ) iff fg = k ) by A1, Def15;
consider g being Morphism of such that
A8: g in Hom c,d and
A9: for k being Morphism of st k in Hom c,d holds
( ( for x being set st x in I holds
(F' /. x) * k = F /. x ) iff g = k ) by A2, A3, Def15;
thus Hom c,d <> {} by A8; :: according to CAT_1:def 17 :: thesis: ex b₁ being Morphism of c,d st b₁ is invertible
reconsider g = g as Morphism of c,d by A8, CAT_1:def 7;
A10: cod g = d by A8, CAT_1:18;

A11: now

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

end;

A12: now

set k = id d;
thus id d in Hom d,d by CAT_1:55; :: thesis: for x being set st x in I holds
(F' /. x) * (id d) = F' /. x
let x be set ; :: thesis: ( x in I implies (F' /. x) * (id d) = F' /. x )
assume x in I ; :: thesis: (F' /. x) * (id d) = F' /. x
then dom (F' /. x) = d by Th45;
hence (F' /. x) * (id d) = F' /. x by CAT_1:47; :: thesis: verum

end;

take g ; :: thesis: g is invertible
take f ; :: according to CAT_1:def 12 :: thesis: ( dom f = cod g & cod f = dom g & g * f = id (cod g) & f * g = id (dom g) )
A13: dom g = c by A8, CAT_1:18;
hence ( dom f = cod g & cod f = dom g ) by A5, A10, CAT_1:18; :: thesis: ( g * f = id (cod g) & f * g = id (dom g) )
A14: cod f = c by A5, CAT_1:18;
A15: dom f = d by A5, CAT_1:18;

now

( dom (g * f) = d & cod (g * f) = d ) by A15, A10, A14, A13, CAT_1:42;
hence g * f in Hom d,d ; :: thesis: for x being set st x in I holds
(F' /. x) * (g * f) = F' /. x
let x be set ; :: thesis: ( x in I implies (F' /. x) * (g * f) = F' /. x )
assume A16: x in I ; :: thesis: (F' /. x) * (g * f) = F' /. x
then dom (F' /. x) = d by Th45;
hence (F' /. x) * (g * f) = ((F' /. x) * g) * f by A10, A14, A13, CAT_1:43
.= (F /. x) * f by A8, A9, A16
.= F' /. x by A5, A6, A16 ;
:: thesis: verum

end;

hence g * f = gf by A4
.= id (cod g) by A10, A4, A12 ;
:: thesis: f * g = id (dom g)

now

( dom (f * g) = c & cod (f * g) = c ) by A15, A10, A14, A13, CAT_1:42;
hence f * g in Hom c,c ; :: thesis: for x being set st x in I holds
(F /. x) * (f * g) = F /. x
let x be set ; :: thesis: ( x in I implies (F /. x) * (f * g) = F /. x )
assume A17: x in I ; :: thesis: (F /. x) * (f * g) = F /. x
then dom (F /. x) = c by Th45;
hence (F /. x) * (f * g) = ((F /. x) * f) * g by A15, A10, A14, CAT_1:43
.= (F' /. x) * g by A5, A6, A17
.= F /. x by A8, A9, A17 ;
:: thesis: verum

end;

hence f * g = fg by A7
.= id (dom g) by A13, A11, A7 ;
:: thesis: verum