let f be constant non empty natural-valued Function; :: thesis: ex r being natural number st
for x being set st x in dom f holds
f . x = r
consider r being set such that
W: for x being set st x in dom f holds
f . x = r by FUNCOP_1:93;
consider x being set such that
W1: x in dom f by XBOOLE_0:def 1;
r = f . x by W, W1;
then r in rng f by W1, FUNCT_1:12;
then r is natural ;
hence ex r being natural number st
for x being set st x in dom f holds
f . x = r by W; :: thesis: verum