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_{1} being Complex st b_{1} = (power F_Complex) . (z,n) holds

b_{1} is imaginary
; :: thesis: verum

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

b