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 Trail-like end;

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

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

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

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

end;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: contradictionend;

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

end;

suppose
a in Seg m
; :: thesis: contradiction

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

end;now :: thesis: contradictionend;

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

end;

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;(W .remove (m,n)) . b = W . b by A2, A10, Lm29;

hence contradiction by A3, A4, A6, A9, A11, Lm57; :: thesis: verum

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;

end;A13: b2 <= len W by A2, A12, Lm30;

A14: (W .remove (m,n)) . b = W . b2 by A2, A12, Lm30;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumsuppose 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;

end;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: contradictionend;

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

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;

end;A21: b2 <= len W by A2, A20, Lm30;

A22: (W .remove (m,n)) . b = W . b2 by A2, A20, Lm30;

now :: thesis: contradiction

hence
contradiction
; :: thesis: verumend;

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

end;

end;