:: deftheorem defines weakly-convergent DUALSP03:def 2 :
for X being RealNormSpace
for x being sequence of X holds
( x is weakly-convergent iff ex x0 being Point of X st
for f being Lipschitzian linear-Functional of X holds
( f * x is convergent & lim (f * x) = f . x0 ) );