:: deftheorem defines |^ RVSUM_4:def 3 :
for c being Complex
for n being non zero Nat holds c |^ n = (Partial_Product (seq_const c)) . (n - 1);