for G1, G2, G3, G4 being _Graph
for F1 being empty PGraphMapping of G1,G2
for F2 being empty PGraphMapping of G3,G4 holds F1 = F2