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:3;
then A7: (len ((W .cut 1,n) .cut 1,m)) + 1 = m + 1 by A1, A2, A4, Lm15, JORDAN12:3;
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:3;
A10: (len (W .cut 1,m)) + 1 = m + 1 by A1, A4, A8, Lm15, JORDAN12:3;
A11: W .cut 1,n = 1,n -cut W by A3, A5, Def11, JORDAN12:3;
A12: (W .cut 1,n) .cut 1,m = 1,m -cut (W .cut 1,n) by A1, A2, A4, A6, Def11, JORDAN12:3;

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:27;
A16: 1 <= x by A14, FINSEQ_3:27;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:18;
A17: 1 <= m by A16, A15, XXREAL_0:2;
A18: xaa1 < (len (W .cut 1,m)) - 0 by A10, A15, XREAL_1:17;
x <= n by A2, A15, XXREAL_0:2;
then A19: xaa1 < (len (W .cut 1,n)) - 0 by A6, XREAL_1:17;
xaa1 < (len ((W .cut 1,n) .cut 1,m)) - 0 by A7, A15, XREAL_1:17;
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:3;
hence (W .cut 1,n) .cut 1,m = W .cut 1,m by A7, A13, FINSEQ_2:10; :: 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