let f be FinSequence of REAL ; :: thesis: ( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) )
U: the carrier of (TOP-REAL (len f)) = the carrier of (Euclid (len f)) by EUCLID:71;
V: for n being Element of NAT holds TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
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 U, V, EUCLID:25; :: thesis: verum