deffunc H₁( object ) -> Element of K19(REAL) = ].((f . $1) - r),((f . $1) + r).[;
ex g being Function st
( dom g = dom f & ( for x being object 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 x being object st x in dom f holds
b₁ . x = ].((f . x) - r),((f . x) + r).[ ) ) ; :: thesis: verum