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

end;

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

proof

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

end;

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