:: JORDAN1D semantic presentation

REAL is V104() V105() V106() V110() set
NAT is V104() V105() V106() V107() V108() V109() V110() Element of K10(REAL)
K10(REAL) is set
COMPLEX is V104() V110() set
omega is V104() V105() V106() V107() V108() V109() V110() set
K10(omega) is set
K10(NAT) is set
RAT is V104() V105() V106() V107() V110() set
INT is V104() V105() V106() V107() V108() V110() set
1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
K11(1,1) is set
K10(K11(1,1)) is set
K11(K11(1,1),1) is set
K10(K11(K11(1,1),1)) is set
K11(K11(1,1),REAL) is set
K10(K11(K11(1,1),REAL)) is set
K11(REAL,REAL) is set
K11(K11(REAL,REAL),REAL) is set
K10(K11(K11(REAL,REAL),REAL)) is set
2 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
K11(2,2) is set
K11(K11(2,2),REAL) is set
K10(K11(K11(2,2),REAL)) is set
K10(K11(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V142() V167() V168() V169() V170() V171() V172() V173() strict RLTopStruct
the U1 of (TOP-REAL 2) is set
K11( the U1 of (TOP-REAL 2),REAL) is set
K10(K11( the U1 of (TOP-REAL 2),REAL)) is set
K10( the U1 of (TOP-REAL 2)) is set
K354( the U1 of (TOP-REAL 2)) is M17( the U1 of (TOP-REAL 2))
K11(COMPLEX,COMPLEX) is set
K10(K11(COMPLEX,COMPLEX)) is set
K11(COMPLEX,REAL) is set
K10(K11(COMPLEX,REAL)) is set
3 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
4 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
0 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
the empty Function-like functional V104() V105() V106() V107() V108() V109() V110() set is empty Function-like functional V104() V105() V106() V107() V108() V109() V110() set
{} is set
2 * 0 is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * 0) + 1 is non empty ordinal natural V14() real V16() non even ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
1 div 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * 1 is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * 1) + 0 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 div 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n is set
C is set
j is set
C \/ j is set
c₄ is set
(C \/ j) \/ c₄ is set
j is set
((C \/ j) \/ c₄) \/ j is set
n is set
C is set
j is set
c₄ is set
{n,C,j,c₄} is set
union {n,C,j,c₄} is set
n \/ C is set
(n \/ C) \/ j is set
((n \/ C) \/ j) \/ c₄ is set
j is set
c₆ is set
j is set
n is set
C is set
union n is set
union C is set
j is set
c₄ is set
j is set
union j is set
c₆ is set
n is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 |^ n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C is ordinal natural V14() real V16() ext-real non negative set
2 |^ C is ordinal natural V14() real V16() ext-real non negative Element of REAL
C + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 |^ (C + 1) is ordinal natural V14() real V16() ext-real non negative Element of REAL
2 |^ (C + 1) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * (2 |^ C) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 |^ 0 is ordinal natural V14() real V16() ext-real non negative Element of REAL
n is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n |^ C is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
j is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n |^ j is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
j + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n |^ (j + 1) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n * (n |^ j) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n |^ 0 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C is V14() real ext-real set
1 / C is V14() real ext-real Element of REAL
C |^ (n + 1) is V14() real ext-real set
(1 / C) * (C |^ (n + 1)) is V14() real ext-real Element of REAL
C |^ n is V14() real ext-real set
(C |^ n) * C is V14() real ext-real set
(1 / C) * ((C |^ n) * C) is V14() real ext-real Element of REAL
(1 / C) * C is V14() real ext-real Element of REAL
((1 / C) * C) * (C |^ n) is V14() real ext-real Element of REAL
1 * (C |^ n) is V14() real ext-real Element of REAL
n is V14() real ext-real set
2 * 2 is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * n is V14() real ext-real Element of REAL
4 - 2 is V14() real V16() ext-real Element of REAL
(2 * n) - 2 is V14() real ext-real Element of REAL
n is V14() real ext-real set
2 * n is V14() real ext-real Element of REAL
2 - 1 is V14() real V16() ext-real Element of REAL
(2 * n) - 1 is V14() real ext-real Element of REAL
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * n is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) - 2 is V14() real V16() ext-real Element of REAL
(2 * n) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * n is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) - 1 is non empty V14() real V16() non even ext-real Element of REAL
(2 * n) -' 1 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * n is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) - 1 is non empty V14() real V16() non even ext-real Element of REAL
(2 * n) -' 1 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
((2 * n) -' 2) + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
((2 * n) -' 1) -' 1 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(((2 * n) -' 1) -' 1) + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n - 2 is V14() real V16() ext-real Element of REAL
2 * n is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
((2 * n) -' 2) - 2 is V14() real V16() ext-real Element of REAL
C is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 |^ C is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 |^ (C + 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
j is V14() real ext-real set
j / (2 |^ C) is V14() real ext-real Element of REAL
(j / (2 |^ C)) * (n - 2) is V14() real ext-real Element of REAL
j / (2 |^ (C + 1)) is V14() real ext-real Element of REAL
(j / (2 |^ (C + 1))) * (((2 * n) -' 2) - 2) is V14() real ext-real Element of REAL
(2 * n) - 2 is V14() real V16() ext-real Element of REAL
(2 |^ C) / (n - 2) is V14() real ext-real Element of REAL
j / ((2 |^ C) / (n - 2)) is V14() real ext-real Element of REAL
(2 |^ C) * 2 is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(n - 2) * 2 is V14() real V16() even ext-real Element of REAL
((2 |^ C) * 2) / ((n - 2) * 2) is V14() real ext-real Element of REAL
j / (((2 |^ C) * 2) / ((n - 2) * 2)) is V14() real ext-real Element of REAL
j / ((2 |^ C) * 2) is V14() real ext-real Element of REAL
(j / ((2 |^ C) * 2)) * ((n - 2) * 2) is V14() real ext-real Element of REAL
((2 * n) - 2) - 2 is V14() real V16() ext-real Element of REAL
(j / (2 |^ (C + 1))) * (((2 * n) - 2) - 2) is V14() real ext-real Element of REAL
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * n is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) - 2 is V14() real V16() ext-real Element of REAL
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * n is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) -' 1 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) - 1 is non empty V14() real V16() non even ext-real Element of REAL
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * n is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 |^ C is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 |^ C) + 3 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 |^ (C + 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 |^ (C + 1)) + 3 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * (n + 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * ((2 |^ C) + 3) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) + (2 * 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * (2 |^ C) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * 3 is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * (2 |^ C)) + (2 * 3) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
6 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 |^ (C + 1)) + 6 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) + 2 is non empty ordinal natural V14() real V16() even ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
((2 * n) + 2) - 4 is V14() real V16() ext-real Element of REAL
((2 |^ (C + 1)) + 6) - 4 is V14() real V16() ext-real Element of REAL
(2 * n) - 2 is V14() real V16() ext-real Element of REAL
(2 |^ (C + 1)) + 2 is non empty ordinal natural V14() real V16() even ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * n is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
((2 * n) -' 2) + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(((2 * n) -' 2) + 1) - 2 is V14() real V16() ext-real Element of REAL
(2 * n) - 2 is V14() real V16() ext-real Element of REAL
((2 * n) - 2) + 1 is V14() real V16() ext-real Element of REAL
(((2 * n) - 2) + 1) - 2 is V14() real V16() ext-real Element of REAL
(2 * n) - 3 is V14() real V16() ext-real Element of REAL
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * n is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
j is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
c₄ is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
j is non empty Element of K10( the U1 of (TOP-REAL 2))
Gauge (j,C) is V18() non empty-yielding V21( NAT ) V22(K354( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K354( the U1 of (TOP-REAL 2))
len (Gauge (j,C)) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
Gauge (j,(C + 1)) is V18() non empty-yielding V21( NAT ) V22(K354( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K354( the U1 of (TOP-REAL 2))
len (Gauge (j,(C + 1))) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(Gauge (j,C)) * (n,j) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (j,C)) * (n,j)) `1 is V14() real ext-real Element of REAL
(Gauge (j,(C + 1))) * (((2 * n) -' 2),c<sub>4</sub>) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (j,(C + 1))) * (((2 * n) -' 2),c<sub>4</sub>)) `1 is V14() real ext-real Element of REAL
N-bound j is V14() real ext-real Element of REAL
(TOP-REAL 2) | j is strict SubSpace of TOP-REAL 2
proj2 is V18() V21( the U1 of (TOP-REAL 2)) V22( REAL ) Function-like V43( the U1 of (TOP-REAL 2), REAL ) Element of K10(K11( the U1 of (TOP-REAL 2),REAL))
proj2 | j is V18() V21( the U1 of ((TOP-REAL 2) | j)) V22( REAL ) Function-like V43( the U1 of ((TOP-REAL 2) | j), REAL ) Element of K10(K11( the U1 of ((TOP-REAL 2) | j),REAL))
the U1 of ((TOP-REAL 2) | j) is set
K11( the U1 of ((TOP-REAL 2) | j),REAL) is set
K10(K11( the U1 of ((TOP-REAL 2) | j),REAL)) is set
K435(((TOP-REAL 2) | j),(proj2 | j)) is V14() real ext-real Element of REAL
K537( the U1 of ((TOP-REAL 2) | j),REAL,(proj2 | j), the U1 of ((TOP-REAL 2) | j)) is V104() V105() V106() Element of K10(REAL)
K506(K537( the U1 of ((TOP-REAL 2) | j),REAL,(proj2 | j), the U1 of ((TOP-REAL 2) | j))) is V14() real ext-real Element of REAL
E-bound j is V14() real ext-real Element of REAL
proj1 is V18() V21( the U1 of (TOP-REAL 2)) V22( REAL ) Function-like V43( the U1 of (TOP-REAL 2), REAL ) Element of K10(K11( the U1 of (TOP-REAL 2),REAL))
proj1 | j is V18() V21( the U1 of ((TOP-REAL 2) | j)) V22( REAL ) Function-like V43( the U1 of ((TOP-REAL 2) | j), REAL ) Element of K10(K11( the U1 of ((TOP-REAL 2) | j),REAL))
K435(((TOP-REAL 2) | j),(proj1 | j)) is V14() real ext-real Element of REAL
K537( the U1 of ((TOP-REAL 2) | j),REAL,(proj1 | j), the U1 of ((TOP-REAL 2) | j)) is V104() V105() V106() Element of K10(REAL)
K506(K537( the U1 of ((TOP-REAL 2) | j),REAL,(proj1 | j), the U1 of ((TOP-REAL 2) | j))) is V14() real ext-real Element of REAL
S-bound j is V14() real ext-real Element of REAL
K434(((TOP-REAL 2) | j),(proj2 | j)) is V14() real ext-real Element of REAL
K507(K537( the U1 of ((TOP-REAL 2) | j),REAL,(proj2 | j), the U1 of ((TOP-REAL 2) | j))) is V14() real ext-real Element of REAL
W-bound j is V14() real ext-real Element of REAL
K434(((TOP-REAL 2) | j),(proj1 | j)) is V14() real ext-real Element of REAL
K507(K537( the U1 of ((TOP-REAL 2) | j),REAL,(proj1 | j), the U1 of ((TOP-REAL 2) | j))) is V14() real ext-real Element of REAL
2 |^ C is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 |^ C) + 3 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 |^ (C + 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 |^ (C + 1)) + 3 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
width (Gauge (j,(C + 1))) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
[((2 * n) -' 2),c₄] is set
{((2 * n) -' 2),c₄} is V104() V105() V106() V107() V108() V109() set
{((2 * n) -' 2)} is V104() V105() V106() V107() V108() V109() set
{{((2 * n) -' 2),c₄},{((2 * n) -' 2)}} is set
Indices (Gauge (j,(C + 1))) is set
width (Gauge (j,C)) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
[n,j] is set
{n,j} is V104() V105() V106() V107() V108() V109() set
{n} is V104() V105() V106() V107() V108() V109() set
{{n,j},{n}} is set
Indices (Gauge (j,C)) is set
(E-bound j) - (W-bound j) is V14() real ext-real Element of REAL
((E-bound j) - (W-bound j)) / (2 |^ C) is V14() real ext-real Element of REAL
n - 2 is V14() real V16() ext-real Element of REAL
(((E-bound j) - (W-bound j)) / (2 |^ C)) * (n - 2) is V14() real ext-real Element of REAL
(W-bound j) + ((((E-bound j) - (W-bound j)) / (2 |^ C)) * (n - 2)) is V14() real ext-real Element of REAL
(N-bound j) - (S-bound j) is V14() real ext-real Element of REAL
((N-bound j) - (S-bound j)) / (2 |^ C) is V14() real ext-real Element of REAL
j - 2 is V14() real V16() ext-real Element of REAL
(((N-bound j) - (S-bound j)) / (2 |^ C)) * (j - 2) is V14() real ext-real Element of REAL
(S-bound j) + ((((N-bound j) - (S-bound j)) / (2 |^ C)) * (j - 2)) is V14() real ext-real Element of REAL
|[((W-bound j) + ((((E-bound j) - (W-bound j)) / (2 |^ C)) * (n - 2))),((S-bound j) + ((((N-bound j) - (S-bound j)) / (2 |^ C)) * (j - 2)))]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
|[((W-bound j) + ((((E-bound j) - (W-bound j)) / (2 |^ C)) * (n - 2))),((S-bound j) + ((((N-bound j) - (S-bound j)) / (2 |^ C)) * (j - 2)))]| `1 is V14() real ext-real Element of REAL
((E-bound j) - (W-bound j)) / (2 |^ (C + 1)) is V14() real ext-real Element of REAL
((2 * n) -' 2) - 2 is V14() real V16() ext-real Element of REAL
(((E-bound j) - (W-bound j)) / (2 |^ (C + 1))) * (((2 * n) -' 2) - 2) is V14() real ext-real Element of REAL
(W-bound j) + ((((E-bound j) - (W-bound j)) / (2 |^ (C + 1))) * (((2 * n) -' 2) - 2)) is V14() real ext-real Element of REAL
((N-bound j) - (S-bound j)) / (2 |^ (C + 1)) is V14() real ext-real Element of REAL
c<sub>4</sub> - 2 is V14() real V16() ext-real Element of REAL
(((N-bound j) - (S-bound j)) / (2 |^ (C + 1))) * (c<sub>4</sub> - 2) is V14() real ext-real Element of REAL
(S-bound j) + ((((N-bound j) - (S-bound j)) / (2 |^ (C + 1))) * (c<sub>4</sub> - 2)) is V14() real ext-real Element of REAL
|[((W-bound j) + ((((E-bound j) - (W-bound j)) / (2 |^ (C + 1))) * (((2 * n) -' 2) - 2))),((S-bound j) + ((((N-bound j) - (S-bound j)) / (2 |^ (C + 1))) * (c<sub>4</sub> - 2)))]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
|[((W-bound j) + ((((E-bound j) - (W-bound j)) / (2 |^ (C + 1))) * (((2 * n) -' 2) - 2))),((S-bound j) + ((((N-bound j) - (S-bound j)) / (2 |^ (C + 1))) * (c<sub>4</sub> - 2)))]| `1 is V14() real ext-real Element of REAL
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * n is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
j is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
c₄ is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
j is non empty Element of K10( the U1 of (TOP-REAL 2))
Gauge (j,C) is V18() non empty-yielding V21( NAT ) V22(K354( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K354( the U1 of (TOP-REAL 2))
len (Gauge (j,C)) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
Gauge (j,(C + 1)) is V18() non empty-yielding V21( NAT ) V22(K354( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K354( the U1 of (TOP-REAL 2))
len (Gauge (j,(C + 1))) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(Gauge (j,C)) * (j,n) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (j,C)) * (j,n)) `2 is V14() real ext-real Element of REAL
(Gauge (j,(C + 1))) * (c<sub>4</sub>,((2 * n) -' 2)) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (j,(C + 1))) * (c<sub>4</sub>,((2 * n) -' 2))) `2 is V14() real ext-real Element of REAL
N-bound j is V14() real ext-real Element of REAL
(TOP-REAL 2) | j is strict SubSpace of TOP-REAL 2
proj2 is V18() V21( the U1 of (TOP-REAL 2)) V22( REAL ) Function-like V43( the U1 of (TOP-REAL 2), REAL ) Element of K10(K11( the U1 of (TOP-REAL 2),REAL))
proj2 | j is V18() V21( the U1 of ((TOP-REAL 2) | j)) V22( REAL ) Function-like V43( the U1 of ((TOP-REAL 2) | j), REAL ) Element of K10(K11( the U1 of ((TOP-REAL 2) | j),REAL))
the U1 of ((TOP-REAL 2) | j) is set
K11( the U1 of ((TOP-REAL 2) | j),REAL) is set
K10(K11( the U1 of ((TOP-REAL 2) | j),REAL)) is set
K435(((TOP-REAL 2) | j),(proj2 | j)) is V14() real ext-real Element of REAL
K537( the U1 of ((TOP-REAL 2) | j),REAL,(proj2 | j), the U1 of ((TOP-REAL 2) | j)) is V104() V105() V106() Element of K10(REAL)
K506(K537( the U1 of ((TOP-REAL 2) | j),REAL,(proj2 | j), the U1 of ((TOP-REAL 2) | j))) is V14() real ext-real Element of REAL
E-bound j is V14() real ext-real Element of REAL
proj1 is V18() V21( the U1 of (TOP-REAL 2)) V22( REAL ) Function-like V43( the U1 of (TOP-REAL 2), REAL ) Element of K10(K11( the U1 of (TOP-REAL 2),REAL))
proj1 | j is V18() V21( the U1 of ((TOP-REAL 2) | j)) V22( REAL ) Function-like V43( the U1 of ((TOP-REAL 2) | j), REAL ) Element of K10(K11( the U1 of ((TOP-REAL 2) | j),REAL))
K435(((TOP-REAL 2) | j),(proj1 | j)) is V14() real ext-real Element of REAL
K537( the U1 of ((TOP-REAL 2) | j),REAL,(proj1 | j), the U1 of ((TOP-REAL 2) | j)) is V104() V105() V106() Element of K10(REAL)
K506(K537( the U1 of ((TOP-REAL 2) | j),REAL,(proj1 | j), the U1 of ((TOP-REAL 2) | j))) is V14() real ext-real Element of REAL
S-bound j is V14() real ext-real Element of REAL
K434(((TOP-REAL 2) | j),(proj2 | j)) is V14() real ext-real Element of REAL
K507(K537( the U1 of ((TOP-REAL 2) | j),REAL,(proj2 | j), the U1 of ((TOP-REAL 2) | j))) is V14() real ext-real Element of REAL
W-bound j is V14() real ext-real Element of REAL
K434(((TOP-REAL 2) | j),(proj1 | j)) is V14() real ext-real Element of REAL
K507(K537( the U1 of ((TOP-REAL 2) | j),REAL,(proj1 | j), the U1 of ((TOP-REAL 2) | j))) is V14() real ext-real Element of REAL
2 |^ C is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 |^ C) + 3 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 |^ (C + 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 |^ (C + 1)) + 3 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
width (Gauge (j,(C + 1))) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
[c₄,((2 * n) -' 2)] is set
{c₄,((2 * n) -' 2)} is V104() V105() V106() V107() V108() V109() set
{c₄} is V104() V105() V106() V107() V108() V109() set
{{c₄,((2 * n) -' 2)},{c₄}} is set
Indices (Gauge (j,(C + 1))) is set
width (Gauge (j,C)) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
[j,n] is set
{j,n} is V104() V105() V106() V107() V108() V109() set
{j} is V104() V105() V106() V107() V108() V109() set
{{j,n},{j}} is set
Indices (Gauge (j,C)) is set
(E-bound j) - (W-bound j) is V14() real ext-real Element of REAL
((E-bound j) - (W-bound j)) / (2 |^ C) is V14() real ext-real Element of REAL
j - 2 is V14() real V16() ext-real Element of REAL
(((E-bound j) - (W-bound j)) / (2 |^ C)) * (j - 2) is V14() real ext-real Element of REAL
(W-bound j) + ((((E-bound j) - (W-bound j)) / (2 |^ C)) * (j - 2)) is V14() real ext-real Element of REAL
(N-bound j) - (S-bound j) is V14() real ext-real Element of REAL
((N-bound j) - (S-bound j)) / (2 |^ C) is V14() real ext-real Element of REAL
n - 2 is V14() real V16() ext-real Element of REAL
(((N-bound j) - (S-bound j)) / (2 |^ C)) * (n - 2) is V14() real ext-real Element of REAL
(S-bound j) + ((((N-bound j) - (S-bound j)) / (2 |^ C)) * (n - 2)) is V14() real ext-real Element of REAL
|[((W-bound j) + ((((E-bound j) - (W-bound j)) / (2 |^ C)) * (j - 2))),((S-bound j) + ((((N-bound j) - (S-bound j)) / (2 |^ C)) * (n - 2)))]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
|[((W-bound j) + ((((E-bound j) - (W-bound j)) / (2 |^ C)) * (j - 2))),((S-bound j) + ((((N-bound j) - (S-bound j)) / (2 |^ C)) * (n - 2)))]| `2 is V14() real ext-real Element of REAL
((N-bound j) - (S-bound j)) / (2 |^ (C + 1)) is V14() real ext-real Element of REAL
((2 * n) -' 2) - 2 is V14() real V16() ext-real Element of REAL
(((N-bound j) - (S-bound j)) / (2 |^ (C + 1))) * (((2 * n) -' 2) - 2) is V14() real ext-real Element of REAL
(S-bound j) + ((((N-bound j) - (S-bound j)) / (2 |^ (C + 1))) * (((2 * n) -' 2) - 2)) is V14() real ext-real Element of REAL
((E-bound j) - (W-bound j)) / (2 |^ (C + 1)) is V14() real ext-real Element of REAL
c<sub>4</sub> - 2 is V14() real V16() ext-real Element of REAL
(((E-bound j) - (W-bound j)) / (2 |^ (C + 1))) * (c<sub>4</sub> - 2) is V14() real ext-real Element of REAL
(W-bound j) + ((((E-bound j) - (W-bound j)) / (2 |^ (C + 1))) * (c<sub>4</sub> - 2)) is V14() real ext-real Element of REAL
|[((W-bound j) + ((((E-bound j) - (W-bound j)) / (2 |^ (C + 1))) * (c<sub>4</sub> - 2))),((S-bound j) + ((((N-bound j) - (S-bound j)) / (2 |^ (C + 1))) * (((2 * n) -' 2) - 2)))]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
|[((W-bound j) + ((((E-bound j) - (W-bound j)) / (2 |^ (C + 1))) * (c<sub>4</sub> - 2))),((S-bound j) + ((((N-bound j) - (S-bound j)) / (2 |^ (C + 1))) * (((2 * n) -' 2) - 2)))]| `2 is V14() real ext-real Element of REAL
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * n is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) -' 1 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
j is non empty Element of K10( the U1 of (TOP-REAL 2))
Gauge (j,C) is V18() non empty-yielding V21( NAT ) V22(K354( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K354( the U1 of (TOP-REAL 2))
len (Gauge (j,C)) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
Gauge (j,(C + 1)) is V18() non empty-yielding V21( NAT ) V22(K354( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K354( the U1 of (TOP-REAL 2))
len (Gauge (j,(C + 1))) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 |^ C is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 |^ C) + 3 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 |^ (C + 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 |^ (C + 1)) + 3 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * (n + 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * (n + 1)) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) + (2 * 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
((2 * n) + (2 * 1)) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * n is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * n) -' 1 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
C + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
j is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
j + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * j is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * j) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * j) -' 1 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
c₄ is non empty compact non horizontal non vertical Element of K10( the U1 of (TOP-REAL 2))
Gauge (c₄,C) is V18() non empty-yielding V21( NAT ) V22(K354( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K354( the U1 of (TOP-REAL 2))
len (Gauge (c₄,C)) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
cell ((Gauge (c₄,C)),n,j) is Element of K10( the U1 of (TOP-REAL 2))
Gauge (c₄,(C + 1)) is V18() non empty-yielding V21( NAT ) V22(K354( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K354( the U1 of (TOP-REAL 2))
cell ((Gauge (c₄,(C + 1))),((2 * n) -' 2),((2 * j) -' 2)) is Element of K10( the U1 of (TOP-REAL 2))
cell ((Gauge (c₄,(C + 1))),((2 * n) -' 1),((2 * j) -' 2)) is Element of K10( the U1 of (TOP-REAL 2))
(cell ((Gauge (c₄,(C + 1))),((2 * n) -' 2),((2 * j) -' 2))) \/ (cell ((Gauge (c₄,(C + 1))),((2 * n) -' 1),((2 * j) -' 2))) is Element of K10( the U1 of (TOP-REAL 2))
cell ((Gauge (c₄,(C + 1))),((2 * n) -' 2),((2 * j) -' 1)) is Element of K10( the U1 of (TOP-REAL 2))
((cell ((Gauge (c₄,(C + 1))),((2 * n) -' 2),((2 * j) -' 2))) \/ (cell ((Gauge (c₄,(C + 1))),((2 * n) -' 1),((2 * j) -' 2)))) \/ (cell ((Gauge (c₄,(C + 1))),((2 * n) -' 2),((2 * j) -' 1))) is Element of K10( the U1 of (TOP-REAL 2))
cell ((Gauge (c₄,(C + 1))),((2 * n) -' 1),((2 * j) -' 1)) is Element of K10( the U1 of (TOP-REAL 2))
(((cell ((Gauge (c₄,(C + 1))),((2 * n) -' 2),((2 * j) -' 2))) \/ (cell ((Gauge (c₄,(C + 1))),((2 * n) -' 1),((2 * j) -' 2)))) \/ (cell ((Gauge (c₄,(C + 1))),((2 * n) -' 2),((2 * j) -' 1)))) \/ (cell ((Gauge (c₄,(C + 1))),((2 * n) -' 1),((2 * j) -' 1))) is Element of K10( the U1 of (TOP-REAL 2))
N-bound c₄ is V14() real ext-real Element of REAL
(TOP-REAL 2) | c₄ is strict SubSpace of TOP-REAL 2
proj2 is V18() V21( the U1 of (TOP-REAL 2)) V22( REAL ) Function-like V43( the U1 of (TOP-REAL 2), REAL ) Element of K10(K11( the U1 of (TOP-REAL 2),REAL))
proj2 | c₄ is V18() V21( the U1 of ((TOP-REAL 2) | c₄)) V22( REAL ) Function-like V43( the U1 of ((TOP-REAL 2) | c₄), REAL ) Element of K10(K11( the U1 of ((TOP-REAL 2) | c₄),REAL))
the U1 of ((TOP-REAL 2) | c₄) is set
K11( the U1 of ((TOP-REAL 2) | c₄),REAL) is set
K10(K11( the U1 of ((TOP-REAL 2) | c₄),REAL)) is set
K435(((TOP-REAL 2) | c₄),(proj2 | c₄)) is V14() real ext-real Element of REAL
K537( the U1 of ((TOP-REAL 2) | c₄),REAL,(proj2 | c₄), the U1 of ((TOP-REAL 2) | c₄)) is V104() V105() V106() Element of K10(REAL)
K506(K537( the U1 of ((TOP-REAL 2) | c₄),REAL,(proj2 | c₄), the U1 of ((TOP-REAL 2) | c₄))) is V14() real ext-real Element of REAL
E-bound c₄ is V14() real ext-real Element of REAL
proj1 is V18() V21( the U1 of (TOP-REAL 2)) V22( REAL ) Function-like V43( the U1 of (TOP-REAL 2), REAL ) Element of K10(K11( the U1 of (TOP-REAL 2),REAL))
proj1 | c₄ is V18() V21( the U1 of ((TOP-REAL 2) | c₄)) V22( REAL ) Function-like V43( the U1 of ((TOP-REAL 2) | c₄), REAL ) Element of K10(K11( the U1 of ((TOP-REAL 2) | c₄),REAL))
K435(((TOP-REAL 2) | c₄),(proj1 | c₄)) is V14() real ext-real Element of REAL
K537( the U1 of ((TOP-REAL 2) | c₄),REAL,(proj1 | c₄), the U1 of ((TOP-REAL 2) | c₄)) is V104() V105() V106() Element of K10(REAL)
K506(K537( the U1 of ((TOP-REAL 2) | c₄),REAL,(proj1 | c₄), the U1 of ((TOP-REAL 2) | c₄))) is V14() real ext-real Element of REAL
S-bound c₄ is V14() real ext-real Element of REAL
K434(((TOP-REAL 2) | c₄),(proj2 | c₄)) is V14() real ext-real Element of REAL
K507(K537( the U1 of ((TOP-REAL 2) | c₄),REAL,(proj2 | c₄), the U1 of ((TOP-REAL 2) | c₄))) is V14() real ext-real Element of REAL
W-bound c₄ is V14() real ext-real Element of REAL
K434(((TOP-REAL 2) | c₄),(proj1 | c₄)) is V14() real ext-real Element of REAL
K507(K537( the U1 of ((TOP-REAL 2) | c₄),REAL,(proj1 | c₄), the U1 of ((TOP-REAL 2) | c₄))) is V14() real ext-real Element of REAL
len (Gauge (c₄,(C + 1))) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
width (Gauge (c₄,(C + 1))) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * j) - 2 is V14() real V16() ext-real Element of REAL
(2 * j) - 3 is V14() real V16() ext-real Element of REAL
(N-bound c₄) - (S-bound c₄) is V14() real ext-real Element of REAL
2 |^ (C + 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
((N-bound c₄) - (S-bound c₄)) / (2 |^ (C + 1)) is V14() real ext-real Element of REAL
(((N-bound c₄) - (S-bound c₄)) / (2 |^ (C + 1))) * ((2 * j) - 3) is V14() real ext-real Element of REAL
(((N-bound c₄) - (S-bound c₄)) / (2 |^ (C + 1))) * ((2 * j) - 2) is V14() real ext-real Element of REAL
(S-bound c₄) + ((((N-bound c₄) - (S-bound c₄)) / (2 |^ (C + 1))) * ((2 * j) - 3)) is V14() real ext-real Element of REAL
(S-bound c₄) + ((((N-bound c₄) - (S-bound c₄)) / (2 |^ (C + 1))) * ((2 * j) - 2)) is V14() real ext-real Element of REAL
2 * (j + 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * (j + 1)) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
((2 * (j + 1)) -' 2) - 2 is V14() real V16() ext-real Element of REAL
(2 * j) + (2 * 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
((2 * j) + (2 * 1)) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(((2 * j) + (2 * 1)) -' 2) - 2 is V14() real V16() ext-real Element of REAL
((2 * n) -' 2) + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
((2 * j) -' 1) + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
[1,(2 * j)] is set
{1,(2 * j)} is V104() V105() V106() V107() V108() V109() set
{1} is V104() V105() V106() V107() V108() V109() set
{{1,(2 * j)},{1}} is set
Indices (Gauge (c₄,(C + 1))) is set
(Gauge (c₄,(C + 1))) * (1,(2 * j)) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c₄,(C + 1))) * (1,(2 * j))) `2 is V14() real ext-real Element of REAL
(E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>) is V14() real ext-real Element of REAL
((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ (C + 1)) is V14() real ext-real Element of REAL
1 - 2 is V14() real V16() ext-real Element of REAL
(((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * (1 - 2) is V14() real ext-real Element of REAL
(W-bound c<sub>4</sub>) + ((((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * (1 - 2)) is V14() real ext-real Element of REAL
|[((W-bound c<sub>4</sub>) + ((((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * (1 - 2))),((S-bound c<sub>4</sub>) + ((((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * ((2 * j) - 2)))]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
|[((W-bound c<sub>4</sub>) + ((((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * (1 - 2))),((S-bound c<sub>4</sub>) + ((((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * ((2 * j) - 2)))]| `2 is V14() real ext-real Element of REAL
(2 * n) - 1 is non empty V14() real V16() non even ext-real Element of REAL
(((2 * n) -' 2) + 1) - 2 is V14() real V16() ext-real Element of REAL
(2 * n) - 3 is V14() real V16() ext-real Element of REAL
((2 * j) -' 2) + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
2 * (n + 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 * (n + 1)) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
((2 * (n + 1)) -' 2) - 2 is V14() real V16() ext-real Element of REAL
(2 * n) + (2 * 1) is ordinal natural V14() real V16() even ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
((2 * n) + (2 * 1)) -' 2 is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(((2 * n) + (2 * 1)) -' 2) - 2 is V14() real V16() ext-real Element of REAL
(2 * n) - 2 is V14() real V16() ext-real Element of REAL
2 |^ C is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 |^ C) + 3 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(2 |^ (C + 1)) + 3 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
[(((2 * n) -' 2) + 1),1] is set
{(((2 * n) -' 2) + 1),1} is V104() V105() V106() V107() V108() V109() set
{(((2 * n) -' 2) + 1)} is V104() V105() V106() V107() V108() V109() set
{{(((2 * n) -' 2) + 1),1},{(((2 * n) -' 2) + 1)}} is set
(Gauge (c₄,(C + 1))) * ((((2 * n) -' 2) + 1),1) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c₄,(C + 1))) * ((((2 * n) -' 2) + 1),1)) `1 is V14() real ext-real Element of REAL
(((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * ((((2 * n) -' 2) + 1) - 2) is V14() real ext-real Element of REAL
(W-bound c<sub>4</sub>) + ((((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * ((((2 * n) -' 2) + 1) - 2)) is V14() real ext-real Element of REAL
(((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * (1 - 2) is V14() real ext-real Element of REAL
(S-bound c<sub>4</sub>) + ((((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * (1 - 2)) is V14() real ext-real Element of REAL
|[((W-bound c<sub>4</sub>) + ((((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * ((((2 * n) -' 2) + 1) - 2))),((S-bound c<sub>4</sub>) + ((((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * (1 - 2)))]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
|[((W-bound c<sub>4</sub>) + ((((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * ((((2 * n) -' 2) + 1) - 2))),((S-bound c<sub>4</sub>) + ((((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * (1 - 2)))]| `1 is V14() real ext-real Element of REAL
(Gauge (c₄,C)) * (n,1) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c₄,C)) * (n,1)) `1 is V14() real ext-real Element of REAL
(Gauge (c<sub>4</sub>,(C + 1))) * (((2 * n) -' 2),1) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c<sub>4</sub>,(C + 1))) * (((2 * n) -' 2),1)) `1 is V14() real ext-real Element of REAL
width (Gauge (c₄,C)) is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(Gauge (c₄,C)) * (1,j) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c₄,C)) * (1,j)) `2 is V14() real ext-real Element of REAL
(Gauge (c<sub>4</sub>,(C + 1))) * (1,((2 * j) -' 2)) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c<sub>4</sub>,(C + 1))) * (1,((2 * j) -' 2))) `2 is V14() real ext-real Element of REAL
(Gauge (c₄,(C + 1))) * (1,((2 * j) -' 1)) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c₄,(C + 1))) * (1,((2 * j) -' 1))) `2 is V14() real ext-real Element of REAL
(Gauge (c<sub>4</sub>,(C + 1))) * (1,(((2 * j) -' 1) + 1)) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c<sub>4</sub>,(C + 1))) * (1,(((2 * j) -' 1) + 1))) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( ((Gauge (c₄,(C + 1))) * (((2 * n) -' 2),1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= ((Gauge (c<sub>4</sub>,(C + 1))) * ((((2 * n) -' 2) + 1),1)) `1 & ((Gauge (c₄,(C + 1))) * (1,((2 * j) -' 1))) `2 <= b<sub>2</sub> & b<sub>2</sub> <= ((Gauge (c<sub>4</sub>,(C + 1))) * (1,(((2 * j) -' 1) + 1))) `2 ) } is set
(Gauge (c₄,(C + 1))) * (((2 * n) -' 1),1) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c₄,(C + 1))) * (((2 * n) -' 1),1)) `1 is V14() real ext-real Element of REAL
(2 * j) - 1 is non empty V14() real V16() non even ext-real Element of REAL
(((2 * j) -' 2) + 1) - 2 is V14() real V16() ext-real Element of REAL
[1,(((2 * j) -' 2) + 1)] is set
{1,(((2 * j) -' 2) + 1)} is V104() V105() V106() V107() V108() V109() set
{{1,(((2 * j) -' 2) + 1)},{1}} is set
(Gauge (c<sub>4</sub>,(C + 1))) * (1,(((2 * j) -' 2) + 1)) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c<sub>4</sub>,(C + 1))) * (1,(((2 * j) -' 2) + 1))) `2 is V14() real ext-real Element of REAL
(((N-bound c₄) - (S-bound c₄)) / (2 |^ (C + 1))) * ((((2 * j) -' 2) + 1) - 2) is V14() real ext-real Element of REAL
(S-bound c₄) + ((((N-bound c₄) - (S-bound c₄)) / (2 |^ (C + 1))) * ((((2 * j) -' 2) + 1) - 2)) is V14() real ext-real Element of REAL
|[((W-bound c₄) + ((((E-bound c₄) - (W-bound c₄)) / (2 |^ (C + 1))) * (1 - 2))),((S-bound c₄) + ((((N-bound c₄) - (S-bound c₄)) / (2 |^ (C + 1))) * ((((2 * j) -' 2) + 1) - 2)))]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
|[((W-bound c₄) + ((((E-bound c₄) - (W-bound c₄)) / (2 |^ (C + 1))) * (1 - 2))),((S-bound c₄) + ((((N-bound c₄) - (S-bound c₄)) / (2 |^ (C + 1))) * ((((2 * j) -' 2) + 1) - 2)))]| `2 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V14() real ext-real Element of REAL : ( ((Gauge (c<sub>4</sub>,(C + 1))) * (((2 * n) -' 2),1)) `1 <= b₁ & b₁ <= ((Gauge (c₄,(C + 1))) * ((((2 * n) -' 2) + 1),1)) `1 & ((Gauge (c<sub>4</sub>,(C + 1))) * (1,((2 * j) -' 2))) `2 <= b₂ & b₂ <= ((Gauge (c₄,(C + 1))) * (1,(((2 * j) -' 2) + 1))) `2 ) } is set
((2 * n) -' 1) + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
(Gauge (c<sub>4</sub>,(C + 1))) * ((((2 * n) -' 1) + 1),1) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c<sub>4</sub>,(C + 1))) * ((((2 * n) -' 1) + 1),1)) `1 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( ((Gauge (c₄,(C + 1))) * (((2 * n) -' 1),1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= ((Gauge (c<sub>4</sub>,(C + 1))) * ((((2 * n) -' 1) + 1),1)) `1 & ((Gauge (c₄,(C + 1))) * (1,((2 * j) -' 2))) `2 <= b<sub>2</sub> & b<sub>2</sub> <= ((Gauge (c<sub>4</sub>,(C + 1))) * (1,(((2 * j) -' 2) + 1))) `2 ) } is set
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( ((Gauge (c₄,(C + 1))) * (((2 * n) -' 1),1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= ((Gauge (c<sub>4</sub>,(C + 1))) * ((((2 * n) -' 1) + 1),1)) `1 & ((Gauge (c₄,(C + 1))) * (1,((2 * j) -' 1))) `2 <= b<sub>2</sub> & b<sub>2</sub> <= ((Gauge (c<sub>4</sub>,(C + 1))) * (1,(((2 * j) -' 1) + 1))) `2 ) } is set
(Gauge (c₄,C)) * ((n + 1),1) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c₄,C)) * ((n + 1),1)) `1 is V14() real ext-real Element of REAL
(Gauge (c<sub>4</sub>,C)) * (1,(j + 1)) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c<sub>4</sub>,C)) * (1,(j + 1))) `2 is V14() real ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V14() real ext-real Element of REAL : ( ((Gauge (c₄,C)) * (n,1)) `1 <= b<sub>1</sub> & b<sub>1</sub> <= ((Gauge (c<sub>4</sub>,C)) * ((n + 1),1)) `1 & ((Gauge (c₄,C)) * (1,j)) `2 <= b<sub>2</sub> & b<sub>2</sub> <= ((Gauge (c<sub>4</sub>,C)) * (1,(j + 1))) `2 ) } is set
[1,(j + 1)] is set
{1,(j + 1)} is V104() V105() V106() V107() V108() V109() set
{{1,(j + 1)},{1}} is set
Indices (Gauge (c₄,C)) is set
((E-bound c₄) - (W-bound c₄)) / (2 |^ C) is V14() real ext-real Element of REAL
(((E-bound c₄) - (W-bound c₄)) / (2 |^ C)) * (1 - 2) is V14() real ext-real Element of REAL
(W-bound c₄) + ((((E-bound c₄) - (W-bound c₄)) / (2 |^ C)) * (1 - 2)) is V14() real ext-real Element of REAL
((N-bound c₄) - (S-bound c₄)) / (2 |^ C) is V14() real ext-real Element of REAL
(j + 1) - 2 is V14() real V16() ext-real Element of REAL
(((N-bound c₄) - (S-bound c₄)) / (2 |^ C)) * ((j + 1) - 2) is V14() real ext-real Element of REAL
(S-bound c₄) + ((((N-bound c₄) - (S-bound c₄)) / (2 |^ C)) * ((j + 1) - 2)) is V14() real ext-real Element of REAL
|[((W-bound c₄) + ((((E-bound c₄) - (W-bound c₄)) / (2 |^ C)) * (1 - 2))),((S-bound c₄) + ((((N-bound c₄) - (S-bound c₄)) / (2 |^ C)) * ((j + 1) - 2)))]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
|[((W-bound c₄) + ((((E-bound c₄) - (W-bound c₄)) / (2 |^ C)) * (1 - 2))),((S-bound c₄) + ((((N-bound c₄) - (S-bound c₄)) / (2 |^ C)) * ((j + 1) - 2)))]| `2 is V14() real ext-real Element of REAL
(((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * (((2 * (j + 1)) -' 2) - 2) is V14() real ext-real Element of REAL
(S-bound c<sub>4</sub>) + ((((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * (((2 * (j + 1)) -' 2) - 2)) is V14() real ext-real Element of REAL
[(n + 1),1] is set
{(n + 1),1} is V104() V105() V106() V107() V108() V109() set
{(n + 1)} is V104() V105() V106() V107() V108() V109() set
{{(n + 1),1},{(n + 1)}} is set
(n + 1) - 2 is V14() real V16() ext-real Element of REAL
(((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ C)) * ((n + 1) - 2) is V14() real ext-real Element of REAL
(W-bound c<sub>4</sub>) + ((((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ C)) * ((n + 1) - 2)) is V14() real ext-real Element of REAL
(((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ C)) * (1 - 2) is V14() real ext-real Element of REAL
(S-bound c<sub>4</sub>) + ((((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ C)) * (1 - 2)) is V14() real ext-real Element of REAL
|[((W-bound c<sub>4</sub>) + ((((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ C)) * ((n + 1) - 2))),((S-bound c<sub>4</sub>) + ((((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ C)) * (1 - 2)))]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
|[((W-bound c<sub>4</sub>) + ((((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ C)) * ((n + 1) - 2))),((S-bound c<sub>4</sub>) + ((((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ C)) * (1 - 2)))]| `1 is V14() real ext-real Element of REAL
(((E-bound c₄) - (W-bound c₄)) / (2 |^ (C + 1))) * (((2 * (n + 1)) -' 2) - 2) is V14() real ext-real Element of REAL
(W-bound c₄) + ((((E-bound c₄) - (W-bound c₄)) / (2 |^ (C + 1))) * (((2 * (n + 1)) -' 2) - 2)) is V14() real ext-real Element of REAL
[(2 * n),1] is set
{(2 * n),1} is V104() V105() V106() V107() V108() V109() set
{(2 * n)} is V104() V105() V106() V107() V108() V109() set
{{(2 * n),1},{(2 * n)}} is set
(Gauge (c₄,(C + 1))) * ((2 * n),1) is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
((Gauge (c₄,(C + 1))) * ((2 * n),1)) `1 is V14() real ext-real Element of REAL
(((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * ((2 * n) - 2) is V14() real ext-real Element of REAL
(W-bound c<sub>4</sub>) + ((((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * ((2 * n) - 2)) is V14() real ext-real Element of REAL
|[((W-bound c<sub>4</sub>) + ((((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * ((2 * n) - 2))),((S-bound c<sub>4</sub>) + ((((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * (1 - 2)))]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
|[((W-bound c<sub>4</sub>) + ((((E-bound c<sub>4</sub>) - (W-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * ((2 * n) - 2))),((S-bound c<sub>4</sub>) + ((((N-bound c<sub>4</sub>) - (S-bound c<sub>4</sub>)) / (2 |^ (C + 1))) * (1 - 2)))]| `1 is V14() real ext-real Element of REAL
a is set
m is V14() real ext-real Element of REAL
q is V14() real ext-real Element of REAL
|[m,q]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
a is set
(((E-bound c₄) - (W-bound c₄)) / (2 |^ (C + 1))) * ((2 * n) - 3) is V14() real ext-real Element of REAL
(W-bound c₄) + ((((E-bound c₄) - (W-bound c₄)) / (2 |^ (C + 1))) * ((2 * n) - 3)) is V14() real ext-real Element of REAL
m is V14() real ext-real Element of REAL
q is V14() real ext-real Element of REAL
|[m,q]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
m is V14() real ext-real Element of REAL
q is V14() real ext-real Element of REAL
|[m,q]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
m is V14() real ext-real Element of REAL
q is V14() real ext-real Element of REAL
|[m,q]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
m is V14() real ext-real Element of REAL
q is V14() real ext-real Element of REAL
|[m,q]| is V38(2) FinSequence-like V95() Element of the U1 of (TOP-REAL 2)
n is ordinal natural V14() real V16() ext-real non negative V103() V104() V105() V106() V107() V108() V109() Element of NAT
n + 1 is non empty ordinal natural V14() real V16() ext-real positive non negative V103() V104() V105() V106()