let f be non empty constant integer-valued Function; :: thesis: ex r being integer number st
for x being set st x in dom f holds
f . x = r
consider r being set such that
A1: for x being set st x in dom f holds
f . x = r by FUNCOP_1:93;
consider x being set such that
A2: x in dom f by XBOOLE_0:def 1;
r = f . x by A1, A2;
hence ex r being integer number st
for x being set st x in dom f holds
f . x = r by A1; :: thesis: verum