let seq, seq1 be Real_Sequence; :: thesis: ( seq is divergent_to-infty & seq1 is subsequence of seq implies seq1 is divergent_to-infty )
assume that
A1: seq is divergent_to-infty and
A2: seq1 is subsequence of seq ; :: thesis: seq1 is divergent_to-infty
consider Ns being increasing sequence of NAT such that
A3: seq1 = seq * Ns by A2, VALUED_0:def 17;
let r be Real; :: according to LIMFUNC1:def 5 :: thesis: ex n being Nat st
for m being Nat st n <= m holds
seq1 . m < r
consider n being Nat such that
A4: for m being Nat st n <= m holds
seq . m < r by A1;
take n ; :: thesis: for m being Nat st n <= m holds
seq1 . m < r
let m be Nat; :: thesis: ( n <= m implies seq1 . m < r )
assume A5: n <= m ; :: thesis: seq1 . m < r
A6: m in NAT by ORDINAL1:def 12;
m <= Ns . m by SEQM_3:14;
then n <= Ns . m by A5, XXREAL_0:2;
then seq . (Ns . m) < r by A4;
hence seq1 . m < r by A3, FUNCT_2:15, A6; :: thesis: verum