for x being Real st x > 0 holds
for n being Nat holds (power F_Complex) . ([**x,0**],n) = [**(x to_power n),0**]