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

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