for G1, G2, G3, G4 being _Graph
for F being PGraphMapping of G1,G2 st G1 == G3 & G2 == G4 holds
F is PGraphMapping of G3,G4