let f be S-Sequence_in_R2; :: thesis: for k1, k2 being Element of 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 Element of NAT ; :: thesis: ( 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)
; :: thesis: ( k1 = 1 or k2 = 1 )
assume A6:
( k1 <> 1 & k2 <> 1 )
; :: thesis: contradiction
consider j being Element of NAT such that
A7:
1 <= j
and
A8:
j + 1 <= len (mid f,k1,k2)
and
A9:
f /. 1 in LSeg (mid f,k1,k2),j
by A5, SPPOL_2:13;
A10:
len f >= 2
by TOPREAL1:def 10;
per cases
( k1 < k2 or k1 > k2 or k1 = k2 )
by XXREAL_0:1;
suppose A11:
k1 < k2
;
:: thesis: contradictionthen
len (mid f,k1,k2) = (k2 -' k1) + 1
by A1, A2, A3, A4, JORDAN3:27;
then
j < (k2 -' k1) + 1
by A8, NAT_1:13;
then
LSeg (mid f,k1,k2),
j = LSeg f,
((j + k1) -' 1)
by A1, A4, A7, A11, JORDAN4:31;
then A12:
(j + k1) -' 1
= 1
by A9, A10, JORDAN5B:33;
j + k1 >= 1
+ 1
by A1, A7, XREAL_1:9;
then
(j + k1) - 1
>= (1 + 1) - 1
by XREAL_1:11;
then
j + (k1 - 1) = 1
by A12, XREAL_0:def 2;
then
k1 - 1
= 1
- j
;
then
k1 - 1
<= 0
by A7, XREAL_1:49;
then
k1 - 1
= 0
by A1, XREAL_1:50;
hence
contradiction
by A6;
:: thesis: verum end; suppose A13:
k1 > k2
;
:: thesis: contradictionthen
len (mid f,k1,k2) = (k1 -' k2) + 1
by A1, A2, A3, A4, JORDAN3:27;
then A14:
j < (k1 -' k2) + 1
by A8, NAT_1:13;
then
LSeg (mid f,k1,k2),
j = LSeg f,
(k1 -' j)
by A2, A3, A7, A13, JORDAN4:32;
then A15:
k1 -' j = 1
by A9, A10, JORDAN5B:33;
k1 - k2 > 0
by A13, XREAL_1:52;
then
k1 -' k2 = k1 - k2
by XREAL_0:def 2;
then
j - 1
< k1 - k2
by A14, XREAL_1:21;
then
(j - 1) + k2 < k1
by XREAL_1:22;
then
j + (- (1 - k2)) < k1
;
then A16:
k2 - 1
< k1 - j
by XREAL_1:22;
k1 - j = 1
by A15, XREAL_0:def 2;
then
k2 < 1
+ 1
by A16, XREAL_1:21;
then
k2 <= 1
by NAT_1:13;
hence
contradiction
by A3, A6, XXREAL_0:1;
:: thesis: verum end;