:: deftheorem defines ext-natural-valued COUNTERS:def 12 :
for f being Function holds
( f is ext-natural-valued iff for x being object st x in dom f holds
f . x is ext-natural );