theorem :: COUNTERS:31

for f being constant non empty ext-natural-valued Function ex N being ExtNat st
for x being object st x in dom f holds
f . x = N