let seq be Real_Sequence; :: thesis: ( seq is non-decreasing & not seq is bounded_above implies seq is divergent_to+infty )
assume that
A1: seq is non-decreasing and
A2: not seq is bounded_above ; :: thesis: seq is divergent_to+infty
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 < seq . m
consider n being Element of NAT such that
A3: r + 1 <= seq . n by A2, SEQ_2:def 3;
take n ; :: thesis: for m being Element of NAT st n <= m holds
r < seq . m
let m be Element of NAT ; :: thesis: ( n <= m implies r < seq . m )
assume n <= m ; :: thesis: r < seq . m
then seq . n <= seq . m by A1, SEQM_3:12;
then r + 1 <= seq . m by A3, XXREAL_0:2;
hence r < seq . m by Lm1; :: thesis: verum