let G be _Graph; :: thesis: for W being Walk of G
for m, n being Element of NAT st m is odd & 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 m is odd & m <= n holds
(W .cut (1,n)) .cut (1,m) = W .cut (1,m)

let m, n be Element of NAT ; :: thesis: ( m is odd & m <= n implies (W .cut (1,n)) .cut (1,m) = W .cut (1,m) )
set W1 = W .cut (1,n);
assume that
A1: m is odd and
A2: m <= n ; :: thesis: (W .cut (1,n)) .cut (1,m) = W .cut (1,m)
now :: thesis: (W .cut (1,n)) .cut (1,m) = W .cut (1,m)
per cases ( ( n is odd & n <= len W ) or not n is odd or not n <= len W ) ;
suppose A3: ( n is odd & n <= len W ) ; :: thesis: (W .cut (1,n)) .cut (1,m) = W .cut (1,m)
A4: 1 <= m by ;
A5: 1 <= n by ;
then A6: (len (W .cut (1,n))) + 1 = n + 1 by ;
then A7: (len ((W .cut (1,n)) .cut (1,m))) + 1 = m + 1 by ;
A8: m <= len W by ;
then A9: W .cut (1,m) = (1,m) -cut W by ;
A10: (len (W .cut (1,m))) + 1 = m + 1 by ;
A11: W .cut (1,n) = (1,n) -cut W by ;
A12: (W .cut (1,n)) .cut (1,m) = (1,m) -cut (W .cut (1,n)) by ;
A13: now :: thesis: for x being Nat st x in dom ((W .cut (1,n)) .cut (1,m)) holds
((W .cut (1,n)) .cut (1,m)) . x = (W .cut (1,m)) . x
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 ;
A16: 1 <= x by ;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:5;
A17: 1 <= m by ;
A18: xaa1 < (len (W .cut (1,m))) - 0 by ;
x <= n by ;
then A19: xaa1 < (len (W .cut (1,n))) - 0 by ;
xaa1 < (len ((W .cut (1,n)) .cut (1,m))) - 0 by ;
hence ((W .cut (1,n)) .cut (1,m)) . x = (W .cut (1,n)) . (1 + xaa1) by
.= W . (1 + xaa1) by
.= (W .cut (1,m)) . x by ;
:: thesis: verum
end;
(len (W .cut (1,m))) + 1 = m + 1 by ;
hence (W .cut (1,n)) .cut (1,m) = W .cut (1,m) by ; :: thesis: verum
end;
suppose ( not n is odd 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