hereby :: thesis: ( 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" ) implies F is full )

assume F is full ; :: thesis: 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" )
then consider B9 being ManySortedSet of [: the carrier of A, the carrier of A:], f being ManySortedFunction of the Arrows of A,B9 such that
A1: B9 = the Arrows of B * the ObjectMap of F and
A2: f = the MorphMap of F and
A3: f is "onto" by Def32;
reconsider f = f as ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F by A1;
take f = f; :: thesis: ( f = the MorphMap of F & f is "onto" )
thus f = the MorphMap of F by A2; :: thesis: f is "onto"
thus f is "onto" by A1, A3; :: thesis: verum

end;

given f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A4: f = the MorphMap of F and
A5: f is "onto" ; :: thesis: F is full
take the Arrows of B * the ObjectMap of F ; :: according to FUNCTOR0:def 31 :: thesis: ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( the Arrows of B * the ObjectMap of F = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" )
thus ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( the Arrows of B * the ObjectMap of F = the Arrows of B * the ObjectMap of F & f = the MorphMap of F & f is "onto" ) by A4, A5; :: thesis: verum