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 x being Point of X
for S being finite OrthonormalFamily of X st not S is empty 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 = (x .|. y) ^2 ) holds
for F being Function of the carrier of X,the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) = setopfunc S,the carrier of X,REAL ,H,addreal )
assume that
A1: ( the addF of X is commutative & the addF of X is associative ) and
A2: the addF of X is having_a_unity ; :: thesis: for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty 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 = (x .|. y) ^2 ) holds
for F being Function of the carrier of X,the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) = setopfunc S,the carrier of X,REAL ,H,addreal
let x be Point of X; :: thesis: for S being finite OrthonormalFamily of X st not S is empty 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 = (x .|. y) ^2 ) holds
for F being Function of the carrier of X,the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) = setopfunc S,the carrier of X,REAL ,H,addreal
let S be finite OrthonormalFamily of X; :: thesis: ( not S is empty 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 = (x .|. y) ^2 ) holds
for F being Function of the carrier of X,the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) = setopfunc S,the carrier of X,REAL ,H,addreal )
assume A3: not S is empty ; :: 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 = (x .|. y) ^2 ) holds
for F being Function of the carrier of X,the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) = setopfunc S,the carrier of X,REAL ,H,addreal
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 = (x .|. y) ^2 ) implies for F being Function of the carrier of X,the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) = setopfunc S,the carrier of X,REAL ,H,addreal )
assume that
A4: S c= dom H and
A5: for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ; :: thesis: for F being Function of the carrier of X,the carrier of X st S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) holds
x .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) = setopfunc S,the carrier of X,REAL ,H,addreal
let F be Function of the carrier of X,the carrier of X; :: thesis: ( S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) implies x .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) = setopfunc S,the carrier of X,REAL ,H,addreal )
assume that
A6: S c= dom F and
A7: for y being Point of X st y in S holds
F . y = (x .|. y) * y ; :: thesis: x .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) = setopfunc S,the carrier of X,REAL ,H,addreal
consider p being FinSequence of the carrier of X such that
A8: p is one-to-one and
A9: rng p = S and
A10: setopfunc S,the carrier of X,the carrier of X,F,the addF of X = the addF of X "**" (Func_Seq F,p) by A1, A2, A6, Def5;
A11: for y being Point of X st y in S holds
H . y = the scalar of X . [x,(F . y)]

proof

let y be Point of X; :: thesis: ( y in S implies H . y = the scalar of X . [x,(F . y)] )
assume A12: y in S ; :: thesis: H . y = the scalar of X . [x,(F . y)]
set a = x .|. y;
H . y = (x .|. y) ^2 by A5, A12
.= x .|. ((x .|. y) * y) by BHSP_1:8
.= the scalar of X . [x,((x .|. y) * y)] by BHSP_1:def 1
.= the scalar of X . [x,(F . y)] by A7, A12 ;
hence H . y = the scalar of X . [x,(F . y)] ; :: thesis: verum

end;

A13: setopfunc S,the carrier of X,REAL ,H,addreal = addreal "**" (Func_Seq H,p) by A4, A8, A9, Def5;
x .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) = the scalar of X . [x,(the addF of X "**" (Func_Seq F,p))] by A10, BHSP_1:def 1;
hence x .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) = setopfunc S,the carrier of X,REAL ,H,addreal by A3, A4, A6, A8, A9, A11, A13, Th10; :: thesis: verum