theorem Th9: :: VALUED_0:9

for f being Function holds
( f is real-valued iff for x being object holds f . x is real )