consider g being Function such that
A1: dom g = dom f and
A2: for x being set st x in dom f holds
g . x = H₁(x) from FUNCT_1:sch 3();
g is complex-valued

proof

let x be set ; :: according to VALUED_0:def 7 :: thesis: ( not x in dom g or g . x is complex )
assume x in dom g ; :: thesis: g . x is complex
then g . x = (f . x) " by A1, A2;
hence g . x is complex ; :: thesis: verum

end;

hence ex b₁ being complex-valued Function st
( dom b₁ = dom f & ( for c being set st c in dom b₁ holds
b₁ . c = (f . c) " ) ) by A1, A2; :: thesis: verum