theorem :: GLIB_010:40

for G1 being _Graph
for G2 being non-multi _Graph
for F1, F2 being PGraphMapping of G1,G2 st F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) holds
F1 = F2