theorem Th26: :: JORDAN4:26

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