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 & W . m = W . n holds

for x being Element of NAT st m <= x & x <= len (W .remove (m,n)) holds

( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W )

let W be Walk of G; :: thesis: for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

for x being Element of NAT st m <= x & x <= len (W .remove (m,n)) holds

( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W )

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W & W . m = W . n implies for x being Element of NAT st m <= x & x <= len (W .remove (m,n)) holds

( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W ) )

set W2 = W .remove (m,n);

set WA = W .cut (1,m);

set WB = W .cut (n,(len W));

assume that

A1: m <= n and

A2: n <= len W and

A3: W . m = W . n ; :: thesis: for x being Element of NAT st m <= x & x <= len (W .remove (m,n)) holds

( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W )

A4: (W .cut (1,m)) .last() = (W .cut (n,(len W))) .first() by A1, A2, A3, Lm28;

let x be Element of NAT ; :: thesis: ( m <= x & x <= len (W .remove (m,n)) implies ( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W ) )

assume that

A5: m <= x and

A6: x <= len (W .remove (m,n)) ; :: thesis: ( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W )

A7: len (W .cut (1,m)) = m by A1, A2, Lm22, XXREAL_0:2;

then consider a being Nat such that

A8: (len (W .cut (1,m))) + a = x by A5, NAT_1:10;

reconsider a = a as Element of NAT by ORDINAL1:def 12;

(len (W .remove (m,n))) + n = (len W) + m by A1, A2, A3, Lm24;

then (m + a) + n <= m + (len W) by A7, A6, A8, XREAL_1:7;

then A9: ((a + n) + m) - m <= ((len W) + m) - m by XREAL_1:13;

(len (W .cut (n,(len W)))) + n = (len W) + 1 by A2, Lm15;

then (a + n) + 1 <= (len (W .cut (n,(len W)))) + n by A9, XREAL_1:7;

then ((a + 1) + n) - n <= ((len (W .cut (n,(len W)))) + n) - n by XREAL_1:13;

then A10: (a + 1) - 1 < ((len (W .cut (n,(len W)))) + 1) - 1 by NAT_1:13;

W .remove (m,n) = (W .cut (1,m)) .append (W .cut (n,(len W))) by A1, A2, A3, Def12;

then (W .remove (m,n)) . x = (W .cut (n,(len W))) . (a + 1) by A4, A8, A10, Lm13

.= W . (a + n) by A2, A10, Lm15 ;

hence (W .remove (m,n)) . x = W . ((x - m) + n) by A7, A8; :: thesis: ( (x - m) + n is Element of NAT & (x - m) + n <= len W )

a + n is Element of NAT ;

hence (x - m) + n is Element of NAT by A7, A8; :: thesis: (x - m) + n <= len W

thus (x - m) + n <= len W by A7, A8, A9; :: thesis: verum

for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

for x being Element of NAT st m <= x & x <= len (W .remove (m,n)) holds

( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W )

let W be Walk of G; :: thesis: for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

for x being Element of NAT st m <= x & x <= len (W .remove (m,n)) holds

( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W )

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W & W . m = W . n implies for x being Element of NAT st m <= x & x <= len (W .remove (m,n)) holds

( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W ) )

set W2 = W .remove (m,n);

set WA = W .cut (1,m);

set WB = W .cut (n,(len W));

assume that

A1: m <= n and

A2: n <= len W and

A3: W . m = W . n ; :: thesis: for x being Element of NAT st m <= x & x <= len (W .remove (m,n)) holds

( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W )

A4: (W .cut (1,m)) .last() = (W .cut (n,(len W))) .first() by A1, A2, A3, Lm28;

let x be Element of NAT ; :: thesis: ( m <= x & x <= len (W .remove (m,n)) implies ( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W ) )

assume that

A5: m <= x and

A6: x <= len (W .remove (m,n)) ; :: thesis: ( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W )

A7: len (W .cut (1,m)) = m by A1, A2, Lm22, XXREAL_0:2;

then consider a being Nat such that

A8: (len (W .cut (1,m))) + a = x by A5, NAT_1:10;

reconsider a = a as Element of NAT by ORDINAL1:def 12;

(len (W .remove (m,n))) + n = (len W) + m by A1, A2, A3, Lm24;

then (m + a) + n <= m + (len W) by A7, A6, A8, XREAL_1:7;

then A9: ((a + n) + m) - m <= ((len W) + m) - m by XREAL_1:13;

(len (W .cut (n,(len W)))) + n = (len W) + 1 by A2, Lm15;

then (a + n) + 1 <= (len (W .cut (n,(len W)))) + n by A9, XREAL_1:7;

then ((a + 1) + n) - n <= ((len (W .cut (n,(len W)))) + n) - n by XREAL_1:13;

then A10: (a + 1) - 1 < ((len (W .cut (n,(len W)))) + 1) - 1 by NAT_1:13;

W .remove (m,n) = (W .cut (1,m)) .append (W .cut (n,(len W))) by A1, A2, A3, Def12;

then (W .remove (m,n)) . x = (W .cut (n,(len W))) . (a + 1) by A4, A8, A10, Lm13

.= W . (a + n) by A2, A10, Lm15 ;

hence (W .remove (m,n)) . x = W . ((x - m) + n) by A7, A8; :: thesis: ( (x - m) + n is Element of NAT & (x - m) + n <= len W )

a + n is Element of NAT ;

hence (x - m) + n is Element of NAT by A7, A8; :: thesis: (x - m) + n <= len W

thus (x - m) + n <= len W by A7, A8, A9; :: thesis: verum