let L be ExtREAL_sequence; :: thesis:
assume L is () ; :: thesis:
then A1: -infty < L . 1 ;
A2: dom L = NAT by FUNCT_2:def 1;
then A3: L . 1 <= sup (rng L) by FUNCT_1:3, XXREAL_2:4;

A4: now :: thesis:

assume sup (rng L) <> +infty ; :: thesis:
then not sup (rng L) in {-infty,+infty} by A1, A3, TARSKI:def 2;
then sup (rng L) in REAL by XBOOLE_0:def 3, XXREAL_0:def 4;
then reconsider S = sup (rng L) as Real ;
take K = max (S,1); :: thesis:
thus 0 < K by XXREAL_0:25; :: thesis:
let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
then A5: L . n <= sup (rng L) by A2, FUNCT_1:3, XXREAL_2:4;
S <= K by XXREAL_0:25;
hence L . n <= K by A5, XXREAL_0:2; :: thesis:

end;

given K being Real such that 0 < K and
A6: for n being Nat holds L . n <= K ; :: thesis:

let w be ExtReal; :: thesis:
assume w in rng L ; :: thesis:
then ex v being object st
( v in dom L & w = L . v ) by FUNCT_1:def 3;
hence w <= K by A6; :: thesis:

end;

then K is UpperBound of rng L by XXREAL_2:def 1;
then A7: sup (rng L) <= K by XXREAL_2:def 3;
K in REAL by XREAL_0:def 1;
hence sup (rng L) <> +infty by A7, XXREAL_0:9; :: thesis:

end;

hence ( sup (rng L) <> +infty iff ex K being Real st
( 0 < K & ( for n being Nat holds L . n <= K ) ) ) by A4; :: thesis: