theorem Th127: :: GLIB_010:127

for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b₃ -defined Walk of G1 holds
( (F _V) . (W1 .first()) = (F .: W1) .first() & (F _V) . (W1 .last()) = (F .: W1) .last() )