theorem Th31: :: TOPREAL8:31

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