theorem :: CFDIFF_1:1

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