set F = Yoneda A;

for c, c9 being Object of A st Hom (((Yoneda A) . c9),((Yoneda A) . c)) <> {} holds

for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds

( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f )

for c, c9 being Object of A st Hom (((Yoneda A) . c9),((Yoneda A) . c)) <> {} holds

for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds

( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f )

proof

hence
Yoneda A is full
; :: thesis: verum
let c, c9 be Object of A; :: thesis: ( Hom (((Yoneda A) . c9),((Yoneda A) . c)) <> {} implies for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds

( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f ) )

assume A1: Hom (((Yoneda A) . c9),((Yoneda A) . c)) <> {} ; :: thesis: for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds

( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f )

A2: <|c9,?> . c9 = (hom?- ((Hom A),c9)) . c9 by ENS_1:def 25

.= (Obj (hom?- ((Hom A),c9))) . c9

.= Hom (c9,c9) by ENS_1:60 ;

let g be Morphism of (Yoneda A) . c9,(Yoneda A) . c; :: thesis: ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f )

g in the carrier' of (Functors (A,(EnsHom A))) ;

then g in NatTrans (A,(EnsHom A)) by NATTRA_1:def 17;

then consider F1, F2 being Functor of A, EnsHom A, t being natural_transformation of F1,F2 such that

A3: g = [[F1,F2],t] and

A4: F1 is_naturally_transformable_to F2 by NATTRA_1:def 16;

A5: dom g = F1 by A3, NATTRA_1:33;

<|c9,?> in Funct (A,(EnsHom A)) by CAT_2:def 2;

then reconsider d1 = <|c9,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def 17;

<|c,?> in Funct (A,(EnsHom A)) by CAT_2:def 2;

then reconsider d = <|c,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def 17;

A6: (Yoneda A) . (id c) = id d

A11: (Yoneda A) . (id c9) = id d1

A16: cod g = F2 by A3, NATTRA_1:33;

then A17: F2 = (Yoneda A) . c by A1, CAT_1:5;

A18: (Yoneda A) . c9 = d1 by A11, OPPCAT_1:30;

A19: <|c,?> . c9 = (hom?- ((Hom A),c)) . c9 by ENS_1:def 25

.= (Obj (hom?- ((Hom A),c))) . c9

.= Hom (c,c9) by ENS_1:60 ;

A20: ( dom g = (Yoneda A) . c9 & cod g = (Yoneda A) . c ) by A1, CAT_1:5;

then reconsider t = t as natural_transformation of <|c9,?>,<|c,?> by A5, A16, A11, A10, OPPCAT_1:30;

(Obj (Yoneda A)) . c = d by A6, OPPCAT_1:30;

then <|c9,?> is_transformable_to <|c,?> by A4, A5, A16, A20, A18, NATTRA_1:def 7;

then Hom ((<|c9,?> . c9),(<|c,?> . c9)) <> {} by NATTRA_1:def 2;

then A21: t . c9 in Hom ((<|c9,?> . c9),(<|c,?> . c9)) by CAT_1:def 5;

then A22: cod (t . c9) = <|c,?> . c9 by CAT_1:1;

A23: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def 13;

then reconsider t1 = t . c9 as Element of Maps (Hom A) ;

A24: cod (t . c9) = (fCod (Hom A)) . (t . c9) by A23

.= cod t1 by ENS_1:def 10 ;

t1 in Maps ((dom t1),(cod t1)) by ENS_1:19;

then A25: t1 `2 in Funcs ((dom t1),(cod t1)) by ENS_1:20;

A26: dom (t . c9) = <|c9,?> . c9 by A21, CAT_1:1;

then the Source of (EnsHom A) . (t . c9) <> {} by A2;

then dom t1 <> {} by A23, ENS_1:def 9;

then A27: cod t1 <> {} by A25;

then A28: cod (t . c9) <> {} by A23, ENS_1:def 10;

hence Hom (c,c9) <> {} by A19, A21, CAT_1:1; :: thesis: ex f being Morphism of c,c9 st g = (Yoneda A) . f

dom (t . c9) = (fDom (Hom A)) . (t . c9) by A23

.= dom t1 by ENS_1:def 9 ;

then A29: t1 `2 is Function of (<|c9,?> . c9),(<|c,?> . c9) by A26, A22, A25, A24, FUNCT_2:66;

then A30: dom (t1 `2) = Hom (c9,c9) by A2, A22, A28, FUNCT_2:def 1;

then id c9 in dom (t1 `2) by CAT_1:27;

then A31: (t1 `2) . (id c9) in rng (t1 `2) by FUNCT_1:def 3;

rng (t1 `2) c= Hom (c,c9) by A19, A29, RELAT_1:def 19;

then (t1 `2) . (id c9) in Hom (c,c9) by A31;

then reconsider f = (t1 `2) . (id c9) as Morphism of c,c9 by CAT_1:def 5;

A32: <|c,?> . c9 <> {} by A22, A23, A27, ENS_1:def 10;

then A33: dom f = c by A19, CAT_1:5;

take f ; :: thesis: g = (Yoneda A) . f

A34: cod f = c9 by A19, A32, CAT_1:5;

A35: F1 = (Yoneda A) . c9 by A1, A5, CAT_1:5;

then A36: <|c9,?> is_transformable_to <|c,?> by A4, A17, A15, A10, NATTRA_1:def 7;

for a being Object of A holds <|f,?> . a = t . a

hence g = (Yoneda A) . f by A3, A5, A16, A20, A15, A10, A33, A34, Def4; :: thesis: verum

end;( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f ) )

assume A1: Hom (((Yoneda A) . c9),((Yoneda A) . c)) <> {} ; :: thesis: for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds

( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f )

A2: <|c9,?> . c9 = (hom?- ((Hom A),c9)) . c9 by ENS_1:def 25

.= (Obj (hom?- ((Hom A),c9))) . c9

.= Hom (c9,c9) by ENS_1:60 ;

let g be Morphism of (Yoneda A) . c9,(Yoneda A) . c; :: thesis: ( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f )

g in the carrier' of (Functors (A,(EnsHom A))) ;

then g in NatTrans (A,(EnsHom A)) by NATTRA_1:def 17;

then consider F1, F2 being Functor of A, EnsHom A, t being natural_transformation of F1,F2 such that

A3: g = [[F1,F2],t] and

A4: F1 is_naturally_transformable_to F2 by NATTRA_1:def 16;

A5: dom g = F1 by A3, NATTRA_1:33;

<|c9,?> in Funct (A,(EnsHom A)) by CAT_2:def 2;

then reconsider d1 = <|c9,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def 17;

<|c,?> in Funct (A,(EnsHom A)) by CAT_2:def 2;

then reconsider d = <|c,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def 17;

A6: (Yoneda A) . (id c) = id d

proof

then A10:
(Yoneda A) . c = d
by OPPCAT_1:30;
set X = dom <|(id c),?>;

A7: for y being object st y in dom <|(id c),?> holds

<|(id c),?> . y = (id <|c,?>) . y

.= dom (id <|c,?>) by FUNCT_2:def 1 ;

then A9: <|(id c),?> = id <|c,?> by A7, FUNCT_1:2;

(Yoneda A) . (id c) = [[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>] by Def4

.= [[<|c,?>,<|(dom (id c)),?>],<|(id c),?>]

.= [[<|c,?>,<|c,?>],(id <|c,?>)] by A9

.= id d by NATTRA_1:def 17 ;

hence (Yoneda A) . (id c) = id d ; :: thesis: verum

end;A7: for y being object st y in dom <|(id c),?> holds

<|(id c),?> . y = (id <|c,?>) . y

proof

dom <|(id c),?> =
the carrier of A
by FUNCT_2:def 1
let y be object ; :: thesis: ( y in dom <|(id c),?> implies <|(id c),?> . y = (id <|c,?>) . y )

assume y in dom <|(id c),?> ; :: thesis: <|(id c),?> . y = (id <|c,?>) . y

then reconsider z = y as Object of A by FUNCT_2:def 1;

reconsider zz = id z as Morphism of z,z ;

A8: Hom (z,z) <> {} ;

<|(id c),?> . z = [[(Hom ((cod (id c)),z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))] by Def3

.= [[(Hom (c,z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))]

.= [[(Hom (c,z)),(Hom (c,z))],(hom ((id c),(id z)))]

.= [[(Hom (c,z)),(Hom (c,z))],(hom (c,(id z)))] by ENS_1:53

.= [[(Hom (c,z)),(Hom (c,(cod (id z))))],(hom (c,(id z)))]

.= [[(Hom (c,(dom (id z)))),(Hom (c,(cod (id z))))],(hom (c,(id z)))]

.= <|c,?> . (id z) by ENS_1:def 21

.= <|c,?> /. zz by A8, CAT_3:def 10

.= id (<|c,?> . z) by NATTRA_1:15

.= (id <|c,?>) . z by NATTRA_1:20

.= (id <|c,?>) . z by NATTRA_1:def 5 ;

hence <|(id c),?> . y = (id <|c,?>) . y by NATTRA_1:def 5; :: thesis: verum

end;assume y in dom <|(id c),?> ; :: thesis: <|(id c),?> . y = (id <|c,?>) . y

then reconsider z = y as Object of A by FUNCT_2:def 1;

reconsider zz = id z as Morphism of z,z ;

A8: Hom (z,z) <> {} ;

<|(id c),?> . z = [[(Hom ((cod (id c)),z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))] by Def3

.= [[(Hom (c,z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))]

.= [[(Hom (c,z)),(Hom (c,z))],(hom ((id c),(id z)))]

.= [[(Hom (c,z)),(Hom (c,z))],(hom (c,(id z)))] by ENS_1:53

.= [[(Hom (c,z)),(Hom (c,(cod (id z))))],(hom (c,(id z)))]

.= [[(Hom (c,(dom (id z)))),(Hom (c,(cod (id z))))],(hom (c,(id z)))]

.= <|c,?> . (id z) by ENS_1:def 21

.= <|c,?> /. zz by A8, CAT_3:def 10

.= id (<|c,?> . z) by NATTRA_1:15

.= (id <|c,?>) . z by NATTRA_1:20

.= (id <|c,?>) . z by NATTRA_1:def 5 ;

hence <|(id c),?> . y = (id <|c,?>) . y by NATTRA_1:def 5; :: thesis: verum

.= dom (id <|c,?>) by FUNCT_2:def 1 ;

then A9: <|(id c),?> = id <|c,?> by A7, FUNCT_1:2;

(Yoneda A) . (id c) = [[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>] by Def4

.= [[<|c,?>,<|(dom (id c)),?>],<|(id c),?>]

.= [[<|c,?>,<|c,?>],(id <|c,?>)] by A9

.= id d by NATTRA_1:def 17 ;

hence (Yoneda A) . (id c) = id d ; :: thesis: verum

A11: (Yoneda A) . (id c9) = id d1

proof

then A15:
(Obj (Yoneda A)) . c9 = d1
by OPPCAT_1:30;
set X = dom <|(id c9),?>;

A12: for y being object st y in dom <|(id c9),?> holds

<|(id c9),?> . y = (id <|c9,?>) . y

.= dom (id <|c9,?>) by FUNCT_2:def 1 ;

then A14: <|(id c9),?> = id <|c9,?> by A12, FUNCT_1:2;

(Yoneda A) . (id c9) = [[<|(cod (id c9)),?>,<|(dom (id c9)),?>],<|(id c9),?>] by Def4

.= [[<|c9,?>,<|(dom (id c9)),?>],<|(id c9),?>]

.= [[<|c9,?>,<|c9,?>],(id <|c9,?>)] by A14

.= id d1 by NATTRA_1:def 17 ;

hence (Yoneda A) . (id c9) = id d1 ; :: thesis: verum

end;A12: for y being object st y in dom <|(id c9),?> holds

<|(id c9),?> . y = (id <|c9,?>) . y

proof

dom <|(id c9),?> =
the carrier of A
by FUNCT_2:def 1
let y be object ; :: thesis: ( y in dom <|(id c9),?> implies <|(id c9),?> . y = (id <|c9,?>) . y )

assume y in dom <|(id c9),?> ; :: thesis: <|(id c9),?> . y = (id <|c9,?>) . y

then reconsider z = y as Object of A by FUNCT_2:def 1;

reconsider zz = id z as Morphism of z,z ;

A13: Hom (z,z) <> {} ;

<|(id c9),?> . z = [[(Hom ((cod (id c9)),z)),(Hom ((dom (id c9)),z))],(hom ((id c9),(id z)))] by Def3

.= [[(Hom (c9,z)),(Hom ((dom (id c9)),z))],(hom ((id c9),(id z)))]

.= [[(Hom (c9,z)),(Hom (c9,z))],(hom ((id c9),(id z)))]

.= [[(Hom (c9,z)),(Hom (c9,z))],(hom (c9,(id z)))] by ENS_1:53

.= [[(Hom (c9,z)),(Hom (c9,(cod (id z))))],(hom (c9,(id z)))]

.= [[(Hom (c9,(dom (id z)))),(Hom (c9,(cod (id z))))],(hom (c9,(id z)))]

.= <|c9,?> . (id z) by ENS_1:def 21

.= <|c9,?> /. zz by A13, CAT_3:def 10

.= id (<|c9,?> . z) by NATTRA_1:15

.= (id <|c9,?>) . z by NATTRA_1:20

.= (id <|c9,?>) . z by NATTRA_1:def 5 ;

hence <|(id c9),?> . y = (id <|c9,?>) . y by NATTRA_1:def 5; :: thesis: verum

end;assume y in dom <|(id c9),?> ; :: thesis: <|(id c9),?> . y = (id <|c9,?>) . y

then reconsider z = y as Object of A by FUNCT_2:def 1;

reconsider zz = id z as Morphism of z,z ;

A13: Hom (z,z) <> {} ;

<|(id c9),?> . z = [[(Hom ((cod (id c9)),z)),(Hom ((dom (id c9)),z))],(hom ((id c9),(id z)))] by Def3

.= [[(Hom (c9,z)),(Hom ((dom (id c9)),z))],(hom ((id c9),(id z)))]

.= [[(Hom (c9,z)),(Hom (c9,z))],(hom ((id c9),(id z)))]

.= [[(Hom (c9,z)),(Hom (c9,z))],(hom (c9,(id z)))] by ENS_1:53

.= [[(Hom (c9,z)),(Hom (c9,(cod (id z))))],(hom (c9,(id z)))]

.= [[(Hom (c9,(dom (id z)))),(Hom (c9,(cod (id z))))],(hom (c9,(id z)))]

.= <|c9,?> . (id z) by ENS_1:def 21

.= <|c9,?> /. zz by A13, CAT_3:def 10

.= id (<|c9,?> . z) by NATTRA_1:15

.= (id <|c9,?>) . z by NATTRA_1:20

.= (id <|c9,?>) . z by NATTRA_1:def 5 ;

hence <|(id c9),?> . y = (id <|c9,?>) . y by NATTRA_1:def 5; :: thesis: verum

.= dom (id <|c9,?>) by FUNCT_2:def 1 ;

then A14: <|(id c9),?> = id <|c9,?> by A12, FUNCT_1:2;

(Yoneda A) . (id c9) = [[<|(cod (id c9)),?>,<|(dom (id c9)),?>],<|(id c9),?>] by Def4

.= [[<|c9,?>,<|(dom (id c9)),?>],<|(id c9),?>]

.= [[<|c9,?>,<|c9,?>],(id <|c9,?>)] by A14

.= id d1 by NATTRA_1:def 17 ;

hence (Yoneda A) . (id c9) = id d1 ; :: thesis: verum

A16: cod g = F2 by A3, NATTRA_1:33;

then A17: F2 = (Yoneda A) . c by A1, CAT_1:5;

A18: (Yoneda A) . c9 = d1 by A11, OPPCAT_1:30;

A19: <|c,?> . c9 = (hom?- ((Hom A),c)) . c9 by ENS_1:def 25

.= (Obj (hom?- ((Hom A),c))) . c9

.= Hom (c,c9) by ENS_1:60 ;

A20: ( dom g = (Yoneda A) . c9 & cod g = (Yoneda A) . c ) by A1, CAT_1:5;

then reconsider t = t as natural_transformation of <|c9,?>,<|c,?> by A5, A16, A11, A10, OPPCAT_1:30;

(Obj (Yoneda A)) . c = d by A6, OPPCAT_1:30;

then <|c9,?> is_transformable_to <|c,?> by A4, A5, A16, A20, A18, NATTRA_1:def 7;

then Hom ((<|c9,?> . c9),(<|c,?> . c9)) <> {} by NATTRA_1:def 2;

then A21: t . c9 in Hom ((<|c9,?> . c9),(<|c,?> . c9)) by CAT_1:def 5;

then A22: cod (t . c9) = <|c,?> . c9 by CAT_1:1;

A23: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)) #) by ENS_1:def 13;

then reconsider t1 = t . c9 as Element of Maps (Hom A) ;

A24: cod (t . c9) = (fCod (Hom A)) . (t . c9) by A23

.= cod t1 by ENS_1:def 10 ;

t1 in Maps ((dom t1),(cod t1)) by ENS_1:19;

then A25: t1 `2 in Funcs ((dom t1),(cod t1)) by ENS_1:20;

A26: dom (t . c9) = <|c9,?> . c9 by A21, CAT_1:1;

then the Source of (EnsHom A) . (t . c9) <> {} by A2;

then dom t1 <> {} by A23, ENS_1:def 9;

then A27: cod t1 <> {} by A25;

then A28: cod (t . c9) <> {} by A23, ENS_1:def 10;

hence Hom (c,c9) <> {} by A19, A21, CAT_1:1; :: thesis: ex f being Morphism of c,c9 st g = (Yoneda A) . f

dom (t . c9) = (fDom (Hom A)) . (t . c9) by A23

.= dom t1 by ENS_1:def 9 ;

then A29: t1 `2 is Function of (<|c9,?> . c9),(<|c,?> . c9) by A26, A22, A25, A24, FUNCT_2:66;

then A30: dom (t1 `2) = Hom (c9,c9) by A2, A22, A28, FUNCT_2:def 1;

then id c9 in dom (t1 `2) by CAT_1:27;

then A31: (t1 `2) . (id c9) in rng (t1 `2) by FUNCT_1:def 3;

rng (t1 `2) c= Hom (c,c9) by A19, A29, RELAT_1:def 19;

then (t1 `2) . (id c9) in Hom (c,c9) by A31;

then reconsider f = (t1 `2) . (id c9) as Morphism of c,c9 by CAT_1:def 5;

A32: <|c,?> . c9 <> {} by A22, A23, A27, ENS_1:def 10;

then A33: dom f = c by A19, CAT_1:5;

take f ; :: thesis: g = (Yoneda A) . f

A34: cod f = c9 by A19, A32, CAT_1:5;

A35: F1 = (Yoneda A) . c9 by A1, A5, CAT_1:5;

then A36: <|c9,?> is_transformable_to <|c,?> by A4, A17, A15, A10, NATTRA_1:def 7;

for a being Object of A holds <|f,?> . a = t . a

proof

then
<|f,?> = t
by A4, A35, A17, A15, A10, A33, A34, ISOCAT_1:26;
let a be Object of A; :: thesis: <|f,?> . a = t . a

A37: <|c,?> . a = (hom?- ((Hom A),c)) . a by ENS_1:def 25

.= (Obj (hom?- ((Hom A),c))) . a

.= Hom (c,a) by ENS_1:60 ;

reconsider ta1 = t . a as Element of Maps (Hom A) by A23;

A38: <|c9,?> . a = (hom?- ((Hom A),c9)) . a by ENS_1:def 25

.= (Obj (hom?- ((Hom A),c9))) . a

.= Hom (c9,a) by ENS_1:60 ;

ta1 in Maps ((dom ta1),(cod ta1)) by ENS_1:19;

then A39: ta1 `2 in Funcs ((dom ta1),(cod ta1)) by ENS_1:20;

then A40: ta1 `2 is Function of (dom ta1),(cod ta1) by FUNCT_2:66;

set X = dom (ta1 `2);

A41: dom (t . a) = (fDom (Hom A)) . (t . a) by A23

.= dom ta1 by ENS_1:def 9 ;

A42: Hom ((<|c9,?> . a),(<|c,?> . a)) <> {} by A36, NATTRA_1:def 2;

then A43: dom (t . a) = <|c9,?> . a by CAT_1:5;

A44: cod (t . a) = <|c,?> . a by A42, CAT_1:5;

A45: cod (t . a) = (fCod (Hom A)) . (t . a) by A23

.= cod ta1 by ENS_1:def 10 ;

then A46: ta1 = [[(<|c9,?> . a),(<|c,?> . a)],(ta1 `2)] by A43, A44, A41, ENS_1:8;

A47: ta1 `2 is Function of (dom (t . a)),(cod (t . a)) by A41, A45, A39, FUNCT_2:66;

A48: dom (ta1 `2) = Hom (c9,a)

(hom (f,(id a))) . x = (ta1 `2) . x

then hom (f,(id a)) = ta1 `2 by A49, FUNCT_1:2;

hence <|f,?> . a = t . a by A33, A34, A38, A37, A46, Def3; :: thesis: verum

end;A37: <|c,?> . a = (hom?- ((Hom A),c)) . a by ENS_1:def 25

.= (Obj (hom?- ((Hom A),c))) . a

.= Hom (c,a) by ENS_1:60 ;

reconsider ta1 = t . a as Element of Maps (Hom A) by A23;

A38: <|c9,?> . a = (hom?- ((Hom A),c9)) . a by ENS_1:def 25

.= (Obj (hom?- ((Hom A),c9))) . a

.= Hom (c9,a) by ENS_1:60 ;

ta1 in Maps ((dom ta1),(cod ta1)) by ENS_1:19;

then A39: ta1 `2 in Funcs ((dom ta1),(cod ta1)) by ENS_1:20;

then A40: ta1 `2 is Function of (dom ta1),(cod ta1) by FUNCT_2:66;

set X = dom (ta1 `2);

A41: dom (t . a) = (fDom (Hom A)) . (t . a) by A23

.= dom ta1 by ENS_1:def 9 ;

A42: Hom ((<|c9,?> . a),(<|c,?> . a)) <> {} by A36, NATTRA_1:def 2;

then A43: dom (t . a) = <|c9,?> . a by CAT_1:5;

A44: cod (t . a) = <|c,?> . a by A42, CAT_1:5;

A45: cod (t . a) = (fCod (Hom A)) . (t . a) by A23

.= cod ta1 by ENS_1:def 10 ;

then A46: ta1 = [[(<|c9,?> . a),(<|c,?> . a)],(ta1 `2)] by A43, A44, A41, ENS_1:8;

A47: ta1 `2 is Function of (dom (t . a)),(cod (t . a)) by A41, A45, A39, FUNCT_2:66;

A48: dom (ta1 `2) = Hom (c9,a)

proof
end;

A49:
for x being object st x in dom (ta1 `2) holds (hom (f,(id a))) . x = (ta1 `2) . x

proof

dom (hom (f,a)) = Hom ((cod f),a)
reconsider t1 = t . c9 as Element of Maps (Hom A) by A23;

let x be object ; :: thesis: ( x in dom (ta1 `2) implies (hom (f,(id a))) . x = (ta1 `2) . x )

A50: f in Hom (c,(cod f)) by A33;

assume A51: x in dom (ta1 `2) ; :: thesis: (hom (f,(id a))) . x = (ta1 `2) . x

then reconsider y = x as Morphism of cod f,a by A34, A48, CAT_1:def 5;

reconsider h = y as Morphism of c9,a by A19, A22, A28, CAT_1:5;

A52: dom h = c9 by A48, A51, CAT_1:5;

reconsider tc9 = <|c9,?> . h as Element of Maps (Hom A) by A23;

A53: cod h = a by A48, A51, CAT_1:5;

reconsider tch = <|c,?> . h as Element of Maps (Hom A) by A23;

A54: [[(Hom (c,(dom h))),(Hom (c,(cod h)))],(hom (c,h))] = <|c,?> . h by ENS_1:def 21

.= <|c,?> . h ;

A55: [[(Hom (c9,(dom h))),(Hom (c9,(cod h)))],(hom (c9,h))] = <|c9,?> . h by ENS_1:def 21

.= <|c9,?> . h ;

A56: cod (<|c9,?> . h) = (fCod (Hom A)) . (<|c9,?> . h) by A23

.= cod tc9 by ENS_1:def 10 ;

then A57: cod (<|c9,?> . h) = (tc9 `1) `2 by ENS_1:def 4

.= [(Hom (c9,(dom h))),(Hom (c9,(cod h)))] `2 by A55

.= Hom (c9,(cod h)) ;

then A58: [(t . a),(<|c9,?> . h)] in dom the Comp of (EnsHom A) by A43, A38, A53, CAT_1:15;

tc9 in Maps ((dom tc9),(cod tc9)) by ENS_1:19;

then A59: tc9 `2 in Funcs ((dom tc9),(cod tc9)) by ENS_1:20;

A60: dom (<|c9,?> . h) = (fDom (Hom A)) . (<|c9,?> . h) by A23

.= dom tc9 by ENS_1:def 9 ;

then dom (<|c9,?> . h) = (tc9 `1) `1 by ENS_1:def 3

.= [(Hom (c9,(dom h))),(Hom (c9,(cod h)))] `1 by A55

.= Hom (c9,(dom h)) ;

then tc9 `2 is Function of (Hom (c9,(dom h))),(Hom (c9,(cod h))) by A60, A56, A57, A59, FUNCT_2:66;

then A61: dom (tc9 `2) = Hom (c9,c9) by A48, A51, A52, A53, FUNCT_2:def 1;

A62: dom y = cod f by A34, A48, A51, CAT_1:5;

tch = [[(dom tch),(cod tch)],(tch `2)] by ENS_1:8;

then [(Hom (c,(dom h))),(Hom (c,(cod h))),(hom (c,h))] = [[(dom tch),(cod tch)],(tch `2)] by A54;

then [(Hom (c,(dom h))),(Hom (c,(cod h))),(hom (c,h))] = [(dom tch),(cod tch),(tch `2)] ;

then A63: hom (c,h) = tch `2 by XTUPLE_0:3;

tc9 = [[(dom tc9),(cod tc9)],(tc9 `2)] by ENS_1:8;

then [(dom tc9),(cod tc9),(tc9 `2)] = [[(Hom (c9,(dom h))),(Hom (c9,(cod h)))],(hom (c9,h))] by A55;

then [(dom tc9),(cod tc9),(tc9 `2)] = [(Hom (c9,(dom h))),(Hom (c9,(cod h))),(hom (c9,h))] ;

then A64: tc9 `2 = hom (c9,h) by XTUPLE_0:3;

A65: Hom ((<|c9,?> . c9),(<|c,?> . c9)) <> {} by A36, NATTRA_1:def 2;

then t . c9 in Hom ((<|c9,?> . c9),(<|c,?> . c9)) by CAT_1:def 5;

then A66: cod (t . c9) = <|c,?> . c9 by CAT_1:1;

dom (<|c,?> . h) = (fDom (Hom A)) . (<|c,?> . h) by A23

.= dom tch by ENS_1:def 9 ;

then dom (<|c,?> . h) = (tch `1) `1 by ENS_1:def 3

.= [(Hom (c,(dom h))),(Hom (c,(cod h)))] `1 by A54

.= Hom (c,(dom h)) ;

then A67: [(<|c,?> . h),(t . c9)] in dom the Comp of (EnsHom A) by A19, A52, A66, CAT_1:15;

cod (t . c9) = (fCod (Hom A)) . (t . c9) by A23

.= cod t1 by ENS_1:def 10 ;

then A68: cod t1 = [(Hom (c,(dom h))),(Hom (c,(cod h)))] `1 by A19, A52, A66

.= (tch `1) `1 by A54

.= dom tch by ENS_1:def 3 ;

A69: h in Hom (c9,a) by A48, A51;

then A70: <|c,?> /. h = <|c,?> . h by CAT_3:def 10;

Hom ((<|c,?> . c9),(<|c,?> . a)) <> {} by A48, A51, CAT_1:84;

then A71: (<|c,?> /. h) * (t . c9) = (<|c,?> . h) (*) (t . c9) by A65, A70, CAT_1:def 13

.= (fComp (Hom A)) . (tch,t1) by A23, A67, CAT_1:def 1

.= tch * t1 by A68, ENS_1:def 11

.= [[(dom t1),(cod tch)],((tch `2) * (t1 `2))] by A68, ENS_1:def 6 ;

A72: cod tc9 = (tc9 `1) `2 by ENS_1:def 4

.= [(Hom (c9,(dom h))),(Hom (c9,(cod h)))] `2 by A55

.= dom ta1 by A43, A41, A38, A53 ;

A73: <|c9,?> /. h = <|c9,?> . h by A69, CAT_3:def 10;

Hom ((<|c9,?> . c9),(<|c9,?> . a)) <> {} by A48, A51, CAT_1:84;

then A74: (t . a) * (<|c9,?> /. h) = (t . a) (*) (<|c9,?> . h) by A42, A73, CAT_1:def 13

.= (fComp (Hom A)) . (ta1,tc9) by A23, A58, CAT_1:def 1

.= ta1 * tc9 by A72, ENS_1:def 11

.= [[(dom tc9),(cod ta1)],((ta1 `2) * (tc9 `2))] by A72, ENS_1:def 6 ;

(t . a) * (<|c9,?> /. h) = (<|c,?> /. h) * (t . c9) by A4, A35, A17, A15, A10, A48, A51, NATTRA_1:def 8;

then [(dom tc9),(cod ta1),((ta1 `2) * (tc9 `2))] = [[(dom t1),(cod tch)],((tch `2) * (t1 `2))] by A74, A71;

then [(dom tc9),(cod ta1),((ta1 `2) * (tc9 `2))] = [(dom t1),(cod tch),((tch `2) * (t1 `2))] ;

then A75: (ta1 `2) * (tc9 `2) = (tch `2) * (t1 `2) by XTUPLE_0:3;

A76: id c9 in Hom (c9,(cod f)) by A34, CAT_1:27;

(hom (f,(id a))) . x = (hom (f,a)) . y by ENS_1:53

.= y (*) f by A34, A48, A51, ENS_1:def 20

.= (tch `2) . ((t1 `2) . (id c9)) by A62, A63, A50, ENS_1:def 19

.= ((ta1 `2) * (tc9 `2)) . (id c9) by A30, A75, CAT_1:27, FUNCT_1:13

.= (ta1 `2) . ((hom (c9,h)) . (id c9)) by A64, A61, CAT_1:27, FUNCT_1:13

.= (ta1 `2) . (y (*) (id c9)) by A62, A76, ENS_1:def 19

.= (ta1 `2) . x by A34, A62, CAT_1:22 ;

hence (hom (f,(id a))) . x = (ta1 `2) . x ; :: thesis: verum

end;let x be object ; :: thesis: ( x in dom (ta1 `2) implies (hom (f,(id a))) . x = (ta1 `2) . x )

A50: f in Hom (c,(cod f)) by A33;

assume A51: x in dom (ta1 `2) ; :: thesis: (hom (f,(id a))) . x = (ta1 `2) . x

then reconsider y = x as Morphism of cod f,a by A34, A48, CAT_1:def 5;

reconsider h = y as Morphism of c9,a by A19, A22, A28, CAT_1:5;

A52: dom h = c9 by A48, A51, CAT_1:5;

reconsider tc9 = <|c9,?> . h as Element of Maps (Hom A) by A23;

A53: cod h = a by A48, A51, CAT_1:5;

reconsider tch = <|c,?> . h as Element of Maps (Hom A) by A23;

A54: [[(Hom (c,(dom h))),(Hom (c,(cod h)))],(hom (c,h))] = <|c,?> . h by ENS_1:def 21

.= <|c,?> . h ;

A55: [[(Hom (c9,(dom h))),(Hom (c9,(cod h)))],(hom (c9,h))] = <|c9,?> . h by ENS_1:def 21

.= <|c9,?> . h ;

A56: cod (<|c9,?> . h) = (fCod (Hom A)) . (<|c9,?> . h) by A23

.= cod tc9 by ENS_1:def 10 ;

then A57: cod (<|c9,?> . h) = (tc9 `1) `2 by ENS_1:def 4

.= [(Hom (c9,(dom h))),(Hom (c9,(cod h)))] `2 by A55

.= Hom (c9,(cod h)) ;

then A58: [(t . a),(<|c9,?> . h)] in dom the Comp of (EnsHom A) by A43, A38, A53, CAT_1:15;

tc9 in Maps ((dom tc9),(cod tc9)) by ENS_1:19;

then A59: tc9 `2 in Funcs ((dom tc9),(cod tc9)) by ENS_1:20;

A60: dom (<|c9,?> . h) = (fDom (Hom A)) . (<|c9,?> . h) by A23

.= dom tc9 by ENS_1:def 9 ;

then dom (<|c9,?> . h) = (tc9 `1) `1 by ENS_1:def 3

.= [(Hom (c9,(dom h))),(Hom (c9,(cod h)))] `1 by A55

.= Hom (c9,(dom h)) ;

then tc9 `2 is Function of (Hom (c9,(dom h))),(Hom (c9,(cod h))) by A60, A56, A57, A59, FUNCT_2:66;

then A61: dom (tc9 `2) = Hom (c9,c9) by A48, A51, A52, A53, FUNCT_2:def 1;

A62: dom y = cod f by A34, A48, A51, CAT_1:5;

tch = [[(dom tch),(cod tch)],(tch `2)] by ENS_1:8;

then [(Hom (c,(dom h))),(Hom (c,(cod h))),(hom (c,h))] = [[(dom tch),(cod tch)],(tch `2)] by A54;

then [(Hom (c,(dom h))),(Hom (c,(cod h))),(hom (c,h))] = [(dom tch),(cod tch),(tch `2)] ;

then A63: hom (c,h) = tch `2 by XTUPLE_0:3;

tc9 = [[(dom tc9),(cod tc9)],(tc9 `2)] by ENS_1:8;

then [(dom tc9),(cod tc9),(tc9 `2)] = [[(Hom (c9,(dom h))),(Hom (c9,(cod h)))],(hom (c9,h))] by A55;

then [(dom tc9),(cod tc9),(tc9 `2)] = [(Hom (c9,(dom h))),(Hom (c9,(cod h))),(hom (c9,h))] ;

then A64: tc9 `2 = hom (c9,h) by XTUPLE_0:3;

A65: Hom ((<|c9,?> . c9),(<|c,?> . c9)) <> {} by A36, NATTRA_1:def 2;

then t . c9 in Hom ((<|c9,?> . c9),(<|c,?> . c9)) by CAT_1:def 5;

then A66: cod (t . c9) = <|c,?> . c9 by CAT_1:1;

dom (<|c,?> . h) = (fDom (Hom A)) . (<|c,?> . h) by A23

.= dom tch by ENS_1:def 9 ;

then dom (<|c,?> . h) = (tch `1) `1 by ENS_1:def 3

.= [(Hom (c,(dom h))),(Hom (c,(cod h)))] `1 by A54

.= Hom (c,(dom h)) ;

then A67: [(<|c,?> . h),(t . c9)] in dom the Comp of (EnsHom A) by A19, A52, A66, CAT_1:15;

cod (t . c9) = (fCod (Hom A)) . (t . c9) by A23

.= cod t1 by ENS_1:def 10 ;

then A68: cod t1 = [(Hom (c,(dom h))),(Hom (c,(cod h)))] `1 by A19, A52, A66

.= (tch `1) `1 by A54

.= dom tch by ENS_1:def 3 ;

A69: h in Hom (c9,a) by A48, A51;

then A70: <|c,?> /. h = <|c,?> . h by CAT_3:def 10;

Hom ((<|c,?> . c9),(<|c,?> . a)) <> {} by A48, A51, CAT_1:84;

then A71: (<|c,?> /. h) * (t . c9) = (<|c,?> . h) (*) (t . c9) by A65, A70, CAT_1:def 13

.= (fComp (Hom A)) . (tch,t1) by A23, A67, CAT_1:def 1

.= tch * t1 by A68, ENS_1:def 11

.= [[(dom t1),(cod tch)],((tch `2) * (t1 `2))] by A68, ENS_1:def 6 ;

A72: cod tc9 = (tc9 `1) `2 by ENS_1:def 4

.= [(Hom (c9,(dom h))),(Hom (c9,(cod h)))] `2 by A55

.= dom ta1 by A43, A41, A38, A53 ;

A73: <|c9,?> /. h = <|c9,?> . h by A69, CAT_3:def 10;

Hom ((<|c9,?> . c9),(<|c9,?> . a)) <> {} by A48, A51, CAT_1:84;

then A74: (t . a) * (<|c9,?> /. h) = (t . a) (*) (<|c9,?> . h) by A42, A73, CAT_1:def 13

.= (fComp (Hom A)) . (ta1,tc9) by A23, A58, CAT_1:def 1

.= ta1 * tc9 by A72, ENS_1:def 11

.= [[(dom tc9),(cod ta1)],((ta1 `2) * (tc9 `2))] by A72, ENS_1:def 6 ;

(t . a) * (<|c9,?> /. h) = (<|c,?> /. h) * (t . c9) by A4, A35, A17, A15, A10, A48, A51, NATTRA_1:def 8;

then [(dom tc9),(cod ta1),((ta1 `2) * (tc9 `2))] = [[(dom t1),(cod tch)],((tch `2) * (t1 `2))] by A74, A71;

then [(dom tc9),(cod ta1),((ta1 `2) * (tc9 `2))] = [(dom t1),(cod tch),((tch `2) * (t1 `2))] ;

then A75: (ta1 `2) * (tc9 `2) = (tch `2) * (t1 `2) by XTUPLE_0:3;

A76: id c9 in Hom (c9,(cod f)) by A34, CAT_1:27;

(hom (f,(id a))) . x = (hom (f,a)) . y by ENS_1:53

.= y (*) f by A34, A48, A51, ENS_1:def 20

.= (tch `2) . ((t1 `2) . (id c9)) by A62, A63, A50, ENS_1:def 19

.= ((ta1 `2) * (tc9 `2)) . (id c9) by A30, A75, CAT_1:27, FUNCT_1:13

.= (ta1 `2) . ((hom (c9,h)) . (id c9)) by A64, A61, CAT_1:27, FUNCT_1:13

.= (ta1 `2) . (y (*) (id c9)) by A62, A76, ENS_1:def 19

.= (ta1 `2) . x by A34, A62, CAT_1:22 ;

hence (hom (f,(id a))) . x = (ta1 `2) . x ; :: thesis: verum

proof
end;

then
dom (ta1 `2) = dom (hom (f,(id a)))
by A34, A48, ENS_1:53;then hom (f,(id a)) = ta1 `2 by A49, FUNCT_1:2;

hence <|f,?> . a = t . a by A33, A34, A38, A37, A46, Def3; :: thesis: verum

hence g = (Yoneda A) . f by A3, A5, A16, A20, A15, A10, A33, A34, Def4; :: thesis: verum