let f be constant non empty ext-natural-valued Function; :: thesis: ex N being ExtNat st
for x being object st x in dom f holds
f . x = N
consider R being ExtReal such that
A1: for x being object st x in dom f holds
f . x = R by VALUED_0:14;
set x = the Element of dom f;
( f . the Element of dom f = R & f . the Element of dom f is ext-natural ) by A1;
then reconsider N = R as ExtNat ;
take N ; :: thesis: for x being object st x in dom f holds
f . x = N
thus for x being object st x in dom f holds
f . x = N by A1; :: thesis: verum