for rseq being Real_Sequence
for seq being Complex_Sequence st ( for n being Nat holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds
( seq is convergent & lim seq = 0c )