theorem :: YONEDA_1:4

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