set W2 = W .remove (m,n);
A1:
len (W .remove (m,n)) <= len W
by Lm26;
now W .remove (m,n) is Path-like per cases
( ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n ) or not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n )
;
suppose A2:
(
m is
odd &
n is
odd &
m <= n &
n <= len W &
W . m = W . n )
;
W .remove (m,n) is Path-like then reconsider m9 =
m,
n9 =
n as
odd Element of
NAT ;
now for x, y being odd Element of NAT st x < y & y <= len (W .remove (m,n)) & (W .remove (m,n)) . x = (W .remove (m,n)) . y holds
( x = 1 & y = len (W .remove (m,n)) )let x,
y be
odd Element of
NAT ;
( x < y & y <= len (W .remove (m,n)) & (W .remove (m,n)) . x = (W .remove (m,n)) . y implies ( x = 1 & y = len (W .remove (m,n)) ) )assume that A3:
x < y
and A4:
y <= len (W .remove (m,n))
and A5:
(W .remove (m,n)) . x = (W .remove (m,n)) . y
;
( x = 1 & y = len (W .remove (m,n)) )A6:
1
<= x
by ABIAN:12;
x <= len (W .remove (m,n))
by A3, A4, XXREAL_0:2;
then A7:
x in dom (W .remove (m,n))
by A6, FINSEQ_3:25;
1
<= y
by ABIAN:12;
then A8:
y in dom (W .remove (m,n))
by A4, FINSEQ_3:25;
A9:
y <= len W
by A1, A4, XXREAL_0:2;
now ( x = 1 & y = len (W .remove (m,n)) )per cases
( x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) )
by A2, A7, Lm34;
suppose
x in Seg m
;
( x = 1 & y = len (W .remove (m,n)) )then A10:
(W .remove (m,n)) . x = W . x
by A2, Lm29;
now ( x = 1 & y = len (W .remove (m,n)) )per cases
( y in Seg m or ( m <= y & y <= len (W .remove (m,n)) ) )
by A2, A8, Lm34;
suppose
y in Seg m
;
( x = 1 & y = len (W .remove (m,n)) )then A11:
(W .remove (m,n)) . y = W . y
by A2, Lm29;
then
y = len W
by A3, A5, A9, A10, Def28;
hence
(
x = 1 &
y = len (W .remove (m,n)) )
by A1, A3, A4, A5, A10, A11, Def28, XXREAL_0:1;
verum end; suppose A12:
(
m <= y &
y <= len (W .remove (m,n)) )
;
( x = 1 & y = len (W .remove (m,n)) )then A13:
(y - m) + n <= len W
by A2, Lm30;
A14:
(W .remove (m,n)) . y = W . ((y - m) + n)
by A2, A12, Lm30;
reconsider y2 =
(y - m9) + n9 as
odd Element of
NAT by A2, A12, Lm30;
(y - m) + n >= (y - m) + m
by A2, XREAL_1:7;
then A15:
x < y2
by A3, XXREAL_0:2;
y2 <= len W
by A2, A12, Lm30;
then
y2 = len W
by A5, A10, A14, A15, Def28;
then (len (W .remove (m,n))) + n =
((y - m) + n) + m
by A2, Lm24
.=
y + n
;
hence
(
x = 1 &
y = len (W .remove (m,n)) )
by A5, A10, A14, A13, A15, Def28;
verum end; end; end; hence
(
x = 1 &
y = len (W .remove (m,n)) )
;
verum end; suppose A16:
(
m <= x &
x <= len (W .remove (m,n)) )
;
( x = 1 & y = len (W .remove (m,n)) )then reconsider x2 =
(x - m9) + n9 as
odd Element of
NAT by A2, Lm30;
A17:
(W .remove (m,n)) . x = W . ((x - m) + n)
by A2, A16, Lm30;
now ( x = 1 & y = len (W .remove (m,n)) )per cases
( y in Seg m or ( m <= y & y <= len (W .remove (m,n)) ) )
by A2, A8, Lm34;
suppose A18:
(
m <= y &
y <= len (W .remove (m,n)) )
;
( x = 1 & y = len (W .remove (m,n)) )then reconsider y2 =
(y - m9) + n9 as
odd Element of
NAT by A2, Lm30;
x + (n - m) < y + (n - m)
by A3, XREAL_1:8;
then A19:
x2 < y2
;
reconsider xm4 =
x - m as
Element of
NAT by A16, INT_1:5;
A20:
1
<= n9
by ABIAN:12;
A21:
1
<= m9
by ABIAN:12;
A22:
(y - m) + n <= len W
by A2, A18, Lm30;
A23:
(W .remove (m,n)) . y = W . ((y - m) + n)
by A2, A18, Lm30;
then
y2 = len W
by A5, A17, A22, A19, Def28;
then A24:
(len (W .remove (m,n))) + n =
((y - m) + n) + m
by A2, Lm24
.=
y + n
;
x2 = 1
by A5, A17, A23, A22, A19, Def28;
then
x2 - n9 <= 1
- 1
by A20, XREAL_1:13;
then A25:
xm4 = 0
;
then
m <= 1
by A2, A5, A17, A23, A22, A19, Def28;
hence
(
x = 1 &
y = len (W .remove (m,n)) )
by A24, A25, A21, XXREAL_0:1;
verum end; end; end; hence
(
x = 1 &
y = len (W .remove (m,n)) )
;
verum end; end; end; hence
(
x = 1 &
y = len (W .remove (m,n)) )
;
verum end; hence
W .remove (
m,
n) is
Path-like
;
verum end; end; end;
hence
W .remove (m,n) is Path-like
; verum