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