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 that
A6: k1 <> len f and
A7: k2 <> len f ; :: thesis: contradiction
consider j being Element of 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;

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

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

end;

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

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