let a be real number ; :: thesis: for s1 being Real_Sequence st s1 is convergent & ( for n being Element of NAT holds s1 . n <= a ) holds
lim s1 <= a
let s1 be Real_Sequence; :: thesis: ( s1 is convergent & ( for n being Element of NAT holds s1 . n <= a ) implies lim s1 <= a )
assume that
A1: s1 is convergent and
A2: for n being Element of NAT holds s1 . n <= a ; :: thesis: lim s1 <= a
a in REAL by XREAL_0:def 1;
then reconsider s = NAT --> a as Real_Sequence by FUNCOP_1:57;

A3: now

let n be Element of NAT ; :: thesis: s1 . n <= s . n
s1 . n <= a by A2;
hence s1 . n <= s . n by FUNCOP_1:13; :: thesis: verum

end;

lim s = s . 0 by SEQ_4:41
.= a by FUNCOP_1:13 ;
hence lim s1 <= a by A1, A3, SEQ_2:32; :: thesis: verum