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 )
proof
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;
assume A6: h = k ; :: thesis: for x being set st x in {y} holds
((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