let f be S-Sequence_in_R2; for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f /. (len f) in L~ (mid (f,k1,k2)) & not k1 = len f holds
k2 = len f
let k1, k2 be Nat; ( 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f /. (len f) in L~ (mid (f,k1,k2)) & not k1 = len f implies k2 = len f )
assume that
A1:
1 <= k1
and
A2:
k1 <= len f
and
A3:
1 <= k2
and
A4:
k2 <= len f
and
A5:
f /. (len f) in L~ (mid (f,k1,k2))
; ( k1 = len f or k2 = len f )
AA:
k1 in dom f
by A1, A2, FINSEQ_3:25;
assume that
A6:
k1 <> len f
and
A7:
k2 <> len f
; contradiction
consider j being Nat such that
A8:
1 <= j
and
A9:
j + 1 <= len (mid (f,k1,k2))
and
A10:
f /. (len f) in LSeg ((mid (f,k1,k2)),j)
by A5, SPPOL_2:13;
per cases
( k1 < k2 or k1 > k2 or k1 = k2 )
by XXREAL_0:1;
suppose A11:
k1 < k2
;
contradictionthen A12:
len (mid (f,k1,k2)) = (k2 -' k1) + 1
by A1, A2, A3, A4, FINSEQ_6:118;
then A13:
j < (k2 -' k1) + 1
by A9, NAT_1:13;
A14:
j + k1 >= 1
+ 1
by A1, A8, XREAL_1:7;
then A15:
(j + k1) - 1
>= (1 + 1) - 1
by XREAL_1:9;
then A16:
(j + k1) -' 1
= (j + k1) - 1
by XREAL_0:def 2;
k2 - k1 > 0
by A11, XREAL_1:50;
then A17:
k2 -' k1 = k2 - k1
by XREAL_0:def 2;
then
j - 1
< k2 - k1
by A13, XREAL_1:19;
then
(j - 1) + k1 < k2
by XREAL_1:20;
then A18:
(j + k1) - 1
< len f
by A4, XXREAL_0:2;
then A19:
(j + k1) -' 1
in dom f
by A15, A16, FINSEQ_3:25;
A20:
j + k1 >= 1
by A14, XXREAL_0:2;
((j + k1) - 1) + 1
<= len f
by A16, A18, NAT_1:13;
then
j + k1 in Seg (len f)
by A20, FINSEQ_1:1;
then A21:
((j + k1) -' 1) + 1
in dom f
by A16, FINSEQ_1:def 3;
LSeg (
(mid (f,k1,k2)),
j)
= LSeg (
f,
((j + k1) -' 1))
by A1, A4, A8, A11, A13, JORDAN4:19;
then A22:
((j + k1) -' 1) + 1
= len f
by A10, A19, A21, GOBOARD2:2;
A23:
(j + k1) -' 1
= (j + k1) - 1
by A15, XREAL_0:def 2;
j < (k2 + 1) - k1
by A9, A17, A12, NAT_1:13;
then
len f < k2 + 1
by A22, A23, XREAL_1:20;
then
len f <= k2
by NAT_1:13;
hence
contradiction
by A4, A7, XXREAL_0:1;
verum end; suppose A24:
k1 > k2
;
contradictionthen
len (mid (f,k1,k2)) = (k1 -' k2) + 1
by A1, A2, A3, A4, FINSEQ_6:118;
then A25:
j < (k1 -' k2) + 1
by A9, NAT_1:13;
k1 - k2 > 0
by A24, XREAL_1:50;
then
k1 -' k2 = k1 - k2
by XREAL_0:def 2;
then
j - 1
< k1 - k2
by A25, XREAL_1:19;
then
(j - 1) + k2 < k1
by XREAL_1:20;
then A26:
j + (- (1 - k2)) < k1
;
then A27:
- (1 - k2) < k1 - j
by XREAL_1:20;
A28:
k2 - 1
>= 0
by A3, XREAL_1:48;
then A29:
(k1 - j) + 1
> 0 + 1
by A27, XREAL_1:6;
k2 - 1
< k1 - j
by A26, XREAL_1:20;
then A30:
k1 - j > 0
by A3, XREAL_1:48;
then A31:
k1 -' j = k1 - j
by XREAL_0:def 2;
k1 - j <= k1 - 1
by A8, XREAL_1:10;
then
(k1 - j) + 1
<= (k1 - 1) + 1
by XREAL_1:7;
then
k1 - j < k1
by A31, NAT_1:13;
then A32:
k1 - j < len f
by A2, XXREAL_0:2;
then
(k1 - j) + 1
<= len f
by A31, NAT_1:13;
then A33:
(k1 -' j) + 1
in dom f
by A31, A29, FINSEQ_3:25;
k1 - j >= 0 + 1
by A27, A28, A31, NAT_1:13;
then A34:
k1 -' j in dom f
by A31, A32, FINSEQ_3:25;
LSeg (
(mid (f,k1,k2)),
j)
= LSeg (
f,
(k1 -' j))
by A2, A3, A8, A24, A25, JORDAN4:20;
then
(k1 -' j) + 1
= len f
by A10, A34, A33, GOBOARD2:2;
then A35:
(k1 - j) + 1
= len f
by A30, XREAL_0:def 2;
k1 - j <= k1 - 1
by A8, XREAL_1:10;
then
len f <= (k1 - 1) + 1
by A35, XREAL_1:7;
hence
contradiction
by A2, A6, XXREAL_0:1;
verum end;