:: deftheorem defines |^ BINOM:def 2 :
for R being non empty unital multMagma
for a being Element of R
for n being Nat holds a |^ n = (power R) . (a,n);