let G be _Graph; :: thesis: for W being Walk of G

for m, n being odd Element of NAT

for i being Element of NAT st m <= n & n <= len W & i in dom (W .cut (m,n)) holds

( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )

let W be Walk of G; :: thesis: for m, n being odd Element of NAT

for i being Element of NAT st m <= n & n <= len W & i in dom (W .cut (m,n)) holds

( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )

let m, n be odd Element of NAT ; :: thesis: for i being Element of NAT st m <= n & n <= len W & i in dom (W .cut (m,n)) holds

( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )

let i be Element of NAT ; :: thesis: ( m <= n & n <= len W & i in dom (W .cut (m,n)) implies ( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W ) )

assume that

A1: m <= n and

A2: n <= len W and

A3: i in dom (W .cut (m,n)) ; :: thesis: ( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )

1 <= i by A3, FINSEQ_3:25;

then reconsider iaa1 = i - 1 as Element of NAT by INT_1:5;

i <= len (W .cut (m,n)) by A3, FINSEQ_3:25;

then A4: iaa1 < (len (W .cut (m,n))) - 0 by XREAL_1:15;

iaa1 + 1 = i ;

then (W .cut (m,n)) . i = W . (m + iaa1) by A1, A2, A4, Lm15;

hence ( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W ) by A1, A2, A4, Lm15; :: thesis: verum

for m, n being odd Element of NAT

for i being Element of NAT st m <= n & n <= len W & i in dom (W .cut (m,n)) holds

( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )

let W be Walk of G; :: thesis: for m, n being odd Element of NAT

for i being Element of NAT st m <= n & n <= len W & i in dom (W .cut (m,n)) holds

( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )

let m, n be odd Element of NAT ; :: thesis: for i being Element of NAT st m <= n & n <= len W & i in dom (W .cut (m,n)) holds

( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )

let i be Element of NAT ; :: thesis: ( m <= n & n <= len W & i in dom (W .cut (m,n)) implies ( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W ) )

assume that

A1: m <= n and

A2: n <= len W and

A3: i in dom (W .cut (m,n)) ; :: thesis: ( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )

1 <= i by A3, FINSEQ_3:25;

then reconsider iaa1 = i - 1 as Element of NAT by INT_1:5;

i <= len (W .cut (m,n)) by A3, FINSEQ_3:25;

then A4: iaa1 < (len (W .cut (m,n))) - 0 by XREAL_1:15;

iaa1 + 1 = i ;

then (W .cut (m,n)) . i = W . (m + iaa1) by A1, A2, A4, Lm15;

hence ( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W ) by A1, A2, A4, Lm15; :: thesis: verum