let X be RealHilbertSpace; :: thesis: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity implies for S being OrthonormalFamily of X
for H being Functional of X st S c= dom H & ( for x being Point of X st x in S holds
H . x = x .|. x ) holds
( S is summable_set iff S is_summable_set_by H ) )
assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) ; :: thesis: for S being OrthonormalFamily of X
for H being Functional of X st S c= dom H & ( for x being Point of X st x in S holds
H . x = x .|. x ) holds
( S is summable_set iff S is_summable_set_by H )
let S be OrthonormalFamily of X; :: thesis: for H being Functional of X st S c= dom H & ( for x being Point of X st x in S holds
H . x = x .|. x ) holds
( S is summable_set iff S is_summable_set_by H )
let H be Functional of X; :: thesis: ( S c= dom H & ( for x being Point of X st x in S holds
H . x = x .|. x ) implies ( S is summable_set iff S is_summable_set_by H ) )
assume that
A2: S c= dom H and
A3: for x being Point of X st x in S holds
H . x = x .|. x ; :: thesis: ( S is summable_set iff S is_summable_set_by H )

A4: now :: thesis: ( S is summable_set implies S is_summable_set_by H )

assume A5: S is summable_set ; :: thesis: S is_summable_set_by H

now :: 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 not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,H,addreal)).| < 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 not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,H,addreal)).| < e ) ) )
assume A6: 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 not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,H,addreal)).| < e ) )
set e9 = sqrt e;
0 < sqrt e by A6, SQUARE_1:25;
then consider e1 being Element of REAL such that
A7: 0 < e1 and
A8: e1 < sqrt e by CHAIN_1:1;
e1 ^2 < (sqrt e) ^2 by A7, A8, SQUARE_1:16;
then A9: e1 * e1 < e by A6, SQUARE_1:def 2;
consider Y0 being finite Subset of X such that
A10: ( not Y0 is empty & Y0 c= S ) and
A11: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
||.(setsum Y1).|| < e1 by A1, A5, A7, BHSP_6:10;
take Y0 = Y0; :: thesis: ( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,H,addreal)).| < e ) )
thus ( not Y0 is empty & Y0 c= S ) by A10; :: thesis: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,H,addreal)).| < e
let Y1 be finite Subset of X; :: thesis: ( not Y1 is empty & Y1 c= S & Y0 misses Y1 implies |.(setopfunc (Y1, the carrier of X,REAL,H,addreal)).| < e )
assume that
A12: not Y1 is empty and
A13: Y1 c= S and
A14: Y0 misses Y1 ; :: thesis: |.(setopfunc (Y1, the carrier of X,REAL,H,addreal)).| < e
Y1 is finite OrthonormalFamily of X by A13, Th5;
then A15: Y1 is finite OrthogonalFamily of X by BHSP_5:def 9;
for x being Point of X st x in Y1 holds
H . x = x .|. x by A3, A13;
then A16: (setsum Y1) .|. (setsum Y1) = setopfunc (Y1, the carrier of X,REAL,H,addreal) by A1, A2, A12, A13, A15, Th3, XBOOLE_1:1;
0 <= ||.(setsum Y1).|| by BHSP_1:28;
then ||.(setsum Y1).|| ^2 < e1 ^2 by A11, A12, A13, A14, SQUARE_1:16;
then A17: ||.(setsum Y1).|| ^2 < e by A9, XXREAL_0:2;
( ||.(setsum Y1).|| = sqrt ((setsum Y1) .|. (setsum Y1)) & 0 <= (setsum Y1) .|. (setsum Y1) ) by BHSP_1:def 2, BHSP_1:def 4;
then A18: ||.(setsum Y1).|| ^2 = setopfunc (Y1, the carrier of X,REAL,H,addreal) by A16, SQUARE_1:def 2;
0 <= setopfunc (Y1, the carrier of X,REAL,H,addreal) by A16, BHSP_1:def 2;
hence |.(setopfunc (Y1, the carrier of X,REAL,H,addreal)).| < e by A17, A18, ABSVALUE:def 1; :: thesis: verum

end;

hence S is_summable_set_by H by Th1; :: thesis: verum

end;

now :: thesis: ( S is_summable_set_by H implies S is summable_set )

assume A19: S is_summable_set_by H ; :: thesis: S is summable_set

now :: 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 not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
||.(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 not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) )
assume A20: 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 not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) )
set e1 = e * e;
0 < e * e by A20, XREAL_1:129;
then consider Y0 being finite Subset of X such that
A21: ( not Y0 is empty & Y0 c= S ) and
A22: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
|.(setopfunc (Y1, the carrier of X,REAL,H,addreal)).| < e * e by A19, Th1;

now :: thesis: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
||.(setsum Y1).|| < e

let Y1 be finite Subset of X; :: thesis: ( not Y1 is empty & Y1 c= S & Y0 misses Y1 implies ||.(setsum Y1).|| < e )
assume that
A23: not Y1 is empty and
A24: Y1 c= S and
A25: Y0 misses Y1 ; :: thesis: ||.(setsum Y1).|| < e
set F = setopfunc (Y1, the carrier of X,REAL,H,addreal);
Y1 is finite OrthonormalFamily of X by A24, Th5;
then A26: Y1 is finite OrthogonalFamily of X by BHSP_5:def 9;
|.(setopfunc (Y1, the carrier of X,REAL,H,addreal)).| < e * e by A22, A23, A24, A25;
then (setopfunc (Y1, the carrier of X,REAL,H,addreal)) - (e * e) < |.(setopfunc (Y1, the carrier of X,REAL,H,addreal)).| - |.(setopfunc (Y1, the carrier of X,REAL,H,addreal)).| by ABSVALUE:4, XREAL_1:15;
then A27: setopfunc (Y1, the carrier of X,REAL,H,addreal) < e * e by XREAL_1:48;
for x being Point of X st x in Y1 holds
H . x = x .|. x by A3, A24;
then A28: (setsum Y1) .|. (setsum Y1) = setopfunc (Y1, the carrier of X,REAL,H,addreal) by A1, A2, A23, A24, A26, Th3, XBOOLE_1:1;
( 0 <= (setsum Y1) .|. (setsum Y1) & ||.(setsum Y1).|| = sqrt ((setsum Y1) .|. (setsum Y1)) ) by BHSP_1:def 2, BHSP_1:def 4;
then ||.(setsum Y1).|| ^2 < e * e by A27, A28, SQUARE_1:def 2;
then sqrt (||.(setsum Y1).|| ^2) < sqrt (e ^2) by SQUARE_1:27, XREAL_1:63;
then sqrt (||.(setsum Y1).|| ^2) < e by A20, SQUARE_1:22;
hence ||.(setsum Y1).|| < e by BHSP_1:28, SQUARE_1:22; :: 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 not Y1 is empty & Y1 c= S & Y0 misses Y1 holds
||.(setsum Y1).|| < e ) ) by A21; :: thesis: verum

end;

hence S is summable_set by A1, BHSP_6:10; :: thesis: verum

end;

hence ( S is summable_set iff S is_summable_set_by H ) by A4; :: thesis: verum