for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
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)