for n being Element of NAT
for z being Element of F_Complex st z is Real holds
ex x being Real st
( x = z & (power F_Complex) . (z,n) = x |^ n )