REAL is non empty V36() V37() V38() V42() V43() set
NAT is V36() V37() V38() V39() V40() V41() V42() Element of bool REAL
bool REAL is non empty set
NAT is V36() V37() V38() V39() V40() V41() V42() set
bool NAT is non empty set
[:NAT,REAL:] is set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
COMPLEX is non empty V36() V42() V43() set
bool NAT is non empty set
{} is empty V36() V37() V38() V39() V40() V41() V42() set
the empty V36() V37() V38() V39() V40() V41() V42() set is empty V36() V37() V38() V39() V40() V41() V42() set
1 is non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() Element of NAT
0 is empty V26() V27() V28() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() V68() Element of NAT
2 is non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() Element of NAT
T is V26() V27() V28() ext-real set
2 |^ T is V26() V27() V28() ext-real Element of REAL
A is V36() V37() V38() Element of bool REAL
A is V36() V37() V38() Element of bool REAL
B is V36() V37() V38() Element of bool REAL
n is set
G is V27() V28() ext-real Element of REAL
S is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
S / (2 |^ T) is V27() V28() ext-real Element of REAL
G is V27() V28() ext-real Element of REAL
S is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
S / (2 |^ T) is V27() V28() ext-real Element of REAL
T is V36() V37() V38() Element of bool REAL
T is V36() V37() V38() Element of bool REAL
A is V36() V37() V38() Element of bool REAL
B is set
n is V27() V28() ext-real Element of REAL
G is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G) is V36() V37() V38() Element of bool REAL
n is V27() V28() ext-real Element of REAL
G is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G) is V36() V37() V38() Element of bool REAL
() is V36() V37() V38() Element of bool REAL
halfline 0 is V36() V37() V38() Element of bool REAL
-infty is non empty V28() ext-real non positive negative set
K165(-infty,0) is set
(halfline 0) \/ () is V36() V37() V38() Element of bool REAL
right_open_halfline 1 is V36() V37() V38() Element of bool REAL
+infty is non empty V28() ext-real positive non negative set
K165(1,+infty) is set
((halfline 0) \/ ()) \/ (right_open_halfline 1) is V36() V37() V38() Element of bool REAL
() is V36() V37() V38() Element of bool REAL
A is non empty V36() V37() V38() Element of bool REAL
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
[:A,(bool the carrier of T):] is non empty set
bool [:A,(bool the carrier of T):] is non empty set
B is V10() V13(A) V14( bool the carrier of T) Function-like V33(A, bool the carrier of T) Element of bool [:A,(bool the carrier of T):]
n is V27() V28() ext-real Element of A
B . n is set
B . n is Element of bool the carrier of T
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T) is V36() V37() V38() Element of bool REAL
A is V27() V28() ext-real Element of REAL
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B / (2 |^ T) is V27() V28() ext-real Element of REAL
0 / (2 |^ T) is V27() V28() ext-real Element of REAL
(2 |^ T) / (2 |^ T) is V27() V28() ext-real Element of REAL
(0) is V36() V37() V38() Element of bool REAL
{0,1} is non empty V36() V37() V38() V39() V40() V41() Element of bool REAL
2 |^ 0 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
T is V27() V28() ext-real Element of REAL
A is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
A / 1 is V27() V28() ext-real Element of REAL
A is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
A / 1 is V27() V28() ext-real Element of REAL
A is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
T is set
A is V27() V28() ext-real Element of REAL
B is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
0 + 1 is non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() Element of NAT
(1) is V36() V37() V38() Element of bool REAL
1 / 2 is V27() V28() ext-real non negative Element of REAL
{0,(1 / 2),1} is non empty V36() V37() V38() Element of bool REAL
2 |^ 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
T is set
0 / 2 is empty V27() V28() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() Element of REAL
A is V27() V28() ext-real Element of REAL
2 / 2 is V27() V28() ext-real non negative Element of REAL
A is V27() V28() ext-real Element of REAL
B is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B / 2 is V27() V28() ext-real Element of REAL
1 + 1 is non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() Element of NAT
0 + 1 is non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() Element of NAT
T is V26() V27() V28() ext-real set
(T) is V36() V37() V38() Element of bool REAL
2 |^ T is V26() V27() V28() ext-real Element of REAL
0 / (2 |^ T) is V27() V28() ext-real Element of REAL
0 / (2 |^ T) is V27() V28() ext-real Element of REAL
B is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B / (2 |^ T) is V27() V28() ext-real Element of REAL
T is V26() V27() V28() ext-real set
2 |^ T is V26() V27() V28() ext-real Element of REAL
(2 |^ T) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
Seg ((2 |^ T) + 1) is V36() V37() V38() V39() V40() V41() Element of bool NAT
A is V10() Function-like FinSequence-like set
len A is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
dom A is V36() V37() V38() V39() V40() V41() Element of bool NAT
B is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
A . B is set
B - 1 is V27() V28() ext-real Element of REAL
(B - 1) / (2 |^ T) is V27() V28() ext-real Element of REAL
A is V10() Function-like FinSequence-like set
dom A is V36() V37() V38() V39() V40() V41() Element of bool NAT
B is V10() Function-like FinSequence-like set
dom B is V36() V37() V38() V39() V40() V41() Element of bool NAT
n is set
G is V26() V27() V28() ext-real set
A . G is set
B . G is set
G - 1 is V27() V28() ext-real Element of REAL
(G - 1) / (2 |^ T) is V27() V28() ext-real Element of REAL
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T) is V10() Function-like FinSequence-like set
dom (T) is V36() V37() V38() V39() V40() V41() Element of bool NAT
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 |^ T) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
Seg ((2 |^ T) + 1) is V36() V37() V38() V39() V40() V41() Element of bool NAT
rng (T) is set
(T) is non empty V36() V37() V38() Element of bool REAL
A is set
B is set
(T) . B is set
n is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n - 1 is V27() V28() ext-real Element of REAL
((2 |^ T) + 1) - 1 is V27() V28() ext-real Element of REAL
G is V26() V27() V28() ext-real set
1 + G is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(n - 1) / (2 |^ T) is V27() V28() ext-real Element of REAL
B is V27() V28() ext-real Element of REAL
n is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n / (2 |^ T) is V27() V28() ext-real Element of REAL
n + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
G is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
0 + 1 is non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() Element of NAT
G - 1 is V27() V28() ext-real Element of REAL
(G - 1) / (2 |^ T) is V27() V28() ext-real Element of REAL
(T) . G is set
T is set
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T) is non empty V36() V37() V38() Element of bool REAL
T + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((T + 1)) is non empty V36() V37() V38() Element of bool REAL
A is set
2 |^ (T + 1) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B is V27() V28() ext-real Element of REAL
n is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n / (2 |^ T) is V27() V28() ext-real Element of REAL
n * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(n * 2) / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
(2 |^ T) * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T) is non empty V36() V37() V38() Element of bool REAL
T + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((T + 1)) is non empty V36() V37() V38() Element of bool REAL
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T) is non empty V36() V37() V38() Element of bool REAL
A is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(A) is non empty V36() V37() V38() Element of bool REAL
A is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
A * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(A * 2) - 1 is V27() V28() ext-real Element of REAL
T + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
2 |^ (T + 1) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((A * 2) - 1) / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
((T + 1)) is non empty V36() V37() V38() Element of bool REAL
(T) is non empty V36() V37() V38() Element of bool REAL
((T + 1)) \ (T) is V36() V37() V38() Element of bool REAL
0 * 2 is empty V26() V27() V28() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() V68() Element of NAT
B is V26() V27() V28() ext-real set
B + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n / (2 |^ T) is V27() V28() ext-real Element of REAL
((A * 2) - 1) * (2 |^ T) is V27() V28() ext-real Element of REAL
n * (2 |^ (T + 1)) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 |^ T) * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n * ((2 |^ T) * 2) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(n * 2) * (2 |^ T) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((A * 2) - 1) / (2 |^ T) is V27() V28() ext-real Element of REAL
(n * 2) / (2 |^ T) is V27() V28() ext-real Element of REAL
- 1 is V27() V28() ext-real non positive Element of REAL
(A * 2) + (- 1) is V27() V28() ext-real Element of REAL
2 * A is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 * A) + 0 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
2 * n is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 * n) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 |^ T) * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
A is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
A * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(A * 2) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
T + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
2 |^ (T + 1) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((A * 2) + 1) / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
((T + 1)) is non empty V36() V37() V38() Element of bool REAL
(T) is non empty V36() V37() V38() Element of bool REAL
((T + 1)) \ (T) is V36() V37() V38() Element of bool REAL
0 + 1 is non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() Element of NAT
A + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(B * 2) - 1 is V27() V28() ext-real Element of REAL
1 + 0 is non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() Element of NAT
(A * 2) + (1 + 0) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
T + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
2 |^ (T + 1) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
1 / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
((T + 1)) is non empty V36() V37() V38() Element of bool REAL
(T) is non empty V36() V37() V38() Element of bool REAL
((T + 1)) \ (T) is V36() V37() V38() Element of bool REAL
2 * 0 is empty V26() V27() V28() ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() V68() Element of NAT
(2 * 0) + 1 is non empty V26() V27() V28() ext-real positive non negative V36() V37() V38() V39() V40() V41() V68() Element of NAT
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
T is V26() V27() V28() ext-real set
(T) is non empty V36() V37() V38() Element of bool REAL
A is V27() V28() ext-real Element of (T)
2 |^ T is V26() V27() V28() ext-real Element of REAL
B is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B / (2 |^ T) is V27() V28() ext-real Element of REAL
B is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B / (2 |^ T) is V27() V28() ext-real Element of REAL
n is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n / (2 |^ T) is V27() V28() ext-real Element of REAL
(B / (2 |^ T)) * (2 |^ T) is V27() V28() ext-real Element of REAL
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T) is non empty V36() V37() V38() Element of bool REAL
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
A is V27() V28() ext-real Element of (T)
(T,A) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T,A) / (2 |^ T) is V27() V28() ext-real Element of REAL
B is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B / (2 |^ T) is V27() V28() ext-real Element of REAL
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T) is non empty V36() V37() V38() Element of bool REAL
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
A is V27() V28() ext-real Element of (T)
(T,A) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T,A) - 1 is V27() V28() ext-real Element of REAL
((T,A) - 1) / (2 |^ T) is V27() V28() ext-real Element of REAL
(T,A) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((T,A) + 1) / (2 |^ T) is V27() V28() ext-real Element of REAL
1 + (T,A) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
0 + (T,A) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T,A) / (2 |^ T) is V27() V28() ext-real Element of REAL
- 1 is V27() V28() ext-real non positive Element of REAL
(- 1) + (T,A) is V27() V28() ext-real Element of REAL
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T) is non empty V36() V37() V38() Element of bool REAL
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
A is V27() V28() ext-real Element of (T)
(T,A) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T,A) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((T,A) + 1) / (2 |^ T) is V27() V28() ext-real Element of REAL
(T,A) - 1 is V27() V28() ext-real Element of REAL
((T,A) - 1) / (2 |^ T) is V27() V28() ext-real Element of REAL
1 + (T,A) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
- 1 is V27() V28() ext-real non positive Element of REAL
(- 1) + (T,A) is V27() V28() ext-real Element of REAL
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
T + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((T + 1)) is non empty V36() V37() V38() Element of bool REAL
(T) is non empty V36() V37() V38() Element of bool REAL
2 |^ (T + 1) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
A is V27() V28() ext-real Element of ((T + 1))
((T + 1),A) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((T + 1),A) - 1 is V27() V28() ext-real Element of REAL
(((T + 1),A) - 1) / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
((T + 1),A) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(((T + 1),A) + 1) / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
B is V27() V28() ext-real Element of REAL
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
G is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
2 * G is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 * G) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
G * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 |^ T) * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G * 2) / ((2 |^ T) * 2) is V27() V28() ext-real Element of REAL
G / (2 |^ T) is V27() V28() ext-real Element of REAL
((2 |^ T) * 2) / 2 is V27() V28() ext-real Element of REAL
G * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G * 2) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 |^ (T + 1)) - 1 is V27() V28() ext-real Element of REAL
(2 |^ T) * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((2 |^ T) * 2) / 2 is V27() V28() ext-real Element of REAL
S is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
S * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(S * 2) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((S * 2) + 1) - 1 is V27() V28() ext-real Element of REAL
(((S * 2) + 1) - 1) / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
(S * 2) / ((2 |^ T) * 2) is V27() V28() ext-real Element of REAL
S / (2 |^ T) is V27() V28() ext-real Element of REAL
2 / 2 is V27() V28() ext-real non negative Element of REAL
(S / (2 |^ T)) * (2 / 2) is V27() V28() ext-real Element of REAL
G * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G * 2) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
G * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G * 2) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
S is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
S / (2 |^ T) is V27() V28() ext-real Element of REAL
F is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
F / (2 |^ T) is V27() V28() ext-real Element of REAL
n is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n / (2 |^ T) is V27() V28() ext-real Element of REAL
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
G is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
2 * G is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 * G) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
G * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 |^ T) * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G * 2) / ((2 |^ T) * 2) is V27() V28() ext-real Element of REAL
G / (2 |^ T) is V27() V28() ext-real Element of REAL
((2 |^ T) * 2) / 2 is V27() V28() ext-real Element of REAL
G * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G * 2) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
G + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
S is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((G * 2) + 1) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
- 1 is V27() V28() ext-real non positive Element of REAL
(((G * 2) + 1) + 1) + (- 1) is V27() V28() ext-real Element of REAL
S * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 |^ T) * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((2 |^ T) * 2) / 2 is V27() V28() ext-real Element of REAL
(((G * 2) + 1) + 1) / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
(G + 1) * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((G + 1) * 2) / ((2 |^ T) * 2) is V27() V28() ext-real Element of REAL
(G + 1) / (2 |^ T) is V27() V28() ext-real Element of REAL
2 / 2 is V27() V28() ext-real non negative Element of REAL
((G + 1) / (2 |^ T)) * (2 / 2) is V27() V28() ext-real Element of REAL
D is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
D / (2 |^ T) is V27() V28() ext-real Element of REAL
G * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G * 2) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
G * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G * 2) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
S is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
S / (2 |^ T) is V27() V28() ext-real Element of REAL
F is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
F / (2 |^ T) is V27() V28() ext-real Element of REAL
n is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n / (2 |^ T) is V27() V28() ext-real Element of REAL
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T) is non empty V36() V37() V38() Element of bool REAL
B is V27() V28() ext-real Element of (T)
A is V27() V28() ext-real Element of (T)
(T,B) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T,A) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T,A) / (2 |^ T) is V27() V28() ext-real Element of REAL
(T,B) / (2 |^ T) is V27() V28() ext-real Element of REAL
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T) is non empty V36() V37() V38() Element of bool REAL
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B is V27() V28() ext-real Element of (T)
A is V27() V28() ext-real Element of (T)
(T,B) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T,B) - 1 is V27() V28() ext-real Element of REAL
((T,B) - 1) / (2 |^ T) is V27() V28() ext-real Element of REAL
(T,A) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(T,A) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((T,A) + 1) / (2 |^ T) is V27() V28() ext-real Element of REAL
(T,B) / (2 |^ T) is V27() V28() ext-real Element of REAL
(T,A) / (2 |^ T) is V27() V28() ext-real Element of REAL
T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
T + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((T + 1)) is non empty V36() V37() V38() Element of bool REAL
(T) is non empty V36() V37() V38() Element of bool REAL
2 |^ (T + 1) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
B is V27() V28() ext-real Element of ((T + 1))
A is V27() V28() ext-real Element of ((T + 1))
((T + 1),A) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((T + 1),A) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(((T + 1),A) + 1) / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
((T + 1),B) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((T + 1),B) - 1 is V27() V28() ext-real Element of REAL
(((T + 1),B) - 1) / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
n is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
2 * n is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 * n) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
n * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(n * 2) / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 |^ T) * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(n * 2) / ((2 |^ T) * 2) is V27() V28() ext-real Element of REAL
n / (2 |^ T) is V27() V28() ext-real Element of REAL
2 / 2 is V27() V28() ext-real non negative Element of REAL
(n / (2 |^ T)) * (2 / 2) is V27() V28() ext-real Element of REAL
((2 |^ T) * 2) / 2 is V27() V28() ext-real Element of REAL
G is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
2 * G is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 * G) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
G * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G * 2) / (2 |^ (T + 1)) is V27() V28() ext-real Element of REAL
2 |^ T is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(2 |^ T) * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G * 2) / ((2 |^ T) * 2) is V27() V28() ext-real Element of REAL
G / (2 |^ T) is V27() V28() ext-real Element of REAL
2 / 2 is V27() V28() ext-real non negative Element of REAL
(G / (2 |^ T)) * (2 / 2) is V27() V28() ext-real Element of REAL
((2 |^ T) * 2) / 2 is V27() V28() ext-real Element of REAL
(n * 2) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G * 2) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
- 1 is V27() V28() ext-real non positive Element of REAL
((n * 2) + 1) + (- 1) is V27() V28() ext-real Element of REAL
((G * 2) + 1) + (- 1) is V27() V28() ext-real Element of REAL
(n * 2) / 2 is V27() V28() ext-real Element of REAL
(G * 2) / 2 is V27() V28() ext-real Element of REAL
G + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(G + 1) * 2 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
A is Element of the carrier of T
B is Element of bool the carrier of T
Int B is open Element of bool the carrier of T
n is open Element of bool the carrier of T
n is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
A is Element of bool the carrier of T
B is Element of the carrier of T
n is Element of bool the carrier of T
B is Element of the carrier of T
n is a_neighborhood of B
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
A is Element of bool the carrier of T
B is Element of the carrier of T
n is a_neighborhood of B
n is a_neighborhood of B
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
A is Element of the carrier of T
B is Element of the carrier of T
n is Element of bool the carrier of T
n ` is Element of bool the carrier of T
the carrier of T \ n is set
G is Element of bool the carrier of T
G ` is Element of bool the carrier of T
the carrier of T \ G is set
A is Element of the carrier of T
B is Element of the carrier of T
n is Element of bool the carrier of T
G is Element of bool the carrier of T
n ` is Element of bool the carrier of T
the carrier of T \ n is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
A is Element of the carrier of T
{A} is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
{A} ` is Element of bool the carrier of T
the carrier of T \ {A} is set
B is Element of bool the carrier of T
bool (bool the carrier of T) is non empty set
n is Element of bool (bool the carrier of T)
G is Element of bool the carrier of T
S is Element of the carrier of T
S is Element of the carrier of T
D is Element of bool the carrier of T
S is Element of the carrier of T
S is Element of the carrier of T
S is Element of the carrier of T
D is Element of the carrier of T
the topology of T is non empty Element of bool (bool the carrier of T)
G is set
S is Element of bool the carrier of T
D is Element of the carrier of T
G is Element of the carrier of T
S is Element of bool the carrier of T
D is Element of bool the carrier of T
S is Element of bool the carrier of T
union n is set
G is set
S is Element of the carrier of T
D is Element of bool the carrier of T
F is set
G is set
S is set
D is Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
([#] T) \ {A} is Element of bool the carrier of T
F is Element of the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
([#] T) \ {A} is Element of bool the carrier of T
A is Element of the carrier of T
{A} is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
bool the carrier of T is non empty set
A is Element of the carrier of T
B is Element of the carrier of T
{A} is non empty Element of bool the carrier of T
{A} ` is Element of bool the carrier of T
the carrier of T \ {A} is set
{B} is non empty Element of bool the carrier of T
{B} ` is Element of bool the carrier of T
the carrier of T \ {B} is set
n is Element of bool the carrier of T
G is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
A is open Element of bool the carrier of T
Cl A is closed Element of bool the carrier of T
B is open Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
([#] T) \ B is Element of bool the carrier of T
n is Element of bool the carrier of T
G is Element of bool the carrier of T
([#] T) \ {} is Element of bool the carrier of T
n /\ G is Element of bool the carrier of T
S is set
([#] T) \ G is Element of bool the carrier of T
S is Element of bool the carrier of T
D is Element of bool the carrier of T
F is Element of bool the carrier of T
Cl F is closed Element of bool the carrier of T
bool ([#] T) is non empty set
r1 is Element of bool ([#] T)
r2 is Element of bool ([#] T)
r1 ` is Element of bool ([#] T)
([#] T) \ r1 is set
D ` is Element of bool the carrier of T
the carrier of T \ D is set
B ` is closed Element of bool the carrier of T
the carrier of T \ B is set
(B `) ` is open Element of bool the carrier of T
the carrier of T \ (B `) is set
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
n is Element of bool the carrier of T
G is Element of bool the carrier of T
Cl G is closed Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
G is Element of bool the carrier of T
Cl G is closed Element of bool the carrier of T
D is Element of bool the carrier of T
Cl D is closed Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
A is open Element of bool the carrier of T
B is Element of the carrier of T
A ` is closed Element of bool the carrier of T
the carrier of T \ A is set
(A `) ` is open Element of bool the carrier of T
the carrier of T \ (A `) is set
n is Element of bool the carrier of T
G is Element of bool the carrier of T
S is Element of bool the carrier of T
G /\ S is Element of bool the carrier of T
Cl G is closed Element of bool the carrier of T
S /\ (Cl G) is Element of bool the carrier of T
{} T is empty proper V36() V37() V38() V39() V40() V41() V42() open closed boundary nowhere_dense Element of bool the carrier of T
Cl ({} T) is closed Element of bool the carrier of T
D is Element of bool the carrier of T
Cl D is closed Element of bool the carrier of T
n is Element of bool the carrier of T
G is open Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
Cl G is closed Element of bool the carrier of T
n is Element of bool the carrier of T
n is Element of bool the carrier of T
S is open Element of bool the carrier of T
Cl S is closed Element of bool the carrier of T
F is open Element of bool the carrier of T
Cl F is closed Element of bool the carrier of T
A is Element of the carrier of T
B is Element of bool the carrier of T
B ` is Element of bool the carrier of T
the carrier of T \ B is set
n is Element of bool the carrier of T
G is open Element of bool the carrier of T
Cl G is closed Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
([#] T) \ (Cl G) is Element of bool the carrier of T
S is Element of bool the carrier of T
D is Element of bool the carrier of T
Cl D is closed Element of bool the carrier of T
F is Element of bool the carrier of T
(Cl D) ` is open Element of bool the carrier of T
the carrier of T \ (Cl D) is set
(B `) ` is Element of bool the carrier of T
the carrier of T \ (B `) is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
A is open Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
([#] T) \ A is Element of bool the carrier of T
([#] T) \ {} is Element of bool the carrier of T
n is set
B is Element of bool the carrier of T
([#] T) \ B is Element of bool the carrier of T
G is Element of the carrier of T
{G} is non empty Element of bool the carrier of T
S is set
D is Element of bool the carrier of T
D /\ B is Element of bool the carrier of T
F is set
F is Element of bool the carrier of T
r1 is Element of bool the carrier of T
r2 is Element of bool the carrier of T
Cl r2 is closed Element of bool the carrier of T
r1 ` is Element of bool the carrier of T
the carrier of T \ r1 is set
A ` is closed Element of bool the carrier of T
the carrier of T \ A is set
(A `) ` is open Element of bool the carrier of T
the carrier of T \ (A `) is set
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
B is Element of bool the carrier of T
n is Element of bool the carrier of T
Cl n is closed Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
n is Element of bool the carrier of T
Cl n is closed Element of bool the carrier of T
S is Element of bool the carrier of T
Cl S is closed Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
A is Element of bool the carrier of T
B is Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
([#] T) \ A is Element of bool the carrier of T
n is Element of bool the carrier of T
([#] T) \ n is Element of bool the carrier of T
B /\ n is Element of bool the carrier of T
G is set
G is Element of bool the carrier of T
S is Element of bool the carrier of T
S ` is Element of bool the carrier of T
the carrier of T \ S is set
Cl G is closed Element of bool the carrier of T
A ` is Element of bool the carrier of T
the carrier of T \ A is set
(A `) ` is Element of bool the carrier of T
the carrier of T \ (A `) is set
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
Cl ([#] T) is closed Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
A is Element of bool the carrier of T
B is Element of bool the carrier of T
Cl A is closed Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
A is closed Element of bool the carrier of T
B is closed Element of bool the carrier of T
n is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(n) is non empty V36() V37() V38() Element of bool REAL
[:(n),(bool the carrier of T):] is non empty set
bool [:(n),(bool the carrier of T):] is non empty set
n + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((n + 1)) is non empty V36() V37() V38() Element of bool REAL
[:((n + 1)),(bool the carrier of T):] is non empty set
bool [:((n + 1)),(bool the carrier of T):] is non empty set
G is V10() V13((n)) V14( bool the carrier of T) Function-like V33((n), bool the carrier of T) Element of bool [:(n),(bool the carrier of T):]
G . 0 is set
G . 1 is set
([#] T) \ (G . 1) is Element of bool the carrier of T
S is V27() V28() ext-real Element of (n)
(T,(n),G,S) is Element of bool the carrier of T
D is V27() V28() ext-real Element of (n)
(T,(n),G,D) is Element of bool the carrier of T
Cl (T,(n),G,D) is closed Element of bool the carrier of T
((n + 1)) \ (n) is V36() V37() V38() Element of bool REAL
S is non empty set
2 |^ (n + 1) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
D is Element of S
F is V27() V28() ext-real Element of ((n + 1))
((n + 1),F) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((n + 1),F) - 1 is V27() V28() ext-real Element of REAL
(((n + 1),F) - 1) / (2 |^ (n + 1)) is V27() V28() ext-real Element of REAL
((n + 1),F) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(((n + 1),F) + 1) / (2 |^ (n + 1)) is V27() V28() ext-real Element of REAL
r1 is V27() V28() ext-real Element of (n)
r2 is V27() V28() ext-real Element of (n)
(T,(n),G,r1) is Element of bool the carrier of T
(T,(n),G,r2) is Element of bool the carrier of T
the (T,(T,(n),G,r1),(T,(n),G,r2)) is (T,(T,(n),G,r1),(T,(n),G,r2))
r is V27() V28() ext-real Element of ((n + 1))
q11 is V27() V28() ext-real Element of (n)
((n + 1),r) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((n + 1),r) - 1 is V27() V28() ext-real Element of REAL
(((n + 1),r) - 1) / (2 |^ (n + 1)) is V27() V28() ext-real Element of REAL
q21 is V27() V28() ext-real Element of (n)
((n + 1),r) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(((n + 1),r) + 1) / (2 |^ (n + 1)) is V27() V28() ext-real Element of REAL
(T,(n),G,q11) is Element of bool the carrier of T
(T,(n),G,q21) is Element of bool the carrier of T
[:S,(bool the carrier of T):] is non empty set
bool [:S,(bool the carrier of T):] is non empty set
D is V10() V13(S) V14( bool the carrier of T) Function-like V33(S, bool the carrier of T) Element of bool [:S,(bool the carrier of T):]
F is V27() V28() ext-real Element of ((n + 1))
r1 is V27() V28() ext-real Element of (n)
(T,(n),G,r1) is Element of bool the carrier of T
r2 is Element of bool the carrier of T
r is V27() V28() ext-real Element of ((n + 1))
G . r is set
D . r is set
r1 is Element of S
D . r1 is Element of bool the carrier of T
r2 is Element of bool the carrier of T
r is V27() V28() ext-real Element of ((n + 1))
G . r is set
D . r is set
F is V10() V13(((n + 1))) V14( bool the carrier of T) Function-like V33(((n + 1)), bool the carrier of T) Element of bool [:((n + 1)),(bool the carrier of T):]
F . 0 is set
F . 1 is set
([#] T) \ (F . 1) is Element of bool the carrier of T
r2 is V27() V28() ext-real Element of ((n + 1))
r1 is V27() V28() ext-real Element of ((n + 1))
(T,((n + 1)),F,r1) is Element of bool the carrier of T
(T,((n + 1)),F,r2) is Element of bool the carrier of T
Cl (T,((n + 1)),F,r1) is closed Element of bool the carrier of T
r is V27() V28() ext-real Element of ((n + 1))
(T,((n + 1)),F,r) is Element of bool the carrier of T
G . r is set
G . r1 is set
G . r2 is set
q21 is V27() V28() ext-real Element of (n)
q11 is V27() V28() ext-real Element of (n)
((n + 1),r2) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((n + 1),r2) - 1 is V27() V28() ext-real Element of REAL
(((n + 1),r2) - 1) / (2 |^ (n + 1)) is V27() V28() ext-real Element of REAL
((n + 1),r2) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(((n + 1),r2) + 1) / (2 |^ (n + 1)) is V27() V28() ext-real Element of REAL
q11 is V27() V28() ext-real Element of (n)
q21 is V27() V28() ext-real Element of (n)
D . r2 is set
(T,(n),G,q11) is Element of bool the carrier of T
(T,(n),G,q21) is Element of bool the carrier of T
Cl (T,(n),G,q11) is closed Element of bool the carrier of T
q12 is V27() V28() ext-real Element of (n)
(T,(n),G,q12) is Element of bool the carrier of T
Cl (T,(n),G,q12) is closed Element of bool the carrier of T
((n + 1),r1) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((n + 1),r1) - 1 is V27() V28() ext-real Element of REAL
(((n + 1),r1) - 1) / (2 |^ (n + 1)) is V27() V28() ext-real Element of REAL
((n + 1),r1) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(((n + 1),r1) + 1) / (2 |^ (n + 1)) is V27() V28() ext-real Element of REAL
q11 is V27() V28() ext-real Element of (n)
q21 is V27() V28() ext-real Element of (n)
D . r1 is set
(T,(n),G,q11) is Element of bool the carrier of T
(T,(n),G,q21) is Element of bool the carrier of T
Cl (T,(n),G,q11) is closed Element of bool the carrier of T
Cl (T,(n),G,q21) is closed Element of bool the carrier of T
q12 is V27() V28() ext-real Element of (n)
(T,(n),G,q12) is Element of bool the carrier of T
((n + 1),r1) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((n + 1),r1) - 1 is V27() V28() ext-real Element of REAL
(((n + 1),r1) - 1) / (2 |^ (n + 1)) is V27() V28() ext-real Element of REAL
((n + 1),r1) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(((n + 1),r1) + 1) / (2 |^ (n + 1)) is V27() V28() ext-real Element of REAL
q11 is V27() V28() ext-real Element of (n)
q21 is V27() V28() ext-real Element of (n)
D . r1 is set
(T,(n),G,q11) is Element of bool the carrier of T
(T,(n),G,q21) is Element of bool the carrier of T
((n + 1),r2) is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
((n + 1),r2) - 1 is V27() V28() ext-real Element of REAL
(((n + 1),r2) - 1) / (2 |^ (n + 1)) is V27() V28() ext-real Element of REAL
((n + 1),r2) + 1 is V26() V27() V28() ext-real V36() V37() V38() V39() V40() V41() V68() Element of NAT
(((n + 1),r2) + 1) / (2 |^ (n + 1)) is V27() V28() ext-real Element of REAL
q12 is V27() V28() ext-real Element of (n)
q22 is V27() V28() ext-real Element of (n)
D . r2 is set
(T,(n),G,q12) is Element of bool the carrier of T
(T,(n),G,q22) is Element of bool the carrier of T
Cl (T,(n),G,q12) is closed Element of bool the carrier of T
Cl (T,(n),G,q11) is closed Element of bool the carrier of T
Cl (T,(n),G,q21) is closed Element of bool the carrier of T
Cl (T,(n),G,q21) is closed Element of bool the carrier of T