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 )

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

end;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 ) )

hence
S is_summable_set_by H
by Th1; :: thesis: verumex 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;( 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

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

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

end;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 ) )

hence
S is summable_set
by A1, BHSP_6:10; :: thesis: verumex 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;

( 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;( 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

hence
ex Y0 being finite Subset of X st ||.(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;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

( 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