theorem :: FUNCOP_1:80
for f being constant Function holds f = (dom f) --> (the_value_of f)