set W2 = W .cut (m,n);
now W .cut (m,n) is vertex-distinct per 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 )
;
suppose A1:
(
m is
odd &
n is
odd &
m <= n &
n <= len W )
;
W .cut (m,n) is vertex-distinct then reconsider m9 =
m as
odd Element of
NAT ;
now 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 = blet a,
b be
odd Element of
NAT ;
( 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
;
a = breconsider 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
;
verum end; hence
W .cut (
m,
n) is
vertex-distinct
;
verum end; end; end;
hence
W .cut (m,n) is vertex-distinct
; verum