theorem Th29: :: TOPREAL8:29

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