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

proof

let x be object ; :: 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;
hence g . x is complex ; :: thesis: verum

end;

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