for n being Nat
for r being Element of F_Real holds FPower (r,(n + 1)) = (FPower (r,n)) (#) (id REAL)