rng (Replace (f,i,p)) c= (rng f) \/ {p} by FUNCT_7:100;
then rng (Replace (f,i,p)) c= REAL by XBOOLE_1:1;
hence Replace (f,i,p) is real-valued by VALUED_0:def 3; :: thesis: verum