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

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

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

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)) )

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;

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

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

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

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 :: thesis: ( 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 ; :: 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;

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;

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

end;

suppose ( not m is odd or not n is odd 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