let f be FinSequence of (TOP-REAL 2); 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 ; ( 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
; mid (f,k1,k2) is being_S-Seq
per cases
( k1 <= k2 or k1 > k2 )
;
suppose A7:
k1 <= k2
;
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;
verum end; suppose A12:
k1 > k2
;
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;
verum end;