let L be ExtREAL_sequence; :: thesis: ( L is without-infty implies ( sup (rng L) <> +infty iff ex K being real number st
( 0 < K & ( for n being Nat holds L . n <= K ) ) ) )
assume A1: L is without-infty ; :: thesis: ( sup (rng L) <> +infty iff ex K being real number st
( 0 < K & ( for n being Nat holds L . n <= K ) ) )
A2: dom L = NAT by FUNCT_2:def 1;
then L . 1 in rng L by FUNCT_1:12;
then A3: ( -infty < L . 1 & L . 1 <= sup (rng L) ) by A1, Def5, XXREAL_2:4;

A4: now

assume sup (rng L) <> +infty ; :: thesis: ex K being set st
( 0 < K & ( for n being Nat holds L . n <= R_EAL K ) )
then not sup (rng L) in {-infty ,+infty } by 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 number ;
take K = max S,1; :: thesis: ( 0 < K & ( for n being Nat holds L . n <= R_EAL K ) )
A5: ( S <= K & 1 <= K ) by XXREAL_0:25;
thus 0 < K by XXREAL_0:25; :: thesis: for n being Nat holds L . n <= R_EAL K
let n be Nat; :: thesis: L . n <= R_EAL K
n in NAT by ORDINAL1:def 13;
then L . n <= sup (rng L) by A2, FUNCT_1:12, XXREAL_2:4;
hence L . n <= R_EAL K by A5, XXREAL_0:2; :: thesis: verum

end;

now

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

now

let w be ext-real number ; :: thesis: ( w in rng L implies w <= R_EAL K )
assume w in rng L ; :: thesis: w <= R_EAL K
then consider v being set such that
A7: v in dom L and
A8: w = L . v by FUNCT_1:def 5;
thus w <= R_EAL K by A6, A7, A8; :: thesis: verum

end;

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

end;

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