let I be set ; :: thesis: for C being Category
for a, b being Object of C
for F being Projections_family of a,I st a is_a_product_wrt F holds
for f being Morphism of b,a st dom f = b & cod f = a & f is invertible holds
b is_a_product_wrt F * f
let C be Category; :: thesis: for a, b being Object of C
for F being Projections_family of a,I st a is_a_product_wrt F holds
for f being Morphism of b,a st dom f = b & cod f = a & f is invertible holds
b is_a_product_wrt F * f
let a, b be Object of C; :: thesis: for F being Projections_family of a,I st a is_a_product_wrt F holds
for f being Morphism of b,a st dom f = b & cod f = a & f is invertible holds
b is_a_product_wrt F * f
let F be Projections_family of a,I; :: thesis: ( a is_a_product_wrt F implies for f being Morphism of b,a st dom f = b & cod f = a & f is invertible holds
b is_a_product_wrt F * f )
assume A1: a is_a_product_wrt F ; :: thesis: for f being Morphism of b,a st dom f = b & cod f = a & f is invertible holds
b is_a_product_wrt F * f
let f be Morphism of b,a; :: thesis: ( dom f = b & cod f = a & f is invertible implies b is_a_product_wrt F * f )
assume that
A2: dom f = b and
A3: cod f = a and
A4: f is invertible ; :: thesis: b is_a_product_wrt F * f
thus F * f is Projections_family of b,I by A2, A3, Th45; :: according to CAT_3:def 14 :: thesis: for b being Object of C
for F9 being Projections_family of b,I st cods (F * f) = cods F9 holds
ex h being Morphism of C st
( h in Hom (b,b) & ( for k being Morphism of C st k in Hom (b,b) holds
( ( for x being set st x in I holds
((F * f) /. x) (*) k = F9 /. x ) iff h = k ) ) )
let c be Object of C; :: thesis: for F9 being Projections_family of c,I st cods (F * f) = cods F9 holds
ex h being Morphism of C st
( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in I holds
((F * f) /. x) (*) k = F9 /. x ) iff h = k ) ) )
A5: doms F = I --> (cod f) by A3, Def13;
let F9 be Projections_family of c,I; :: thesis: ( cods (F * f) = cods F9 implies ex h being Morphism of C st
( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in I holds
((F * f) /. x) (*) k = F9 /. x ) iff h = k ) ) ) )
assume cods (F * f) = cods F9 ; :: thesis: ex h being Morphism of C st
( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in I holds
((F * f) /. x) (*) k = F9 /. x ) iff h = k ) ) )
then cods F = cods F9 by A5, Th16;
then consider h being Morphism of C such that
A6: h in Hom (c,a) and
A7: for k being Morphism of C st k in Hom (c,a) holds
( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff h = k ) by A1, Def14;
A8: cod h = a by A6, CAT_1:1;
consider g being Morphism of a,b such that
A9: f * g = id a and
A10: g * f = id b by A4, CAT_1:def 16;
A11: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A4, CAT_1:def 16;
then A12: dom g = cod f by A3, CAT_1:5;
A13: cod g = dom f by A2, A11, CAT_1:5;
A14: f (*) g = id (cod f) by A9, A3, A11, CAT_1:def 13;
A15: g (*) f = id (dom f) by A10, A2, A11, CAT_1:def 13;
dom h = c by A6, CAT_1:1;
then A16: dom (g (*) h) = c by A3, A12, A8, CAT_1:17;
take gh = g (*) h; :: thesis: ( gh in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in I holds
((F * f) /. x) (*) k = F9 /. x ) iff gh = k ) ) )
cod (g (*) h) = b by A2, A3, A12, A13, A8, CAT_1:17;
hence gh in Hom (c,b) by A16; :: thesis: for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in I holds
((F * f) /. x) (*) k = F9 /. x ) iff gh = k )
let k be Morphism of C; :: thesis: ( k in Hom (c,b) implies ( ( for x being set st x in I holds
((F * f) /. x) (*) k = F9 /. x ) iff gh = k ) )
assume A17: k in Hom (c,b) ; :: thesis: ( ( for x being set st x in I holds
((F * f) /. x) (*) k = F9 /. x ) iff gh = k )
then A18: cod k = b by CAT_1:1;
A19: dom k = c by A17, CAT_1:1;
thus ( ( for x being set st x in I holds
((F * f) /. x) (*) k = F9 /. x ) implies gh = k ) :: thesis: ( gh = k implies for x being set st x in I holds
((F * f) /. x) (*) k = F9 /. x )

proof

assume A20: for x being set st x in I holds
((F * f) /. x) (*) k = F9 /. x ; :: thesis: gh = k

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

( dom (f (*) k) = c & cod (f (*) k) = a ) by A2, A3, A19, A18, CAT_1:17;
hence f (*) k in Hom (c,a) ; :: thesis: for x being set st x in I holds
(F /. x) (*) (f (*) k) = F9 /. x
let x be set ; :: thesis: ( x in I implies (F /. x) (*) (f (*) k) = F9 /. x )
assume A21: x in I ; :: thesis: (F /. x) (*) (f (*) k) = F9 /. x
then dom (F /. x) = a by Th41;
hence (F /. x) (*) (f (*) k) = ((F /. x) (*) f) (*) k by A2, A3, A18, CAT_1:18
.= ((F * f) /. x) (*) k by A21, Def5
.= F9 /. x by A20, A21 ;
:: thesis: verum

end;

then g (*) (f (*) k) = g (*) h by A7;
hence gh = (id b) (*) k by A2, A12, A15, A18, CAT_1:18
.= k by A18, CAT_1:21 ;
:: thesis: verum

end;

assume A22: gh = k ; :: thesis: for x being set st x in I holds
((F * f) /. x) (*) k = F9 /. x
let x be set ; :: thesis: ( x in I implies ((F * f) /. x) (*) k = F9 /. x )
assume A23: x in I ; :: thesis: ((F * f) /. x) (*) k = F9 /. x
then A24: dom (F /. x) = a by Th41;
thus ((F * f) /. x) (*) k = ((F /. x) (*) f) (*) k by A23, Def5
.= (F /. x) (*) (f (*) (g (*) h)) by A2, A3, A18, A22, A24, CAT_1:18
.= (F /. x) (*) ((id (cod f)) (*) h) by A3, A12, A13, A14, A8, CAT_1:18
.= (F /. x) (*) h by A3, A8, CAT_1:21
.= F9 /. x by A6, A7, A23 ; :: thesis: verum