theorem Th28: :: JORDAN4:28

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 = ((len f) + i1) -' i2 & g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) )