theorem :: CLVECT_2:93
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Nat st seq is Cauchy holds
seq ^\ k is Cauchy by Th85;