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 ( the carrier of (TOP-REAL (len f)) = the carrier of (Euclid (len f)) & f in (len f) -tuples_on REAL ) by Th39;
hence ( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) ) ; :: thesis: verum