:: On Some Properties of Real {H}ilbert Space, {II}
:: by Hiroshi Yamazaki , Yasumasa Suzuki , Takao Inou\'e and Yasunari Shidama
::
:: Received April 17, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

Lm1:  for x, y, z, e being Real st abs (x - y) < e / 2 &amp; abs (y - z) < e / 2 holds
abs (x - z) < e
proofend;

Lm2:  for p being real number st p > 0 holds
ex k being Element of NAT st 1 / (k + 1) < p
proofend;

Lm3:  for p being real number
for m being Element of NAT st p > 0 holds
ex i being Element of NAT st
( 1 / (i + 1) < p &amp; i >= m )
proofend;

theorem Th1: :: BHSP_7:1
for X being RealUnitarySpace
for Y being Subset of X
for L being Functional of X holds
( Y is_summable_set_by L iff for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= Y &amp; ( for Y1 being finite Subset of X st not Y1 is empty &amp; Y1 c= Y &amp; Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) ) )
proofend;

theorem Th2: :: BHSP_7:2
for X being RealUnitarySpace st the addF of X is commutative &amp; the addF of X is associative &amp; the addF of X is having_a_unity holds
for S being finite OrthogonalFamily of X st not S is empty holds
for I being Function of the carrier of X, the carrier of X st S c= dom I &amp; ( for y being Point of X st y in S holds
I . y = y ) holds
for H being Function of the carrier of X,REAL st S c= dom H &amp; ( for y being Point of X st y in S holds
H . y = y .|. y ) holds
(setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)
proofend;

theorem Th3: :: BHSP_7:3
for X being RealUnitarySpace st the addF of X is commutative &amp; the addF of X is associative &amp; the addF of X is having_a_unity holds
for S being finite OrthogonalFamily of X st not S is empty holds
for H being Functional of X st S c= dom H &amp; ( for x being Point of X st x in S holds
H . x = x .|. x ) holds
(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal)
proofend;

theorem Th4: :: BHSP_7:4
for X being RealUnitarySpace
for Y being OrthogonalFamily of X
for Z being Subset of X st Z is Subset of Y holds
Z is OrthogonalFamily of X
proofend;

theorem Th5: :: BHSP_7:5
for X being RealUnitarySpace
for Y being OrthonormalFamily of X
for Z being Subset of X st Z is Subset of Y holds
Z is OrthonormalFamily of X
proofend;

begin

theorem Th6: :: BHSP_7:6
for X being RealHilbertSpace st the addF of X is commutative &amp; the addF of X is associative &amp; the addF of X is having_a_unity holds
for S being OrthonormalFamily of X
for H being Functional of X st S c= dom H &amp; ( 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 )
proofend;

theorem Th7: :: BHSP_7:7
for X being RealUnitarySpace
for S being Subset of X st S is summable_set holds
for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty &amp; Y0 c= S &amp; ( for Y1 being finite Subset of X st Y0 c= Y1 &amp; Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) )
proofend;

Lm4:  for p1, p2 being real number st ( for e being Real st 0 < e holds
abs (p1 - p2) < e ) holds
p1 = p2
proofend;

theorem :: BHSP_7:8
for X being RealHilbertSpace st the addF of X is commutative &amp; the addF of X is associative &amp; the addF of X is having_a_unity holds
for S being OrthonormalFamily of X
for H being Functional of X st S c= dom H &amp; ( for x being Point of X st x in S holds
H . x = x .|. x ) &amp; S is summable_set holds
(sum S) .|. (sum S) = sum_byfunc (S,H)
proofend;