theorem Th3: :: SPPOL_2:3

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