let f be constant standard special_circular_sequence; :: thesis: for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 < len f holds
mid (f,i1,i2) is_a_part>_of f,i1,i2
let i1, i2 be Nat; :: thesis: ( 1 <= i1 & i1 <= i2 & i2 < len f implies mid (f,i1,i2) is_a_part>_of f,i1,i2 )
assume that
A1: 1 <= i1 and
A2: i1 <= i2 and
A3: i2 < len f ; :: thesis: mid (f,i1,i2) is_a_part>_of f,i1,i2
A4: 1 <= i2 by A1, A2, XXREAL_0:2;
A5: i1 < len f by A2, A3, XXREAL_0:2;
then A6: len (mid (f,i1,i2)) = (i2 -' i1) + 1 by A1, A2, A3, A4, FINSEQ_6:118;
then A7: 1 <= len (mid (f,i1,i2)) by NAT_1:11;
A8: i2 + 1 <= len f by A3, NAT_1:13;
A9: (i2 -' i1) + 1 = (i2 - i1) + 1 by A2, XREAL_1:233;
A10: for i being Nat st 1 <= i & i <= len (mid (f,i1,i2)) holds
(mid (f,i1,i2)) . i = f . (S_Drop (((i1 + i) -' 1),f))

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (mid (f,i1,i2)) implies (mid (f,i1,i2)) . i = f . (S_Drop (((i1 + i) -' 1),f)) )
assume that
A11: 1 <= i and
A12: i <= len (mid (f,i1,i2)) ; :: thesis: (mid (f,i1,i2)) . i = f . (S_Drop (((i1 + i) -' 1),f))
i + i1 <= ((i2 - i1) + 1) + i1 by A6, A9, A12, XREAL_1:6;
then i1 + i <= len f by A8, XXREAL_0:2;
then (i1 + i) - 1 <= (len f) - 1 by XREAL_1:9;
then (i1 + i) - 1 <= (len f) -' 1 by A3, A4, XREAL_1:233, XXREAL_0:2;
then A13: (i1 + i) -' 1 <= (len f) -' 1 by A1, NAT_D:37;
1 + 1 <= i1 + i by A1, A11, XREAL_1:7;
then (1 + 1) - 1 <= (i1 + i) - 1 by XREAL_1:9;
then 1 <= (i1 + i) -' 1 by A1, NAT_D:37;
then S_Drop (((i1 + i) -' 1),f) = (i1 + i) -' 1 by A13, Th22;
hence (mid (f,i1,i2)) . i = f . (S_Drop (((i1 + i) -' 1),f)) by A1, A2, A3, A4, A5, A11, A12, FINSEQ_6:118; :: thesis: verum

end;

A14: (mid (f,i1,i2)) . (len (mid (f,i1,i2))) = f . i2 by A1, A2, A3, FINSEQ_6:188;
A15: i1 + 1 <= len f by A5, NAT_1:13;
i2 + 1 < (i2 + 1) + i1 by A1, XREAL_1:29;
then (i2 + 1) - i1 < ((i2 + 1) + i1) - i1 by XREAL_1:9;
then len (mid (f,i1,i2)) < len f by A8, A6, A9, XXREAL_0:2;
hence mid (f,i1,i2) is_a_part>_of f,i1,i2 by A1, A4, A15, A8, A14, A7, A10; :: thesis: verum