theorem Th8: :: VALUED_0:8

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