let f be S-Sequence_in_R2; :: thesis: 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; :: 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 )

AA: k1 in dom f by FINSEQ_3:25, A1, A2;

assume that

A6: k1 <> 1 and

A7: k2 <> 1 ; :: thesis: 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;

k2 = 1

let k1, k2 be 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 )

AA: k1 in dom f by FINSEQ_3:25, A1, A2;

assume that

A6: k1 <> 1 and

A7: k2 <> 1 ; :: thesis: 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;

end;

suppose A12:
k1 < k2
; :: thesis: contradiction

then
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; :: thesis: verum

end;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; :: thesis: verum

suppose A14:
k1 > k2
; :: thesis: contradiction

then
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; :: thesis: verum

end;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; :: thesis: verum

suppose
k1 = k2
; :: thesis: contradiction

then mid (f,k1,k2) =
<*(f . k1)*>
by AA, JORDAN4:15

.= <*(f /. k1)*> by AA, PARTFUN1:def 6 ;

hence contradiction by A5, SPPOL_2:12; :: thesis: verum

end;.= <*(f /. k1)*> by AA, PARTFUN1:def 6 ;

hence contradiction by A5, SPPOL_2:12; :: thesis: verum