theorem Th95: :: GLIBPRE1:94

for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b₃ -valued Walk of G2 holds (F " W2) .vertices() = (F _V) " (W2 .vertices())