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
thus dom h = dom g by A3, A5; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom h or h . b₁ = g . b₁ )
let x be object ; :: thesis: ( not x in dom h or 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