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 that
A1: f is being_S-Seq and
A2: 1 <= k1 and
A3: k1 <= len f and
A4: 1 <= k2 and
A5: k2 <= len f and
A6: k1 <> k2 ; :: thesis: mid (f,k1,k2) is being_S-Seq

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

suppose A7: k1 <= k2 ; :: thesis: mid (f,k1,k2) is being_S-Seq

then k1 < k2 by A6, XXREAL_0:1;
then A8: k1 + 1 <= k2 by NAT_1:13;
then (k1 + 1) - k1 <= k2 - k1 by XREAL_1:9;
then 1 <= k2 -' k1 by NAT_D:39;
then A9: 1 + 1 <= (k2 -' k1) + 1 by XREAL_1:6;
k1 + 1 <= len f by A5, A8, XXREAL_0:2;
then (k1 + 1) - k1 <= (len f) - k1 by XREAL_1:9;
then A10: 1 + 1 <= ((len f) - k1) + 1 by XREAL_1:6;
(len f) -' (k1 -' 1) = (len f) - (k1 -' 1) by A3, NAT_D:50, XREAL_1:233
.= (len f) - (k1 - 1) by A2, XREAL_1:233
.= ((len f) - k1) + 1 ;
then A11: f /^ (k1 -' 1) is being_S-Seq by A1, A3, A10, Th5, NAT_D:50;
mid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) by A7, FINSEQ_6:def 3;
hence mid (f,k1,k2) is being_S-Seq by A11, A9, Th4; :: thesis: verum

end;

suppose A12: k1 > k2 ; :: thesis: mid (f,k1,k2) is being_S-Seq

then A13: k2 + 1 <= k1 by NAT_1:13;
then (k2 + 1) - k2 <= k1 - k2 by XREAL_1:9;
then 1 <= k1 -' k2 by NAT_D:39;
then A14: 1 + 1 <= (k1 -' k2) + 1 by XREAL_1:6;
k2 + 1 <= len f by A3, A13, XXREAL_0:2;
then (k2 + 1) - k2 <= (len f) - k2 by XREAL_1:9;
then A15: 1 + 1 <= ((len f) - k2) + 1 by XREAL_1:6;
(len f) -' (k2 -' 1) = (len f) - (k2 -' 1) by A5, NAT_D:50, XREAL_1:233
.= (len f) - (k2 - 1) by A4, XREAL_1:233
.= ((len f) - k2) + 1 ;
then f /^ (k2 -' 1) is being_S-Seq by A1, A5, A15, Th5, NAT_D:50;
then A16: (f /^ (k2 -' 1)) | ((k1 -' k2) + 1) is S-Sequence_in_R2 by A14, Th4;
mid (f,k1,k2) = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) by A12, FINSEQ_6:def 3;
hence mid (f,k1,k2) is being_S-Seq by A16; :: thesis: verum

end;

end;