let X be RealBanachSpace; :: thesis: for M being Real
for X0 being non empty Subset of (DualSp X) st X is separable & 0 <= M & cl_Ball ((0. (DualSp X)),M) = X0 holds
X0 is weakly*-sequentially-compact
let M be Real; :: thesis: for X0 being non empty Subset of (DualSp X) st X is separable & 0 <= M & cl_Ball ((0. (DualSp X)),M) = X0 holds
X0 is weakly*-sequentially-compact
let X0 be non empty Subset of (DualSp X); :: thesis: ( X is separable & 0 <= M & cl_Ball ((0. (DualSp X)),M) = X0 implies X0 is weakly*-sequentially-compact )
assume that
A1: X is separable and
A2: ( 0 <= M & cl_Ball ((0. (DualSp X)),M) = X0 ) ; :: thesis: X0 is weakly*-sequentially-compact
for seq being sequence of X0 ex seq1 being sequence of (DualSp X) st
( seq1 is subsequence of seq & seq1 is weakly*-convergent & w*-lim seq1 in X0 )

proof

let seq be sequence of X0; :: thesis: ex seq1 being sequence of (DualSp X) st
( seq1 is subsequence of seq & seq1 is weakly*-convergent & w*-lim seq1 in X0 )
rng seq c= the carrier of (DualSp X) by XBOOLE_1:1;
then reconsider seq0 = seq as sequence of the carrier of (DualSp X) by FUNCT_2:6;
A3: for z being Point of (DualSp X) st z in X0 holds
||.z.|| <= M

proof

let z be Point of (DualSp X); :: thesis: ( z in X0 implies ||.z.|| <= M )
assume z in X0 ; :: thesis: ||.z.|| <= M
then z in { y where y is Point of (DualSp X) : ||.(y - (0. (DualSp X))).|| <= M } by NDIFF_8:18, A2;
then ex y being Point of (DualSp X) st
( z = y & ||.(y - (0. (DualSp X))).|| <= M ) ;
hence ||.z.|| <= M ; :: thesis: verum

end;

set f = ||.seq0.||;
for y being set st y in dom ||.seq0.|| holds
|.(||.seq0.|| . y).| < M + 1

proof

let y be set ; :: thesis: ( y in dom ||.seq0.|| implies |.(||.seq0.|| . y).| < M + 1 )
assume A4: y in dom ||.seq0.|| ; :: thesis: |.(||.seq0.|| . y).| < M + 1
then reconsider i = y as Nat ;
A5: ||.seq0.|| . y = ||.(seq0 . i).|| by NORMSP_0:def 4;
seq . i in rng seq by FUNCT_2:4, A4;
then A6: ||.(seq0 . i).|| <= M by A3;
M + 0 < M + 1 by XREAL_1:8;
hence |.(||.seq0.|| . y).| < M + 1 by A5, A6, XXREAL_0:2; :: thesis: verum

end;

then ||.seq0.|| is bounded by COMSEQ_2:def 3;
then consider f0 being sequence of (DualSp X) such that
A7: ( f0 is subsequence of seq0 & f0 is weakly*-convergent ) by A1, DUALSP03:26;
take f0 ; :: thesis: ( f0 is subsequence of seq & f0 is weakly*-convergent & w*-lim f0 in X0 )
thus f0 is subsequence of seq by A7; :: thesis: ( f0 is weakly*-convergent & w*-lim f0 in X0 )
thus f0 is weakly*-convergent by A7; :: thesis: w*-lim f0 in X0
A8: ( ||.f0.|| is bounded & ||.(w*-lim f0).|| <= lim_inf ||.f0.|| ) by DUALSP03:15, A7;
for s being Real st 0 < s holds
for n being Nat ex k being Nat st ||.f0.|| . (n + k) < M + s

proof

let s be Real; :: thesis: ( 0 < s implies for n being Nat ex k being Nat st ||.f0.|| . (n + k) < M + s )
assume A9: 0 < s ; :: thesis: for n being Nat ex k being Nat st ||.f0.|| . (n + k) < M + s
let n be Nat; :: thesis: ex k being Nat st ||.f0.|| . (n + k) < M + s
reconsider k = 0 as Nat ;
take k ; :: thesis: ||.f0.|| . (n + k) < M + s
A10: ||.f0.|| . (n + k) = ||.(f0 . (n + k)).|| by NORMSP_0:def 4;
consider N being increasing sequence of NAT such that
A11: f0 = seq0 * N by A7, VALUED_0:def 17;
A14: f0 . (n + k) = seq0 . (N . (n + k)) by FUNCT_2:15, ORDINAL1:def 12, A11;
seq . (N . (n + k)) in rng seq by FUNCT_2:4;
then A15: ||.(f0 . (n + k)).|| <= M by A14, A3;
0 + M < M + s by XREAL_1:8, A9;
hence ||.f0.|| . (n + k) < M + s by A15, A10, XXREAL_0:2; :: thesis: verum

end;

then lim_inf ||.f0.|| <= M by A8, RINFSUP1:81;
then ||.((w*-lim f0) - (0. (DualSp X))).|| <= M by A8, XXREAL_0:2;
then w*-lim f0 in { y where y is Point of (DualSp X) : ||.(y - (0. (DualSp X))).|| <= M } ;
hence w*-lim f0 in X0 by A2, NDIFF_8:18; :: thesis: verum

end;

hence X0 is weakly*-sequentially-compact ; :: thesis: verum