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

now

let L be linear-Functional of X; :: thesis: ( L is Bounded 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
abs (L . (x - (setsum Y1))) < e1 ) ) )
assume A2: L is Bounded ; :: 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
abs (L . (x - (setsum Y1))) < e1 ) )
consider K being Real such that
A3: ( 0 < K & ( for x being Point of X holds abs (L . x) <= K * ||.x.|| ) ) by A2, Def4;

now

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
abs (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
abs (L . (x - (setsum Y1))) < e1 ) )
set e = e1 / K;
A5: 0 < e1 / K by A3, A4, XREAL_1:141;
A6: (e1 / K) * K = e1 by A3, XCMPLX_1:88;
consider Y0 being finite Subset of X such that
A7: ( 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)).|| < e1 / K ) ) by A1, A5;

now

let Y1 be finite Subset of X; :: thesis: ( Y0 c= Y1 & Y1 c= Y implies abs (L . (x - (setsum Y1))) < e1 )
assume A8: ( Y0 c= Y1 & Y1 c= Y ) ; :: thesis: abs (L . (x - (setsum Y1))) < e1
K * ||.(x - (setsum Y1)).|| < e1 by A3, A6, A7, A8, XREAL_1:70;
then (abs (L . (x - (setsum Y1)))) + (K * ||.(x - (setsum Y1)).||) < (K * ||.(x - (setsum Y1)).||) + e1 by A3, XREAL_1:10;
then ((abs (L . (x - (setsum Y1)))) + (K * ||.(x - (setsum Y1)).||)) - (K * ||.(x - (setsum Y1)).||) < ((K * ||.(x - (setsum Y1)).||) + e1) - (K * ||.(x - (setsum Y1)).||) by XREAL_1:16;
hence abs (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
abs (L . (x - (setsum Y1))) < e1 ) ) by A7; :: 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
abs (L . (x - (setsum Y1))) < e1 ) ) ; :: thesis: verum

end;

hence Y is weakly_summable_set by Def5; :: thesis: verum