let F be PGraphMapping of G1,G2; :: thesis: ( not F is empty implies F is onto )

consider v being Vertex of G2 such that

A1: the_Vertices_of G2 = {v} by GLIB_000:22;

assume not F is empty ; :: thesis: F is onto

then not rng (F _V) is empty ;

hence rng (F _V) = the_Vertices_of G2 by A1, ZFMISC_1:33; :: according to GLIB_010:def 12 :: thesis: rng (F _E) = the_Edges_of G2

thus rng (F _E) = the_Edges_of G2 ; :: thesis: verum

consider v being Vertex of G2 such that

A1: the_Vertices_of G2 = {v} by GLIB_000:22;

assume not F is empty ; :: thesis: F is onto

then not rng (F _V) is empty ;

hence rng (F _V) = the_Vertices_of G2 by A1, ZFMISC_1:33; :: according to GLIB_010:def 12 :: thesis: rng (F _E) = the_Edges_of G2

thus rng (F _E) = the_Edges_of G2 ; :: thesis: verum