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

proof

let y be ExtReal; :: thesis: ( y in rng seq implies y <= p )
assume y in rng seq ; :: thesis: y <= p
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 y <= p by A4; :: thesis: verum

end;

then A5: p is UpperBound of rng seq by XXREAL_2:def 1;
reconsider SUPSEQ = superior_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: SUPSEQ . 0 = sup Y by RINFSUP2:def 7;

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 inf SUPSEQ <= SUPSEQ . n

proof

let n be Element of NAT ; :: thesis: inf SUPSEQ <= SUPSEQ . n
NAT = dom SUPSEQ by FUNCT_2:def 1;
then SUPSEQ . n in rng SUPSEQ by FUNCT_1:def 3;
hence inf SUPSEQ <= SUPSEQ . n by XXREAL_2:3; :: thesis: verum

end;

then A11: inf SUPSEQ <= SUPSEQ . 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 (superior_realsequence seq) . 0 <= p by A5, A7, XXREAL_2:def 3;
then lim_sup seq <= p by A11, XXREAL_0:2;
hence lim seq <= p by A1, RINFSUP2:41; :: thesis: verum