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

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

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.|| ;

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

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;

now :: thesis: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
|.(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;

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

end;

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

end;

hence Y is weakly_summable_set ; :: thesis: verum