theorem Th25: :: JORDAN4:25

for f being constant standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st g is_a_part>_of f,i1,i2 & i1 <= i2 holds
( len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) )