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