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