let i be Nat; :: according to BASEL_2:def 4 :: thesis: <%im1,im2%> . i is imaginary
( i = 0 or i = 1 or i >= 2 ) by NAT_1:23;
hence <%im1,im2%> . i is imaginary by POLYNOM5:38; :: thesis: verum