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