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 that
A1: x in dom (W .cut (1,m)) and
A2: m <= len W ; :: thesis: (W .cut (1,m)) . x = W . x
x <= len (W .cut (1,m)) by A1, FINSEQ_3:25;
then A3: x - 1 < (len (W .cut (1,m))) - 0 by XREAL_1:15;
1 <= x by A1, FINSEQ_3:25;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:5;
A4: 1 <= m by ABIAN:12;
xaa1 + 1 = x ;
hence (W .cut (1,m)) . x = W . x by A2, A4, A3, Lm15, JORDAN12:2; :: thesis: verum