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

now :: thesis: W .cut (m,n) is vertex-distinct end;

hence
W .cut (m,n) is vertex-distinct
; :: thesis: verumper cases
( ( m is odd & n is odd & m <= n & n <= len W ) or not m is odd or not n is odd or not m <= n or not n <= len W )
;

end;

suppose A1:
( m is odd & n is odd & m <= n & n <= len W )
; :: thesis: W .cut (m,n) is vertex-distinct

then reconsider m9 = m as odd Element of NAT ;

end;now :: thesis: for a, b being odd Element of NAT st a <= len (W .cut (m,n)) & b <= len (W .cut (m,n)) & (W .cut (m,n)) . a = (W .cut (m,n)) . b holds

a = b

hence
W .cut (m,n) is vertex-distinct
; :: thesis: veruma = b

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 ABIAN:12, INT_1:5;

A5: baa1 < (len (W .cut (m,n))) - 0 by A3, XREAL_1:15;

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:15;

then m + aaa1 in dom W by A1, Lm15;

then A8: m9 + aaa1 <= len W by FINSEQ_3:25;

m + baa1 in dom W by A1, A5, Lm15;

then A9: m9 + baa1 <= len W by FINSEQ_3:25;

(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;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 ABIAN:12, INT_1:5;

A5: baa1 < (len (W .cut (m,n))) - 0 by A3, XREAL_1:15;

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:15;

then m + aaa1 in dom W by A1, Lm15;

then A8: m9 + aaa1 <= len W by FINSEQ_3:25;

m + baa1 in dom W by A1, A5, Lm15;

then A9: m9 + baa1 <= len W by FINSEQ_3:25;

(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

suppose
( not m is odd or not n is odd or not m <= n or not n <= len W )
; :: thesis: W .cut (m,n) is vertex-distinct

end;

end;