let f be PVertexMapping of G1,G2; :: thesis: ( f is onto implies not f is empty )
assume f is onto ; :: thesis: not f is empty
then rng f = the_Vertices_of G2 by FUNCT_2:def 3;
hence not f is empty ; :: thesis: verum