:: deftheorem defines . YONEDA_1:def 5 :
for A, B being Category
for F being Contravariant_Functor of A,B
for c being Object of A holds F . c = (Obj F) . c;