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 A3: ( S c= dom I & ( 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
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 A4: ( S c= dom H & ( 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
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,I,the addF of X = the addF of X "**" (Func_Seq I,p) ) by A1, A3, BHSP_5:def 5;
A6: setopfunc S,the carrier of X,REAL ,H,addreal = addreal "**" (Func_Seq H,p) by A4, A5, BHSP_5:def 5;
A7: 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 A8: ( y1 in S & y2 in S & y1 <> y2 ) ; :: thesis: the scalar of X . [(I . y1),(I . y2)] = 0
then A9: ( I . y1 = y1 & I . y2 = y2 ) by A3;
y1 .|. y2 = 0 by A8, BHSP_5:def 8;
hence the scalar of X . [(I . y1),(I . y2)] = 0 by A9, 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 A10: y in S ; :: thesis: H . y = the scalar of X . [(I . y),(I . y)]
then A11: I . y = y by A3;
H . y = y .|. y by A4, A10
.= the scalar of X . [(I . y),(I . y)] by A11, 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, A4, A5, A7, 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 A5, A6, BHSP_1:def 1; :: thesis: verum