theorem :: GLIB_001:46

for G being _Graph
for W being Walk of G
for m being odd Element of NAT
for x being Element of NAT st x in dom (W .cut (1,m)) & m <= len W holds
(W .cut (1,m)) . x = W . x by Lm23;