:: Formalization of Separable Version of {B}anach {A}laoglu Theorem
:: by Hiroyuki Okazaki and Takehiko Mieno
::
:: Received December 21, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 4.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/4.0/.
environ
vocabularies DUALSP07, NUMBERS, SUBSET_1, XBOOLE_0, FUNCT_1, NAT_1, RELAT_1,
XXREAL_2, CARD_1, CARD_3, XXREAL_0, SEQ_4, REAL_1, ARYTM_3, ARYTM_1,
SEQ_2, ORDINAL2, HAHNBAN, COMPLEX1, STRUCT_0, PARTFUN1, TARSKI, DUALSP01,
PRE_TOPC, NORMSP_1, FCONT_1, RLVECT_1, LOPBAN_1, SUPINF_2, RLVECT_3,
RLVECT_2, VALUED_0, METRIC_1, MEMBERED, DUALSP03, PBOOLE, FUNCT_2,
TOPS_1, TOPGEN_1, FINSET_1;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, CARD_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1,
VALUED_0, MEMBERED, COMPLEX1, XXREAL_2, SEQ_2, SEQ_4, RINFSUP1, DOMAIN_1,
STRUCT_0, PRE_TOPC, RLVECT_1, RLVECT_2, RLVECT_3, NORMSP_0, NORMSP_1,
HAHNBAN, LOPBAN_1, DUALSP01, NORMSP_3, DUALSP03, NDIFF_8;
constructors REAL_1, SEQ_4, NAT_D, SEQ_2, RSSPACE, TOPMETR, COMSEQ_2,
RLVECT_2, RLVECT_3, NORMSP_3, RINFSUP1, DUALSP03, NDIFF_8;
registrations NUMBERS, XREAL_0, SEQ_2, FUNCT_2, NAT_1, CARD_1, MEMBERED,
ORDINAL1, VALUED_0, RELSET_1, STRUCT_0, ABSVALUE, NORMSP_1, DUALSP01,
XXREAL_2, XBOOLE_0, RLVECT_1, XCMPLX_0, XXREAL_0, NORMSP_3, RLVECT_2,
FINSET_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities STRUCT_0, DUALSP01, XCMPLX_0, RLVECT_2;
expansions TARSKI, DUALSP03;
theorems XXREAL_0, RELAT_1, XREAL_1, SEQ_4, SEQ_2, FUNCT_1, FUNCT_2, TARSKI,
COMPLEX1, HAHNBAN, VALUED_0, DUALSP01, NAT_1, RLVECT_1, XBOOLE_0,
XREAL_0, STRUCT_0, RLVECT_3, COMSEQ_2, XBOOLE_1, RLVECT_2, NORMSP_0,
NDIFF_8, SEQM_3, XXREAL_2, DUALSP03, CARD_2, ORDINAL1, XCMPLX_1,
RINFSUP1, NORMSP_4, ZFMISC_1;
schemes FUNCT_2, NAT_1;
begin :: Preliminaries.
:: Weak* Sequentially Compactness in Separable Dual Normed Spaces
theorem Th1:
for X being RealNormSpace,
vseq being sequence of (DualSp X),
x,y be Point of X
st vseq # x is convergent & vseq # y is convergent
holds vseq # (x+y) is convergent
& lim ( vseq # (x+y) ) = lim ( vseq # x) + lim ( vseq # y)
proof
let X be RealNormSpace,
vseq be sequence of (DualSp X),
x,y be Point of X;
assume that
A1: vseq # x is convergent and
A2: vseq # y is convergent;
A3:
now let p0 be Real;
set p = p0/2;
assume A4: 0 < p0; then
consider n1 being Nat such that
A6: for m being Nat st n1 <= m holds
|.(vseq # x).m - lim (vseq # x).| < p/2
by SEQ_2:def 7,A1;
consider n2 being Nat such that
A7: for m being Nat st n2 <= m holds
|.(vseq # y).m - lim (vseq # y).| < p/2
by SEQ_2:def 7,A2,A4;
reconsider n = max(n1,n2) as Nat
by XXREAL_0:def 10;
take n;
A8: n1 <= n & n2 <= n by XXREAL_0:25;
let m be Nat;
assume A9:n <= m; then
n1 <= m by XXREAL_0:2,A8; then
A10: |.(vseq # x).m - lim (vseq # x).| < p/2 by A6;
n2 <= m by A9,XXREAL_0:2,A8; then
A11: |.(vseq # y).m - lim (vseq # y).| < p/2 by A7;
reconsider vseqm = vseq.m
as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
(vseq # (x+y)).m = vseqm.(x+y) by DUALSP03:def 1
.=(vseq.m).x + (vseq.m).y by HAHNBAN:def 2
.=(vseq # x ).m + (vseq.m).y by DUALSP03:def 1
.=(vseq # x ).m + (vseq # y ).m by DUALSP03:def 1;
then
(vseq # (x+y)).m
- ( lim (vseq # x) + lim (vseq # y) )
= ( (vseq # x ).m - lim (vseq # x) )
+ ( (vseq # y ).m - lim (vseq # y) );
then
A12: |.(vseq # (x+y)).m
- ( lim (vseq # x) + lim (vseq # y) ) .|
<= |. (vseq # x ).m - lim (vseq # x) .|
+ |. (vseq # y ).m - lim (vseq # y) .|
by COMPLEX1:56;
|. (vseq # x ).m - lim (vseq # x) .|
+ |. (vseq # y ).m - lim (vseq # y) .|
<= p/2 + p/2 by A10,A11,XREAL_1:7; then
A13: |.(vseq # (x+y)).m
- ( lim (vseq # x) + lim (vseq # y) ) .|
<= p by A12,XXREAL_0:2;
p < p0 by XREAL_1:216,A4;
hence |.(vseq # (x+y)).m
- ( lim (vseq # x) + lim (vseq # y) ) .| < p0
by XXREAL_0:2,A13;
end;
hence
vseq # (x+y) is convergent by SEQ_2:def 6;
hence
lim ( vseq # (x+y) ) = lim ( vseq # x) + lim ( vseq # y)
by SEQ_2:def 7,A3;
end;
theorem Th2:
for X being RealNormSpace,
vseq being sequence of (DualSp X),
x be Point of X, a be Real
st vseq # x is convergent
holds vseq # (a*x) is convergent
& lim (vseq # (a*x)) = a * lim (vseq # x)
proof
let X be RealNormSpace,
vseq be sequence of (DualSp X),
x be Point of X, a be Real;
assume
A1: vseq # x is convergent;
per cases;
suppose A2: a = 0;
A3:
now let p be Real;
assume A4: 0 < p;
reconsider n = 0 as Nat;
take n;
let m be Nat;
assume n <= m;
reconsider vseqm = vseq.m
as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
(vseq # (a*x)).m
= (vseq.m).(a*x) by DUALSP03:def 1
.= a*vseqm.x by HAHNBAN:def 3
.= 0 by A2;
hence |.(vseq # (a*x)).m - a* lim ( vseq # x) .| < p
by A4,A2;
end;
hence vseq # (a*x) is convergent by SEQ_2:def 6;
hence
lim ( vseq # (a*x) ) = a*lim ( vseq # x)
by SEQ_2:def 7,A3;
end;
suppose a <> 0; then
A5: 0 < |.a.| by COMPLEX1:47;
A6:
now let p0 be Real;
assume A7: 0 < p0;
set p = p0/2;
consider n being Nat such that
A8: for m being Nat st n <= m holds
|.(vseq # x).m - lim (vseq # x).|
< p / |.a.| by SEQ_2:def 7,A1,A5,A7;
take n;
let m be Nat;
assume n <= m; then
A9: |.(vseq # x).m - lim (vseq # x).| < p / |.a.|
by A8;
reconsider vseqm = vseq.m
as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
(vseq # (a*x)).m
= (vseq.m).(a*x) by DUALSP03:def 1
.= a*vseqm.x by HAHNBAN:def 3
.= a* (vseq # x ).m by DUALSP03:def 1;
then
(vseq # (a*x)).m - a*lim (vseq # x)
= a* ( (vseq # x ).m - lim (vseq # x) );
then
A10: |.(vseq # (a*x)).m
- a*lim (vseq # x) .|
=|.a.|* |. (vseq # x ).m - lim (vseq # x) .|
by COMPLEX1:65;
|.a.|* |. (vseq # x ).m - lim (vseq # x) .|
<= |.a.|*(p / |.a.|) by A5,A9,XREAL_1:64;
then
A11: |.(vseq # (a*x)).m - a*lim (vseq # x) .|
<= p by A10,A5,XCMPLX_1:87;
p < p0 by XREAL_1:216,A7;
hence |.(vseq # (a*x)).m
- a*lim (vseq # x) .| < p0 by XXREAL_0:2,A11;
end;
hence vseq # (a*x) is convergent by SEQ_2:def 6;
hence lim ( vseq # (a*x) ) = a*lim ( vseq # x)
by SEQ_2:def 7,A6;
end;
end;
theorem Th3:
for X being RealNormSpace,
X0 being Subset of X,
vseq being sequence of (DualSp X)
st
for x being Point of X st x in X0 holds
vseq # x is convergent
holds
for x being Point of X st x in Lin X0 holds
vseq # x is convergent
proof
let X be RealNormSpace,
X0 be Subset of X,
vseq be sequence of DualSp X;
assume A1:
for x being Point of X st x in X0 holds
vseq # x is convergent;
defpred P[Nat] means
for x being Point of X,
X1 being Subset of X,
L being Linear_Combination of X1
st X1 c= X0
& card Carrier L <= $1
& x in Lin X1
& x = Sum L
holds vseq # x is convergent;
A2:P[0]
proof
let x be Point of X,
X1 be Subset of X,
L be Linear_Combination of X1;
assume
A3:X1 c= X0
& card Carrier L <= 0
& x in Lin X1
& x = Sum L;
Carrier L = {} by A3;
then
A4:x = 0.X by A3,RLVECT_2:34;
now let p be Real;
assume A5: 0 < p;
reconsider n = 0 as Nat;
take n;
let m be Nat;
assume n <= m;
reconsider vseqm = vseq.m
as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
(vseq # x).m
= vseqm.(0 * x) by A4,DUALSP03:def 1
.= 0*vseqm.x by HAHNBAN:def 3
.= 0;
hence
|.(vseq # x).m - 0 .| < p by A5;
end;
hence
vseq # x is convergent by SEQ_2:def 6;
end;
A6:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A7: P[k];
let x be Point of X,
X1 be Subset of X,
L be Linear_Combination of X1;
assume
A8: X1 c= X0
&
card Carrier L <= k+1
& x in Lin X1
& x = Sum L;
per cases;
suppose Carrier L = {}; then
A10:x = 0.X by A8,RLVECT_2:34;
now let p be Real;
assume A11: 0 < p;
reconsider n = 0 as Nat;
take n;
let m be Nat;
assume n <= m;
reconsider vseqm = vseq.m
as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
(vseq # x).m
= vseqm.(0 * x) by A10,DUALSP03:def 1
.= 0*vseqm.x by HAHNBAN:def 3
.= 0;
hence |.(vseq # x).m - 0 .| < p by A11;
end;
hence
vseq # x is convergent by SEQ_2:def 6;
end;
suppose Carrier L <> {}; then
consider v be object such that
A13: v in Carrier L by XBOOLE_0:def 1;
reconsider v as Point of X by A13;
A15P: Carrier L c= X1 by RLVECT_2:def 6;
reconsider X2 = X1\{v} as Subset of X;
reconsider X3 = {v} as Subset of X;
X2 c= X1 by XBOOLE_1:36;
then
A18:X2 c= X0 by A8;
X1 = X2 \/ X3 by XBOOLE_1:45,A15P,A13,ZFMISC_1:31;
then
consider L1 being Linear_Combination of X2,
L2 being Linear_Combination of X3 such that
A19: Carrier L
= (Carrier L1) \/ (Carrier L2)
& L = L1 + L2
& Carrier L1 = (Carrier L) \ X3
& Carrier L2 = (Carrier L) \ X2
by NORMSP_4:8,XBOOLE_1:79;
A20: Sum L = (Sum L1) + (Sum L2) by A19,RLVECT_3:1;
A21: Sum L2 = (L2.v) * v by RLVECT_2:32;
vseq # v is convergent by A1,A8,A13,A15P;
then
A22: vseq # (Sum L2) is convergent by A21,Th2;
not v in Carrier L1
proof
assume v in Carrier L1; then
v in Carrier L
& not v in {v} by A19,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end; then
A24: Carrier L1 c< Carrier L
by A19,XBOOLE_1:7,XBOOLE_0:def 8,A13;
A25P: card Carrier L1 < k+1
by A8,XXREAL_0:2,CARD_2:48,A24;
Sum L1 in Lin X2 by RLVECT_3:14;
then
vseq # (Sum L1)
is convergent by A7,A25P,A18,NAT_1:13;
hence
vseq # x is convergent by Th1,A8,A20,A22;
end;
end;
A27: for n be Nat holds P[n]
from NAT_1:sch 2(A2,A6);
let x be Point of X;
assume A28: x in Lin X0;
then
consider l being Linear_Combination of X0
such that
A29: x = Sum l by RLVECT_3:14;
card (Carrier l) + 0
<= card (Carrier l) + 1 by XREAL_1:7;
hence vseq # x is convergent by A28,A29,A27;
end;
theorem Th4:
for X being RealBanachSpace,
X0,X1 being Subset of X,
vseq being sequence of DualSp X
st
X1 = the carrier of Lin X0 & X1 is dense & ||.vseq.|| is bounded
&
for x being Point of X st x in X0 holds
vseq # x is convergent
holds
vseq is weakly*-convergent
proof
let X be RealBanachSpace,
X0,X1 be Subset of X,
vseq be sequence of DualSp X;
assume that
A1: X1= the carrier of Lin X0 and
A2: X1 is dense and
A3: ||.vseq.|| is bounded and
A4:
for x being Point of X st x in X0 holds
vseq # x is convergent;
for x being Point of X st x in X1
holds
vseq # x is convergent by STRUCT_0:def 5,Th3,A1,A4;
hence vseq is weakly*-convergent by A2,A3,DUALSP03:17;
end;
theorem Th5: :::
for V be RealLinearSpace, v be VECTOR of V, a be Real
st a <> 0
holds ex l being Linear_Combination of V
st l.v = a & Carrier l = {v}
proof
let V be RealLinearSpace, v be VECTOR of V, a be Real;
assume A1: a <> 0;
reconsider zz=0, a as Element of REAL by XREAL_0:def 1;
deffunc F(VECTOR of V)=zz;
consider f being Function of the carrier of V,REAL such that
A2: f.v = a and
A3: for u being VECTOR of V st u <> v holds f.u = F(u) from FUNCT_2:
sch 6;
reconsider f as Element of Funcs(the carrier of V,REAL) by FUNCT_2:8;
now
let u be VECTOR of V;
assume not u in {v};
then u <> v by TARSKI:def 1;
hence f.u = 0 by A3;
end;
then reconsider f as Linear_Combination of V by RLVECT_2:def 3;
A4:
{v} c= Carrier f
proof
let x be object;
assume x in {v};
then x=v by TARSKI:def 1;
hence thesis by A1,A2;
end;
A6: Carrier f c= {v}
proof
let x be object;
assume that
A7: x in Carrier f and
A8: not x in {v};
f.x <> 0 & x <> v by A7,A8,RLVECT_2:19,TARSKI:def 1;
hence thesis by A3,A7;
end;
take f;
thus thesis by A2,A4,A6,XBOOLE_0:def 10;
end;
theorem Th6:
for X be RealLinearSpace holds
[#] Lin ([#]X) = [#]X
proof
let X be RealLinearSpace;
for x be object holds
x in [#] Lin ([#]X)
iff
x in [#]X
proof
let x be object;
hereby assume x in [#] Lin ([#]X);
then
ex l being Linear_Combination of [#]X
st x = Sum l by RLVECT_3:14,STRUCT_0:def 5;
hence x in [#]X;
end;
assume x in [#]X;
then
reconsider v=x as Point of X;
consider l being Linear_Combination of X such that
A1: l.v = 1 & Carrier l = {v} by Th5;
A2: Sum l = (l . v) * v by A1,RLVECT_2:35
.= v by RLVECT_1:def 8,A1;
Carrier l c= [#]X;
then
reconsider l as Linear_Combination of [#]X
by RLVECT_2:def 6;
x = Sum l by A2;
hence x in [#] Lin ([#]X) by STRUCT_0:def 5,RLVECT_3:14;
end;
hence thesis by TARSKI:2;
end;
theorem
for X being RealBanachSpace,
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 ) ) ) )
proof
let X be RealBanachSpace;
let f be sequence of (DualSp X);
now
assume A1: f is weakly*-convergent;
hence ||.f.|| is bounded by DUALSP03:15;
set X0 = [#] X;
take X0,X0;
[#] Lin ([#]X) = [#]X by Th6;
hence X0 = the carrier of Lin X0;
thus X0 is dense;
thus for x being Point of X st x in X0 holds
f # x is convergent by A1;
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;
end;
::$INSERT Weak* Sequentially Compactness in Separable Dual Normed Spaces
definition
let X be RealNormSpace;
let X0 be non empty Subset of (DualSp X);
attr X0 is weakly*-sequentially-compact means
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);
end;
begin :: Banach Alaoglu theorem (case of separable)
::$MR Banach Alaoglu theorem (case of separable)
theorem
for X be RealBanachSpace,
M be Real,
X0 be 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
proof
let X be RealBanachSpace,
M be Real,
X0 be non empty Subset of DualSp X;
assume that
A1: X is separable and
A2:0<= M & cl_Ball(0.(DualSp X),M ) = X0;
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;
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 be Point of DualSp X
st z in X0 holds ||.z.|| <= M
proof
let z be Point of DualSp X;
assume z in X0; then
z in
{ y where y is Point of DualSp X : ||.(y - 0.(DualSp X)).|| <= M }
by NDIFF_8:18,A2;
then
ex y be Point of DualSp X st z=y & ||.(y - 0.(DualSp X)).|| <= M;
hence thesis;
end;
set f = ||.seq0.||;
for y being set st y in dom f holds
|.(f . y).| < M+1
proof
let y be set;
assume A4: y in dom f; then
reconsider i=y as Nat;
A5:
f.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
|.(f . y).| < M+1 by A5,A6,XXREAL_0:2;
end;
then
f 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;
thus f0 is subsequence of seq by A7;
thus f0 is weakly*-convergent by A7;
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;
assume A9: 0 < s;
let n be Nat;
reconsider k = 0 as Nat;
take k;
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;
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 thesis by A2,NDIFF_8:18;
end;
hence thesis;
end;
::$INSERT Weakly* sequentially continuous mappings on Normed Spaces
definition
let X be RealNormSpace;
let f be PartFunc of X,REAL;
let x0 be Point of X;
pred f is_weakly_continuous_in x0
means
x0 in dom f &
for e being Real st 0 < e holds
ex d being Real,
Y be Subset of DualSp X
st 0 < d & Y is finite & Y <> {}
&
for x being Point of X
st x in dom f
& for y be Point of (DualSp X)
st y in Y
holds |.y.(x-x0) .| < d
holds |.f.x-f.x0 .| < e;
end;
definition
let X be RealNormSpace;
let f be PartFunc of X,REAL;
let X0 be Subset of X;
pred f is_weakly_continuous_on X0
means
X0 c= dom f &
for x0 be Point of X
st x0 in X0
holds
for e being Real st 0 < e holds
ex d being Real,
Y be Subset of DualSp X
st 0 < d & Y is finite & Y <> {}
&
for x being Point of X
st x in X0
& for y be Point of DualSp X
st y in Y
holds |.y.(x-x0) .| < d
holds |.f.x-f.x0 .| < e;
end;
theorem
for X be RealNormSpace,
f be PartFunc of X,REAL,
X0 be Subset of X
holds
f is_weakly_continuous_on X0
iff
( X0 c= dom f
&
for x0 be Point of X
st x0 in X0
holds ( f|X0 ) is_weakly_continuous_in x0 )
proof
let X be RealNormSpace,
f be PartFunc of X,REAL,
X0 be Subset of X;
hereby assume A1: f is_weakly_continuous_on X0;
hence X0 c= dom f;
thus
for x0 be Point of X
st x0 in X0
holds ( f|X0 ) is_weakly_continuous_in x0
proof
let x0 be Point of X;
assume A4: x0 in X0;
hence
x0 in dom (f|X0) by RELAT_1:62,A1;
let e be Real;
assume 0 < e;
then
consider d being Real,
Y be Subset of DualSp X such that
A6: 0 < d & Y is finite & Y <> {}
&
for x being Point of X
st x in X0
& for y be Point of DualSp X
st y in Y
holds |.y.(x-x0) .| < d
holds |.f.x-f.x0 .| < e by A1,A4;
take d,Y;
thus
0 < d & Y is finite & Y <> {} by A6;
let x be Point of X;
assume x in dom (f|X0);
then
A7:x in X0 by RELAT_1:62,A1;
assume A8P:
for y be Point of (DualSp X)
st y in Y
holds |.y.(x-x0) .| < d;
(f|X0).x = f.x & (f|X0).x0 = f.x0 by A4,A7,FUNCT_1:49;
hence
|.(f|X0).x-(f|X0).x0 .| < e by A8P,A6,A7;
end;
end;
assume A9:
X0 c= dom f
&
for x0 be Point of X
st x0 in X0 holds (f|X0) is_weakly_continuous_in x0;
thus X0 c= dom f by A9;
A10: dom (f|X0) = X0 by RELAT_1:62,A9;
let x0 be Point of X;
assume A11: x0 in X0; then
A12: ( f|X0 ) is_weakly_continuous_in x0 by A9;
let e be Real;
assume 0 < e;
then consider d being Real,
Y be Subset of DualSp X
such that A13:
0 < d & Y is finite & Y <> {}
&
for x being Point of X
st x in dom (f|X0)
& for y be Point of DualSp X
st y in Y
holds |.y.(x-x0) .| < d
holds |.(f|X0).x-(f|X0).x0 .| < e
by A12;
take d,Y;
thus 0 < d & Y is finite & Y <> {} by A13;
let x be Point of X;
assume A14: x in X0
& for y be Point of DualSp X
st y in Y holds |.y.(x-x0) .| < d;
(f|X0).x = f.x & (f|X0).x0 = f.x0
by A11,A14,FUNCT_1:49;
hence |.f.x-f.x0 .| < e by A13,A14,A10;
end;
definition
let X be RealNormSpace;
let f be PartFunc of (DualSp X),REAL;
let x0 be Point of (DualSp X);
pred f is_weakly*_continuous_in x0
means
x0 in dom f &
for e being Real st 0 < e holds
ex d being Real,
Y be Subset of X
st 0 < d & Y is finite & Y <> {}
&
for x being Point of (DualSp X)
st x in dom f
& for y be Point of X
st y in Y
holds |.(x-x0).y .| < d
holds |.f.x-f.x0 .| < e;
end;
definition
let X be RealNormSpace;
let f be PartFunc of (DualSp X),REAL;
let X0 be Subset of DualSp X;
pred f is_weakly*_continuous_on X0
means
X0 c= dom f &
for x0 being Point of DualSp X
st x0 in X0 holds
for e being Real st 0 < e holds
ex d being Real,
Y be Subset of X
st 0 < d & Y is finite & Y <> {}
&
for x being Point of DualSp X
st x in X0
& for y be Point of X
st y in Y
holds |.(x-x0).y .| < d
holds |.f.x-f.x0 .| < e;
end;
theorem Th10:
for X be RealNormSpace,
f be PartFunc of (DualSp X),REAL,
X0 be Subset of DualSp X
holds
f is_weakly*_continuous_on X0
iff
( X0 c= dom f
&
for x0 be Point of DualSp X
st x0 in X0
holds ( f|X0 ) is_weakly*_continuous_in x0 )
proof
let X be RealNormSpace,
f be PartFunc of (DualSp X),REAL,
X0 be Subset of (DualSp X);
hereby assume A1:
f is_weakly*_continuous_on X0;
hence X0 c= dom f;
thus
for x0 be Point of DualSp X
st x0 in X0
holds ( f|X0 ) is_weakly*_continuous_in x0
proof
let x0 be Point of DualSp X;
assume A4: x0 in X0;
hence
x0 in dom (f|X0) by RELAT_1:62,A1;
let e be Real;
assume 0 < e;
then
consider d being Real,
Y be Subset of X such that
A6: 0 < d & Y is finite & Y <> {}
&
for x being Point of DualSp X
st x in X0
& for y be Point of X
st y in Y
holds |.(x-x0).y .| < d
holds |.f.x-f.x0 .| < e
by A1,A4;
take d,Y;
thus
0 < d & Y is finite & Y <> {} by A6;
let x be Point of DualSp X;
assume x in dom (f|X0);
then
A7:x in X0 by RELAT_1:62,A1;
assume A8P:
for y be Point of X
st y in Y
holds |.(x-x0).y .| < d;
(f|X0).x = f.x & (f|X0).x0 = f.x0
by A4,A7,FUNCT_1:49;
hence |.(f|X0).x-(f|X0).x0 .| < e by A8P,A6,A7;
end;
end;
assume A9:
X0 c= dom f
&
for x0 be Point of (DualSp X)
st x0 in X0
holds ( f|X0 )
is_weakly*_continuous_in x0;
thus X0 c= dom f by A9;
let x0 be Point of DualSp X;
assume A11: x0 in X0;
then
A12: ( f|X0 ) is_weakly*_continuous_in x0 by A9;
let e be Real;
assume 0 < e;
then consider d being Real,
Y be Subset of X
such that A13:
0 < d & Y is finite & Y <> {}
&
for x being Point of (DualSp X)
st x in dom (f|X0)
& for y be Point of X
st y in Y
holds |.(x-x0).y .| < d
holds |.(f|X0).x-(f|X0).x0 .| < e by A12;
take d,Y;
thus 0 < d & Y is finite & Y <> {} by A13;
let x be Point of DualSp X;
assume A14: x in X0
& for y be Point of X
st y in Y
holds |.(x-x0).y .| < d;
then
A15P: x in dom (f|X0) by A9,RELAT_1:62;
(f|X0).x = f.x & (f|X0).x0 = f.x0
by A11,A14,FUNCT_1:49;
hence |.f.x-f.x0 .| < e by A15P,A13,A14;
end;
theorem
for X be RealNormSpace,
f be PartFunc of X,REAL,
x0 be Point of X,
x be sequence of X
st f is_weakly_continuous_in x0
& rng x c= dom f
& x is weakly-convergent
& w-lim x = x0
holds f/*x is convergent & lim (f/*x) = f.x0
proof
let X be RealNormSpace,
f be PartFunc of X,REAL,
x0 be Point of X,
x be sequence of X;
assume that
A1: f is_weakly_continuous_in x0 and
A2: rng x c= dom f &
x is weakly-convergent and
A3: w-lim x = x0;
A6:
for e being Real st 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
|.(f/*x). m - f.x0.| < e
proof
let e be Real;
assume 0 < e; then
consider d being Real,
Y be Subset of DualSp X such that
A7: 0 < d & Y is finite & Y <> {}
&
for z being Point of X
st z in dom f
& for y be Point of DualSp X
st y in Y
holds |.y.(z-x0) .| < d
holds |.f.z-f.x0 .| < e by A1;
A8:
now let y be Point of DualSp X;
assume y in Y;
reconsider Ly = y as
Lipschitzian linear-Functional of X
by DUALSP01:def 10;
Ly * x is convergent & lim (Ly * x)
= Ly. x0 by DUALSP03:def 3,A2,A3; then
consider ny being Nat such that
A9: for m being Nat st ny <= m holds
|.(Ly * x). m - Ly.x0.| < d by A7,SEQ_2:def 7;
take ny;
let m be Nat;
assume A10P: ny <= m;
(Ly * x). m - Ly.x0
= Ly.(x.m) - Ly.x0 by FUNCT_2:15,ORDINAL1:def 12
.= Ly.(x.m-x0) by HAHNBAN:19;
hence |.y.((x. m) - x0) .| < d by A10P,A9;
end;
defpred P1[object,object] means
ex y be Point of (DualSp X),n be Nat
st $1 = y & $2 = n
& for m be Nat st n <= m holds
|.y.((x. m) - x0) .| < d;
A12: for z being object st z in Y holds
ex w being object st w in NAT & P1[z,w]
proof
let z be object;
assume A13:z in Y;
then
reconsider y=z as Point of DualSp X;
consider ny be Nat
such that
A14:for m being Nat st ny <= m
holds
|.y.((x. m) - x0) .| < d by A13,A8;
take ny;
thus ny in NAT by ORDINAL1:def 12;
thus thesis by A14;
end;
consider N being Function of Y,NAT such that
A15:for z being object st z in Y holds
P1[z,N . z] from FUNCT_2:sch 1(A12);
consider z be object such that
A16: z in Y by A7,XBOOLE_0:def 1;
reconsider M = rng N
as non empty finite Subset of NAT
by A7,A16,FUNCT_2:4;
set n0 = max M;
n0 in NAT by ORDINAL1:def 12; then
reconsider n0 as Nat;
A17: for m be Nat st n0 <= m
holds
for y be Point of DualSp X
st y in Y
holds
|.y.((x. m) - x0) .| < d
proof
let m be Nat;
assume A18: n0 <= m;
let y be Point of DualSp X;
assume A19: y in Y;
then
A20P: ex y0 be Point of (DualSp X),n be Nat
st y = y0 & N.y = n
& for m be Nat st n <= m
holds
|.y0.((x. m) - x0) .| < d by A15;
A21:n0 is UpperBound of M by XXREAL_2:def 3;
N.y <= n0 by A21,XXREAL_2:def 1,A19,FUNCT_2:4;
then
N.y <= m by A18,XXREAL_0:2;
hence |.y.((x. m) - x0) .| < d by A20P;
end;
take n0;
let m be Nat;
assume n0 <= m;
then
A22: for y be Point of DualSp X
st y in Y
holds
|.y.((x. m) - x0) .| < d by A17;
A23:m in NAT by ORDINAL1:def 12;
x.m in rng x by FUNCT_2:4,ORDINAL1:def 12;
then
|.f.(x.m)-f.x0 .| < e by A7,A22,A2;
hence
|.(f/*x).m-f.x0 .| < e
by A2,A23,FUNCT_2:108;
end;
hence f/*x is convergent by SEQ_2:def 6;
hence lim (f/*x) = f.x0 by A6,SEQ_2:def 7;
end;
theorem Th12:
for X be RealNormSpace,
f be PartFunc of (DualSp X),REAL,
x0 be Point of (DualSp X),
x be sequence of DualSp X
st f is_weakly*_continuous_in x0
& rng x c= dom f
& x is weakly*-convergent
& w*-lim x = x0
holds f/*x is convergent
& lim (f/*x) = f.x0
proof
let X be RealNormSpace,
f be PartFunc of (DualSp X),REAL,
x0 be Point of DualSp X,
x be sequence of DualSp X;
assume that
A1: f is_weakly*_continuous_in x0
and
A2: rng x c= dom f
&
x is weakly*-convergent
and
A3: w*-lim x = x0;
A6:
for e being Real st 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
|.(f/*x). m - f.x0.| < e
proof
let e be Real;
assume 0 < e; then
consider d being Real,
Y be Subset of X
such that
A7: 0 < d & Y is finite & Y <> {}
&
for z being Point of DualSp X
st z in dom f
& for y be Point of X
st y in Y
holds |.(z-x0).y .| < d
holds |.f.z-f.x0 .| < e by A1;
A8:
now let y be Point of X;
assume y in Y;
x#y is convergent & lim (x#y)
= x0.y by DUALSP03:def 5,A2,A3;
then
consider ny being Nat such that
A9: for m being Nat st ny <= m holds
|.(x#y). m - x0.y.| < d
by A7,SEQ_2:def 7;
take ny;
let m be Nat;
assume A10P: ny <= m;
(x#y). m - x0.y
= (x.m).y - x0.y by DUALSP03:def 1
.=(x.m-x0).y by DUALSP01:33;
hence |.((x. m) - x0).y .| < d
by A10P,A9;
end;
defpred P1[object,object]
means
ex y be Point of X,n be Nat
st $1=y & $2=n
& for m be Nat st n <= m
holds
|.((x. m) - x0).y .| < d;
A12: for z being object st z in Y holds
ex w being object st
( w in NAT & P1[z,w] )
proof
let z be object;
assume A13:z in Y;
then
reconsider y=z as Point of X;
consider ny be Nat such that
A14:for m being Nat
st ny <= m
holds
|.((x. m) - x0).y .| < d
by A13,A8;
take ny;
thus ny in NAT by ORDINAL1:def 12;
thus thesis by A14;
end;
consider N being Function of Y,NAT such that
A15:for z being object st z in Y holds
P1[z,N . z] from FUNCT_2:sch 1(A12);
consider z be object such that
A16: z in Y by A7,XBOOLE_0:def 1;
reconsider M = rng N
as non empty finite Subset of NAT
by A16,FUNCT_2:4,A7;
set n0 = max M;
n0 in NAT by ORDINAL1:def 12;
then
reconsider n0 as Nat;
A17: for m be Nat st n0 <= m
holds
for y be Point of X
st y in Y
holds
|.((x. m) - x0).y .| < d
proof
let m be Nat;
assume A18: n0 <= m;
let y be Point of X;
assume A19: y in Y; then
A20P: ex y0 be Point of X,n be Nat
st y = y0 & N.y = n
& for m be Nat st n <= m
holds
|.((x. m) - x0).y0 .| < d by A15;
n0 is UpperBound of M by XXREAL_2:def 3;
then
N.y <= n0 by XXREAL_2:def 1,A19,FUNCT_2:4;
then
N.y <= m by A18,XXREAL_0:2;
hence
|.((x. m) - x0).y .| < d by A20P;
end;
take n0;
let m be Nat;
assume n0 <= m;
then
A22: for y be Point of X st
y in Y
holds
|.((x. m) - x0).y .| < d by A17;
A23:m in NAT by ORDINAL1:def 12;
x.m in rng x by FUNCT_2:4,ORDINAL1:def 12;
then
|.f.(x.m)-f.x0 .| < e by A7,A22,A2;
hence
|.(f/*x).m-f.x0 .| < e by A2,A23,FUNCT_2:108;
end;
hence f/*x is convergent by SEQ_2:def 6;
hence lim (f/*x) = f.x0 by A6,SEQ_2:def 7;
end;
theorem
for X be RealNormSpace,
f be PartFunc of (DualSp X),REAL,
S be non empty Subset of (DualSp X)
st S is weakly*-sequentially-compact
& f is_weakly*_continuous_on S
holds
( ex r be Real
st for x be Point of DualSp X
st x in S holds |.f.x.| <= r )
&
( ex x0 be Point of DualSp X
st x0 in S
&
for x be Point of DualSp X
st x in S holds f.x <= f.x0 )
&
( ex v0 be Point of DualSp X
st v0 in S
&
for x be Point of DualSp X
st x in S holds f.v0 <= f.x )
proof
let X be RealNormSpace,
f be PartFunc of (DualSp X),REAL,
S be non empty Subset of DualSp X;
assume that
A1: S is weakly*-sequentially-compact
and
A2: f is_weakly*_continuous_on S;
A4: dom ( f|S ) = S by RELAT_1:62,A2;
thus
A5: ex r be Real
st for x be Point of DualSp X
st x in S holds |.f.x.| <= r
proof
assume
A6:not
( ex r be Real
st for x be Point of DualSp X
st x in S holds |.f.x.| <= r );
defpred P1[ Element of NAT,
Point of DualSp X] means
$2 in S & $1 < |.f.$2.|;
A7: for x being Element of NAT
ex y being Element of DualSp X
st P1[x,y] by A6;
consider seq being Function of NAT,(DualSp X)
such that
A9: for x being Element of NAT
holds P1[x,seq . x] from FUNCT_2:sch 3(A7);
A10: dom seq = NAT by FUNCT_2:def 1;
for x being object
st x in NAT holds seq.x in S by A9;
then
reconsider seq as sequence of S
by A10,FUNCT_2:3;
consider seq1 being sequence of DualSp X such that
A11: seq1 is subsequence of seq
& seq1 is weakly*-convergent & w*-lim seq1 in S by A1;
A12: ( f|S ) is_weakly*_continuous_in w*-lim seq1
by A11,A2,Th10;
A13: rng seq1 c= dom ( f|S )
by A4,A11,RELAT_1:def 19;
then
A14: ( f|S )/*seq1 is convergent
& lim (( f|S )/*seq1) = ( f|S ).(w*-lim seq1)
by Th12,A12,A11;
set r = ( f|S ).(w*-lim seq1);
set g = ( f|S )/*seq1;
consider r being Real such that
A15: 0 < r & for n being Nat holds |.g .n.| < r
by SEQ_2:3,A14;
consider N being increasing sequence of NAT
such that
A16: seq1 = seq*N by A11,VALUED_0:def 17;
consider n0 be Nat such that
A17: r < n0 by SEQ_4:3;
n0 <= N . n0 by SEQM_3:14;
then
A18: r < N.n0 by A17,XXREAL_0:2;
A19: n0 in NAT by ORDINAL1:def 12;
A20: seq1.n0 = seq.(N.n0) by ORDINAL1:def 12,FUNCT_2:15,A16;
A22: g.n0 = ( f|S ).(seq1.n0) by FUNCT_2:108,A19,A13
.= f.(seq.(N.n0)) by A20,FUNCT_1:49;
r < |. g.n0 .| by A18,XXREAL_0:2,A9,A22;
hence contradiction by A15;
end;
consider r be Real such that
A24: for x be Point of DualSp X
st x in S holds |.f.x.| <= r by A5;
dom (f|S) <> {} by A2,RELAT_1:62;
then reconsider
Y = rng (f|S) as non empty real-membered set by RELAT_1:42;
consider s be object such that
A25:s in S by XBOOLE_0:def 1;
reconsider s as Point of DualSp X by A25;
|.f.s.| <= r by A24,A25;
then
A27P: 0 <=r by COMPLEX1:46;
for z being Real st z in Y holds
|.z.| < r + 1
proof
let z be Real;
assume z in Y; then
consider t be object such that
A28: t in dom (f|S) & z=(f|S).t
by FUNCT_1:def 3;
A29: t in S by RELAT_1:62,A2,A28;
reconsider t as Point of DualSp X by A28;
(f|S).t = f.t by A29,FUNCT_1:49;
then
A30: |.(f|S).t.| <= r by A29,A24;
r + 0 < r + 1 by XREAL_1:8;
hence |.z.| < r + 1 by A30,A28,XXREAL_0:2;
end;
then
A31: Y is real-bounded by A27P,SEQ_4:4;
thus ex x0 be Point of DualSp X
st x0 in S
&
for x be Point of DualSp X
st x in S holds f.x <= f.x0
proof
set M = upper_bound Y;
defpred P2[Nat,Point of DualSp X]
means
$2 in S & |.(f|S).$2 - M .| < 1/($1+1);
A32: for x being Element of NAT
ex y being Element of DualSp X
st P2[x,y]
proof
let n be Element of NAT;
consider r be Real such that
A34: r in Y & M -1 /(n+1) < r by A31,SEQ_4:def 1;
r <= M by A34,SEQ_4:def 1,A31;
then
A35P:r + 0 < M + 1/(n+1) by XREAL_1:8;
consider t be object such that
A36: t in dom (f|S) & r=(f|S).t
by A34,FUNCT_1:def 3;
reconsider t as Point of DualSp X by A36;
take t;
thus t in S & |.(f|S).t - M .| < 1/(n+1)
by A35P,A34,RINFSUP1:1,RELAT_1:62,A2,A36;
end;
consider seq being Function of NAT,(DualSp X)
such that
A38: for n being Element of NAT
holds P2[n,seq . n]
from FUNCT_2:sch 3(A32);
A39: dom seq = NAT by FUNCT_2:def 1;
reconsider seq as sequence of DualSp X;
now let y be object;
assume y in rng seq;
then
consider x be object such that
A40: x in dom seq & y = seq.x
by FUNCT_1:def 3;
reconsider x as Element of NAT by A40;
thus y in S by A40,A38;
end; then
A42: rng seq c= dom (f|S) by A4;
A43:
now let p be Real;
assume A44:0 < p;
consider n be Nat such that
A45: n > (1/p)-1 by SEQ_4:3;
take n;
let m be Nat;
assume A46: n <= m;
(1/p)-1 < m by A45,A46,XXREAL_0:2;
then
(1/p)-1+1 < m+1 by XREAL_1:8;
then
p" " > (m+1)" by A44,XREAL_1:88;
then
A48: 1/(m+1) < p;
A49: m is Element of NAT
& m in NAT by ORDINAL1:def 12; then
|.(f|S).(seq.m) - M .| < p by A38,A48,XXREAL_0:2;
hence |.((f|S)/*seq).m - M .| < p
by A42,A49,FUNCT_2:108;
end; then
(f|S)/*seq is convergent by SEQ_2:def 6;
then
A51: lim ((f|S)/*seq) = M by A43,SEQ_2:def 7;
for x being object
st x in NAT holds seq.x in S by A38;
then
A52: seq is sequence of S by A39,FUNCT_2:3;
then
consider seq1 being sequence of DualSp X such that
A53: seq1 is subsequence of seq
& seq1 is weakly*-convergent & w*-lim seq1 in S by A1;
A54: ( f|S ) is_weakly*_continuous_in w*-lim seq1
by A53, A2,Th10;
A55: rng seq1 c= dom ( f|S )
by A52,A4,A53,RELAT_1:def 19; then
A56: ( f|S )/*seq1 is convergent
& lim (( f|S )/*seq1) = ( f|S ).(w*-lim seq1)
by Th12,A53,A54;
consider N being increasing sequence of NAT such that
A57: seq1 = seq * N by A53,VALUED_0:def 17;
( f|S )/*seq1
= ( f|S )*seq1 by A55,FUNCT_2:def 11
.= (( f|S )*seq)*N by RELAT_1:36,A57
.= (( f|S )/*seq)*N by A42,FUNCT_2:def 11;
then
A58: ( f|S ).(w*-lim seq1) = M by A43,SEQ_2:def 6,SEQ_4:17,A51,A56;
take
x0 = w*-lim seq1;
thus x0 in S by A53;
let x be Point of DualSp X;
assume A59: x in S; then
A60: f.x = (f|S).x by FUNCT_1:49;
A61: (f|S).x in Y by A59,A4,FUNCT_1:3;
( f|S ).(w*-lim seq1) = f.x0 by FUNCT_1:49,A53;
hence f.x <= f.x0 by A31,A60,A61,A58,SEQ_4:def 1;
end;
set N = lower_bound Y;
defpred P2[Nat,Point of DualSp X] means
$2 in S & |.(f|S).$2 - N .| < 1/($1+1);
A63: for x being Element of NAT
ex y being Element of DualSp X st P2[x,y]
proof
let n be Element of NAT;
consider r be Real such that
A65: r in Y & r < N + 1 /(n+1)
by A31,SEQ_4:def 2;
N <= r by A65,SEQ_4:def 2,A31; then
A66P:N - 1/(n+1) < r - 0 by XREAL_1:8;
consider t be object such that
A67: t in dom (f|S) & r = (f|S).t
by A65,FUNCT_1:def 3;
reconsider t as Point of DualSp X by A67;
take t;
thus t in S & |.(f|S).t - N .| < 1/(n+1)
by A66P,RELAT_1:62,A2,A67,A65,RINFSUP1:1;
end;
consider seq being Function of NAT,(DualSp X)
such that
A69: for n being Element of NAT
holds P2[n,seq . n]
from FUNCT_2:sch 3(A63);
A70: dom seq = NAT by FUNCT_2:def 1;
reconsider seq as sequence of DualSp X;
now let y be object;
assume y in rng seq; then
consider x be object such that
A71: x in dom seq & y = seq.x
by FUNCT_1:def 3;
reconsider x as Element of NAT by A71;
thus y in S by A71,A69;
end;
then
A73: rng seq c= dom (f|S) by A4;
A74:
now let p be Real;
assume A75:0 < p;
consider n be Nat such that
A76: n > (1/p)-1 by SEQ_4:3;
take n;
let m be Nat;
assume A77: n <= m;
(1/p)-1 < m by A76,A77,XXREAL_0:2;
then
(1/p)-1+1 < m+1 by XREAL_1:8;
then p" " > (m+1)" by A75,XREAL_1:88;
then
A79: 1/(m+1) < p;
A80: m is Element of NAT
& m in NAT by ORDINAL1:def 12;
then
|.(f|S).(seq.m) - N .| < p by A79,XXREAL_0:2,A69;
hence |.((f|S)/*seq).m - N .| < p
by A73,A80,FUNCT_2:108;
end; then
(f|S)/*seq is convergent by SEQ_2:def 6; then
A82: lim ((f|S)/*seq) = N by A74,SEQ_2:def 7;
for x being object st x in NAT
holds seq.x in S by A69; then
A83: seq is sequence of S by A70,FUNCT_2:3;
then
consider seq1 being sequence of DualSp X such that
A84: seq1 is subsequence of seq
& seq1 is weakly*-convergent & w*-lim seq1 in S
by A1;
A85: ( f|S ) is_weakly*_continuous_in w*-lim seq1
by A84,A2,Th10;
A86: rng seq1 c= dom ( f|S ) by A83,A4,A84,RELAT_1:def 19;
then
A87: ( f|S )/*seq1 is convergent
& lim (( f|S )/*seq1) = ( f|S ).(w*-lim seq1)
by Th12,A84,A85;
consider K being increasing sequence of NAT such that
A88: seq1 = seq * K by A84,VALUED_0:def 17;
( f|S )/*seq1
= ( f|S )*seq1 by A86,FUNCT_2:def 11
.= (( f|S )*seq)*K by RELAT_1:36,A88
.= (( f|S )/*seq)*K by A73,FUNCT_2:def 11;
then
A89: ( f|S ).(w*-lim seq1) = N by SEQ_2:def 6,A74,SEQ_4:17,A82,A87;
take v0 = w*-lim seq1;
thus v0 in S by A84;
let x be Point of DualSp X;
assume A90: x in S; then
A91: f.x = (f|S).x by FUNCT_1:49;
A92: (f|S).x in Y by A90,A4,FUNCT_1:3;
( f|S ).(w*-lim seq1) = f.v0 by FUNCT_1:49,A84;
hence f.v0 <= f.x by A31,A91,A92,A89,SEQ_4:def 2;
end;