:: BHSP_7 semantic presentation

begin

     Lm1:  for x, y, z, e being Real st abs (x - y) < e / 2 & abs (y - z) < e / 2 holds
abs (x - z) < e
proof
let x, y, z, e be Real; ::_thesis: ( abs (x - y) < e / 2 & abs (y - z) < e / 2 implies abs (x - z) < e )
assume  ( abs (x - y) < e / 2 & abs (y - z) < e / 2 ) ; ::_thesis: abs (x - z) < e
then  ( abs ((x - y) + (y - z)) <= (abs (x - y)) + (abs (y - z)) & (abs (x - y)) + (abs (y - z)) < (e / 2) + (e / 2) ) by COMPLEX1:56, XREAL_1:8;
hence  abs (x - z) < e by XXREAL_0:2; ::_thesis: verum
end;

Lm2:  for p being real number st p > 0 holds
ex k being Element of NAT st 1 / (k + 1) < p
proof
let p be real number ; ::_thesis: ( p > 0 implies ex k being Element of NAT st 1 / (k + 1) < p )
consider k1 being Element of NAT  such that
A1: p " < k1 by SEQ_4:3;
assume  p > 0 ; ::_thesis: ex k being Element of NAT st 1 / (k + 1) < p
then A2: 0 < p " by XREAL_1:122;
take  k1 ; ::_thesis: 1 / (k1 + 1) < p
 (p ") + 0 < k1 + 1 by A1, XREAL_1:8;
then  1 / (k1 + 1) < 1 / (p ") by A2, XREAL_1:76;
hence  1 / (k1 + 1) < p by XCMPLX_1:216; ::_thesis: verum
end;

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 & i >= m )
proof
let p be real number ; ::_thesis: for m being Element of NAT st p > 0 holds
ex i being Element of NAT st
( 1 / (i + 1) < p & i >= m )
let m be Element of NAT ; ::_thesis: ( p > 0 implies ex i being Element of NAT st
( 1 / (i + 1) < p & i >= m ) )
consider k1 being Element of NAT  such that
A1: p " < k1 by SEQ_4:3;
assume  p > 0 ; ::_thesis: ex i being Element of NAT st
( 1 / (i + 1) < p & i >= m )
then A2: 0 < p " by XREAL_1:122;
take i = k1 + m; ::_thesis: ( 1 / (i + 1) < p & i >= m )
 k1 <= k1 + m by NAT_1:11;
then  p " < i by A1, XXREAL_0:2;
then  (p ") + 0 < i + 1 by XREAL_1:8;
then  1 / (i + 1) < 1 / (p ") by A2, XREAL_1:76;
hence  ( 1 / (i + 1) < p & i >= m ) by NAT_1:11, XCMPLX_1:216; ::_thesis: verum
end;

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 & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) ) )
proof
let X be RealUnitarySpace; ::_thesis: 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 & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) ) )
let Y be Subset of X; ::_thesis: 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 & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) ) )
let L be Functional of X; ::_thesis: ( 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 & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) ) )
thus  ( Y is_summable_set_by L implies for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) ) ) ::_thesis: ( ( for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) ) ) implies Y is_summable_set_by L )
proof
assume  Y is_summable_set_by L ; ::_thesis: for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) )
then consider r being Real such that
A1: for e being Real st e > 0 holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) by BHSP_6:def_6;
 for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) )
proof
let e be Real; ::_thesis: ( 0 < e implies ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) ) )
assume  0 < e ; ::_thesis: ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) )
then consider Y0 being finite Subset of X such that
A2: not Y0 is empty and
A3: Y0 c= Y and
A4: for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e / 2 by A1, XREAL_1:139;
 for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e
proof
let Y1 be finite Subset of X; ::_thesis: ( not Y1 is empty & Y1 c= Y & Y0 misses Y1 implies abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e )
assume that
 not Y1 is empty and
A5: Y1 c= Y and
A6: Y0 misses Y1 ; ::_thesis: abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e
set Y19 = Y0 \/ Y1;
 dom L = the carrier of X by FUNCT_2:def_1;
then  setopfunc ((Y0 \/ Y1), the carrier of X,REAL,L,addreal) = addreal . ((setopfunc (Y0, the carrier of X,REAL,L,addreal)),(setopfunc (Y1, the carrier of X,REAL,L,addreal))) by A6, BHSP_5:14
.= (setopfunc (Y0, the carrier of X,REAL,L,addreal)) + (setopfunc (Y1, the carrier of X,REAL,L,addreal)) by BINOP_2:def_9 ;
then A7: setopfunc (Y1, the carrier of X,REAL,L,addreal) = (setopfunc ((Y0 \/ Y1), the carrier of X,REAL,L,addreal)) - (setopfunc (Y0, the carrier of X,REAL,L,addreal)) ;
 Y0 c= Y0 \/ Y1 by XBOOLE_1:7;
then  abs (r - (setopfunc ((Y0 \/ Y1), the carrier of X,REAL,L,addreal))) < e / 2 by A3, A4, A5, XBOOLE_1:8;
then A8: abs ((setopfunc ((Y0 \/ Y1), the carrier of X,REAL,L,addreal)) - r) < e / 2 by UNIFORM1:11;
 abs (r - (setopfunc (Y0, the carrier of X,REAL,L,addreal))) < e / 2 by A3, A4;
hence  abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e by A8, A7, Lm1; ::_thesis: verum
end;
hence  ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) ) by A2, A3; ::_thesis: verum
end;
hence  for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) ) ; ::_thesis: verum
end;
assume A9: for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) ) ; ::_thesis: Y is_summable_set_by L
 ex r being Real st
for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) )
proof
defpred S1[ set , set ] means ( $2 is finite Subset of X & not $2 is empty & $2 c= Y & ( for z being Real st z = $1 holds
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & $2 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / (z + 1) ) );
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
ex_y_being_set_st_
(_y_in_bool_Y_&_y_is_finite_Subset_of_X_&_not_y_is_empty_&_y_c=_Y_&_(_for_z_being_Real_st_z_=_x_holds_
for_Y1_being_finite_Subset_of_X_st_not_Y1_is_empty_&_Y1_c=_Y_&_y_misses_Y1_holds_
abs_(setopfunc_(Y1,_the_carrier_of_X,REAL,L,addreal))_<_1_/_(z_+_1)_)_)
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in bool Y & y is finite Subset of X & not y is empty & y c= Y & ( for z being Real st z = x holds
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & y misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / (z + 1) ) ) )
assume  x in NAT ; ::_thesis: ex y being set st
( y in bool Y & y is finite Subset of X & not y is empty & y c= Y & ( for z being Real st z = x holds
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & y misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / (z + 1) ) )
then reconsider xx = x as Element of NAT ;
reconsider e = 1 / (xx + 1) as Real ;
 0 <= xx by NAT_1:2;
then  0 < xx + 1 by NAT_1:13;
then  0 / (xx + 1) < 1 / (xx + 1) by XREAL_1:74;
then consider Y0 being finite Subset of X such that
A10: not Y0 is empty and
A11: ( Y0 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < e ) ) by A9;
 ( Y0 in bool Y & ( for z being Real st z = x holds
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / (z + 1) ) ) by A11, ZFMISC_1:def_1;
hence  ex y being set st
( y in bool Y & y is finite Subset of X & not y is empty & y c= Y & ( for z being Real st z = x holds
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & y misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / (z + 1) ) ) by A10; ::_thesis: verum
end;
then A12: for x being set st x in NAT holds
ex y being set st
( y in bool Y & S1[x,y] ) ;
A13: ex B being Function of NAT,(bool Y) st
for x being set st x in NAT holds
S1[x,B . x] from FUNCT_2:sch_1(A12);
 ex A being Function of NAT,(bool Y) st
for i being Element of NAT holds
( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds
A . i c= A . j ) )
proof
consider B being Function of NAT,(bool Y) such that
A14: for x being set st x in NAT holds
( B . x is finite Subset of X & not B . x is empty & B . x c= Y & ( for z being Real st z = x holds
for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & B . x misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / (z + 1) ) ) by A13;
deffunc H1( Nat, set ) ->  set = (B . ($1 + 1)) \/ $2;
 ex A being Function st
( dom A = NAT & A . 0 = B . 0 & ( for n being Nat holds A . (n + 1) = H1(n,A . n) ) ) from NAT_1:sch_11();
then consider A being Function such that
A15: dom A = NAT and
A16: A . 0 = B . 0 and
A17: for n being Nat holds A . (n + 1) = (B . (n + 1)) \/ (A . n) ;
defpred S2[ Element of NAT ] means ( A . $1 is finite Subset of X & not A . $1 is empty & A . $1 c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . $1 misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / ($1 + 1) ) & ( for j being Element of NAT st $1 <= j holds
A . $1 c= A . j ) );
A18: now__::_thesis:_for_n_being_Element_of_NAT_st_S2[n]_holds_
S2[n_+_1]
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A19: S2[n] ; ::_thesis: S2[n + 1]
A20: for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . (n + 1) misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / ((n + 1) + 1)
proof
let Y1 be finite Subset of X; ::_thesis: ( not Y1 is empty & Y1 c= Y & A . (n + 1) misses Y1 implies abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / ((n + 1) + 1) )
assume that
A21: ( not Y1 is empty & Y1 c= Y ) and
A22: A . (n + 1) misses Y1 ; ::_thesis: abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / ((n + 1) + 1)
 A . (n + 1) = (B . (n + 1)) \/ (A . n) by A17;
then  B . (n + 1) misses Y1 by A22, XBOOLE_1:7, XBOOLE_1:63;
hence  abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / ((n + 1) + 1) by A14, A21; ::_thesis: verum
end;
defpred S3[ Element of NAT ] means ( n + 1 <= $1 implies A . (n + 1) c= A . $1 );
A23: for j being Element of NAT st S3[j] holds
S3[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( S3[j] implies S3[j + 1] )
assume that
A24: S3[j] and
A25: n + 1 <= j + 1 ; ::_thesis: A . (n + 1) c= A . (j + 1)
now__::_thesis:_(_(_n_=_j_&_A_._(n_+_1)_c=_A_._(j_+_1)_)_or_(_n_<>_j_&_A_._(n_+_1)_c=_A_._(j_+_1)_)_)
percases ( n = j or n <> j ) ;
case n = j ; ::_thesis: A . (n + 1) c= A . (j + 1)
hence  A . (n + 1) c= A . (j + 1) ; ::_thesis: verum
end;
caseA26: n <> j ; ::_thesis: A . (n + 1) c= A . (j + 1)
 A . (j + 1) = (B . (j + 1)) \/ (A . j) by A17;
then A27: A . j c= A . (j + 1) by XBOOLE_1:7;
 n <= j by A25, XREAL_1:6;
then  n < j by A26, XXREAL_0:1;
hence  A . (n + 1) c= A . (j + 1) by A24, A27, NAT_1:13, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
hence  A . (n + 1) c= A . (j + 1) ; ::_thesis: verum
end;
A28: S3[ 0 ] by NAT_1:3;
A29: for j being Element of NAT holds S3[j] from NAT_1:sch_1(A28, A23);
 ( A . (n + 1) = (B . (n + 1)) \/ (A . n) & B . (n + 1) is finite Subset of X ) by A14, A17;
hence  S2[n + 1] by A19, A20, A29, XBOOLE_1:8; ::_thesis: verum
end;
 for j0 being Element of NAT st j0 = 0 holds
for j being Element of NAT st j0 <= j holds
A . j0 c= A . j
proof
let j0 be Element of NAT ; ::_thesis: ( j0 = 0 implies for j being Element of NAT st j0 <= j holds
A . j0 c= A . j )
assume A30: j0 = 0 ; ::_thesis: for j being Element of NAT st j0 <= j holds
A . j0 c= A . j
defpred S3[ Element of NAT ] means ( j0 <= $1 implies A . j0 c= A . $1 );
A31: now__::_thesis:_for_j_being_Element_of_NAT_st_S3[j]_holds_
S3[j_+_1]
let j be Element of NAT ; ::_thesis: ( S3[j] implies S3[j + 1] )
assume A32: S3[j] ; ::_thesis: S3[j + 1]
 A . (j + 1) = (B . (j + 1)) \/ (A . j) by A17;
then  A . j c= A . (j + 1) by XBOOLE_1:7;
hence  S3[j + 1] by A30, A32, NAT_1:2, XBOOLE_1:1; ::_thesis: verum
end;
A33: S3[ 0 ] by A30;
thus  for j being Element of NAT holds S3[j] from NAT_1:sch_1(A33, A31); ::_thesis: verum
end;
then A34: S2[ 0 ] by A14, A16;
A35: for i being Element of NAT holds S2[i] from NAT_1:sch_1(A34, A18);
 rng A c= bool Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng A or y in bool Y )
assume  y in rng A ; ::_thesis: y in bool Y
then consider x being set  such that
A36: x in dom A and
A37: y = A . x by FUNCT_1:def_3;
reconsider i = x as Element of NAT by A15, A36;
 A . i c= Y by A35;
hence  y in bool Y by A37, ZFMISC_1:def_1; ::_thesis: verum
end;
then  A is Function of NAT,(bool Y) by A15, FUNCT_2:2;
hence  ex A being Function of NAT,(bool Y) st
for i being Element of NAT holds
( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds
A . i c= A . j ) ) by A35; ::_thesis: verum
end;
then consider A being Function of NAT,(bool Y) such that
A38: for i being Element of NAT holds
( A . i is finite Subset of X & not A . i is empty & A . i c= Y & ( for Y1 being finite Subset of X st not Y1 is empty & Y1 c= Y & A . i misses Y1 holds
abs (setopfunc (Y1, the carrier of X,REAL,L,addreal)) < 1 / (i + 1) ) & ( for j being Element of NAT st i <= j holds
A . i c= A . j ) ) ;
defpred S2[ set , set ] means  ex Y1 being finite Subset of X st
( not Y1 is empty & A . $1 = Y1 & $2 = setopfunc (Y1, the carrier of X,REAL,L,addreal) );
A39: for x being set st x in NAT holds
ex y being set st
( y in REAL & S2[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in REAL & S2[x,y] ) )
assume  x in NAT ; ::_thesis: ex y being set st
( y in REAL & S2[x,y] )
then reconsider i = x as Element of NAT ;
 A . i is finite Subset of X by A38;
then reconsider Y1 = A . x as finite Subset of X ;
reconsider y = setopfunc (Y1, the carrier of X,REAL,L,addreal) as set ;
 not A . i is empty by A38;
then  ex Y1 being finite Subset of X st
( not Y1 is empty & A . x = Y1 & y = setopfunc (Y1, the carrier of X,REAL,L,addreal) ) ;
hence  ex y being set st
( y in REAL & S2[x,y] ) ; ::_thesis: verum
end;
 ex F being Function of NAT,REAL st
for x being set st x in NAT holds
S2[x,F . x] from FUNCT_2:sch_1(A39);
then consider F being Function of NAT,REAL such that
A40: for x being set st x in NAT holds
ex Y1 being finite Subset of X st
( not Y1 is empty & A . x = Y1 & F . x = setopfunc (Y1, the carrier of X,REAL,L,addreal) ) ;
set seq = F;
A41: for e being real number st e > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
abs ((F . n) - (F . m)) < e
proof
let e be real number ; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
abs ((F . n) - (F . m)) < e )
assume A42: e > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
abs ((F . n) - (F . m)) < e
A43: e / 2 > 0 / 2 by A42, XREAL_1:74;
then consider k being Element of NAT  such that
A44: 1 / (k + 1) < e / 2 by Lm2;
take  k ; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
abs ((F . n) - (F . m)) < e
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies abs ((F . n) - (F . m)) < e )
assume that
A45: n >= k and
A46: m >= k ; ::_thesis: abs ((F . n) - (F . m)) < e
consider Y2 being finite Subset of X such that
 not Y2 is empty and
A47: A . m = Y2 and
A48: F . m = setopfunc (Y2, the carrier of X,REAL,L,addreal) by A40;
consider Y0 being finite Subset of X such that
 not Y0 is empty and
A49: A . k = Y0 and
 F . k = setopfunc (Y0, the carrier of X,REAL,L,addreal) by A40;
A50: Y0 c= Y2 by A38, A46, A49, A47;
consider Y1 being finite Subset of X such that
 not Y1 is empty and
A51: A . n = Y1 and
A52: F . n = setopfunc (Y1, the carrier of X,REAL,L,addreal) by A40;
A53: Y0 c= Y1 by A38, A45, A49, A51;
now__::_thesis:_(_(_Y0_=_Y1_&_abs_((F_._n)_-_(F_._m))_<_e_)_or_(_Y0_<>_Y1_&_abs_((F_._n)_-_(F_._m))_<_e_)_)
percases ( Y0 = Y1 or Y0 <> Y1 ) ;
caseA54: Y0 = Y1 ; ::_thesis: abs ((F . n) - (F . m)) < e
now__::_thesis:_(_(_Y0_=_Y2_&_abs_((F_._n)_-_(F_._m))_<_e_)_or_(_Y0_<>_Y2_&_abs_((F_._n)_-_(F_._m))_<_e_)_)
percases ( Y0 = Y2 or Y0 <> Y2 ) ;
case Y0 = Y2 ; ::_thesis: abs ((F . n) - (F . m)) < e
hence  abs ((F . n) - (F . m)) < e by A42, A52, A48, A54, ABSVALUE:2; ::_thesis: verum
end;
caseA55: Y0 <> Y2 ; ::_thesis: abs ((F . n) - (F . m)) < e
 ex Y02 being finite Subset of X st
( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )
proof
take Y02 = Y2 \ Y0; ::_thesis: ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )
A56: Y2 \ Y0 c= Y2 by XBOOLE_1:36;
Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
.= Y2 by A50, XBOOLE_1:12 ;
hence  ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A47, A55, A56, XBOOLE_1:1, XBOOLE_1:79; ::_thesis: verum
end;
then consider Y02 being finite Subset of X such that
A57: ( not Y02 is empty & Y02 c= Y ) and
A58: Y02 misses Y0 and
A59: Y0 \/ Y02 = Y2 ;
 abs (setopfunc (Y02, the carrier of X,REAL,L,addreal)) < 1 / (k + 1) by A38, A49, A57, A58;
then A60: abs (setopfunc (Y02, the carrier of X,REAL,L,addreal)) < e / 2 by A44, XXREAL_0:2;
 dom L = the carrier of X by FUNCT_2:def_1;
then  setopfunc (Y2, the carrier of X,REAL,L,addreal) = addreal . ((setopfunc (Y0, the carrier of X,REAL,L,addreal)),(setopfunc (Y02, the carrier of X,REAL,L,addreal))) by A58, A59, BHSP_5:14
.= (setopfunc (Y0, the carrier of X,REAL,L,addreal)) + (setopfunc (Y02, the carrier of X,REAL,L,addreal)) by BINOP_2:def_9 ;
then A61: abs ((F . n) - (F . m)) = abs (- (setopfunc (Y02, the carrier of X,REAL,L,addreal))) by A52, A48, A54
.= abs (setopfunc (Y02, the carrier of X,REAL,L,addreal)) by COMPLEX1:52 ;
 e / 2 < e by A42, XREAL_1:216;
hence  abs ((F . n) - (F . m)) < e by A60, A61, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  abs ((F . n) - (F . m)) < e ; ::_thesis: verum
end;
caseA62: Y0 <> Y1 ; ::_thesis: abs ((F . n) - (F . m)) < e
now__::_thesis:_(_(_Y0_=_Y2_&_abs_((F_._n)_-_(F_._m))_<_e_)_or_(_Y0_<>_Y2_&_abs_((F_._n)_-_(F_._m))_<_e_)_)
percases ( Y0 = Y2 or Y0 <> Y2 ) ;
caseA63: Y0 = Y2 ; ::_thesis: abs ((F . n) - (F . m)) < e
 ex Y01 being finite Subset of X st
( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )
proof
take Y01 = Y1 \ Y0; ::_thesis: ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )
A64: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A53, XBOOLE_1:12 ;
hence  ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A51, A62, A64, XBOOLE_1:1, XBOOLE_1:79; ::_thesis: verum
end;
then consider Y01 being finite Subset of X such that
A65: ( not Y01 is empty & Y01 c= Y ) and
A66: Y01 misses Y0 and
A67: Y0 \/ Y01 = Y1 ;
 dom L = the carrier of X by FUNCT_2:def_1;
then A68: setopfunc (Y1, the carrier of X,REAL,L,addreal) = addreal . ((setopfunc (Y0, the carrier of X,REAL,L,addreal)),(setopfunc (Y01, the carrier of X,REAL,L,addreal))) by A66, A67, BHSP_5:14
.= (setopfunc (Y0, the carrier of X,REAL,L,addreal)) + (setopfunc (Y01, the carrier of X,REAL,L,addreal)) by BINOP_2:def_9 ;
 abs (setopfunc (Y01, the carrier of X,REAL,L,addreal)) < 1 / (k + 1) by A38, A49, A65, A66;
then  abs ((F . n) - (F . m)) < e / 2 by A44, A52, A48, A63, A68, XXREAL_0:2;
then  (abs ((F . n) - (F . m))) + 0 < (e / 2) + (e / 2) by A43, XREAL_1:8;
hence  abs ((F . n) - (F . m)) < e ; ::_thesis: verum
end;
caseA69: Y0 <> Y2 ; ::_thesis: abs ((F . n) - (F . m)) < e
 ex Y02 being finite Subset of X st
( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )
proof
take Y02 = Y2 \ Y0; ::_thesis: ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 )
A70: Y2 \ Y0 c= Y2 by XBOOLE_1:36;
Y0 \/ Y02 = Y0 \/ Y2 by XBOOLE_1:39
.= Y2 by A50, XBOOLE_1:12 ;
hence  ( not Y02 is empty & Y02 c= Y & Y02 misses Y0 & Y0 \/ Y02 = Y2 ) by A47, A69, A70, XBOOLE_1:1, XBOOLE_1:79; ::_thesis: verum
end;
then consider Y02 being finite Subset of X such that
A71: ( not Y02 is empty & Y02 c= Y ) and
A72: Y02 misses Y0 and
A73: Y0 \/ Y02 = Y2 ;
 dom L = the carrier of X by FUNCT_2:def_1;
then A74: setopfunc (Y2, the carrier of X,REAL,L,addreal) = addreal . ((setopfunc (Y0, the carrier of X,REAL,L,addreal)),(setopfunc (Y02, the carrier of X,REAL,L,addreal))) by A72, A73, BHSP_5:14
.= (setopfunc (Y0, the carrier of X,REAL,L,addreal)) + (setopfunc (Y02, the carrier of X,REAL,L,addreal)) by BINOP_2:def_9 ;
 ex Y01 being finite Subset of X st
( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )
proof
take Y01 = Y1 \ Y0; ::_thesis: ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 )
A75: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y01 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A53, XBOOLE_1:12 ;
hence  ( not Y01 is empty & Y01 c= Y & Y01 misses Y0 & Y0 \/ Y01 = Y1 ) by A51, A62, A75, XBOOLE_1:1, XBOOLE_1:79; ::_thesis: verum
end;
then consider Y01 being finite Subset of X such that
A76: ( not Y01 is empty & Y01 c= Y ) and
A77: Y01 misses Y0 and
A78: Y0 \/ Y01 = Y1 ;
 dom L = the carrier of X by FUNCT_2:def_1;
then  setopfunc (Y1, the carrier of X,REAL,L,addreal) = addreal . ((setopfunc (Y0, the carrier of X,REAL,L,addreal)),(setopfunc (Y01, the carrier of X,REAL,L,addreal))) by A77, A78, BHSP_5:14
.= (setopfunc (Y0, the carrier of X,REAL,L,addreal)) + (setopfunc (Y01, the carrier of X,REAL,L,addreal)) by BINOP_2:def_9 ;
then  (F . n) - (F . m) = (setopfunc (Y01, the carrier of X,REAL,L,addreal)) - (setopfunc (Y02, the carrier of X,REAL,L,addreal)) by A52, A48, A74;
then A79: abs ((F . n) - (F . m)) <= (abs (setopfunc (Y01, the carrier of X,REAL,L,addreal))) + (abs (setopfunc (Y02, the carrier of X,REAL,L,addreal))) by COMPLEX1:57;
 abs (setopfunc (Y02, the carrier of X,REAL,L,addreal)) < 1 / (k + 1) by A38, A49, A71, A72;
then A80: abs (setopfunc (Y02, the carrier of X,REAL,L,addreal)) < e / 2 by A44, XXREAL_0:2;
 abs (setopfunc (Y01, the carrier of X,REAL,L,addreal)) < 1 / (k + 1) by A38, A49, A76, A77;
then  abs (setopfunc (Y01, the carrier of X,REAL,L,addreal)) < e / 2 by A44, XXREAL_0:2;
then  (abs (setopfunc (Y01, the carrier of X,REAL,L,addreal))) + (abs (setopfunc (Y02, the carrier of X,REAL,L,addreal))) < (e / 2) + (e / 2) by A80, XREAL_1:8;
hence  abs ((F . n) - (F . m)) < e by A79, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  abs ((F . n) - (F . m)) < e ; ::_thesis: verum
end;
end;
end;
hence  abs ((F . n) - (F . m)) < e ; ::_thesis: verum
end;
 for e being real number st 0 < e holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((F . m) - (F . k)) < e
proof
let e be real number ; ::_thesis: ( 0 < e implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((F . m) - (F . k)) < e )
assume  0 < e ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((F . m) - (F . k)) < e
then consider k being Element of NAT  such that
A81: for n, m being Element of NAT st n >= k & m >= k holds
abs ((F . n) - (F . m)) < e by A41;
 for m being Element of NAT st k <= m holds
abs ((F . m) - (F . k)) < e by A81;
hence  ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((F . m) - (F . k)) < e ; ::_thesis: verum
end;
then  F is convergent by SEQ_4:41;
then consider x being real number  such that
A82: for r being real number st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
abs ((F . n) - x) < r by SEQ_2:def_6;
reconsider r = x as Real by XREAL_0:def_1;
take  r ; ::_thesis: for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) )
 for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) )
proof
let e be Real; ::_thesis: ( 0 < e implies ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) )
assume  e > 0 ; ::_thesis: ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) )
then A83: e / 2 > 0 / 2 by XREAL_1:74;
then consider m being Element of NAT  such that
A84: for n being Element of NAT st n >= m holds
abs ((F . n) - r) < e / 2 by A82;
consider i being Element of NAT  such that
A85: 1 / (i + 1) < e / 2 and
A86: i >= m by A83, Lm3;
consider Y0 being finite Subset of X such that
A87: not Y0 is empty and
A88: A . i = Y0 and
A89: F . i = setopfunc (Y0, the carrier of X,REAL,L,addreal) by A40;
A90: abs ((setopfunc (Y0, the carrier of X,REAL,L,addreal)) - r) < e / 2 by A84, A86, A89;
now__::_thesis:_for_Y1_being_finite_Subset_of_X_st_Y0_c=_Y1_&_Y1_c=_Y_holds_
abs_(r_-_(setopfunc_(Y1,_the_carrier_of_X,REAL,L,addreal)))_<_e
let Y1 be finite Subset of X; ::_thesis: ( Y0 c= Y1 & Y1 c= Y implies abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e )
assume that
A91: Y0 c= Y1 and
A92: Y1 c= Y ; ::_thesis: abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e
now__::_thesis:_(_(_Y0_=_Y1_&_abs_(r_-_(setopfunc_(Y1,_the_carrier_of_X,REAL,L,addreal)))_<_e_)_or_(_Y0_<>_Y1_&_abs_(r_-_(setopfunc_(Y1,_the_carrier_of_X,REAL,L,addreal)))_<_e_)_)
percases ( Y0 = Y1 or Y0 <> Y1 ) ;
case Y0 = Y1 ; ::_thesis: abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e
then  abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e / 2 by A90, UNIFORM1:11;
then  (abs (x - (setopfunc (Y1, the carrier of X,REAL,L,addreal)))) + 0 < (e / 2) + (e / 2) by A83, XREAL_1:8;
hence  abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ; ::_thesis: verum
end;
caseA93: Y0 <> Y1 ; ::_thesis: abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e
 ex Y2 being finite Subset of X st
( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 )
proof
take Y2 = Y1 \ Y0; ::_thesis: ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 )
A94: Y1 \ Y0 c= Y1 by XBOOLE_1:36;
Y0 \/ Y2 = Y0 \/ Y1 by XBOOLE_1:39
.= Y1 by A91, XBOOLE_1:12 ;
hence  ( not Y2 is empty & Y2 c= Y & Y0 misses Y2 & Y0 \/ Y2 = Y1 ) by A92, A93, A94, XBOOLE_1:1, XBOOLE_1:79; ::_thesis: verum
end;
then consider Y2 being finite Subset of X such that
A95: ( not Y2 is empty & Y2 c= Y ) and
A96: Y0 misses Y2 and
A97: Y0 \/ Y2 = Y1 ;
 dom L = the carrier of X by FUNCT_2:def_1;
then (setopfunc (Y1, the carrier of X,REAL,L,addreal)) - r = (addreal . ((setopfunc (Y0, the carrier of X,REAL,L,addreal)),(setopfunc (Y2, the carrier of X,REAL,L,addreal)))) - r by A96, A97, BHSP_5:14
.= ((setopfunc (Y0, the carrier of X,REAL,L,addreal)) + (setopfunc (Y2, the carrier of X,REAL,L,addreal))) - r by BINOP_2:def_9
.= ((setopfunc (Y0, the carrier of X,REAL,L,addreal)) - r) + (setopfunc (Y2, the carrier of X,REAL,L,addreal)) ;
then  abs ((setopfunc (Y1, the carrier of X,REAL,L,addreal)) - r) <= (abs ((setopfunc (Y0, the carrier of X,REAL,L,addreal)) - r)) + (abs (setopfunc (Y2, the carrier of X,REAL,L,addreal))) by ABSVALUE:9;
then A98: abs (x - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) <= (abs ((setopfunc (Y0, the carrier of X,REAL,L,addreal)) - r)) + (abs (setopfunc (Y2, the carrier of X,REAL,L,addreal))) by UNIFORM1:11;
 abs (setopfunc (Y2, the carrier of X,REAL,L,addreal)) < 1 / (i + 1) by A38, A88, A95, A96;
then  abs (setopfunc (Y2, the carrier of X,REAL,L,addreal)) < e / 2 by A85, XXREAL_0:2;
then  (abs ((setopfunc (Y0, the carrier of X,REAL,L,addreal)) - r)) + (abs (setopfunc (Y2, the carrier of X,REAL,L,addreal))) < (e / 2) + (e / 2) by A90, XREAL_1:8;
hence  abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e by A98, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ; ::_thesis: verum
end;
hence  ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) by A87, A88; ::_thesis: verum
end;
hence  for e being Real st 0 < e holds
ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds
abs (r - (setopfunc (Y1, the carrier of X,REAL,L,addreal))) < e ) ) ; ::_thesis: verum
end;
hence  Y is_summable_set_by L by BHSP_6:def_6; ::_thesis: verum
end;

theorem Th2: :: BHSP_7:2
for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & 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 & ( 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 & ( 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)
proof
let X be RealUnitarySpace; ::_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 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 & ( 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 & ( 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) )
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 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 & ( 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 & ( 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)
let S be finite OrthogonalFamily of X; ::_thesis: ( not S is empty implies for I being Function of the carrier of X, the carrier of X st S c= dom I & ( 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 & ( 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) )
assume A2: not S is empty ; ::_thesis: for I being Function of the carrier of X, the carrier of X st S c= dom I & ( 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 & ( 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)
let I be Function of the carrier of X, the carrier of X; ::_thesis: ( S c= dom I & ( for y being Point of X st y in S holds
I . y = y ) implies for H being Function of the carrier of X,REAL st S c= dom H & ( 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) )
assume that
A3: S c= dom I and
A4: for y being Point of X st y in S holds
I . y = y ; ::_thesis: for H being Function of the carrier of X,REAL st S c= dom H & ( 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)
consider p being FinSequence of the carrier of X such that
A5: ( p is one-to-one & rng p = S ) and
A6: setopfunc (S, the carrier of X, the carrier of X,I, the addF of X) = the addF of X "**" (Func_Seq (I,p)) by A1, A3, BHSP_5:def_5;
let H be Function of the carrier of X,REAL; ::_thesis: ( S c= dom H & ( for y being Point of X st y in S holds
H . y = y .|. y ) implies (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) )
assume that
A7: S c= dom H and
A8: for y being Point of X st y in S holds
H . y = y .|. y ; ::_thesis: (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)
A9: setopfunc (S, the carrier of X,REAL,H,addreal) = addreal "**" (Func_Seq (H,p)) by A7, A5, BHSP_5:def_5;
A10: for y1, y2 being Point of X st y1 in S & y2 in S & y1 <> y2 holds
the scalar of X . [(I . y1),(I . y2)] = 0
proof
let y1, y2 be Point of X; ::_thesis: ( y1 in S & y2 in S & y1 <> y2 implies the scalar of X . [(I . y1),(I . y2)] = 0 )
assume that
A11: ( y1 in S & y2 in S ) and
A12: y1 <> y2 ; ::_thesis: the scalar of X . [(I . y1),(I . y2)] = 0
A13: y1 .|. y2 = 0 by A11, A12, BHSP_5:def_8;
 ( I . y1 = y1 & I . y2 = y2 ) by A4, A11;
hence  the scalar of X . [(I . y1),(I . y2)] = 0 by A13, BHSP_1:def_1; ::_thesis: verum
end;
 for y being Point of X st y in S holds
H . y = the scalar of X . [(I . y),(I . y)]
proof
let y be Point of X; ::_thesis: ( y in S implies H . y = the scalar of X . [(I . y),(I . y)] )
assume A14: y in S ; ::_thesis: H . y = the scalar of X . [(I . y),(I . y)]
then A15: I . y = y by A4;
H . y = y .|. y by A8, A14
.= the scalar of X . [(I . y),(I . y)] by A15, BHSP_1:def_1 ;
hence  H . y = the scalar of X . [(I . y),(I . y)] ; ::_thesis: verum
end;
then  the scalar of X . [( the addF of X "**" (Func_Seq (I,p))),( the addF of X "**" (Func_Seq (I,p)))] = addreal "**" (Func_Seq (H,p)) by A2, A3, A7, A5, A10, BHSP_5:9;
hence  (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) by A6, A9, BHSP_1:def_1; ::_thesis: verum
end;

theorem Th3: :: BHSP_7:3
for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & 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 & ( 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)
proof
let X be RealUnitarySpace; ::_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 finite OrthogonalFamily of X st not S is empty holds
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
(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal) )
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 finite OrthogonalFamily of X st not S is empty holds
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
(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal)
reconsider I = id the carrier of X as Function of the carrier of X, the carrier of X ;
let S be finite OrthogonalFamily of X; ::_thesis: ( not S is empty implies 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
(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal) )
assume A2: not S is empty ; ::_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
(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal)
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 (setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal) )
assume A3: ( S c= dom H & ( for x being Point of X st x in S holds
H . x = x .|. x ) ) ; ::_thesis: (setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal)
A4: for x being Point of X st x in S holds
I . x = x by FUNCT_1:18;
A5: dom I = the carrier of X by FUNCT_2:def_1;
 for x being set st x in the carrier of X holds
I . x = x by FUNCT_1:18;
then  setsum S = setopfunc (S, the carrier of X, the carrier of X,I, the addF of X) by A1, A5, BHSP_6:1;
hence  (setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal) by A1, A2, A3, A5, A4, Th2; ::_thesis: verum
end;

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
proof
let X be RealUnitarySpace; ::_thesis: for Y being OrthogonalFamily of X
for Z being Subset of X st Z is Subset of Y holds
Z is OrthogonalFamily of X
let Y be OrthogonalFamily of X; ::_thesis: for Z being Subset of X st Z is Subset of Y holds
Z is OrthogonalFamily of X
let Z be Subset of X; ::_thesis: ( Z is Subset of Y implies Z is OrthogonalFamily of X )
assume  Z is Subset of Y ; ::_thesis: Z is OrthogonalFamily of X
then  for x, y being Point of X st x in Z & y in Z & x <> y holds
x .|. y = 0 by BHSP_5:def_8;
hence  Z is OrthogonalFamily of X by BHSP_5:def_8; ::_thesis: verum
end;

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
proof
let X be RealUnitarySpace; ::_thesis: for Y being OrthonormalFamily of X
for Z being Subset of X st Z is Subset of Y holds
Z is OrthonormalFamily of X
let Y be OrthonormalFamily of X; ::_thesis: for Z being Subset of X st Z is Subset of Y holds
Z is OrthonormalFamily of X
let Z be Subset of X; ::_thesis: ( Z is Subset of Y implies Z is OrthonormalFamily of X )
assume A1: Z is Subset of Y ; ::_thesis: Z is OrthonormalFamily of X
then A2: for x being Point of X st x in Z holds
x .|. x = 1 by BHSP_5:def_9;
 Y is OrthogonalFamily of X by BHSP_5:def_9;
then  Z is OrthogonalFamily of X by A1, Th4;
hence  Z is OrthonormalFamily of X by A2, BHSP_5:def_9; ::_thesis: verum
end;

begin

theorem Th6: :: BHSP_7:6
for X being RealHilbertSpace st the addF of X is commutative & the addF of X is associative & 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 & ( 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 )
proof
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 )
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
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_
abs_(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
abs (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
abs (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 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
abs (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
abs (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 abs (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: abs (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  abs (setopfunc (Y1, the carrier of X,REAL,H,addreal)) < e by A17, A18, ABSVALUE:def_1; ::_thesis: verum
end;
hence  S is_summable_set_by H by Th1; ::_thesis: verum
end;
now__::_thesis:_(_S_is_summable_set_by_H_implies_S_is_summable_set_)
assume A19: S is_summable_set_by H ; ::_thesis: S is summable_set
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_)_)
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
abs (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
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;
 abs (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) < (abs (setopfunc (Y1, the carrier of X,REAL,H,addreal))) - (abs (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;
hence  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 ) ) by A21; ::_thesis: verum
end;
hence  S is summable_set by A1, BHSP_6:10; ::_thesis: verum
end;
hence  ( S is summable_set iff S is_summable_set_by H ) by A4; ::_thesis: verum
end;

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 & Y0 c= S & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) )
proof
let X be RealUnitarySpace; ::_thesis: 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 & Y0 c= S & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) )
let S be Subset of X; ::_thesis: ( S is summable_set implies 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 Y0 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) ) )
assume A1: S is summable_set ; ::_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 Y0 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) )
consider Y02 being finite Subset of X such that
 not Y02 is empty and
A2: Y02 c= S and
A3: for Y1 being finite Subset of X st Y02 c= Y1 & Y1 c= S holds
||.((sum S) - (setsum Y1)).|| < 1 by A1, BHSP_6:def_3;
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 Y0 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) ) )
assume A4: 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 Y0 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) )
set e9 = e / ((2 * ||.(sum S).||) + 1);
 0 <= ||.(sum S).|| by BHSP_1:28;
then  0 <= 2 * ||.(sum S).|| by XREAL_1:127;
then A5: 0 + 0 < (2 * ||.(sum S).||) + 1 by XREAL_1:8;
then  0 < e / ((2 * ||.(sum S).||) + 1) by A4, XREAL_1:139;
then consider Y01 being finite Subset of X such that
A6: not Y01 is empty and
A7: Y01 c= S and
A8: for Y1 being finite Subset of X st Y01 c= Y1 & Y1 c= S holds
||.((sum S) - (setsum Y1)).|| < e / ((2 * ||.(sum S).||) + 1) by A1, BHSP_6:def_3;
set Y0 = Y01 \/ Y02;
A9: for Y1 being finite Subset of X st Y01 \/ Y02 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e
proof
let Y1 be finite Subset of X; ::_thesis: ( Y01 \/ Y02 c= Y1 & Y1 c= S implies abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e )
assume that
A10: Y01 \/ Y02 c= Y1 and
A11: Y1 c= S ; ::_thesis: abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e
set SS = (sum S) - (setsum Y1);
set SY = setsum Y1;
 Y01 c= Y1 by A10, XBOOLE_1:11;
then A12: ||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1) < (e / ((2 * ||.(sum S).||) + 1)) * ((2 * ||.(sum S).||) + 1) by A5, A8, A11, XREAL_1:68;
||.(setsum Y1).|| = ||.(- (setsum Y1)).|| by BHSP_1:31
.= ||.((0. X) - (setsum Y1)).|| by RLVECT_1:14
.= ||.(((- (sum S)) + (sum S)) - (setsum Y1)).|| by RLVECT_1:5
.= ||.((- (sum S)) + ((sum S) - (setsum Y1))).|| by RLVECT_1:def_3 ;
then  ||.(setsum Y1).|| <= ||.(- (sum S)).|| + ||.((sum S) - (setsum Y1)).|| by BHSP_1:30;
then A13: ||.(setsum Y1).|| <= ||.(sum S).|| + ||.((sum S) - (setsum Y1)).|| by BHSP_1:31;
 Y02 c= Y1 by A10, XBOOLE_1:11;
then  ||.((sum S) - (setsum Y1)).|| + ||.(setsum Y1).|| < 1 + (||.(sum S).|| + ||.((sum S) - (setsum Y1)).||) by A3, A11, A13, XREAL_1:8;
then  (||.(setsum Y1).|| + ||.((sum S) - (setsum Y1)).||) - ||.((sum S) - (setsum Y1)).|| < ((1 + ||.(sum S).||) + ||.((sum S) - (setsum Y1)).||) - ||.((sum S) - (setsum Y1)).|| by XREAL_1:14;
then A14: ||.(sum S).|| + ||.(setsum Y1).|| < (1 + ||.(sum S).||) + ||.(sum S).|| by XREAL_1:8;
 0 <= ||.((sum S) - (setsum Y1)).|| by BHSP_1:28;
then  ||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||) <= ||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1) by A14, XREAL_1:64;
then  (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||)) + (||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1)) < ((e / ((2 * ||.(sum S).||) + 1)) * ((2 * ||.(sum S).||) + 1)) + (||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1)) by A12, XREAL_1:8;
then  ((||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||)) + (||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1))) - (||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1)) < (((e / ((2 * ||.(sum S).||) + 1)) * ((2 * ||.(sum S).||) + 1)) + (||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1))) - (||.((sum S) - (setsum Y1)).|| * ((2 * ||.(sum S).||) + 1)) by XREAL_1:14;
then A15: ||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||) < e by A5, XCMPLX_1:87;
set F = (sum S) .|. (sum S);
set G = (setsum Y1) .|. (setsum Y1);
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) = abs ((((sum S) .|. (sum S)) - ((sum S) .|. (setsum Y1))) + (((sum S) .|. (setsum Y1)) - ((setsum Y1) .|. (setsum Y1))))
.= abs (((sum S) .|. ((sum S) - (setsum Y1))) + (((sum S) .|. (setsum Y1)) - ((setsum Y1) .|. (setsum Y1)))) by BHSP_1:12
.= abs (((sum S) .|. ((sum S) - (setsum Y1))) + (((sum S) - (setsum Y1)) .|. (setsum Y1))) by BHSP_1:11 ;
then A16: abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) <= (abs ((sum S) .|. ((sum S) - (setsum Y1)))) + (abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) by COMPLEX1:56;
 abs ((sum S) .|. ((sum S) - (setsum Y1))) <= ||.(sum S).|| * ||.((sum S) - (setsum Y1)).|| by BHSP_1:29;
then  (abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1)))) + (abs ((sum S) .|. ((sum S) - (setsum Y1)))) <= ((abs ((sum S) .|. ((sum S) - (setsum Y1)))) + (abs (((sum S) - (setsum Y1)) .|. (setsum Y1)))) + (||.(sum S).|| * ||.((sum S) - (setsum Y1)).||) by A16, XREAL_1:7;
then  (abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1)))) + (abs ((sum S) .|. ((sum S) - (setsum Y1)))) <= ((abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) + (||.(sum S).|| * ||.((sum S) - (setsum Y1)).||)) + (abs ((sum S) .|. ((sum S) - (setsum Y1)))) ;
then A17: abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) <= (abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) + (||.(sum S).|| * ||.((sum S) - (setsum Y1)).||) by XREAL_1:6;
 abs (((sum S) - (setsum Y1)) .|. (setsum Y1)) <= ||.((sum S) - (setsum Y1)).|| * ||.(setsum Y1).|| by BHSP_1:29;
then  (abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1)))) + (abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) <= ((abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) + (||.(sum S).|| * ||.((sum S) - (setsum Y1)).||)) + (||.((sum S) - (setsum Y1)).|| * ||.(setsum Y1).||) by A17, XREAL_1:7;
then  (abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1)))) + (abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) <= ((||.(sum S).|| * ||.((sum S) - (setsum Y1)).||) + (||.((sum S) - (setsum Y1)).|| * ||.(setsum Y1).||)) + (abs (((sum S) - (setsum Y1)) .|. (setsum Y1))) ;
then  abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) <= (||.((sum S) - (setsum Y1)).|| * ||.(sum S).||) + (||.((sum S) - (setsum Y1)).|| * ||.(setsum Y1).||) by XREAL_1:6;
then  (abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1)))) + (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||)) < e + (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||)) by A15, XREAL_1:8;
then  ((abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1)))) + (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||))) - (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||)) < (e + (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||))) - (||.((sum S) - (setsum Y1)).|| * (||.(sum S).|| + ||.(setsum Y1).||)) by XREAL_1:14;
hence  abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ; ::_thesis: verum
end;
 Y01 \/ Y02 c= S by A7, A2, XBOOLE_1:8;
hence  ex Y0 being finite Subset of X st
( not Y0 is empty & Y0 c= S & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= S holds
abs (((sum S) .|. (sum S)) - ((setsum Y1) .|. (setsum Y1))) < e ) ) by A6, A9; ::_thesis: verum
end;

Lm4:  for p1, p2 being real number st ( for e being Real st 0 < e holds
abs (p1 - p2) < e ) holds
p1 = p2
proof
let p1, p2 be real number ; ::_thesis: ( ( for e being Real st 0 < e holds
abs (p1 - p2) < e ) implies p1 = p2 )
assume A1: for e being Real st 0 < e holds
abs (p1 - p2) < e ; ::_thesis: p1 = p2
assume  p1 <> p2 ; ::_thesis: contradiction
then  p1 - p2 <> 0 ;
then  0 < abs (p1 - p2) by COMPLEX1:47;
hence  contradiction by A1; ::_thesis: verum
end;

theorem :: BHSP_7:8
for X being RealHilbertSpace st the addF of X is commutative & the addF of X is associative & 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 & ( 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)
proof
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
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 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
abs ((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
abs (((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 & abs (((sum S) .|. (sum S)) - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal))) < e / 2 ) by A15, A16, 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 A12, A16, XREAL_1:8;
then A17: (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: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  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:56;
hence  abs (((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
end;