set F = Yoneda A;
for x1, x2 being set 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

let x1, x2 be set ; :: 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 ;
A3: Hom (c1,c1) <> {} by CAT_1:56;
<|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 18;
<|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 18;
(Yoneda A) . (id c1) = id d1

proof

set X = dom <|(id c1),?>;
A4: for y being set st y in dom <|(id c1),?> holds
<|(id c1),?> . y = (id <|c1,?>) . y

proof

let y be set ; :: 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 ;
A5: Hom (z,z) <> {} by CAT_1:56;
<|(cod (id c1)),?> is_transformable_to <|c1,?> by CAT_1:44;
then A6: <|(cod (id c1)),?> is_transformable_to <|(dom (id c1)),?> by CAT_1:44;
<|(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)))] by CAT_1:44
.= [[(Hom (c1,z)),(Hom (c1,z))],(hom ((id c1),(id z)))] by CAT_1:44
.= [[(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)))] by CAT_1:44
.= [[(Hom (c1,(dom (id z)))),(Hom (c1,(cod (id z))))],(hom (c1,(id z)))] by CAT_1:44
.= <|c1,?> . (id z) by ENS_1:def 22
.= <|c1,?> . zz by A5, NATTRA_1:def 1
.= id (<|c1,?> . z) by NATTRA_1:15
.= (id <|c1,?>) . z by NATTRA_1:21
.= (id <|c1,?>) . z by NATTRA_1:def 5 ;
hence <|(id c1),?> . y = (id <|c1,?>) . y by A6, NATTRA_1:def 5; :: thesis: verum

end;

dom <|(id c1),?> = the carrier of A by FUNCT_2:def 1
.= dom (id <|c1,?>) by FUNCT_2:def 1 ;
then A7: <|(id c1),?> = id <|c1,?> by A4, FUNCT_1:9;
(Yoneda A) . (id c1) = [[<|(cod (id c1)),?>,<|(dom (id c1)),?>],<|(id c1),?>] by Def4
.= [[<|c1,?>,<|(dom (id c1)),?>],<|(id c1),?>] by CAT_1:44
.= [[<|c1,?>,<|c1,?>],(id <|c1,?>)] by A7, CAT_1:44
.= id d1 by NATTRA_1:def 18 ;
hence (Yoneda A) . (id c1) = id d1 ; :: thesis: verum

end;

then A8: (Obj (Yoneda A)) . c1 = d1 by OPPCAT_1:31;
(Yoneda A) . (id c) = id d

proof

set X = dom <|(id c),?>;
A9: for y being set st y in dom <|(id c),?> holds
<|(id c),?> . y = (id <|c,?>) . y

proof

let y be set ; :: 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 ;
A10: Hom (z,z) <> {} by CAT_1:56;
<|(cod (id c)),?> is_transformable_to <|c,?> by CAT_1:44;
then A11: <|(cod (id c)),?> is_transformable_to <|(dom (id c)),?> by CAT_1:44;
<|(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)))] by CAT_1:44
.= [[(Hom (c,z)),(Hom (c,z))],(hom ((id c),(id z)))] by CAT_1:44
.= [[(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)))] by CAT_1:44
.= [[(Hom (c,(dom (id z)))),(Hom (c,(cod (id z))))],(hom (c,(id z)))] by CAT_1:44
.= <|c,?> . (id z) by ENS_1:def 22
.= <|c,?> . zz by A10, NATTRA_1:def 1
.= id (<|c,?> . z) by NATTRA_1:15
.= (id <|c,?>) . z by NATTRA_1:21
.= (id <|c,?>) . z by NATTRA_1:def 5 ;
hence <|(id c),?> . y = (id <|c,?>) . y by A11, NATTRA_1:def 5; :: thesis: verum

end;

dom <|(id c),?> = the carrier of A by FUNCT_2:def 1
.= dom (id <|c,?>) by FUNCT_2:def 1 ;
then A12: <|(id c),?> = id <|c,?> by A9, FUNCT_1:9;
(Yoneda A) . (id c) = [[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>] by Def4
.= [[<|c,?>,<|(dom (id c)),?>],<|(id c),?>] by CAT_1:44
.= [[<|c,?>,<|c,?>],(id <|c,?>)] by A12, CAT_1:44
.= id d by NATTRA_1:def 18 ;
hence (Yoneda A) . (id c) = id d ; :: thesis: verum

end;

then (Obj (Yoneda A)) . c = d by OPPCAT_1:31;
then [[(Hom (c,(dom f))),(Hom (c,(cod f)))],(hom (c,f))] = (hom?- c1) . f by A2, A8, ENS_1:def 22;
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 22;
then [(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [[(Hom (c1,(dom f))),(Hom (c1,(cod f)))],(hom (c1,f))] by MCART_1:def 3;
then [(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [(Hom (c1,(dom f))),(Hom (c1,(cod f))),(hom (c1,f))] by MCART_1:def 3;
then Hom (c,(dom f)) = Hom (c1,(dom f)) by MCART_1:28;
then Hom (c,(dom f)) = Hom (c1,c1) by A3, CAT_1:23;
then A13: Hom (c,c1) = Hom (c1,c1) by A3, CAT_1:23;
id c1 in Hom (c1,c1) by CAT_1:55;
then reconsider h = id c1 as Morphism of c,c1 by A13, CAT_1:def 7;
dom h = c by A3, A13, CAT_1:23;
hence x1 = x2 by A3, CAT_1:23; :: thesis: verum

end;

then Obj (Yoneda A) is one-to-one by FUNCT_1:def 8;
hence Yoneda A is one-to-one by Th6; :: thesis: verum