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