let f be constant Function; :: thesis: f = (dom f) --> (the_value_of f)

per cases ( f = {} or f <> {} ) ;

suppose f = {} ; :: thesis: f = (dom f) --> (the_value_of f)

then ( dom f = {} & dom ({} --> (the_value_of f)) = {} ) ;
hence f = (dom f) --> (the_value_of f) ; :: thesis: verum

end;

suppose A1: f <> {} ; :: thesis: f = (dom f) --> (the_value_of f)

A2: dom ((dom f) --> (the_value_of f)) = dom f by FUNCOP_1:19;

now

let x be set ; :: thesis: ( x in dom f implies f . x = ((dom f) --> (the_value_of f)) . x )
assume A3: x in dom f ; :: thesis: f . x = ((dom f) --> (the_value_of f)) . x
then ((dom f) --> (the_value_of f)) . x = the_value_of f by FUNCOP_1:13;
hence f . x = ((dom f) --> (the_value_of f)) . x by A1, A3, YELLOW_6:def 1; :: thesis: verum

end;

hence f = (dom f) --> (the_value_of f) by A2, FUNCT_1:9; :: thesis: verum

end;

end;