reconsider f = f as Functional of X by Def7;
f . v is Element of REAL ;
hence f . v is Element of REAL ; :: thesis: verum