REAL is non empty non trivial non finite set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL
bool REAL is 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
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is set
omega is non empty epsilon-transitive epsilon-connected ordinal set
bool omega is set
bool NAT is set
K118(NAT) is V27() set
[:NAT,REAL:] is set
bool [:NAT,REAL:] is set
{} is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real finite V47() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive Element of NAT
0 is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real ext-real finite V47() Element of NAT
addreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like V14([:REAL,REAL:]) V18([:REAL,REAL:], REAL ) commutative associative having_a_unity Element of bool [:[:REAL,REAL:],REAL:]
2 is non empty epsilon-transitive epsilon-connected ordinal natural V36() real ext-real positive Element of NAT
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
S is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
S + 1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
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
S is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
X " is V36() real ext-real Element of REAL
H is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
H + S is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
p1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
p1 + 1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
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
p2 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
p2 + 1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
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 is Relation-like NAT -defined bool S -valued Function-like V18( NAT , bool S) Element of bool [:NAT,(bool S):]
p1 is Relation-like NAT -defined bool S -valued Function-like V18( NAT , bool S) Element of bool [:NAT,(bool S):]
p1 . 0 is Element of bool S
p2 is Relation-like Function-like set
dom p2 is set
p2 . 0 is set
p2 is Relation-like Function-like set
dom p2 is set
p2 . 0 is set
e is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
p2 . e is set
e + 1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
1 / (e + 1) is V36() real ext-real Element of REAL
p2 . (e + 1) is set
(e + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
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
Y02 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
p2 . Y02 is set
Y02 + 1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
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
Y01 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
p2 . Y01 is set
e is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
p2 . e is set
Y02 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
p2 . Y02 is set
Y02 + 1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
p2 . (Y02 + 1) is set
p1 . (Y02 + 1) is Element of bool S
(p1 . (Y02 + 1)) \/ (p2 . Y02) is set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
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
Y02 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
p2 . Y02 is set
rng p2 is set
e is set
Y02 is set
p2 . Y02 is set
Y01 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
p2 . Y01 is set
p1 is Relation-like NAT -defined bool S -valued Function-like V18( NAT , bool S) Element of bool [:NAT,(bool S):]
p1 is Relation-like NAT -defined bool S -valued Function-like V18( NAT , bool S) Element of bool [:NAT,(bool S):]
p2 is set
p1 . p2 is set
e is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
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
p2 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) Element of bool [:NAT,REAL:]
p2 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) Element of bool [:NAT,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
Y01 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
Y01 + 1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
1 / (Y01 + 1) is V36() real ext-real Element of REAL
Y1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
Y011 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
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
Y01 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
p2 . Y01 is V36() real ext-real Element of REAL
Y1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
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
Y011 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
r + 1 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
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
p1 is Relation-like NAT -defined the carrier of X -valued Function-like FinSequence-like FinSequence of the carrier of X
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
Func_Seq (p2,p1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence 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
(setsum H) .|. (setsum H) 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
0 + 0 is epsilon-transitive epsilon-connected ordinal natural V36() real ext-real Element of NAT
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