:: deftheorem Def6 defines to_power NUMBER15:def 6 :
for f, g being real-valued Function
for b₃ being Function holds
( b₃ = f to_power g iff ( dom b₃ = (dom f) /\ (dom g) & ( for x being object st x in dom b₃ holds
b₃ . x = (f . x) to_power (g . x) ) ) );