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 ) & S is summable_set holds
(sum S) .|. (sum S) = sum_byfunc (S,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 ) & 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, 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