ex g being Function st
( dom g = dom f & ( for x being set st x in dom f holds
g . x = H₁(x) ) ) from FUNCT_1:sch 3();
hence ex b₁ being Function st
( dom b₁ = dom f & ( for c being set st c in dom b₁ holds
b₁ . c = r * (f . c) ) ) ; :: thesis: verum