:: deftheorem defines injective FUNCTOR0:def 33 :
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is injective iff ( F is one-to-one & F is faithful ) );