theorem Th24: :: NDIFF_1:24

for S, T being RealNormSpace
for R being RestFunc of S,T
for s being 0. b₁ -convergent sequence of S st s is non-zero holds
( R /* s is convergent & lim (R /* s) = 0. T )