:: deftheorem defines full FUNCTOR0:def 32 :
for A being AltGraph
for B being non empty AltGraph
for F being FunctorStr over A,B holds
( F is full iff ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" ) );