let g1, g2 be PartFunc of Z,REAL; :: thesis: ( dom g1 = dom f & ( for x being set st x in dom g1 holds
g1 /. x = |.(f /. x).| ) & dom g2 = dom f & ( for x being set st x in dom g2 holds
g2 /. x = |.(f /. x).| ) implies g1 = g2 )
assume that
A4: ( dom g1 = dom f & ( for x being set st x in dom g1 holds
g1 /. x = H₁(x) ) ) and
A5: ( dom g2 = dom f & ( for x being set st x in dom g2 holds
g2 /. x = H₁(x) ) ) ; :: thesis: g1 = g2

now :: thesis: for x being Element of Z st x in dom g1 holds
g1 . x = g2 . x

let x be Element of Z; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume A6: x in dom g1 ; :: thesis: g1 . x = g2 . x
then A7: g1 /. x = |.(f /. x).| by A4;
g1 /. x = g2 /. x by A5, A7, A4, A6;
then g1 . x = g2 /. x by A6, PARTFUN1:def 6;
hence g1 . x = g2 . x by A4, A5, A6, PARTFUN1:def 6; :: thesis: verum

end;

hence g1 = g2 by A4, A5, PARTFUN1:5; :: thesis: verum