let seq be Real_Sequence; :: thesis:
assume A1: ( seq is divergent_to+infty or seq is divergent_to-infty ) ; :: thesis:

now :: thesis:

per cases by A1;

suppose seq is divergent_to+infty ; :: thesis:

then consider n being Nat such that
A2: for m being Nat st n <= m holds
0 < seq . m ;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume A3: n <= m ; :: thesis:

now :: thesis:

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

end;

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

end;

suppose seq is divergent_to-infty ; :: thesis:

then consider n being Nat such that
A4: for m being Nat st n <= m holds
seq . m < 0 ;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume A5: n <= m ; :: thesis:

now :: thesis:

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

end;

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

end;

end;

end;

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