:: deftheorem Def12 defines onto GLIB_010:def 12 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is onto iff ( rng (F _V) = the_Vertices_of G2 & rng (F _E) = the_Edges_of G2 ) );