deffunc H₁( object ) -> Element of f . $1 = the Element of f . $1;
consider g being Function such that
A1: dom g = dom f and
A2: for x being object st x in dom f holds
g . x = H₁(x) from FUNCT_1:sch 3();
take g ; :: thesis: ( dom g = dom f & ( for x being object st x in dom f holds
g . x = the Element of f . x ) )
thus dom g = dom f by A1; :: thesis: for x being object st x in dom f holds
g . x = the Element of f . x
let x be object ; :: thesis: ( x in dom f implies g . x = the Element of f . x )
assume A3: x in dom f ; :: thesis: g . x = the Element of f . x
reconsider x = x as set by TARSKI:1;
g . x = H₁(x) by A3, A2;
hence g . x = the Element of f . x ; :: thesis: verum