theorem Th129: :: GLIB_010:129

for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for W1 being b₃ -defined Walk of G1
for n being odd Element of NAT st n <= len W1 holds
(F _V) . (W1 . n) = (F .: W1) . n