let h, g be real-valued Function; :: thesis: ( dom h = dom f & ( for c being object st c in dom h holds
h . c = |.(f . c).| ) & dom g = dom f & ( for c being object st c in dom g holds
g . c = |.(f . c).| ) implies h = g )
assume that
A2: dom h = dom f and
A3: for c being object st c in dom h holds
h . c = H₁(c) and
A4: dom g = dom f and
A5: for c being object st c in dom g holds
g . c = H₁(c) ; :: thesis: h = g

now :: thesis: for x being object st x in dom h holds
h . x = g . x

let x be object ; :: thesis: ( x in dom h implies h . x = g . x )
assume A6: x in dom h ; :: thesis: h . x = g . x
hence h . x = H₁(x) by A3
.= g . x by A2, A4, A5, A6 ;
:: thesis: verum

end;

hence h = g by A2, A4; :: thesis: verum