:: deftheorem Def6 defines Im COMSEQ_3:def 6 :
for c being Complex_Sequence
for b₂ being Real_Sequence holds
( b₂ = Im c iff for n being Nat holds b₂ . n = Im (c . n) );