theorem Th1: :: GOBOARD1:1

for f being FinSequence of (TOP-REAL 2)
for i being Nat st i in dom f & 2 <= len f holds
f /. i in L~ f