let G be _Graph; 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; 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 ; ( 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
; 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 ; ( 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))
; ( (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; ( (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; (x - m) + n <= len W
thus
(x - m) + n <= len W
by A7, A8, A9; verum