theorem :: FUNCTOR1:15
for C1, C2 being non empty AltCatStr
for F being Covariant FunctorStr over C1,C2 holds
( F is full iff for o1, o2 being Object of C1 holds Morph-Map (F,o1,o2) is onto )