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 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 ) ) )
then A1: -infty < L . 1 by Def5;
A2: dom L = NAT by FUNCT_2:def 1;
then A3: L . 1 <= sup (rng L) by FUNCT_1:12, 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 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 number ;
take K = max S,1; :: thesis: ( 0 < K & ( for n being Nat holds L . n <= R_EAL K ) )
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 A5: L . n <= sup (rng L) by A2, FUNCT_1:12, XXREAL_2:4;
S <= K by XXREAL_0:25;
hence L . n <= R_EAL K by A5, XXREAL_0:2; :: thesis: verum

end;

now

given K being real number such that 0 < K and
A6: 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 ex v being set st
( v in dom L & w = L . v ) by FUNCT_1:def 5;
hence w <= R_EAL K by A6; :: thesis: verum

end;

then R_EAL K is UpperBound of rng L by XXREAL_2:def 1;
then A7: 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 A7, 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