for X being RealNormSpace
for x being sequence of X st X is Reflexive holds
( x is weakly-convergent iff (BidualFunc X) * x is weakly*-convergent )