:: SEQFUNC semantic presentation

REAL is non empty V47() V48() V49() V53() V66() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V47() V53() V66() set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V47() V48() V49() V50() V51() V52() V53() set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V47() V48() V49() V50() V51() V52() V53() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V47() V48() V49() V50() V51() V52() V53() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
{{},1} is non empty V47() V48() V49() V50() V51() V52() set
INT is non empty V47() V48() V49() V50() V51() V53() V66() set
K20(REAL,REAL) is V35() V36() V37() set
K19(K20(REAL,REAL)) is set
RAT is non empty V47() V48() V49() V50() V53() V66() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V47() V48() V49() V50() V51() V52() V53() V64() V65() Element of NAT
K20(NAT,REAL) is V35() V36() V37() set
K19(K20(NAT,REAL)) is set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
omega is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() set
X is set
H is set
PFuncs (X,H) is functional non empty set
K20(NAT,(PFuncs (X,H))) is set
K19(K20(NAT,(PFuncs (X,H)))) is set
l is Relation-like NAT -defined PFuncs (X,H) -valued Function-like non empty total V18( NAT , PFuncs (X,H)) Element of K19(K20(NAT,(PFuncs (X,H))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real set
l . x0 is set
K20(X,H) is set
K19(K20(X,H)) is set
dom l is V47() V48() V49() V50() V51() V52() Element of K19(NAT)
K19(NAT) is set
rng l is Element of K19((PFuncs (X,H)))
K19((PFuncs (X,H))) is set
X is set
H is set
PFuncs (X,H) is functional non empty set
K20(NAT,(PFuncs (X,H))) is set
K19(K20(NAT,(PFuncs (X,H)))) is set
K20(X,H) is set
K19(K20(X,H)) is set
l is Relation-like Function-like set
dom l is set
x0 is set
l . x0 is set
rng l is set
x0 is set
rng l is set
x0 is set
l . x0 is set
X is set
H is set
PFuncs (X,H) is functional non empty set
K20(NAT,(PFuncs (X,H))) is set
K19(K20(NAT,(PFuncs (X,H)))) is set
K20(X,H) is set
K19(K20(X,H)) is set
l is Relation-like Function-like set
dom l is set
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
l . x0 is set
x0 is set
l . x0 is set
F₁() is set
F₂() is set
K20(F₁(),F₂()) is set
K19(K20(F₁(),F₂())) is set
PFuncs (F₁(),F₂()) is functional non empty set
K20(NAT,(PFuncs (F₁(),F₂()))) is set
K19(K20(NAT,(PFuncs (F₁(),F₂())))) is set
X is set
F₃(X) is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
X is Relation-like Function-like set
dom X is set
H is set
X . H is set
F₃(H) is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
H is Relation-like NAT -defined PFuncs (F₁(),F₂()) -valued Function-like non empty total V18( NAT , PFuncs (F₁(),F₂())) Element of K19(K20(NAT,(PFuncs (F₁(),F₂()))))
l is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real set
(F₁(),F₂(),H,l) is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
F₃(l) is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is V30() real ext-real set
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,x0,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,H,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
l (#) (X,REAL,H,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) ^ is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- 1 is V30() real ext-real Element of REAL
(X,H,(- 1)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real set
(X,REAL,(X,H,(- 1)),l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,H,l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- (X,REAL,H,l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K116(1) is V30() real ext-real set
K116(1) (#) (X,REAL,H,l) is Relation-like X -defined Function-like V35() V36() V37() set
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- (X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K116(1) is V30() real ext-real set
K116(1) (#) (X,REAL,H,x0) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real set
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- (X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K116(1) is V30() real ext-real set
K116(1) (#) (X,REAL,l,x0) is Relation-like X -defined Function-like V35() V36() V37() set
- (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K116(1) (#) (X,REAL,x0,x0) is Relation-like X -defined Function-like V35() V36() V37() set
- (- (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K116(1) (#) (- (X,REAL,x0,x0)) is Relation-like X -defined Function-like V35() V36() V37() set
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
abs (X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real set
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
abs (X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
abs (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
abs (abs (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,x0,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,H,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,r) + (X,REAL,l,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H,(X,l)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,x0,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,H,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,r) (#) (X,REAL,l,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,(X,H)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,x0,l) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,(X,x0)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) / (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) (#) (X,REAL,(X,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) ^ is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) (#) ((X,REAL,x0,x0) ^) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) / (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) ^ is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) (#) ((X,REAL,x0,x0) ^) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) (#) (X,REAL,(X,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,x0,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,(X,x0)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) - (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- (X,REAL,x0,x0) is Relation-like X -defined Function-like V35() V36() V37() set
K116(1) is V30() real ext-real set
K116(1) (#) (X,REAL,x0,x0) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,l,x0) + (- (X,REAL,x0,x0)) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,(X,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) + (X,REAL,(X,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) - (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- (X,REAL,x0,x0) is Relation-like X -defined Function-like V35() V36() V37() set
K116(1) is V30() real ext-real set
K116(1) (#) (X,REAL,x0,x0) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,l,x0) + (- (X,REAL,x0,x0)) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,(X,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) + (X,REAL,(X,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H,l) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,H,l),x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H,(X,l,x0)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,H,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) + (X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,(X,H,l),x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,l),x0) + (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) + (X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
((X,REAL,H,x0) + (X,REAL,l,x0)) + (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) + (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) + ((X,REAL,l,x0) + (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) + (X,REAL,(X,l,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,(X,l,x0)),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H,l) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,H,l),x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H,(X,l,x0)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,H,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) (#) (X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,(X,H,l),x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,l),x0) (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) (#) (X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
((X,REAL,H,x0) (#) (X,REAL,l,x0)) (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) (#) ((X,REAL,l,x0) (#) (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) (#) (X,REAL,(X,l,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,(X,l,x0)),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H,l) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,H,l),x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H,x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,H,x0),(X,l,x0)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,x0,(X,H,l)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,x0,H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,x0,l) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,x0,H),(X,x0,l)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,(X,H,l),x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,(X,H,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,l),x0) (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) + (X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
((X,REAL,H,x0) + (X,REAL,l,x0)) (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
((X,REAL,H,x0) (#) (X,REAL,x0,x0)) + ((X,REAL,l,x0) (#) (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,x0),x0) + ((X,REAL,l,x0) (#) (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,x0),x0) + (X,REAL,(X,l,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,(X,H,x0),(X,l,x0)),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,(X,x0,H),(X,l,x0)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
- 1 is V30() real ext-real Element of REAL
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H,(- 1)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,H),l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,H,l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- (X,REAL,H,l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K116(1) is V30() real ext-real set
K116(1) (#) (X,REAL,H,l) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,(X,H,(- 1)),l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H,l) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H,(X,l)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,H,l),x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H,x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,H,x0),(X,l,x0)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,l,x0)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,H,x0),(X,(X,l,x0))) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,x0,H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,x0,l) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,x0,H),(X,x0,l)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,x0,l)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,x0,H),(X,(X,x0,l))) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,x0,(X,H,l)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,(X,H,l),x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,(X,H,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,l),x0) (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) - (X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- (X,REAL,l,x0) is Relation-like X -defined Function-like V35() V36() V37() set
K116(1) is V30() real ext-real set
K116(1) (#) (X,REAL,l,x0) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,H,x0) + (- (X,REAL,l,x0)) is Relation-like X -defined Function-like V35() V36() V37() set
((X,REAL,H,x0) - (X,REAL,l,x0)) (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
((X,REAL,H,x0) (#) (X,REAL,x0,x0)) - ((X,REAL,l,x0) (#) (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- ((X,REAL,l,x0) (#) (X,REAL,x0,x0)) is Relation-like X -defined Function-like V35() V36() V37() set
K116(1) (#) ((X,REAL,l,x0) (#) (X,REAL,x0,x0)) is Relation-like X -defined Function-like V35() V36() V37() set
((X,REAL,H,x0) (#) (X,REAL,x0,x0)) + (- ((X,REAL,l,x0) (#) (X,REAL,x0,x0))) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,(X,H,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,x0),x0) - ((X,REAL,l,x0) (#) (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,x0),x0) + (- ((X,REAL,l,x0) (#) (X,REAL,x0,x0))) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,(X,l,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,x0),x0) - (X,REAL,(X,l,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- (X,REAL,(X,l,x0),x0) is Relation-like X -defined Function-like V35() V36() V37() set
K116(1) (#) (X,REAL,(X,l,x0),x0) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,(X,H,x0),x0) + (- (X,REAL,(X,l,x0),x0)) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,(X,(X,H,x0),(X,l,x0)),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,(X,x0,H),(X,l,x0)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,x0,H),(X,(X,l,x0))) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is V30() real ext-real Element of REAL
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,l,x0),H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,x0,H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,l,H),(X,x0,H)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,x0) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,(X,x0)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,l,x0),H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,l,H),(X,x0,H)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,x0,H)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,l,H),(X,(X,x0,H))) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,(X,l,x0),H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,(X,l,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
H (#) (X,REAL,(X,l,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) + (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
H (#) ((X,REAL,l,x0) + (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
H (#) (X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
H (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(H (#) (X,REAL,l,x0)) + (H (#) (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,H),x0) + (H (#) (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,x0,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,H),x0) + (X,REAL,(X,x0,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,(X,l,H),(X,x0,H)),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,(X,l,x0),H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
H (#) (X,REAL,(X,l,x0),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) - (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- (X,REAL,x0,x0) is Relation-like X -defined Function-like V35() V36() V37() set
K116(1) is V30() real ext-real set
K116(1) (#) (X,REAL,x0,x0) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,l,x0) + (- (X,REAL,x0,x0)) is Relation-like X -defined Function-like V35() V36() V37() set
H (#) ((X,REAL,l,x0) - (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
H (#) (X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
H (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(H (#) (X,REAL,l,x0)) - (H (#) (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- (H (#) (X,REAL,x0,x0)) is Relation-like X -defined Function-like V35() V36() V37() set
K116(1) (#) (H (#) (X,REAL,x0,x0)) is Relation-like X -defined Function-like V35() V36() V37() set
(H (#) (X,REAL,l,x0)) + (- (H (#) (X,REAL,x0,x0))) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,(X,l,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,H),x0) - (H (#) (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,H),x0) + (- (H (#) (X,REAL,x0,x0))) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,(X,x0,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,H),x0) - (X,REAL,(X,x0,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- (X,REAL,(X,x0,H),x0) is Relation-like X -defined Function-like V35() V36() V37() set
K116(1) (#) (X,REAL,(X,x0,H),x0) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,(X,l,H),x0) + (- (X,REAL,(X,x0,H),x0)) is Relation-like X -defined Function-like V35() V36() V37() set
(X,REAL,(X,(X,l,H),(X,x0,H)),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is V30() real ext-real Element of REAL
l is V30() real ext-real Element of REAL
H * l is V30() real ext-real Element of REAL
x0 is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,x0,(H * l)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,x0,l) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,x0,l),H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,x0,(H * l)),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(H * l) (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
l (#) (X,REAL,x0,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
H (#) (l (#) (X,REAL,x0,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,x0,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
H (#) (X,REAL,(X,x0,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,(X,x0,l),H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H,1) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,H,1),l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,H,l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
1 (#) (X,REAL,H,l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,H),(X,l)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H,l) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,H,l)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,(X,H),(X,l)),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,(X,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H),x0) (#) (X,REAL,(X,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) ^ is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
((X,REAL,H,x0) ^) (#) (X,REAL,(X,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) ^ is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
((X,REAL,H,x0) ^) (#) ((X,REAL,l,x0) ^) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,x0) (#) (X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
((X,REAL,H,x0) (#) (X,REAL,l,x0)) ^ is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H,l),x0) ^ is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,(X,H,l)),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is V30() real ext-real Element of REAL
H " is V30() real ext-real Element of REAL
l is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l,H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,l,H)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,l) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,l),(H ")) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,(X,l,H)),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
(X,REAL,(X,l,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l,H),x0) ^ is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
H (#) (X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(H (#) (X,REAL,l,x0)) ^ is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,l,x0) ^ is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(H ") (#) ((X,REAL,l,x0) ^) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(H ") (#) (X,REAL,(X,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,(X,l),(H ")),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
X is non empty set
PFuncs (X,REAL) is functional non empty set
K20(NAT,(PFuncs (X,REAL))) is set
K19(K20(NAT,(PFuncs (X,REAL)))) is set
H is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,H)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,H) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
(X,(X,H)) is Relation-like NAT -defined PFuncs (X,REAL) -valued Function-like non empty total V18( NAT , PFuncs (X,REAL)) Element of K19(K20(NAT,(PFuncs (X,REAL))))
l is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,REAL,(X,(X,H)),l) is Relation-like X -defined