set F = Yoneda A;

for x1, x2 being object st x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) & (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 holds

x1 = x2

hence Yoneda A is one-to-one by Th5; :: thesis: verum

for x1, x2 being object st x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) & (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 holds

x1 = x2

proof

then
Obj (Yoneda A) is one-to-one
by FUNCT_1:def 4;
let x1, x2 be object ; :: thesis: ( x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) & (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 implies x1 = x2 )

assume that

A1: ( x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) ) and

A2: (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 ; :: thesis: x1 = x2

reconsider c = x1, c1 = x2 as Object of A by A1, FUNCT_2:def 1;

reconsider f = id c1 as Morphism of c1,c1 ;

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

then reconsider d1 = <|c1,?> 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;

(Yoneda A) . (id c1) = id d1

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

then [[(Hom (c,(dom f))),(Hom (c,(cod f)))],(hom (c,f))] = (hom?- c1) . f by A2, A6, ENS_1:def 21;

then [[(Hom (c,(dom f))),(Hom (c,(cod f)))],(hom (c,f))] = [[(Hom (c1,(dom f))),(Hom (c1,(cod f)))],(hom (c1,f))] by ENS_1:def 21;

then [(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [[(Hom (c1,(dom f))),(Hom (c1,(cod f)))],(hom (c1,f))] ;

then [(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [(Hom (c1,(dom f))),(Hom (c1,(cod f))),(hom (c1,f))] ;

then Hom (c,(dom f)) = Hom (c1,(dom f)) by XTUPLE_0:3;

then Hom (c,(dom f)) = Hom (c1,c1) ;

then A10: Hom (c,c1) = Hom (c1,c1) ;

id c1 in Hom (c1,c1) by CAT_1:27;

then reconsider h = id c1 as Morphism of c,c1 by A10, CAT_1:def 5;

dom h = c by A10, CAT_1:5;

hence x1 = x2 ; :: thesis: verum

end;assume that

A1: ( x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) ) and

A2: (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 ; :: thesis: x1 = x2

reconsider c = x1, c1 = x2 as Object of A by A1, FUNCT_2:def 1;

reconsider f = id c1 as Morphism of c1,c1 ;

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

then reconsider d1 = <|c1,?> 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;

(Yoneda A) . (id c1) = id d1

proof

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

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

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

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

then A5: <|(id c1),?> = id <|c1,?> by A3, FUNCT_1:2;

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

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

.= [[<|c1,?>,<|c1,?>],(id <|c1,?>)] by A5

.= id d1 by NATTRA_1:def 17 ;

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

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

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

proof

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

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

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

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

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

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

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

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

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

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

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

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

.= <|c1,?> /. zz by A4, CAT_3:def 10

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

.= <|c1,?> /. zz by A4, CAT_3:def 10

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

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

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

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

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

then A5: <|(id c1),?> = id <|c1,?> by A3, FUNCT_1:2;

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

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

.= [[<|c1,?>,<|c1,?>],(id <|c1,?>)] by A5

.= id d1 by NATTRA_1:def 17 ;

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

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

proof

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

then [[(Hom (c,(dom f))),(Hom (c,(cod f)))],(hom (c,f))] = (hom?- c1) . f by A2, A6, ENS_1:def 21;

then [[(Hom (c,(dom f))),(Hom (c,(cod f)))],(hom (c,f))] = [[(Hom (c1,(dom f))),(Hom (c1,(cod f)))],(hom (c1,f))] by ENS_1:def 21;

then [(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [[(Hom (c1,(dom f))),(Hom (c1,(cod f)))],(hom (c1,f))] ;

then [(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [(Hom (c1,(dom f))),(Hom (c1,(cod f))),(hom (c1,f))] ;

then Hom (c,(dom f)) = Hom (c1,(dom f)) by XTUPLE_0:3;

then Hom (c,(dom f)) = Hom (c1,c1) ;

then A10: Hom (c,c1) = Hom (c1,c1) ;

id c1 in Hom (c1,c1) by CAT_1:27;

then reconsider h = id c1 as Morphism of c,c1 by A10, CAT_1:def 5;

dom h = c by A10, CAT_1:5;

hence x1 = x2 ; :: thesis: verum

hence Yoneda A is one-to-one by Th5; :: thesis: verum