theorem ThFunc1: :: COUNTERS:30

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