:: BHSP_7 semantic presentation

REAL is non empty non trivial non finite set

COMPLEX is non empty non trivial non finite set
RAT is non empty non trivial non finite set
INT is non empty non trivial non finite set

K118(NAT) is V27() set

p1 is V36() real ext-real Element of REAL
p1 / 2 is V36() real ext-real Element of REAL
X is V36() real ext-real Element of REAL
S is V36() real ext-real Element of REAL
X - S is V36() real ext-real Element of REAL
abs (X - S) is V36() real ext-real Element of REAL
H is V36() real ext-real Element of REAL
S - H is V36() real ext-real Element of REAL
abs (S - H) is V36() real ext-real Element of REAL
X - H is V36() real ext-real Element of REAL
abs (X - H) is V36() real ext-real Element of REAL
(X - S) + (S - H) is V36() real ext-real Element of REAL
abs ((X - S) + (S - H)) is V36() real ext-real Element of REAL
(abs (X - S)) + (abs (S - H)) is V36() real ext-real Element of REAL
(p1 / 2) + (p1 / 2) is V36() real ext-real Element of REAL
X is V36() real ext-real set
X " is V36() real ext-real Element of REAL

1 / (S + 1) is V36() real ext-real Element of REAL
(X ") + 0 is V36() real ext-real Element of REAL
1 / (X ") is V36() real ext-real Element of REAL
X is V36() real ext-real set

X " is V36() real ext-real Element of REAL

1 / (p1 + 1) is V36() real ext-real Element of REAL
(X ") + 0 is V36() real ext-real Element of REAL
1 / (X ") is V36() real ext-real Element of REAL
X is non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
bool the carrier of X is set
[: the carrier of X,REAL:] is set
bool [: the carrier of X,REAL:] is set
S is Element of bool the carrier of X
H is Relation-like the carrier of X -defined REAL -valued Function-like non empty V14( the carrier of X) V18( the carrier of X, REAL ) Element of bool [: the carrier of X,REAL:]
p1 is V36() real ext-real Element of REAL
p2 is V36() real ext-real Element of REAL
p2 / 2 is V36() real ext-real Element of REAL
e is finite Element of bool the carrier of X
Y02 is finite Element of bool the carrier of X
setopfunc (Y02, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
abs (setopfunc (Y02, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
e \/ Y02 is finite Element of bool the carrier of X
dom H is set
setopfunc ((e \/ Y02), the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
setopfunc (e, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
addreal . ((setopfunc (e, the carrier of X,REAL,H,addreal)),(setopfunc (Y02, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(setopfunc (e, the carrier of X,REAL,H,addreal)) + (setopfunc (Y02, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
(setopfunc ((e \/ Y02), the carrier of X,REAL,H,addreal)) - (setopfunc (e, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
p1 - (setopfunc ((e \/ Y02), the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs (p1 - (setopfunc ((e \/ Y02), the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(setopfunc ((e \/ Y02), the carrier of X,REAL,H,addreal)) - p1 is V36() real ext-real Element of REAL
abs ((setopfunc ((e \/ Y02), the carrier of X,REAL,H,addreal)) - p1) is V36() real ext-real Element of REAL
p1 - (setopfunc (e, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs (p1 - (setopfunc (e, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
p2 is V36() real ext-real Element of REAL
p1 is set

1 / (p2 + 1) is V36() real ext-real Element of REAL
0 / (p2 + 1) is V36() real ext-real Element of REAL
e is V36() real ext-real Element of REAL
Y02 is finite Element of bool the carrier of X
bool S is set
Y01 is V36() real ext-real Element of REAL
Y1 is finite Element of bool the carrier of X
Y01 + 1 is V36() real ext-real Element of REAL
1 / (Y01 + 1) is V36() real ext-real Element of REAL
setopfunc (Y1, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
abs (setopfunc (Y1, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
p1 is set
[:NAT,(bool S):] is set
bool [:NAT,(bool S):] is set

p1 . 0 is Element of bool S

dom p2 is set
p2 . 0 is set

dom p2 is set
p2 . 0 is set

p2 . e is set

1 / (e + 1) is V36() real ext-real Element of REAL
p2 . (e + 1) is set

1 / ((e + 1) + 1) is V36() real ext-real Element of REAL
Y02 is finite Element of bool the carrier of X
setopfunc (Y02, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
abs (setopfunc (Y02, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
p1 . (e + 1) is Element of bool S
(p1 . (e + 1)) \/ (p2 . e) is set

p2 . Y02 is set

p2 . (Y02 + 1) is set
p1 . (Y02 + 1) is Element of bool S
(p1 . (Y02 + 1)) \/ (p2 . Y02) is set
p1 . (e + 1) is Element of bool S
(p1 . (e + 1)) \/ (p2 . e) is set
Y02 is finite Element of bool the carrier of X
setopfunc (Y02, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
abs (setopfunc (Y02, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL

p2 . Y01 is set

p2 . e is set

p2 . Y02 is set

p2 . (Y02 + 1) is set
p1 . (Y02 + 1) is Element of bool S
(p1 . (Y02 + 1)) \/ (p2 . Y02) is set

1 / (0 + 1) is V36() real ext-real Element of REAL
e is finite Element of bool the carrier of X
setopfunc (e, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
abs (setopfunc (e, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL

p2 . Y02 is set
rng p2 is set
e is set
Y02 is set
p2 . Y02 is set

p2 . Y01 is set

p2 is set
p1 . p2 is set

p1 . e is Element of bool S
Y02 is finite Element of bool the carrier of X
setopfunc (Y02, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
Y01 is set
Y1 is finite Element of bool the carrier of X
setopfunc (Y1, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL

Y02 is V36() real ext-real set
Y02 / 2 is V36() real ext-real Element of REAL
0 / 2 is V36() real ext-real Element of REAL

1 / (Y01 + 1) is V36() real ext-real Element of REAL

p2 . Y1 is V36() real ext-real Element of REAL
p2 . Y011 is V36() real ext-real Element of REAL
(p2 . Y1) - (p2 . Y011) is V36() real ext-real Element of REAL
abs ((p2 . Y1) - (p2 . Y011)) is V36() real ext-real Element of REAL
p1 . Y011 is Element of bool S
r is finite Element of bool the carrier of X
setopfunc (r, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
p1 . Y01 is Element of bool S
p2 . Y01 is V36() real ext-real Element of REAL
G is finite Element of bool the carrier of X
setopfunc (G, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
p1 . Y1 is Element of bool S
Y1 is finite Element of bool the carrier of X
setopfunc (Y1, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
r \ G is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
G \/ Y2 is finite Element of bool the carrier of X
G \/ r is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
G \/ Y2 is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
G \/ Y2 is finite Element of bool the carrier of X
setopfunc (Y2, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
abs (setopfunc (Y2, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
dom H is set
addreal . ((setopfunc (G, the carrier of X,REAL,H,addreal)),(setopfunc (Y2, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(setopfunc (G, the carrier of X,REAL,H,addreal)) + (setopfunc (Y2, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
- (setopfunc (Y2, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs (- (setopfunc (Y2, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
Y1 \ G is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
G \/ Y2 is finite Element of bool the carrier of X
G \/ Y1 is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
G \/ Y2 is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
G \/ Y2 is finite Element of bool the carrier of X
dom H is set
setopfunc (Y2, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
addreal . ((setopfunc (G, the carrier of X,REAL,H,addreal)),(setopfunc (Y2, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(setopfunc (G, the carrier of X,REAL,H,addreal)) + (setopfunc (Y2, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs (setopfunc (Y2, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
(Y02 / 2) + (Y02 / 2) is V36() real ext-real Element of REAL
(abs ((p2 . Y1) - (p2 . Y011))) + 0 is V36() real ext-real Element of REAL
r \ G is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
G \/ Y2 is finite Element of bool the carrier of X
G \/ r is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
G \/ Y2 is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
G \/ Y2 is finite Element of bool the carrier of X
dom H is set
setopfunc (Y2, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
addreal . ((setopfunc (G, the carrier of X,REAL,H,addreal)),(setopfunc (Y2, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(setopfunc (G, the carrier of X,REAL,H,addreal)) + (setopfunc (Y2, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
Y1 \ G is finite Element of bool the carrier of X
Y01 is finite Element of bool the carrier of X
G \/ Y01 is finite Element of bool the carrier of X
G \/ Y1 is finite Element of bool the carrier of X
Y01 is finite Element of bool the carrier of X
G \/ Y01 is finite Element of bool the carrier of X
Y01 is finite Element of bool the carrier of X
G \/ Y01 is finite Element of bool the carrier of X
setopfunc (Y01, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
addreal . ((setopfunc (G, the carrier of X,REAL,H,addreal)),(setopfunc (Y01, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(setopfunc (G, the carrier of X,REAL,H,addreal)) + (setopfunc (Y01, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
(setopfunc (Y01, the carrier of X,REAL,H,addreal)) - (setopfunc (Y2, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs (setopfunc (Y01, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs (setopfunc (Y2, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
(abs (setopfunc (Y01, the carrier of X,REAL,H,addreal))) + (abs (setopfunc (Y2, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(Y02 / 2) + (Y02 / 2) is V36() real ext-real Element of REAL
Y02 is V36() real ext-real set

p2 . Y01 is V36() real ext-real Element of REAL

p2 . Y1 is V36() real ext-real Element of REAL
(p2 . Y1) - (p2 . Y01) is V36() real ext-real Element of REAL
abs ((p2 . Y1) - (p2 . Y01)) is V36() real ext-real Element of REAL
Y02 is V36() real ext-real set
Y01 is V36() real ext-real Element of REAL
Y1 is V36() real ext-real Element of REAL
Y1 / 2 is V36() real ext-real Element of REAL
0 / 2 is V36() real ext-real Element of REAL

1 / (r + 1) is V36() real ext-real Element of REAL
p1 . r is Element of bool S
p2 . r is V36() real ext-real Element of REAL
G is finite Element of bool the carrier of X
setopfunc (G, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
(setopfunc (G, the carrier of X,REAL,H,addreal)) - Y01 is V36() real ext-real Element of REAL
abs ((setopfunc (G, the carrier of X,REAL,H,addreal)) - Y01) is V36() real ext-real Element of REAL
Y1 is finite Element of bool the carrier of X
setopfunc (Y1, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
Y01 - (setopfunc (Y1, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs (Y01 - (setopfunc (Y1, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(Y1 / 2) + (Y1 / 2) is V36() real ext-real Element of REAL
Y02 - (setopfunc (Y1, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs (Y02 - (setopfunc (Y1, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(abs (Y02 - (setopfunc (Y1, the carrier of X,REAL,H,addreal)))) + 0 is V36() real ext-real Element of REAL
Y1 \ G is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
G \/ Y2 is finite Element of bool the carrier of X
G \/ Y1 is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
G \/ Y2 is finite Element of bool the carrier of X
Y2 is finite Element of bool the carrier of X
G \/ Y2 is finite Element of bool the carrier of X
dom H is set
setopfunc (Y1, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
(setopfunc (Y1, the carrier of X,REAL,H,addreal)) - Y01 is V36() real ext-real Element of REAL
setopfunc (Y2, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
addreal . ((setopfunc (G, the carrier of X,REAL,H,addreal)),(setopfunc (Y2, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(addreal . ((setopfunc (G, the carrier of X,REAL,H,addreal)),(setopfunc (Y2, the carrier of X,REAL,H,addreal)))) - Y01 is V36() real ext-real Element of REAL
(setopfunc (G, the carrier of X,REAL,H,addreal)) + (setopfunc (Y2, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
((setopfunc (G, the carrier of X,REAL,H,addreal)) + (setopfunc (Y2, the carrier of X,REAL,H,addreal))) - Y01 is V36() real ext-real Element of REAL
((setopfunc (G, the carrier of X,REAL,H,addreal)) - Y01) + (setopfunc (Y2, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs ((setopfunc (Y1, the carrier of X,REAL,H,addreal)) - Y01) is V36() real ext-real Element of REAL
abs (setopfunc (Y2, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
(abs ((setopfunc (G, the carrier of X,REAL,H,addreal)) - Y01)) + (abs (setopfunc (Y2, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
Y02 - (setopfunc (Y1, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs (Y02 - (setopfunc (Y1, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(Y1 / 2) + (Y1 / 2) is V36() real ext-real Element of REAL
Y01 - (setopfunc (Y1, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs (Y01 - (setopfunc (Y1, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
setopfunc (Y1, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
Y01 - (setopfunc (Y1, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs (Y01 - (setopfunc (Y1, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
setopfunc (Y1, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
Y01 - (setopfunc (Y1, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs (Y01 - (setopfunc (Y1, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
Y1 is V36() real ext-real Element of REAL
p1 is V36() real ext-real Element of REAL
X is non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V14([: the carrier of X, the carrier of X:]) V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set
bool [: the carrier of X, the carrier of X:] is set
[: the carrier of X,REAL:] is set
bool [: the carrier of X,REAL:] is set
S is finite OrthogonalFamily of X
H is Relation-like the carrier of X -defined the carrier of X -valued Function-like non empty V14( the carrier of X) V18( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]
dom H is set
setopfunc (S, the carrier of X, the carrier of X,H, the addF of X) is Element of the carrier of X
(setopfunc (S, the carrier of X, the carrier of X,H, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,H, the addF of X)) is V36() real ext-real Element of REAL

rng p1 is set
Func_Seq (H,p1) is Relation-like NAT -defined the carrier of X -valued Function-like FinSequence-like FinSequence of the carrier of X
the addF of X "**" (Func_Seq (H,p1)) is Element of the carrier of X
p2 is Relation-like the carrier of X -defined REAL -valued Function-like non empty V14( the carrier of X) V18( the carrier of X, REAL ) Element of bool [: the carrier of X,REAL:]
dom p2 is set
setopfunc (S, the carrier of X,REAL,p2,addreal) is V36() real ext-real Element of REAL

addreal "**" (Func_Seq (p2,p1)) is V36() real ext-real Element of REAL
the scalar of X is Relation-like [: the carrier of X, the carrier of X:] -defined REAL -valued Function-like V14([: the carrier of X, the carrier of X:]) V18([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[:[: the carrier of X, the carrier of X:],REAL:] is set
bool [:[: the carrier of X, the carrier of X:],REAL:] is set
e is Element of the carrier of X
H . e is Element of the carrier of X
Y02 is Element of the carrier of X
H . Y02 is Element of the carrier of X
[(H . e),(H . Y02)] is set
{(H . e),(H . Y02)} is non empty finite set
{(H . e)} is non empty finite set
{{(H . e),(H . Y02)},{(H . e)}} is non empty finite V47() set
the scalar of X . [(H . e),(H . Y02)] is set
e .|. Y02 is V36() real ext-real Element of REAL
e is Element of the carrier of X
p2 . e is V36() real ext-real Element of REAL
H . e is Element of the carrier of X
[(H . e),(H . e)] is set
{(H . e),(H . e)} is non empty finite set
{(H . e)} is non empty finite set
{{(H . e),(H . e)},{(H . e)}} is non empty finite V47() set
the scalar of X . [(H . e),(H . e)] is set
e .|. e is V36() real ext-real Element of REAL
[( the addF of X "**" (Func_Seq (H,p1))),( the addF of X "**" (Func_Seq (H,p1)))] is set
{( the addF of X "**" (Func_Seq (H,p1))),( the addF of X "**" (Func_Seq (H,p1)))} is non empty finite set
{( the addF of X "**" (Func_Seq (H,p1)))} is non empty finite set
{{( the addF of X "**" (Func_Seq (H,p1))),( the addF of X "**" (Func_Seq (H,p1)))},{( the addF of X "**" (Func_Seq (H,p1)))}} is non empty finite V47() set
the scalar of X . [( the addF of X "**" (Func_Seq (H,p1))),( the addF of X "**" (Func_Seq (H,p1)))] is set
X is non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V14([: the carrier of X, the carrier of X:]) V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set
[: the carrier of X,REAL:] is set
bool [: the carrier of X,REAL:] is set
bool [: the carrier of X, the carrier of X:] is set
id the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one non empty V14( the carrier of X) V18( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]
H is finite OrthogonalFamily of X
setsum H is Element of the carrier of X
() .|. () is V36() real ext-real Element of REAL
p1 is Relation-like the carrier of X -defined REAL -valued Function-like non empty V14( the carrier of X) V18( the carrier of X, REAL ) Element of bool [: the carrier of X,REAL:]
dom p1 is set
setopfunc (H, the carrier of X,REAL,p1,addreal) is V36() real ext-real Element of REAL
S is Relation-like the carrier of X -defined the carrier of X -valued Function-like non empty V14( the carrier of X) V18( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]
p2 is Element of the carrier of X
S . p2 is Element of the carrier of X
dom S is set
p2 is set
S . p2 is set
setopfunc (H, the carrier of X, the carrier of X,S, the addF of X) is Element of the carrier of X
X is non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
bool the carrier of X is set
S is OrthogonalFamily of X
bool S is set
H is Element of bool the carrier of X
p1 is Element of the carrier of X
p2 is Element of the carrier of X
p1 .|. p2 is V36() real ext-real Element of REAL
X is non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
bool the carrier of X is set
S is OrthonormalFamily of X
bool S is set
H is Element of bool the carrier of X
p1 is Element of the carrier of X
p1 .|. p1 is V36() real ext-real Element of REAL
X is non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like V125() UNITSTR
the carrier of X is non empty set
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V14([: the carrier of X, the carrier of X:]) V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set
[: the carrier of X,REAL:] is set
bool [: the carrier of X,REAL:] is set
S is OrthonormalFamily of X
H is Relation-like the carrier of X -defined REAL -valued Function-like non empty V14( the carrier of X) V18( the carrier of X, REAL ) Element of bool [: the carrier of X,REAL:]
dom H is set
p1 is V36() real ext-real Element of REAL
sqrt p1 is V36() real ext-real Element of REAL
e is V36() real ext-real Element of REAL
(sqrt p1) ^2 is V36() real ext-real Element of REAL
K143((sqrt p1),(sqrt p1)) is V36() real ext-real set
e ^2 is V36() real ext-real Element of REAL
K143(e,e) is V36() real ext-real set
e * e is V36() real ext-real Element of REAL
bool the carrier of X is set
Y02 is finite Element of bool the carrier of X
Y01 is finite Element of bool the carrier of X
Y1 is finite Element of bool the carrier of X
Y011 is Element of the carrier of X
H . Y011 is V36() real ext-real Element of REAL
Y011 .|. Y011 is V36() real ext-real Element of REAL
setsum Y1 is Element of the carrier of X
(setsum Y1) .|. (setsum Y1) is V36() real ext-real Element of REAL
setopfunc (Y1, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
||.(setsum Y1).|| is V36() real ext-real Element of REAL
||.(setsum Y1).|| ^2 is V36() real ext-real Element of REAL
K143(||.(setsum Y1).||,||.(setsum Y1).||) is V36() real ext-real set
sqrt ((setsum Y1) .|. (setsum Y1)) is V36() real ext-real Element of REAL
abs (setopfunc (Y1, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
p1 is V36() real ext-real Element of REAL
p1 * p1 is V36() real ext-real Element of REAL
e is finite Element of bool the carrier of X
Y02 is finite Element of bool the carrier of X
setopfunc (Y02, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
abs (setopfunc (Y02, the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
(abs (setopfunc (Y02, the carrier of X,REAL,H,addreal))) - (abs (setopfunc (Y02, the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(setopfunc (Y02, the carrier of X,REAL,H,addreal)) - (p1 * p1) is V36() real ext-real Element of REAL
Y1 is Element of the carrier of X
H . Y1 is V36() real ext-real Element of REAL
Y1 .|. Y1 is V36() real ext-real Element of REAL
setsum Y02 is Element of the carrier of X
(setsum Y02) .|. (setsum Y02) is V36() real ext-real Element of REAL
||.(setsum Y02).|| is V36() real ext-real Element of REAL
sqrt ((setsum Y02) .|. (setsum Y02)) is V36() real ext-real Element of REAL
||.(setsum Y02).|| ^2 is V36() real ext-real Element of REAL
K143(||.(setsum Y02).||,||.(setsum Y02).||) is V36() real ext-real set
p1 ^2 is V36() real ext-real Element of REAL
K143(p1,p1) is V36() real ext-real set
sqrt (p1 ^2) is V36() real ext-real Element of REAL
sqrt (||.(setsum Y02).|| ^2) is V36() real ext-real Element of REAL
X is non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like UNITSTR
the carrier of X is non empty set
bool the carrier of X is set
S is Element of bool the carrier of X
sum S is Element of the carrier of X
(sum S) .|. (sum S) is V36() real ext-real Element of REAL
H is finite Element of bool the carrier of X
p1 is V36() real ext-real Element of REAL
||.(sum S).|| is V36() real ext-real Element of REAL
2 * ||.(sum S).|| is V36() real ext-real Element of REAL
(2 * ||.(sum S).||) + 1 is V36() real ext-real Element of REAL
p1 / ((2 * ||.(sum S).||) + 1) is V36() real ext-real Element of REAL

e is finite Element of bool the carrier of X
e \/ H is finite Element of bool the carrier of X
Y01 is finite Element of bool the carrier of X
setsum Y01 is Element of the carrier of X
(setsum Y01) .|. (setsum Y01) is V36() real ext-real Element of REAL
((sum S) .|. (sum S)) - ((setsum Y01) .|. (setsum Y01)) is V36() real ext-real Element of REAL
abs (((sum S) .|. (sum S)) - ((setsum Y01) .|. (setsum Y01))) is V36() real ext-real Element of REAL
(sum S) - (setsum Y01) is Element of the carrier of X
- (setsum Y01) is Element of the carrier of X
(sum S) + (- (setsum Y01)) is Element of the carrier of X
(p1 / ((2 * ||.(sum S).||) + 1)) * ((2 * ||.(sum S).||) + 1) is V36() real ext-real Element of REAL
||.((sum S) - (setsum Y01)).|| is V36() real ext-real Element of REAL
||.((sum S) - (setsum Y01)).|| * ((2 * ||.(sum S).||) + 1) is V36() real ext-real Element of REAL
||.(setsum Y01).|| is V36() real ext-real Element of REAL
||.(- (setsum Y01)).|| is V36() real ext-real Element of REAL
0. X is V62(X) Element of the carrier of X
(0. X) - (setsum Y01) is Element of the carrier of X
(0. X) + (- (setsum Y01)) is Element of the carrier of X
||.((0. X) - (setsum Y01)).|| is V36() real ext-real Element of REAL
- (sum S) is Element of the carrier of X
(- (sum S)) + (sum S) is Element of the carrier of X
((- (sum S)) + (sum S)) - (setsum Y01) is Element of the carrier of X
((- (sum S)) + (sum S)) + (- (setsum Y01)) is Element of the carrier of X
||.(((- (sum S)) + (sum S)) - (setsum Y01)).|| is V36() real ext-real Element of REAL
(- (sum S)) + ((sum S) - (setsum Y01)) is Element of the carrier of X
||.((- (sum S)) + ((sum S) - (setsum Y01))).|| is V36() real ext-real Element of REAL
||.(- (sum S)).|| is V36() real ext-real Element of REAL
||.(- (sum S)).|| + ||.((sum S) - (setsum Y01)).|| is V36() real ext-real Element of REAL
||.(sum S).|| + ||.((sum S) - (setsum Y01)).|| is V36() real ext-real Element of REAL
1 + (||.(sum S).|| + ||.((sum S) - (setsum Y01)).||) is V36() real ext-real Element of REAL
||.((sum S) - (setsum Y01)).|| + ||.(setsum Y01).|| is V36() real ext-real Element of REAL
1 + ||.(sum S).|| is V36() real ext-real Element of REAL
(1 + ||.(sum S).||) + ||.((sum S) - (setsum Y01)).|| is V36() real ext-real Element of REAL
((1 + ||.(sum S).||) + ||.((sum S) - (setsum Y01)).||) - ||.((sum S) - (setsum Y01)).|| is V36() real ext-real Element of REAL
||.(setsum Y01).|| + ||.((sum S) - (setsum Y01)).|| is V36() real ext-real Element of REAL
(||.(setsum Y01).|| + ||.((sum S) - (setsum Y01)).||) - ||.((sum S) - (setsum Y01)).|| is V36() real ext-real Element of REAL
(1 + ||.(sum S).||) + ||.(sum S).|| is V36() real ext-real Element of REAL
||.(sum S).|| + ||.(setsum Y01).|| is V36() real ext-real Element of REAL
||.((sum S) - (setsum Y01)).|| * (||.(sum S).|| + ||.(setsum Y01).||) is V36() real ext-real Element of REAL
((p1 / ((2 * ||.(sum S).||) + 1)) * ((2 * ||.(sum S).||) + 1)) + (||.((sum S) - (setsum Y01)).|| * ((2 * ||.(sum S).||) + 1)) is V36() real ext-real Element of REAL
(||.((sum S) - (setsum Y01)).|| * (||.(sum S).|| + ||.(setsum Y01).||)) + (||.((sum S) - (setsum Y01)).|| * ((2 * ||.(sum S).||) + 1)) is V36() real ext-real Element of REAL
(((p1 / ((2 * ||.(sum S).||) + 1)) * ((2 * ||.(sum S).||) + 1)) + (||.((sum S) - (setsum Y01)).|| * ((2 * ||.(sum S).||) + 1))) - (||.((sum S) - (setsum Y01)).|| * ((2 * ||.(sum S).||) + 1)) is V36() real ext-real Element of REAL
((||.((sum S) - (setsum Y01)).|| * (||.(sum S).|| + ||.(setsum Y01).||)) + (||.((sum S) - (setsum Y01)).|| * ((2 * ||.(sum S).||) + 1))) - (||.((sum S) - (setsum Y01)).|| * ((2 * ||.(sum S).||) + 1)) is V36() real ext-real Element of REAL
(sum S) .|. (setsum Y01) is V36() real ext-real Element of REAL
((sum S) .|. (sum S)) - ((sum S) .|. (setsum Y01)) is V36() real ext-real Element of REAL
((sum S) .|. (setsum Y01)) - ((setsum Y01) .|. (setsum Y01)) is V36() real ext-real Element of REAL
(((sum S) .|. (sum S)) - ((sum S) .|. (setsum Y01))) + (((sum S) .|. (setsum Y01)) - ((setsum Y01) .|. (setsum Y01))) is V36() real ext-real Element of REAL
abs ((((sum S) .|. (sum S)) - ((sum S) .|. (setsum Y01))) + (((sum S) .|. (setsum Y01)) - ((setsum Y01) .|. (setsum Y01)))) is V36() real ext-real Element of REAL
(sum S) .|. ((sum S) - (setsum Y01)) is V36() real ext-real Element of REAL
((sum S) .|. ((sum S) - (setsum Y01))) + (((sum S) .|. (setsum Y01)) - ((setsum Y01) .|. (setsum Y01))) is V36() real ext-real Element of REAL
abs (((sum S) .|. ((sum S) - (setsum Y01))) + (((sum S) .|. (setsum Y01)) - ((setsum Y01) .|. (setsum Y01)))) is V36() real ext-real Element of REAL
((sum S) - (setsum Y01)) .|. (setsum Y01) is V36() real ext-real Element of REAL
((sum S) .|. ((sum S) - (setsum Y01))) + (((sum S) - (setsum Y01)) .|. (setsum Y01)) is V36() real ext-real Element of REAL
abs (((sum S) .|. ((sum S) - (setsum Y01))) + (((sum S) - (setsum Y01)) .|. (setsum Y01))) is V36() real ext-real Element of REAL
abs ((sum S) .|. ((sum S) - (setsum Y01))) is V36() real ext-real Element of REAL
abs (((sum S) - (setsum Y01)) .|. (setsum Y01)) is V36() real ext-real Element of REAL
(abs ((sum S) .|. ((sum S) - (setsum Y01)))) + (abs (((sum S) - (setsum Y01)) .|. (setsum Y01))) is V36() real ext-real Element of REAL
||.(sum S).|| * ||.((sum S) - (setsum Y01)).|| is V36() real ext-real Element of REAL
(abs (((sum S) .|. (sum S)) - ((setsum Y01) .|. (setsum Y01)))) + (abs ((sum S) .|. ((sum S) - (setsum Y01)))) is V36() real ext-real Element of REAL
((abs ((sum S) .|. ((sum S) - (setsum Y01)))) + (abs (((sum S) - (setsum Y01)) .|. (setsum Y01)))) + (||.(sum S).|| * ||.((sum S) - (setsum Y01)).||) is V36() real ext-real Element of REAL
(abs (((sum S) - (setsum Y01)) .|. (setsum Y01))) + (||.(sum S).|| * ||.((sum S) - (setsum Y01)).||) is V36() real ext-real Element of REAL
((abs (((sum S) - (setsum Y01)) .|. (setsum Y01))) + (||.(sum S).|| * ||.((sum S) - (setsum Y01)).||)) + (abs ((sum S) .|. ((sum S) - (setsum Y01)))) is V36() real ext-real Element of REAL
||.((sum S) - (setsum Y01)).|| * ||.(setsum Y01).|| is V36() real ext-real Element of REAL
(abs (((sum S) .|. (sum S)) - ((setsum Y01) .|. (setsum Y01)))) + (abs (((sum S) - (setsum Y01)) .|. (setsum Y01))) is V36() real ext-real Element of REAL
((abs (((sum S) - (setsum Y01)) .|. (setsum Y01))) + (||.(sum S).|| * ||.((sum S) - (setsum Y01)).||)) + (||.((sum S) - (setsum Y01)).|| * ||.(setsum Y01).||) is V36() real ext-real Element of REAL
(||.(sum S).|| * ||.((sum S) - (setsum Y01)).||) + (||.((sum S) - (setsum Y01)).|| * ||.(setsum Y01).||) is V36() real ext-real Element of REAL
((||.(sum S).|| * ||.((sum S) - (setsum Y01)).||) + (||.((sum S) - (setsum Y01)).|| * ||.(setsum Y01).||)) + (abs (((sum S) - (setsum Y01)) .|. (setsum Y01))) is V36() real ext-real Element of REAL
||.((sum S) - (setsum Y01)).|| * ||.(sum S).|| is V36() real ext-real Element of REAL
(||.((sum S) - (setsum Y01)).|| * ||.(sum S).||) + (||.((sum S) - (setsum Y01)).|| * ||.(setsum Y01).||) is V36() real ext-real Element of REAL
p1 + (||.((sum S) - (setsum Y01)).|| * (||.(sum S).|| + ||.(setsum Y01).||)) is V36() real ext-real Element of REAL
(abs (((sum S) .|. (sum S)) - ((setsum Y01) .|. (setsum Y01)))) + (||.((sum S) - (setsum Y01)).|| * (||.(sum S).|| + ||.(setsum Y01).||)) is V36() real ext-real Element of REAL
(p1 + (||.((sum S) - (setsum Y01)).|| * (||.(sum S).|| + ||.(setsum Y01).||))) - (||.((sum S) - (setsum Y01)).|| * (||.(sum S).|| + ||.(setsum Y01).||)) is V36() real ext-real Element of REAL
((abs (((sum S) .|. (sum S)) - ((setsum Y01) .|. (setsum Y01)))) + (||.((sum S) - (setsum Y01)).|| * (||.(sum S).|| + ||.(setsum Y01).||))) - (||.((sum S) - (setsum Y01)).|| * (||.(sum S).|| + ||.(setsum Y01).||)) is V36() real ext-real Element of REAL
X is V36() real ext-real set
S is V36() real ext-real set
X - S is V36() real ext-real Element of REAL
abs (X - S) is V36() real ext-real Element of REAL
X is non empty right_complementable V106() V107() V108() V109() V110() V111() V112() RealUnitarySpace-like V125() UNITSTR
the carrier of X is non empty set
the addF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V14([: the carrier of X, the carrier of X:]) V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set
[: the carrier of X,REAL:] is set
bool [: the carrier of X,REAL:] is set
S is OrthonormalFamily of X
sum S is Element of the carrier of X
(sum S) .|. (sum S) is V36() real ext-real Element of REAL
H is Relation-like the carrier of X -defined REAL -valued Function-like non empty V14( the carrier of X) V18( the carrier of X, REAL ) Element of bool [: the carrier of X,REAL:]
dom H is set
sum_byfunc (S,H) is V36() real ext-real Element of REAL
bool the carrier of X is set
p1 is finite Element of bool the carrier of X
setsum p1 is Element of the carrier of X
(setsum p1) .|. (setsum p1) is V36() real ext-real Element of REAL
setopfunc (p1, the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
p2 is Element of the carrier of X
H . p2 is V36() real ext-real Element of REAL
p2 .|. p2 is V36() real ext-real Element of REAL
((sum S) .|. (sum S)) - (sum_byfunc (S,H)) is V36() real ext-real Element of REAL
abs (((sum S) .|. (sum S)) - (sum_byfunc (S,H))) is V36() real ext-real Element of REAL
e is V36() real ext-real Element of REAL
e / 2 is V36() real ext-real Element of REAL
0 / 2 is V36() real ext-real Element of REAL
Y02 is finite Element of bool the carrier of X
Y01 is finite Element of bool the carrier of X
Y01 \/ Y02 is finite Element of bool the carrier of X
setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal) is V36() real ext-real Element of REAL
Y011 is non empty set
Y011 \/ Y02 is non empty set
setsum (Y01 \/ Y02) is Element of the carrier of X
(setsum (Y01 \/ Y02)) .|. (setsum (Y01 \/ Y02)) is V36() real ext-real Element of REAL
((sum S) .|. (sum S)) - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs (((sum S) .|. (sum S)) - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(e / 2) + (e / 2) is V36() real ext-real Element of REAL
(sum_byfunc (S,H)) - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal)) is V36() real ext-real Element of REAL
abs ((sum_byfunc (S,H)) - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal))) is V36() real ext-real Element of REAL
(abs (((sum S) .|. (sum S)) - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal)))) + (abs ((sum_byfunc (S,H)) - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal)))) is V36() real ext-real Element of REAL
(setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal)) - (sum_byfunc (S,H)) is V36() real ext-real Element of REAL
abs ((setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal)) - (sum_byfunc (S,H))) is V36() real ext-real Element of REAL
(abs (((sum S) .|. (sum S)) - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal)))) + (abs ((setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal)) - (sum_byfunc (S,H)))) is V36() real ext-real Element of REAL
(((sum S) .|. (sum S)) - (setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal))) + ((setopfunc ((Y01 \/ Y02), the carrier of X,REAL,H,addreal)) - (sum_byfunc (S,H))) is V36() real ext-real Element of REAL