consider g being Function such that

A1: ( dom g = dom f & ( for x being object st x in dom f holds

g . x = H_{1}(x) ) )
from FUNCT_1:sch 3();

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_{1}(x)
by A1;

hence g /. x = |.(f /. x).| by A3, PARTFUN1:def 6; :: thesis: verum

A1: ( dom g = dom f & ( for x being object st x in dom f holds

g . x = H

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

y in REAL

then
rng g c= REAL
;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_{1}(x)
by A1, A2;

hence y in REAL by A2, XREAL_0:def 1; :: thesis: verum

end;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

hence y in REAL by A2, XREAL_0:def 1; :: thesis: verum

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

hence g /. x = |.(f /. x).| by A3, PARTFUN1:def 6; :: thesis: verum