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

now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (0. G)).|| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (0. G)).|| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (0. G)).|| < p
then consider n being Nat such that
A4: for m being Nat st n <= m holds
|.((s1 . m) - 0).| < p by A2, A3, SEQ_2:def 7;
reconsider n = n as Element of NAT by ORDINAL1:def 12;

now :: thesis: for m being Nat st n <= m holds
||.((seq . m) - (0. G)).|| < p

let m be Nat; :: thesis: ( n <= m implies ||.((seq . m) - (0. G)).|| < p )
A5: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: ||.((seq . m) - (0. G)).|| < p
then A6: |.((s1 . m) - 0).| < p by A4;
A7: ||.((seq . m) - (0. G)).|| = ||.(seq . m).|| by RLVECT_1:13;
A8: s1 . m <= |.(s1 . m).| by ABSVALUE:4;
||.(seq . m).|| <= s1 . m by A1, A5;
then ||.((seq . m) - (0. G)).|| <= |.(s1 . m).| by A7, A8, XXREAL_0:2;
hence ||.((seq . m) - (0. G)).|| < p by A6, XXREAL_0:2; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (0. G)).|| < p ; :: thesis: verum

end;

then A9: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (0. G)).|| < p ;
hence seq is convergent by NORMSP_1:def 6; :: thesis: lim seq = 0. G
hence lim seq = 0. G by A9, NORMSP_1:def 7; :: thesis: verum