theorem Th30: :: TOPREAL8:30

for f being non empty FinSequence of (TOP-REAL 2)
for g being non trivial FinSequence of (TOP-REAL 2) st f /. (len f) = g /. 1 holds
LSeg ((f ^' g),(len f)) = LSeg (g,1)