deffunc H_{1}( 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_{1}(x) ) )
from FUNCT_1:sch 3();

hence ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = ].((f . x) - r),((f . x) + r).[ ) )
; :: thesis: verum

ex g being Function st

( dom g = dom f & ( for x being object st x in dom f holds

g . x = H

hence ex b

( dom b

b