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 /. (len f) in L~ (mid f,k1,k2) & not k1 = len f holds
k2 = len f
let k1, k2 be Element of 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 )
assume A6: ( k1 <> len f & k2 <> len f ) ; :: 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 /. (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 A10: k1 < k2 ; :: thesis: contradiction

then k2 - k1 > 0 by XREAL_1:52;
then A11: k2 -' k1 = k2 - k1 by XREAL_0:def 2;
A12: j + k1 >= 1 + 1 by A1, A7, XREAL_1:9;
then A13: (j + k1) - 1 >= (1 + 1) - 1 by XREAL_1:11;
then A14: (j + k1) -' 1 = (j + k1) - 1 by XREAL_0:def 2;
A15: len (mid f,k1,k2) = (k2 -' k1) + 1 by A1, A2, A3, A4, A10, JORDAN3:27;
then A16: j < (k2 -' k1) + 1 by A8, NAT_1:13;
then j - 1 < k2 - k1 by A11, XREAL_1:21;
then (j - 1) + k1 < k2 by XREAL_1:22;
then A17: (j + k1) - 1 < len f by A4, XXREAL_0:2;
then A18: (j + k1) -' 1 in dom f by A13, A14, FINSEQ_3:27;
A19: j + k1 >= 1 by A12, XXREAL_0:2;
((j + k1) - 1) + 1 <= len f by A14, A17, NAT_1:13;
then j + k1 in Seg (len f) by A19, FINSEQ_1:3;
then A20: ((j + k1) -' 1) + 1 in dom f by A14, FINSEQ_1:def 3;
LSeg (mid f,k1,k2),j = LSeg f,((j + k1) -' 1) by A1, A4, A7, A10, A16, JORDAN4:31;
then A21: ((j + k1) -' 1) + 1 = len f by A9, A18, A20, GOBOARD2:7;
A22: (j + k1) -' 1 = (j + k1) - 1 by A13, XREAL_0:def 2;
j < (k2 + 1) - k1 by A8, A11, A15, NAT_1:13;
then len f < k2 + 1 by A21, A22, XREAL_1:22;
then len f <= k2 by NAT_1:13;
hence contradiction by A4, A6, XXREAL_0:1; :: thesis: verum

end;

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

then len (mid f,k1,k2) = (k1 -' k2) + 1 by A1, A2, A3, A4, JORDAN3:27;
then A24: j < (k1 -' k2) + 1 by A8, NAT_1:13;
k1 - k2 > 0 by A23, XREAL_1:52;
then k1 -' k2 = k1 - k2 by XREAL_0:def 2;
then j - 1 < k1 - k2 by A24, XREAL_1:21;
then (j - 1) + k2 < k1 by XREAL_1:22;
then A25: j + (- (1 - k2)) < k1 ;
then A26: - (1 - k2) < k1 - j by XREAL_1:22;
A27: k2 - 1 < k1 - j by A25, XREAL_1:22;
A28: k2 - 1 >= 0 by A3, XREAL_1:50;
A29: k1 - j > 0 by A3, A27, XREAL_1:50;
then A30: k1 -' j = k1 - j by XREAL_0:def 2;
then A31: k1 - j >= 0 + 1 by A26, A28, NAT_1:13;
k1 - j <= k1 - 1 by A7, XREAL_1:12;
then (k1 - j) + 1 <= (k1 - 1) + 1 by XREAL_1:9;
then k1 - j < k1 by A30, NAT_1:13;
then A32: k1 - j < len f by A2, XXREAL_0:2;
then A33: k1 -' j in dom f by A30, A31, FINSEQ_3:27;
A34: (k1 - j) + 1 > 0 + 1 by A26, A28, XREAL_1:8;
(k1 - j) + 1 <= len f by A30, A32, NAT_1:13;
then A35: (k1 -' j) + 1 in dom f by A30, A34, FINSEQ_3:27;
LSeg (mid f,k1,k2),j = LSeg f,(k1 -' j) by A2, A3, A7, A23, A24, JORDAN4:32;
then (k1 -' j) + 1 = len f by A9, A33, A35, GOBOARD2:7;
then A36: (k1 - j) + 1 = len f by A29, XREAL_0:def 2;
k1 - j <= k1 - 1 by A7, XREAL_1:12;
then len f <= (k1 - 1) + 1 by A36, XREAL_1:9;
hence contradiction by A2, A6, XXREAL_0:1; :: thesis: verum

end;

suppose k1 = k2 ; :: thesis: contradiction

then mid f,k1,k2 = <*(f /. k1)*> by A1, A2, JORDAN4:27;
hence contradiction by A5, SPPOL_2:12; :: thesis: verum

end;

end;