for f being V26() standard special_circular_sequence
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