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

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