:: deftheorem defines the_value_of FUNCT_1:def 12 :
for f being Function st not f is empty & f is constant holds
for b₂ being object holds
( b₂ = the_value_of f iff ex x being set st
( x in dom f & b₂ = f . x ) );