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