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 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
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
(setopfunc S,the carrier of X,the carrier of X,F,the addF of 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 A1: ( the addF of X is commutative & the addF of X is associative & 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 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
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
(setopfunc S,the carrier of X,the carrier of X,F,the addF of 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 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
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
(setopfunc S,the carrier of X,the carrier of X,F,the addF of 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 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
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
(setopfunc S,the carrier of X,the carrier of X,F,the addF of 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 A2: not S is empty ; :: 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
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
(setopfunc S,the carrier of X,the carrier of X,F,the addF of 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 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
(setopfunc S,the carrier of X,the carrier of X,F,the addF of 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: ( S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. 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 = (x .|. y) ^2 ) holds
(setopfunc S,the carrier of X,the carrier of X,F,the addF of 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 (setopfunc S,the carrier of X,the carrier of X,F,the addF of 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 A4: ( S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) ) ; :: thesis: (setopfunc S,the carrier of X,the carrier of X,F,the addF of 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
A5: ( p is one-to-one & rng p = S & 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, A3, Def5;
A6: for y1, y2 being Point of X st y1 in S & y2 in S & y1 <> y2 holds
the scalar of X . [(F . y1),(F . y2)] = 0

proof

let y1, y2 be Point of X; :: thesis: ( y1 in S & y2 in S & y1 <> y2 implies the scalar of X . [(F . y1),(F . y2)] = 0 )
assume A7: ( y1 in S & y2 in S & y1 <> y2 ) ; :: thesis: the scalar of X . [(F . y1),(F . y2)] = 0
set z1 = x .|. y1;
set z2 = x .|. y2;
S is OrthogonalFamily of X by Def9;
then A8: y1 .|. y2 = 0 by A7, Def8;
the scalar of X . [(F . y1),(F . y2)] = the scalar of X . [((x .|. y1) * y1),(F . y2)] by A3, A7
.= the scalar of X . [((x .|. y1) * y1),((x .|. y2) * y2)] by A3, A7
.= ((x .|. y1) * y1) .|. ((x .|. y2) * y2) by BHSP_1:def 1
.= (x .|. y2) * (y2 .|. ((x .|. y1) * y1)) by BHSP_1:8
.= (x .|. y2) * ((x .|. y1) * (y2 .|. y1)) by BHSP_1:8
.= 0 by A8 ;
hence the scalar of X . [(F . y1),(F . y2)] = 0 ; :: thesis: verum

end;

A9: for y being Point of X st y in S holds
H . y = the scalar of X . [(F . y),(F . y)]

proof

let y be Point of X; :: thesis: ( y in S implies H . y = the scalar of X . [(F . y),(F . y)] )
assume A10: y in S ; :: thesis: H . y = the scalar of X . [(F . y),(F . y)]
then A11: F . y = (x .|. y) * y by A3;
H . y = (x .|. y) ^2 by A4, A10
.= ((x .|. y) * (x .|. y)) * 1
.= ((x .|. y) * (x .|. y)) * (y .|. y) by A10, Def9
.= (x .|. y) * ((x .|. y) * (y .|. y))
.= (x .|. y) * (((x .|. y) * y) .|. y) by BHSP_1:8
.= ((x .|. y) * y) .|. ((x .|. y) * y) by BHSP_1:8
.= the scalar of X . [(F . y),(F . y)] by A11, BHSP_1:def 1 ;
hence H . y = the scalar of X . [(F . y),(F . y)] ; :: thesis: verum

end;

(setopfunc S,the carrier of X,the carrier of X,F,the addF of X) .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) = the scalar of X . [(the addF of X "**" (Func_Seq F,p)),(the addF of X "**" (Func_Seq F,p))] by A5, BHSP_1:def 1
.= addreal "**" (Func_Seq H,p) by A2, A3, A4, A5, A6, A9, Th9
.= setopfunc S,the carrier of X,REAL ,H,addreal by A4, A5, Def5 ;
hence (setopfunc S,the carrier of X,the carrier of X,F,the addF of 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 ; :: thesis: verum