for c being Complex
for seq being Complex_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| ) by Lm22;