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