:: deftheorem defines full YONEDA_1:def 7 :
for C, D being Category
for T being Contravariant_Functor of C,D holds
( T is full iff for c, c9 being Object of C st Hom ((T . c9),(T . c)) <> {} holds
for g being Morphism of T . c9,T . c holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) );