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

now

per cases ( ( not m is even & not n is even & m <= n & n <= len W & W . m = W . n ) or m is even or n is even or not m <= n or not n <= len W or not W . m = W . n ) ;

suppose A2: ( not m is even & not n is even & 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 ;

now

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:27;
1 <= y by ABIAN:12;
then A8: y in dom (W .remove m,n) by A4, FINSEQ_3:27;
A9: y <= len W by A1, A4, XXREAL_0:2;

now

per cases ( x in Seg m or ( m <= x & x <= len (W .remove m,n) ) ) by A2, A7, Lm34;

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;

now

per cases ( y in Seg m or ( m <= y & y <= len (W .remove m,n) ) ) by A2, A8, Lm34;

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;

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

end;

end;

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

end;

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;

now

per cases ( y in Seg m or ( m <= y & y <= len (W .remove m,n) ) ) by A2, A8, Lm34;

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

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

end;

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:10;
then A19: x2 < y2 ;
reconsider xm4 = x - m as Element of NAT by A16, INT_1:18;
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:15;
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;

end;

end;

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

end;

end;

end;

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

end;

hence W .remove m,n is Path-like by Def28; :: thesis: verum

end;

suppose ( m is even or n is even or not m <= n or not n <= len W or not W . m = W . n ) ; :: thesis: W .remove m,n is Path-like

hence W .remove m,n is Path-like by Def12; :: thesis: verum

end;

end;

end;

hence W .remove m,n is Path-like ; :: thesis: verum