let f be real-valued FinSequence; :: thesis: f is Element of REAL (len f)
f is FinSequence of REAL by Lm1;
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