:: deftheorem defines weakly*-convergent DUALSP03:def 4 :
for X being RealNormSpace
for g being sequence of (DualSp X) holds
( g is weakly*-convergent iff ex g0 being Point of (DualSp X) st
for x being Point of X holds
( g # x is convergent & lim (g # x) = g0 . x ) );