let L be ExtREAL_sequence; :: thesis: for K being R_eal st K <> +infty & ( for n being Nat holds L . n <= K ) holds

sup (rng L) < +infty

let K be R_eal; :: thesis: ( K <> +infty & ( for n being Nat holds L . n <= K ) implies sup (rng L) < +infty )

assume that

A1: K <> +infty and

A2: for n being Nat holds L . n <= K ; :: thesis: sup (rng L) < +infty

then sup (rng L) <= K by XXREAL_2:def 3;

hence sup (rng L) < +infty by A1, XXREAL_0:2, XXREAL_0:4; :: thesis: verum

sup (rng L) < +infty

let K be R_eal; :: thesis: ( K <> +infty & ( for n being Nat holds L . n <= K ) implies sup (rng L) < +infty )

assume that

A1: K <> +infty and

A2: for n being Nat holds L . n <= K ; :: thesis: sup (rng L) < +infty

now :: thesis: for x being ExtReal st x in rng L holds

x <= K

then
K is UpperBound of rng L
by XXREAL_2:def 1;x <= K

let x be ExtReal; :: thesis: ( x in rng L implies x <= K )

assume x in rng L ; :: thesis: x <= K

then ex z being object st

( z in dom L & x = L . z ) by FUNCT_1:def 3;

hence x <= K by A2; :: thesis: verum

end;assume x in rng L ; :: thesis: x <= K

then ex z being object st

( z in dom L & x = L . z ) by FUNCT_1:def 3;

hence x <= K by A2; :: thesis: verum

then sup (rng L) <= K by XXREAL_2:def 3;

hence sup (rng L) < +infty by A1, XXREAL_0:2, XXREAL_0:4; :: thesis: verum