for X being ComplexUnitarySpace
for seq being sequence of X
for k being Nat st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by Th83, Th84;