let f be constant Function; :: thesis: f = (dom f) --> (the_value_of f)
thus dom ((dom f) --> (the_value_of f)) = dom f ; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in proj1 f or f . b₁ = ((dom f) --> (the_value_of f)) . b₁ )
let x be object ; :: thesis: ( not x in proj1 f or f . x = ((dom f) --> (the_value_of f)) . x )
assume A1: x in dom f ; :: thesis: f . x = ((dom f) --> (the_value_of f)) . x
then ( f <> {} & ((dom f) --> (the_value_of f)) . x = the_value_of f ) by Th7;
hence f . x = ((dom f) --> (the_value_of f)) . x by A1, FUNCT_1:def 12; :: thesis: verum