set W2 = W .cut (m,n);

now

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

suppose A1: ( not m is even & not n is even & m <= n & n <= len W ) ; :: thesis: W .cut (m,n) is trivial

then A2: 1 <= n by ABIAN:12;
n <= 1 by A1, Lm55;
then A3: n = 1 by A2, XXREAL_0:1;
A4: 1 <= m by A1, ABIAN:12;
(len (W .cut (m,n))) + m = n + 1 by A1, Lm15;
then (len (W .cut (m,n))) + 1 = 1 + 1 by A1, A4, A3, XXREAL_0:1;
hence W .cut (m,n) is trivial by Lm55; :: thesis: verum

end;

suppose ( m is even or n is even or not m <= n or not n <= len W ) ; :: thesis: W .cut (m,n) is trivial

hence W .cut (m,n) is trivial by Def11; :: thesis: verum

end;

end;

end;

hence W .cut (m,n) is trivial ; :: thesis: verum