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

A1: len (W .remove (m,n)) <= len W by Lm26;

A1: len (W .remove (m,n)) <= len W by Lm26;

now :: thesis: W .remove (m,n) is Path-like end;

hence
W .remove (m,n) is Path-like
; :: thesis: verumper 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 )
;

end;

suppose A2:
( m is odd & n is odd & m <= n & n <= len W & W . m = W . n )
; :: thesis: W .remove (m,n) is Path-like

then reconsider m9 = m, n9 = n as odd Element of NAT ;

end;now :: thesis: 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)) )

hence
W .remove (m,n) is Path-like
; :: thesis: verum( x = 1 & y = len (W .remove (m,n)) )

let x, y be odd Element of NAT ; :: thesis: ( 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 ; :: thesis: ( 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;

end;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 ; :: thesis: ( 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 :: thesis: ( x = 1 & y = len (W .remove (m,n)) )end;

hence
( x = 1 & y = len (W .remove (m,n)) )
; :: thesis: verumper cases
( x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) )
by A2, A7, Lm34;

end;

suppose
x in Seg m
; :: thesis: ( x = 1 & y = len (W .remove (m,n)) )

then A10:
(W .remove (m,n)) . x = W . x
by A2, Lm29;

end;now :: thesis: ( x = 1 & y = len (W .remove (m,n)) )end;

hence
( x = 1 & y = len (W .remove (m,n)) )
; :: thesis: verumper cases
( y in Seg m or ( m <= y & y <= len (W .remove (m,n)) ) )
by A2, A8, Lm34;

end;

suppose
y in Seg m
; :: thesis: ( 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; :: thesis: verum

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

suppose A12:
( m <= y & y <= len (W .remove (m,n)) )
; :: thesis: ( 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; :: thesis: verum

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

suppose A16:
( m <= x & x <= len (W .remove (m,n)) )
; :: thesis: ( 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;

end;A17: (W .remove (m,n)) . x = W . ((x - m) + n) by A2, A16, Lm30;

now :: thesis: ( x = 1 & y = len (W .remove (m,n)) )end;

hence
( x = 1 & y = len (W .remove (m,n)) )
; :: thesis: verumper cases
( y in Seg m or ( m <= y & y <= len (W .remove (m,n)) ) )
by A2, A8, Lm34;

end;

suppose
y in Seg m
; :: thesis: ( x = 1 & y = len (W .remove (m,n)) )

then
y <= m
by FINSEQ_1:1;

hence ( x = 1 & y = len (W .remove (m,n)) ) by A3, A16, XXREAL_0:2; :: thesis: verum

end;hence ( x = 1 & y = len (W .remove (m,n)) ) by A3, A16, XXREAL_0:2; :: thesis: verum

suppose A18:
( m <= y & y <= len (W .remove (m,n)) )
; :: thesis: ( 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; :: thesis: verum

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