let X be RealBanachSpace; :: thesis: for f being sequence of (DualSp X) holds
( f is weakly*-convergent iff ( ||.f.|| is bounded & ex X0, X1 being Subset of X st
( X1 = the carrier of (Lin X0) & X1 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, X1 being Subset of X st
( X1 = the carrier of (Lin X0) & X1 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, X0 being Element of K16( the carrier of X) st
( X0 = the carrier of (Lin X0) & X0 is dense & ( for x being Point of X st x in X0 holds
f # x is convergent ) ) ) )

assume A1: f is weakly*-convergent ; :: thesis: ( ||.f.|| is bounded & ex X0, X0 being Element of K16( the carrier of X) st
( X0 = the carrier of (Lin X0) & X0 is dense & ( for x being Point of X st x in X0 holds
f # x is convergent ) ) )
hence ||.f.|| is bounded by DUALSP03:15; :: thesis: ex X0, X0 being Element of K16( the carrier of X) st
( X0 = the carrier of (Lin X0) & 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: ex X0 being Element of K16( the carrier of X) st
( X0 = the carrier of (Lin X0) & X0 is dense & ( for x being Point of X st x in X0 holds
f # x is convergent ) )
take X0 = X0; :: thesis: ( X0 = the carrier of (Lin X0) & X0 is dense & ( for x being Point of X st x in X0 holds
f # x is convergent ) )
[#] (Lin ([#] X)) = [#] X by Th6;
hence X0 = the carrier of (Lin X0) ; :: 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 A1; :: thesis: verum

end;

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