let G1, G2 be non-multi _Graph; :: thesis: for f being directed PVertexMapping of G1,G2 holds PVM2PGM f = DPVM2PGM f
let f be directed PVertexMapping of G1,G2; :: thesis: PVM2PGM f = DPVM2PGM f
A1: ( (PVM2PGM f) _V = f & (DPVM2PGM f) _V = f ) ;
( dom ((PVM2PGM f) _E) = G1 .edgesBetween (dom f) & dom ((DPVM2PGM f) _E) = G1 .edgesBetween (dom f) ) by Def10, Def11;
hence PVM2PGM f = DPVM2PGM f by A1, GLIB_010:40; :: thesis: verum