:: deftheorem Def4 defines to_power MESFUN6C:def 4 :
for k being Real
for X being non empty set
for f, b₄ being PartFunc of X,REAL holds
( b₄ = f to_power k iff ( dom b₄ = dom f & ( for x being Element of X st x in dom b₄ holds
b₄ . x = (f . x) to_power k ) ) );