let X be RealUnitarySpace; :: thesis: for S being Subset of X st 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
|.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| < e ) )
let S be Subset of X; :: thesis: ( 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
|.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| < e ) ) )
assume A1: 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
|.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| < e ) )
consider Y02 being finite Subset of X such that
not Y02 is empty and
A2: Y02 c= S and
A3: 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;
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
|.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| < e ) ) )
assume A4: 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
|.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| < e ) )
set e9 = e / ((2 * ||.(sum S).||) + 1);
0 <= ||.(sum S).|| by BHSP_1:28;
then 0 <= 2 * ||.(sum S).|| ;
then A5: 0 + 0 < (2 * ||.(sum S).||) + 1 ;
then 0 < e / ((2 * ||.(sum S).||) + 1) by A4, XREAL_1:139;
then consider Y01 being finite Subset of X such that
A6: not Y01 is empty and
A7: Y01 c= S and
A8: 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;
set Y0 = Y01 \/ Y02;
A9: for Y1 being finite Subset of X st Y01 \/ Y02 c= Y1 & Y1 c= S holds
|.(((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 |.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| < e )
assume that
A10: Y01 \/ Y02 c= Y1 and
A11: Y1 c= S ; :: thesis: |.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| < e
set SS = (sum S) - (setsum Y1);
set SY = setsum Y1;
Y01 c= Y1 by A10, XBOOLE_1:11;
then A12: ||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1) < (e / ((2 * ||.(sum S).||) + 1)) * ((2 * ||.(sum S).||) + 1) by A5, A8, A11, XREAL_1:68;
||.(setsum Y1).|| = ||.(- (setsum Y1)).|| by BHSP_1:31
.= ||.((0. X) - (setsum Y1)).|| by RLVECT_1:14
.= ||.(((- (sum S)) + (sum S)) - (setsum Y1)).|| by RLVECT_1:5
.= ||.((- (sum S)) + ((sum S) - (setsum Y1))).|| by RLVECT_1:def 3 ;
then ||.(setsum Y1).|| <= ||.(- (sum S)).|| + ||.((sum S) - (setsum Y1)).|| by BHSP_1:30;
then A13: ||.(setsum Y1).|| <= ||.(sum S).|| + ||.((sum S) - (setsum Y1)).|| by BHSP_1:31;
Y02 c= Y1 by A10, XBOOLE_1:11;
then ||.((sum S) - (setsum Y1)).|| + ||.(setsum Y1).|| < 1 + (||.(sum S).|| + ||.((sum S) - (setsum Y1)).||) by A3, A11, A13, XREAL_1:8;
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:14;
then A14: ||.(sum S).|| + ||.(setsum Y1).|| < (1 + ||.(sum S).||) + ||.(sum S).|| by XREAL_1:8;
0 <= ||.((sum S) - (setsum Y1)).|| by BHSP_1:28;
then ||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||) <= ||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1) by A14, XREAL_1:64;
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 A12, XREAL_1:8;
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:14;
then A15: ||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||) < e by A5, XCMPLX_1:87;
set F = (sum S) .|. (sum S);
set G = (setsum Y1) .|. (setsum Y1);
|.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| = |.((((sum S) .|. (sum S)) - ((sum S) .|. (setsum Y1))) + (((sum S) .|. (setsum Y1)) - ((setsum Y1) .|. (setsum Y1)))).|
.= |.(((sum S) .|. ((sum S) - (setsum Y1))) + (((sum S) .|. (setsum Y1)) - ((setsum Y1) .|. (setsum Y1)))).| by BHSP_1:12
.= |.(((sum S) .|. ((sum S) - (setsum Y1))) + (((sum S) - (setsum Y1)) .|. (setsum Y1))).| by BHSP_1:11 ;
then A16: |.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| <= |.((sum S) .|. ((sum S) - (setsum Y1))).| + |.(((sum S) - (setsum Y1)) .|. (setsum Y1)).| by COMPLEX1:56;
|.((sum S) .|. ((sum S) - (setsum Y1))).| <= ||.(sum S).|| * ||.((sum S) - (setsum Y1)).|| by BHSP_1:29;
then |.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| + |.((sum S) .|. ((sum S) - (setsum Y1))).| <= (|.((sum S) .|. ((sum S) - (setsum Y1))).| + |.(((sum S) - (setsum Y1)) .|. (setsum Y1)).|) + (||.(sum S).|| * ||.((sum S) - (setsum Y1)).||) by A16, XREAL_1:7;
then |.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| + |.((sum S) .|. ((sum S) - (setsum Y1))).| <= (|.(((sum S) - (setsum Y1)) .|. (setsum Y1)).| + (||.(sum S).|| * ||.((sum S) - (setsum Y1)).||)) + |.((sum S) .|. ((sum S) - (setsum Y1))).| ;
then A17: |.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| <= |.(((sum S) - (setsum Y1)) .|. (setsum Y1)).| + (||.(sum S).|| * ||.((sum S) - (setsum Y1)).||) by XREAL_1:6;
|.(((sum S) - (setsum Y1)) .|. (setsum Y1)).| <= ||.((sum S) - (setsum Y1)).|| * ||.(setsum Y1).|| by BHSP_1:29;
then |.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| + |.(((sum S) - (setsum Y1)) .|. (setsum Y1)).| <= (|.(((sum S) - (setsum Y1)) .|. (setsum Y1)).| + (||.(sum S).|| * ||.((sum S) - (setsum Y1)).||)) + (||.((sum S) - (setsum Y1)).|| * ||.(setsum Y1).||) by A17, XREAL_1:7;
then |.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| + |.(((sum S) - (setsum Y1)) .|. (setsum Y1)).| <= ((||.(sum S).|| * ||.((sum S) - (setsum Y1)).||) + (||.((sum S) - (setsum Y1)).|| * ||.(setsum Y1).||)) + |.(((sum S) - (setsum Y1)) .|. (setsum Y1)).| ;
then |.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| <= (||.((sum S) - (setsum Y1)).|| * ||.(sum S).||) + (||.((sum S) - (setsum Y1)).|| * ||.(setsum Y1).||) by XREAL_1:6;
then |.(((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 A15, XREAL_1:8;
then (|.(((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:14;
hence |.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| < e ; :: thesis: verum
end;
Y01 \/ Y02 c= S by A7, A2, XBOOLE_1:8;
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
|.(((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))).| < e ) ) by A6, A9; :: thesis: verum