let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is total holds
F _V is PVertexMapping of G1,G2
let F be PGraphMapping of G1,G2; :: thesis: ( F is total implies F _V is PVertexMapping of G1,G2 )
assume F is total ; :: thesis: F _V is PVertexMapping of G1,G2
then dom (F _E) = the_Edges_of G1 by GLIB_010:def 11;
hence F _V is PVertexMapping of G1,G2 by Th17; :: thesis: verum