let f be real-valued Function; :: thesis: f is Function of (dom f),REAL
rng f c= REAL ;
hence f is Function of (dom f),REAL by FUNCT_2:2; :: thesis: verum