let G be _Graph; :: thesis: 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
let W be Walk of G; :: thesis: 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
let m be odd Element of NAT ; :: thesis: 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
let x be Element of NAT ; :: thesis: ( x in dom (W .cut 1,m) & m <= len W implies (W .cut 1,m) . x = W . x )
assume A1: ( x in dom (W .cut 1,m) & m <= len W ) ; :: thesis: (W .cut 1,m) . x = W . x
then A2: ( 1 <= x & x <= len (W .cut 1,m) ) by FINSEQ_3:27;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:18;
A3: xaa1 + 1 = x ;
A4: ( not 1 is even & 1 <= m ) by HEYTING3:1, JORDAN12:3;
x - 1 < (len (W .cut 1,m)) - 0 by A2, XREAL_1:17;
hence (W .cut 1,m) . x = W . x by A1, A3, A4, Lm15; :: thesis: verum