let G1, G2, G3, G4 be _Graph; :: thesis: for F1 being empty PGraphMapping of G1,G2
for F2 being empty PGraphMapping of G3,G4 holds F1 = F2
let F1 be empty PGraphMapping of G1,G2; :: thesis: for F2 being empty PGraphMapping of G3,G4 holds F1 = F2
let F2 be empty PGraphMapping of G3,G4; :: thesis: F1 = F2
[(F1 _V),(F1 _E)] = [(F2 _V),(F2 _E)] ;
hence F1 = F2 ; :: thesis: verum