let f be V26() standard special_circular_sequence; :: thesis: for i1, i2 being Nat st 1 < i1 & i1 < i2 & i2 <= len f holds
mid (f,i1,i2) is being_S-Seq
let i1, i2 be Nat; :: thesis: ( 1 < i1 & i1 < i2 & i2 <= len f implies mid (f,i1,i2) is being_S-Seq )
assume that
A1: 1 < i1 and
A2: i1 < i2 and
A3: i2 <= len f ; :: thesis: mid (f,i1,i2) is being_S-Seq
A4: i2 - (i1 -' 1) <= (len f) - (i1 -' 1) by A3, XREAL_1:9;
1 + 1 <= i1 by A1, NAT_1:13;
then (1 + 1) - 1 <= i1 - 1 by XREAL_1:9;
then A5: 1 <= i1 -' 1 by NAT_D:39;
A6: mid (f,i1,i2) = (f /^ (i1 -' 1)) | ((i2 -' i1) + 1) by A2, FINSEQ_6:def 3;
A7: i2 - i1 > 0 by A2, XREAL_1:50;
then A8: 1 <> (i2 -' i1) + 1 by XREAL_0:def 2;
i2 -' i1 > 0 by A7, XREAL_0:def 2;
then A9: i2 -' i1 >= 0 + 1 by NAT_1:13;
then A10: 1 <= (i2 -' i1) + 1 by NAT_1:13;
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 i1 -' 1 < i2 by A1, XREAL_1:233;
then A11: i1 -' 1 < len f by A3, XXREAL_0:2;
then len (f /^ (i1 -' 1)) = (len f) - (i1 -' 1) by RFINSEQ:def 1;
then i2 - (i1 - 1) <= len (f /^ (i1 -' 1)) by A1, A4, XREAL_1:233;
then (i2 - i1) + 1 <= len (f /^ (i1 -' 1)) ;
then A12: (i2 -' i1) + 1 <= len (f /^ (i1 -' 1)) by A9, NAT_D:39;
A13: i1 < len f by A2, A3, XXREAL_0:2;
then (i1 -' 1) + 1 < len f by A1, XREAL_1:235;
then ((i1 -' 1) + 1) - (i1 -' 1) < (len f) - (i1 -' 1) by XREAL_1:9;
then A14: 1 <= len (f /^ (i1 -' 1)) by A11, RFINSEQ:def 1;
(i1 -' 1) + 1 < len f by A1, A13, XREAL_1:235;
then mid ((f /^ (i1 -' 1)),1,((i2 -' i1) + 1)) is being_S-Seq by A5, A14, A10, A12, A8, Th38, JORDAN3:6;
hence mid (f,i1,i2) is being_S-Seq by A6, A10, FINSEQ_6:116; :: thesis: verum