theorem :: LIMFUNC1:6

for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds
ex n being Nat st
for m being Nat st n <= m holds
seq ^\ m is non-zero