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