let A be Category; :: thesis: Yoneda A is faithful
set F = Yoneda A;
for o1, o2 being Object of A st Hom o1,o2 <> {} holds
for x1, x2 being Morphism of o1,o2 st (Yoneda A) . x1 = (Yoneda A) . x2 holds
x1 = x2

proof

let o1, o2 be Object of A; :: thesis: ( Hom o1,o2 <> {} implies for x1, x2 being Morphism of o1,o2 st (Yoneda A) . x1 = (Yoneda A) . x2 holds
x1 = x2 )
assume A1: Hom o1,o2 <> {} ; :: thesis: for x1, x2 being Morphism of o1,o2 st (Yoneda A) . x1 = (Yoneda A) . x2 holds
x1 = x2
let x1, x2 be Morphism of o1,o2; :: thesis: ( (Yoneda A) . x1 = (Yoneda A) . x2 implies x1 = x2 )
A2: x2 in Hom o1,o2 by A1, CAT_1:def 7;
assume (Yoneda A) . x1 = (Yoneda A) . x2 ; :: thesis: x1 = x2
then [[<|(cod x1),?>,<|(dom x1),?>],<|x1,?>] = (Yoneda A) . x2 by Def4;
then [[<|(cod x1),?>,<|(dom x1),?>],<|x1,?>] = [[<|(cod x2),?>,<|(dom x2),?>],<|x2,?>] by Def4;
then [<|(cod x1),?>,<|(dom x1),?>,<|x1,?>] = [[<|(cod x2),?>,<|(dom x2),?>],<|x2,?>] by MCART_1:def 3;
then [<|(cod x1),?>,<|(dom x1),?>,<|x1,?>] = [<|(cod x2),?>,<|(dom x2),?>,<|x2,?>] by MCART_1:def 3;
then A3: <|x1,?> = <|x2,?> by MCART_1:28;
A4: x1 in Hom o1,o2 by A1, CAT_1:def 7;
then A5: dom x1 = o1 by CAT_1:18
.= dom x2 by A2, CAT_1:18 ;
cod x1 = o2 by A4, CAT_1:18
.= cod x2 by A2, CAT_1:18 ;
then [[(Hom (cod x1),o2),(Hom (dom x1),o2)],(hom x1,(id o2))] = <|x2,?> . o2 by A5, A3, Def3;
then [[(Hom (cod x1),o2),(Hom (dom x1),o2)],(hom x1,(id o2))] = [[(Hom (cod x2),o2),(Hom (dom x2),o2)],(hom x2,(id o2))] by Def3;
then [[(Hom o2,o2),(Hom (dom x1),o2)],(hom x1,(id o2))] = [[(Hom (cod x2),o2),(Hom (dom x2),o2)],(hom x2,(id o2))] by A4, CAT_1:18;
then [[(Hom o2,o2),(Hom o1,o2)],(hom x1,(id o2))] = [[(Hom (cod x2),o2),(Hom (dom x2),o2)],(hom x2,(id o2))] by A4, CAT_1:18;
then [[(Hom o2,o2),(Hom o1,o2)],(hom x1,(id o2))] = [[(Hom o2,o2),(Hom (dom x2),o2)],(hom x2,(id o2))] by A2, CAT_1:18;
then [[(Hom o2,o2),(Hom o1,o2)],(hom x1,(id o2))] = [[(Hom o2,o2),(Hom o1,o2)],(hom x2,(id o2))] by A2, CAT_1:18;
then [[(Hom o2,o2),(Hom o1,o2)],(hom x1,(id o2))] = [(Hom o2,o2),(Hom o1,o2),(hom x2,(id o2))] by MCART_1:def 3;
then A6: [(Hom o2,o2),(Hom o1,o2),(hom x1,(id o2))] = [(Hom o2,o2),(Hom o1,o2),(hom x2,(id o2))] by MCART_1:def 3;
reconsider dd = id o2 as Morphism of A ;
A7: Hom o2,o2 <> {} by CAT_1:56;
then A8: (id o2) * dd = (id o2) * (id o2) by CAT_1:def 13;
id o2 in Hom o2,o2 by CAT_1:55;
then id o2 in Hom (cod x2),o2 by A2, CAT_1:18;
then id o2 in Hom (cod x2),(dom (id o2)) by CAT_1:44;
then A9: (hom x2,(id o2)) . dd = ((id o2) * (id o2)) * x2 by A8, ENS_1:def 24
.= (id o2) * x2 by CAT_1:59
.= (id o2) * x2 by A1, A7, CAT_1:def 13
.= x2 by A1, CAT_1:57 ;
id o2 in Hom o2,o2 by CAT_1:55;
then id o2 in Hom (cod x1),o2 by A4, CAT_1:18;
then id o2 in Hom (cod x1),(dom (id o2)) by CAT_1:44;
then (hom x1,(id o2)) . dd = ((id o2) * (id o2)) * x1 by A8, ENS_1:def 24
.= (id o2) * x1 by CAT_1:59
.= (id o2) * x1 by A1, A7, CAT_1:def 13
.= x1 by A1, CAT_1:57 ;
hence x1 = x2 by A9, A6, MCART_1:28; :: thesis: verum

end;

hence Yoneda A is faithful by Def6; :: thesis: verum