theorem Th88: :: GLIBPRE0:82

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is onto & F is semi-continuous & v in dom (F _V) holds
(F _E) .: (v .edgesInOut()) = ((F _V) /. v) .edgesInOut()