let I be set ; :: thesis: for C being Category
for c, d being Object of C
for F being Projections_family of c,I
for F9 being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F9 & cods F = cods F9 holds
c,d are_isomorphic
let C be Category; :: thesis: for c, d being Object of C
for F being Projections_family of c,I
for F9 being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F9 & cods F = cods F9 holds
c,d are_isomorphic
let c, d be Object of C; :: thesis: for F being Projections_family of c,I
for F9 being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F9 & cods F = cods F9 holds
c,d are_isomorphic
let F be Projections_family of c,I; :: thesis: for F9 being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F9 & cods F = cods F9 holds
c,d are_isomorphic
let F9 be Projections_family of d,I; :: thesis: ( c is_a_product_wrt F & d is_a_product_wrt F9 & cods F = cods F9 implies c,d are_isomorphic )
assume that
A1: c is_a_product_wrt F and
A2: d is_a_product_wrt F9 and
A3: cods F = cods F9 ; :: thesis: c,d are_isomorphic
cods F9 = cods F9 ;
then consider gf being Morphism of C such that
gf 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
(F9 /. x) (*) k = F9 /. x ) iff gf = k ) by A2, Def14;
consider f being Morphism of C such that
A5: f in Hom (d,c) and
A6: for k being Morphism of C st k in Hom (d,c) holds
( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff f = k ) by A1, A3, Def14;
reconsider f = f as Morphism of d,c by A5, CAT_1:def 5;
cods F = cods F ;
then consider fg being Morphism of C such that
fg in Hom (c,c) and
A7: for k being Morphism of C 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, Def14;
consider g being Morphism of C such that
A8: g in Hom (c,d) and
A9: for k being Morphism of C st k in Hom (c,d) holds
( ( for x being set st x in I holds
(F9 /. x) (*) k = F /. x ) iff g = k ) by A2, A3, Def14;
reconsider g = g as Morphism of c,d by A8, CAT_1:def 5;
A10: cod g = d by A8, CAT_1:1;

A11: now :: thesis: ( id c in Hom (c,c) & ( for x being set st x in I holds
(F /. x) (*) (id c) = F /. x ) )

set k = id c;
thus id c in Hom (c,c) by CAT_1:27; :: 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 Th41;
hence (F /. x) (*) (id c) = F /. x by CAT_1:22; :: thesis: verum

end;

A12: now :: thesis: ( id d in Hom (d,d) & ( for x being set st x in I holds
(F9 /. x) (*) (id d) = F9 /. x ) )

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

end;

take g ; :: according to CAT_1:def 20 :: thesis: g is invertible
thus ( Hom (c,d) <> {} & Hom (d,c) <> {} ) by A5, A8; :: according to CAT_1:def 16 :: thesis: ex b₁ being Morphism of d,c st
( g * b₁ = id d & b₁ * g = id c )
take f ; :: thesis: ( g * f = id d & f * g = id c )
A13: dom g = c by A8, CAT_1:1;
A14: cod f = c by A5, CAT_1:1;
A15: dom f = d by A5, CAT_1:1;

A16: now :: thesis: ( g (*) f in Hom (d,d) & ( for x being set st x in I holds
(F9 /. x) (*) (g (*) f) = F9 /. x ) )

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

end;

thus g * f = g (*) f by A5, A8, CAT_1:def 13
.= gf by A4, A16
.= id d by A4, A12 ; :: thesis: f * g = id c

A18: now :: thesis: ( f (*) g in Hom (c,c) & ( for x being set st x in I holds
(F /. x) (*) (f (*) g) = F /. x ) )

( dom (f (*) g) = c & cod (f (*) g) = c ) by A15, A10, A14, A13, CAT_1:17;
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 A19: x in I ; :: thesis: (F /. x) (*) (f (*) g) = F /. x
then dom (F /. x) = c by Th41;
hence (F /. x) (*) (f (*) g) = ((F /. x) (*) f) (*) g by A15, A10, A14, CAT_1:18
.= (F9 /. x) (*) g by A5, A6, A19
.= F /. x by A8, A9, A19 ;
:: thesis: verum

end;

thus f * g = f (*) g by A5, A8, CAT_1:def 13
.= fg by A7, A18
.= id c by A11, A7 ; :: thesis: verum