theorem :: TOPREAL3:38

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