let f be constant non empty Function; :: thesis: ex y being set st
for x being set st x in dom f holds
f . x = y
consider y being set such that
A1: y in rng f by XBOOLE_0:def 1;
take y ; :: thesis: for x being set st x in dom f holds
f . x = y
ex x0 being set st
( x0 in dom f & f . x0 = y ) by A1, FUNCT_1:def 3;
hence for x being set st x in dom f holds
f . x = y by FUNCT_1:def 10; :: thesis: verum