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 m' = m, n' = 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 A3: ( x < y & y <= len (W .remove m,n) & (W .remove m,n) . x = (W .remove m,n) . y ) ; :: thesis: ( x = 1 & y = len (W .remove m,n) )
then A4: ( 1 <= x & 1 <= y & x <= len (W .remove m,n) ) by HEYTING3:1, XXREAL_0:2;
then A5: ( x in dom (W .remove m,n) & y in dom (W .remove m,n) ) by A3, FINSEQ_3:27;
A6: ( x <= len W & y <= len W ) by A1, A3, A4, XXREAL_0:2;

now

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

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

then A7: (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, A5, Lm34;

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

then (W .remove m,n) . y = W . y by A2, Lm29;
then ( x = 1 & y = len W ) by A3, A6, A7, Def28;
hence ( x = 1 & y = len (W .remove m,n) ) by A1, A3, XXREAL_0:1; :: thesis: verum

end;

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

then A9: ( (W .remove m,n) . y = W . ((y - m) + n) & (y - m) + n is Element of NAT & (y - m) + n <= len W ) by A2, Lm30;
reconsider y2 = (y - m') + n' as odd Element of NAT by A2, A8, Lm30;
(y - m) + n >= (y - m) + m by A2, XREAL_1:9;
then A10: ( x < y2 & y2 <= len W ) by A2, A3, A8, Lm30, XXREAL_0:2;
then ( x = 1 & y2 = len W ) by A3, A7, A9, 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 A3, A7, A9, A10, Def28; :: thesis: verum

end;

end;

end;

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

end;

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

then A12: ( (W .remove m,n) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W ) by A2, Lm30;
reconsider x2 = (x - m') + n' as odd Element of NAT by A2, A11, Lm30;

now

per cases ( y in Seg m or ( m <= y & y <= len (W .remove m,n) ) ) by A2, A5, 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, A11, XXREAL_0:2; :: thesis: verum

end;

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

then A14: ( (W .remove m,n) . y = W . ((y - m) + n) & (y - m) + n is Element of NAT & (y - m) + n <= len W ) by A2, Lm30;
reconsider y2 = (y - m') + n' as odd Element of NAT by A2, A13, Lm30;
x + (n - m) < y + (n - m) by A3, XREAL_1:10;
then A15: x2 < y2 ;
then A16: ( x2 = 1 & y2 = len W ) by A3, A12, A14, Def28;
then A17: (len (W .remove m,n)) + n = ((y - m) + n) + m by A2, Lm24
.= y + n ;
reconsider xm4 = x - m as Element of NAT by A11, INT_1:18;
1 <= n' by HEYTING3:1;
then x2 - n' <= 1 - 1 by A16, XREAL_1:15;
then A18: xm4 = 0 ;
then A19: m <= 1 by A2, A3, A12, A14, A15, Def28;
1 <= m' by HEYTING3:1;
hence ( x = 1 & y = len (W .remove m,n) ) by A17, A18, A19, 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