begin
begin
begin
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)
theorem Th12:
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)
theorem
for
DK,
DX being non
empty set for
f being
BinOp of
DK st
f is
commutative &
f is
associative &
f is
having_a_unity holds
for
Y1,
Y2 being
finite Subset of
DX st
Y1 misses Y2 holds
for
F being
Function of
DX,
DK st
Y1 c= dom F &
Y2 c= dom F holds
for
Z being
finite Subset of
DX st
Z = Y1 \/ Y2 holds
setopfunc (
Z,
DX,
DK,
F,
f)
= f . (
(setopfunc (Y1,DX,DK,F,f)),
(setopfunc (Y2,DX,DK,F,f)))