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;

( 0 < K & ( for n being Nat holds L . n <= K ) ) ) by A4; :: thesis: verum

( 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 ) ) )

( 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;( 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

now :: thesis: ( ex K being Real st

( 0 < K & ( for n being Nat holds L . n <= K ) ) implies sup (rng L) <> +infty )

hence
( sup (rng L) <> +infty iff 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

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;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

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

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

( 0 < K & ( for n being Nat holds L . n <= K ) ) ) by A4; :: thesis: verum