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:
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 ;
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 ;
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;
A8: cod h = a by ;
consider g being Morphism of a,b such that
A9: f * g = id a and
A10: g * f = id b by A4;
A11: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A4;
then A12: dom g = cod f by ;
A13: cod g = dom f by ;
A14: f (*) g = id (cod f) by ;
A15: g (*) f = id (dom f) by ;
dom h = c by ;
then A16: dom (g (*) h) = c by ;
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 ;
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 ;
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
.= ((F * f) /. x) (*) k by
.= F9 /. x by ;
:: thesis: verum
end;
then g (*) (f (*) k) = g (*) h by A7;
hence gh = (id b) (*) k by
.= k by ;
:: 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
.= (F /. x) (*) (f (*) (g (*) h)) by
.= (F /. x) (*) ((id (cod f)) (*) h) by
.= (F /. x) (*) h by
.= F9 /. x by A6, A7, A23 ; :: thesis: verum