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

for m, n being odd Element of NAT st m <= n & n <= len W holds

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

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

let W be Walk of G; :: thesis: for m, n being odd Element of NAT st m <= n & n <= len W holds

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

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

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

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

set W2 = W .cut (m,n);

assume that

A1: m <= n and

A2: n <= len W ; :: thesis: ( (len (W .cut (m,n))) + m = n + 1 & ( for i being Element of NAT st i < len (W .cut (m,n)) holds

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

A3: 1 <= m by ABIAN:12;

A4: W .cut (m,n) = (m,n) -cut W by A1, A2, Def11;

hence A5: (len (W .cut (m,n))) + m = n + 1 by A1, A2, A3, FINSEQ_6:def 4; :: thesis: for i being Element of NAT st i < len (W .cut (m,n)) holds

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

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

assume A6: i < len (W .cut (m,n)) ; :: thesis: ( (W .cut (m,n)) . (i + 1) = W . (m + i) & m + i in dom W )

hence (W .cut (m,n)) . (i + 1) = W . (m + i) by A1, A2, A4, A3, FINSEQ_6:def 4; :: thesis: m + i in dom W

m + i < n + 1 by A5, A6, XREAL_1:8;

then m + i <= n by NAT_1:13;

then A7: m + i <= len W by A2, XXREAL_0:2;

1 <= m + i by ABIAN:12, NAT_1:12;

hence m + i in dom W by A7, FINSEQ_3:25; :: thesis: verum

for m, n being odd Element of NAT st m <= n & n <= len W holds

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

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

let W be Walk of G; :: thesis: for m, n being odd Element of NAT st m <= n & n <= len W holds

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

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

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

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

set W2 = W .cut (m,n);

assume that

A1: m <= n and

A2: n <= len W ; :: thesis: ( (len (W .cut (m,n))) + m = n + 1 & ( for i being Element of NAT st i < len (W .cut (m,n)) holds

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

A3: 1 <= m by ABIAN:12;

A4: W .cut (m,n) = (m,n) -cut W by A1, A2, Def11;

hence A5: (len (W .cut (m,n))) + m = n + 1 by A1, A2, A3, FINSEQ_6:def 4; :: thesis: for i being Element of NAT st i < len (W .cut (m,n)) holds

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

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

assume A6: i < len (W .cut (m,n)) ; :: thesis: ( (W .cut (m,n)) . (i + 1) = W . (m + i) & m + i in dom W )

hence (W .cut (m,n)) . (i + 1) = W . (m + i) by A1, A2, A4, A3, FINSEQ_6:def 4; :: thesis: m + i in dom W

m + i < n + 1 by A5, A6, XREAL_1:8;

then m + i <= n by NAT_1:13;

then A7: m + i <= len W by A2, XXREAL_0:2;

1 <= m + i by ABIAN:12, NAT_1:12;

hence m + i in dom W by A7, FINSEQ_3:25; :: thesis: verum