for n being Nat
for f being FinSequence of REAL st len f = n holds
f in the carrier of (TOP-REAL n)