for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 st F is onto holds
for v being Vertex of G2 holds ((F ") _V) . v is Vertex of G1 by Th34, Th72;