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