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_{1} being object holds

( not b_{1} in proj1 f or f . b_{1} = ((dom f) --> (the_value_of f)) . b_{1} )

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

thus dom ((dom f) --> (the_value_of f)) = dom f ; :: according to FUNCT_1:def 11 :: thesis: for b

( not 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