let G1, G2 be non-Dmulti _Graph; :: thesis: for f being directed PVertexMapping of G1,G2 st f is total holds
DPVM2PGM f is total
let f be directed PVertexMapping of G1,G2; :: thesis: ( f is total implies DPVM2PGM f is total )
assume f is total ; :: thesis: DPVM2PGM f is total
then A1: dom f = the_Vertices_of G1 by PARTFUN1:def 2;
A2: dom ((DPVM2PGM f) _E) = G1 .edgesBetween (dom f) by Def11
.= the_Edges_of G1 by A1, GLIB_000:34 ;
(DPVM2PGM f) _V = f ;
hence DPVM2PGM f is total by A1, A2, GLIB_010:def 11; :: thesis: verum