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 Re ((power F_Complex) . (Z,n)) = 0 by HURWITZ2:6;
hence for b₁ being Complex st b₁ = (power F_Complex) . (z,n) holds
b₁ is imaginary ; :: thesis: verum