theorem Th5: :: SPPOL_2:5

for f being FinSequence of (TOP-REAL 2)
for i, n being Nat st 1 <= i & i + 1 <= (len f) - n holds
LSeg ((f /^ n),i) = LSeg (f,(n + i))