let seq be ExtREAL_sequence; :: thesis: for p being ExtReal st seq is convergent & ( for k being Nat holds p <= seq . k ) holds
p <= lim seq
let p be ExtReal; :: thesis: ( seq is convergent & ( for k being Nat holds p <= seq . k ) implies p <= lim seq )
assume that
A1: seq is convergent and
A2: for k being Nat holds p <= seq . k ; :: thesis: p <= lim seq
for y being ExtReal st y in rng seq holds
p <= y

proof

let y be ExtReal; :: thesis: ( y in rng seq implies p <= y )
assume y in rng seq ; :: thesis: p <= y
then consider x being object such that
A3: x in dom seq and
A4: y = seq . x by FUNCT_1:def 3;
reconsider x = x as Nat by A3;
seq . x >= p by A2;
hence p <= y by A4; :: thesis: verum

end;

then A5: p is LowerBound of rng seq by XXREAL_2:def 2;
reconsider INFSEQ = inferior_realsequence seq as sequence of ExtREAL ;
consider Y being non empty Subset of ExtREAL such that
A6: Y = { (seq . k) where k is Nat : 0 <= k } and
A7: INFSEQ . 0 = inf Y by RINFSUP2:def 6;

now :: thesis: for x being object st x in rng seq holds
x in Y

let x be object ; :: thesis: ( x in rng seq implies x in Y )
assume x in rng seq ; :: thesis: x in Y
then consider k being object such that
A8: k in dom seq and
A9: x = seq . k by FUNCT_1:def 3;
thus x in Y by A6, A8, A9; :: thesis: verum

end;

then A10: rng seq c= Y ;
for n being Element of NAT holds sup INFSEQ >= INFSEQ . n

proof

let n be Element of NAT ; :: thesis: sup INFSEQ >= INFSEQ . n
NAT = dom INFSEQ by FUNCT_2:def 1;
then INFSEQ . n in rng INFSEQ by FUNCT_1:def 3;
hence sup INFSEQ >= INFSEQ . n by XXREAL_2:4; :: thesis: verum

end;

then A11: sup INFSEQ >= INFSEQ . 0 ;

now :: thesis: for x being object st x in Y holds
x in rng seq

let x be object ; :: thesis: ( x in Y implies x in rng seq )
assume x in Y ; :: thesis: x in rng seq
then consider k being Nat such that
A12: ( x = seq . k & 0 <= k ) by A6;
A13: k in NAT by ORDINAL1:def 12;
dom seq = NAT by FUNCT_2:def 1;
hence x in rng seq by A12, FUNCT_1:3, A13; :: thesis: verum

end;

then Y c= rng seq ;
then Y = rng seq by A10, XBOOLE_0:def 10;
then (inferior_realsequence seq) . 0 >= p by A5, A7, XXREAL_2:def 4;
then lim_inf seq >= p by A11, XXREAL_0:2;
hence p <= lim seq by A1, RINFSUP2:41; :: thesis: verum