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