let f be S-Sequence_in_R2; for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f /. 1 in L~ (mid (f,k1,k2)) & not k1 = 1 holds
k2 = 1
let k1, k2 be Nat; ( 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f /. 1 in L~ (mid (f,k1,k2)) & not k1 = 1 implies k2 = 1 )
assume that
A1:
1 <= k1
and
A2:
k1 <= len f
and
A3:
1 <= k2
and
A4:
k2 <= len f
and
A5:
f /. 1 in L~ (mid (f,k1,k2))
; ( k1 = 1 or k2 = 1 )
AA:
k1 in dom f
by FINSEQ_3:25, A1, A2;
assume that
A6:
k1 <> 1
and
A7:
k2 <> 1
; contradiction
A8:
len f >= 2
by TOPREAL1:def 8;
consider j being Nat such that
A9:
1 <= j
and
A10:
j + 1 <= len (mid (f,k1,k2))
and
A11:
f /. 1 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 A12:
k1 < k2
;
contradictionthen
len (mid (f,k1,k2)) = (k2 -' k1) + 1
by A1, A2, A3, A4, FINSEQ_6:118;
then
j < (k2 -' k1) + 1
by A10, NAT_1:13;
then
LSeg (
(mid (f,k1,k2)),
j)
= LSeg (
f,
((j + k1) -' 1))
by A1, A4, A9, A12, JORDAN4:19;
then A13:
(j + k1) -' 1
= 1
by A11, A8, JORDAN5B:30;
j + k1 >= 1
+ 1
by A1, A9, XREAL_1:7;
then
(j + k1) - 1
>= (1 + 1) - 1
by XREAL_1:9;
then
j + (k1 - 1) = 1
by A13, XREAL_0:def 2;
then
k1 - 1
= 1
- j
;
then
k1 - 1
<= 0
by A9, XREAL_1:47;
then
k1 - 1
= 0
by A1, XREAL_1:48;
hence
contradiction
by A6;
verum end; suppose A14:
k1 > k2
;
contradictionthen
len (mid (f,k1,k2)) = (k1 -' k2) + 1
by A1, A2, A3, A4, FINSEQ_6:118;
then A15:
j < (k1 -' k2) + 1
by A10, NAT_1:13;
k1 - k2 > 0
by A14, XREAL_1:50;
then
k1 -' k2 = k1 - k2
by XREAL_0:def 2;
then
j - 1
< k1 - k2
by A15, XREAL_1:19;
then
(j - 1) + k2 < k1
by XREAL_1:20;
then
j + (- (1 - k2)) < k1
;
then A16:
k2 - 1
< k1 - j
by XREAL_1:20;
LSeg (
(mid (f,k1,k2)),
j)
= LSeg (
f,
(k1 -' j))
by A2, A3, A9, A14, A15, JORDAN4:20;
then
k1 -' j = 1
by A11, A8, JORDAN5B:30;
then
k1 - j = 1
by XREAL_0:def 2;
then
k2 < 1
+ 1
by A16, XREAL_1:19;
then
k2 <= 1
by NAT_1:13;
hence
contradiction
by A3, A7, XXREAL_0:1;
verum end;