theorem Th5: :: YONEDA_1:5

for A being Category
for F being Contravariant_Functor of A, Functors (A,(EnsHom A)) st Obj F is one-to-one & F is faithful holds
F is one-to-one