theorem :: TOPREAL3:18

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