theorem Th35: :: TOPREAL8:35

for f, g being FinSequence of (TOP-REAL 2) st not f is empty & not g is trivial & f /. (len f) = g /. 1 holds
L~ (f ^' g) = (L~ f) \/ (L~ g)