for rs being Real_Sequence
for cs being Complex_Sequence st rs = cs & rs is convergent holds
cs is convergent ;