:: deftheorem Def4 defines |^ FLEXARY1:def 4 :
for r being Real
for f, b₃ being real-valued Function holds
( b₃ = r |^ f iff ( dom b₃ = dom f & ( for x being object st x in dom f holds
b₃ . x = r to_power (f . x) ) ) );