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

.= 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

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

lim (seq_const r) =
(seq_const r) . 0
by SEQ_4:26
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;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

.= 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