r + f is Function of X,REAL ;
hence r + f is Function of X,R^1 by TOPMETR:17; :: thesis: verum