let f be real-valued FinSequence; :: thesis: f is Element of REAL (len f)
rng f c= REAL ;
then f is FinSequence of REAL by FINSEQ_1:def 4;
then 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) ; :: thesis: verum