let X be RealUnitarySpace; :: thesis: for Y being Subset of X st Y is summable_set holds

Y is weakly_summable_set

let Y be Subset of X; :: thesis: ( Y is summable_set implies Y is weakly_summable_set )

assume Y is summable_set ; :: thesis: Y is weakly_summable_set

then consider x being Point of X such that

A1: for e being Real st 0 < e 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

||.(x - (setsum Y1)).|| < e ) ) ;

Y is weakly_summable_set

let Y be Subset of X; :: thesis: ( Y is summable_set implies Y is weakly_summable_set )

assume Y is summable_set ; :: thesis: Y is weakly_summable_set

then consider x being Point of X such that

A1: for e being Real st 0 < e 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

||.(x - (setsum Y1)).|| < e ) ) ;

now :: thesis: for L being linear-Functional of X st L is Lipschitzian holds

for e1 being Real st 0 < e1 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))).| < e1 ) )

hence
Y is weakly_summable_set
; :: thesis: verumfor e1 being Real st 0 < e1 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))).| < e1 ) )

let L be linear-Functional of X; :: thesis: ( L is Lipschitzian implies for e1 being Real st 0 < e1 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))).| < e1 ) ) )

assume L is Lipschitzian ; :: thesis: for e1 being Real st 0 < e1 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))).| < e1 ) )

then consider K being Real such that

A2: 0 < K and

A3: for x being Point of X holds |.(L . x).| <= K * ||.x.|| ;

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))).| < e1 ) ) ; :: 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 - (setsum Y1))).| < e1 ) ) )

assume L is Lipschitzian ; :: thesis: for e1 being Real st 0 < e1 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))).| < e1 ) )

then consider K being Real such that

A2: 0 < K and

A3: for x being Point of X holds |.(L . x).| <= K * ||.x.|| ;

now :: thesis: for e1 being Real st 0 < e1 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))).| < e1 ) )

hence
for e1 being Real st 0 < e1 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))).| < e1 ) )

let e1 be Real; :: thesis: ( 0 < e1 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 - (setsum Y1))).| < e1 ) ) )

assume A4: 0 < e1 ; :: 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 - (setsum Y1))).| < e1 ) )

set e = e1 / K;

consider Y0 being finite Subset of X such that

A5: ( not Y0 is empty & Y0 c= Y ) and

A6: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

||.(x - (setsum Y1)).|| < e1 / K by A1, A2, A4, XREAL_1:139;

A7: (e1 / K) * K = e1 by A2, XCMPLX_1:87;

( 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))).| < e1 ) ) by 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 - (setsum Y1))).| < e1 ) ) )

assume A4: 0 < e1 ; :: 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 - (setsum Y1))).| < e1 ) )

set e = e1 / K;

consider Y0 being finite Subset of X such that

A5: ( not Y0 is empty & Y0 c= Y ) and

A6: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

||.(x - (setsum Y1)).|| < e1 / K by A1, A2, A4, XREAL_1:139;

A7: (e1 / K) * K = e1 by A2, XCMPLX_1:87;

now :: thesis: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

|.(L . (x - (setsum Y1))).| < e1

hence
ex Y0 being finite Subset of X st |.(L . (x - (setsum Y1))).| < e1

let Y1 be finite Subset of X; :: thesis: ( Y0 c= Y1 & Y1 c= Y implies |.(L . (x - (setsum Y1))).| < e1 )

assume ( Y0 c= Y1 & Y1 c= Y ) ; :: thesis: |.(L . (x - (setsum Y1))).| < e1

then K * ||.(x - (setsum Y1)).|| < e1 by A2, A7, A6, XREAL_1:68;

then |.(L . (x - (setsum Y1))).| + (K * ||.(x - (setsum Y1)).||) < (K * ||.(x - (setsum Y1)).||) + e1 by A3, XREAL_1:8;

then (|.(L . (x - (setsum Y1))).| + (K * ||.(x - (setsum Y1)).||)) - (K * ||.(x - (setsum Y1)).||) < ((K * ||.(x - (setsum Y1)).||) + e1) - (K * ||.(x - (setsum Y1)).||) by XREAL_1:14;

hence |.(L . (x - (setsum Y1))).| < e1 ; :: thesis: verum

end;assume ( Y0 c= Y1 & Y1 c= Y ) ; :: thesis: |.(L . (x - (setsum Y1))).| < e1

then K * ||.(x - (setsum Y1)).|| < e1 by A2, A7, A6, XREAL_1:68;

then |.(L . (x - (setsum Y1))).| + (K * ||.(x - (setsum Y1)).||) < (K * ||.(x - (setsum Y1)).||) + e1 by A3, XREAL_1:8;

then (|.(L . (x - (setsum Y1))).| + (K * ||.(x - (setsum Y1)).||)) - (K * ||.(x - (setsum Y1)).||) < ((K * ||.(x - (setsum Y1)).||) + e1) - (K * ||.(x - (setsum Y1)).||) by XREAL_1:14;

hence |.(L . (x - (setsum Y1))).| < e1 ; :: thesis: verum

( 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))).| < e1 ) ) by 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 - (setsum Y1))).| < e1 ) ) ; :: thesis: verum