theorem :: GLIBPRE0:84

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is isomorphism holds
(F _E) .: (v .edgesInOut()) = ((F _V) /. v) .edgesInOut()