for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 holds (PVM2PGM f) _V = f by Def10;