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

now

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

end;

hence h = g by A3, A5, FUNCT_1:9; :: thesis: verum