:: deftheorem defines real-valued VALUED_0:def 9 :
for f being Function holds
( f is real-valued iff for x being object st x in dom f holds
f . x is real );