:: deftheorem Def4 defines |^ MESFUNC7:def 4 :
for k being Nat
for X being non empty set
for f, b₄ being PartFunc of X,ExtREAL holds
( b₄ = f |^ k iff ( dom b₄ = dom f & ( for x being Element of X st x in dom b₄ holds
b₄ . x = (f . x) |^ k ) ) );