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 /. (len f) in L~ (mid (f,k1,k2)) & not k1 = len f holds

k2 = len f

let k1, k2 be Nat; :: thesis: ( 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)) ; :: thesis: ( 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 ; :: thesis: 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;

k2 = len f

let k1, k2 be Nat; :: thesis: ( 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)) ; :: thesis: ( 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 ; :: thesis: 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;

end;

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

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

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

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

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

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