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, 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 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