environ
vocabularies HIDDEN, NUMBERS, BHSP_1, PRE_TOPC, SUBSET_1, FINSEQ_1, FUNCT_1, RELAT_1, FUNCT_2, CARD_1, TARSKI, XBOOLE_0, BINOP_1, SETWISEO, FINSET_1, MEMBER_1, FINSOP_1, ALGSTR_0, SUPINF_2, NAT_1, DECOMP_1, REAL_1, STRUCT_0, BINOP_2, PROB_2, NORMSP_1, ARYTM_3, SQUARE_1, ARYTM_1, XXREAL_0, RVSUM_1, RLVECT_1, ORDINAL4, BHSP_5;
notations HIDDEN, TARSKI, SUBSET_1, XBOOLE_0, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, STRUCT_0, ALGSTR_0, REAL_1, XREAL_0, FUNCT_2, FINSET_1, NAT_1, RELAT_1, BINOP_2, PRE_TOPC, RLVECT_1, BHSP_1, SQUARE_1, BINOP_1, SETWISEO, FUNCT_1, FINSEQ_1, FINSOP_1;
definitions TARSKI;
theorems XBOOLE_0, SUBSET_1, BHSP_1, SQUARE_1, TARSKI, INT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCT_1, NAT_1, FUNCT_2, FINSOP_1, HILBASIS, XBOOLE_1, BINOP_2, XREAL_1, XXREAL_0, RELAT_1, XREAL_0, ORDINAL1;
schemes NAT_1, FINSEQ_1, FUNCT_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, BINOP_2, MEMBERED, STRUCT_0, CARD_1, XREAL_0, SQUARE_1, NAT_1, INT_1;
constructors HIDDEN, BINOP_1, DOMAIN_1, SETWISEO, REAL_1, SQUARE_1, NAT_1, BINOP_2, MEMBERED, FINSOP_1, BHSP_1, RELSET_1, INT_1;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities SQUARE_1, BINOP_1, RLVECT_1, ALGSTR_0;
expansions TARSKI;
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)))