:: deftheorem defines EnsHom YONEDA_1:def 1 :
for A being Category holds EnsHom A = Ens (Hom A);