let f be constant standard special_circular_sequence; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum