theorem Th12: :: VALUED_0:12

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