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_{1}(c)
and

A5: dom g = dom f and

A6: for c being set st c in dom g holds

g . c = H_{1}(c)
; :: thesis: h = g

thus dom h = dom g by A3, A5; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom h or h . b_{1} = g . b_{1} )

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

.= g . x by A3, A5, A6, A7 ;

:: thesis: verum

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

A5: dom g = dom f and

A6: for c being set st c in dom g holds

g . c = H

thus dom h = dom g by A3, A5; :: according to FUNCT_1:def 11 :: thesis: for b

( not 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

.= g . x by A3, A5, A6, A7 ;

:: thesis: verum