theorem Th3: :: BHSP_7:3

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 S being finite OrthogonalFamily of X st not S is empty holds
for H being Functional of X st S c= dom H & ( for x being Point of X st x in S holds
H . x = x .|. x ) holds
(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal)