theorem :: FUNCOP_1:80

for f being constant Function holds f = (dom f) --> (the_value_of f)