for n being Nat
for r being Element of F_Real holds power (r,n) = r |^ n