reconsider f = 1* n as FinSequence ;
len f = n by FINSEQ_1:def 18;
hence 1* n is Element of REAL n by FINSEQ_2:110; :: thesis: verum