GOBOARD5

:: GOBOARD5 semantic presentation

REAL is non empty V33() V187() V188() V189() V193() set
NAT is V187() V188() V189() V190() V191() V192() V193() Element of bool REAL
bool REAL is set
INT is non empty V33() V187() V188() V189() V190() V191() V193() set
COMPLEX is non empty V33() V187() V193() set
NAT is V187() V188() V189() V190() V191() V192() V193() set
bool NAT is set
bool NAT is set
1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
2 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[:1,1:] is V5( RAT ) V5( INT ) V177() V178() V179() V180() set
RAT is non empty V33() V187() V188() V189() V190() V193() set
bool [:1,1:] is set
[:[:1,1:],1:] is V5( RAT ) V5( INT ) V177() V178() V179() V180() set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is V177() V178() V179() set
bool [:[:1,1:],REAL:] is set
[:REAL,REAL:] is V177() V178() V179() set
[:[:REAL,REAL:],REAL:] is V177() V178() V179() set
bool [:[:REAL,REAL:],REAL:] is set
[:2,2:] is V5( RAT ) V5( INT ) V177() V178() V179() V180() set
[:[:2,2:],REAL:] is V177() V178() V179() set
bool [:[:2,2:],REAL:] is set
bool [:REAL,REAL:] is set
TOP-REAL 2 is non empty V90() V121() V122() V123() V124() V125() V126() V127() TopSpace-like strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
bool the carrier of (TOP-REAL 2) is set
K227( the carrier of (TOP-REAL 2)) is functional non empty FinSequence-membered M10( the carrier of (TOP-REAL 2))
[:COMPLEX,COMPLEX:] is V177() set
bool [:COMPLEX,COMPLEX:] is set
[:COMPLEX,REAL:] is V177() V178() V179() set
bool [:COMPLEX,REAL:] is set
{} is set
the functional empty FinSequence-membered V187() V188() V189() V190() V191() V192() V193() set is functional empty FinSequence-membered V187() V188() V189() V190() V191() V192() V193() set
3 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
0 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
Seg 1 is non empty V33() 1 -element V187() V188() V189() V190() V191() V192() Element of bool NAT
{1} is V187() V188() V189() V190() V191() V192() set
Seg 2 is non empty V33() 2 -element V187() V188() V189() V190() V191() V192() Element of bool NAT
{1,2} is V187() V188() V189() V190() V191() V192() set
|[0,0]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
|[0,1]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
LSeg (|[0,0]|,|[0,1]|) is Element of bool the carrier of (TOP-REAL 2)
|[1,1]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
LSeg (|[0,1]|,|[1,1]|) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) is Element of bool the carrier of (TOP-REAL 2)
{|[0,1]|} is set
|[1,0]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
LSeg (|[0,0]|,|[1,0]|) is Element of bool the carrier of (TOP-REAL 2)
LSeg (|[1,0]|,|[1,1]|) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is Element of bool the carrier of (TOP-REAL 2)
{|[1,0]|} is set
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is Element of bool the carrier of (TOP-REAL 2)
{|[1,1]|} is set
4 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
5 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[:(Seg 2),(Seg 2):] is V5( INT ) V5( RAT ) V177() V178() V179() V180() set
[1,1] is set
{1,1} is V187() V188() V189() V190() V191() V192() set
{{1,1},{1}} is set
[1,2] is set
{{1,2},{1}} is set
[2,1] is set
{2,1} is V187() V188() V189() V190() V191() V192() set
{2} is V187() V188() V189() V190() V191() V192() set
{{2,1},{2}} is set
[2,2] is set
{2,2} is V187() V188() V189() V190() V191() V192() set
{{2,2},{2}} is set
f is ext-real non negative V20() V24() V25() V32() set
k is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
len k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k * (f,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(k * (f,1)) `1 is ext-real V25() V32() Element of REAL
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k * ((f + 1),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(k * ((f + 1),1)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (k * (f,1)) `1 <= b₁ & b₁ <= (k * ((f + 1),1)) `1 ) } is set
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : (k * (f,1)) `1 <= b₁ } is set
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₁ <= (k * ((f + 1),1)) `1 } is set
j1 is set
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
j1 is set
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
j1 is set
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
i1 is Element of bool the carrier of (TOP-REAL 2)
width k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k * (1,f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(k * (1,f)) `2 is ext-real V25() V32() Element of REAL
k * (1,(f + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(k * (1,(f + 1))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (k * (1,f)) `2 <= b₂ & b₂ <= (k * (1,(f + 1))) `2 ) } is set
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : (k * (1,f)) `2 <= b₂ } is set
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₂ <= (k * (1,(f + 1))) `2 } is set
j1 is set
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
j1 is set
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
j1 is set
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
i1 is Element of bool the carrier of (TOP-REAL 2)
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * (f,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (f,k)) `2 is ext-real V25() V32() Element of REAL
i1 * (1,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (1,k)) `2 is ext-real V25() V32() Element of REAL
Seg (width i1) is V33() width i1 -element V187() V188() V189() V190() V191() V192() Element of bool NAT
Col (i1,k) is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K228((len i1), the carrier of (TOP-REAL 2)))
K228((len i1), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
Y_axis (Col (i1,k)) is V1() V4( NAT ) V5( REAL ) Function-like V33() FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
dom i1 is V187() V188() V189() V190() V191() V192() Element of bool NAT
j1 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
dom j1 is V187() V188() V189() V190() V191() V192() Element of bool NAT
j1 /. 1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 . 1 is set
j1 /. f is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 . f is set
len (Y_axis (Col (i1,k))) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
dom (Y_axis (Col (i1,k))) is V187() V188() V189() V190() V191() V192() Element of bool NAT
(j1 /. f) `2 is ext-real V25() V32() Element of REAL
(Y_axis (Col (i1,k))) . f is ext-real V25() V32() set
(Y_axis (Col (i1,k))) . 1 is ext-real V25() V32() set
(j1 /. 1) `2 is ext-real V25() V32() Element of REAL
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * (f,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (f,k)) `1 is ext-real V25() V32() Element of REAL
i1 * (f,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (f,1)) `1 is ext-real V25() V32() Element of REAL
dom i1 is V187() V188() V189() V190() V191() V192() Element of bool NAT
Line (i1,f) is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K228((width i1), the carrier of (TOP-REAL 2)))
K228((width i1), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
X_axis (Line (i1,f)) is V1() V4( NAT ) V5( REAL ) Function-like V33() FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
Seg (width i1) is V33() width i1 -element V187() V188() V189() V190() V191() V192() Element of bool NAT
j1 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
dom j1 is V187() V188() V189() V190() V191() V192() Element of bool NAT
j1 /. 1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 . 1 is set
j1 /. k is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 . k is set
len (X_axis (Line (i1,f))) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
dom (X_axis (Line (i1,f))) is V187() V188() V189() V190() V191() V192() Element of bool NAT
(j1 /. k) `1 is ext-real V25() V32() Element of REAL
(X_axis (Line (i1,f))) . k is ext-real V25() V32() set
(X_axis (Line (i1,f))) . 1 is ext-real V25() V32() set
(j1 /. 1) `1 is ext-real V25() V32() Element of REAL
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
width j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 * (i1,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(j1 * (i1,k)) `1 is ext-real V25() V32() Element of REAL
j1 * (f,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(j1 * (f,k)) `1 is ext-real V25() V32() Element of REAL
Seg (width j1) is V33() width j1 -element V187() V188() V189() V190() V191() V192() Element of bool NAT
Col (j1,k) is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K228((len j1), the carrier of (TOP-REAL 2)))
K228((len j1), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
X_axis (Col (j1,k)) is V1() V4( NAT ) V5( REAL ) Function-like V33() FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
dom j1 is V187() V188() V189() V190() V191() V192() Element of bool NAT
i2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len i2 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
dom i2 is V187() V188() V189() V190() V191() V192() Element of bool NAT
i2 /. f is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i2 . f is set
i2 /. i1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i2 . i1 is set
len (X_axis (Col (j1,k))) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
dom (X_axis (Col (j1,k))) is V187() V188() V189() V190() V191() V192() Element of bool NAT
(i2 /. f) `1 is ext-real V25() V32() Element of REAL
(X_axis (Col (j1,k))) . f is ext-real V25() V32() set
(X_axis (Col (j1,k))) . i1 is ext-real V25() V32() set
(i2 /. i1) `1 is ext-real V25() V32() Element of REAL
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
width j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 * (i1,f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(j1 * (i1,f)) `2 is ext-real V25() V32() Element of REAL
j1 * (i1,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(j1 * (i1,k)) `2 is ext-real V25() V32() Element of REAL
dom j1 is V187() V188() V189() V190() V191() V192() Element of bool NAT
Line (j1,i1) is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K228((width j1), the carrier of (TOP-REAL 2)))
K228((width j1), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
Y_axis (Line (j1,i1)) is V1() V4( NAT ) V5( REAL ) Function-like V33() FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
Seg (width j1) is V33() width j1 -element V187() V188() V189() V190() V191() V192() Element of bool NAT
i2 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len i2 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
dom i2 is V187() V188() V189() V190() V191() V192() Element of bool NAT
i2 /. k is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i2 . k is set
i2 /. f is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i2 . f is set
len (Y_axis (Line (j1,i1))) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
dom (Y_axis (Line (j1,i1))) is V187() V188() V189() V190() V191() V192() Element of bool NAT
(i2 /. k) `2 is ext-real V25() V32() Element of REAL
(Y_axis (Line (j1,i1))) . k is ext-real V25() V32() set
(Y_axis (Line (j1,i1))) . f is ext-real V25() V32() set
(i2 /. f) `2 is ext-real V25() V32() Element of REAL
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(i1,k) is Element of bool the carrier of (TOP-REAL 2)
i1 * (f,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (f,k)) `2 is ext-real V25() V32() Element of REAL
i1 * (f,(k + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (f,(k + 1))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (i1 * (f,k)) `2 <= b₂ & b₂ <= (i1 * (f,(k + 1))) `2 ) } is set
i1 * (1,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (1,k)) `2 is ext-real V25() V32() Element of REAL
i1 * (1,(k + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (1,(k + 1))) `2 is ext-real V25() V32() Element of REAL
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
len f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
width f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(f,(width f)) is Element of bool the carrier of (TOP-REAL 2)
f * (k,(width f)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (k,(width f))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : (f * (k,(width f))) `2 <= b₂ } is set
f * (1,(width f)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,(width f))) `2 is ext-real V25() V32() Element of REAL
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
len f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(f,0) is Element of bool the carrier of (TOP-REAL 2)
f * (k,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (k,1)) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₂ <= (f * (k,1)) `2 } is set
width f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * (1,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,1)) `2 is ext-real V25() V32() Element of REAL
1 + 0 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * (1,(1 + 0)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,(1 + 0))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₂ <= (f * (1,(1 + 0))) `2 } is set
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(i1,k) is Element of bool the carrier of (TOP-REAL 2)
i1 * (k,f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (k,f)) `1 is ext-real V25() V32() Element of REAL
i1 * ((k + 1),f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * ((k + 1),f)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (i1 * (k,f)) `1 <= b₁ & b₁ <= (i1 * ((k + 1),f)) `1 ) } is set
i1 * (k,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (k,1)) `1 is ext-real V25() V32() Element of REAL
i1 * ((k + 1),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * ((k + 1),1)) `1 is ext-real V25() V32() Element of REAL
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
width f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(f,(len f)) is Element of bool the carrier of (TOP-REAL 2)
f * ((len f),k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * ((len f),k)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : (f * ((len f),k)) `1 <= b₁ } is set
f * ((len f),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * ((len f),1)) `1 is ext-real V25() V32() Element of REAL
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
width f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(f,0) is Element of bool the carrier of (TOP-REAL 2)
f * (1,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,k)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₁ <= (f * (1,k)) `1 } is set
len f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * (1,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,1)) `1 is ext-real V25() V32() Element of REAL
1 + 0 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * (1,(1 + 0)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,(1 + 0))) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₁ <= (f * (1,(1 + 0))) `1 } is set
k is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
f is ext-real non negative V20() V24() V25() V32() set
(k,f) is Element of bool the carrier of (TOP-REAL 2)
i1 is ext-real non negative V20() V24() V25() V32() set
(k,i1) is Element of bool the carrier of (TOP-REAL 2)
(k,f) /\ (k,i1) is Element of bool the carrier of (TOP-REAL 2)
<*|[0,0]|,|[0,1]|,|[1,1]|*> is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V33() 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
<*|[1,0]|,|[0,0]|*> is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len <*|[0,0]|,|[0,1]|,|[1,1]|*> is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len <*|[1,0]|,|[0,0]|*> is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
<*|[0,0]|,|[0,1]|,|[1,1]|*> ^ <*|[1,0]|,|[0,0]|*> is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V33() 3 + 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
3 + 2 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len (<*|[0,0]|,|[0,1]|,|[1,1]|*> ^ <*|[1,0]|,|[0,0]|*>) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
3 + 2 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom <*|[0,0]|,|[0,1]|,|[1,1]|*> is V187() V188() V189() V190() V191() V192() Element of bool NAT
i1 /. 1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
<*|[0,0]|,|[0,1]|,|[1,1]|*> /. 1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 /. 2 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
<*|[0,0]|,|[0,1]|,|[1,1]|*> /. 2 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
dom i1 is V187() V188() V189() V190() V191() V192() Element of bool NAT
i1 . 1 is set
i1 . 2 is set
i1 /. 3 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
<*|[0,0]|,|[0,1]|,|[1,1]|*> /. 3 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
dom <*|[1,0]|,|[0,0]|*> is V187() V188() V189() V190() V191() V192() Element of bool NAT
3 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 /. (3 + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
<*|[1,0]|,|[0,0]|*> /. 1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 /. (3 + 2) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
<*|[1,0]|,|[0,0]|*> /. 2 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
LSeg (i1,1) is Element of bool the carrier of (TOP-REAL 2)
2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
LSeg (i1,2) is Element of bool the carrier of (TOP-REAL 2)
LSeg (i1,3) is Element of bool the carrier of (TOP-REAL 2)
LSeg (|[1,1]|,|[1,0]|) is Element of bool the carrier of (TOP-REAL 2)
4 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
LSeg (i1,4) is Element of bool the carrier of (TOP-REAL 2)
LSeg (|[1,0]|,|[0,0]|) is Element of bool the carrier of (TOP-REAL 2)
j1 is ext-real non negative V20() V24() V25() V32() set
j1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 /. j1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. j1) `1 is ext-real V25() V32() Element of REAL
i1 /. (j1 + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. (j1 + 1)) `1 is ext-real V25() V32() Element of REAL
(i1 /. j1) `2 is ext-real V25() V32() Element of REAL
(i1 /. (j1 + 1)) `2 is ext-real V25() V32() Element of REAL
(i1 /. 1) `1 is ext-real V25() V32() Element of REAL
i1 /. (1 + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. (1 + 1)) `1 is ext-real V25() V32() Element of REAL
(i1 /. 2) `2 is ext-real V25() V32() Element of REAL
i1 /. (2 + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. (2 + 1)) `2 is ext-real V25() V32() Element of REAL
(i1 /. 3) `1 is ext-real V25() V32() Element of REAL
(i1 /. (3 + 1)) `1 is ext-real V25() V32() Element of REAL
i1 /. 4 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. 4) `2 is ext-real V25() V32() Element of REAL
i1 /. (4 + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. (4 + 1)) `2 is ext-real V25() V32() Element of REAL
j1 is ext-real non negative V20() V24() V25() V32() set
j1 + 2 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
LSeg (i1,j1) is Element of bool the carrier of (TOP-REAL 2)
j1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
LSeg (i1,(j1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (i1,j1)) /\ (LSeg (i1,(j1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
i1 /. (j1 + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
{(i1 /. (j1 + 1))} is set
1 + 2 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
2 + 2 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 /. (len i1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
LSeg (i1,j1) is Element of bool the carrier of (TOP-REAL 2)
i2 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
LSeg (i1,i2) is Element of bool the carrier of (TOP-REAL 2)
0 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(j1 + 1) + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 + (1 + 1) is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 + 2 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
2 + 2 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
1 + 2 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
0 + 2 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(LSeg (i1,j1)) /\ (LSeg (i1,i2)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (i1,j1)) /\ (LSeg (i1,i2)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (i1,j1)) /\ (LSeg (i1,i2)) is Element of bool the carrier of (TOP-REAL 2)
<*0,0,1*> is V1() V4( NAT ) V5( REAL ) Function-like non empty V33() 3 -element FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
<*1,0*> is V1() V4( NAT ) V5( REAL ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
<*0,0,1*> ^ <*1,0*> is V1() V4( NAT ) V5( REAL ) Function-like non empty V33() 3 + 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
len <*0,0,1*> is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len <*1,0*> is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j2 is V1() V4( NAT ) V5( REAL ) Function-like V33() FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
len j2 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
dom <*0,0,1*> is V187() V188() V189() V190() V191() V192() Element of bool NAT
j2 . 1 is ext-real V25() V32() set
<*0,0,1*> . 1 is ext-real V25() V32() set
j2 . 2 is ext-real V25() V32() set
<*0,0,1*> . 2 is ext-real V25() V32() set
j2 . 3 is ext-real V25() V32() set
<*0,0,1*> . 3 is ext-real V25() V32() set
dom <*1,0*> is V187() V188() V189() V190() V191() V192() Element of bool NAT
j2 . (3 + 1) is ext-real V25() V32() set
<*1,0*> . 1 is ext-real V25() V32() set
j2 . (3 + 2) is ext-real V25() V32() set
<*1,0*> . 2 is ext-real V25() V32() set
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
dom j2 is V187() V188() V189() V190() V191() V192() Element of bool NAT
j2 . i is ext-real V25() V32() set
i1 /. i is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. i) `1 is ext-real V25() V32() Element of REAL
j2 . i is ext-real V25() V32() set
i1 /. i is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. i) `1 is ext-real V25() V32() Element of REAL
j2 . i is ext-real V25() V32() set
i1 /. i is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. i) `1 is ext-real V25() V32() Element of REAL
j2 . i is ext-real V25() V32() set
i1 /. i is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. i) `1 is ext-real V25() V32() Element of REAL
j2 . i is ext-real V25() V32() set
i1 /. i is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. i) `1 is ext-real V25() V32() Element of REAL
X_axis i1 is V1() V4( NAT ) V5( REAL ) Function-like non empty V33() FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
rng <*0,0,1*> is V187() V188() V189() set
{0,0,1} is V187() V188() V189() V190() V191() V192() set
{0,1} is V187() V188() V189() V190() V191() V192() set
rng <*1,0*> is V187() V188() V189() set
rng j2 is V187() V188() V189() set
{0,1} \/ {0,1} is V187() V188() V189() V190() V191() V192() set
<*0,1*> is V1() V4( NAT ) V5( REAL ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
rng <*0,1*> is V187() V188() V189() set
len <*0,1*> is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
card (rng j2) is cardinal set
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
K83(<*0,1*>) is set
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
K441(<*0,1*>,i) is ext-real V25() V32() Element of REAL
K441(<*0,1*>,i) is ext-real V25() V32() Element of REAL
dom <*0,1*> is V187() V188() V189() V190() V191() V192() Element of bool NAT
<*0,1*> . i is ext-real V25() V32() set
<*0,1*> . i is ext-real V25() V32() set
Incr (X_axis i1) is V1() V4( NAT ) V5( REAL ) Function-like one-to-one non empty V33() FinSequence-like FinSubsequence-like V177() V178() V179() increasing V183() FinSequence of REAL
<*0,1,1*> is V1() V4( NAT ) V5( REAL ) Function-like non empty V33() 3 -element FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
<*0,0*> is V1() V4( NAT ) V5( REAL ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
<*0,1,1*> ^ <*0,0*> is V1() V4( NAT ) V5( REAL ) Function-like non empty V33() 3 + 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
len <*0,1,1*> is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len <*0,0*> is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j is V1() V4( NAT ) V5( REAL ) Function-like V33() FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
len j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
dom <*0,1,1*> is V187() V188() V189() V190() V191() V192() Element of bool NAT
j . 1 is ext-real V25() V32() set
<*0,1,1*> . 1 is ext-real V25() V32() set
j . 2 is ext-real V25() V32() set
<*0,1,1*> . 2 is ext-real V25() V32() set
j . 3 is ext-real V25() V32() set
<*0,1,1*> . 3 is ext-real V25() V32() set
dom <*0,0*> is V187() V188() V189() V190() V191() V192() Element of bool NAT
j . (3 + 1) is ext-real V25() V32() set
<*0,0*> . 1 is ext-real V25() V32() set
j . (3 + 2) is ext-real V25() V32() set
<*0,0*> . 2 is ext-real V25() V32() set
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
dom j is V187() V188() V189() V190() V191() V192() Element of bool NAT
j . j is ext-real V25() V32() set
i1 /. j is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. j) `2 is ext-real V25() V32() Element of REAL
j . j is ext-real V25() V32() set
i1 /. j is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. j) `2 is ext-real V25() V32() Element of REAL
j . j is ext-real V25() V32() set
i1 /. j is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. j) `2 is ext-real V25() V32() Element of REAL
j . j is ext-real V25() V32() set
i1 /. j is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. j) `2 is ext-real V25() V32() Element of REAL
j . j is ext-real V25() V32() set
i1 /. j is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 /. j) `2 is ext-real V25() V32() Element of REAL
Y_axis i1 is V1() V4( NAT ) V5( REAL ) Function-like non empty V33() FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
rng <*0,1,1*> is V187() V188() V189() set
{0,1,1} is V187() V188() V189() V190() V191() V192() set
{1,1,0} is V187() V188() V189() V190() V191() V192() set
rng <*0,0*> is V187() V188() V189() set
{0,0} is V187() V188() V189() V190() V191() V192() set
{0} is V187() V188() V189() V190() V191() V192() Element of bool REAL
rng j is V187() V188() V189() set
{0,1} \/ {0} is V187() V188() V189() V190() V191() V192() set
card (rng j) is cardinal set
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
K83(<*0,1*>) is set
n is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
K441(<*0,1*>,n) is ext-real V25() V32() Element of REAL
K441(<*0,1*>,j) is ext-real V25() V32() Element of REAL
dom <*0,1*> is V187() V188() V189() V190() V191() V192() Element of bool NAT
<*0,1*> . j is ext-real V25() V32() set
<*0,1*> . n is ext-real V25() V32() set
Incr (Y_axis i1) is V1() V4( NAT ) V5( REAL ) Function-like one-to-one non empty V33() FinSequence-like FinSubsequence-like V177() V178() V179() increasing V183() FinSequence of REAL
(|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|) is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of (TOP-REAL 2)
len ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len (Incr (X_axis i1)) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
width ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len (Incr (Y_axis i1)) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
Indices ((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) is set
n is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
m is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[n,m] is set
{n,m} is V187() V188() V189() V190() V191() V192() set
{n} is V187() V188() V189() V190() V191() V192() set
{{n,m},{n}} is set
((|[0,0]|,|[0,1]|) ][ (|[1,0]|,|[1,1]|)) * (n,m) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(Incr (X_axis i1)) . n is ext-real V25() V32() set
(Incr (Y_axis i1)) . m is ext-real V25() V32() set
|[((Incr (X_axis i1)) . n),((Incr (Y_axis i1)) . m)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
[:{1,2},{1,2}:] is V5( INT ) V5( RAT ) V177() V178() V179() V180() set
{[1,1],[1,2],[2,1],[2,2]} is set
<*0,1*> . 1 is ext-real V25() V32() set
<*0,1*> . 2 is ext-real V25() V32() set
GoB ((Incr (X_axis i1)),(Incr (Y_axis i1))) is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
GoB i1 is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
(GoB i1) * (1,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB i1) * (1,2) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB i1) * (2,2) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 /. 4 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB i1) * (2,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
Indices (GoB i1) is set
n is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 /. n is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
n is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
n + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 /. n is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 /. (n + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
m is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[m,k] is set
{m,k} is V187() V188() V189() V190() V191() V192() set
{m} is V187() V188() V189() V190() V191() V192() set
{{m,k},{m}} is set
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i,j] is set
{i,j} is V187() V188() V189() V190() V191() V192() set
{i} is V187() V188() V189() V190() V191() V192() set
{{i,j},{i}} is set
(GoB i1) * (m,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB i1) * (i,j) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
m - i is ext-real V25() V32() set
abs (m - i) is ext-real V25() V32() Element of REAL
k - j is ext-real V25() V32() set
abs (k - j) is ext-real V25() V32() Element of REAL
(abs (m - i)) + (abs (k - j)) is ext-real V25() V32() set
k is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
X_axis k is V1() V4( NAT ) V5( REAL ) Function-like V33() FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
dom (X_axis k) is V187() V188() V189() V190() V191() V192() Element of bool NAT
dom k is V187() V188() V189() V190() V191() V192() Element of bool NAT
len (X_axis k) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
Y_axis k is V1() V4( NAT ) V5( REAL ) Function-like V33() FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
dom (Y_axis k) is V187() V188() V189() V190() V191() V192() Element of bool NAT
dom k is V187() V188() V189() V190() V191() V192() Element of bool NAT
len (Y_axis k) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom k is V187() V188() V189() V190() V191() V192() Element of bool NAT
GoB k is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
Indices (GoB k) is set
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k /. f is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
X_axis k is V1() V4( NAT ) V5( REAL ) Function-like non empty V33() FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
Incr (X_axis k) is V1() V4( NAT ) V5( REAL ) Function-like one-to-one non empty V33() FinSequence-like FinSubsequence-like V177() V178() V179() increasing V183() FinSequence of REAL
Y_axis k is V1() V4( NAT ) V5( REAL ) Function-like non empty V33() FinSequence-like FinSubsequence-like V177() V178() V179() FinSequence of REAL
Incr (Y_axis k) is V1() V4( NAT ) V5( REAL ) Function-like one-to-one non empty V33() FinSequence-like FinSubsequence-like V177() V178() V179() increasing V183() FinSequence of REAL
GoB ((Incr (X_axis k)),(Incr (Y_axis k))) is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
(k /. f) `1 is ext-real V25() V32() Element of REAL
(k /. f) `2 is ext-real V25() V32() Element of REAL
dom (X_axis k) is V187() V188() V189() V190() V191() V192() Element of bool NAT
(X_axis k) . f is ext-real V25() V32() set
rng (X_axis k) is V187() V188() V189() set
rng (Incr (X_axis k)) is V187() V188() V189() set
dom (Incr (X_axis k)) is V187() V188() V189() V190() V191() V192() Element of bool NAT
i2 is ext-real non negative V20() V24() V25() V32() set
(Incr (X_axis k)) . i2 is ext-real V25() V32() set
dom (Y_axis k) is V187() V188() V189() V190() V191() V192() Element of bool NAT
(Y_axis k) . f is ext-real V25() V32() set
rng (Y_axis k) is V187() V188() V189() set
rng (Incr (Y_axis k)) is V187() V188() V189() set
dom (Incr (Y_axis k)) is V187() V188() V189() V190() V191() V192() Element of bool NAT
j2 is ext-real non negative V20() V24() V25() V32() set
(Incr (Y_axis k)) . j2 is ext-real V25() V32() set
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i,i] is set
{i,i} is V187() V188() V189() V190() V191() V192() set
{i} is V187() V188() V189() V190() V191() V192() set
{{i,i},{i}} is set
(GoB k) * (i,i) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
len (Incr (X_axis k)) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
Seg (len (Incr (X_axis k))) is V33() len (Incr (X_axis k)) -element V187() V188() V189() V190() V191() V192() Element of bool NAT
len (GoB ((Incr (X_axis k)),(Incr (Y_axis k)))) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
Seg (len (GoB ((Incr (X_axis k)),(Incr (Y_axis k))))) is V33() len (GoB ((Incr (X_axis k)),(Incr (Y_axis k)))) -element V187() V188() V189() V190() V191() V192() Element of bool NAT
dom (GoB k) is V187() V188() V189() V190() V191() V192() Element of bool NAT
len (Incr (Y_axis k)) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
Seg (len (Incr (Y_axis k))) is V33() len (Incr (Y_axis k)) -element V187() V188() V189() V190() V191() V192() Element of bool NAT
width (GoB ((Incr (X_axis k)),(Incr (Y_axis k)))) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
Seg (width (GoB ((Incr (X_axis k)),(Incr (Y_axis k))))) is V33() width (GoB ((Incr (X_axis k)),(Incr (Y_axis k)))) -element V187() V188() V189() V190() V191() V192() Element of bool NAT
width (GoB k) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
Seg (width (GoB k)) is V33() width (GoB k) -element V187() V188() V189() V190() V191() V192() Element of bool NAT
[:(dom (GoB k)),(Seg (width (GoB k))):] is V5( INT ) V5( RAT ) V177() V178() V179() V180() set
(Incr (X_axis k)) . i is ext-real V25() V32() set
(Incr (Y_axis k)) . i is ext-real V25() V32() set
|[((Incr (X_axis k)) . i),((Incr (Y_axis k)) . i)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
k is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V33() FinSequence-like FinSubsequence-like () FinSequence of the carrier of (TOP-REAL 2)
dom k is V187() V188() V189() V190() V191() V192() Element of bool NAT
GoB k is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
Indices (GoB k) is set
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k /. f is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
k /. (f + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i1,j1] is set
{i1,j1} is V187() V188() V189() V190() V191() V192() set
{i1} is V187() V188() V189() V190() V191() V192() set
{{i1,j1},{i1}} is set
i2 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j2 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i2,j2] is set
{i2,j2} is V187() V188() V189() V190() V191() V192() set
{i2} is V187() V188() V189() V190() V191() V192() set
{{i2,j2},{i2}} is set
(GoB k) * (i1,j1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB k) * (i2,j2) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 - i2 is ext-real V25() V32() set
abs (i1 - i2) is ext-real V25() V32() Element of REAL
j1 - j2 is ext-real V25() V32() set
abs (j1 - j2) is ext-real V25() V32() Element of REAL
(abs (i1 - i2)) + (abs (j1 - j2)) is ext-real V25() V32() Element of REAL
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V33() FinSequence-like FinSubsequence-like circular special unfolded () () FinSequence of the carrier of (TOP-REAL 2)
len k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
dom k is V187() V188() V189() V190() V191() V192() Element of bool NAT
GoB k is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
Indices (GoB k) is set
k /. f is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i1,j1] is set
{i1,j1} is V187() V188() V189() V190() V191() V192() set
{i1} is V187() V188() V189() V190() V191() V192() set
{{i1,j1},{i1}} is set
(GoB k) * (i1,j1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
k /. (f + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i2 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j2 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i2,j2] is set
{i2,j2} is V187() V188() V189() V190() V191() V192() set
{i2} is V187() V188() V189() V190() V191() V192() set
{{i2,j2},{i2}} is set
(GoB k) * (i2,j2) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 - i2 is ext-real V25() V32() set
abs (i1 - i2) is ext-real V25() V32() Element of REAL
j1 - j2 is ext-real V25() V32() set
abs (j1 - j2) is ext-real V25() V32() Element of REAL
(abs (i1 - i2)) + (abs (j1 - j2)) is ext-real V25() V32() Element of REAL
- (i1 - i2) is ext-real V25() V32() set
i2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
- (j1 - j2) is ext-real V25() V32() set
j2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i1,j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) /\ ((GoB k),j1) is Element of bool the carrier of (TOP-REAL 2)
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i,i] is set
{i,i} is V187() V188() V189() V190() V191() V192() set
{i} is V187() V188() V189() V190() V191() V192() set
{{i,i},{i}} is set
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[j,j] is set
{j,j} is V187() V188() V189() V190() V191() V192() set
{j} is V187() V188() V189() V190() V191() V192() set
{{j,j},{j}} is set
(GoB k) * (i,i) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB k) * (j,j) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),j,j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) /\ ((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),(i -' 1),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) /\ ((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
j1 -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i1,(j1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(j1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) /\ ((GoB k),(j1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i,i] is set
{i,i} is V187() V188() V189() V190() V191() V192() set
{i} is V187() V188() V189() V190() V191() V192() set
{{i,i},{i}} is set
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[j,j] is set
{j,j} is V187() V188() V189() V190() V191() V192() set
{j} is V187() V188() V189() V190() V191() V192() set
{{j,j},{j}} is set
(GoB k) * (i,i) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB k) * (j,j) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),j,j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) /\ ((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),(i -' 1),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) /\ ((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i2,j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i2) /\ ((GoB k),j2) is Element of bool the carrier of (TOP-REAL 2)
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i,i] is set
{i,i} is V187() V188() V189() V190() V191() V192() set
{i} is V187() V188() V189() V190() V191() V192() set
{{i,i},{i}} is set
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[j,j] is set
{j,j} is V187() V188() V189() V190() V191() V192() set
{j} is V187() V188() V189() V190() V191() V192() set
{{j,j},{j}} is set
(GoB k) * (i,i) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB k) * (j,j) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),j,j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) /\ ((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),(i -' 1),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) /\ ((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
i1 -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),(i1 -' 1),j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i1 -' 1)) /\ ((GoB k),j2) is Element of bool the carrier of (TOP-REAL 2)
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i,i] is set
{i,i} is V187() V188() V189() V190() V191() V192() set
{i} is V187() V188() V189() V190() V191() V192() set
{{i,i},{i}} is set
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[j,j] is set
{j,j} is V187() V188() V189() V190() V191() V192() set
{j} is V187() V188() V189() V190() V191() V192() set
{{j,j},{j}} is set
(GoB k) * (i,i) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB k) * (j,j) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),j,j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) /\ ((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),(i -' 1),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) /\ ((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
i is Element of bool the carrier of (TOP-REAL 2)
i is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1,j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) /\ ((GoB k),j1) is Element of bool the carrier of (TOP-REAL 2)
j1 -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i1,(j1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(j1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) /\ ((GoB k),(j1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i2,j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i2) /\ ((GoB k),j2) is Element of bool the carrier of (TOP-REAL 2)
i1 -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),(i1 -' 1),j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i1 -' 1)) /\ ((GoB k),j2) is Element of bool the carrier of (TOP-REAL 2)
i1 -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),(i1 -' 1),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i1 -' 1)) /\ ((GoB k),j1) is Element of bool the carrier of (TOP-REAL 2)
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i,i] is set
{i,i} is V187() V188() V189() V190() V191() V192() set
{i} is V187() V188() V189() V190() V191() V192() set
{{i,i},{i}} is set
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[j,j] is set
{j,j} is V187() V188() V189() V190() V191() V192() set
{j} is V187() V188() V189() V190() V191() V192() set
{{j,j},{j}} is set
(GoB k) * (i,i) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB k) * (j,j) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),(i -' 1),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) /\ ((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),j,(j -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(j -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) /\ ((GoB k),(j -' 1)) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1,j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) /\ ((GoB k),j1) is Element of bool the carrier of (TOP-REAL 2)
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i,i] is set
{i,i} is V187() V188() V189() V190() V191() V192() set
{i} is V187() V188() V189() V190() V191() V192() set
{{i,i},{i}} is set
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[j,j] is set
{j,j} is V187() V188() V189() V190() V191() V192() set
{j} is V187() V188() V189() V190() V191() V192() set
{{j,j},{j}} is set
(GoB k) * (i,i) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB k) * (j,j) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),(i -' 1),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) /\ ((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),j,(j -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(j -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) /\ ((GoB k),(j -' 1)) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
j2 -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i2,(j2 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(j2 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i2) /\ ((GoB k),(j2 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i,i] is set
{i,i} is V187() V188() V189() V190() V191() V192() set
{i} is V187() V188() V189() V190() V191() V192() set
{{i,i},{i}} is set
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[j,j] is set
{j,j} is V187() V188() V189() V190() V191() V192() set
{j} is V187() V188() V189() V190() V191() V192() set
{{j,j},{j}} is set
(GoB k) * (i,i) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB k) * (j,j) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),(i -' 1),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) /\ ((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),j,(j -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(j -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) /\ ((GoB k),(j -' 1)) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1,j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) /\ ((GoB k),j2) is Element of bool the carrier of (TOP-REAL 2)
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i,i] is set
{i,i} is V187() V188() V189() V190() V191() V192() set
{i} is V187() V188() V189() V190() V191() V192() set
{{i,i},{i}} is set
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[j,j] is set
{j,j} is V187() V188() V189() V190() V191() V192() set
{j} is V187() V188() V189() V190() V191() V192() set
{{j,j},{j}} is set
(GoB k) * (i,i) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB k) * (j,j) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),(i -' 1),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i -' 1)) /\ ((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),i) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),j,(j -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(j -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) /\ ((GoB k),(j -' 1)) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i,j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i) /\ ((GoB k),j) is Element of bool the carrier of (TOP-REAL 2)
i is Element of bool the carrier of (TOP-REAL 2)
i is Element of bool the carrier of (TOP-REAL 2)
i1 -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),(i1 -' 1),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(i1 -' 1)) /\ ((GoB k),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1,j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) /\ ((GoB k),j1) is Element of bool the carrier of (TOP-REAL 2)
j2 -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB k),i2,(j2 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),(j2 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i2) /\ ((GoB k),(j2 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1,j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB k),i1) /\ ((GoB k),j2) is Element of bool the carrier of (TOP-REAL 2)
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * ((k + 1),f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 * ((k + 1),(f + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg ((i1 * ((k + 1),f)),(i1 * ((k + 1),(f + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) is Element of bool the carrier of (TOP-REAL 2)
j1 is set
i2 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i2 `1 is ext-real V25() V32() Element of REAL
i2 `2 is ext-real V25() V32() Element of REAL
|[(i2 `1),(i2 `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(i1 * ((k + 1),f)) `1 is ext-real V25() V32() Element of REAL
i1 * ((k + 1),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * ((k + 1),1)) `1 is ext-real V25() V32() Element of REAL
(i1 * ((k + 1),(f + 1))) `1 is ext-real V25() V32() Element of REAL
i1 * (1,f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (1,f)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₁ <= (i1 * (1,f)) `1 } is set
0 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * (k,f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (k,f)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (i1 * (k,f)) `1 <= b₁ & b₁ <= (i1 * ((k + 1),f)) `1 ) } is set
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * (k,f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 * (k,(f + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg ((i1 * (k,f)),(i1 * (k,(f + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) is Element of bool the carrier of (TOP-REAL 2)
j1 is set
i2 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i2 `1 is ext-real V25() V32() Element of REAL
i2 `2 is ext-real V25() V32() Element of REAL
|[(i2 `1),(i2 `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(i1 * (k,f)) `1 is ext-real V25() V32() Element of REAL
i1 * (k,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (k,1)) `1 is ext-real V25() V32() Element of REAL
(i1 * (k,(f + 1))) `1 is ext-real V25() V32() Element of REAL
i1 * ((len i1),f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * ((len i1),f)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : (i1 * ((len i1),f)) `1 <= b₁ } is set
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * ((k + 1),f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * ((k + 1),f)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (i1 * (k,f)) `1 <= b₁ & b₁ <= (i1 * ((k + 1),f)) `1 ) } is set
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * (f,(k + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 * ((f + 1),(k + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg ((i1 * (f,(k + 1))),(i1 * ((f + 1),(k + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) is Element of bool the carrier of (TOP-REAL 2)
j1 is set
i2 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i2 `1 is ext-real V25() V32() Element of REAL
i2 `2 is ext-real V25() V32() Element of REAL
|[(i2 `1),(i2 `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(i1 * (f,(k + 1))) `2 is ext-real V25() V32() Element of REAL
i1 * (1,(k + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (1,(k + 1))) `2 is ext-real V25() V32() Element of REAL
(i1 * ((f + 1),(k + 1))) `2 is ext-real V25() V32() Element of REAL
i1 * (f,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (f,1)) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₂ <= (i1 * (f,1)) `2 } is set
0 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * (f,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (f,k)) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (i1 * (f,k)) `2 <= b₂ & b₂ <= (i1 * (f,(k + 1))) `2 ) } is set
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * (f,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 * ((f + 1),k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg ((i1 * (f,k)),(i1 * ((f + 1),k))) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) is Element of bool the carrier of (TOP-REAL 2)
j1 is set
i2 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i2 `1 is ext-real V25() V32() Element of REAL
i2 `2 is ext-real V25() V32() Element of REAL
|[(i2 `1),(i2 `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(i1 * (f,k)) `2 is ext-real V25() V32() Element of REAL
i1 * (1,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (1,k)) `2 is ext-real V25() V32() Element of REAL
(i1 * ((f + 1),k)) `2 is ext-real V25() V32() Element of REAL
i1 * (f,(width i1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (f,(width i1))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : (i1 * (f,(width i1))) `2 <= b₂ } is set
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * (f,(k + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (f,(k + 1))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (i1 * (f,k)) `2 <= b₂ & b₂ <= (i1 * (f,(k + 1))) `2 ) } is set
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * (k,f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 * (k,(f + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg ((i1 * (k,f)),(i1 * (k,(f + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(i1,f) is Element of bool the carrier of (TOP-REAL 2)
j1 is set
i2 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i2 `1 is ext-real V25() V32() Element of REAL
i2 `2 is ext-real V25() V32() Element of REAL
|[(i2 `1),(i2 `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(i1 * (k,(f + 1))) `2 is ext-real V25() V32() Element of REAL
(i1 * (k,f)) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (i1 * (k,f)) `2 <= b₂ & b₂ <= (i1 * (k,(f + 1))) `2 ) } is set
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * ((k + 1),f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 * ((k + 1),(f + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg ((i1 * ((k + 1),f)),(i1 * ((k + 1),(f + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(i1,k,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) is Element of bool the carrier of (TOP-REAL 2)
(i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) /\ (i1,f) is Element of bool the carrier of (TOP-REAL 2)
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * (k,f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 * (k,(f + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg ((i1 * (k,f)),(i1 * (k,(f + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(i1,k,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) is Element of bool the carrier of (TOP-REAL 2)
(i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) /\ (i1,f) is Element of bool the carrier of (TOP-REAL 2)
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * (f,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 * ((f + 1),k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg ((i1 * (f,k)),(i1 * ((f + 1),k))) is Element of bool the carrier of (TOP-REAL 2)
(i1,f) is Element of bool the carrier of (TOP-REAL 2)
j1 is set
i2 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i2 `1 is ext-real V25() V32() Element of REAL
i2 `2 is ext-real V25() V32() Element of REAL
|[(i2 `1),(i2 `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(i1 * ((f + 1),k)) `1 is ext-real V25() V32() Element of REAL
(i1 * (f,k)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (i1 * (f,k)) `1 <= b₁ & b₁ <= (i1 * ((f + 1),k)) `1 ) } is set
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * (f,(k + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 * ((f + 1),(k + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg ((i1 * (f,(k + 1))),(i1 * ((f + 1),(k + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(i1,f,k) is Element of bool the carrier of (TOP-REAL 2)
(i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) is Element of bool the carrier of (TOP-REAL 2)
(i1,f) /\ (i1,k) is Element of bool the carrier of (TOP-REAL 2)
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 * (k,f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 * ((k + 1),f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg ((i1 * (k,f)),(i1 * ((k + 1),f))) is Element of bool the carrier of (TOP-REAL 2)
(i1,k,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) is Element of bool the carrier of (TOP-REAL 2)
(i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) /\ (i1,f) is Element of bool the carrier of (TOP-REAL 2)
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
len f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(f,k) is Element of bool the carrier of (TOP-REAL 2)
(f,(k + 1)) is Element of bool the carrier of (TOP-REAL 2)
(f,k) /\ (f,(k + 1)) is Element of bool the carrier of (TOP-REAL 2)
f * ((k + 1),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * ((k + 1),1)) `1 is ext-real V25() V32() Element of REAL
{ b₁ where b₁ is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2) : b₁ `1 = (f * ((k + 1),1)) `1 } is set
width f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is set
0 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * ((0 + 1),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * ((0 + 1),1)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₁ <= (f * ((0 + 1),1)) `1 } is set
f * (1,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,1)) `1 is ext-real V25() V32() Element of REAL
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(f,(len f)) is Element of bool the carrier of (TOP-REAL 2)
f * ((len f),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * ((len f),1)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : (f * ((len f),1)) `1 <= b₁ } is set
i is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
|[i,i]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
|[i,i]| `1 is ext-real V25() V32() Element of REAL
j1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 `1 is ext-real V25() V32() Element of REAL
0 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * ((0 + 1),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * ((0 + 1),1)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₁ <= (f * ((0 + 1),1)) `1 } is set
f * (1,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,1)) `1 is ext-real V25() V32() Element of REAL
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(0 + 1) + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * (((0 + 1) + 1),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (((0 + 1) + 1),1)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (f * ((0 + 1),1)) `1 <= b₁ & b₁ <= (f * (((0 + 1) + 1),1)) `1 ) } is set
1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * ((1 + 1),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * ((1 + 1),1)) `1 is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
|[i,i]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
|[i,i]| `1 is ext-real V25() V32() Element of REAL
j1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 `1 is ext-real V25() V32() Element of REAL
f * (k,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (k,1)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (f * (k,1)) `1 <= b₁ & b₁ <= (f * ((k + 1),1)) `1 ) } is set
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(f,(len f)) is Element of bool the carrier of (TOP-REAL 2)
f * ((len f),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * ((len f),1)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : (f * ((len f),1)) `1 <= b₁ } is set
i is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
|[i,i]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
|[i,i]| `1 is ext-real V25() V32() Element of REAL
j1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 `1 is ext-real V25() V32() Element of REAL
f * (k,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (k,1)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (f * (k,1)) `1 <= b₁ & b₁ <= (f * ((k + 1),1)) `1 ) } is set
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(k + 1) + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * (((k + 1) + 1),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (((k + 1) + 1),1)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (f * ((k + 1),1)) `1 <= b₁ & b₁ <= (f * (((k + 1) + 1),1)) `1 ) } is set
i is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
|[i,i]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
|[i,i]| `1 is ext-real V25() V32() Element of REAL
j1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 `1 is ext-real V25() V32() Element of REAL
i1 is set
j1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 `1 is ext-real V25() V32() Element of REAL
j1 `2 is ext-real V25() V32() Element of REAL
|[(j1 `1),(j1 `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
f * (1,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,1)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₁ <= (f * (1,1)) `1 } is set
f * (k,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (k,1)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (f * (k,1)) `1 <= b₁ & b₁ <= (f * ((k + 1),1)) `1 ) } is set
i1 is set
j1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 `1 is ext-real V25() V32() Element of REAL
j1 `2 is ext-real V25() V32() Element of REAL
|[(j1 `1),(j1 `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
f * ((len f),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * ((len f),1)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : (f * ((len f),1)) `1 <= b₁ } is set
(k + 1) + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * (((k + 1) + 1),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (((k + 1) + 1),1)) `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (f * ((k + 1),1)) `1 <= b₁ & b₁ <= (f * (((k + 1) + 1),1)) `1 ) } is set
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is V1() V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular FinSequence of K227( the carrier of (TOP-REAL 2))
width f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(f,k) is Element of bool the carrier of (TOP-REAL 2)
(f,(k + 1)) is Element of bool the carrier of (TOP-REAL 2)
(f,k) /\ (f,(k + 1)) is Element of bool the carrier of (TOP-REAL 2)
f * (1,(k + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,(k + 1))) `2 is ext-real V25() V32() Element of REAL
{ b₁ where b₁ is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2) : b₁ `2 = (f * (1,(k + 1))) `2 } is set
len f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is set
0 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * (1,(0 + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,(0 + 1))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₂ <= (f * (1,(0 + 1))) `2 } is set
f * (1,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,1)) `2 is ext-real V25() V32() Element of REAL
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(f,(width f)) is Element of bool the carrier of (TOP-REAL 2)
f * (1,(width f)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,(width f))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : (f * (1,(width f))) `2 <= b₂ } is set
i is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
|[i,i]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
|[i,i]| `2 is ext-real V25() V32() Element of REAL
j1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 `2 is ext-real V25() V32() Element of REAL
0 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * (1,(0 + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,(0 + 1))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₂ <= (f * (1,(0 + 1))) `2 } is set
f * (1,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,1)) `2 is ext-real V25() V32() Element of REAL
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(0 + 1) + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * (1,((0 + 1) + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,((0 + 1) + 1))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (f * (1,(0 + 1))) `2 <= b₂ & b₂ <= (f * (1,((0 + 1) + 1))) `2 ) } is set
1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * (1,(1 + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,(1 + 1))) `2 is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
|[i,i]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
|[i,i]| `2 is ext-real V25() V32() Element of REAL
j1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 `2 is ext-real V25() V32() Element of REAL
f * (1,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,k)) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (f * (1,k)) `2 <= b₂ & b₂ <= (f * (1,(k + 1))) `2 ) } is set
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(f,(width f)) is Element of bool the carrier of (TOP-REAL 2)
f * (1,(width f)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,(width f))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : (f * (1,(width f))) `2 <= b₂ } is set
i is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
|[i,i]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
|[i,i]| `2 is ext-real V25() V32() Element of REAL
j1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 `2 is ext-real V25() V32() Element of REAL
f * (1,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,k)) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (f * (1,k)) `2 <= b₂ & b₂ <= (f * (1,(k + 1))) `2 ) } is set
i2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
|[i2,j2]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
(k + 1) + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * (1,((k + 1) + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,((k + 1) + 1))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (f * (1,(k + 1))) `2 <= b₂ & b₂ <= (f * (1,((k + 1) + 1))) `2 ) } is set
i is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
|[i,i]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
|[i,i]| `2 is ext-real V25() V32() Element of REAL
j1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 `2 is ext-real V25() V32() Element of REAL
i1 is set
j1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 `2 is ext-real V25() V32() Element of REAL
j1 `1 is ext-real V25() V32() Element of REAL
|[(j1 `1),(j1 `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
f * (1,1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,1)) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : b₂ <= (f * (1,1)) `2 } is set
f * (1,k) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,k)) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (f * (1,k)) `2 <= b₂ & b₂ <= (f * (1,(k + 1))) `2 ) } is set
i1 is set
j1 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 `2 is ext-real V25() V32() Element of REAL
j1 `1 is ext-real V25() V32() Element of REAL
|[(j1 `1),(j1 `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
f * (1,(width f)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,(width f))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : (f * (1,(width f))) `2 <= b₂ } is set
(k + 1) + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f * (1,((k + 1) + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(f * (1,((k + 1) + 1))) `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (f * (1,(k + 1))) `2 <= b₂ & b₂ <= (f * (1,((k + 1) + 1))) `2 ) } is set
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(i1,k,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) is Element of bool the carrier of (TOP-REAL 2)
(i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) /\ (i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,(k + 1),f) is Element of bool the carrier of (TOP-REAL 2)
(i1,(k + 1)) is Element of bool the carrier of (TOP-REAL 2)
(i1,(k + 1)) /\ (i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,k,f) /\ (i1,(k + 1),f) is Element of bool the carrier of (TOP-REAL 2)
i1 * ((k + 1),f) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 * ((k + 1),(f + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg ((i1 * ((k + 1),f)),(i1 * ((k + 1),(f + 1)))) is Element of bool the carrier of (TOP-REAL 2)
0 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 is set
((i1,(k + 1)) /\ (i1,f)) /\ (i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) /\ (((i1,(k + 1)) /\ (i1,f)) /\ (i1,f)) is Element of bool the carrier of (TOP-REAL 2)
(i1,f) /\ (i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,(k + 1)) /\ ((i1,f) /\ (i1,f)) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) /\ ((i1,(k + 1)) /\ ((i1,f) /\ (i1,f))) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) /\ (i1,(k + 1)) is Element of bool the carrier of (TOP-REAL 2)
((i1,k) /\ (i1,(k + 1))) /\ (i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1 * ((k + 1),(f + 1))) `2 is ext-real V25() V32() Element of REAL
(i1 * ((k + 1),f)) `2 is ext-real V25() V32() Element of REAL
(i1 * ((k + 1),f)) `1 is ext-real V25() V32() Element of REAL
|[((i1 * ((k + 1),f)) `1),((i1 * ((k + 1),f)) `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
i1 * ((k + 1),1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * ((k + 1),1)) `1 is ext-real V25() V32() Element of REAL
(i1 * ((k + 1),(f + 1))) `1 is ext-real V25() V32() Element of REAL
|[((i1 * ((k + 1),f)) `1),((i1 * ((k + 1),(f + 1))) `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
i2 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2) : b₁ `1 = (i1 * ((k + 1),1)) `1 } is set
i2 `1 is ext-real V25() V32() Element of REAL
j2 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j2 `1 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (i1 * ((k + 1),f)) `2 <= b₂ & b₂ <= (i1 * ((k + 1),(f + 1))) `2 ) } is set
i2 `2 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
|[j2,i]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
j2 is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
|[j2,i]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = (i1 * ((k + 1),f)) `1 & (i1 * ((k + 1),f)) `2 <= b₁ `2 & b₁ `2 <= (i1 * ((k + 1),(f + 1))) `2 ) } is set
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
width i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(i1,f,k) is Element of bool the carrier of (TOP-REAL 2)
(i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) is Element of bool the carrier of (TOP-REAL 2)
(i1,f) /\ (i1,k) is Element of bool the carrier of (TOP-REAL 2)
(i1,f,(k + 1)) is Element of bool the carrier of (TOP-REAL 2)
(i1,(k + 1)) is Element of bool the carrier of (TOP-REAL 2)
(i1,f) /\ (i1,(k + 1)) is Element of bool the carrier of (TOP-REAL 2)
(i1,f,k) /\ (i1,f,(k + 1)) is Element of bool the carrier of (TOP-REAL 2)
i1 * (f,(k + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 * ((f + 1),(k + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg ((i1 * (f,(k + 1))),(i1 * ((f + 1),(k + 1)))) is Element of bool the carrier of (TOP-REAL 2)
0 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 is set
(i1,(k + 1)) /\ (i1,f) is Element of bool the carrier of (TOP-REAL 2)
((i1,(k + 1)) /\ (i1,f)) /\ (i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) /\ (((i1,(k + 1)) /\ (i1,f)) /\ (i1,f)) is Element of bool the carrier of (TOP-REAL 2)
(i1,f) /\ (i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1,(k + 1)) /\ ((i1,f) /\ (i1,f)) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) /\ ((i1,(k + 1)) /\ ((i1,f) /\ (i1,f))) is Element of bool the carrier of (TOP-REAL 2)
(i1,k) /\ (i1,(k + 1)) is Element of bool the carrier of (TOP-REAL 2)
((i1,k) /\ (i1,(k + 1))) /\ (i1,f) is Element of bool the carrier of (TOP-REAL 2)
(i1 * ((f + 1),(k + 1))) `1 is ext-real V25() V32() Element of REAL
(i1 * (f,(k + 1))) `1 is ext-real V25() V32() Element of REAL
(i1 * (f,(k + 1))) `2 is ext-real V25() V32() Element of REAL
|[((i1 * (f,(k + 1))) `1),((i1 * (f,(k + 1))) `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
i1 * (1,(k + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(i1 * (1,(k + 1))) `2 is ext-real V25() V32() Element of REAL
(i1 * ((f + 1),(k + 1))) `2 is ext-real V25() V32() Element of REAL
|[((i1 * ((f + 1),(k + 1))) `1),((i1 * (f,(k + 1))) `2)]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
i2 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2) : b₁ `2 = (i1 * (1,(k + 1))) `2 } is set
i2 `2 is ext-real V25() V32() Element of REAL
j2 is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j2 `2 is ext-real V25() V32() Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is ext-real V25() V32() Element of REAL : ( (i1 * (f,(k + 1))) `1 <= b₁ & b₁ <= (i1 * ((f + 1),(k + 1))) `1 ) } is set
i2 `1 is ext-real V25() V32() Element of REAL
j2 is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
|[j2,i]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
j2 is ext-real V25() V32() Element of REAL
i is ext-real V25() V32() Element of REAL
|[j2,i]| is V1() V4( NAT ) Function-like non empty V33() 2 -element FinSequence-like FinSubsequence-like V177() V178() V179() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = (i1 * (f,(k + 1))) `2 & (i1 * (f,(k + 1))) `1 <= b₁ `1 & b₁ `1 <= (i1 * ((f + 1),(k + 1))) `1 ) } is set
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[(f + 1),i1] is set
{(f + 1),i1} is V187() V188() V189() V190() V191() V192() set
{(f + 1)} is V187() V188() V189() V190() V191() V192() set
{{(f + 1),i1},{(f + 1)}} is set
i1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[(f + 1),(i1 + 1)] is set
{(f + 1),(i1 + 1)} is V187() V188() V189() V190() V191() V192() set
{{(f + 1),(i1 + 1)},{(f + 1)}} is set
j1 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V33() FinSequence-like FinSubsequence-like circular special unfolded () () FinSequence of the carrier of (TOP-REAL 2)
len j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
GoB j1 is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
Indices (GoB j1) is set
j1 /. k is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB j1) * ((f + 1),i1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 /. (k + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB j1) * ((f + 1),(i1 + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(j1,k) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f,i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f) /\ ((GoB j1),i1) is Element of bool the carrier of (TOP-REAL 2)
(j1,k) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),(f + 1),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),(f + 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),(f + 1)) /\ ((GoB j1),i1) is Element of bool the carrier of (TOP-REAL 2)
(i1 + 1) + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(f + 1) -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB j1),((f + 1) -' 1),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),((f + 1) -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),((f + 1) -' 1)) /\ ((GoB j1),i1) is Element of bool the carrier of (TOP-REAL 2)
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[f,(i1 + 1)] is set
{f,(i1 + 1)} is V187() V188() V189() V190() V191() V192() set
{f} is V187() V188() V189() V190() V191() V192() set
{{f,(i1 + 1)},{f}} is set
[(f + 1),(i1 + 1)] is set
{(f + 1),(i1 + 1)} is V187() V188() V189() V190() V191() V192() set
{(f + 1)} is V187() V188() V189() V190() V191() V192() set
{{(f + 1),(i1 + 1)},{(f + 1)}} is set
j1 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V33() FinSequence-like FinSubsequence-like circular special unfolded () () FinSequence of the carrier of (TOP-REAL 2)
len j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
GoB j1 is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
Indices (GoB j1) is set
j1 /. k is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB j1) * (f,(i1 + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 /. (k + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB j1) * ((f + 1),(i1 + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(j1,k) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f,(i1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),(i1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f) /\ ((GoB j1),(i1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(j1,k) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f,i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f) /\ ((GoB j1),i1) is Element of bool the carrier of (TOP-REAL 2)
(f + 1) + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(i1 + 1) -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB j1),f,((i1 + 1) -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),((i1 + 1) -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f) /\ ((GoB j1),((i1 + 1) -' 1)) is Element of bool the carrier of (TOP-REAL 2)
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[f,(i1 + 1)] is set
{f,(i1 + 1)} is V187() V188() V189() V190() V191() V192() set
{f} is V187() V188() V189() V190() V191() V192() set
{{f,(i1 + 1)},{f}} is set
[(f + 1),(i1 + 1)] is set
{(f + 1),(i1 + 1)} is V187() V188() V189() V190() V191() V192() set
{(f + 1)} is V187() V188() V189() V190() V191() V192() set
{{(f + 1),(i1 + 1)},{(f + 1)}} is set
j1 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V33() FinSequence-like FinSubsequence-like circular special unfolded () () FinSequence of the carrier of (TOP-REAL 2)
len j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
GoB j1 is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
Indices (GoB j1) is set
j1 /. k is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB j1) * ((f + 1),(i1 + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 /. (k + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB j1) * (f,(i1 + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(j1,k) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f,i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f) /\ ((GoB j1),i1) is Element of bool the carrier of (TOP-REAL 2)
(j1,k) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f,(i1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),(i1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f) /\ ((GoB j1),(i1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(f + 1) + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(i1 + 1) -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB j1),f,((i1 + 1) -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),((i1 + 1) -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f) /\ ((GoB j1),((i1 + 1) -' 1)) is Element of bool the carrier of (TOP-REAL 2)
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[(f + 1),(i1 + 1)] is set
{(f + 1),(i1 + 1)} is V187() V188() V189() V190() V191() V192() set
{(f + 1)} is V187() V188() V189() V190() V191() V192() set
{{(f + 1),(i1 + 1)},{(f + 1)}} is set
[(f + 1),i1] is set
{(f + 1),i1} is V187() V188() V189() V190() V191() V192() set
{{(f + 1),i1},{(f + 1)}} is set
j1 is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V33() FinSequence-like FinSubsequence-like circular special unfolded () () FinSequence of the carrier of (TOP-REAL 2)
len j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
GoB j1 is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
Indices (GoB j1) is set
j1 /. k is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB j1) * ((f + 1),(i1 + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
j1 /. (k + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB j1) * ((f + 1),i1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(j1,k) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),(f + 1),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),(f + 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),(f + 1)) /\ ((GoB j1),i1) is Element of bool the carrier of (TOP-REAL 2)
(j1,k) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f,i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),f) /\ ((GoB j1),i1) is Element of bool the carrier of (TOP-REAL 2)
(i1 + 1) + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(f + 1) -' 1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB j1),((f + 1) -' 1),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),((f + 1) -' 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB j1),((f + 1) -' 1)) /\ ((GoB j1),i1) is Element of bool the carrier of (TOP-REAL 2)
k is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
k + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
f is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like non empty V33() FinSequence-like FinSubsequence-like circular special unfolded () () FinSequence of the carrier of (TOP-REAL 2)
len f is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
(f,k) is Element of bool the carrier of (TOP-REAL 2)
(f,k) is Element of bool the carrier of (TOP-REAL 2)
(f,k) /\ (f,k) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f,k) is Element of bool the carrier of (TOP-REAL 2)
dom f is V187() V188() V189() V190() V191() V192() Element of bool NAT
GoB f is V1() non empty-yielding V4( NAT ) V5(K227( the carrier of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K227( the carrier of (TOP-REAL 2))
Indices (GoB f) is set
f /. k is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i1,j1] is set
{i1,j1} is V187() V188() V189() V190() V191() V192() set
{i1} is V187() V188() V189() V190() V191() V192() set
{{i1,j1},{i1}} is set
(GoB f) * (i1,j1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
f /. (k + 1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i2 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j2 is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
[i2,j2] is set
{i2,j2} is V187() V188() V189() V190() V191() V192() set
{i2} is V187() V188() V189() V190() V191() V192() set
{{i2,j2},{i2}} is set
(GoB f) * (i2,j2) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
i1 - i2 is ext-real V25() V32() set
abs (i1 - i2) is ext-real V25() V32() Element of REAL
j1 - j2 is ext-real V25() V32() set
abs (j1 - j2) is ext-real V25() V32() Element of REAL
(abs (i1 - i2)) + (abs (j1 - j2)) is ext-real V25() V32() Element of REAL
- (i1 - i2) is ext-real V25() V32() set
i2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
- (j1 - j2) is ext-real V25() V32() set
j2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j2 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j1 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
0 + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
width (GoB f) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
len (GoB f) is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i is ext-real non negative V20() V24() V25() V32() set
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
i + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j is ext-real non negative V20() V24() V25() V32() set
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j is ext-real non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
j + 1 is non empty ext-real positive non negative V20() V24() V25() V32() V44() V161() V187() V188() V189() V190() V191() V192() Element of NAT
((GoB f),i,j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i) /\ ((GoB f),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i1,j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i1) /\ ((GoB f),j1) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (i1,(j1 + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (i1,j1)),((GoB f) * (i1,(j1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i1,j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i1) /\ ((GoB f),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i1,j) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i1) /\ ((GoB f),j) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * ((i1 + 1),j1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (i1,j1)),((GoB f) * ((i1 + 1),j1))) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i2,j) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i2) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i2) /\ ((GoB f),j) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i2,j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),j1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i2) /\ ((GoB f),j1) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * ((i2 + 1),j1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i2,j1) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * ((i2 + 1),j1)),((GoB f) * (i2,j1))) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i1,j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i1) /\ ((GoB f),j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i,j2) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i) is Element of bool the carrier of (TOP-REAL 2)
((GoB f),i) /\ ((GoB f),j2) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (i1,(j2 + 1)) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i1,j2) is 2 -element FinSequence-like V179() Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (i1,(j2 + 1))),((GoB f) * (i1,j2))) is Element of bool the carrier of (TOP-REAL 2)