let G be _Graph; :: thesis: for W being Walk of G
for m, n being Element of NAT st not m is even & m <= n holds
(W .cut (1,n)) .cut (1,m) = W .cut (1,m)
let W be Walk of G; :: thesis: for m, n being Element of NAT st not m is even & m <= n holds
(W .cut (1,n)) .cut (1,m) = W .cut (1,m)
let m, n be Element of NAT ; :: thesis: ( not m is even & m <= n implies (W .cut (1,n)) .cut (1,m) = W .cut (1,m) )
set W1 = W .cut (1,n);
assume that
A1: not m is even and
A2: m <= n ; :: thesis: (W .cut (1,n)) .cut (1,m) = W .cut (1,m)

now

per cases ( ( not n is even & n <= len W ) or n is even or not n <= len W ) ;

suppose A3: ( not n is even & n <= len W ) ; :: thesis: (W .cut (1,n)) .cut (1,m) = W .cut (1,m)

A4: 1 <= m by A1, ABIAN:12;
A5: 1 <= n by A3, ABIAN:12;
then A6: (len (W .cut (1,n))) + 1 = n + 1 by A3, Lm15, JORDAN12:2;
then A7: (len ((W .cut (1,n)) .cut (1,m))) + 1 = m + 1 by A1, A2, A4, Lm15, JORDAN12:2;
A8: m <= len W by A2, A3, XXREAL_0:2;
then A9: W .cut (1,m) = (1,m) -cut W by A1, A4, Def11, JORDAN12:2;
A10: (len (W .cut (1,m))) + 1 = m + 1 by A1, A4, A8, Lm15, JORDAN12:2;
A11: W .cut (1,n) = (1,n) -cut W by A3, A5, Def11, JORDAN12:2;
A12: (W .cut (1,n)) .cut (1,m) = (1,m) -cut (W .cut (1,n)) by A1, A2, A4, A6, Def11, JORDAN12:2;

A13: now

let x be Nat; :: thesis: ( x in dom ((W .cut (1,n)) .cut (1,m)) implies ((W .cut (1,n)) .cut (1,m)) . x = (W .cut (1,m)) . x )
assume A14: x in dom ((W .cut (1,n)) .cut (1,m)) ; :: thesis: ((W .cut (1,n)) .cut (1,m)) . x = (W .cut (1,m)) . x
then A15: x <= m by A7, FINSEQ_3:25;
A16: 1 <= x by A14, FINSEQ_3:25;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:5;
A17: 1 <= m by A16, A15, XXREAL_0:2;
A18: xaa1 < (len (W .cut (1,m))) - 0 by A10, A15, XREAL_1:15;
x <= n by A2, A15, XXREAL_0:2;
then A19: xaa1 < (len (W .cut (1,n))) - 0 by A6, XREAL_1:15;
xaa1 < (len ((W .cut (1,n)) .cut (1,m))) - 0 by A7, A15, XREAL_1:15;
hence ((W .cut (1,n)) .cut (1,m)) . x = (W .cut (1,n)) . (1 + xaa1) by A2, A6, A12, A17, GRAPH_2:def 1
.= W . (1 + xaa1) by A3, A5, A11, A19, GRAPH_2:def 1
.= (W .cut (1,m)) . x by A4, A8, A9, A18, GRAPH_2:def 1 ;
:: thesis: verum

end;

(len (W .cut (1,m))) + 1 = m + 1 by A1, A4, A8, Lm15, JORDAN12:2;
hence (W .cut (1,n)) .cut (1,m) = W .cut (1,m) by A7, A13, FINSEQ_2:9; :: thesis: verum

end;

suppose ( n is even or not n <= len W ) ; :: thesis: (W .cut (1,n)) .cut (1,m) = W .cut (1,m)

hence (W .cut (1,n)) .cut (1,m) = W .cut (1,m) by Def11; :: thesis: verum

end;

end;

end;

hence (W .cut (1,n)) .cut (1,m) = W .cut (1,m) ; :: thesis: verum