theorem Th4: :: SPPOL_2:4

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