theorem Th23: :: SPPOL_2:23

for f1, f2 being FinSequence of (TOP-REAL 2) st not f1 is empty & not f2 is empty holds
L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2)