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