let X be RealBanachSpace; :: thesis: for f being sequence of (DualSp X) holds
( f is weakly*-convergent iff ( ||.f.|| is bounded & ex X0 being Subset of X st
( X0 is dense & ( for x being Point of X st x in X0 holds
f # x is convergent ) ) ) )
let f be sequence of (DualSp X); :: thesis: ( f is weakly*-convergent iff ( ||.f.|| is bounded & ex X0 being Subset of X st
( X0 is dense & ( for x being Point of X st x in X0 holds
f # x is convergent ) ) ) )

now :: thesis: ( f is weakly*-convergent implies ( ||.f.|| is bounded & ex X0 being Element of K16( the carrier of X) st
( X0 is dense & ( for x being Point of X st x in X0 holds
f # x is convergent ) ) ) )

assume AS: f is weakly*-convergent ; :: thesis: ( ||.f.|| is bounded & ex X0 being Element of K16( the carrier of X) st
( X0 is dense & ( for x being Point of X st x in X0 holds
f # x is convergent ) ) )
hence ||.f.|| is bounded by Th711; :: thesis: ex X0 being Element of K16( the carrier of X) st
( X0 is dense & ( for x being Point of X st x in X0 holds
f # x is convergent ) )
set X0 = [#] X;
take X0 = [#] X; :: thesis: ( X0 is dense & ( for x being Point of X st x in X0 holds
f # x is convergent ) )
thus X0 is dense ; :: thesis: for x being Point of X st x in X0 holds
f # x is convergent
thus for x being Point of X st x in X0 holds
f # x is convergent by AS; :: thesis: verum

end;

hence ( f is weakly*-convergent iff ( ||.f.|| is bounded & ex X0 being Subset of X st
( X0 is dense & ( for x being Point of X st x in X0 holds
f # x is convergent ) ) ) ) by Th712A; :: thesis: verum