let y be set ; :: thesis: for C being Category

for a being Object of C holds a is_a_product_wrt y .--> (id a)

let C be Category; :: thesis: for a being Object of C holds a is_a_product_wrt y .--> (id a)

let a be Object of C; :: thesis: a is_a_product_wrt y .--> (id a)

set F = y .--> (id a);

dom (id a) = a ;

hence y .--> (id a) is Projections_family of a,{y} by Th43; :: according to CAT_3:def 14 :: thesis: for b being Object of C

for F9 being Projections_family of b,{y} st cods (y .--> (id a)) = cods F9 holds

ex h being Morphism of C st

( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k ) ) )

let b be Object of C; :: thesis: for F9 being Projections_family of b,{y} st cods (y .--> (id a)) = cods F9 holds

ex h being Morphism of C st

( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k ) ) )

let F9 be Projections_family of b,{y}; :: thesis: ( cods (y .--> (id a)) = cods F9 implies ex h being Morphism of C st

( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k ) ) ) )

assume A1: cods (y .--> (id a)) = cods F9 ; :: thesis: ex h being Morphism of C st

( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k ) ) )

take h = F9 /. y; :: thesis: ( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k ) ) )

A2: y in {y} by TARSKI:def 1;

then A3: dom h = b by Th41;

cod h = (cods (y .--> (id a))) /. y by A1, A2, Def2

.= cod ((y .--> (id a)) /. y) by A2, Def2

.= cod (id a) by A2, Th2

.= a ;

hence h in Hom (b,a) by A3; :: thesis: for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k )

let k be Morphism of C; :: thesis: ( k in Hom (b,a) implies ( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k ) )

assume k in Hom (b,a) ; :: thesis: ( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k )

then A4: cod k = a by CAT_1:1;

thus ( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) implies h = k ) :: thesis: ( h = k implies for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x )

((y .--> (id a)) /. x) (*) k = F9 /. x

let x be set ; :: thesis: ( x in {y} implies ((y .--> (id a)) /. x) (*) k = F9 /. x )

assume A7: x in {y} ; :: thesis: ((y .--> (id a)) /. x) (*) k = F9 /. x

hence F9 /. x = k by A6, TARSKI:def 1

.= (id a) (*) k by A4, CAT_1:21

.= ((y .--> (id a)) /. x) (*) k by A7, Th2 ;

:: thesis: verum

for a being Object of C holds a is_a_product_wrt y .--> (id a)

let C be Category; :: thesis: for a being Object of C holds a is_a_product_wrt y .--> (id a)

let a be Object of C; :: thesis: a is_a_product_wrt y .--> (id a)

set F = y .--> (id a);

dom (id a) = a ;

hence y .--> (id a) is Projections_family of a,{y} by Th43; :: according to CAT_3:def 14 :: thesis: for b being Object of C

for F9 being Projections_family of b,{y} st cods (y .--> (id a)) = cods F9 holds

ex h being Morphism of C st

( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k ) ) )

let b be Object of C; :: thesis: for F9 being Projections_family of b,{y} st cods (y .--> (id a)) = cods F9 holds

ex h being Morphism of C st

( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k ) ) )

let F9 be Projections_family of b,{y}; :: thesis: ( cods (y .--> (id a)) = cods F9 implies ex h being Morphism of C st

( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k ) ) ) )

assume A1: cods (y .--> (id a)) = cods F9 ; :: thesis: ex h being Morphism of C st

( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k ) ) )

take h = F9 /. y; :: thesis: ( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k ) ) )

A2: y in {y} by TARSKI:def 1;

then A3: dom h = b by Th41;

cod h = (cods (y .--> (id a))) /. y by A1, A2, Def2

.= cod ((y .--> (id a)) /. y) by A2, Def2

.= cod (id a) by A2, Th2

.= a ;

hence h in Hom (b,a) by A3; :: thesis: for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k )

let k be Morphism of C; :: thesis: ( k in Hom (b,a) implies ( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k ) )

assume k in Hom (b,a) ; :: thesis: ( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) iff h = k )

then A4: cod k = a by CAT_1:1;

thus ( ( for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ) implies h = k ) :: thesis: ( h = k implies for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x )

proof

assume A6:
h = k
; :: thesis: for x being set st x in {y} holds
assume A5:
for x being set st x in {y} holds

((y .--> (id a)) /. x) (*) k = F9 /. x ; :: thesis: h = k

thus k = (id a) (*) k by A4, CAT_1:21

.= ((y .--> (id a)) /. y) (*) k by A2, Th2

.= h by A2, A5 ; :: thesis: verum

end;((y .--> (id a)) /. x) (*) k = F9 /. x ; :: thesis: h = k

thus k = (id a) (*) k by A4, CAT_1:21

.= ((y .--> (id a)) /. y) (*) k by A2, Th2

.= h by A2, A5 ; :: thesis: verum

((y .--> (id a)) /. x) (*) k = F9 /. x

let x be set ; :: thesis: ( x in {y} implies ((y .--> (id a)) /. x) (*) k = F9 /. x )

assume A7: x in {y} ; :: thesis: ((y .--> (id a)) /. x) (*) k = F9 /. x

hence F9 /. x = k by A6, TARSKI:def 1

.= (id a) (*) k by A4, CAT_1:21

.= ((y .--> (id a)) /. x) (*) k by A7, Th2 ;

:: thesis: verum