for f being FinSequence of REAL holds
( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) ) by EUCLID:76;