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:
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 * ;
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 ;
A7: (e1 / K) * K = e1 by ;
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 ;
then |.(L . (x - (setsum Y1))).| + (K * ||.(x - (setsum Y1)).||) < (K * ||.(x - (setsum Y1)).||) + e1 by ;
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