:: deftheorem defines |^ NEWTON:def 1 :
for x being Complex
for n being natural Number holds x |^ n = Product (n |-> x);