<%i_FC%> is imaginary ;
hence ex b₁ being Polynomial of F_Complex st b₁ is imaginary ; :: thesis: verum