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

now :: thesis: for y being object st y in rng g holds
y in REAL

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

end;

then rng g c= REAL ;
then g in PFuncs (Z,REAL) by A1, 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 A1; :: 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 A3: x in dom g ; :: thesis: g /. x = |.(f /. x).|
then g . x = H₁(x) by A1;
hence g /. x = |.(f /. x).| by A3, PARTFUN1:def 6; :: thesis: verum