f . k in REAL n ;
hence f . k is Element of REAL n ; :: thesis: verum