set b = seq_const r;
let a be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not rng a c= right_closed_halfline r or not a is convergent or lim a in right_closed_halfline r )
assume that
A1: rng a c= right_closed_halfline r and
A2: a is convergent ; :: thesis: lim a in right_closed_halfline r
A3: now :: thesis: for n being Nat holds (seq_const r) . n <= a . n
let n be Nat; :: thesis: (seq_const r) . n <= a . n
a . n in rng a by VALUED_0:28;
then a . n in right_closed_halfline r by A1;
then a . n in { g1 where g1 is Real : r <= g1 } by XXREAL_1:232;
then ex r1 being Real st
( a . n = r1 & r <= r1 ) ;
hence (seq_const r) . n <= a . 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 r <= lim a by A2, A3, SEQ_2:18;
then lim a in { g1 where g1 is Real : r <= g1 } ;
hence lim a in right_closed_halfline r by XXREAL_1:232; :: thesis: verum