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