theorem :: EUCLID:76

for f being FinSequence of REAL holds
( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) )