theorem Th17: :: TOPREAL3:17

for f being FinSequence of (TOP-REAL 2)
for i, j being Nat st j in dom (f | i) & j + 1 in dom (f | i) holds
LSeg (f,j) = LSeg ((f | i),j)