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

( (W .cut (m,n)) .first() = W . m & (W .cut (m,n)) .last() = W . n & W .cut (m,n) is_Walk_from W . m,W . n )

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

( (W .cut (m,n)) .first() = W . m & (W .cut (m,n)) .last() = W . n & W .cut (m,n) is_Walk_from W . m,W . n )

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W implies ( (W .cut (m,n)) .first() = W . m & (W .cut (m,n)) .last() = W . n & W .cut (m,n) is_Walk_from W . m,W . n ) )

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

assume that

A1: m <= n and

A2: n <= len W ; :: thesis: ( (W .cut (m,n)) .first() = W . m & (W .cut (m,n)) .last() = W . n & W .cut (m,n) is_Walk_from W . m,W . n )

1 - 1 < (len (W .cut (m,n))) - 0 ;

then (W .cut (m,n)) . (0 + 1) = W . (m + 0) by A1, A2, Lm15;

hence A3: (W .cut (m,n)) .first() = W . m ; :: thesis: ( (W .cut (m,n)) .last() = W . n & W .cut (m,n) is_Walk_from W . m,W . n )

reconsider nm4 = n - m as Element of NAT by A1, INT_1:5;

A4: ((len (W .cut (m,n))) + m) - m = (n + 1) - m by A1, A2, Lm15;

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

then nm4 < len (W .cut (m,n)) ;

then (W .cut (m,n)) . ((n - m) + 1) = W . (m + (n - m)) by A1, A2, Lm15;

hence (W .cut (m,n)) .last() = W . n by A4; :: thesis: W .cut (m,n) is_Walk_from W . m,W . n

hence W .cut (m,n) is_Walk_from W . m,W . n by A3; :: thesis: verum

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

( (W .cut (m,n)) .first() = W . m & (W .cut (m,n)) .last() = W . n & W .cut (m,n) is_Walk_from W . m,W . n )

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

( (W .cut (m,n)) .first() = W . m & (W .cut (m,n)) .last() = W . n & W .cut (m,n) is_Walk_from W . m,W . n )

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W implies ( (W .cut (m,n)) .first() = W . m & (W .cut (m,n)) .last() = W . n & W .cut (m,n) is_Walk_from W . m,W . n ) )

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

assume that

A1: m <= n and

A2: n <= len W ; :: thesis: ( (W .cut (m,n)) .first() = W . m & (W .cut (m,n)) .last() = W . n & W .cut (m,n) is_Walk_from W . m,W . n )

1 - 1 < (len (W .cut (m,n))) - 0 ;

then (W .cut (m,n)) . (0 + 1) = W . (m + 0) by A1, A2, Lm15;

hence A3: (W .cut (m,n)) .first() = W . m ; :: thesis: ( (W .cut (m,n)) .last() = W . n & W .cut (m,n) is_Walk_from W . m,W . n )

reconsider nm4 = n - m as Element of NAT by A1, INT_1:5;

A4: ((len (W .cut (m,n))) + m) - m = (n + 1) - m by A1, A2, Lm15;

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

then nm4 < len (W .cut (m,n)) ;

then (W .cut (m,n)) . ((n - m) + 1) = W . (m + (n - m)) by A1, A2, Lm15;

hence (W .cut (m,n)) .last() = W . n by A4; :: thesis: W .cut (m,n) is_Walk_from W . m,W . n

hence W .cut (m,n) is_Walk_from W . m,W . n by A3; :: thesis: verum