let f be V26() standard special_circular_sequence; for i1, i2 being Nat st 1 <= i1 & i1 < i2 & i2 + 1 <= len f holds
mid (f,i1,i2) is being_S-Seq
let i1, i2 be Nat; ( 1 <= i1 & i1 < i2 & i2 + 1 <= len f implies mid (f,i1,i2) is being_S-Seq )
assume that
A1:
1 <= i1
and
A2:
i1 < i2
and
A3:
i2 + 1 <= len f
; mid (f,i1,i2) is being_S-Seq
A4:
mid (f,i1,i2) = (f /^ (i1 -' 1)) | ((i2 -' i1) + 1)
by A2, FINSEQ_6:def 3;
i1 < i1 + 1
by NAT_1:13;
then
i1 - 1 < (i1 + 1) - 1
by XREAL_1:9;
then
i1 - 1 < i2
by A2, XXREAL_0:2;
then A5:
i1 -' 1 < i2
by A1, XREAL_1:233;
(i2 -' i1) + 1 =
(i2 - i1) + 1
by A2, XREAL_1:233
.=
i2 - (i1 - 1)
.=
i2 - (i1 -' 1)
by A1, XREAL_1:233
.=
i2 -' (i1 -' 1)
by A5, XREAL_1:233
;
then A6:
mid (f,i1,i2) = (f | i2) /^ (i1 -' 1)
by A4, FINSEQ_5:80;
i2 < len f
by A3, NAT_1:13;
then
(i1 - 1) + 1 < len (f | i2)
by A2, FINSEQ_1:59;
then A7:
(i1 -' 1) + 1 < len (f | i2)
by A1, XREAL_1:233;
1 < i2
by A1, A2, XXREAL_0:2;
hence
mid (f,i1,i2) is being_S-Seq
by A3, A6, A7, Th7, Th37; verum