for f, g being FinSequence of (TOP-REAL 2) st f,g are_in_general_position holds
for k being Nat holds (L~ f) /\ (LSeg (g,k)) is finite