theorem Th3: :: GOBOARD2:3

for f being FinSequence of (TOP-REAL 2)
for k being Nat st k <> 0 & len f = k + 1 holds
L~ f = (L~ (f | k)) \/ (LSeg (f,k))