let f be constant Function; :: thesis: f = (dom f) --> (the_value_of f)
thus dom ((dom f) --> (the_value_of f)) = dom f by Th19; :: according to FUNCT_1:def 11 :: thesis: for b₁ being set holds
( not b₁ in proj1 f or f . b₁ = ((dom f) --> (the_value_of f)) . b₁ )
let x be set ; :: 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 Th13;
hence f . x = ((dom f) --> (the_value_of f)) . x by A1, FUNCT_1:def 12; :: thesis: verum