:: HEINE semantic presentation

REAL is non empty non trivial V51() V52() V53() V57() non finite set
NAT is non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() Element of K10(REAL)
K10(REAL) is non empty set
COMPLEX is non empty non trivial V51() V57() non finite set
RAT is non empty non trivial V51() V52() V53() V54() V57() non finite set
INT is non empty non trivial V51() V52() V53() V54() V55() V57() non finite set
omega is non empty epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() set
K10(omega) is non empty set
K10(NAT) is non empty set
K11(COMPLEX,COMPLEX) is non empty complex-valued set
K10(K11(COMPLEX,COMPLEX)) is non empty set
K11(COMPLEX,REAL) is non empty complex-valued ext-real-valued real-valued set
K10(K11(COMPLEX,REAL)) is non empty set
K404() is TopStruct
the carrier of K404() is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V14() real ext-real positive non negative V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
K11(1,1) is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K10(K11(1,1)) is non empty set
K11(K11(1,1),1) is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K10(K11(K11(1,1),1)) is non empty set
K11(K11(1,1),REAL) is non empty complex-valued ext-real-valued real-valued set
K10(K11(K11(1,1),REAL)) is non empty set
K11(REAL,REAL) is non empty complex-valued ext-real-valued real-valued set
K11(K11(REAL,REAL),REAL) is non empty complex-valued ext-real-valued real-valued set
K10(K11(K11(REAL,REAL),REAL)) is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V14() real ext-real positive non negative V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
K11(2,2) is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K11(K11(2,2),REAL) is non empty complex-valued ext-real-valued real-valued set
K10(K11(K11(2,2),REAL)) is non empty set
RealSpace is non empty strict Reflexive discerning V146() triangle Discerning MetrStruct
R^1 is TopSpace-like TopStruct
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V56() V57() finite V62() Element of NAT
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real ext-real non positive non negative V51() V52() V53() V54() V55() V56() V57() finite V62() set
K11(NAT,REAL) is non empty complex-valued ext-real-valued real-valued set
K10(K11(NAT,REAL)) is non empty set
real_dist is non empty Relation-like K11(REAL,REAL) -defined REAL -valued V24() V29(K11(REAL,REAL)) V33(K11(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(K11(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
K11(NAT,NAT) is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K10(K11(NAT,NAT)) is non empty set
a is V14() real ext-real set
b is V14() real ext-real set
a - b is V14() real ext-real set
- b is V14() real ext-real set
a + (- b) is V14() real ext-real set
abs (a - b) is V14() real ext-real Element of REAL
M is Reflexive discerning V146() triangle SubSpace of RealSpace
the carrier of M is set
a is Element of the carrier of M
b is Element of the carrier of M
dist (a,b) is V14() real ext-real Element of REAL
the distance of M is Relation-like K11( the carrier of M, the carrier of M) -defined REAL -valued V24() V29(K11( the carrier of M, the carrier of M)) V33(K11( the carrier of M, the carrier of M), REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(K11( the carrier of M, the carrier of M),REAL))
K11( the carrier of M, the carrier of M) is set
K11(K11( the carrier of M, the carrier of M),REAL) is complex-valued ext-real-valued real-valued set
K10(K11(K11( the carrier of M, the carrier of M),REAL)) is non empty set
the distance of M . (a,b) is set
real_dist . (a,b) is set
a is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
b is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
rng b is V51() V52() V53() set
b . a is V14() real ext-real Element of REAL
M is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
b . M is V14() real ext-real Element of REAL
M + 1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
b . (M + 1) is V14() real ext-real Element of REAL
dom b is V51() V52() V53() V54() V55() V56() set
a is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
dom b is V51() V52() V53() V54() V55() V56() set
b . 0 is V14() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
a is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
M is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
a is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
b is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
K77(M,b) is V14() real ext-real set
K77(a,b) is V14() real ext-real set
M . b is V14() real ext-real Element of REAL
a . b is V14() real ext-real Element of REAL
b to_power (a . b) is V14() real ext-real Element of REAL
a . b is V14() real ext-real Element of REAL
a is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
(a,2) is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
b is V14() real ext-real Element of REAL
M is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(a,2) . b is V14() real ext-real Element of REAL
a . b is V14() real ext-real Element of REAL
2 to_power (a . b) is V14() real ext-real Element of REAL
2 to_power M is V14() real ext-real Element of REAL
2 |^ M is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
a is V14() real ext-real set
b is V14() real ext-real set
Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like SubSpace of R^1
Closed-Interval-MSpace (a,b) is non empty strict Reflexive discerning V146() triangle Discerning SubSpace of RealSpace
b is V14() real ext-real Element of REAL
a is V14() real ext-real Element of REAL
b - a is V14() real ext-real Element of REAL
- a is V14() real ext-real set
b + (- a) is V14() real ext-real set
[.a,b.] is V51() V52() V53() Element of K10(REAL)
{a} is non empty V51() V52() V53() finite set
Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like SubSpace of R^1
the carrier of (Closed-Interval-TSpace (a,b)) is set
TopSpaceMetr (Closed-Interval-MSpace (a,b)) is TopStruct
Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like SubSpace of R^1
the carrier of (Closed-Interval-MSpace (a,b)) is set
K10( the carrier of (Closed-Interval-MSpace (a,b))) is non empty set
K10(K10( the carrier of (Closed-Interval-MSpace (a,b)))) is non empty set
F is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
f is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
f + 1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (f + 1) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (f + 1)) is V14() real ext-real Element of REAL
(2 |^ (f + 1)) " is V14() real ext-real set
(b - a) * ((2 |^ (f + 1)) ") is V14() real ext-real set
f + 2 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (f + 2) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (f + 2)) is V14() real ext-real Element of REAL
(2 |^ (f + 2)) " is V14() real ext-real set
(b - a) * ((2 |^ (f + 2)) ") is V14() real ext-real set
f is V14() real ext-real Element of REAL
f - ((b - a) / (2 |^ (f + 1))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (f + 1))) is V14() real ext-real set
f + (- ((b - a) / (2 |^ (f + 1)))) is V14() real ext-real set
[.(f - ((b - a) / (2 |^ (f + 1)))),f.] is V51() V52() V53() Element of K10(REAL)
f - ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (f + 2))) is V14() real ext-real set
f + (- ((b - a) / (2 |^ (f + 2)))) is V14() real ext-real set
f + ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
s is V14() real ext-real Element of REAL
ls is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union ls is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
s is V14() real ext-real Element of REAL
ls is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union ls is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
Nseq is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union Nseq is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
s is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union s is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
ls is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union ls is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
s is V14() real ext-real Element of REAL
a + b is V14() real ext-real Element of REAL
(a + b) / 2 is V14() real ext-real Element of REAL
2 " is non empty V14() real ext-real positive non negative set
(a + b) * (2 ") is V14() real ext-real set
f is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
f . 0 is V14() real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V14() real ext-real positive non negative V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (0 + 1)) is V14() real ext-real Element of REAL
(2 |^ (0 + 1)) " is V14() real ext-real set
(b - a) * ((2 |^ (0 + 1)) ") is V14() real ext-real set
(f . 0) + ((b - a) / (2 |^ (0 + 1))) is V14() real ext-real Element of REAL
(b - a) / 2 is V14() real ext-real Element of REAL
(b - a) * (2 ") is V14() real ext-real set
((a + b) / 2) + ((b - a) / 2) is V14() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
f + 1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
f . (f + 1) is V14() real ext-real Element of REAL
f . f is V14() real ext-real Element of REAL
f + 2 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (f + 2) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (f + 2)) is V14() real ext-real Element of REAL
(2 |^ (f + 2)) " is V14() real ext-real set
(b - a) * ((2 |^ (f + 2)) ") is V14() real ext-real set
(f . f) + ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
(f . f) - ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (f + 2))) is V14() real ext-real set
(f . f) + (- ((b - a) / (2 |^ (f + 2)))) is V14() real ext-real set
2 |^ (f + 1) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (f + 1)) is V14() real ext-real Element of REAL
(2 |^ (f + 1)) " is V14() real ext-real set
(b - a) * ((2 |^ (f + 1)) ") is V14() real ext-real set
(f . f) - ((b - a) / (2 |^ (f + 1))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (f + 1))) is V14() real ext-real set
(f . f) + (- ((b - a) / (2 |^ (f + 1)))) is V14() real ext-real set
[.((f . f) - ((b - a) / (2 |^ (f + 1)))),(f . f).] is V51() V52() V53() Element of K10(REAL)
s is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union s is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
s is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union s is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
f is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
f . f is V14() real ext-real Element of REAL
f + 1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (f + 1) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (f + 1)) is V14() real ext-real Element of REAL
(2 |^ (f + 1)) " is V14() real ext-real set
(b - a) * ((2 |^ (f + 1)) ") is V14() real ext-real set
(f . f) - ((b - a) / (2 |^ (f + 1))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (f + 1))) is V14() real ext-real set
(f . f) + (- ((b - a) / (2 |^ (f + 1)))) is V14() real ext-real set
(f . f) + ((b - a) / (2 |^ (f + 1))) is V14() real ext-real Element of REAL
f . (f + 1) is V14() real ext-real Element of REAL
(f + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ ((f + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ ((f + 1) + 1)) is V14() real ext-real Element of REAL
(2 |^ ((f + 1) + 1)) " is V14() real ext-real set
(b - a) * ((2 |^ ((f + 1) + 1)) ") is V14() real ext-real set
(f . (f + 1)) - ((b - a) / (2 |^ ((f + 1) + 1))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ ((f + 1) + 1))) is V14() real ext-real set
(f . (f + 1)) + (- ((b - a) / (2 |^ ((f + 1) + 1)))) is V14() real ext-real set
(f . (f + 1)) + ((b - a) / (2 |^ ((f + 1) + 1))) is V14() real ext-real Element of REAL
2 * (2 |^ (f + 1)) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 * (2 |^ (f + 1))) is V14() real ext-real Element of REAL
(2 * (2 |^ (f + 1))) " is V14() real ext-real set
(b - a) * ((2 * (2 |^ (f + 1))) ") is V14() real ext-real set
((b - a) / (2 * (2 |^ (f + 1)))) + ((b - a) / (2 * (2 |^ (f + 1)))) is V14() real ext-real Element of REAL
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V14() real ext-real positive non negative V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
f + (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (f + (1 + 1)) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (f + (1 + 1))) is V14() real ext-real Element of REAL
(2 |^ (f + (1 + 1))) " is V14() real ext-real set
(b - a) * ((2 |^ (f + (1 + 1))) ") is V14() real ext-real set
((b - a) / (2 |^ (f + 1))) - ((b - a) / (2 |^ (f + (1 + 1)))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (f + (1 + 1)))) is V14() real ext-real set
((b - a) / (2 |^ (f + 1))) + (- ((b - a) / (2 |^ (f + (1 + 1))))) is V14() real ext-real set
((b - a) / (2 |^ (f + 1))) - ((b - a) / (2 |^ ((f + 1) + 1))) is V14() real ext-real Element of REAL
((b - a) / (2 |^ (f + 1))) + (- ((b - a) / (2 |^ ((f + 1) + 1)))) is V14() real ext-real set
((b - a) / (2 |^ (f + 1))) - ((b - a) / (2 * (2 |^ (f + 1)))) is V14() real ext-real Element of REAL
- ((b - a) / (2 * (2 |^ (f + 1)))) is V14() real ext-real set
((b - a) / (2 |^ (f + 1))) + (- ((b - a) / (2 * (2 |^ (f + 1))))) is V14() real ext-real set
b - (f . f) is V14() real ext-real Element of REAL
- (f . f) is V14() real ext-real set
b + (- (f . f)) is V14() real ext-real set
(f . f) - a is V14() real ext-real Element of REAL
(f . f) + (- a) is V14() real ext-real set
f + 2 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (f + 2) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (f + 2)) is V14() real ext-real Element of REAL
(2 |^ (f + 2)) " is V14() real ext-real set
(b - a) * ((2 |^ (f + 2)) ") is V14() real ext-real set
(f . f) + ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
(f . (f + 1)) - a is V14() real ext-real Element of REAL
(f . (f + 1)) + (- a) is V14() real ext-real set
((f . f) - a) + ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
b - (f . (f + 1)) is V14() real ext-real Element of REAL
- (f . (f + 1)) is V14() real ext-real set
b + (- (f . (f + 1))) is V14() real ext-real set
(b - (f . f)) - ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (f + 2))) is V14() real ext-real set
(b - (f . f)) + (- ((b - a) / (2 |^ (f + 2)))) is V14() real ext-real set
f + 2 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (f + 2) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (f + 2)) is V14() real ext-real Element of REAL
(2 |^ (f + 2)) " is V14() real ext-real set
(b - a) * ((2 |^ (f + 2)) ") is V14() real ext-real set
(f . f) - ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (f + 2))) is V14() real ext-real set
(f . f) + (- ((b - a) / (2 |^ (f + 2)))) is V14() real ext-real set
(f . (f + 1)) - a is V14() real ext-real Element of REAL
(f . (f + 1)) + (- a) is V14() real ext-real set
((f . f) - a) - ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
((f . f) - a) + (- ((b - a) / (2 |^ (f + 2)))) is V14() real ext-real set
b - (f . (f + 1)) is V14() real ext-real Element of REAL
- (f . (f + 1)) is V14() real ext-real set
b + (- (f . (f + 1))) is V14() real ext-real set
(b - (f . f)) + ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
f + 2 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (f + 2) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (f + 2)) is V14() real ext-real Element of REAL
(2 |^ (f + 2)) " is V14() real ext-real set
(b - a) * ((2 |^ (f + 2)) ") is V14() real ext-real set
(f . f) + ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
(f . f) - ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (f + 2))) is V14() real ext-real set
(f . f) + (- ((b - a) / (2 |^ (f + 2)))) is V14() real ext-real set
(f . 0) - ((b - a) / (2 |^ (0 + 1))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (0 + 1))) is V14() real ext-real set
(f . 0) + (- ((b - a) / (2 |^ (0 + 1)))) is V14() real ext-real set
((a + b) / 2) - ((b - a) / 2) is V14() real ext-real Element of REAL
- ((b - a) / 2) is V14() real ext-real set
((a + b) / 2) + (- ((b - a) / 2)) is V14() real ext-real set
rng f is V51() V52() V53() set
[.a,b.] is V51() V52() V53() Element of K10(REAL)
f is set
dom f is V51() V52() V53() V54() V55() V56() set
s is set
f . s is V14() real ext-real Element of REAL
ls is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
ls + 1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (ls + 1) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
f . ls is V14() real ext-real Element of REAL
(b - a) / (2 |^ (ls + 1)) is V14() real ext-real Element of REAL
(2 |^ (ls + 1)) " is V14() real ext-real set
(b - a) * ((2 |^ (ls + 1)) ") is V14() real ext-real set
(f . ls) + ((b - a) / (2 |^ (ls + 1))) is V14() real ext-real Element of REAL
(f . ls) - ((b - a) / (2 |^ (ls + 1))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (ls + 1))) is V14() real ext-real set
(f . ls) + (- ((b - a) / (2 |^ (ls + 1)))) is V14() real ext-real set
{ b₁ where b₁ is V14() real ext-real Element of REAL : ( a <= b₁ & b₁ <= b ) } is set
f is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
f . f is V14() real ext-real Element of REAL
f + 1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (f + 1) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (f + 1)) is V14() real ext-real Element of REAL
(2 |^ (f + 1)) " is V14() real ext-real set
(b - a) * ((2 |^ (f + 1)) ") is V14() real ext-real set
(f . f) - ((b - a) / (2 |^ (f + 1))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (f + 1))) is V14() real ext-real set
(f . f) + (- ((b - a) / (2 |^ (f + 1)))) is V14() real ext-real set
(f . f) + ((b - a) / (2 |^ (f + 1))) is V14() real ext-real Element of REAL
[.((f . f) - ((b - a) / (2 |^ (f + 1)))),((f . f) + ((b - a) / (2 |^ (f + 1)))).] is V51() V52() V53() Element of K10(REAL)
f . (f + 1) is V14() real ext-real Element of REAL
(f + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ ((f + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ ((f + 1) + 1)) is V14() real ext-real Element of REAL
(2 |^ ((f + 1) + 1)) " is V14() real ext-real set
(b - a) * ((2 |^ ((f + 1) + 1)) ") is V14() real ext-real set
(f . (f + 1)) - ((b - a) / (2 |^ ((f + 1) + 1))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ ((f + 1) + 1))) is V14() real ext-real set
(f . (f + 1)) + (- ((b - a) / (2 |^ ((f + 1) + 1)))) is V14() real ext-real set
(f . (f + 1)) + ((b - a) / (2 |^ ((f + 1) + 1))) is V14() real ext-real Element of REAL
[.((f . (f + 1)) - ((b - a) / (2 |^ ((f + 1) + 1)))),((f . (f + 1)) + ((b - a) / (2 |^ ((f + 1) + 1)))).] is V51() V52() V53() Element of K10(REAL)
s is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union s is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V14() real ext-real positive non negative V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
f + (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (f + (1 + 1)) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (f + (1 + 1))) is V14() real ext-real Element of REAL
(2 |^ (f + (1 + 1))) " is V14() real ext-real set
(b - a) * ((2 |^ (f + (1 + 1))) ") is V14() real ext-real set
(2 |^ (f + 1)) * 2 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / ((2 |^ (f + 1)) * 2) is V14() real ext-real Element of REAL
((2 |^ (f + 1)) * 2) " is V14() real ext-real set
(b - a) * (((2 |^ (f + 1)) * 2) ") is V14() real ext-real set
((b - a) / (2 |^ (f + 1))) / 2 is V14() real ext-real Element of REAL
((b - a) / (2 |^ (f + 1))) * (2 ") is V14() real ext-real set
[.((f . f) - ((b - a) / (2 |^ (f + 1)))),(f . f).] is V51() V52() V53() Element of K10(REAL)
[.(f . f),((f . f) + ((b - a) / (2 |^ (f + 1)))).] is V51() V52() V53() Element of K10(REAL)
[.((f . f) - ((b - a) / (2 |^ (f + 1)))),(f . f).] \/ [.(f . f),((f . f) + ((b - a) / (2 |^ (f + 1)))).] is V51() V52() V53() Element of K10(REAL)
f + 2 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (f + 2) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (f + 2)) is V14() real ext-real Element of REAL
(2 |^ (f + 2)) " is V14() real ext-real set
(b - a) * ((2 |^ (f + 2)) ") is V14() real ext-real set
(f . f) + ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
((f . f) + ((b - a) / (2 |^ (f + 2)))) - ((b - a) / (2 |^ (f + (1 + 1)))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (f + (1 + 1)))) is V14() real ext-real set
((f . f) + ((b - a) / (2 |^ (f + 2)))) + (- ((b - a) / (2 |^ (f + (1 + 1))))) is V14() real ext-real set
ls is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union ls is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
ls is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union ls is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
ls is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union ls is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
ls \/ s is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
((f . f) + ((b - a) / (2 |^ (f + 2)))) + ((b - a) / (2 |^ (f + (1 + 1)))) is V14() real ext-real Element of REAL
(f . f) + (((b - a) / (2 |^ (f + 1))) / 2) is V14() real ext-real Element of REAL
((f . f) + (((b - a) / (2 |^ (f + 1))) / 2)) + (((b - a) / (2 |^ (f + 1))) / 2) is V14() real ext-real Element of REAL
Z is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union Z is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
(union ls) \/ (union s) is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
Nseq is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union Nseq is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
[.((f . f) - ((b - a) / (2 |^ (f + 1)))),(f . f).] is V51() V52() V53() Element of K10(REAL)
f + 2 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ (f + 2) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(b - a) / (2 |^ (f + 2)) is V14() real ext-real Element of REAL
(2 |^ (f + 2)) " is V14() real ext-real set
(b - a) * ((2 |^ (f + 2)) ") is V14() real ext-real set
(f . f) - ((b - a) / (2 |^ (f + 2))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (f + 2))) is V14() real ext-real set
(f . f) + (- ((b - a) / (2 |^ (f + 2)))) is V14() real ext-real set
((f . f) - ((b - a) / (2 |^ (f + 2)))) + ((b - a) / (2 |^ (f + (1 + 1)))) is V14() real ext-real Element of REAL
((f . f) - ((b - a) / (2 |^ (f + 2)))) - ((b - a) / (2 |^ (f + (1 + 1)))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ (f + (1 + 1)))) is V14() real ext-real set
((f . f) - ((b - a) / (2 |^ (f + 2)))) + (- ((b - a) / (2 |^ (f + (1 + 1))))) is V14() real ext-real set
(f . f) - (((b - a) / (2 |^ (f + 1))) / 2) is V14() real ext-real Element of REAL
- (((b - a) / (2 |^ (f + 1))) / 2) is V14() real ext-real set
(f . f) + (- (((b - a) / (2 |^ (f + 1))) / 2)) is V14() real ext-real set
((f . f) - (((b - a) / (2 |^ (f + 1))) / 2)) - (((b - a) / (2 |^ (f + 1))) / 2) is V14() real ext-real Element of REAL
((f . f) - (((b - a) / (2 |^ (f + 1))) / 2)) + (- (((b - a) / (2 |^ (f + 1))) / 2)) is V14() real ext-real set
[.((f . f) - ((b - a) / (2 |^ (f + 1)))),(f . f).] is V51() V52() V53() Element of K10(REAL)
ls is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union ls is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
[.((f . 0) - ((b - a) / (2 |^ (0 + 1)))),((f . 0) + ((b - a) / (2 |^ (0 + 1)))).] is V51() V52() V53() Element of K10(REAL)
f is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
union f is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
f is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
s is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
lim s is V14() real ext-real Element of REAL
Nseq is non empty Relation-like NAT -defined NAT -valued V24() V29( NAT ) V33( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K10(K11(NAT,NAT))
f * Nseq is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of f
union F is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
Z is set
p is Element of the carrier of (Closed-Interval-MSpace (a,b))
r0 is V14() real ext-real Element of REAL
Ball (p,r0) is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
{(Ball (p,r0))} is non empty finite set
bool the carrier of (Closed-Interval-MSpace (a,b)) is non empty Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
G is set
G is Element of K10(K10( the carrier of (Closed-Interval-MSpace (a,b))))
Ns is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
r1 is V14() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
rng Nseq is V51() V52() V53() V54() V55() V56() set
Ns . n is V14() real ext-real Element of REAL
(Ns,2) is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
(Ns,2) " is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
ls is Element of the carrier of (Closed-Interval-MSpace (a,b))
r1 is V14() real ext-real Element of REAL
Ball (ls,r1) is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
r1 / 2 is V14() real ext-real Element of REAL
r1 * (2 ") is V14() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
s . i is V14() real ext-real Element of REAL
l is Element of the carrier of (Closed-Interval-MSpace (a,b))
dist (ls,l) is V14() real ext-real Element of REAL
(s . i) - (lim s) is V14() real ext-real Element of REAL
- (lim s) is V14() real ext-real set
(s . i) + (- (lim s)) is V14() real ext-real set
abs ((s . i) - (lim s)) is V14() real ext-real Element of REAL
- ((s . i) - (lim s)) is V14() real ext-real Element of REAL
abs (- ((s . i) - (lim s))) is V14() real ext-real Element of REAL
the distance of (Closed-Interval-MSpace (a,b)) is Relation-like K11( the carrier of (Closed-Interval-MSpace (a,b)), the carrier of (Closed-Interval-MSpace (a,b))) -defined REAL -valued V24() V29(K11( the carrier of (Closed-Interval-MSpace (a,b)), the carrier of (Closed-Interval-MSpace (a,b)))) V33(K11( the carrier of (Closed-Interval-MSpace (a,b)), the carrier of (Closed-Interval-MSpace (a,b))), REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(K11( the carrier of (Closed-Interval-MSpace (a,b)), the carrier of (Closed-Interval-MSpace (a,b))),REAL))
K11( the carrier of (Closed-Interval-MSpace (a,b)), the carrier of (Closed-Interval-MSpace (a,b))) is set
K11(K11( the carrier of (Closed-Interval-MSpace (a,b)), the carrier of (Closed-Interval-MSpace (a,b))),REAL) is complex-valued ext-real-valued real-valued set
K10(K11(K11( the carrier of (Closed-Interval-MSpace (a,b)), the carrier of (Closed-Interval-MSpace (a,b))),REAL)) is non empty set
the distance of (Closed-Interval-MSpace (a,b)) . ((lim s),(s . i)) is set
the distance of RealSpace is Relation-like K11( the carrier of RealSpace, the carrier of RealSpace) -defined REAL -valued V24() V29(K11( the carrier of RealSpace, the carrier of RealSpace)) V33(K11( the carrier of RealSpace, the carrier of RealSpace), REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(K11( the carrier of RealSpace, the carrier of RealSpace),REAL))
the carrier of RealSpace is set
K11( the carrier of RealSpace, the carrier of RealSpace) is set
K11(K11( the carrier of RealSpace, the carrier of RealSpace),REAL) is complex-valued ext-real-valued real-valued set
K10(K11(K11( the carrier of RealSpace, the carrier of RealSpace),REAL)) is non empty set
the distance of RealSpace . (ls,l) is set
(lim s) - (s . i) is V14() real ext-real Element of REAL
- (s . i) is V14() real ext-real set
(lim s) + (- (s . i)) is V14() real ext-real set
abs ((lim s) - (s . i)) is V14() real ext-real Element of REAL
Ball (ls,(r1 / 2)) is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
i is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(f * Nseq) . i is V14() real ext-real Element of REAL
dom f is V51() V52() V53() V54() V55() V56() set
s . i is V14() real ext-real Element of REAL
Nseq . i is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
f . (Nseq . i) is V14() real ext-real Element of REAL
rng f is V51() V52() V53() set
l is Element of the carrier of (Closed-Interval-MSpace (a,b))
dist (ls,l) is V14() real ext-real Element of REAL
lim ((Ns,2) ") is V14() real ext-real Element of REAL
(b - a) (#) ((Ns,2) ") is non empty Relation-like NAT -defined REAL -valued V24() V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
lim ((b - a) (#) ((Ns,2) ")) is V14() real ext-real Element of REAL
(b - a) * 0 is V14() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
i + 1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(i + 1) + n is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(n + 1) + i is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
s . ((i + 1) + n) is V14() real ext-real Element of REAL
Nseq . ((i + 1) + n) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(Nseq . ((i + 1) + n)) + 1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 |^ ((Nseq . ((i + 1) + n)) + 1) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(2 |^ ((Nseq . ((i + 1) + n)) + 1)) " is V14() real ext-real Element of REAL
(b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") is V14() real ext-real Element of REAL
(s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) is V14() real ext-real Element of REAL
- ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) is V14() real ext-real set
(s . ((i + 1) + n)) + (- ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))) is V14() real ext-real set
(s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) is V14() real ext-real Element of REAL
[.((s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))).] is V51() V52() V53() Element of K10(REAL)
((b - a) (#) ((Ns,2) ")) . ((i + 1) + n) is V14() real ext-real Element of REAL
(((b - a) (#) ((Ns,2) ")) . ((i + 1) + n)) - 0 is V14() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real ext-real non positive non negative V51() V52() V53() V54() V55() V56() V57() finite V62() set
(((b - a) (#) ((Ns,2) ")) . ((i + 1) + n)) + (- 0) is V14() real ext-real set
abs ((((b - a) (#) ((Ns,2) ")) . ((i + 1) + n)) - 0) is V14() real ext-real Element of REAL
((Ns,2) ") . ((i + 1) + n) is V14() real ext-real Element of REAL
(b - a) * (((Ns,2) ") . ((i + 1) + n)) is V14() real ext-real Element of REAL
abs ((b - a) * (((Ns,2) ") . ((i + 1) + n))) is V14() real ext-real Element of REAL
(Ns,2) . ((i + 1) + n) is V14() real ext-real Element of REAL
((Ns,2) . ((i + 1) + n)) " is V14() real ext-real Element of REAL
(b - a) * (((Ns,2) . ((i + 1) + n)) ") is V14() real ext-real Element of REAL
abs ((b - a) * (((Ns,2) . ((i + 1) + n)) ")) is V14() real ext-real Element of REAL
Ns . ((i + 1) + n) is V14() real ext-real Element of REAL
2 to_power (Ns . ((i + 1) + n)) is V14() real ext-real Element of REAL
(2 to_power (Ns . ((i + 1) + n))) " is V14() real ext-real Element of REAL
(b - a) * ((2 to_power (Ns . ((i + 1) + n))) ") is V14() real ext-real Element of REAL
abs ((b - a) * ((2 to_power (Ns . ((i + 1) + n))) ")) is V14() real ext-real Element of REAL
2 |^ (Nseq . ((i + 1) + n)) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
(2 |^ (Nseq . ((i + 1) + n))) " is V14() real ext-real Element of REAL
(b - a) * ((2 |^ (Nseq . ((i + 1) + n))) ") is V14() real ext-real Element of REAL
abs ((b - a) * ((2 |^ (Nseq . ((i + 1) + n))) ")) is V14() real ext-real Element of REAL
2 * (2 |^ (Nseq . ((i + 1) + n))) is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
1 / (2 |^ ((Nseq . ((i + 1) + n)) + 1)) is V14() real ext-real Element of REAL
(2 |^ ((Nseq . ((i + 1) + n)) + 1)) " is V14() real ext-real set
1 * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") is V14() real ext-real set
abs ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) is V14() real ext-real Element of REAL
sl is Element of the carrier of (Closed-Interval-MSpace (a,b))
dist (ls,sl) is V14() real ext-real Element of REAL
(lim s) - (s . ((i + 1) + n)) is V14() real ext-real Element of REAL
- (s . ((i + 1) + n)) is V14() real ext-real set
(lim s) + (- (s . ((i + 1) + n))) is V14() real ext-real set
abs ((lim s) - (s . ((i + 1) + n))) is V14() real ext-real Element of REAL
z is set
{ b₁ where b₁ is V14() real ext-real Element of REAL : ( (s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) <= b₁ & b₁ <= (s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) ) } is set
x is V14() real ext-real Element of REAL
f . (Nseq . ((i + 1) + n)) is V14() real ext-real Element of REAL
(b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)) is V14() real ext-real Element of REAL
(b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") is V14() real ext-real set
(f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) is V14() real ext-real set
(f . (Nseq . ((i + 1) + n))) + (- ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))) is V14() real ext-real set
(f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) is V14() real ext-real Element of REAL
{ b₁ where b₁ is V14() real ext-real Element of REAL : ( a <= b₁ & b₁ <= b ) } is set
(lim s) - x is V14() real ext-real Element of REAL
- x is V14() real ext-real set
(lim s) + (- x) is V14() real ext-real set
abs ((lim s) - x) is V14() real ext-real Element of REAL
(s . ((i + 1) + n)) - x is V14() real ext-real Element of REAL
(s . ((i + 1) + n)) + (- x) is V14() real ext-real set
((lim s) - (s . ((i + 1) + n))) + ((s . ((i + 1) + n)) - x) is V14() real ext-real Element of REAL
abs (((lim s) - (s . ((i + 1) + n))) + ((s . ((i + 1) + n)) - x)) is V14() real ext-real Element of REAL
abs ((s . ((i + 1) + n)) - x) is V14() real ext-real Element of REAL
(abs ((lim s) - (s . ((i + 1) + n)))) + (abs ((s . ((i + 1) + n)) - x)) is V14() real ext-real Element of REAL
x - (s . ((i + 1) + n)) is V14() real ext-real Element of REAL
x + (- (s . ((i + 1) + n))) is V14() real ext-real set
- ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) is V14() real ext-real Element of REAL
- (x - (s . ((i + 1) + n))) is V14() real ext-real Element of REAL
((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) + x is V14() real ext-real Element of REAL
(r1 / 2) + (r1 / 2) is V14() real ext-real Element of REAL
x9 is Element of the carrier of (Closed-Interval-MSpace (a,b))
dist (ls,x9) is V14() real ext-real Element of REAL
(b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)) is V14() real ext-real Element of REAL
(2 |^ ((Nseq . ((i + 1) + n)) + 1)) " is V14() real ext-real set
(b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") is V14() real ext-real set
(s . ((i + 1) + n)) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) is V14() real ext-real Element of REAL
- ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) is V14() real ext-real set
(s . ((i + 1) + n)) + (- ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))) is V14() real ext-real set
[.((s . ((i + 1) + n)) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))).] is V51() V52() V53() Element of K10(REAL)
f . (Nseq . ((i + 1) + n)) is V14() real ext-real Element of REAL
(f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) is V14() real ext-real Element of REAL
(f . (Nseq . ((i + 1) + n))) + (- ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))) is V14() real ext-real set
(s . ((i + 1) + n)) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) is V14() real ext-real Element of REAL
[.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((s . ((i + 1) + n)) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] is V51() V52() V53() Element of K10(REAL)
(f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) is V14() real ext-real Element of REAL
[.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] is V51() V52() V53() Element of K10(REAL)
union G is Element of K10( the carrier of (Closed-Interval-MSpace (a,b)))
Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like SubSpace of R^1
Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like SubSpace of R^1