let X be RealUnitarySpace; :: thesis:
assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity & X is Hilbert ) ; :: thesis:
let S be OrthonormalFamily of X; :: thesis:
let H be Functional of X; :: thesis:
assume A2: ( S c= dom H & ( for x being Point of X st x in S holds
H . x = x .|. x ) ) ; :: thesis:

A3: now

assume A4: S is summable_set ; :: thesis:

now

let e be Real; :: thesis:
assume A5: 0 < e ; :: thesis:
set e' = sqrt e;
0 < sqrt e by A5, SQUARE_1:93;
then consider e1 being Real such that
A6: ( 0 < e1 & e1 < sqrt e ) by CHAIN_1:1;
e1 ^2 < (sqrt e) ^2 by A6, SQUARE_1:78;
then A7: ( e1 > 0 & e1 * e1 < e ) by A5, A6, SQUARE_1:def 4;
consider Y0 being finite Subset of X such that
A8: ( 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).|| < e1 ) ) by A1, A4, A6, BHSP_6:10;
take Y0 = Y0; :: thesis:
thus ( not Y0 is empty & Y0 c= S ) by A8; :: thesis:
let Y1 be finite Subset of X; :: thesis:
assume A9: ( not Y1 is empty & Y1 c= S & Y0 misses Y1 ) ; :: thesis:
0 <= ||.(setsum Y1).|| by BHSP_1:34;
then ||.(setsum Y1).|| ^2 < e1 ^2 by A8, A9, SQUARE_1:78;
then A10: ||.(setsum Y1).|| ^2 < e by A7, XXREAL_0:2;
Y1 is finite OrthonormalFamily of X by A9, Th5;
then A11: 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 A2, A9;
then A13: (setsum Y1) .|. (setsum Y1) = setopfunc Y1,the carrier of X,REAL ,H,addreal by A1, A9, A11, Th3, A2, XBOOLE_1:1;
A14: ||.(setsum Y1).|| = sqrt ((setsum Y1) .|. (setsum Y1)) by BHSP_1:def 4;
0 <= (setsum Y1) .|. (setsum Y1) by BHSP_1:def 2;
then A15: ||.(setsum Y1).|| ^2 = setopfunc Y1,the carrier of X,REAL ,H,addreal by A13, A14, SQUARE_1:def 4;
0 <= setopfunc Y1,the carrier of X,REAL ,H,addreal by A13, BHSP_1:def 2;
hence abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ) < e by A10, A15, ABSVALUE:def 1; :: thesis:

end;

hence S is_summable_set_by H by Th1; :: thesis:

end;

now

assume A16: S is_summable_set_by H ; :: thesis:

now

let e be Real; :: thesis:
assume A17: 0 < e ; :: thesis:
set e1 = e * e;
( 0 < e * e & e * e = e * e ) by A17, XREAL_1:131;
then consider Y0 being finite Subset of X such that
A18: ( 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
abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ) < e * e ) ) by A16, Th1;

now

let Y1 be finite Subset of X; :: thesis:
assume A19: ( not Y1 is empty & Y1 c= S & Y0 misses Y1 ) ; :: thesis:
set F = setopfunc Y1,the carrier of X,REAL ,H,addreal ;
A20: abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ) < e * e by A18, A19;
setopfunc Y1,the carrier of X,REAL ,H,addreal <= abs (setopfunc Y1,the carrier of X,REAL ,H,addreal ) by ABSVALUE:11;
then (setopfunc Y1,the carrier of X,REAL ,H,addreal ) - (e * e) < (abs (setopfunc Y1,the carrier of X,REAL ,H,addreal )) - (abs (setopfunc Y1,the carrier of X,REAL ,H,addreal )) by A20, XREAL_1:17;
then A21: setopfunc Y1,the carrier of X,REAL ,H,addreal < e * e by XREAL_1:50;
Y1 is finite OrthonormalFamily of X by A19, Th5;
then A22: 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 A2, A19;
then A24: (setsum Y1) .|. (setsum Y1) = setopfunc Y1,the carrier of X,REAL ,H,addreal by A1, A19, A22, Th3, A2, XBOOLE_1:1;
A25: 0 <= (setsum Y1) .|. (setsum Y1) by BHSP_1:def 2;
||.(setsum Y1).|| = sqrt ((setsum Y1) .|. (setsum Y1)) by BHSP_1:def 4;
then ||.(setsum Y1).|| ^2 < e * e by A21, A24, A25, SQUARE_1:def 4;
then sqrt (||.(setsum Y1).|| ^2 ) < sqrt (e ^2 ) by SQUARE_1:95, XREAL_1:65;
then sqrt (||.(setsum Y1).|| ^2 ) < e by A17, SQUARE_1:89;
hence ||.(setsum Y1).|| < e by BHSP_1:34, SQUARE_1:89; :: thesis:

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 A18; :: thesis:

end;

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

end;

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