let f be FinSequence of (TOP-REAL 2); :: thesis: for k1, k2 being Element of NAT st f is being_S-Seq & 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & k1 <> k2 holds
mid f,k1,k2 is being_S-Seq
let k1, k2 be Element of NAT ; :: thesis: ( f is being_S-Seq & 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & k1 <> k2 implies mid f,k1,k2 is being_S-Seq )
assume A1: ( f is being_S-Seq & 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & k1 <> k2 ) ; :: thesis: mid f,k1,k2 is being_S-Seq

per cases ( k1 <= k2 or k1 > k2 ) ;

suppose A2: k1 <= k2 ; :: thesis: mid f,k1,k2 is being_S-Seq

then A3: mid f,k1,k2 = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) by Def1;
k1 < k2 by A1, A2, XXREAL_0:1;
then A4: k1 + 1 <= k2 by NAT_1:13;
then A5: k1 + 1 <= len f by A1, XXREAL_0:2;
A6: (len f) -' (k1 -' 1) = (len f) - (k1 -' 1) by A1, NAT_D:50, XREAL_1:235
.= (len f) - (k1 - 1) by A1, XREAL_1:235
.= ((len f) - k1) + 1 ;
(k1 + 1) - k1 <= (len f) - k1 by A5, XREAL_1:11;
then 1 + 1 <= ((len f) - k1) + 1 by XREAL_1:8;
then A7: f /^ (k1 -' 1) is being_S-Seq by A1, A6, Th38, NAT_D:50;
(k1 + 1) - k1 <= k2 - k1 by A4, XREAL_1:11;
then 1 <= k2 -' k1 by NAT_D:39;
then 1 + 1 <= (k2 -' k1) + 1 by XREAL_1:8;
hence mid f,k1,k2 is being_S-Seq by A3, A7, Th37; :: thesis: verum

end;

suppose A8: k1 > k2 ; :: thesis: mid f,k1,k2 is being_S-Seq

then A9: mid f,k1,k2 = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) by Def1;
A10: k2 + 1 <= k1 by A8, NAT_1:13;
then A11: k2 + 1 <= len f by A1, XXREAL_0:2;
A12: (len f) -' (k2 -' 1) = (len f) - (k2 -' 1) by A1, NAT_D:50, XREAL_1:235
.= (len f) - (k2 - 1) by A1, XREAL_1:235
.= ((len f) - k2) + 1 ;
(k2 + 1) - k2 <= (len f) - k2 by A11, XREAL_1:11;
then 1 + 1 <= ((len f) - k2) + 1 by XREAL_1:8;
then A13: f /^ (k2 -' 1) is being_S-Seq by A1, A12, Th38, NAT_D:50;
(k2 + 1) - k2 <= k1 - k2 by A10, XREAL_1:11;
then 1 <= k1 -' k2 by NAT_D:39;
then 1 + 1 <= (k1 -' k2) + 1 by XREAL_1:8;
then (f /^ (k2 -' 1)) | ((k1 -' k2) + 1) is S-Sequence_in_R2 by A13, Th37;
hence mid f,k1,k2 is being_S-Seq by A9, SPPOL_2:47; :: thesis: verum

end;

end;