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)

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)end;

hence
(W .cut (1,n)) .cut (1,m) = W .cut (1,m)
; :: thesis: verumper cases
( ( n is odd & n <= len W ) or not n is odd or not n <= len W )
;

end;

suppose A3:
( n is odd & 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;

hence (W .cut (1,n)) .cut (1,m) = W .cut (1,m) by A7, A13, FINSEQ_2:9; :: thesis: verum

end;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 :: 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

(len (W .cut (1,m))) + 1 = m + 1
by A1, A4, A8, Lm15, JORDAN12:2;((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 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, FINSEQ_6:def 4

.= W . (1 + xaa1) by A3, A5, A11, A19, FINSEQ_6:def 4

.= (W .cut (1,m)) . x by A4, A8, A9, A18, FINSEQ_6:def 4 ;

:: thesis: verum

end;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, FINSEQ_6:def 4

.= W . (1 + xaa1) by A3, A5, A11, A19, FINSEQ_6:def 4

.= (W .cut (1,m)) . x by A4, A8, A9, A18, FINSEQ_6:def 4 ;

:: thesis: verum

hence (W .cut (1,n)) .cut (1,m) = W .cut (1,m) by A7, A13, FINSEQ_2:9; :: thesis: verum