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

for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds

ex j being odd Nat st

( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )

let W be Walk of G; :: thesis: for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds

ex j being odd Nat st

( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )

let m, n, i be odd Nat; :: thesis: ( m <= n & n <= len W & i <= len (W .cut (m,n)) implies ex j being odd Nat st

( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W ) )

assume that

A1: m <= n and

A2: n <= len W and

A3: i <= len (W .cut (m,n)) ; :: thesis: ex j being odd Nat st

( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )

set j = (m + i) - 1;

( m >= 1 & i >= 1 ) by ABIAN:12;

then m + i >= 1 + 1 by XREAL_1:7;

then (m + i) - 1 >= (1 + 1) - 1 by XREAL_1:9;

then (m + i) - 1 is odd Element of NAT by INT_1:3;

then reconsider j = (m + i) - 1 as odd Nat ;

take j ; :: thesis: ( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )

reconsider m9 = m, n9 = n as odd Element of NAT by ORDINAL1:def 12;

i >= 1 by ABIAN:12;

then i - 1 >= 1 - 1 by XREAL_1:9;

then reconsider i1 = i - 1 as Element of NAT by INT_1:3;

i < (len (W .cut (m,n))) + 1 by A3, NAT_1:13;

then A4: i1 < ((len (W .cut (m,n))) + 1) - 1 by XREAL_1:9;

thus (W .cut (m,n)) . i = (W .cut (m9,n9)) . (i1 + 1)

.= W . (m + i1) by A1, A2, A4, GLIB_001:36

.= W . j ; :: thesis: ( j = (m + i) - 1 & j <= len W )

thus j = (m + i) - 1 ; :: thesis: j <= len W

m + i <= (len (W .cut (m,n))) + m by A3, XREAL_1:7;

then m9 + i <= n9 + 1 by A1, A2, GLIB_001:36;

then (m + i) - 1 <= (n + 1) - 1 by XREAL_1:9;

hence j <= len W by A2, XXREAL_0:2; :: thesis: verum

for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds

ex j being odd Nat st

( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )

let W be Walk of G; :: thesis: for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds

ex j being odd Nat st

( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )

let m, n, i be odd Nat; :: thesis: ( m <= n & n <= len W & i <= len (W .cut (m,n)) implies ex j being odd Nat st

( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W ) )

assume that

A1: m <= n and

A2: n <= len W and

A3: i <= len (W .cut (m,n)) ; :: thesis: ex j being odd Nat st

( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )

set j = (m + i) - 1;

( m >= 1 & i >= 1 ) by ABIAN:12;

then m + i >= 1 + 1 by XREAL_1:7;

then (m + i) - 1 >= (1 + 1) - 1 by XREAL_1:9;

then (m + i) - 1 is odd Element of NAT by INT_1:3;

then reconsider j = (m + i) - 1 as odd Nat ;

take j ; :: thesis: ( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )

reconsider m9 = m, n9 = n as odd Element of NAT by ORDINAL1:def 12;

i >= 1 by ABIAN:12;

then i - 1 >= 1 - 1 by XREAL_1:9;

then reconsider i1 = i - 1 as Element of NAT by INT_1:3;

i < (len (W .cut (m,n))) + 1 by A3, NAT_1:13;

then A4: i1 < ((len (W .cut (m,n))) + 1) - 1 by XREAL_1:9;

thus (W .cut (m,n)) . i = (W .cut (m9,n9)) . (i1 + 1)

.= W . (m + i1) by A1, A2, A4, GLIB_001:36

.= W . j ; :: thesis: ( j = (m + i) - 1 & j <= len W )

thus j = (m + i) - 1 ; :: thesis: j <= len W

m + i <= (len (W .cut (m,n))) + m by A3, XREAL_1:7;

then m9 + i <= n9 + 1 by A1, A2, GLIB_001:36;

then (m + i) - 1 <= (n + 1) - 1 by XREAL_1:9;

hence j <= len W by A2, XXREAL_0:2; :: thesis: verum