REAL is V89() V90() V91() V95() set
NAT is V89() V90() V91() V92() V93() V94() V95() Element of bool REAL
bool REAL is non empty set
NAT is V89() V90() V91() V92() V93() V94() V95() set
bool NAT is non empty set
COMPLEX is V89() V95() set
RAT is V89() V90() V91() V92() V95() set
INT is V89() V90() V91() V92() V93() V95() set
bool NAT is non empty set
1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
[:2,2:] is non empty set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is non empty set
bool [:REAL,REAL:] is non empty set
TOP-REAL 2 is non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K267( the carrier of (TOP-REAL 2)) is M11( the carrier of (TOP-REAL 2))
bool the carrier of (TOP-REAL 2) is non empty set
{} is empty V89() V90() V91() V92() V93() V94() V95() set
4 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
1 / 2 is V24() V25() ext-real Element of REAL
0 is empty V19() V23() V24() V25() ext-real non positive non negative V87() V88() V89() V90() V91() V92() V93() V94() V95() Element of NAT
f is non empty V7() V10( NAT ) V11( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ f is Element of bool the carrier of (TOP-REAL 2)
(L~ f) ` is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | ((L~ f) `) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
[#] ((TOP-REAL 2) | ((L~ f) `)) is non empty non proper closed Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
bool the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
REAL 2 is non empty FinSequence-membered M11( REAL )
f is non empty V7() V10( NAT ) V11( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
GoB f is V7() non empty-yielding V10( NAT ) V11(K267( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular V183() V184() V185() V186() FinSequence of K267( the carrier of (TOP-REAL 2))
len (GoB f) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
width (GoB f) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
L~ f is Element of bool the carrier of (TOP-REAL 2)
(L~ f) ` is non empty Element of bool the carrier of (TOP-REAL 2)
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B1,B1)) is Element of bool the carrier of (TOP-REAL 2)
f is non empty V7() V10( NAT ) V11( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
GoB f is V7() non empty-yielding V10( NAT ) V11(K267( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular V183() V184() V185() V186() FinSequence of K267( the carrier of (TOP-REAL 2))
len (GoB f) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
width (GoB f) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
L~ f is Element of bool the carrier of (TOP-REAL 2)
(L~ f) ` is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | ((L~ f) `) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B1,B1)) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),B1,B1))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
bool the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
(Int (cell ((GoB f),B1,B1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),B1,B1))),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
B1 is Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | B1 is strict TopSpace-like SubSpace of TOP-REAL 2
B2 is Element of bool the carrier of (TOP-REAL 2)
Down (B2,B1) is Element of bool the carrier of ((TOP-REAL 2) | B1)
the carrier of ((TOP-REAL 2) | B1) is set
bool the carrier of ((TOP-REAL 2) | B1) is non empty set
B2 /\ B1 is Element of bool the carrier of (TOP-REAL 2)
Cl (Down (B2,B1)) is Element of bool the carrier of ((TOP-REAL 2) | B1)
Cl B2 is Element of bool the carrier of (TOP-REAL 2)
(Cl B2) /\ B1 is Element of bool the carrier of (TOP-REAL 2)
f is non empty V7() V10( NAT ) V11( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
GoB f is V7() non empty-yielding V10( NAT ) V11(K267( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular V183() V184() V185() V186() FinSequence of K267( the carrier of (TOP-REAL 2))
len (GoB f) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
width (GoB f) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
L~ f is Element of bool the carrier of (TOP-REAL 2)
(L~ f) ` is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | ((L~ f) `) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B1,B1)) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),B1,B1))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
bool the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
(Int (cell ((GoB f),B1,B1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),B1,B1))),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
f is non empty V7() V10( NAT ) V11( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ f is Element of bool the carrier of (TOP-REAL 2)
(L~ f) ` is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | ((L~ f) `) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
LeftComp f is Element of bool the carrier of (TOP-REAL 2)
Down ((LeftComp f),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
bool the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
(LeftComp f) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((LeftComp f),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
f is non empty V7() V10( NAT ) V11( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ f is Element of bool the carrier of (TOP-REAL 2)
(L~ f) ` is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | ((L~ f) `) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
RightComp f is Element of bool the carrier of (TOP-REAL 2)
Down ((RightComp f),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
bool the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
(RightComp f) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((RightComp f),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
f is non empty V7() V10( NAT ) V11( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ f is Element of bool the carrier of (TOP-REAL 2)
(L~ f) ` is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | ((L~ f) `) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
GoB f is V7() non empty-yielding V10( NAT ) V11(K267( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular V183() V184() V185() V186() FinSequence of K267( the carrier of (TOP-REAL 2))
len (GoB f) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
width (GoB f) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
{ (Cl (Down ((Int (cell ((GoB f),b1,b2))),((L~ f) `)))) where b1, b2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT : ( b1 <= len (GoB f) & b2 <= width (GoB f) ) } is set
union { (Cl (Down ((Int (cell ((GoB f),b1,b2))),((L~ f) `)))) where b1, b2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT : ( b1 <= len (GoB f) & b2 <= width (GoB f) ) } is set
{ (cell ((GoB f),b1,b2)) where b1, b2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT : ( b1 <= len (GoB f) & b2 <= width (GoB f) ) } is set
union { (cell ((GoB f),b1,b2)) where b1, b2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT : ( b1 <= len (GoB f) & b2 <= width (GoB f) ) } is set
B1 is set
B1 is set
B2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,B1)) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),B2,B1))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
bool the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
(Int (cell ((GoB f),B2,B1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),B2,B1))),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
B1 is set
B1 is set
B1 is set
B2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,B1)) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),B2,B1))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
bool the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
(Int (cell ((GoB f),B2,B1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),B2,B1))),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
f is non empty V7() V10( NAT ) V11( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ f is Element of bool the carrier of (TOP-REAL 2)
(L~ f) ` is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | ((L~ f) `) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
LeftComp f is Element of bool the carrier of (TOP-REAL 2)
Down ((LeftComp f),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
bool the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
(LeftComp f) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
RightComp f is Element of bool the carrier of (TOP-REAL 2)
Down ((RightComp f),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(RightComp f) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
bool ((L~ f) `) is non empty set
f is non empty V7() V10( NAT ) V11( the carrier of (TOP-REAL 2)) Function-like non constant FinSequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
GoB f is V7() non empty-yielding V10( NAT ) V11(K267( the carrier of (TOP-REAL 2))) Function-like FinSequence-like tabular V183() V184() V185() V186() FinSequence of K267( the carrier of (TOP-REAL 2))
len (GoB f) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
width (GoB f) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
LeftComp f is Element of bool the carrier of (TOP-REAL 2)
RightComp f is Element of bool the carrier of (TOP-REAL 2)
(LeftComp f) \/ (RightComp f) is Element of bool the carrier of (TOP-REAL 2)
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B1,B1)) is Element of bool the carrier of (TOP-REAL 2)
B2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B2 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,B1)) is Element of bool the carrier of (TOP-REAL 2)
len f is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B1 + 1),B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B1 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * ((B1 + 1),B1)),((GoB f) * ((B1 + 1),(B1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
f /. B1 is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
f /. (B1 + 1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((f /. B1),(f /. (B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
f /. B1 is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
f /. (B1 + 1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((f /. B1),(f /. (B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
right_cell (f,B1) is Element of bool the carrier of (TOP-REAL 2)
Int (right_cell (f,B1)) is Element of bool the carrier of (TOP-REAL 2)
0 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
Indices (GoB f) is set
dom (GoB f) is V89() V90() V91() V92() V93() V94() Element of bool NAT
Seg (width (GoB f)) is V89() V90() V91() V92() V93() V94() Element of bool NAT
[:(dom (GoB f)),(Seg (width (GoB f))):] is set
[(B1 + 1),(B1 + 1)] is set
{(B1 + 1),(B1 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{(B1 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{{(B1 + 1),(B1 + 1)},{(B1 + 1)}} is non empty set
[(B1 + 1),B1] is set
{(B1 + 1),B1} is non empty V89() V90() V91() V92() V93() V94() set
{{(B1 + 1),B1},{(B1 + 1)}} is non empty set
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 + 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
left_cell (f,B1) is Element of bool the carrier of (TOP-REAL 2)
Int (left_cell (f,B1)) is Element of bool the carrier of (TOP-REAL 2)
0 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
Indices (GoB f) is set
dom (GoB f) is V89() V90() V91() V92() V93() V94() Element of bool NAT
Seg (width (GoB f)) is V89() V90() V91() V92() V93() V94() Element of bool NAT
[:(dom (GoB f)),(Seg (width (GoB f))):] is set
[(B1 + 1),(B1 + 1)] is set
{(B1 + 1),(B1 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{(B1 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{{(B1 + 1),(B1 + 1)},{(B1 + 1)}} is non empty set
[(B1 + 1),B1] is set
{(B1 + 1),B1} is non empty V89() V90() V91() V92() V93() V94() set
{{(B1 + 1),B1},{(B1 + 1)}} is non empty set
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 + 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 + 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 + 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
len f is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B1 + 1),B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B1 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * ((B1 + 1),B1)),((GoB f) * ((B1 + 1),(B1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * ((B1 + 1),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((B1 + 1),1)) `1 is V24() V25() ext-real Element of REAL
((GoB f) * ((B1 + 1),1)) `2 is V24() V25() ext-real Element of REAL
(((GoB f) * ((B1 + 1),1)) `2) - 1 is V24() V25() ext-real Element of REAL
|[(((GoB f) * ((B1 + 1),1)) `1),((((GoB f) * ((B1 + 1),1)) `2) - 1)]| is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
B1 is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
{B1} is non empty Element of bool the carrier of (TOP-REAL 2)
B1 `2 is V24() V25() ext-real Element of REAL
(B1 `2) + 1 is V24() V25() ext-real Element of REAL
(GoB f) * (1,1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,1)) `2 is V24() V25() ext-real Element of REAL
(((GoB f) * (1,1)) `2) - 1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : b2 <= ((GoB f) * (1,1)) `2 } is set
B1 `1 is V24() V25() ext-real Element of REAL
|[(B1 `1),(B1 `2)]| is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
Q is Element of bool the carrier of (TOP-REAL 2)
L~ f is Element of bool the carrier of (TOP-REAL 2)
(L~ f) ` is non empty Element of bool the carrier of (TOP-REAL 2)
x is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
x `2 is V24() V25() ext-real Element of REAL
(TOP-REAL 2) | ((L~ f) `) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
0 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(B1 + 1) + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * (((B1 + 1) + 1),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (((B1 + 1) + 1),1)) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((B1 + 1),1)) `1 <= b1 & b1 <= ((GoB f) * (((B1 + 1) + 1),1)) `1 ) } is set
v_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B1 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (B1,1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (B1,1)) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (B1,1)) `1 <= b1 & b1 <= ((GoB f) * ((B1 + 1),1)) `1 ) } is set
v_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B1)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (B1,1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (B1,1)) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (B1,1)) `1 <= b1 & b1 <= ((GoB f) * ((B1 + 1),1)) `1 ) } is set
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ((GoB f) * ((B1 + 1),1)) `1 <= b1 } is set
v_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B1 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B1)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(B1 + 1) + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * (((B1 + 1) + 1),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (((B1 + 1) + 1),1)) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((B1 + 1),1)) `1 <= b1 & b1 <= ((GoB f) * (((B1 + 1) + 1),1)) `1 ) } is set
v_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B1 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f) * (1,1)) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : b1 <= ((GoB f) * (1,1)) `1 } is set
v_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B1)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ((GoB f) * ((B1 + 1),1)) `1 <= b1 } is set
v_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B1 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f) * (1,1)) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : b1 <= ((GoB f) * (1,1)) `1 } is set
v_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B1)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 + 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),(B1 + 1),B1))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
bool the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
(Int (cell ((GoB f),(B1 + 1),B1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),(B1 + 1),B1))),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
x is Element of the carrier of ((TOP-REAL 2) | ((L~ f) `))
Component_of x is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Down ((RightComp f),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(RightComp f) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((RightComp f),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Down ((LeftComp f),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(LeftComp f) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((LeftComp f),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
((LeftComp f) \/ (RightComp f)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Int (cell ((GoB f),B1,B1)) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),B1,B1))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Int (cell ((GoB f),B1,B1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),B1,B1))),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(GoB f) * ((B1 + 1),(width (GoB f))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((B1 + 1),(width (GoB f)))) `1 is V24() V25() ext-real Element of REAL
((GoB f) * ((B1 + 1),(width (GoB f)))) `2 is V24() V25() ext-real Element of REAL
(((GoB f) * ((B1 + 1),(width (GoB f)))) `2) + 1 is V24() V25() ext-real Element of REAL
|[(((GoB f) * ((B1 + 1),(width (GoB f)))) `1),((((GoB f) * ((B1 + 1),(width (GoB f)))) `2) + 1)]| is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
B1 is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
{B1} is non empty Element of bool the carrier of (TOP-REAL 2)
Q is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (1,(width (GoB f))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,(width (GoB f)))) `2 is V24() V25() ext-real Element of REAL
L~ f is Element of bool the carrier of (TOP-REAL 2)
1 + B1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 `2 is V24() V25() ext-real Element of REAL
(((GoB f) * (1,(width (GoB f)))) `2) + 1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ((GoB f) * (1,(width (GoB f)))) `2 <= b2 } is set
B1 `1 is V24() V25() ext-real Element of REAL
|[(B1 `1),(B1 `2)]| is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(L~ f) ` is non empty Element of bool the carrier of (TOP-REAL 2)
x is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
x `2 is V24() V25() ext-real Element of REAL
(TOP-REAL 2) | ((L~ f) `) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
0 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(B1 + 1) + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * (((B1 + 1) + 1),(width (GoB f))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (((B1 + 1) + 1),(width (GoB f)))) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((B1 + 1),(width (GoB f)))) `1 <= b1 & b1 <= ((GoB f) * (((B1 + 1) + 1),(width (GoB f)))) `1 ) } is set
v_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B1 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (B1,(width (GoB f))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (B1,(width (GoB f)))) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (B1,(width (GoB f)))) `1 <= b1 & b1 <= ((GoB f) * ((B1 + 1),(width (GoB f)))) `1 ) } is set
v_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B1)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (B1,(width (GoB f))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (B1,(width (GoB f)))) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (B1,(width (GoB f)))) `1 <= b1 & b1 <= ((GoB f) * ((B1 + 1),(width (GoB f)))) `1 ) } is set
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ((GoB f) * ((B1 + 1),(width (GoB f)))) `1 <= b1 } is set
v_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B1 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B1)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(B1 + 1) + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * (((B1 + 1) + 1),(width (GoB f))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (((B1 + 1) + 1),(width (GoB f)))) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((B1 + 1),(width (GoB f)))) `1 <= b1 & b1 <= ((GoB f) * (((B1 + 1) + 1),(width (GoB f)))) `1 ) } is set
v_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B1 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
((GoB f) * (1,(width (GoB f)))) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : b1 <= ((GoB f) * (1,(width (GoB f)))) `1 } is set
v_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B1)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 + 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),(B1 + 1),B1))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
bool the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
(Int (cell ((GoB f),(B1 + 1),B1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),(B1 + 1),B1))),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
x is Element of the carrier of ((TOP-REAL 2) | ((L~ f) `))
Component_of x is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Down ((RightComp f),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(RightComp f) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((RightComp f),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Down ((LeftComp f),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(LeftComp f) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((LeftComp f),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
((LeftComp f) \/ (RightComp f)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Int (cell ((GoB f),B1,B1)) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),B1,B1))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Int (cell ((GoB f),B1,B1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),B1,B1))),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
LSeg (f,B1) is Element of bool the carrier of (TOP-REAL 2)
f /. B1 is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
f /. (B1 + 1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((f /. B1),(f /. (B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
((GoB f) * ((B1 + 1),B1)) + ((GoB f) * ((B1 + 1),(B1 + 1))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((B1 + 1),B1)) + ((GoB f) * ((B1 + 1),(B1 + 1)))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
L~ f is Element of bool the carrier of (TOP-REAL 2)
B1 is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
B1 `2 is V24() V25() ext-real Element of REAL
(((GoB f) * ((B1 + 1),B1)) + ((GoB f) * ((B1 + 1),(B1 + 1)))) `2 is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * ((B1 + 1),B1)) + ((GoB f) * ((B1 + 1),(B1 + 1)))) `2) is V24() V25() ext-real Element of REAL
((GoB f) * ((B1 + 1),B1)) `2 is V24() V25() ext-real Element of REAL
((GoB f) * ((B1 + 1),(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
(((GoB f) * ((B1 + 1),B1)) `2) + (((GoB f) * ((B1 + 1),(B1 + 1))) `2) is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * ((B1 + 1),B1)) `2) + (((GoB f) * ((B1 + 1),(B1 + 1))) `2)) is V24() V25() ext-real Element of REAL
{B1} is non empty Element of bool the carrier of (TOP-REAL 2)
(L~ f) ` is non empty Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | ((L~ f) `) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
Down ((RightComp f),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
bool the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
(RightComp f) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((RightComp f),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Down ((LeftComp f),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(LeftComp f) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((LeftComp f),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Down ((LeftComp f),((L~ f) `))) \/ (Down ((RightComp f),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Down (((LeftComp f) \/ (RightComp f)),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
((LeftComp f) \/ (RightComp f)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down (((LeftComp f) \/ (RightComp f)),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
cell ((GoB f),B1,B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B1,B1)) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),B1,B1))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Int (cell ((GoB f),B1,B1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),B1,B1))),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 + 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),(B1 + 1),B1))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Int (cell ((GoB f),(B1 + 1),B1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),(B1 + 1),B1))),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
0 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
Q is Element of bool the carrier of (TOP-REAL 2)
x is set
1 + B1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 `1 is V24() V25() ext-real Element of REAL
(((GoB f) * ((B1 + 1),B1)) + ((GoB f) * ((B1 + 1),(B1 + 1)))) `1 is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * ((B1 + 1),B1)) + ((GoB f) * ((B1 + 1),(B1 + 1)))) `1) is V24() V25() ext-real Element of REAL
((GoB f) * ((B1 + 1),B1)) `1 is V24() V25() ext-real Element of REAL
((GoB f) * ((B1 + 1),(B1 + 1))) `1 is V24() V25() ext-real Element of REAL
(((GoB f) * ((B1 + 1),B1)) `1) + (((GoB f) * ((B1 + 1),(B1 + 1))) `1) is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * ((B1 + 1),B1)) `1) + (((GoB f) * ((B1 + 1),(B1 + 1))) `1)) is V24() V25() ext-real Element of REAL
|[((1 / 2) * ((((GoB f) * ((B1 + 1),B1)) `1) + (((GoB f) * ((B1 + 1),(B1 + 1))) `1))),((1 / 2) * ((((GoB f) * ((B1 + 1),B1)) `2) + (((GoB f) * ((B1 + 1),(B1 + 1))) `2)))]| is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
(((GoB f) * ((B1 + 1),(B1 + 1))) `2) + (((GoB f) * ((B1 + 1),(B1 + 1))) `2) is V24() V25() ext-real Element of REAL
((((GoB f) * ((B1 + 1),(B1 + 1))) `2) + (((GoB f) * ((B1 + 1),(B1 + 1))) `2)) / 2 is V24() V25() ext-real Element of REAL
((((GoB f) * ((B1 + 1),B1)) `2) + (((GoB f) * ((B1 + 1),(B1 + 1))) `2)) / 2 is V24() V25() ext-real Element of REAL
(((GoB f) * ((B1 + 1),B1)) `2) + (((GoB f) * ((B1 + 1),B1)) `2) is V24() V25() ext-real Element of REAL
((((GoB f) * ((B1 + 1),B1)) `2) + (((GoB f) * ((B1 + 1),B1)) `2)) / 2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((B1 + 1),B1)) `2 <= b2 & b2 <= ((GoB f) * ((B1 + 1),(B1 + 1))) `2 ) } is set
|[(B1 `1),(B1 `2)]| is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(B1 + 1) + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B1 + 1),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((B1 + 1),1)) `1 is V24() V25() ext-real Element of REAL
(GoB f) * (((B1 + 1) + 1),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (((B1 + 1) + 1),1)) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((B1 + 1),1)) `1 <= b1 & b1 <= ((GoB f) * (((B1 + 1) + 1),1)) `1 ) } is set
v_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B1 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (B1,1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (B1,1)) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (B1,1)) `1 <= b1 & b1 <= ((GoB f) * ((B1 + 1),1)) `1 ) } is set
v_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B1)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (B1,1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (B1,1)) `1 is V24() V25() ext-real Element of REAL
(GoB f) * ((B1 + 1),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((B1 + 1),1)) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (B1,1)) `1 <= b1 & b1 <= ((GoB f) * ((B1 + 1),1)) `1 ) } is set
v_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B1)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ((GoB f) * ((B1 + 1),1)) `1 <= b1 } is set
v_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B1 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(B1 + 1) + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B1 + 1),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((B1 + 1),1)) `1 is V24() V25() ext-real Element of REAL
(GoB f) * (((B1 + 1) + 1),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (((B1 + 1) + 1),1)) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((B1 + 1),1)) `1 <= b1 & b1 <= ((GoB f) * (((B1 + 1) + 1),1)) `1 ) } is set
v_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B1 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (1,1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,1)) `1 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : b1 <= ((GoB f) * (1,1)) `1 } is set
v_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B1)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B1 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B1,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
x is Element of the carrier of ((TOP-REAL 2) | ((L~ f) `))
Component_of x is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
f /. B1 is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
f /. (B1 + 1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((f /. B1),(f /. (B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 + 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 + 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
len f is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B1 + 1),B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B1 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * ((B1 + 1),B1)),((GoB f) * ((B1 + 1),(B1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
f /. B1 is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
f /. (B1 + 1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((f /. B1),(f /. (B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 + 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
len f is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B1 + 1),B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B1 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * ((B1 + 1),B1)),((GoB f) * ((B1 + 1),(B1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 + 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
f /. B1 is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
f /. (B1 + 1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((f /. B1),(f /. (B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
B1 -' 1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(B1 -' 1) + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(B2 + 1) + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 - 1 is V24() V25() ext-real Element of REAL
len f is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B2 + 1),B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B2 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * ((B2 + 1),B1)),((GoB f) * ((B2 + 1),(B1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (((B1 -' 1) + 1),B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
(GoB f) * (((B1 -' 1) + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (((B1 -' 1) + 1),B1)),((GoB f) * (((B1 -' 1) + 1),(B1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
f /. B1 is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
f /. (B1 + 1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((f /. B1),(f /. (B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
f /. B1 is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
f /. (B1 + 1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((f /. B1),(f /. (B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
left_cell (f,B1) is Element of bool the carrier of (TOP-REAL 2)
Int (left_cell (f,B1)) is Element of bool the carrier of (TOP-REAL 2)
Indices (GoB f) is set
dom (GoB f) is V89() V90() V91() V92() V93() V94() Element of bool NAT
Seg (width (GoB f)) is V89() V90() V91() V92() V93() V94() Element of bool NAT
[:(dom (GoB f)),(Seg (width (GoB f))):] is set
[((B1 -' 1) + 1),(B1 + 1)] is set
{((B1 -' 1) + 1),(B1 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{((B1 -' 1) + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{{((B1 -' 1) + 1),(B1 + 1)},{((B1 -' 1) + 1)}} is non empty set
0 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
[((B1 -' 1) + 1),B1] is set
{((B1 -' 1) + 1),B1} is non empty V89() V90() V91() V92() V93() V94() set
{{((B1 -' 1) + 1),B1},{((B1 -' 1) + 1)}} is non empty set
cell ((GoB f),(B1 -' 1),B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 -' 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
right_cell (f,B1) is Element of bool the carrier of (TOP-REAL 2)
Int (right_cell (f,B1)) is Element of bool the carrier of (TOP-REAL 2)
Indices (GoB f) is set
dom (GoB f) is V89() V90() V91() V92() V93() V94() Element of bool NAT
Seg (width (GoB f)) is V89() V90() V91() V92() V93() V94() Element of bool NAT
[:(dom (GoB f)),(Seg (width (GoB f))):] is set
[((B1 -' 1) + 1),(B1 + 1)] is set
{((B1 -' 1) + 1),(B1 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{((B1 -' 1) + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{{((B1 -' 1) + 1),(B1 + 1)},{((B1 -' 1) + 1)}} is non empty set
0 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
[((B1 -' 1) + 1),B1] is set
{((B1 -' 1) + 1),B1} is non empty V89() V90() V91() V92() V93() V94() set
{{((B1 -' 1) + 1),B1},{((B1 -' 1) + 1)}} is non empty set
cell ((GoB f),(B1 -' 1),B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 -' 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 -' 1),B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 -' 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B1 -' 1),B1) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 -' 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
len f is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B2 + 1),B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
B1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(GoB f) * ((B2 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * ((B2 + 1),B1)),((GoB f) * ((B2 + 1),(B1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * ((B2 + 1),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((B2 + 1),1)) `1 is V24() V25() ext-real Element of REAL