let f be PVertexMapping of G1,G2; :: thesis: ( not f is empty implies f is onto )
assume A1: not f is empty ; :: thesis: f is onto
consider v being Vertex of G2 such that
A2: the_Vertices_of G2 = {v} by GLIB_000:22;
rng f = the_Vertices_of G2 by A1, A2, ZFMISC_1:33;
hence f is onto by FUNCT_2:def 3; :: thesis: verum