:: deftheorem Def11 defines total GLIB_010:def 11 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is total iff ( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 ) );