let X be RealUnitarySpace; :: thesis: for S being Subset of X st not S is empty & S is summable_set holds
for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) )
let S be Subset of X; :: thesis: ( not S is empty & S is summable_set implies for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) ) )
assume A1: ( not S is empty & S is summable_set ) ; :: thesis: for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) )
let e be Real; :: thesis: ( 0 < e implies ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) ) )
assume A2: 0 < e ; :: thesis: ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) )
0 <= ||.(sum S).|| by BHSP_1:34;
then 0 <= 2 * ||.(sum S).|| by XREAL_1:129;
then A3: 0 + 0 < (2 * ||.(sum S).||) + 1 by XREAL_1:10;
set e' = e / ((2 * ||.(sum S).||) + 1);
0 < e / ((2 * ||.(sum S).||) + 1) by A2, A3, XREAL_1:141;
then consider Y01 being finite Subset of X such that
A4: ( not Y01 is empty & Y01 c= S & ( for Y1 being finite Subset of X st Y01 c= Y1 & Y1 c= S holds
||.((sum S) - (setsum Y1)).|| < e / ((2 * ||.(sum S).||) + 1) ) ) by A1, BHSP_6:def 3;
consider Y02 being finite Subset of X such that
A5: ( not Y02 is empty & Y02 c= S & ( for Y1 being finite Subset of X st Y02 c= Y1 & Y1 c= S holds
||.((sum S) - (setsum Y1)).|| < 1 ) ) by A1, BHSP_6:def 3;
set Y0 = Y01 \/ Y02;
ex x being set st x in Y01 by A4, XBOOLE_0:def 1;
then A6: not Y01 \/ Y02 is empty ;
A7: Y01 \/ Y02 c= S by A4, A5, XBOOLE_1:8;
for Y1 being finite Subset of X st Y01 \/ Y02 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e

proof

let Y1 be finite Subset of X; :: thesis: ( Y01 \/ Y02 c= Y1 & Y1 c= S implies abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e )
assume A8: ( Y01 \/ Y02 c= Y1 & Y1 c= S ) ; :: thesis: abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e
set F = (sum S) .|. (sum S);
set G = (setsum Y1) .|. (setsum Y1);
set SS = (sum S) - (setsum Y1);
set SY = setsum Y1;
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) = abs ((((sum S) .|. (sum S)) - ((sum S) .|. (setsum Y1))) + (((sum S) .|. (setsum Y1)) - ((setsum Y1) .|. (setsum Y1))))
.= abs (((sum S) .|. ((sum S) - (setsum Y1))) + (((sum S) .|. (setsum Y1)) - ((setsum Y1) .|. (setsum Y1)))) by BHSP_1:17
.= abs (((sum S) .|. ((sum S) - (setsum Y1))) + (((sum S) - (setsum Y1)) .|. (setsum Y1))) by BHSP_1:16 ;
then A9: abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) <= (abs ((sum S) .|. ((sum S) - (setsum Y1)))) + (abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) by COMPLEX1:142;
abs ((sum S) .|. ((sum S) - (setsum Y1))) <= ||.(sum S).|| * ||.((sum S) - (setsum Y1)).|| by BHSP_1:35;
then (abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1)))) + (abs ((sum S) .|. ((sum S) - (setsum Y1)))) <= ((abs ((sum S) .|. ((sum S) - (setsum Y1)))) + (abs (((sum S) - (setsum Y1)) .|. (setsum Y1)))) + (||.(sum S).|| * ||.((sum S) - (setsum Y1)).||) by A9, XREAL_1:9;
then (abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1)))) + (abs ((sum S) .|. ((sum S) - (setsum Y1)))) <= ((abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) + (||.(sum S).|| * ||.((sum S) - (setsum Y1)).||)) + (abs ((sum S) .|. ((sum S) - (setsum Y1)))) ;
then A10: abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) <= (abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) + (||.(sum S).|| * ||.((sum S) - (setsum Y1)).||) by XREAL_1:8;
abs (((sum S) - (setsum Y1)) .|. (setsum Y1)) <= ||.((sum S) - (setsum Y1)).|| * ||.(setsum Y1).|| by BHSP_1:35;
then (abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1)))) + (abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) <= ((abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) + (||.(sum S).|| * ||.((sum S) - (setsum Y1)).||)) + (||.((sum S) - (setsum Y1)).|| * ||.(setsum Y1).||) by A10, XREAL_1:9;
then (abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1)))) + (abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) <= ((||.(sum S).|| * ||.((sum S) - (setsum Y1)).||) + (||.((sum S) - (setsum Y1)).|| * ||.(setsum Y1).||)) + (abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) ;
then A11: abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) <= (||.((sum S) - (setsum Y1)).|| * ||.(sum S).||) + (||.((sum S) - (setsum Y1)).|| * ||.(setsum Y1).||) by XREAL_1:8;
||.(setsum Y1).|| = ||.(- (setsum Y1)).|| by BHSP_1:37
.= ||.((0. X) - (setsum Y1)).|| by RLVECT_1:27
.= ||.(((- (sum S)) + (sum S)) - (setsum Y1)).|| by RLVECT_1:16
.= ||.((- (sum S)) + ((sum S) - (setsum Y1))).|| by RLVECT_1:def 6 ;
then ||.(setsum Y1).|| <= ||.(- (sum S)).|| + ||.((sum S) - (setsum Y1)).|| by BHSP_1:36;
then A12: ||.(setsum Y1).|| <= ||.(sum S).|| + ||.((sum S) - (setsum Y1)).|| by BHSP_1:37;
Y02 c= Y1 by A8, XBOOLE_1:11;
then ||.((sum S) - (setsum Y1)).|| + ||.(setsum Y1).|| < 1 + (||.(sum S).|| + ||.((sum S) - (setsum Y1)).||) by A5, A8, A12, XREAL_1:10;
then (||.(setsum Y1).|| + ||.((sum S) - (setsum Y1)).||) - ||.((sum S) - (setsum Y1)).|| < ((1 + ||.(sum S).||) + ||.((sum S) - (setsum Y1)).||) - ||.((sum S) - (setsum Y1)).|| by XREAL_1:16;
then A13: ||.(sum S).|| + ||.(setsum Y1).|| < (1 + ||.(sum S).||) + ||.(sum S).|| by XREAL_1:10;
0 <= ||.((sum S) - (setsum Y1)).|| by BHSP_1:34;
then A14: ||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||) <= ||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1) by A13, XREAL_1:66;
Y01 c= Y1 by A8, XBOOLE_1:11;
then ||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1) < (e / ((2 * ||.(sum S).||) + 1)) * ((2 * ||.(sum S).||) + 1) by A3, A4, A8, XREAL_1:70;
then (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||)) + (||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1)) < ((e / ((2 * ||.(sum S).||) + 1)) * ((2 * ||.(sum S).||) + 1)) + (||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1)) by A14, XREAL_1:10;
then ((||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||)) + (||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1))) - (||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1)) < (((e / ((2 * ||.(sum S).||) + 1)) * ((2 * ||.(sum S).||) + 1)) + (||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1))) - (||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1)) by XREAL_1:16;
then ||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||) < e by A3, XCMPLX_1:88;
then (abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1)))) + (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||)) < e + (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||)) by A11, XREAL_1:10;
then ((abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1)))) + (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||))) - (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||)) < (e + (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||))) - (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||)) by XREAL_1:16;
hence abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ; :: thesis: verum

end;

hence ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) ) by A6, A7; :: thesis: verum