consider g being Function such that
P3: ( dom g = dom f & ( for x being set st x in dom f holds
g . x = H₁(x) ) ) from FUNCT_1:sch 3();

now

let y be set ; :: thesis: ( y in rng g implies y in REAL )
assume y in rng g ; :: thesis: y in REAL
then consider x being set such that
P41: ( x in dom g & y = g . x ) by FUNCT_1:def 3;
g . x = H₁(x) by P3, P41;
hence y in REAL by P41; :: thesis: verum

end;

then rng g c= REAL by TARSKI:def 3;
then g in PFuncs (Z,REAL) by P3, PARTFUN1:def 3;
then reconsider g = g as PartFunc of Z,REAL by PARTFUN1:46;
take g ; :: thesis: ( dom g = dom f & ( for x being set st x in dom g holds
g /. x = |.(f /. x).| ) )
thus dom g = dom f by P3; :: thesis: for x being set st x in dom g holds
g /. x = |.(f /. x).|
let x be set ; :: thesis: ( x in dom g implies g /. x = |.(f /. x).| )
assume P6: x in dom g ; :: thesis: g /. x = |.(f /. x).|
then g . x = H₁(x) by P3;
hence g /. x = |.(f /. x).| by P6, PARTFUN1:def 6; :: thesis: verum