let L be ExtREAL_sequence; :: thesis: ( L is () implies ( sup (rng L) <> +infty iff ex K being Real st
( 0 < K & ( for n being Nat holds L . n <= K ) ) ) )
assume L is () ; :: thesis: ( sup (rng L) <> +infty iff ex K being Real st
( 0 < K & ( for n being Nat holds L . n <= K ) ) )
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: ( sup (rng L) <> +infty implies ex K being object st
( 0 < K & ( for n being Nat holds L . n <= K ) ) )

assume sup (rng L) <> +infty ; :: thesis: ex K being object st
( 0 < K & ( for n being Nat holds L . n <= K ) )
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: ( 0 < K & ( for n being Nat holds L . n <= K ) )
thus 0 < K by XXREAL_0:25; :: thesis: for n being Nat holds L . n <= K
let n be Nat; :: thesis: L . n <= K
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: verum

end;

now :: thesis: ( ex K being Real st
( 0 < K & ( for n being Nat holds L . n <= K ) ) implies sup (rng L) <> +infty )

given K being Real such that 0 < K and
A6: for n being Nat holds L . n <= K ; :: thesis: sup (rng L) <> +infty

now :: thesis: for w being ExtReal st w in rng L holds
w <= K

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

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: verum

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: verum