deffunc H₁( 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₁(x) ) ) from FUNCT_1:sch 3();
hence ex b₁ being Function st
( dom b₁ = dom f & ( for x being object st x in dom b₁ holds
b₁ . x = sqrt (f . x) ) ) ; :: thesis: verum