:: deftheorem Def5 defines Re COMSEQ_3:def 5 :
for c being Complex_Sequence
for b₂ being Real_Sequence holds
( b₂ = Re c iff for n being Nat holds b₂ . n = Re (c . n) );