let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is total & F is onto & G1 is loopfull holds
G2 is loopfull
let F be PGraphMapping of G1,G2; :: thesis: ( F is total & F is onto & G1 is loopfull implies G2 is loopfull )
assume A1: ( F is total & F is onto ) ; :: thesis: ( not G1 is loopfull or G2 is loopfull )
G1 .loops() c= the_Edges_of G1 ;
then ( G1 .loops() c= dom (F _E) & rng (F _V) = the_Vertices_of G2 ) by A1, GLIB_010:def 11, GLIB_010:def 12;
hence ( not G1 is loopfull or G2 is loopfull ) by Th6; :: thesis: verum