:: deftheorem Def6 defines |^ NAT_3:def 6 :
for X being set
for b being real-valued ManySortedSet of X
for n being non zero Nat
for b₄ being ManySortedSet of X holds
( b₄ = b |^ n iff ( support b₄ = support b & ( for i being object holds b₄ . i = (b . i) |^ n ) ) );