let i be Nat; :: according to BASEL_2:def 4 :: thesis: <%im1%> . i is imaginary
A1: i in NAT by ORDINAL1:def 12;
( i = 0 or i >= 1 ) by NAT_1:14;
then ( <%im1%> . i = im1 or <%im1%> . i = 0. F_Complex ) by POLYNOM5:32, A1;
hence <%im1%> . i is imaginary ; :: thesis: verum