theorem Th23: :: SEQ_4:23

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex k being Nat st seq ^\ k is non-zero