consider F being Function such that

A1: dom F = dom f and

A2: for x being object st x in dom f holds

F . x = H_{1}(x)
from FUNCT_1:sch 3();

for x being object st x in dom F holds

F . x is complex

take F ; :: thesis: ( dom F = dom f & ( for c being set st c in dom F holds

F . c = (f . c) *' ) )

thus dom f = dom F by A1; :: thesis: for c being set st c in dom F holds

F . c = (f . c) *'

thus for c being set st c in dom F holds

F . c = (f . c) *' by A1, A2; :: thesis: verum

A1: dom F = dom f and

A2: for x being object st x in dom f holds

F . x = H

for x being object st x in dom F holds

F . x is complex

proof

then reconsider F = F as complex-valued Function by VALUED_0:def 7;
let x be object ; :: thesis: ( x in dom F implies F . x is complex )

assume x in dom F ; :: thesis: F . x is complex

then F . x = H_{1}(x)
by A1, A2;

hence F . x is complex ; :: thesis: verum

end;assume x in dom F ; :: thesis: F . x is complex

then F . x = H

hence F . x is complex ; :: thesis: verum

take F ; :: thesis: ( dom F = dom f & ( for c being set st c in dom F holds

F . c = (f . c) *' ) )

thus dom f = dom F by A1; :: thesis: for c being set st c in dom F holds

F . c = (f . c) *'

thus for c being set st c in dom F holds

F . c = (f . c) *' by A1, A2; :: thesis: verum