REAL is V86() V87() V88() V92() set
NAT is V86() V87() V88() V89() V90() V91() V92() Element of bool REAL
bool REAL is set
COMPLEX is V86() V92() set
NAT is V86() V87() V88() V89() V90() V91() V92() set
bool NAT is set
bool NAT is set
INT is V86() V87() V88() V89() V90() V92() set
RAT is V86() V87() V88() V89() V92() set
1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[:1,1:] is V1() V5( RAT ) V5( INT ) V75() V76() V77() V78() set
bool [:1,1:] is set
[:[:1,1:],1:] is V1() V5( RAT ) V5( INT ) V75() V76() V77() V78() set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is V1() V75() V76() V77() set
bool [:[:1,1:],REAL:] is set
[:REAL,REAL:] is V1() V75() V76() V77() set
[:[:REAL,REAL:],REAL:] is V1() V75() V76() V77() set
bool [:[:REAL,REAL:],REAL:] is set
2 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[:2,2:] is V1() V5( RAT ) V5( INT ) V75() V76() V77() V78() set
[:[:2,2:],REAL:] is V1() V75() V76() V77() set
bool [:[:2,2:],REAL:] is set
bool [:REAL,REAL:] is set
TOP-REAL 2 is non empty TopSpace-like V124() V149() V150() V151() V152() V153() V154() V155() V161() L15()
the carrier of (TOP-REAL 2) is non empty set
K274( the carrier of (TOP-REAL 2)) is functional non empty FinSequence-membered M11( the carrier of (TOP-REAL 2))
bool the carrier of (TOP-REAL 2) is set
[: the carrier of (TOP-REAL 2),REAL:] is V1() V75() V76() V77() set
bool [: the carrier of (TOP-REAL 2),REAL:] is set
{} is set
the V1() non-empty empty-yielding V5( RAT ) functional empty FinSequence-like FinSequence-membered V75() V76() V77() V78() V86() V87() V88() V89() V90() V91() V92() set is V1() non-empty empty-yielding V5( RAT ) functional empty FinSequence-like FinSequence-membered V75() V76() V77() V78() V86() V87() V88() V89() V90() V91() V92() set
3 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
0 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
C is set
K274(C) is functional non empty FinSequence-membered M11(C)
<*> C is V1() non-empty empty-yielding V4( NAT ) V5(C) Function-like functional empty V28() FinSequence-like FinSubsequence-like FinSequence-membered V75() V76() V77() V78() V86() V87() V88() V89() V90() V91() V92() FinSequence of C
j is V1() V4( NAT ) V5(K274(C)) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of K274(C)
dom (<*> C) is V1() non-empty empty-yielding V5( RAT ) functional empty FinSequence-like FinSequence-membered V75() V76() V77() V78() V86() V87() V88() V89() V90() V91() V92() Element of bool NAT
Indices j is set
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(<*> C) /. G is Element of C
p is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
p + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[W,S] is set
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
N is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[E,N] is set
(<*> C) /. p is Element of C
j * (W,S) is Element of C
(<*> C) /. (p + 1) is Element of C
j * (E,N) is Element of C
W - E is V21() V22() ext-real set
abs (W - E) is V21() V22() ext-real Element of REAL
S - N is V21() V22() ext-real set
abs (S - N) is V21() V22() ext-real Element of REAL
(abs (W - E)) + (abs (S - N)) is V21() V22() ext-real Element of REAL
C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j is non empty set
K274(j) is functional non empty FinSequence-membered M11(j)
n is V1() V4( NAT ) V5(j) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of j
n /^ C is V1() V4( NAT ) V5(j) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of j
G is V1() V4( NAT ) V5(K274(j)) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of K274(j)
dom n is V86() V87() V88() V89() V90() V91() Element of bool NAT
Indices G is set
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
dom (n /^ C) is V86() V87() V88() V89() V90() V91() Element of bool NAT
W + C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
n /. (W + C) is Element of j
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[S,E] is set
G * (S,E) is Element of j
N is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
EW is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[N,EW] is set
(n /^ C) /. W is Element of j
G * (N,EW) is Element of j
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(n /^ C) /. W is Element of j
(n /^ C) /. (W + 1) is Element of j
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[S,E] is set
G * (S,E) is Element of j
N is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
S - N is V21() V22() ext-real set
abs (S - N) is V21() V22() ext-real Element of REAL
EW is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[N,EW] is set
G * (N,EW) is Element of j
E - EW is V21() V22() ext-real set
abs (E - EW) is V21() V22() ext-real Element of REAL
(abs (S - N)) + (abs (E - EW)) is V21() V22() ext-real set
W + C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(W + 1) + C is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(W + C) + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
n /. (W + C) is Element of j
n /. ((W + C) + 1) is Element of j
C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
C + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j is set
K274(j) is functional non empty FinSequence-membered M11(j)
n is V1() V4( NAT ) V5(j) Function-like V28() FinSequence-like FinSubsequence-like FinSequence of j
len n is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
n /. C is Element of j
n /. (C + 1) is Element of j
G is V1() V4( NAT ) V5(K274(j)) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of K274(j)
Indices G is set
dom n is V86() V87() V88() V89() V90() V91() Element of bool NAT
p is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[p,W] is set
G * (p,W) is Element of j
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[S,E] is set
G * (S,E) is Element of j
p - S is V21() V22() ext-real set
abs (p - S) is V21() V22() ext-real Element of REAL
W - E is V21() V22() ext-real set
abs (W - E) is V21() V22() ext-real Element of REAL
(abs (p - S)) + (abs (W - E)) is V21() V22() ext-real Element of REAL
- (p - S) is V21() V22() ext-real set
S + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
p + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
- (W - E) is V21() V22() ext-real set
E + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
S + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
p + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
E + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
S + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
p + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
E + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
C is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
j is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
GoB j is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
dom j is non empty V86() V87() V88() V89() V90() V91() Element of bool NAT
Indices (GoB j) is set
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j /. G is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
G + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j /. G is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
j /. (G + 1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
p is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[p,W] is set
(GoB j) * (p,W) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
p - S is V21() V22() ext-real set
abs (p - S) is V21() V22() ext-real Element of REAL
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[S,E] is set
(GoB j) * (S,E) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
W - E is V21() V22() ext-real set
abs (W - E) is V21() V22() ext-real Element of REAL
(abs (p - S)) + (abs (W - E)) is V21() V22() ext-real set
len (GoB j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
width (GoB j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
((GoB j) * (S,E)) `1 is V21() V22() ext-real Element of REAL
(GoB j) * (S,1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * (S,1)) `1 is V21() V22() ext-real Element of REAL
(GoB j) * (S,W) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * (S,W)) `1 is V21() V22() ext-real Element of REAL
((GoB j) * (S,E)) `2 is V21() V22() ext-real Element of REAL
(GoB j) * (1,E) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * (1,E)) `2 is V21() V22() ext-real Element of REAL
(GoB j) * (p,E) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * (p,E)) `2 is V21() V22() ext-real Element of REAL
len j is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
Indices C is set
N is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
EW is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[N,EW] is set
C * (N,EW) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
r is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
s is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[r,s] is set
C * (r,s) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
EW + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
N + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
r + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
s + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
len C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
width C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(C * (N,EW)) `1 is V21() V22() ext-real Element of REAL
C * (N,1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (N,1)) `1 is V21() V22() ext-real Element of REAL
(C * (r,s)) `1 is V21() V22() ext-real Element of REAL
C * (r,1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (r,1)) `1 is V21() V22() ext-real Element of REAL
(C * (N,EW)) `2 is V21() V22() ext-real Element of REAL
C * (1,EW) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (1,EW)) `2 is V21() V22() ext-real Element of REAL
C * (r,EW) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (r,EW)) `2 is V21() V22() ext-real Element of REAL
W + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
E + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
p + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
S + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
((GoB j) * (p,W)) `2 is V21() V22() ext-real Element of REAL
l is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
i9 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[i9,(W + 1)] is set
j /. l is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(GoB j) * (i9,(W + 1)) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * (i9,(W + 1))) `2 is V21() V22() ext-real Element of REAL
(GoB j) * (1,(W + 1)) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * (1,(W + 1))) `2 is V21() V22() ext-real Element of REAL
(GoB j) * (p,(W + 1)) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * (p,(W + 1))) `2 is V21() V22() ext-real Element of REAL
i19 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j19 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[i19,j19] is set
C * (i19,j19) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C * (i19,EW) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (i19,EW)) `2 is V21() V22() ext-real Element of REAL
(C * (r,s)) `2 is V21() V22() ext-real Element of REAL
C * (1,s) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (1,s)) `2 is V21() V22() ext-real Element of REAL
C * (i19,s) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (i19,s)) `2 is V21() V22() ext-real Element of REAL
(C * (i19,j19)) `2 is V21() V22() ext-real Element of REAL
E - W is V21() V22() ext-real set
abs (E - W) is V21() V22() ext-real Element of REAL
((GoB j) * (p,W)) `1 is V21() V22() ext-real Element of REAL
l is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
i9 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[(p + 1),i9] is set
j /. l is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(GoB j) * ((p + 1),i9) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * ((p + 1),i9)) `1 is V21() V22() ext-real Element of REAL
(GoB j) * ((p + 1),1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * ((p + 1),1)) `1 is V21() V22() ext-real Element of REAL
(GoB j) * ((p + 1),W) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * ((p + 1),W)) `1 is V21() V22() ext-real Element of REAL
i19 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j19 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[i19,j19] is set
C * (i19,j19) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C * (N,j19) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (N,j19)) `1 is V21() V22() ext-real Element of REAL
C * (r,j19) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (r,j19)) `1 is V21() V22() ext-real Element of REAL
(C * (i19,j19)) `1 is V21() V22() ext-real Element of REAL
S - p is V21() V22() ext-real set
abs (S - p) is V21() V22() ext-real Element of REAL
((GoB j) * (p,W)) `1 is V21() V22() ext-real Element of REAL
l is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
i9 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[(S + 1),i9] is set
j /. l is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(GoB j) * ((S + 1),i9) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * ((S + 1),i9)) `1 is V21() V22() ext-real Element of REAL
(GoB j) * ((S + 1),1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * ((S + 1),1)) `1 is V21() V22() ext-real Element of REAL
(GoB j) * ((S + 1),W) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * ((S + 1),W)) `1 is V21() V22() ext-real Element of REAL
(GoB j) * ((S + 1),E) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * ((S + 1),E)) `1 is V21() V22() ext-real Element of REAL
i19 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j19 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[i19,j19] is set
C * (i19,j19) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C * (N,j19) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (N,j19)) `1 is V21() V22() ext-real Element of REAL
C * (r,j19) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (r,j19)) `1 is V21() V22() ext-real Element of REAL
(C * (i19,j19)) `1 is V21() V22() ext-real Element of REAL
((GoB j) * (p,W)) `2 is V21() V22() ext-real Element of REAL
l is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
i9 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[i9,(E + 1)] is set
j /. l is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(GoB j) * (i9,(E + 1)) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * (i9,(E + 1))) `2 is V21() V22() ext-real Element of REAL
(GoB j) * (1,(E + 1)) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * (1,(E + 1))) `2 is V21() V22() ext-real Element of REAL
(GoB j) * (S,(E + 1)) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * (S,(E + 1))) `2 is V21() V22() ext-real Element of REAL
(GoB j) * (p,(E + 1)) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((GoB j) * (p,(E + 1))) `2 is V21() V22() ext-real Element of REAL
i19 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j19 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[i19,j19] is set
C * (i19,j19) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C * (i19,EW) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (i19,EW)) `2 is V21() V22() ext-real Element of REAL
(C * (r,s)) `2 is V21() V22() ext-real Element of REAL
C * (1,s) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (1,s)) `2 is V21() V22() ext-real Element of REAL
C * (i19,s) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (i19,s)) `2 is V21() V22() ext-real Element of REAL
(C * (i19,j19)) `2 is V21() V22() ext-real Element of REAL
n is V16() V20() V21() V22() ext-real non negative set
n + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
len j is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j /. n is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(j /. n) `1 is V21() V22() ext-real Element of REAL
j /. (n + 1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(j /. (n + 1)) `1 is V21() V22() ext-real Element of REAL
(j /. n) `2 is V21() V22() ext-real Element of REAL
(j /. (n + 1)) `2 is V21() V22() ext-real Element of REAL
Indices C is set
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
p is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[G,p] is set
C * (G,p) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[W,S] is set
C * (W,S) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
p + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
G + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
S + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
len C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
width C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(C * (G,p)) `2 is V21() V22() ext-real Element of REAL
C * (1,p) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (1,p)) `2 is V21() V22() ext-real Element of REAL
(C * (G,p)) `1 is V21() V22() ext-real Element of REAL
C * (G,1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(C * (G,1)) `1 is V21() V22() ext-real Element of REAL
C is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
j is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len j is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
dom j is non empty V86() V87() V88() V89() V90() V91() Element of bool NAT
Indices C is set
j /. 1 is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
n is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[n,G] is set
C * (n,G) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
1 + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j /. 2 is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
p is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[p,W] is set
C * (p,W) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
j . 1 is set
j . 2 is set
n - p is V21() V22() ext-real set
abs (n - p) is V21() V22() ext-real Element of REAL
G - W is V21() V22() ext-real set
abs (G - W) is V21() V22() ext-real Element of REAL
(abs (n - p)) + (abs (G - W)) is V21() V22() ext-real Element of REAL
C is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
Indices C is set
j is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
<*j*> is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V28() V35(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
n is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len n is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
n /. (len n) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
n ^ <*j*> is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V28() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom n is non empty V86() V87() V88() V89() V90() V91() Element of bool NAT
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
G + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
p is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[p,W] is set
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[S,E] is set
n /. G is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C * (p,W) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
n /. (G + 1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C * (S,E) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
p - S is V21() V22() ext-real set
abs (p - S) is V21() V22() ext-real Element of REAL
W - E is V21() V22() ext-real set
abs (W - E) is V21() V22() ext-real Element of REAL
(abs (p - S)) + (abs (W - E)) is V21() V22() ext-real Element of REAL
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
dom <*j*> is non empty V86() V87() V88() V89() V90() V91() Element of bool NAT
G + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
len <*j*> is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
1 + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
<*j*> /. G is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
<*j*> /. (G + 1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
p is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[p,W] is set
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[S,E] is set
C * (p,W) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C * (S,E) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
p - S is V21() V22() ext-real set
abs (p - S) is V21() V22() ext-real Element of REAL
W - E is V21() V22() ext-real set
abs (W - E) is V21() V22() ext-real Element of REAL
(abs (p - S)) + (abs (W - E)) is V21() V22() ext-real Element of REAL
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
p is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[G,p] is set
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[W,S] is set
C * (G,p) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
<*j*> /. 1 is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C * (W,S) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
W - G is V21() V22() ext-real set
abs (W - G) is V21() V22() ext-real Element of REAL
S - p is V21() V22() ext-real set
abs (S - p) is V21() V22() ext-real Element of REAL
(abs (W - G)) + (abs (S - p)) is V21() V22() ext-real Element of REAL
G - W is V21() V22() ext-real set
abs (G - W) is V21() V22() ext-real Element of REAL
(abs (G - W)) + (abs (S - p)) is V21() V22() ext-real Element of REAL
p - S is V21() V22() ext-real set
abs (p - S) is V21() V22() ext-real Element of REAL
(abs (G - W)) + (abs (p - S)) is V21() V22() ext-real Element of REAL
dom (n ^ <*j*>) is non empty V86() V87() V88() V89() V90() V91() Element of bool NAT
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
G + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
p is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[p,W] is set
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[S,E] is set
(n ^ <*j*>) /. G is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C * (p,W) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(n ^ <*j*>) /. (G + 1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C * (S,E) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
p - S is V21() V22() ext-real set
abs (p - S) is V21() V22() ext-real Element of REAL
W - E is V21() V22() ext-real set
abs (W - E) is V21() V22() ext-real Element of REAL
(abs (p - S)) + (abs (W - E)) is V21() V22() ext-real Element of REAL
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
n /. G is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
p is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[p,W] is set
C * (p,W) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[S,E] is set
(n ^ <*j*>) /. G is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C * (S,E) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
p is V16() V20() V21() V22() ext-real non negative set
(len n) + p is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
p is V16() V20() V21() V22() ext-real non negative set
(len n) + p is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[W,S] is set
C * (W,S) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
W is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[W,S] is set
C * (W,S) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
N is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[E,N] is set
<*j*> /. p is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(n ^ <*j*>) /. G is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C * (E,N) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
C + j is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
n is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
G is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
len G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
width G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
cell (G,C,n) is Element of bool the carrier of (TOP-REAL 2)
v_strip (G,C) is Element of bool the carrier of (TOP-REAL 2)
h_strip (G,n) is Element of bool the carrier of (TOP-REAL 2)
(v_strip (G,C)) /\ (h_strip (G,n)) is Element of bool the carrier of (TOP-REAL 2)
cell (G,(C + j),n) is Element of bool the carrier of (TOP-REAL 2)
v_strip (G,(C + j)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip (G,(C + j))) /\ (h_strip (G,n)) is Element of bool the carrier of (TOP-REAL 2)
(cell (G,C,n)) /\ (cell (G,(C + j),n)) is Element of bool the carrier of (TOP-REAL 2)
p is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
G * ((C + j),1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(G * ((C + j),1)) `1 is V21() V22() ext-real Element of REAL
(C + j) + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
G * (((C + j) + 1),1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(G * (((C + j) + 1),1)) `1 is V21() V22() ext-real Element of REAL
G * (1,n) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(G * (1,n)) `2 is V21() V22() ext-real Element of REAL
n + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
G * (1,(n + 1)) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(G * (1,(n + 1))) `2 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( (G * ((C + j),1)) `1 <= b1 & b1 <= (G * (((C + j) + 1),1)) `1 & (G * (1,n)) `2 <= b2 & b2 <= (G * (1,(n + 1))) `2 ) } is set
W is V21() V22() ext-real Element of REAL
S is V21() V22() ext-real Element of REAL
|[W,S]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
1 + 0 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
G * (1,1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(G * (1,1)) `1 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( b1 <= (G * (1,1)) `1 & (G * (1,n)) `2 <= b2 & b2 <= (G * (1,(n + 1))) `2 ) } is set
E is V21() V22() ext-real Element of REAL
N is V21() V22() ext-real Element of REAL
|[E,N]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
p `1 is V21() V22() ext-real Element of REAL
G * (j,1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(G * (j,1)) `1 is V21() V22() ext-real Element of REAL
G * (C,1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(G * (C,1)) `1 is V21() V22() ext-real Element of REAL
C + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
G * ((C + 1),1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(G * ((C + 1),1)) `1 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( (G * (C,1)) `1 <= b1 & b1 <= (G * ((C + 1),1)) `1 & (G * (1,n)) `2 <= b2 & b2 <= (G * (1,(n + 1))) `2 ) } is set
E is V21() V22() ext-real Element of REAL
N is V21() V22() ext-real Element of REAL
|[E,N]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
j + C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
p `1 is V21() V22() ext-real Element of REAL
C is non empty compact Element of bool the carrier of (TOP-REAL 2)
E-bound C is V21() V22() ext-real Element of REAL
W-bound C is V21() V22() ext-real Element of REAL
C is non empty compact Element of bool the carrier of (TOP-REAL 2)
N-bound C is V21() V22() ext-real Element of REAL
S-bound C is V21() V22() ext-real Element of REAL
C is Element of bool the carrier of (TOP-REAL 2)
W-bound C is V21() V22() ext-real Element of REAL
E-bound C is V21() V22() ext-real Element of REAL
(E-bound C) - (W-bound C) is V21() V22() ext-real Element of REAL
j is V16() V20() V21() V22() ext-real non negative set
2 |^ j is V16() V20() V21() V22() ext-real non negative Element of REAL
((E-bound C) - (W-bound C)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
S-bound C is V21() V22() ext-real Element of REAL
N-bound C is V21() V22() ext-real Element of REAL
(N-bound C) - (S-bound C) is V21() V22() ext-real Element of REAL
((N-bound C) - (S-bound C)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
(2 |^ j) + 3 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
n is V1() V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular Matrix of (2 |^ j) + 3,(2 |^ j) + 3, the carrier of (TOP-REAL 2)
Indices n is set
len n is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
width n is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
G is V16() V20() V21() V22() ext-real non negative set
p is V16() V20() V21() V22() ext-real non negative set
[G,p] is set
n * (G,p) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
G - 2 is V21() V22() ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2) is V21() V22() ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2)) is V21() V22() ext-real Element of REAL
p - 2 is V21() V22() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ j)) * (p - 2) is V21() V22() ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (p - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (p - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
n is V1() V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of K274( the carrier of (TOP-REAL 2))
len n is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
width n is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
Indices n is set
G is V1() V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of K274( the carrier of (TOP-REAL 2))
len G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
width G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
Indices G is set
p is V16() V20() V21() V22() ext-real non negative set
W is V16() V20() V21() V22() ext-real non negative set
[p,W] is set
n * (p,W) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
p - 2 is V21() V22() ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ j)) * (p - 2) is V21() V22() ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (p - 2)) is V21() V22() ext-real Element of REAL
W - 2 is V21() V22() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ j)) * (W - 2) is V21() V22() ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (W - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (p - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (W - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
G * (p,W) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
C is non empty Element of bool the carrier of (TOP-REAL 2)
j is V16() V20() V21() V22() ext-real non negative set
(C,j) is V1() V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of K274( the carrier of (TOP-REAL 2))
len (C,j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
2 |^ j is V16() V20() V21() V22() ext-real non negative Element of REAL
(2 |^ j) + 3 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
width (C,j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
Indices (C,j) is set
dom (C,j) is V86() V87() V88() V89() V90() V91() Element of bool NAT
Seg (width (C,j)) is V28() V35( width (C,j)) V86() V87() V88() V89() V90() V91() Element of bool NAT
[:(dom (C,j)),(Seg (width (C,j))):] is V1() V5( INT ) V5( RAT ) V75() V76() V77() V78() set
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
Line ((C,j),G) is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like M12( the carrier of (TOP-REAL 2),K275((width (C,j)), the carrier of (TOP-REAL 2)))
K275((width (C,j)), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M11( the carrier of (TOP-REAL 2))
X_axis (Line ((C,j),G)) is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like V75() V76() V77() FinSequence of REAL
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
dom (X_axis (Line ((C,j),G))) is V86() V87() V88() V89() V90() V91() Element of bool NAT
(X_axis (Line ((C,j),G))) . S is V21() V22() ext-real set
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(X_axis (Line ((C,j),G))) . E is V21() V22() ext-real set
len (Line ((C,j),G)) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
dom (Line ((C,j),G)) is V86() V87() V88() V89() V90() V91() Element of bool NAT
(Line ((C,j),G)) /. S is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(Line ((C,j),G)) . S is set
(C,j) * (G,S) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
[G,S] is set
(Line ((C,j),G)) /. E is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(Line ((C,j),G)) . E is set
(C,j) * (G,E) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
[G,E] is set
W-bound C is V21() V22() ext-real Element of REAL
E-bound C is V21() V22() ext-real Element of REAL
(E-bound C) - (W-bound C) is V21() V22() ext-real Element of REAL
((E-bound C) - (W-bound C)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
G - 2 is V21() V22() ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2) is V21() V22() ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2)) is V21() V22() ext-real Element of REAL
N-bound C is V21() V22() ext-real Element of REAL
S-bound C is V21() V22() ext-real Element of REAL
(N-bound C) - (S-bound C) is V21() V22() ext-real Element of REAL
((N-bound C) - (S-bound C)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
((Line ((C,j),G)) /. S) `1 is V21() V22() ext-real Element of REAL
S - 2 is V21() V22() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ j)) * (S - 2) is V21() V22() ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (S - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (S - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (S - 2)))]| `1 is V21() V22() ext-real Element of REAL
E - 2 is V21() V22() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ j)) * (E - 2) is V21() V22() ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (E - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (E - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (E - 2)))]| `1 is V21() V22() ext-real Element of REAL
((Line ((C,j),G)) /. E) `1 is V21() V22() ext-real Element of REAL
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
Col ((C,j),G) is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like M12( the carrier of (TOP-REAL 2),K275((len (C,j)), the carrier of (TOP-REAL 2)))
K275((len (C,j)), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M11( the carrier of (TOP-REAL 2))
Y_axis (Col ((C,j),G)) is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like V75() V76() V77() FinSequence of REAL
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
dom (Y_axis (Col ((C,j),G))) is V86() V87() V88() V89() V90() V91() Element of bool NAT
(Y_axis (Col ((C,j),G))) . S is V21() V22() ext-real set
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(Y_axis (Col ((C,j),G))) . E is V21() V22() ext-real set
len (Col ((C,j),G)) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
dom (Col ((C,j),G)) is V86() V87() V88() V89() V90() V91() Element of bool NAT
(Col ((C,j),G)) /. S is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(Col ((C,j),G)) . S is set
(C,j) * (S,G) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
[S,G] is set
(Col ((C,j),G)) /. E is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(Col ((C,j),G)) . E is set
(C,j) * (E,G) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
[E,G] is set
S-bound C is V21() V22() ext-real Element of REAL
N-bound C is V21() V22() ext-real Element of REAL
(N-bound C) - (S-bound C) is V21() V22() ext-real Element of REAL
((N-bound C) - (S-bound C)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
G - 2 is V21() V22() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ j)) * (G - 2) is V21() V22() ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (G - 2)) is V21() V22() ext-real Element of REAL
E-bound C is V21() V22() ext-real Element of REAL
W-bound C is V21() V22() ext-real Element of REAL
(E-bound C) - (W-bound C) is V21() V22() ext-real Element of REAL
((E-bound C) - (W-bound C)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
((Col ((C,j),G)) /. S) `2 is V21() V22() ext-real Element of REAL
S - 2 is V21() V22() ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ j)) * (S - 2) is V21() V22() ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (S - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (S - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (G - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (S - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (G - 2)))]| `2 is V21() V22() ext-real Element of REAL
E - 2 is V21() V22() ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ j)) * (E - 2) is V21() V22() ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (E - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (E - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (G - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (E - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (G - 2)))]| `2 is V21() V22() ext-real Element of REAL
((Col ((C,j),G)) /. E) `2 is V21() V22() ext-real Element of REAL
C is non empty compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
j is V16() V20() V21() V22() ext-real non negative set
(C,j) is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
Indices (C,j) is set
dom (C,j) is V86() V87() V88() V89() V90() V91() Element of bool NAT
width (C,j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
Seg (width (C,j)) is V28() V35( width (C,j)) V86() V87() V88() V89() V90() V91() Element of bool NAT
[:(dom (C,j)),(Seg (width (C,j))):] is V1() V5( INT ) V5( RAT ) V75() V76() V77() V78() set
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
Line ((C,j),G) is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like M12( the carrier of (TOP-REAL 2),K275((width (C,j)), the carrier of (TOP-REAL 2)))
K275((width (C,j)), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M11( the carrier of (TOP-REAL 2))
Y_axis (Line ((C,j),G)) is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like V75() V76() V77() FinSequence of REAL
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
K64((Y_axis (Line ((C,j),G)))) is set
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
K412((Y_axis (Line ((C,j),G))),E) is V21() V22() ext-real Element of REAL
K412((Y_axis (Line ((C,j),G))),S) is V21() V22() ext-real Element of REAL
dom (Y_axis (Line ((C,j),G))) is V86() V87() V88() V89() V90() V91() Element of bool NAT
len (Line ((C,j),G)) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
dom (Line ((C,j),G)) is V86() V87() V88() V89() V90() V91() Element of bool NAT
(Line ((C,j),G)) /. S is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(Line ((C,j),G)) . S is set
(C,j) * (G,S) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
[G,S] is set
(Line ((C,j),G)) /. E is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(Line ((C,j),G)) . E is set
(C,j) * (G,E) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
[G,E] is set
W-bound C is V21() V22() ext-real Element of REAL
E-bound C is V21() V22() ext-real Element of REAL
(E-bound C) - (W-bound C) is V21() V22() ext-real Element of REAL
2 |^ j is V16() V20() V21() V22() ext-real non negative Element of REAL
((E-bound C) - (W-bound C)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
G - 2 is V21() V22() ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2) is V21() V22() ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2)) is V21() V22() ext-real Element of REAL
N-bound C is V21() V22() ext-real Element of REAL
S-bound C is V21() V22() ext-real Element of REAL
(N-bound C) - (S-bound C) is V21() V22() ext-real Element of REAL
((N-bound C) - (S-bound C)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
(Y_axis (Line ((C,j),G))) . S is V21() V22() ext-real set
((Line ((C,j),G)) /. S) `2 is V21() V22() ext-real Element of REAL
S - 2 is V21() V22() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ j)) * (S - 2) is V21() V22() ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (S - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (S - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (S - 2)))]| `2 is V21() V22() ext-real Element of REAL
(Y_axis (Line ((C,j),G))) . E is V21() V22() ext-real set
((Line ((C,j),G)) /. E) `2 is V21() V22() ext-real Element of REAL
E - 2 is V21() V22() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ j)) * (E - 2) is V21() V22() ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (E - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (E - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (G - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (E - 2)))]| `2 is V21() V22() ext-real Element of REAL
G is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
Col ((C,j),G) is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V28() FinSequence-like FinSubsequence-like M12( the carrier of (TOP-REAL 2),K275((len (C,j)), the carrier of (TOP-REAL 2)))
len (C,j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
K275((len (C,j)), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M11( the carrier of (TOP-REAL 2))
X_axis (Col ((C,j),G)) is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like V75() V76() V77() FinSequence of REAL
S is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
K64((X_axis (Col ((C,j),G)))) is set
K412((X_axis (Col ((C,j),G))),S) is V21() V22() ext-real Element of REAL
E is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
K412((X_axis (Col ((C,j),G))),E) is V21() V22() ext-real Element of REAL
dom (X_axis (Col ((C,j),G))) is V86() V87() V88() V89() V90() V91() Element of bool NAT
len (Col ((C,j),G)) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
dom (Col ((C,j),G)) is V86() V87() V88() V89() V90() V91() Element of bool NAT
(Col ((C,j),G)) /. S is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(Col ((C,j),G)) . S is set
(C,j) * (S,G) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
[S,G] is set
(Col ((C,j),G)) /. E is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(Col ((C,j),G)) . E is set
(C,j) * (E,G) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
[E,G] is set
S-bound C is V21() V22() ext-real Element of REAL
N-bound C is V21() V22() ext-real Element of REAL
(N-bound C) - (S-bound C) is V21() V22() ext-real Element of REAL
2 |^ j is V16() V20() V21() V22() ext-real non negative Element of REAL
((N-bound C) - (S-bound C)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
G - 2 is V21() V22() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ j)) * (G - 2) is V21() V22() ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (G - 2)) is V21() V22() ext-real Element of REAL
E-bound C is V21() V22() ext-real Element of REAL
W-bound C is V21() V22() ext-real Element of REAL
(E-bound C) - (W-bound C) is V21() V22() ext-real Element of REAL
((E-bound C) - (W-bound C)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
(X_axis (Col ((C,j),G))) . S is V21() V22() ext-real set
((Col ((C,j),G)) /. S) `1 is V21() V22() ext-real Element of REAL
S - 2 is V21() V22() ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ j)) * (S - 2) is V21() V22() ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (S - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (S - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (G - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (S - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (G - 2)))]| `1 is V21() V22() ext-real Element of REAL
(X_axis (Col ((C,j),G))) . E is V21() V22() ext-real set
((Col ((C,j),G)) /. E) `1 is V21() V22() ext-real Element of REAL
E - 2 is V21() V22() ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ j)) * (E - 2) is V21() V22() ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (E - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (E - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (G - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ j)) * (E - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ j)) * (G - 2)))]| `1 is V21() V22() ext-real Element of REAL
4 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
C is non empty Element of bool the carrier of (TOP-REAL 2)
j is V16() V20() V21() V22() ext-real non negative set
(C,j) is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
len (C,j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
2 |^ j is V16() V20() V21() V22() ext-real non negative Element of REAL
(2 |^ j) + 3 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(j + 1) + 3 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j + 4 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
n is non empty Element of bool the carrier of (TOP-REAL 2)
(n,j) is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
len (n,j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(n,j) * (2,C) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((n,j) * (2,C)) `1 is V21() V22() ext-real Element of REAL
W-bound n is V21() V22() ext-real Element of REAL
S-bound n is V21() V22() ext-real Element of REAL
E-bound n is V21() V22() ext-real Element of REAL
N-bound n is V21() V22() ext-real Element of REAL
width (n,j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[2,C] is set
Indices (n,j) is set
(E-bound n) - (W-bound n) is V21() V22() ext-real Element of REAL
2 |^ j is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
((E-bound n) - (W-bound n)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
2 - 2 is V21() V22() ext-real Element of REAL
(((E-bound n) - (W-bound n)) / (2 |^ j)) * (2 - 2) is V21() V22() ext-real Element of REAL
(W-bound n) + ((((E-bound n) - (W-bound n)) / (2 |^ j)) * (2 - 2)) is V21() V22() ext-real Element of REAL
(N-bound n) - (S-bound n) is V21() V22() ext-real Element of REAL
((N-bound n) - (S-bound n)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
C - 2 is V21() V22() ext-real Element of REAL
(((N-bound n) - (S-bound n)) / (2 |^ j)) * (C - 2) is V21() V22() ext-real Element of REAL
(S-bound n) + ((((N-bound n) - (S-bound n)) / (2 |^ j)) * (C - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound n) + ((((E-bound n) - (W-bound n)) / (2 |^ j)) * (2 - 2))),((S-bound n) + ((((N-bound n) - (S-bound n)) / (2 |^ j)) * (C - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
n is non empty Element of bool the carrier of (TOP-REAL 2)
(n,j) is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
len (n,j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(len (n,j)) -' 1 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(n,j) * (((len (n,j)) -' 1),C) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((n,j) * (((len (n,j)) -' 1),C)) `1 is V21() V22() ext-real Element of REAL
E-bound n is V21() V22() ext-real Element of REAL
W-bound n is V21() V22() ext-real Element of REAL
S-bound n is V21() V22() ext-real Element of REAL
N-bound n is V21() V22() ext-real Element of REAL
2 |^ j is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(2 |^ j) + 3 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
width (n,j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
((len (n,j)) -' 1) - 2 is V21() V22() ext-real Element of REAL
(len (n,j)) - 1 is V21() V22() ext-real Element of REAL
((len (n,j)) - 1) - 2 is V21() V22() ext-real Element of REAL
[((len (n,j)) -' 1),C] is set
Indices (n,j) is set
(E-bound n) - (W-bound n) is V21() V22() ext-real Element of REAL
((E-bound n) - (W-bound n)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
(((E-bound n) - (W-bound n)) / (2 |^ j)) * (((len (n,j)) -' 1) - 2) is V21() V22() ext-real Element of REAL
(W-bound n) + ((((E-bound n) - (W-bound n)) / (2 |^ j)) * (((len (n,j)) -' 1) - 2)) is V21() V22() ext-real Element of REAL
(N-bound n) - (S-bound n) is V21() V22() ext-real Element of REAL
((N-bound n) - (S-bound n)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
C - 2 is V21() V22() ext-real Element of REAL
(((N-bound n) - (S-bound n)) / (2 |^ j)) * (C - 2) is V21() V22() ext-real Element of REAL
(S-bound n) + ((((N-bound n) - (S-bound n)) / (2 |^ j)) * (C - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound n) + ((((E-bound n) - (W-bound n)) / (2 |^ j)) * (((len (n,j)) -' 1) - 2))),((S-bound n) + ((((N-bound n) - (S-bound n)) / (2 |^ j)) * (C - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
(((E-bound n) - (W-bound n)) / (2 |^ j)) * (2 |^ j) is V21() V22() ext-real Element of REAL
(W-bound n) + ((((E-bound n) - (W-bound n)) / (2 |^ j)) * (2 |^ j)) is V21() V22() ext-real Element of REAL
(W-bound n) + ((E-bound n) - (W-bound n)) is V21() V22() ext-real Element of REAL
C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
n is non empty Element of bool the carrier of (TOP-REAL 2)
(n,j) is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
len (n,j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(n,j) * (C,2) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((n,j) * (C,2)) `2 is V21() V22() ext-real Element of REAL
S-bound n is V21() V22() ext-real Element of REAL
W-bound n is V21() V22() ext-real Element of REAL
E-bound n is V21() V22() ext-real Element of REAL
N-bound n is V21() V22() ext-real Element of REAL
width (n,j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
[C,2] is set
Indices (n,j) is set
(E-bound n) - (W-bound n) is V21() V22() ext-real Element of REAL
2 |^ j is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
((E-bound n) - (W-bound n)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
C - 2 is V21() V22() ext-real Element of REAL
(((E-bound n) - (W-bound n)) / (2 |^ j)) * (C - 2) is V21() V22() ext-real Element of REAL
(W-bound n) + ((((E-bound n) - (W-bound n)) / (2 |^ j)) * (C - 2)) is V21() V22() ext-real Element of REAL
(N-bound n) - (S-bound n) is V21() V22() ext-real Element of REAL
((N-bound n) - (S-bound n)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
2 - 2 is V21() V22() ext-real Element of REAL
(((N-bound n) - (S-bound n)) / (2 |^ j)) * (2 - 2) is V21() V22() ext-real Element of REAL
(S-bound n) + ((((N-bound n) - (S-bound n)) / (2 |^ j)) * (2 - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound n) + ((((E-bound n) - (W-bound n)) / (2 |^ j)) * (C - 2))),((S-bound n) + ((((N-bound n) - (S-bound n)) / (2 |^ j)) * (2 - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
C is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
j is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
n is non empty Element of bool the carrier of (TOP-REAL 2)
(n,j) is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
len (n,j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(len (n,j)) -' 1 is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(n,j) * (C,((len (n,j)) -' 1)) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((n,j) * (C,((len (n,j)) -' 1))) `2 is V21() V22() ext-real Element of REAL
N-bound n is V21() V22() ext-real Element of REAL
W-bound n is V21() V22() ext-real Element of REAL
S-bound n is V21() V22() ext-real Element of REAL
E-bound n is V21() V22() ext-real Element of REAL
2 |^ j is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(2 |^ j) + 3 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
width (n,j) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
((len (n,j)) -' 1) - 2 is V21() V22() ext-real Element of REAL
(len (n,j)) - 1 is V21() V22() ext-real Element of REAL
((len (n,j)) - 1) - 2 is V21() V22() ext-real Element of REAL
[C,((len (n,j)) -' 1)] is set
Indices (n,j) is set
(E-bound n) - (W-bound n) is V21() V22() ext-real Element of REAL
((E-bound n) - (W-bound n)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
C - 2 is V21() V22() ext-real Element of REAL
(((E-bound n) - (W-bound n)) / (2 |^ j)) * (C - 2) is V21() V22() ext-real Element of REAL
(W-bound n) + ((((E-bound n) - (W-bound n)) / (2 |^ j)) * (C - 2)) is V21() V22() ext-real Element of REAL
(N-bound n) - (S-bound n) is V21() V22() ext-real Element of REAL
((N-bound n) - (S-bound n)) / (2 |^ j) is V21() V22() ext-real Element of COMPLEX
(((N-bound n) - (S-bound n)) / (2 |^ j)) * (((len (n,j)) -' 1) - 2) is V21() V22() ext-real Element of REAL
(S-bound n) + ((((N-bound n) - (S-bound n)) / (2 |^ j)) * (((len (n,j)) -' 1) - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound n) + ((((E-bound n) - (W-bound n)) / (2 |^ j)) * (C - 2))),((S-bound n) + ((((N-bound n) - (S-bound n)) / (2 |^ j)) * (((len (n,j)) -' 1) - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
(((N-bound n) - (S-bound n)) / (2 |^ j)) * (2 |^ j) is V21() V22() ext-real Element of REAL
(S-bound n) + ((((N-bound n) - (S-bound n)) / (2 |^ j)) * (2 |^ j)) is V21() V22() ext-real Element of REAL
(S-bound n) + ((N-bound n) - (S-bound n)) is V21() V22() ext-real Element of REAL
C is non empty compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
j is V16() V20() V21() V22() ext-real non negative set
n is V16() V20() V21() V22() ext-real non negative set
(C,n) is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
len (C,n) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
cell ((C,n),j,(len (C,n))) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((C,n),j) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((C,n),(len (C,n))) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((C,n),j)) /\ (h_strip ((C,n),(len (C,n)))) is Element of bool the carrier of (TOP-REAL 2)
2 |^ n is V16() V20() V21() V22() ext-real non negative Element of REAL
1 + 2 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(2 |^ n) + (1 + 2) is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
width (C,n) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(cell ((C,n),j,(len (C,n)))) /\ C is Element of bool the carrier of (TOP-REAL 2)
p is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
W-bound C is V21() V22() ext-real Element of REAL
S-bound C is V21() V22() ext-real Element of REAL
E-bound C is V21() V22() ext-real Element of REAL
N-bound C is V21() V22() ext-real Element of REAL
(N-bound C) - (S-bound C) is V21() V22() ext-real Element of REAL
((N-bound C) - (S-bound C)) / (2 |^ n) is V21() V22() ext-real Element of COMPLEX
[1,(width (C,n))] is set
Indices (C,n) is set
(C,n) * (1,(width (C,n))) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(E-bound C) - (W-bound C) is V21() V22() ext-real Element of REAL
((E-bound C) - (W-bound C)) / (2 |^ n) is V21() V22() ext-real Element of COMPLEX
1 - 2 is V21() V22() ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2) is V21() V22() ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2)) is V21() V22() ext-real Element of REAL
(width (C,n)) - 2 is V21() V22() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) * ((width (C,n)) - 2) is V21() V22() ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((width (C,n)) - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((width (C,n)) - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
(((N-bound C) - (S-bound C)) / (2 |^ n)) * (2 |^ n) is V21() V22() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) * 1 is V21() V22() ext-real Element of REAL
((((N-bound C) - (S-bound C)) / (2 |^ n)) * (2 |^ n)) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * 1) is V21() V22() ext-real Element of REAL
((N-bound C) - (S-bound C)) + (((N-bound C) - (S-bound C)) / (2 |^ n)) is V21() V22() ext-real Element of REAL
((C,n) * (1,(width (C,n)))) `2 is V21() V22() ext-real Element of REAL
(N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) is V21() V22() ext-real Element of REAL
1 + 0 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
cell ((C,n),j,(width (C,n))) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((C,n),(width (C,n))) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((C,n),j)) /\ (h_strip ((C,n),(width (C,n)))) is Element of bool the carrier of (TOP-REAL 2)
(C,n) * (1,1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * (1,1)) `1 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( b1 <= ((C,n) * (1,1)) `1 & ((C,n) * (1,(width (C,n)))) `2 <= b2 ) } is set
r is V21() V22() ext-real Element of REAL
s is V21() V22() ext-real Element of REAL
|[r,s]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
p `2 is V21() V22() ext-real Element of REAL
cell ((C,n),j,(width (C,n))) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((C,n),(width (C,n))) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((C,n),j)) /\ (h_strip ((C,n),(width (C,n)))) is Element of bool the carrier of (TOP-REAL 2)
(C,n) * ((len (C,n)),1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * ((len (C,n)),1)) `1 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( ((C,n) * ((len (C,n)),1)) `1 <= b1 & ((C,n) * (1,(width (C,n)))) `2 <= b2 ) } is set
r is V21() V22() ext-real Element of REAL
s is V21() V22() ext-real Element of REAL
|[r,s]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
p `2 is V21() V22() ext-real Element of REAL
cell ((C,n),j,(width (C,n))) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((C,n),(width (C,n))) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((C,n),j)) /\ (h_strip ((C,n),(width (C,n)))) is Element of bool the carrier of (TOP-REAL 2)
(C,n) * (j,1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * (j,1)) `1 is V21() V22() ext-real Element of REAL
j + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(C,n) * ((j + 1),1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * ((j + 1),1)) `1 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( ((C,n) * (j,1)) `1 <= b1 & b1 <= ((C,n) * ((j + 1),1)) `1 & ((C,n) * (1,(width (C,n)))) `2 <= b2 ) } is set
r is V21() V22() ext-real Element of REAL
s is V21() V22() ext-real Element of REAL
|[r,s]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
p `2 is V21() V22() ext-real Element of REAL
C is non empty compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
j is V16() V20() V21() V22() ext-real non negative set
n is V16() V20() V21() V22() ext-real non negative set
(C,n) is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
len (C,n) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
cell ((C,n),(len (C,n)),j) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((C,n),(len (C,n))) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((C,n),j) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((C,n),(len (C,n)))) /\ (h_strip ((C,n),j)) is Element of bool the carrier of (TOP-REAL 2)
2 |^ n is V16() V20() V21() V22() ext-real non negative Element of REAL
1 + 2 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(2 |^ n) + (1 + 2) is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
width (C,n) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(cell ((C,n),(len (C,n)),j)) /\ C is Element of bool the carrier of (TOP-REAL 2)
p is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
W-bound C is V21() V22() ext-real Element of REAL
S-bound C is V21() V22() ext-real Element of REAL
E-bound C is V21() V22() ext-real Element of REAL
N-bound C is V21() V22() ext-real Element of REAL
(E-bound C) - (W-bound C) is V21() V22() ext-real Element of REAL
((E-bound C) - (W-bound C)) / (2 |^ n) is V21() V22() ext-real Element of COMPLEX
[(len (C,n)),1] is set
Indices (C,n) is set
(C,n) * ((len (C,n)),1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(len (C,n)) - 2 is V21() V22() ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ n)) * ((len (C,n)) - 2) is V21() V22() ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((len (C,n)) - 2)) is V21() V22() ext-real Element of REAL
(N-bound C) - (S-bound C) is V21() V22() ext-real Element of REAL
((N-bound C) - (S-bound C)) / (2 |^ n) is V21() V22() ext-real Element of COMPLEX
1 - 2 is V21() V22() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2) is V21() V22() ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((len (C,n)) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
(((E-bound C) - (W-bound C)) / (2 |^ n)) * (2 |^ n) is V21() V22() ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ n)) * 1 is V21() V22() ext-real Element of REAL
((((E-bound C) - (W-bound C)) / (2 |^ n)) * (2 |^ n)) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * 1) is V21() V22() ext-real Element of REAL
((E-bound C) - (W-bound C)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) is V21() V22() ext-real Element of REAL
((C,n) * ((len (C,n)),1)) `1 is V21() V22() ext-real Element of REAL
(E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ n)) is V21() V22() ext-real Element of REAL
1 + 0 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(C,n) * (1,1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * (1,1)) `2 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( ((C,n) * ((len (C,n)),1)) `1 <= b1 & b2 <= ((C,n) * (1,1)) `2 ) } is set
r is V21() V22() ext-real Element of REAL
s is V21() V22() ext-real Element of REAL
|[r,s]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
p `1 is V21() V22() ext-real Element of REAL
(C,n) * (1,(width (C,n))) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * (1,(width (C,n)))) `2 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( ((C,n) * ((len (C,n)),1)) `1 <= b1 & ((C,n) * (1,(width (C,n)))) `2 <= b2 ) } is set
r is V21() V22() ext-real Element of REAL
s is V21() V22() ext-real Element of REAL
|[r,s]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
p `1 is V21() V22() ext-real Element of REAL
(C,n) * (1,j) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * (1,j)) `2 is V21() V22() ext-real Element of REAL
j + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(C,n) * (1,(j + 1)) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * (1,(j + 1))) `2 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( ((C,n) * ((len (C,n)),1)) `1 <= b1 & ((C,n) * (1,j)) `2 <= b2 & b2 <= ((C,n) * (1,(j + 1))) `2 ) } is set
r is V21() V22() ext-real Element of REAL
s is V21() V22() ext-real Element of REAL
|[r,s]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
p `1 is V21() V22() ext-real Element of REAL
C is non empty compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
j is V16() V20() V21() V22() ext-real non negative set
n is V16() V20() V21() V22() ext-real non negative set
(C,n) is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
len (C,n) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
cell ((C,n),j,0) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((C,n),j) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((C,n),0) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((C,n),j)) /\ (h_strip ((C,n),0)) is Element of bool the carrier of (TOP-REAL 2)
width (C,n) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(cell ((C,n),j,0)) /\ C is Element of bool the carrier of (TOP-REAL 2)
p is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
W-bound C is V21() V22() ext-real Element of REAL
S-bound C is V21() V22() ext-real Element of REAL
E-bound C is V21() V22() ext-real Element of REAL
N-bound C is V21() V22() ext-real Element of REAL
(N-bound C) - (S-bound C) is V21() V22() ext-real Element of REAL
2 |^ n is V16() V20() V21() V22() ext-real non negative Element of REAL
((N-bound C) - (S-bound C)) / (2 |^ n) is V21() V22() ext-real Element of COMPLEX
[1,1] is set
Indices (C,n) is set
(C,n) * (1,1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
(E-bound C) - (W-bound C) is V21() V22() ext-real Element of REAL
((E-bound C) - (W-bound C)) / (2 |^ n) is V21() V22() ext-real Element of COMPLEX
1 - 2 is V21() V22() ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2) is V21() V22() ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2)) is V21() V22() ext-real Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2) is V21() V22() ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
((C,n) * (1,1)) `2 is V21() V22() ext-real Element of REAL
- 1 is V21() V22() ext-real non positive Element of REAL
(((N-bound C) - (S-bound C)) / (2 |^ n)) * (- 1) is V21() V22() ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (- 1)) is V21() V22() ext-real Element of REAL
0 * (- 1) is V21() V22() ext-real non positive Element of REAL
(S-bound C) + 0 is V21() V22() ext-real Element of REAL
1 + 0 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
((C,n) * (1,1)) `1 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( b1 <= ((C,n) * (1,1)) `1 & b2 <= ((C,n) * (1,1)) `2 ) } is set
r is V21() V22() ext-real Element of REAL
s is V21() V22() ext-real Element of REAL
|[r,s]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
p `2 is V21() V22() ext-real Element of REAL
(C,n) * ((len (C,n)),1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * ((len (C,n)),1)) `1 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( ((C,n) * ((len (C,n)),1)) `1 <= b1 & b2 <= ((C,n) * (1,1)) `2 ) } is set
r is V21() V22() ext-real Element of REAL
s is V21() V22() ext-real Element of REAL
|[r,s]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
p `2 is V21() V22() ext-real Element of REAL
(C,n) * (j,1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * (j,1)) `1 is V21() V22() ext-real Element of REAL
j + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(C,n) * ((j + 1),1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * ((j + 1),1)) `1 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( ((C,n) * (j,1)) `1 <= b1 & b1 <= ((C,n) * ((j + 1),1)) `1 & b2 <= ((C,n) * (1,1)) `2 ) } is set
r is V21() V22() ext-real Element of REAL
s is V21() V22() ext-real Element of REAL
|[r,s]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
p `2 is V21() V22() ext-real Element of REAL
C is non empty compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
j is V16() V20() V21() V22() ext-real non negative set
n is V16() V20() V21() V22() ext-real non negative set
(C,n) is V1() non empty-yielding V4( NAT ) V5(K274( the carrier of (TOP-REAL 2))) Function-like V28() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K274( the carrier of (TOP-REAL 2))
len (C,n) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
cell ((C,n),0,j) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((C,n),0) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((C,n),j) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((C,n),0)) /\ (h_strip ((C,n),j)) is Element of bool the carrier of (TOP-REAL 2)
width (C,n) is V16() V20() V21() V22() V26() ext-real non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(cell ((C,n),0,j)) /\ C is Element of bool the carrier of (TOP-REAL 2)
p is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
W-bound C is V21() V22() ext-real Element of REAL
S-bound C is V21() V22() ext-real Element of REAL
E-bound C is V21() V22() ext-real Element of REAL
N-bound C is V21() V22() ext-real Element of REAL
(E-bound C) - (W-bound C) is V21() V22() ext-real Element of REAL
2 |^ n is V16() V20() V21() V22() ext-real non negative Element of REAL
((E-bound C) - (W-bound C)) / (2 |^ n) is V21() V22() ext-real Element of COMPLEX
[1,1] is set
Indices (C,n) is set
(C,n) * (1,1) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
1 - 2 is V21() V22() ext-real Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2) is V21() V22() ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2)) is V21() V22() ext-real Element of REAL
(N-bound C) - (S-bound C) is V21() V22() ext-real Element of REAL
((N-bound C) - (S-bound C)) / (2 |^ n) is V21() V22() ext-real Element of COMPLEX
(((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2) is V21() V22() ext-real Element of REAL
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2)) is V21() V22() ext-real Element of REAL
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2)))]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
((C,n) * (1,1)) `1 is V21() V22() ext-real Element of REAL
- 1 is V21() V22() ext-real non positive Element of REAL
(((E-bound C) - (W-bound C)) / (2 |^ n)) * (- 1) is V21() V22() ext-real Element of REAL
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (- 1)) is V21() V22() ext-real Element of REAL
0 * (- 1) is V21() V22() ext-real non positive Element of REAL
(W-bound C) + 0 is V21() V22() ext-real Element of REAL
1 + 0 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
((C,n) * (1,1)) `2 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( b1 <= ((C,n) * (1,1)) `1 & b2 <= ((C,n) * (1,1)) `2 ) } is set
r is V21() V22() ext-real Element of REAL
s is V21() V22() ext-real Element of REAL
|[r,s]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
p `1 is V21() V22() ext-real Element of REAL
(C,n) * (1,(width (C,n))) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * (1,(width (C,n)))) `2 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( b1 <= ((C,n) * (1,1)) `1 & ((C,n) * (1,(width (C,n)))) `2 <= b2 ) } is set
r is V21() V22() ext-real Element of REAL
s is V21() V22() ext-real Element of REAL
|[r,s]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
p `1 is V21() V22() ext-real Element of REAL
(C,n) * (1,j) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * (1,j)) `2 is V21() V22() ext-real Element of REAL
j + 1 is non empty V16() V20() V21() V22() V26() ext-real positive non negative V85() V86() V87() V88() V89() V90() V91() Element of NAT
(C,n) * (1,(j + 1)) is V35(2) FinSequence-like V77() Element of the carrier of (TOP-REAL 2)
((C,n) * (1,(j + 1))) `2 is V21() V22() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V21() V22() ext-real Element of REAL : ( b1 <= ((C,n) * (1,1)) `1 & ((C,n) * (1,j)) `2 <= b2 & b2 <= ((C,n) * (1,(j + 1))) `2 ) } is set
r is V21() V22() ext-real Element of REAL
s is V21() V22() ext-real Element of REAL
|[r,s]| is V1() V4( NAT ) Function-like non empty V28() V35(2) FinSequence-like FinSubsequence-like V75() V76() V77() Element of the carrier of (TOP-REAL 2)
p `1 is V21() V22() ext-real Element of REAL