let seq be Real_Sequence; :: thesis: ( ( seq is divergent_to+infty or seq is divergent_to-infty ) implies ex n being Nat st
for m being Nat st n <= m holds
seq ^\ m is non-zero )
assume A1: ( seq is divergent_to+infty or seq is divergent_to-infty ) ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
seq ^\ m is non-zero

now :: thesis: ex n being Nat st
for m being Nat st n <= m holds
seq ^\ m is non-zero

per cases ( seq is divergent_to+infty or seq is divergent_to-infty ) by A1;

suppose seq is divergent_to+infty ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
seq ^\ m is non-zero

then consider n being Nat such that
A2: for m being Nat st n <= m holds
0 < seq . m ;
take n = n; :: thesis: for m being Nat st n <= m holds
seq ^\ m is non-zero
let m be Nat; :: thesis: ( n <= m implies seq ^\ m is non-zero )
assume A3: n <= m ; :: thesis: seq ^\ m is non-zero

now :: thesis: for k being Nat holds 0 <> (seq ^\ m) . k

let k be Nat; :: thesis: 0 <> (seq ^\ m) . k
0 < seq . (k + m) by A2, A3, NAT_1:12;
hence 0 <> (seq ^\ m) . k by NAT_1:def 3; :: thesis: verum

end;

hence seq ^\ m is non-zero by SEQ_1:5; :: thesis: verum

end;

suppose seq is divergent_to-infty ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
seq ^\ m is non-zero

then consider n being Nat such that
A4: for m being Nat st n <= m holds
seq . m < 0 ;
take n = n; :: thesis: for m being Nat st n <= m holds
seq ^\ m is non-zero
let m be Nat; :: thesis: ( n <= m implies seq ^\ m is non-zero )
assume A5: n <= m ; :: thesis: seq ^\ m is non-zero

now :: thesis: for k being Nat holds (seq ^\ m) . k <> 0

let k be Nat; :: thesis: (seq ^\ m) . k <> 0
seq . (k + m) < 0 by A4, A5, NAT_1:12;
hence (seq ^\ m) . k <> 0 by NAT_1:def 3; :: thesis: verum

end;

hence seq ^\ m is non-zero by SEQ_1:5; :: thesis: verum

end;

end;

end;

hence ex n being Nat st
for m being Nat st n <= m holds
seq ^\ m is non-zero ; :: thesis: verum