:: deftheorem defines power POLYNOM5:def 1 :
for R being non empty multMagma
for z being Element of R
for n being Nat holds power (z,n) = (power R) . (z,n);