theorem Th7: :: JORDAN4:7

for g being FinSequence of (TOP-REAL 2)
for i being Nat st g is being_S-Seq & i + 1 < len g holds
g /^ i is being_S-Seq