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 vertex-distinct

then reconsider m9 = m as odd Element of NAT ;

now

let a, b be odd Element of NAT ; :: thesis: ( a <= len (W .cut m,n) & b <= len (W .cut m,n) & (W .cut m,n) . a = (W .cut m,n) . b implies a = b )
assume that
A2: a <= len (W .cut m,n) and
A3: b <= len (W .cut m,n) and
A4: (W .cut m,n) . a = (W .cut m,n) . b ; :: thesis: a = b
reconsider aaa1 = a - 1, baa1 = b - 1 as even Element of NAT by HEYTING3:1, INT_1:18;
A5: baa1 < (len (W .cut m,n)) - 0 by A3, XREAL_1:17;
then A6: (W .cut m,n) . (baa1 + 1) = W . (m + baa1) by A1, Lm15;
A7: aaa1 < (len (W .cut m,n)) - 0 by A2, XREAL_1:17;
then m + aaa1 in dom W by A1, Lm15;
then A8: m9 + aaa1 <= len W by FINSEQ_3:27;
m + baa1 in dom W by A1, A5, Lm15;
then A9: m9 + baa1 <= len W by FINSEQ_3:27;
(W .cut m,n) . (aaa1 + 1) = W . (m + aaa1) by A1, A7, Lm15;
then aaa1 + m9 = baa1 + m9 by A4, A6, A8, A9, Def29;
hence a = b ; :: thesis: verum

end;

hence W .cut m,n is vertex-distinct by Def29; :: 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 vertex-distinct

hence W .cut m,n is vertex-distinct by Def11; :: thesis: verum

end;

end;

end;

hence W .cut m,n is vertex-distinct ; :: thesis: verum