z in COMPLEX by XCMPLX_0:def 2;
then reconsider Z = z as Element of F_Complex by COMPLFLD:def 1;
( n in NAT & Re z = 0 ) by Def3, ORDINAL1:def 12;
then Im ((power F_Complex) . (Z,n)) = 0 by HURWITZ2:5;
hence (power F_Complex) . (z,n) is real ; :: thesis: verum