theorem Th2: :: DUALSP07:2

for X being RealNormSpace
for vseq being sequence of (DualSp X)
for x being Point of X
for a being Real st vseq # x is convergent holds
( vseq # (a * x) is convergent & lim (vseq # (a * x)) = a * (lim (vseq # x)) )