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
F1() is set
F2() is set
K20(F1(),F2()) is set
K19(K20(F1(),F2())) is set
PFuncs (F1(),F2()) is functional non empty set
K20(NAT,(PFuncs (F1(),F2()))) is set
K19(K20(NAT,(PFuncs (F1(),F2())))) is set
X is set
F3(X) is Relation-like F1() -defined F2() -valued Function-like Element of K19(K20(F1(),F2()))
X is Relation-like Function-like set
dom X is set
H is set
X . H is set
F3(H) is Relation-like F1() -defined F2() -valued Function-like Element of K19(K20(F1(),F2()))
H is Relation-like NAT -defined PFuncs (F1(),F2()) -valued Function-like non empty total V18( NAT , PFuncs (F1(),F2())) Element of K19(K20(NAT,(PFuncs (F1(),F2()))))
l is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real set
(F1(),F2(),H,l) is Relation-like F1() -defined F2() -valued Function-like Element of K19(K20(F1(),F2()))
F3(l) is Relation-like F1() -defined F2() -valued Function-like Element of K19(K20(F1(),F2()))
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 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) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
abs (X,REAL,(X,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))
(X,REAL,H,l) ^ is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
abs ((X,REAL,H,l) ^) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
abs (X,REAL,H,l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(abs (X,REAL,H,l)) ^ is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H),l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H),l) ^ is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,(X,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,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))))
(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))))
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) 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))
abs (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,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))
abs ((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))
abs (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,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(abs (X,REAL,H,x0)) (#) (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,(X,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,(X,H),x0) (#) (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,(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,(X,(X,H),(X,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))))
(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,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,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,(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),(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,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,(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)) 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,(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 V30() real ext-real Element of REAL
abs 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),(abs 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))
abs (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))
abs (H (#) (X,REAL,l,x0)) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
abs (X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(abs H) (#) (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,(X,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(abs 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),(abs H)),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
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
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 Element of X
x0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
x0 is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
x0 . r is V30() real ext-real Element of REAL
(X,REAL,H,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) . l is V30() real ext-real Element of REAL
x0 . r 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
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
K20(X,REAL) is V35() V36() V37() set
K19(K20(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 set
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
K19(X) is set
x0 is Element of X
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (X,H,x0) is V30() real ext-real Element of REAL
x0 . x0 is V30() real ext-real Element of REAL
r is V30() real ext-real set
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
k1 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,k1) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,k1) . x0 is V30() real ext-real Element of REAL
((X,REAL,H,k1) . x0) - (x0 . x0) is V30() real ext-real Element of REAL
abs (((X,REAL,H,k1) . x0) - (x0 . x0)) is V30() real ext-real Element of REAL
(X,H,x0) . k1 is V30() real ext-real Element of REAL
((X,H,x0) . k1) - (x0 . x0) is V30() real ext-real Element of REAL
abs (((X,H,x0) . k1) - (x0 . x0)) is V30() real ext-real Element of REAL
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
K19(X) is set
x0 is Element of X
x0 . x0 is V30() real ext-real Element of REAL
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (X,H,x0) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
k 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,k) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,k) . x0 is V30() real ext-real Element of REAL
((X,REAL,H,k) . x0) - (x0 . x0) is V30() real ext-real Element of REAL
abs (((X,REAL,H,k) . x0) - (x0 . x0)) is V30() real ext-real Element of REAL
(X,H,x0) . k is V30() real ext-real Element of REAL
((X,H,x0) . k) - (x0 . x0) is V30() real ext-real Element of REAL
abs (((X,H,x0) . k) - (x0 . x0)) is V30() real ext-real Element of REAL
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
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 set
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
K19(X) is set
x0 is Element of X
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
r is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom r is Element of K19(X)
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
r is set
(X,REAL,H,0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (X,REAL,H,0) is Element of K19(X)
r is Element of X
r is set
r is Element of X
(X,H,r) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
x0 . r is V30() real ext-real Element of REAL
lim (X,H,r) is V30() real ext-real Element of REAL
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
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
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 set
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
K19(X) is set
x0 is Element of X
x0 . x0 is V30() real ext-real Element of REAL
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (X,H,x0) 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
K20(X,REAL) is V35() V36() V37() set
K19(K20(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 set
(X,H,l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
K19(X) is set
x0 is Element of X
x0 . x0 is V30() real ext-real Element of REAL
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
lim (X,H,x0) is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
k 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,k) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,k) . x0 is V30() real ext-real Element of REAL
((X,REAL,H,k) . x0) - (x0 . x0) is V30() real ext-real Element of REAL
abs (((X,REAL,H,k) . x0) - (x0 . x0)) is V30() real ext-real Element of REAL
(X,H,x0) . k is V30() real ext-real Element of REAL
((X,H,x0) . k) - (x0 . x0) is V30() real ext-real Element of REAL
abs (((X,H,x0) . k) - (x0 . x0)) is V30() real ext-real Element of REAL
x0 is Element of X
r is V30() real ext-real set
x0 . x0 is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
k1 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,k1) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,k1) . x0 is V30() real ext-real Element of REAL
((X,REAL,H,k1) . x0) - (x0 . x0) is V30() real ext-real Element of REAL
abs (((X,REAL,H,k1) . x0) - (x0 . x0)) is V30() real ext-real Element of REAL
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,x0) . k1 is V30() real ext-real Element of REAL
((X,H,x0) . k1) - (x0 . x0) is V30() real ext-real Element of REAL
abs (((X,H,x0) . k1) - (x0 . x0)) is V30() real ext-real Element of REAL
lim (X,H,x0) 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))))
l is set
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
K19(X) is set
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
r is Element of X
r is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
m 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,m) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,m) . r is V30() real ext-real Element of REAL
x0 . r is V30() real ext-real Element of REAL
((X,REAL,H,m) . r) - (x0 . r) is V30() real ext-real Element of REAL
abs (((X,REAL,H,m) . r) - (x0 . r)) is V30() real ext-real Element of REAL
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
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 set
x0 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
(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
dom (X,REAL,H,x0) is Element of K19(X)
K19(X) is set
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 set
(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
x0 is set
(X,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,H,x0) | l is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
K19(X) is set
x0 | l is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
r is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom r is Element of K19(X)
r is Element of X
k is V30() real ext-real Element of REAL
x0 . r is V30() real ext-real Element of REAL
k1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
h 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,h) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,h) . r is V30() real ext-real Element of REAL
((X,REAL,H,h) . r) - (x0 . r) is V30() real ext-real Element of REAL
abs (((X,REAL,H,h) . r) - (x0 . r)) is V30() real ext-real Element of REAL
r . r is V30() real ext-real Element of REAL
((X,REAL,H,h) . r) - (r . r) is V30() real ext-real Element of REAL
abs (((X,REAL,H,h) . r) - (r . r)) is V30() real ext-real Element of REAL
r is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom r is Element of K19(X)
r is Element of X
dom ((X,H,x0) | l) is Element of K19(X)
dom (X,H,x0) is Element of K19(X)
(dom (X,H,x0)) /\ l is Element of K19(X)
dom (X,H,l) is Element of K19(X)
((X,H,x0) | l) . r is V30() real ext-real Element of REAL
(X,H,x0) . r is V30() real ext-real Element of REAL
(X,H,r) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (X,H,r) is V30() real ext-real Element of REAL
(X,H,l) . r 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))))
l is set
x0 is set
K20(X,REAL) is V35() V36() V37() set
K19(K20(X,REAL)) is set
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
K19(X) is set
x0 | l is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
r is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom r is Element of K19(X)
(dom x0) /\ l is Element of K19(X)
r is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
h is Element of X
(X,REAL,H,m) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,m) . h is V30() real ext-real Element of REAL
x0 . h is V30() real ext-real Element of REAL
((X,REAL,H,m) . h) - (x0 . h) is V30() real ext-real Element of REAL
abs (((X,REAL,H,m) . h) - (x0 . h)) is V30() real ext-real Element of REAL
r . h is V30() real ext-real Element of REAL
((X,REAL,H,m) . h) - (r . h) is V30() real ext-real Element of REAL
abs (((X,REAL,H,m) . h) - (r . h)) is V30() real ext-real Element of REAL
r is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom r is Element of K19(X)
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 set
x0 is Element of X
{x0} is non empty set
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
dom (X,REAL,H,x0) is Element of K19(X)
K19(X) 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
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (X,REAL,H,x0) is Element of K19(X)
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 set
x0 is Element of X
{x0} is non empty set
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,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))))
(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 Element of X
{x0} is non empty set
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,x0) + (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,x0) - (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
- (X,l,x0) is Relation-like NAT -defined Function-like total V35() V36() V37() set
K116(1) is V30() real ext-real set
K116(1) (#) (X,l,x0) is Relation-like NAT -defined Function-like total V35() V36() V37() set
(X,H,x0) + (- (X,l,x0)) is Relation-like NAT -defined Function-like total V35() V36() V37() set
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,x0) (#) (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,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
dom (X,REAL,l,x0) is Element of K19(X)
K19(X) is set
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (X,REAL,H,x0) is Element of K19(X)
(dom (X,REAL,H,x0)) /\ (dom (X,REAL,l,x0)) is Element of K19(X)
(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))
dom ((X,REAL,H,x0) + (X,REAL,l,x0)) is Element of K19(X)
((X,H,x0) + (X,l,x0)) . x0 is V30() real ext-real Element of REAL
(X,H,x0) . x0 is V30() real ext-real Element of REAL
(X,l,x0) . x0 is V30() real ext-real Element of REAL
((X,H,x0) . x0) + ((X,l,x0) . x0) is V30() real ext-real Element of REAL
(X,REAL,H,x0) . x0 is V30() real ext-real Element of REAL
((X,REAL,H,x0) . x0) + ((X,l,x0) . x0) is V30() real ext-real Element of REAL
(X,REAL,l,x0) . x0 is V30() real ext-real Element of REAL
((X,REAL,H,x0) . x0) + ((X,REAL,l,x0) . x0) is V30() real ext-real Element of REAL
((X,REAL,H,x0) + (X,REAL,l,x0)) . x0 is V30() real ext-real Element of 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) . x0 is V30() real ext-real Element of REAL
(X,(X,H,l),x0) . x0 is V30() real ext-real Element of 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))
dom (X,REAL,l,x0) is Element of K19(X)
(X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (X,REAL,H,x0) is Element of K19(X)
(dom (X,REAL,H,x0)) /\ (dom (X,REAL,l,x0)) is Element of K19(X)
(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) (#) (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
dom ((X,REAL,H,x0) - (X,REAL,l,x0)) is Element of K19(X)
((X,H,x0) - (X,l,x0)) . x0 is V30() real ext-real Element of REAL
(X,H,x0) . x0 is V30() real ext-real Element of REAL
(X,l,x0) . x0 is V30() real ext-real Element of REAL
((X,H,x0) . x0) - ((X,l,x0) . x0) is V30() real ext-real Element of REAL
(X,REAL,H,x0) . x0 is V30() real ext-real Element of REAL
((X,REAL,H,x0) . x0) - ((X,l,x0) . x0) is V30() real ext-real Element of REAL
(X,REAL,l,x0) . x0 is V30() real ext-real Element of REAL
((X,REAL,H,x0) . x0) - ((X,REAL,l,x0) . x0) is V30() real ext-real Element of REAL
((X,REAL,H,x0) - (X,REAL,l,x0)) . x0 is V30() real ext-real Element of 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) . x0 is V30() real ext-real Element of REAL
(X,(X,H,l),x0) . x0 is V30() real ext-real Element of 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,H,x0) (#) (X,l,x0)) . x0 is V30() real ext-real Element of REAL
(X,H,x0) . x0 is V30() real ext-real Element of REAL
(X,l,x0) . x0 is V30() real ext-real Element of REAL
((X,H,x0) . x0) * ((X,l,x0) . x0) is V30() real ext-real Element of 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) . x0 is V30() real ext-real Element of REAL
((X,REAL,H,x0) . x0) * ((X,l,x0) . x0) is V30() real ext-real Element of 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) . x0 is V30() real ext-real Element of REAL
((X,REAL,H,x0) . x0) * ((X,REAL,l,x0) . x0) is V30() real ext-real Element of 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)) . x0 is V30() real ext-real Element of 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) . x0 is V30() real ext-real Element of REAL
(X,(X,H,l),x0) . x0 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) 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 Element of X
(X,(X,H),l) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,l) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
abs (X,H,l) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,(X,H),l) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
- (X,H,l) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
K116(1) is V30() real ext-real set
K116(1) (#) (X,H,l) is Relation-like NAT -defined Function-like total V35() V36() V37() set
x0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(X,(X,H),l) . x0 is V30() real ext-real Element of REAL
(X,REAL,(X,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,H),x0) . l is V30() real ext-real Element of REAL
(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))
(abs (X,REAL,H,x0)) . l is V30() real ext-real Element of REAL
(X,REAL,H,x0) . l is V30() real ext-real Element of REAL
abs ((X,REAL,H,x0) . l) is V30() real ext-real Element of REAL
(X,H,l) . x0 is V30() real ext-real Element of REAL
abs ((X,H,l) . x0) is V30() real ext-real Element of REAL
(abs (X,H,l)) . x0 is V30() real ext-real Element of 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,(X,H),l) . x0 is V30() real ext-real Element of REAL
(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,H),x0) . l is V30() real ext-real Element of 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))
K116(1) (#) (X,REAL,H,x0) is Relation-like X -defined Function-like V35() V36() V37() set
(- (X,REAL,H,x0)) . l is V30() real ext-real Element of REAL
(X,REAL,H,x0) . l is V30() real ext-real Element of REAL
- ((X,REAL,H,x0) . l) is V30() real ext-real Element of REAL
(X,H,l) . x0 is V30() real ext-real Element of REAL
- ((X,H,l) . x0) is V30() real ext-real Element of REAL
(- (X,H,l)) . x0 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 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 Element of X
{x0} is non empty set
(X,(X,l,H),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
H (#) (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,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
dom (X,REAL,l,x0) is Element of K19(X)
K19(X) is set
H (#) (X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (H (#) (X,REAL,l,x0)) is Element of K19(X)
(X,(X,l,H),x0) . x0 is V30() real ext-real Element of 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) . x0 is V30() real ext-real Element of REAL
(H (#) (X,REAL,l,x0)) . x0 is V30() real ext-real Element of REAL
(X,REAL,l,x0) . x0 is V30() real ext-real Element of REAL
H * ((X,REAL,l,x0) . x0) is V30() real ext-real Element of REAL
(X,l,x0) . x0 is V30() real ext-real Element of REAL
H * ((X,l,x0) . x0) is V30() real ext-real Element of REAL
(H (#) (X,l,x0)) . x0 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))))
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,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))))
(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 set
x0 is Element of X
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,x0) + (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,x0) - (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
- (X,l,x0) is Relation-like NAT -defined Function-like total V35() V36() V37() set
K116(1) is V30() real ext-real set
K116(1) (#) (X,l,x0) is Relation-like NAT -defined Function-like total V35() V36() V37() set
(X,H,x0) + (- (X,l,x0)) is Relation-like NAT -defined Function-like total V35() V36() V37() set
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,x0) (#) (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
{x0} is non empty set
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
x0 is non empty set
PFuncs (x0,REAL) is functional non empty set
K20(NAT,(PFuncs (x0,REAL))) is set
K19(K20(NAT,(PFuncs (x0,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 Element of X
(X,(X,H),l) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,l) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
abs (X,H,l) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
x0 is Relation-like NAT -defined PFuncs (x0,REAL) -valued Function-like non empty total V18( NAT , PFuncs (x0,REAL)) Element of K19(K20(NAT,(PFuncs (x0,REAL))))
(x0,x0) is Relation-like NAT -defined PFuncs (x0,REAL) -valued Function-like non empty total V18( NAT , PFuncs (x0,REAL)) Element of K19(K20(NAT,(PFuncs (x0,REAL))))
r is Element of x0
(x0,(x0,x0),r) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(x0,x0,r) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
- (x0,x0,r) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
K116(1) is V30() real ext-real set
K116(1) (#) (x0,x0,r) is Relation-like NAT -defined Function-like total V35() V36() V37() set
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 set
x0 is Element of X
(X,(X,l,H),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
H (#) (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
{x0} is non empty set
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,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))))
(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 set
x0 is Element of X
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,x0) + (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,x0) - (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
- (X,l,x0) is Relation-like NAT -defined Function-like total V35() V36() V37() set
K116(1) is V30() real ext-real set
K116(1) (#) (X,l,x0) is Relation-like NAT -defined Function-like total V35() V36() V37() set
(X,H,x0) + (- (X,l,x0)) is Relation-like NAT -defined Function-like total V35() V36() V37() set
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,x0) (#) (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,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
x0 is non empty set
PFuncs (x0,REAL) is functional non empty set
K20(NAT,(PFuncs (x0,REAL))) is set
K19(K20(NAT,(PFuncs (x0,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 Element of X
(X,(X,H),l) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,l) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
abs (X,H,l) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
x0 is Relation-like NAT -defined PFuncs (x0,REAL) -valued Function-like non empty total V18( NAT , PFuncs (x0,REAL)) Element of K19(K20(NAT,(PFuncs (x0,REAL))))
(x0,x0) is Relation-like NAT -defined PFuncs (x0,REAL) -valued Function-like non empty total V18( NAT , PFuncs (x0,REAL)) Element of K19(K20(NAT,(PFuncs (x0,REAL))))
r is Element of x0
(x0,(x0,x0),r) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(x0,x0,r) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
- (x0,x0,r) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
K116(1) is V30() real ext-real set
K116(1) (#) (x0,x0,r) is Relation-like NAT -defined Function-like total V35() V36() V37() set
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 set
x0 is Element of X
(X,(X,l,H),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
H (#) (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,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,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))))
(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 set
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
dom (X,REAL,H,x0) is Element of K19(X)
K19(X) is set
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (X,REAL,l,x0) is Element of K19(X)
(dom (X,REAL,H,x0)) /\ (dom (X,REAL,l,x0)) is Element of K19(X)
(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))
dom ((X,REAL,H,x0) + (X,REAL,l,x0)) is Element of K19(X)
(X,REAL,(X,H,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (X,REAL,(X,H,l),x0) is Element of K19(X)
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))
dom (X,REAL,H,x0) is Element of K19(X)
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (X,REAL,l,x0) is Element of K19(X)
(dom (X,REAL,H,x0)) /\ (dom (X,REAL,l,x0)) is Element of K19(X)
(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
dom ((X,REAL,H,x0) - (X,REAL,l,x0)) is Element of K19(X)
(X,REAL,(X,H,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (X,REAL,(X,H,l),x0) is Element of K19(X)
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))
dom (X,REAL,H,x0) is Element of K19(X)
(X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (X,REAL,l,x0) is Element of K19(X)
(dom (X,REAL,H,x0)) /\ (dom (X,REAL,l,x0)) is Element of K19(X)
(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))
dom ((X,REAL,H,x0) (#) (X,REAL,l,x0)) is Element of K19(X)
(X,REAL,(X,H,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (X,REAL,(X,H,l),x0) is Element of K19(X)
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) 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 set
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
dom (X,REAL,H,x0) is Element of K19(X)
K19(X) is set
abs (X,REAL,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (abs (X,REAL,H,x0)) is Element of K19(X)
(X,REAL,(X,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (X,REAL,(X,H),x0) is Element of K19(X)
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))
dom (X,REAL,H,x0) is Element of K19(X)
- (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
dom (- (X,REAL,H,x0)) is Element of K19(X)
(X,REAL,(X,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (X,REAL,(X,H),x0) is Element of K19(X)
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 set
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
dom (X,REAL,l,x0) is Element of K19(X)
K19(X) is set
H (#) (X,REAL,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (H (#) (X,REAL,l,x0)) is Element of K19(X)
(X,REAL,(X,l,H),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom (X,REAL,(X,l,H),x0) is Element of K19(X)
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,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))))
(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 set
(X,(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,H,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,H,x0) + (X,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(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,H,x0) - (X,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- (X,l,x0) is Relation-like X -defined Function-like V35() V36() V37() set
K116(1) is V30() real ext-real set
K116(1) (#) (X,l,x0) is Relation-like X -defined Function-like V35() V36() V37() set
(X,H,x0) + (- (X,l,x0)) is Relation-like X -defined Function-like V35() V36() V37() set
(X,(X,H,l),x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,H,x0) (#) (X,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
x0 is Element of X
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,x0) + (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
x0 is Element of X
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,x0) - (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
- (X,l,x0) is Relation-like NAT -defined Function-like total V35() V36() V37() set
K116(1) (#) (X,l,x0) is Relation-like NAT -defined Function-like total V35() V36() V37() set
(X,H,x0) + (- (X,l,x0)) is Relation-like NAT -defined Function-like total V35() V36() V37() set
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
x0 is Element of X
dom ((X,H,x0) + (X,l,x0)) is Element of K19(X)
K19(X) is set
dom (X,H,x0) is Element of K19(X)
dom (X,l,x0) is Element of K19(X)
(dom (X,H,x0)) /\ (dom (X,l,x0)) is Element of K19(X)
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
((X,H,x0) + (X,l,x0)) . x0 is V30() real ext-real Element of REAL
(X,H,x0) . x0 is V30() real ext-real Element of REAL
(X,l,x0) . x0 is V30() real ext-real Element of REAL
((X,H,x0) . x0) + ((X,l,x0) . x0) is V30() real ext-real Element of REAL
lim (X,H,x0) is V30() real ext-real Element of REAL
(lim (X,H,x0)) + ((X,l,x0) . x0) is V30() real ext-real Element of REAL
lim (X,l,x0) is V30() real ext-real Element of REAL
(lim (X,H,x0)) + (lim (X,l,x0)) is V30() real ext-real Element of REAL
(X,H,x0) + (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim ((X,H,x0) + (X,l,x0)) is V30() real ext-real Element of REAL
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (X,(X,H,l),x0) is V30() real ext-real Element of REAL
x0 is Element of X
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,H,x0) (#) (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
x0 is Element of X
dom ((X,H,x0) (#) (X,l,x0)) is Element of K19(X)
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
((X,H,x0) (#) (X,l,x0)) . x0 is V30() real ext-real Element of REAL
(X,H,x0) . x0 is V30() real ext-real Element of REAL
(X,l,x0) . x0 is V30() real ext-real Element of REAL
((X,H,x0) . x0) * ((X,l,x0) . x0) is V30() real ext-real Element of REAL
lim (X,H,x0) is V30() real ext-real Element of REAL
(lim (X,H,x0)) * ((X,l,x0) . x0) is V30() real ext-real Element of REAL
lim (X,l,x0) is V30() real ext-real Element of REAL
(lim (X,H,x0)) * (lim (X,l,x0)) is V30() real ext-real Element of REAL
(X,H,x0) (#) (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim ((X,H,x0) (#) (X,l,x0)) is V30() real ext-real Element of REAL
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (X,(X,H,l),x0) is V30() real ext-real Element of REAL
x0 is Element of X
dom ((X,H,x0) - (X,l,x0)) is Element of K19(X)
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
((X,H,x0) - (X,l,x0)) . x0 is V30() real ext-real Element of REAL
(X,H,x0) . x0 is V30() real ext-real Element of REAL
(X,l,x0) . x0 is V30() real ext-real Element of REAL
((X,H,x0) . x0) - ((X,l,x0) . x0) is V30() real ext-real Element of REAL
lim (X,H,x0) is V30() real ext-real Element of REAL
(lim (X,H,x0)) - ((X,l,x0) . x0) is V30() real ext-real Element of REAL
lim (X,l,x0) is V30() real ext-real Element of REAL
(lim (X,H,x0)) - (lim (X,l,x0)) is V30() real ext-real Element of REAL
(X,H,x0) - (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
- (X,l,x0) is Relation-like NAT -defined Function-like total V35() V36() V37() set
K116(1) (#) (X,l,x0) is Relation-like NAT -defined Function-like total V35() V36() V37() set
(X,H,x0) + (- (X,l,x0)) is Relation-like NAT -defined Function-like total V35() V36() V37() set
lim ((X,H,x0) - (X,l,x0)) is V30() real ext-real Element of REAL
(X,(X,H,l),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (X,(X,H,l),x0) is V30() real ext-real Element of REAL
x0 /\ (dom (X,l,x0)) is Element of K19(X)
x0 /\ x0 is set
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) 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 set
(X,(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,H,l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
abs (X,H,l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,(X,H),l) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
- (X,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,H,l) is Relation-like X -defined Function-like V35() V36() V37() set
x0 is Element of X
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
abs (X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,(X,H),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
x0 is Element of X
dom (- (X,H,l)) is Element of K19(X)
K19(X) is set
dom (X,H,l) is Element of K19(X)
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(- (X,H,l)) . x0 is V30() real ext-real Element of REAL
(X,H,l) . x0 is V30() real ext-real Element of REAL
- ((X,H,l) . x0) is V30() real ext-real Element of REAL
lim (X,H,x0) is V30() real ext-real Element of REAL
- (lim (X,H,x0)) is V30() real ext-real Element of REAL
- (X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
K116(1) (#) (X,H,x0) is Relation-like NAT -defined Function-like total V35() V36() V37() set
lim (- (X,H,x0)) is V30() real ext-real Element of REAL
(X,(X,H),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (X,(X,H),x0) is V30() real ext-real Element of REAL
x0 is Element of X
dom (abs (X,H,l)) is Element of K19(X)
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(abs (X,H,l)) . x0 is V30() real ext-real Element of REAL
(X,H,l) . x0 is V30() real ext-real Element of REAL
abs ((X,H,l) . x0) is V30() real ext-real Element of REAL
lim (X,H,x0) is V30() real ext-real Element of REAL
abs (lim (X,H,x0)) is V30() real ext-real Element of REAL
abs (X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (abs (X,H,x0)) is V30() real ext-real Element of REAL
(X,(X,H),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (X,(X,H),x0) is V30() real ext-real Element of REAL
x0 is Element of X
(X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
- (X,H,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
K116(1) (#) (X,H,x0) is Relation-like NAT -defined Function-like total V35() V36() V37() set
(X,(X,H),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,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 set
(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,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
H (#) (X,l,x0) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
x0 is Element of X
dom (H (#) (X,l,x0)) is Element of K19(X)
K19(X) is set
dom (X,l,x0) is Element of K19(X)
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(H (#) (X,l,x0)) . x0 is V30() real ext-real Element of REAL
(X,l,x0) . x0 is V30() real ext-real Element of REAL
H * ((X,l,x0) . x0) is V30() real ext-real Element of REAL
lim (X,l,x0) is V30() real ext-real Element of REAL
H * (lim (X,l,x0)) is V30() real ext-real Element of REAL
H (#) (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (H (#) (X,l,x0)) is V30() real ext-real Element of REAL
(X,(X,l,H),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
lim (X,(X,l,H),x0) is V30() real ext-real Element of REAL
x0 is Element of X
(X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
H (#) (X,l,x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,REAL))
(X,(X,l,H),x0) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) V35() V36() V37() Element of K19(K20(NAT,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 set
(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
x0 is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
dom x0 is Element of K19(X)
K19(X) is set
x0 is Element of X
r is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
k1 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,k1) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
(X,REAL,H,k1) . x0 is V30() real ext-real Element of REAL
x0 . x0 is V30() real ext-real Element of REAL
((X,REAL,H,k1) . x0) - (x0 . x0) is V30() real ext-real Element of REAL
abs (((X,REAL,H,k1) . x0) - (x0 . x0)) is V30() real ext-real Element of REAL
x0 is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
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,H,r) is Relation-like X -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(X,REAL))
k is Element of X
(X,REAL,H,r) . k is V30() real ext-real Element of REAL
(X,H,l) . k is V30() real ext-real Element of REAL
((X,REAL,H,r) . k) - ((X,H,l) . k) is V30() real ext-real Element of REAL
abs (((X,REAL,H,r) . k) - ((X,H,l) . k)) is V30() real ext-real Element of REAL
dom (X,H,l) is Element of K19(X)
K19(X) is set
PFuncs (REAL,REAL) is functional non empty set
K20(NAT,(PFuncs (REAL,REAL))) is set
K19(K20(NAT,(PFuncs (REAL,REAL)))) is set
X is set
H is Relation-like NAT -defined PFuncs (REAL,REAL) -valued Function-like non empty total V18( NAT , PFuncs (REAL,REAL)) Element of K19(K20(NAT,(PFuncs (REAL,REAL))))
(REAL,H,X) is Relation-like REAL -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(REAL,REAL))
(REAL,H,X) | X is Relation-like REAL -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(REAL,REAL))
dom (REAL,H,X) is V47() V48() V49() Element of K19(REAL)
dom ((REAL,H,X) | X) is V47() V48() V49() Element of K19(REAL)
x0 is V30() real ext-real set
x0 is V30() real ext-real Element of REAL
((REAL,H,X) | X) . x0 is V30() real ext-real Element of REAL
r is V30() real ext-real set
r / 3 is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
r / 3 is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(REAL,H,X) . x0 is V30() real ext-real Element of REAL
k1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
max (k,k1) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V47() V48() V49() V50() V51() V52() V64() V65() Element of NAT
(REAL,REAL,H,(max (k,k1))) is Relation-like REAL -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(REAL,REAL))
dom (REAL,REAL,H,(max (k,k1))) is V47() V48() V49() Element of K19(REAL)
(REAL,REAL,H,(max (k,k1))) | X is Relation-like REAL -defined REAL -valued Function-like V35() V36() V37() Element of K19(K20(REAL,REAL))
dom ((REAL,REAL,H,(max (k,k1))) | X) is V47() V48() V49() Element of K19(REAL)
(dom (REAL,REAL,H,(max (k,k1)))) /\ X is V47() V48() V49() Element of K19(REAL)
((REAL,REAL,H,(max (k,k1))) | X) . x0 is V30() real ext-real Element of REAL
s is V30() real ext-real set
s is V30() real ext-real Element of REAL
x1 is V30() real ext-real set
x1 - x0 is V30() real ext-real Element of REAL
abs (x1 - x0) is V30() real ext-real Element of REAL
((REAL,H,X) | X) . x1 is V30() real ext-real Element of REAL
(((REAL,H,X) | X) . x1) - (((REAL,H,X) | X) . x0) is V30() real ext-real Element of REAL
abs ((((REAL,H,X) | X) . x1) - (((REAL,H,X) | X) . x0)) is V30() real ext-real Element of REAL
(dom (REAL,H,X)) /\ X is V47() V48() V49() Element of K19(REAL)
((REAL,REAL,H,(max (k,k1))) | X) . x1 is V30() real ext-real Element of REAL
(((REAL,REAL,H,(max (k,k1))) | X) . x1) - (((REAL,REAL,H,(max (k,k1))) | X) . x0) is V30() real ext-real Element of REAL
abs ((((REAL,REAL,H,(max (k,k1))) | X) . x1) - (((REAL,REAL,H,(max (k,k1))) | X) . x0)) is V30() real ext-real Element of REAL
(REAL,REAL,H,(max (k,k1))) . x1 is V30() real ext-real Element of REAL
((REAL,REAL,H,(max (k,k1))) . x1) - (((REAL,REAL,H,(max (k,k1))) | X) . x0) is V30() real ext-real Element of REAL
abs (((REAL,REAL,H,(max (k,k1))) . x1) - (((REAL,REAL,H,(max (k,k1))) | X) . x0)) is V30() real ext-real Element of REAL
(REAL,REAL,H,(max (k,k1))) . x0 is V30() real ext-real Element of REAL
((REAL,REAL,H,(max (k,k1))) . x1) - ((REAL,REAL,H,(max (k,k1))) . x0) is V30() real ext-real Element of REAL
abs (((REAL,REAL,H,(max (k,k1))) . x1) - ((REAL,REAL,H,(max (k,k1))) . x0)) is V30() real ext-real Element of REAL
((REAL,REAL,H,(max (k,k1))) . x0) - ((REAL,H,X) . x0) is V30() real ext-real Element of REAL
abs (((REAL,REAL,H,(max (k,k1))) . x0) - ((REAL,H,X) . x0)) is V30() real ext-real Element of REAL
(((REAL,REAL,H,(max (k,k1))) . x1) - ((REAL,REAL,H,(max (k,k1))) . x0)) + (((REAL,REAL,H,(max (k,k1))) . x0) - ((REAL,H,X) . x0)) is V30() real ext-real Element of REAL
abs ((((REAL,REAL,H,(max (k,k1))) . x1) - ((REAL,REAL,H,(max (k,k1))) . x0)) + (((REAL,REAL,H,(max (k,k1))) . x0) - ((REAL,H,X) . x0))) is V30() real ext-real Element of REAL
(abs (((REAL,REAL,H,(max (k,k1))) . x1) - ((REAL,REAL,H,(max (k,k1))) . x0))) + (abs (((REAL,REAL,H,(max (k,k1))) . x0) - ((REAL,H,X) . x0))) is V30() real ext-real Element of REAL
(r / 3) + (r / 3) is V30() real ext-real Element of REAL
(REAL,H,X) . x1 is V30() real ext-real Element of REAL
((REAL,H,X) . x1) - ((REAL,H,X) . x0) is V30() real ext-real Element of REAL
abs (((REAL,H,X) . x1) - ((REAL,H,X) . x0)) is V30() real ext-real Element of REAL
((REAL,H,X) . x1) - ((REAL,REAL,H,(max (k,k1))) . x1) is V30() real ext-real Element of REAL
(((REAL,H,X) . x1) - ((REAL,REAL,H,(max (k,k1))) . x1)) + ((((REAL,REAL,H,(max (k,k1))) . x1) - ((REAL,REAL,H,(max (k,k1))) . x0)) + (((REAL,REAL,H,(max (k,k1))) . x0) - ((REAL,H,X) . x0))) is V30() real ext-real Element of REAL
abs ((((REAL,H,X) . x1) - ((REAL,REAL,H,(max (k,k1))) . x1)) + ((((REAL,REAL,H,(max (k,k1))) . x1) - ((REAL,REAL,H,(max (k,k1))) . x0)) + (((REAL,REAL,H,(max (k,k1))) . x0) - ((REAL,H,X) . x0)))) is V30() real ext-real Element of REAL
abs (((REAL,H,X) . x1) - ((REAL,REAL,H,(max (k,k1))) . x1)) is V30() real ext-real Element of REAL
(abs (((REAL,H,X) . x1) - ((REAL,REAL,H,(max (k,k1))) . x1))) + (abs ((((REAL,REAL,H,(max (k,k1))) . x1) - ((REAL,REAL,H,(max (k,k1))) . x0)) + (((REAL,REAL,H,(max (k,k1))) . x0) - ((REAL,H,X) . x0)))) is V30() real ext-real Element of REAL
((REAL,REAL,H,(max (k,k1))) . x1) - ((REAL,H,X) . x1) is V30() real ext-real Element of REAL
abs (((REAL,REAL,H,(max (k,k1))) . x1) - ((REAL,H,X) . x1)) is V30() real ext-real Element of REAL
- (((REAL,H,X) . x1) - ((REAL,REAL,H,(max (k,k1))) . x1)) is V30() real ext-real Element of REAL
abs (- (((REAL,H,X) . x1) - ((REAL,REAL,H,(max (k,k1))) . x1))) is V30() real ext-real Element of REAL
(r / 3) + ((r / 3) + (r / 3)) is V30() real ext-real Element of REAL
((r / 3) + (r / 3)) + (r / 3) is V30() real ext-real Element of REAL
(((REAL,H,X) | X) . x1) - ((REAL,H,X) . x0) is V30() real ext-real Element of REAL
abs ((((REAL,H,X) | X) . x1) - ((REAL,H,X) . x0)) is V30() real ext-real Element of REAL