theorem Th7: :: SPPOL_2:7

for f, g being FinSequence of (TOP-REAL 2)
for i being Nat st 1 <= i holds
LSeg ((f ^ g),((len f) + i)) = LSeg (g,i)