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 V39() sequence of NAT such that
A3: seq1 = seq * Ns by A2, VALUED_0:def 17;
let r be Real; :: according to LIMFUNC1:def 4 :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < seq1 . m
consider n being Element of NAT such that
A4: for m being Element of NAT st n <= m holds
r < seq . m by A1, Def4;
take n ; :: thesis: for m being Element of NAT st n <= m holds
r < seq1 . m
let m be Element of NAT ; :: thesis: ( n <= m implies r < seq1 . m )
assume A5: n <= m ; :: thesis: r < seq1 . m
m <= Ns . m by SEQM_3:33;
then n <= Ns . m by A5, XXREAL_0:2;
then r < seq . (Ns . m) by A4;
hence r < seq1 . m by A3, FUNCT_2:21; :: thesis: verum