theorem :: GLIB_010:128

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 _V) ") . (W2 .first()) = (F " W2) .first() & ((F _V) ") . (W2 .last()) = (F " W2) .last() ) by Th127;