theorem Th80: :: CLVECT_2:80

for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
seq is bounded