let X be RealUnitarySpace; :: thesis: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity & X is Hilbert 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 ) & S is summable_set holds
(sum S) .|. (sum S) = sum_byfunc S,H )
assume that
A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) and
A2: X is Hilbert ; :: 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 ) & S is summable_set holds
(sum S) .|. (sum S) = sum_byfunc S,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 ) & S is summable_set holds
(sum S) .|. (sum S) = sum_byfunc S,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 ) & S is summable_set implies (sum S) .|. (sum S) = sum_byfunc S,H )
assume that
A3: S c= dom H and
A4: for x being Point of X st x in S holds
H . x = x .|. x ; :: thesis: ( not S is summable_set or (sum S) .|. (sum S) = sum_byfunc S,H )
A5: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= S holds
(setsum Y1) .|. (setsum Y1) = setopfunc Y1,the carrier of X,REAL ,H,addreal

proof

let Y1 be finite Subset of X; :: thesis: ( not Y1 is empty & Y1 c= S implies (setsum Y1) .|. (setsum Y1) = setopfunc Y1,the carrier of X,REAL ,H,addreal )
assume that
A6: not Y1 is empty and
A7: Y1 c= S ; :: thesis: (setsum Y1) .|. (setsum Y1) = setopfunc Y1,the carrier of X,REAL ,H,addreal
Y1 is finite OrthonormalFamily of X by A7, Th5;
then A8: 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 A4, A7;
hence (setsum Y1) .|. (setsum Y1) = setopfunc Y1,the carrier of X,REAL ,H,addreal by A1, A3, A6, A7, A8, Th3, XBOOLE_1:1; :: thesis: verum

end;

set p1 = (sum S) .|. (sum S);
set p2 = sum_byfunc S,H;
assume A9: S is summable_set ; :: thesis: (sum S) .|. (sum S) = sum_byfunc S,H
then A10: S is_summable_set_by H by A1, A2, A3, A4, Th6;
for e being Real st 0 < e holds
abs (((sum S) .|. (sum S)) - (sum_byfunc S,H)) < e

proof

let e be Real; :: thesis: ( 0 < e implies abs (((sum S) .|. (sum S)) - (sum_byfunc S,H)) < e )
assume 0 < e ; :: thesis: abs (((sum S) .|. (sum S)) - (sum_byfunc S,H)) < e
then A11: 0 / 2 < e / 2 by XREAL_1:76;
then consider Y02 being finite Subset of X such that
not Y02 is empty and
A12: Y02 c= S and
A13: for Y1 being finite Subset of X st Y02 c= Y1 & Y1 c= S holds
abs ((sum_byfunc S,H) - (setopfunc Y1,the carrier of X,REAL ,H,addreal )) < e / 2 by A10, BHSP_6:def 7;
consider Y01 being finite Subset of X such that
A14: not Y01 is empty and
A15: Y01 c= S and
A16: for Y1 being finite Subset of X st Y01 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e / 2 by A9, A11, Th7;
set Y1 = Y01 \/ Y02;
A17: Y01 \/ Y02 c= S by A15, A12, XBOOLE_1:8;
reconsider Y011 = Y01 as non empty set by A14;
set r = setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ;
Y01 \/ Y02 = Y011 \/ Y02 ;
then (setsum (Y01 \/ Y02)) .|. (setsum (Y01 \/ Y02)) = setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal by A5, A15, A12, XBOOLE_1:8;
then ( Y02 c= Y01 \/ Y02 & abs (((sum S) .|. (sum S)) - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal )) < e / 2 ) by A16, A17, XBOOLE_1:7;
then (abs (((sum S) .|. (sum S)) - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ))) + (abs ((sum_byfunc S,H) - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ))) < (e / 2) + (e / 2) by A13, A17, XREAL_1:10;
then A18: (abs (((sum S) .|. (sum S)) - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ))) + (abs ((setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ) - (sum_byfunc S,H))) < e by UNIFORM1:13;
((sum S) .|. (sum S)) - (sum_byfunc S,H) = (((sum S) .|. (sum S)) - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal )) + ((setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ) - (sum_byfunc S,H)) ;
then abs (((sum S) .|. (sum S)) - (sum_byfunc S,H)) <= (abs (((sum S) .|. (sum S)) - (setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ))) + (abs ((setopfunc (Y01 \/ Y02),the carrier of X,REAL ,H,addreal ) - (sum_byfunc S,H))) by COMPLEX1:142;
hence abs (((sum S) .|. (sum S)) - (sum_byfunc S,H)) < e by A18, XXREAL_0:2; :: thesis: verum

end;

hence (sum S) .|. (sum S) = sum_byfunc S,H by Lm4; :: thesis: verum