let f be PVertexMapping of G1,G2; :: thesis: ( not f is empty implies f is total )
assume A8: not f is empty ; :: thesis: f is total
consider v being Vertex of G1 such that
A9: the_Vertices_of G1 = {v} by GLIB_000:22;
dom f = the_Vertices_of G1 by A8, A9, ZFMISC_1:33;
hence f is total by PARTFUN1:def 2; :: thesis: verum