theorem :: CLVECT_2:97

for X being ComplexUnitarySpace
for seq being sequence of X st X is complete & seq is Cauchy holds
seq is bounded by Th80;