theorem Th29: :: BHSP_4:29

for r being Real
for X being RealUnitarySpace
for seq being sequence of X st r > 0 & ex m being Nat st
for n being Nat st n >= m holds
||.(seq . n).|| >= r & seq is convergent holds
lim seq <> 0. X