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

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 )
;

end;

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

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