for G being RealNormSpace
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 )