:: deftheorem defines faithful FUNCTOR0:def 30 :
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is faithful iff the MorphMap of F is "1-1" );