let X be RealUnitarySpace; ( 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 )
; 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; ( 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
; 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; ( 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
; 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; ( 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
; (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
for y being Point of X st y in S holds
H . y = the scalar of X . [(I . y),(I . y)]
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; verum