:: BHSP_7 semantic presentation

Lemma1: for b1, b2, b3, b4 being Real st abs (b1 - b2) < b4 / 2 & abs (b2 - b3) < b4 / 2 holds
abs (b1 - b3) < b4
proof end;

Lemma2: for b1 being real number st b1 > 0 holds
ex b2 being Nat st 1 / (b2 + 1) < b1
proof end;

Lemma3: for b1 being real number
for b2 being Nat st b1 > 0 holds
ex b3 being Nat st
( 1 / (b3 + 1) < b1 & b3 >= b2 )
proof end;

theorem Th1: :: BHSP_7:1
for b1 being RealUnitarySpace
for b2 being Subset of b1
for b3 being Functional of b1 holds
( b2 is_summable_set_by b3 iff for b4 being Real st 0 < b4 holds
ex b5 being finite Subset of b1 st
( not b5 is empty & b5 c= b2 & ( for b6 being finite Subset of b1 st not b6 is empty & b6 c= b2 & b5 misses b6 holds
abs (setopfunc b6,the carrier of b1,REAL ,b3,addreal ) < b4 ) ) )
proof end;

theorem Th2: :: BHSP_7:2
for b1 being RealUnitarySpace st the add of b1 is commutative & the add of b1 is associative & the add of b1 has_a_unity holds
for b2 being finite OrthogonalFamily of b1 st not b2 is empty holds
for b3 being Function of the carrier of b1,the carrier of b1 st b2 c= dom b3 & ( for b4 being Point of b1 st b4 in b2 holds
b3 . b4 = b4 ) holds
for b4 being Function of the carrier of b1, REAL st b2 c= dom b4 & ( for b5 being Point of b1 st b5 in b2 holds
b4 . b5 = b5 .|. b5 ) holds
(setopfunc b2,the carrier of b1,the carrier of b1,b3,the add of b1) .|. (setopfunc b2,the carrier of b1,the carrier of b1,b3,the add of b1) = setopfunc b2,the carrier of b1,REAL ,b4,addreal
proof end;

theorem Th3: :: BHSP_7:3
for b1 being RealUnitarySpace st the add of b1 is commutative & the add of b1 is associative & the add of b1 has_a_unity holds
for b2 being finite OrthogonalFamily of b1 st not b2 is empty holds
for b3 being Functional of b1 st b2 c= dom b3 & ( for b4 being Point of b1 st b4 in b2 holds
b3 . b4 = b4 .|. b4 ) holds
(setsum b2) .|. (setsum b2) = setopfunc b2,the carrier of b1,REAL ,b3,addreal
proof end;

theorem Th4: :: BHSP_7:4
for b1 being RealUnitarySpace
for b2 being OrthogonalFamily of b1
for b3 being Subset of b1 st b3 is Subset of b2 holds
b3 is OrthogonalFamily of b1
proof end;

theorem Th5: :: BHSP_7:5
for b1 being RealUnitarySpace
for b2 being OrthonormalFamily of b1
for b3 being Subset of b1 st b3 is Subset of b2 holds
b3 is OrthonormalFamily of b1
proof end;

theorem Th6: :: BHSP_7:6
for b1 being RealUnitarySpace st the add of b1 is commutative & the add of b1 is associative & the add of b1 has_a_unity & b1 is_Hilbert_space holds
for b2 being OrthonormalFamily of b1
for b3 being Functional of b1 st b2 c= dom b3 & ( for b4 being Point of b1 st b4 in b2 holds
b3 . b4 = b4 .|. b4 ) holds
( b2 is summable_set iff b2 is_summable_set_by b3 )
proof end;

theorem Th7: :: BHSP_7:7
for b1 being RealUnitarySpace
for b2 being Subset of b1 st not b2 is empty & b2 is summable_set holds
for b3 being Real st 0 < b3 holds
ex b4 being finite Subset of b1 st
( not b4 is empty & b4 c= b2 & ( for b5 being finite Subset of b1 st b4 c= b5 & b5 c= b2 holds
abs (((sum b2) .|. (sum b2)) - ((setsum b5) .|. (setsum b5))) < b3 ) )
proof end;

Lemma11: for b1, b2 being real number st ( for b3 being Real st 0 < b3 holds
abs (b1 - b2) < b3 ) holds
b1 = b2
proof end;

theorem Th8: :: BHSP_7:8
for b1 being RealUnitarySpace st the add of b1 is commutative & the add of b1 is associative & the add of b1 has_a_unity & b1 is_Hilbert_space holds
for b2 being OrthonormalFamily of b1 st not b2 is empty holds
for b3 being Functional of b1 st b2 c= dom b3 & ( for b4 being Point of b1 st b4 in b2 holds
b3 . b4 = b4 .|. b4 ) & b2 is summable_set holds
(sum b2) .|. (sum b2) = sum_byfunc b2,b3
proof end;