let f be Relation; :: thesis: ( f is real-valued implies f is REAL -valued )
assume f is real-valued ; :: thesis: f is REAL -valued
hence rng f c= REAL by VALUED_0:def 3; :: according to RELAT_1:def 19 :: thesis: verum