theorem Th79: :: CLVECT_2:79

for X being ComplexUnitarySpace
for seq being sequence of X
for m being Nat ex M being Real st
( M > 0 & ( for n being Nat st n <= m holds
||.(seq . n).|| < M ) )