set b = seq_const r;
let a be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not rng a c= left_closed_halfline r or not a is convergent or lim a in left_closed_halfline r )
assume that
A4: rng a c= left_closed_halfline r and
A5: a is convergent ; :: thesis: lim a in left_closed_halfline r

A6: now :: thesis: for n being Nat holds a . n <= (seq_const r) . n

let n be Nat; :: thesis: a . n <= (seq_const r) . n
a . n in rng a by VALUED_0:28;
then a . n in left_closed_halfline r by A4;
then a . n in { g where g is Real : g <= r } by XXREAL_1:231;
then ex r1 being Real st
( a . n = r1 & r1 <= r ) ;
hence a . n <= (seq_const r) . n by SEQ_1:57; :: thesis: verum

end;

lim (seq_const r) = (seq_const r) . 0 by SEQ_4:26
.= r by SEQ_1:57 ;
then lim a <= r by A5, A6, SEQ_2:18;
then lim a in { g1 where g1 is Real : g1 <= r } ;
hence lim a in left_closed_halfline r by XXREAL_1:231; :: thesis: verum