theorem :: FUNCTOR1:16

for C1, C2 being non empty AltCatStr
for F being Covariant FunctorStr over C1,C2 holds
( F is faithful iff for o1, o2 being Object of C1 holds Morph-Map (F,o1,o2) is one-to-one )