theorem Th3: :: DUALSP07:3

for X being RealNormSpace
for X0 being Subset of X
for vseq being sequence of (DualSp X) st ( for x being Point of X st x in X0 holds
vseq # x is convergent ) holds
for x being Point of X st x in Lin X0 holds
vseq # x is convergent