:: deftheorem Def4 defines imaginary BASEL_2:def 4 :
for p being sequence of F_Complex holds
( p is imaginary iff for i being Nat holds p . i is imaginary );