let X be Banach_Algebra; :: thesis: for seq being sequence of X
for rseq being Real_Sequence st ( for n being Element of NAT holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds
( seq is convergent & lim seq = 0. X )
let seq be sequence of X; :: thesis: for rseq being Real_Sequence st ( for n being Element of NAT holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds
( seq is convergent & lim seq = 0. X )
let rseq be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds ||.(seq . n).|| <= rseq . n ) & rseq is convergent & lim rseq = 0 implies ( seq is convergent & lim seq = 0. X ) )
assume that
A1: for n being Element of NAT holds ||.(seq . n).|| <= rseq . n and
A2: rseq is convergent and
A3: lim rseq = 0 ; :: thesis: ( seq is convergent & lim seq = 0. X )

now

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (0. X)).|| < p )
assume A4: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (0. X)).|| < p
consider n being Element of NAT such that
A5: for m being Element of NAT st n <= m holds
abs ((rseq . m) - 0 ) < p by A2, A3, A4, SEQ_2:def 7;

now

let m be Element of NAT ; :: thesis: ( n <= m implies ||.((seq . m) - (0. X)).|| < p )
assume A6: n <= m ; :: thesis: ||.((seq . m) - (0. X)).|| < p
A7: abs ((rseq . m) - 0 ) < p by A5, A6;
A8: ||.((seq . m) - (0. X)).|| = ||.(seq . m).|| by RLVECT_1:26;
A9: ||.(seq . m).|| <= rseq . m by A1;
rseq . m <= abs (rseq . m) by ABSVALUE:11;
then ||.((seq . m) - (0. X)).|| <= abs (rseq . m) by A8, A9, XXREAL_0:2;
hence ||.((seq . m) - (0. X)).|| < p by A7, XXREAL_0:2; :: thesis: verum

end;

hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (0. X)).|| < p ; :: thesis: verum

end;

then A10: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (0. X)).|| < p ;
hence seq is convergent by NORMSP_1:def 9; :: thesis: lim seq = 0. X
hence lim seq = 0. X by A10, NORMSP_1:def 11; :: thesis: verum