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;

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;

A11: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A4;

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 )

((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

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;

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;

A11: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A4;

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 A22:
gh = k
; :: thesis: for x being set st x in I holds
assume A20:
for x being set st x in I holds

((F * f) /. x) (*) k = F9 /. x ; :: thesis: gh = k

hence gh = (id b) (*) k by A2, A12, A15, A18, CAT_1:18

.= k by A18, CAT_1:21 ;

:: thesis: verum

end;((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 ) )

then
g (*) (f (*) k) = g (*) h
by A7;(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;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

hence gh = (id b) (*) k by A2, A12, A15, A18, CAT_1:18

.= k by A18, CAT_1:21 ;

:: thesis: verum

((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