theorem Th1: :: CSSPACE3:1

for c being Complex
for seq being Complex_Sequence
for rseq being Real_Sequence st seq is convergent & ( for i being Nat holds rseq . i = |.((seq . i) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| )