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
W1: y in rng f by XBOOLE_0:def 1;
consider x0 being set such that
W2: x0 in dom f and
W3: f . x0 = y by W1, FUNCT_1:def 5;
take y ; :: thesis: for x being set st x in dom f holds
f . x = y
let x be set ; :: thesis: ( x in dom f implies f . x = y )
assume x in dom f ; :: thesis: f . x = y
hence f . x = y by W2, W3, FUNCT_1:def 16; :: thesis: verum