deffunc H_{1}( object ) -> object = sqrt (f . $1);

ex h being Function st

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

h . 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 b_{1} holds

b_{1} . x = sqrt (f . x) ) )
; :: thesis: verum

ex h being Function st

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

h . x = H

hence ex b

( dom b

b