let f be FinSequence of REAL ; :: thesis: ( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) )
f is Element of REAL * by FINSEQ_1:def 11;
then f in (len f) -tuples_on REAL ;
hence ( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) ) by EUCLID:25; :: thesis: verum