let X be RealUnitarySpace; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 ) )

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 ) ) ; :: thesis: verum

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 ) ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 :: thesis: 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 ) )

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 ) )

let L be linear-Functional of X; :: thesis: ( 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 ; :: thesis: 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 ) )

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 ) ) ; :: thesis: verum

end;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 ; :: thesis: 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 :: thesis: 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 ) )

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 ) )

let e be Real; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ) )

|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) by A4, A5; :: thesis: verum

end;( 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 ; :: thesis: 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; :: thesis: ( 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 :: thesis: 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

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

set x1 = x;

let Y1 be finite Subset of X; :: thesis: ( 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 ; :: thesis: |.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e

set 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; :: thesis: verum

end;let Y1 be finite Subset of X; :: thesis: ( 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 ; :: thesis: |.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e

set 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; :: thesis: verum

|.((L . x) - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) by A4, A5; :: thesis: verum

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 ) ) ; :: thesis: verum

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 ) ) ; :: thesis: verum