consider g being Function such that
A1: ( dom g = dom f & ( for x being object st x in dom f holds
g . x = H1(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 b1 being complex-valued Function st
( dom b1 = dom f & ( for c being object st c in dom b1 holds
b1 . c = (f . c) " ) ) by A1; :: thesis: verum