theorem Th42: :: DUALSP01:34

for X being RealNormSpace
for seq being sequence of (DualSp X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent