deffunc H₁( object ) -> object = r to_power (f . $1);
A1: for x being object st x in dom f holds
H₁(x) in REAL by XREAL_0:def 1;
consider g being Function of (dom f),REAL such that
A2: for x being object st x in dom f holds
g . x = H₁(x) from FUNCT_2:sch 2(A1);
take g ; :: thesis: ( dom g = dom f & ( for x being object st x in dom f holds
g . x = r to_power (f . x) ) )
thus ( dom g = dom f & ( for x being object st x in dom f holds
g . x = r to_power (f . x) ) ) by A2, FUNCT_2:def 1; :: thesis: verum