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₁(x) from FUNCT_1:sch 3();
for x being object st x in dom F holds
F . x is complex

proof

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₁(x) by A1, A2;
hence F . x is complex ; :: thesis: verum

end;

then reconsider F = F as complex-valued Function by VALUED_0:def 7;
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