let F be PGraphMapping of G1,G2; :: thesis: ( not F is empty implies F is total )
consider v being Vertex of G1 such that
A1: the_Vertices_of G1 = {v} by GLIB_000:22;
assume not F is empty ; :: thesis: F is total
then not dom (F _V) is empty ;
hence dom (F _V) = the_Vertices_of G1 by A1, ZFMISC_1:33; :: according to GLIB_010:def 11 :: thesis: dom (F _E) = the_Edges_of G1
thus dom (F _E) = the_Edges_of G1 ; :: thesis: verum