let seq be ExtREAL_sequence; :: thesis: for p being ext-real number st seq is convergent & ( for k being Nat holds seq . k <= p ) holds
lim seq <= p
let p be ext-real number ; :: 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 ext-real number st y in rng seq holds
y <= p

proof

let y be ext-real number ; :: thesis: ( y in rng seq implies y <= p )
assume y in rng seq ; :: thesis: y <= p
then consider x being set such that
A3: x in dom seq and
A4: y = seq . x by FUNCT_1:def 5;
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 Function of NAT ,ExtREAL ;
consider Y being non empty Subset of ExtREAL such that
A6: Y = { (seq . k) where k is Element of NAT : 0 <= k } and
A7: SUPSEQ . 0 = sup Y by RINFSUP2:def 7;

now

let x be set ; :: thesis: ( x in rng seq implies x in Y )
assume x in rng seq ; :: thesis: x in Y
then consider k being set such that
A8: k in dom seq and
A9: x = seq . k by FUNCT_1:def 5;
thus x in Y by A6, A8, A9; :: thesis: verum
reconsider k = k as Element of NAT by A8;

end;

then A10: rng seq c= Y by TARSKI:def 3;
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 5;
hence inf SUPSEQ <= SUPSEQ . n by XXREAL_2:3; :: thesis: verum

end;

then A11: inf SUPSEQ <= SUPSEQ . 0 ;

now

let x be set ; :: thesis: ( x in Y implies x in rng seq )
assume x in Y ; :: thesis: x in rng seq
then A12: ex k being Element of NAT st
( x = seq . k & 0 <= k ) by A6;
dom seq = NAT by FUNCT_2:def 1;
hence x in rng seq by A12, FUNCT_1:12; :: thesis: verum

end;

then Y c= rng seq by TARSKI:def 3;
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