let seq, seq1 be Real_Sequence; :: thesis: ( seq is divergent_to-infty & ( for n being Element of NAT holds seq1 . n <= seq . n ) implies seq1 is divergent_to-infty )
assume that
A1: seq is divergent_to-infty and
A2: for n being Element of NAT holds seq1 . n <= seq . n ; :: thesis: seq1 is divergent_to-infty
let r be Real; :: according to LIMFUNC1:def 5 :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq1 . m < r
consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
seq . m < r by A1, Def5;
take n ; :: thesis: for m being Element of NAT st n <= m holds
seq1 . m < r
let m be Element of NAT ; :: thesis: ( n <= m implies seq1 . m < r )
assume n <= m ; :: thesis: seq1 . m < r
then A4: seq . m < r by A3;
seq1 . m <= seq . m by A2;
hence seq1 . m < r by A4, XXREAL_0:2; :: thesis: verum