theorem Th30: :: CLVECT_3:30

for X being ComplexUnitarySpace
for seq being sequence of X st ( for n being Nat holds seq . n <> 0. X ) & ex m being Nat st
for n being Nat st n >= m holds
||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 holds
not seq is summable