let a be Real; :: thesis: for s1 being Real_Sequence st s1 is convergent & ( for n being Nat holds s1 . n <= a ) holds
lim s1 <= a
let s1 be Real_Sequence; :: thesis: ( s1 is convergent & ( for n being Nat holds s1 . n <= a ) implies lim s1 <= a )
assume that
A1: s1 is convergent and
A2: for n being Nat holds s1 . n <= a ; :: thesis: lim s1 <= a
set s = seq_const a;

A3: now :: thesis: for n being Nat holds s1 . n <= (seq_const a) . n

let n be Nat; :: thesis: s1 . n <= (seq_const a) . n
s1 . n <= a by A2;
hence s1 . n <= (seq_const a) . n by SEQ_1:57; :: thesis: verum

end;

lim (seq_const a) = (seq_const a) . 0 by SEQ_4:26
.= a by SEQ_1:57 ;
hence lim s1 <= a by A1, A3, SEQ_2:18; :: thesis: verum