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