:: deftheorem defines full FUNCTOR0:def 31 :
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is full iff ex B9 being ManySortedSet of [: the carrier of A, the carrier of A:] ex f being ManySortedFunction of the Arrows of A,B9 st
( B9 = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" ) );