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

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

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

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

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