theorem Th96: :: GLIBPRE1:95
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b3 -valued Walk of G2 holds (F " W2) .edges() = (F _E) " (W2 .edges())