:: deftheorem Def8 defines NPower NUMPOLY1:def 8 :
for n, k being Nat
for b₃ being FinSequence of REAL holds
( b₃ = NPower (n,k) iff ( dom b₃ = Seg k & ( for i being Nat st i in dom b₃ holds
b₃ . i = i |^ n ) ) );