for k being Nat
for seq being Complex_Sequence st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by Th17, Th18;