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

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

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

now :: thesis: for a, b being even Element of NAT holds
( not 1 <= a or not a < b or not b <= len (W .remove (m,n)) or not (W .remove (m,n)) . a = (W .remove (m,n)) . b )

given a, b being even Element of NAT such that A3: 1 <= a and
A4: a < b and
A5: b <= len (W .remove (m,n)) and
A6: (W .remove (m,n)) . a = (W .remove (m,n)) . b ; :: thesis: contradiction
1 <= b by A3, A4, XXREAL_0:2;
then A7: b in dom (W .remove (m,n)) by A5, FINSEQ_3:25;
a <= len (W .remove (m,n)) by A4, A5, XXREAL_0:2;
then A8: a in dom (W .remove (m,n)) by A3, FINSEQ_3:25;

now :: thesis: contradiction

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

suppose a in Seg m ; :: thesis: contradiction

then A9: (W .remove (m,n)) . a = W . a by A2, Lm29;

now :: thesis: contradiction

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

suppose A10: b in Seg m ; :: thesis: contradiction

A11: b <= len W by A1, A5, XXREAL_0:2;
(W .remove (m,n)) . b = W . b by A2, A10, Lm29;
hence contradiction by A3, A4, A6, A9, A11, Lm57; :: thesis: verum

end;

suppose A12: ( m <= b & b <= len (W .remove (m,n)) ) ; :: thesis: contradiction

then reconsider b2 = (b - m9) + n9 as even Element of NAT by A2, Lm30;
A13: b2 <= len W by A2, A12, Lm30;
A14: (W .remove (m,n)) . b = W . b2 by A2, A12, Lm30;

now :: thesis: contradiction

per cases ( a < b2 or b2 <= a ) ;

suppose a < b2 ; :: thesis: contradiction

hence contradiction by A3, A6, A9, A14, A13, Lm57; :: thesis: verum

end;

suppose A15: b2 <= a ; :: thesis: contradiction

A16: n - m >= m - m by A2, XREAL_1:13;
A17: a - b < b - b by A4, XREAL_1:14;
((n - m) + b) - b <= a - b by A15, XREAL_1:13;
then 0 <= a - b by A16;
hence contradiction by A17; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A18: ( m <= a & a <= len (W .remove (m,n)) ) ; :: thesis: contradiction

then reconsider a2 = (a - m9) + n9 as even Element of NAT by A2, Lm30;
reconsider nm4 = n9 - m9 as even Element of NAT by A2, INT_1:5;
A19: (W .remove (m,n)) . a = W . a2 by A2, A18, Lm30;

now :: thesis: contradiction

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

suppose b in Seg m ; :: thesis: contradiction

then b <= m by FINSEQ_1:1;
hence contradiction by A4, A18, XXREAL_0:2; :: thesis: verum

end;

suppose A20: ( m <= b & b <= len (W .remove (m,n)) ) ; :: thesis: contradiction

then reconsider b2 = (b - m9) + n9 as even Element of NAT by A2, Lm30;
A21: b2 <= len W by A2, A20, Lm30;
A22: (W .remove (m,n)) . b = W . b2 by A2, A20, Lm30;

now :: thesis: contradiction

per cases ( a2 < b2 or b2 <= a2 ) ;

suppose A23: a2 < b2 ; :: thesis: contradiction

1 <= m9 by ABIAN:12;
then 1 <= a by A18, XXREAL_0:2;
then 1 <= a + nm4 by NAT_1:12;
hence contradiction by A6, A19, A22, A21, A23, Lm57; :: thesis: verum

end;

suppose b2 <= a2 ; :: thesis: contradiction

then b + nm4 <= a + nm4 ;
hence contradiction by A4, XREAL_1:6; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence W .remove (m,n) is Trail-like by Lm57; :: 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 Trail-like

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

end;

end;

end;

hence W .remove (m,n) is Trail-like ; :: thesis: verum