let seq be Real_Sequence; :: thesis: ( ( seq is divergent_to+infty or seq is divergent_to-infty ) implies ex n being Element of NAT st
for m being Element of 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 Element of NAT st
for m being Element of NAT st n <= m holds
seq ^\ m is non-zero

now

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 Element of NAT st
for m being Element of NAT st n <= m holds
seq ^\ m is non-zero

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

now

let k be Element of 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 Element of NAT st
for m being Element of NAT st n <= m holds
seq ^\ m is non-zero

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

now

let k be Element of 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 Element of NAT st
for m being Element of NAT st n <= m holds
seq ^\ m is non-zero ; :: thesis: verum