let X be RealUnitarySpace; ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity implies for Y being Subset of X st Y is weakly_summable_set holds
ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) )
assume A1:
( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity )
; for Y being Subset of X st Y is weakly_summable_set holds
ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )
let Y be Subset of X; ( Y is weakly_summable_set implies ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) )
assume
Y is weakly_summable_set
; ex x being Point of X st
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )
then consider x being Point of X such that
A2:
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.(L . (x - (setsum Y1))).| < e ) )
;
take
x
; for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )
now for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )let L be
linear-Functional of
X;
( L is Lipschitzian implies for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) )assume A3:
L is
Lipschitzian
;
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )now for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )let e be
Real;
( e > 0 implies ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) )assume
e > 0
;
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )then consider Y0 being
finite Subset of
X such that A4:
not
Y0 is
empty
and A5:
Y0 c= Y
and A6:
for
Y1 being
finite Subset of
X st
Y0 c= Y1 &
Y1 c= Y holds
|.(L . (x - (setsum Y1))).| < e
by A2, A3;
take Y0 =
Y0;
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )now for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < eset x1 =
x;
let Y1 be
finite Subset of
X;
( Y0 c= Y1 & Y1 c= Y implies |.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e )assume that A7:
Y0 c= Y1
and A8:
Y1 c= Y
;
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < eset y1 =
setsum Y1;
set r =
L . (x - (setsum Y1));
Y1 <> {}
by A4, A7;
then
(
L . (x - (setsum Y1)) = (L . x) - (L . (setsum Y1)) &
L . (setsum Y1) = setopfunc (
Y1, the
carrier of
X,
REAL,
L,
addreal) )
by A1, Th5, HAHNBAN:19;
hence
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e
by A6, A7, A8;
verum end; hence
( not
Y0 is
empty &
Y0 c= Y & ( for
Y1 being
finite Subset of
X st
Y0 c= Y1 &
Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )
by A4, A5;
verum end; hence
for
e being
Real st
e > 0 holds
ex
Y0 being
finite Subset of
X st
( not
Y0 is
empty &
Y0 c= Y & ( for
Y1 being
finite Subset of
X st
Y0 c= Y1 &
Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )
;
verum end;
hence
for L being linear-Functional of X st L is Lipschitzian holds
for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) )
; verum