let L be ExtREAL_sequence; :: thesis: for K being R_eal st ( for n being Nat holds L . n <= K ) holds
sup (rng L) <= K
let K be R_eal; :: thesis: ( ( for n being Nat holds L . n <= K ) implies sup (rng L) <= K )
assume A1: for n being Nat holds L . n <= K ; :: thesis: sup (rng L) <= K

now

let x be ext-real number ; :: thesis: ( x in rng L implies x <= K )
assume x in rng L ; :: thesis: x <= K
then consider z being set such that
A2: z in dom L and
A3: x = L . z by FUNCT_1:def 5;
thus x <= K by A1, A2, A3; :: thesis: verum

end;

then K is UpperBound of rng L by XXREAL_2:def 1;
hence sup (rng L) <= K by XXREAL_2:def 3; :: thesis: verum