for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 st F is isomorphism holds
( F * (F ") = id G2 & (F ") * F = id G1 )