f . n is Element of REAL * ;
hence f . n is FinSequence of REAL ; :: thesis: verum