for n being Nat
for r being Element of F_Real holds power (r,n) = (#Z n) . r