for n being Nat
for f being FinSequence of REAL st dom f = Seg n holds
f is Element of REAL n