theorem Th2:
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
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)