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