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
((GoB f) * ((B2 + 1),1)) `2 is V24() V25() ext-real Element of REAL
(((GoB f) * ((B2 + 1),1)) `2) - 1 is V24() V25() ext-real Element of REAL
|[(((GoB f) * ((B2 + 1),1)) `1),((((GoB f) * ((B2 + 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
(GoB f) * (((B2 + 1) + 1),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (((B2 + 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) * ((B2 + 1),1)) `1 <= b1 & b1 <= ((GoB f) * (((B2 + 1) + 1),1)) `1 ) } is 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
(GoB f) * (B2,1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (B2,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) * (B2,1)) `1 <= b1 & b1 <= ((GoB f) * ((B2 + 1),1)) `1 ) } is set
v_strip ((GoB f),B2) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B2)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((GoB f),(B2 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B2 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (((B2 + 1) + 1),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (((B2 + 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) * ((B2 + 1),1)) `1 <= b1 & b1 <= ((GoB f) * (((B2 + 1) + 1),1)) `1 ) } is set
v_strip ((GoB f),(B2 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B2 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : b1 <= ((GoB f) * ((B2 + 1),1)) `1 } is set
v_strip ((GoB f),B2) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B2)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) 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
(GoB f) * (B2,1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (B2,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) * (B2,1)) `1 <= b1 & b1 <= ((GoB f) * ((B2 + 1),1)) `1 ) } is set
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ((GoB f) * ((B2 + 1),1)) `1 <= b1 } is set
v_strip ((GoB f),(B2 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B2 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((GoB f),B2) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B2)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,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) * ((B2 + 1),1)) `1 <= b1 } is set
v_strip ((GoB f),(B2 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B2 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 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),B2) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B2)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) 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) `))
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) `))
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) `))
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) `))
Int (cell ((GoB f),(B2 + 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),(B2 + 1),B1))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Int (cell ((GoB f),(B2 + 1),B1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),(B2 + 1),B1))),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(GoB f) * ((B2 + 1),(width (GoB f))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((B2 + 1),(width (GoB f)))) `1 is V24() V25() ext-real Element of REAL
((GoB f) * ((B2 + 1),(width (GoB f)))) `2 is V24() V25() ext-real Element of REAL
(((GoB f) * ((B2 + 1),(width (GoB f)))) `2) + 1 is V24() V25() ext-real Element of REAL
|[(((GoB f) * ((B2 + 1),(width (GoB f)))) `1),((((GoB f) * ((B2 + 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)
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
(GoB f) * (((B2 + 1) + 1),(width (GoB f))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (((B2 + 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) * ((B2 + 1),(width (GoB f)))) `1 <= b1 & b1 <= ((GoB f) * (((B2 + 1) + 1),(width (GoB f)))) `1 ) } is set
v_strip ((GoB f),(B2 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B2 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),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
(GoB f) * (B2,(width (GoB f))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (B2,(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) * (B2,(width (GoB f)))) `1 <= b1 & b1 <= ((GoB f) * ((B2 + 1),(width (GoB f)))) `1 ) } is set
v_strip ((GoB f),B2) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B2)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (((B2 + 1) + 1),(width (GoB f))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (((B2 + 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) * ((B2 + 1),(width (GoB f)))) `1 <= b1 & b1 <= ((GoB f) * (((B2 + 1) + 1),(width (GoB f)))) `1 ) } is set
v_strip ((GoB f),(B2 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B2 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 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),B2) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B2)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) 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
(GoB f) * (B2,(width (GoB f))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (B2,(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) * (B2,(width (GoB f)))) `1 <= b1 & b1 <= ((GoB f) * ((B2 + 1),(width (GoB f)))) `1 ) } is set
(GoB f) * ((len (GoB f)),(width (GoB f))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),(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) * ((len (GoB f)),(width (GoB f)))) `1 <= b1 } is set
v_strip ((GoB f),(B2 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B2 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((GoB f),B2) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B2)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) 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) `))
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) `))
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) `))
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) `))
Int (cell ((GoB f),(B2 + 1),B1)) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),(B2 + 1),B1))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Int (cell ((GoB f),(B2 + 1),B1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),(B2 + 1),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) * ((B2 + 1),B1)) + ((GoB f) * ((B2 + 1),(B1 + 1))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((B2 + 1),B1)) + ((GoB f) * ((B2 + 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) * ((B2 + 1),B1)) + ((GoB f) * ((B2 + 1),(B1 + 1)))) `2 is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * ((B2 + 1),B1)) + ((GoB f) * ((B2 + 1),(B1 + 1)))) `2) is V24() V25() ext-real Element of REAL
((GoB f) * ((B2 + 1),B1)) `2 is V24() V25() ext-real Element of REAL
((GoB f) * ((B2 + 1),(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
(((GoB f) * ((B2 + 1),B1)) `2) + (((GoB f) * ((B2 + 1),(B1 + 1))) `2) is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * ((B2 + 1),B1)) `2) + (((GoB f) * ((B2 + 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) `))
B1 `1 is V24() V25() ext-real Element of REAL
(((GoB f) * ((B2 + 1),B1)) + ((GoB f) * ((B2 + 1),(B1 + 1)))) `1 is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * ((B2 + 1),B1)) + ((GoB f) * ((B2 + 1),(B1 + 1)))) `1) is V24() V25() ext-real Element of REAL
((GoB f) * ((B2 + 1),B1)) `1 is V24() V25() ext-real Element of REAL
((GoB f) * ((B2 + 1),(B1 + 1))) `1 is V24() V25() ext-real Element of REAL
(((GoB f) * ((B2 + 1),B1)) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1) is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * ((B2 + 1),B1)) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1)) is V24() V25() ext-real Element of REAL
|[((1 / 2) * ((((GoB f) * ((B2 + 1),B1)) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1))),((1 / 2) * ((((GoB f) * ((B2 + 1),B1)) `2) + (((GoB f) * ((B2 + 1),(B1 + 1))) `2)))]| is V37(2) V79() FinSequence-like Element of 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) `))
(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),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) `))
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 + B2 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))) `2) + (((GoB f) * ((B2 + 1),(B1 + 1))) `2) is V24() V25() ext-real Element of REAL
((((GoB f) * ((B2 + 1),(B1 + 1))) `2) + (((GoB f) * ((B2 + 1),(B1 + 1))) `2)) / 2 is V24() V25() ext-real Element of REAL
((((GoB f) * ((B2 + 1),B1)) `2) + (((GoB f) * ((B2 + 1),(B1 + 1))) `2)) / 2 is V24() V25() ext-real Element of REAL
(((GoB f) * ((B2 + 1),B1)) `2) + (((GoB f) * ((B2 + 1),B1)) `2) is V24() V25() ext-real Element of REAL
((((GoB f) * ((B2 + 1),B1)) `2) + (((GoB f) * ((B2 + 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) * ((B2 + 1),B1)) `2 <= b2 & b2 <= ((GoB f) * ((B2 + 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)
(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
(GoB f) * (((B2 + 1) + 1),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (((B2 + 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) * ((B2 + 1),1)) `1 <= b1 & b1 <= ((GoB f) * (((B2 + 1) + 1),1)) `1 ) } is set
v_strip ((GoB f),(B2 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B2 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (B2,1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (B2,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) * (B2,1)) `1 <= b1 & b1 <= ((GoB f) * ((B2 + 1),1)) `1 ) } is set
v_strip ((GoB f),B2) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B2)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (B2,1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (B2,1)) `1 is V24() V25() ext-real Element of REAL
(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
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (B2,1)) `1 <= b1 & b1 <= ((GoB f) * ((B2 + 1),1)) `1 ) } is set
v_strip ((GoB f),B2) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B2)) /\ (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) * ((B2 + 1),1)) `1 <= b1 } is set
v_strip ((GoB f),(B2 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B2 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) 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
(GoB f) * (((B2 + 1) + 1),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (((B2 + 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) * ((B2 + 1),1)) `1 <= b1 & b1 <= ((GoB f) * (((B2 + 1) + 1),1)) `1 ) } is set
v_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((GoB f),(B2 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),(B2 + 1))) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),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),B2) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f),B2)) /\ (h_strip ((GoB f),B1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),(B2 + 1),B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),(B2 + 1),B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,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)
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)
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)
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)
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)
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 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
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
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
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) * (B2,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
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
(GoB f) * ((B2 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (B2,(B1 + 1))),((GoB f) * ((B2 + 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)
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
[(B2 + 1),(B1 + 1)] is set
{(B2 + 1),(B1 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{(B2 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{{(B2 + 1),(B1 + 1)},{(B2 + 1)}} is non empty set
[B2,(B1 + 1)] is set
{B2,(B1 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{B2} is non empty V89() V90() V91() V92() V93() V94() set
{{B2,(B1 + 1)},{B2}} is non empty set
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(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
[(B2 + 1),(B1 + 1)] is set
{(B2 + 1),(B1 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{(B2 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{{(B2 + 1),(B1 + 1)},{(B2 + 1)}} is non empty set
[B2,(B1 + 1)] is set
{B2,(B1 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{B2} is non empty V89() V90() V91() V92() V93() V94() set
{{B2,(B1 + 1)},{B2}} is non empty set
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(B1 + 1))) 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,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
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
(GoB f) * ((B2 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (B2,(B1 + 1))),((GoB f) * ((B2 + 1),(B1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (1,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,(B1 + 1))) `1 is V24() V25() ext-real Element of REAL
(((GoB f) * (1,(B1 + 1))) `1) - 1 is V24() V25() ext-real Element of REAL
((GoB f) * (1,(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
|[((((GoB f) * (1,(B1 + 1))) `1) - 1),(((GoB f) * (1,(B1 + 1))) `2)]| 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 `1 is V24() V25() ext-real Element of REAL
(B1 `1) + 1 is V24() V25() ext-real Element of REAL
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
(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
(((GoB f) * (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 : b1 <= ((GoB f) * (1,1)) `1 } is set
B1 `2 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)
v_strip ((GoB f),B2) 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 `1 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) * (1,((B1 + 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,((B1 + 1) + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,(B1 + 1))) `2 <= b2 & b2 <= ((GoB f) * (1,((B1 + 1) + 1))) `2 ) } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (1,B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,B1)) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,B1)) `2 <= b2 & b2 <= ((GoB f) * (1,(B1 + 1))) `2 ) } is set
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (1,B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,B1)) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,B1)) `2 <= b2 & b2 <= ((GoB f) * (1,(B1 + 1))) `2 ) } is set
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ((GoB f) * (1,(B1 + 1))) `2 <= b2 } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,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) * (1,((B1 + 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,((B1 + 1) + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,(B1 + 1))) `2 <= b2 & b2 <= ((GoB f) * (1,((B1 + 1) + 1))) `2 ) } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB f) * (1,1)) `2 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
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,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) * (1,(B1 + 1))) `2 <= b2 } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB f) * (1,1)) `2 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
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),B2,(B1 + 1)))),((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),B2,(B1 + 1)))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),B2,(B1 + 1)))),((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),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) `))
(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) `))
(GoB f) * ((len (GoB f)),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),(B1 + 1))) `1 is V24() V25() ext-real Element of REAL
(((GoB f) * ((len (GoB f)),(B1 + 1))) `1) + 1 is V24() V25() ext-real Element of REAL
((GoB f) * ((len (GoB f)),(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
|[((((GoB f) * ((len (GoB f)),(B1 + 1))) `1) + 1),(((GoB f) * ((len (GoB f)),(B1 + 1))) `2)]| 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) * ((len (GoB f)),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),1)) `1 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 `1 is V24() V25() ext-real Element of REAL
(((GoB f) * ((len (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 : ((GoB f) * ((len (GoB f)),1)) `1 <= b1 } is set
B1 `2 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)
v_strip ((GoB f),B2) 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 `1 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) * ((len (GoB f)),((B1 + 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),((B1 + 1) + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((len (GoB f)),(B1 + 1))) `2 <= b2 & b2 <= ((GoB f) * ((len (GoB f)),((B1 + 1) + 1))) `2 ) } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * ((len (GoB f)),B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),B1)) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((len (GoB f)),B1)) `2 <= b2 & b2 <= ((GoB f) * ((len (GoB f)),(B1 + 1))) `2 ) } is set
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * ((len (GoB f)),B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),B1)) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((len (GoB f)),B1)) `2 <= b2 & b2 <= ((GoB f) * ((len (GoB f)),(B1 + 1))) `2 ) } is set
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ((GoB f) * ((len (GoB f)),(B1 + 1))) `2 <= b2 } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,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) * ((len (GoB f)),((B1 + 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),((B1 + 1) + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((len (GoB f)),(B1 + 1))) `2 <= b2 & b2 <= ((GoB f) * ((len (GoB f)),((B1 + 1) + 1))) `2 ) } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),1)) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : b2 <= ((GoB f) * ((len (GoB f)),1)) `2 } is set
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,B1) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),B2,(B1 + 1)))),((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),B2,(B1 + 1)))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),B2,(B1 + 1)))),((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),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) `))
(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) `))
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) * (B2,(B1 + 1))) + ((GoB f) * ((B2 + 1),(B1 + 1))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (B2,(B1 + 1))) + ((GoB f) * ((B2 + 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 `1 is V24() V25() ext-real Element of REAL
(((GoB f) * (B2,(B1 + 1))) + ((GoB f) * ((B2 + 1),(B1 + 1)))) `1 is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * (B2,(B1 + 1))) + ((GoB f) * ((B2 + 1),(B1 + 1)))) `1) is V24() V25() ext-real Element of REAL
((GoB f) * (B2,(B1 + 1))) `1 is V24() V25() ext-real Element of REAL
((GoB f) * ((B2 + 1),(B1 + 1))) `1 is V24() V25() ext-real Element of REAL
(((GoB f) * (B2,(B1 + 1))) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1) is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * (B2,(B1 + 1))) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1)) 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),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) `))
(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 + 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),B2,(B1 + 1)))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Int (cell ((GoB f),B2,(B1 + 1)))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),B2,(B1 + 1)))),((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 `2 is V24() V25() ext-real Element of REAL
(((GoB f) * (B2,(B1 + 1))) + ((GoB f) * ((B2 + 1),(B1 + 1)))) `2 is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * (B2,(B1 + 1))) + ((GoB f) * ((B2 + 1),(B1 + 1)))) `2) is V24() V25() ext-real Element of REAL
((GoB f) * (B2,(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
((GoB f) * ((B2 + 1),(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
(((GoB f) * (B2,(B1 + 1))) `2) + (((GoB f) * ((B2 + 1),(B1 + 1))) `2) is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * (B2,(B1 + 1))) `2) + (((GoB f) * ((B2 + 1),(B1 + 1))) `2)) is V24() V25() ext-real Element of REAL
|[((1 / 2) * ((((GoB f) * (B2,(B1 + 1))) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1))),((1 / 2) * ((((GoB f) * (B2,(B1 + 1))) `2) + (((GoB f) * ((B2 + 1),(B1 + 1))) `2)))]| is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
(((GoB f) * ((B2 + 1),(B1 + 1))) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1) is V24() V25() ext-real Element of REAL
((((GoB f) * ((B2 + 1),(B1 + 1))) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1)) / 2 is V24() V25() ext-real Element of REAL
((((GoB f) * (B2,(B1 + 1))) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1)) / 2 is V24() V25() ext-real Element of REAL
(((GoB f) * (B2,(B1 + 1))) `1) + (((GoB f) * (B2,(B1 + 1))) `1) is V24() V25() ext-real Element of REAL
((((GoB f) * (B2,(B1 + 1))) `1) + (((GoB f) * (B2,(B1 + 1))) `1)) / 2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (B2,(B1 + 1))) `1 <= b1 & b1 <= ((GoB f) * ((B2 + 1),(B1 + 1))) `1 ) } is set
|[(B1 `1),(B1 `2)]| is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
v_strip ((GoB f),B2) 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) * (1,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
(GoB f) * (1,((B1 + 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,((B1 + 1) + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,(B1 + 1))) `2 <= b2 & b2 <= ((GoB f) * (1,((B1 + 1) + 1))) `2 ) } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (1,B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,B1)) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,B1)) `2 <= b2 & b2 <= ((GoB f) * (1,(B1 + 1))) `2 ) } is set
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (1,B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,B1)) `2 is V24() V25() ext-real Element of REAL
(GoB f) * (1,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,B1)) `2 <= b2 & b2 <= ((GoB f) * (1,(B1 + 1))) `2 ) } is set
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) 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) * (1,(B1 + 1))) `2 <= b2 } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,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) * (1,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
(GoB f) * (1,((B1 + 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,((B1 + 1) + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,(B1 + 1))) `2 <= b2 & b2 <= ((GoB f) * (1,((B1 + 1) + 1))) `2 ) } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) 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)) `2 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
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,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),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(B1 + 1))) 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,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
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
(GoB f) * ((B2 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (B2,(B1 + 1))),((GoB f) * ((B2 + 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),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(B1 + 1))) 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,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
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
(GoB f) * ((B2 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (B2,(B1 + 1))),((GoB f) * ((B2 + 1),(B1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(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 -' 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
(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
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,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
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
(GoB f) * ((B2 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (B2,(B1 + 1))),((GoB f) * ((B2 + 1),(B1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (B2,((B1 -' 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
(GoB f) * ((B2 + 1),((B1 -' 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (B2,((B1 -' 1) + 1))),((GoB f) * ((B2 + 1),((B1 -' 1) + 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)
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
[(B2 + 1),((B1 -' 1) + 1)] is set
{(B2 + 1),((B1 -' 1) + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{(B2 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{{(B2 + 1),((B1 -' 1) + 1)},{(B2 + 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
[B2,((B1 -' 1) + 1)] is set
{B2,((B1 -' 1) + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{B2} is non empty V89() V90() V91() V92() V93() V94() set
{{B2,((B1 -' 1) + 1)},{B2}} is non empty set
cell ((GoB f),B2,(B1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(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
[(B2 + 1),((B1 -' 1) + 1)] is set
{(B2 + 1),((B1 -' 1) + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{(B2 + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{{(B2 + 1),((B1 -' 1) + 1)},{(B2 + 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
[B2,((B1 -' 1) + 1)] is set
{B2,((B1 -' 1) + 1)} is non empty V89() V90() V91() V92() V93() V94() set
{B2} is non empty V89() V90() V91() V92() V93() V94() set
{{B2,((B1 -' 1) + 1)},{B2}} is non empty set
cell ((GoB f),B2,(B1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(B1 -' 1))) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(B1 -' 1))) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B2,(B1 -' 1))) 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,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
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
(GoB f) * ((B2 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (B2,(B1 + 1))),((GoB f) * ((B2 + 1),(B1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (1,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,(B1 + 1))) `1 is V24() V25() ext-real Element of REAL
(((GoB f) * (1,(B1 + 1))) `1) - 1 is V24() V25() ext-real Element of REAL
((GoB f) * (1,(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
|[((((GoB f) * (1,(B1 + 1))) `1) - 1),(((GoB f) * (1,(B1 + 1))) `2)]| 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 `1 is V24() V25() ext-real Element of REAL
(B1 `1) + 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)) `1 is V24() V25() ext-real Element of REAL
(((GoB f) * (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 : b1 <= ((GoB f) * (1,1)) `1 } is set
B1 `2 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)
v_strip ((GoB f),B2) 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 `1 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
(GoB f) * (1,((B1 + 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,((B1 + 1) + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,(B1 + 1))) `2 <= b2 & b2 <= ((GoB f) * (1,((B1 + 1) + 1))) `2 ) } is 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
(GoB f) * (1,B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,B1)) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,B1)) `2 <= b2 & b2 <= ((GoB f) * (1,(B1 + 1))) `2 ) } is set
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (1,((B1 + 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,((B1 + 1) + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,(B1 + 1))) `2 <= b2 & b2 <= ((GoB f) * (1,((B1 + 1) + 1))) `2 ) } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : b2 <= ((GoB f) * (1,(B1 + 1))) `2 } is set
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) 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
(GoB f) * (1,B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,B1)) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,B1)) `2 <= b2 & b2 <= ((GoB f) * (1,(B1 + 1))) `2 ) } is set
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ((GoB f) * (1,(B1 + 1))) `2 <= b2 } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,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) * (1,(B1 + 1))) `2 <= b2 } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB f) * (1,1)) `2 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
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) 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) `))
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) `))
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) `))
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) `))
(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) `))
Int (cell ((GoB f),B2,(B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),B2,(B1 + 1)))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Int (cell ((GoB f),B2,(B1 + 1)))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),B2,(B1 + 1)))),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(GoB f) * ((len (GoB f)),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),(B1 + 1))) `1 is V24() V25() ext-real Element of REAL
(((GoB f) * ((len (GoB f)),(B1 + 1))) `1) + 1 is V24() V25() ext-real Element of REAL
((GoB f) * ((len (GoB f)),(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
|[((((GoB f) * ((len (GoB f)),(B1 + 1))) `1) + 1),(((GoB f) * ((len (GoB f)),(B1 + 1))) `2)]| 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) * ((len (GoB f)),1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),1)) `1 is V24() V25() ext-real Element of REAL
L~ f is Element of bool the carrier of (TOP-REAL 2)
B1 `1 is V24() V25() ext-real Element of REAL
(((GoB f) * ((len (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 : ((GoB f) * ((len (GoB f)),1)) `1 <= b1 } is set
B1 `2 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)
v_strip ((GoB f),B2) 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 `1 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
(GoB f) * ((len (GoB f)),((B1 + 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),((B1 + 1) + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((len (GoB f)),(B1 + 1))) `2 <= b2 & b2 <= ((GoB f) * ((len (GoB f)),((B1 + 1) + 1))) `2 ) } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) 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
(GoB f) * ((len (GoB f)),B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),B1)) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((len (GoB f)),B1)) `2 <= b2 & b2 <= ((GoB f) * ((len (GoB f)),(B1 + 1))) `2 ) } is set
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * ((len (GoB f)),((B1 + 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),((B1 + 1) + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((len (GoB f)),(B1 + 1))) `2 <= b2 & b2 <= ((GoB f) * ((len (GoB f)),((B1 + 1) + 1))) `2 ) } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),1)) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : b2 <= ((GoB f) * ((len (GoB f)),1)) `2 } is set
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) 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
(GoB f) * ((len (GoB f)),B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),B1)) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * ((len (GoB f)),B1)) `2 <= b2 & b2 <= ((GoB f) * ((len (GoB f)),(B1 + 1))) `2 ) } is set
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * ((len (GoB f)),(width (GoB f))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),(width (GoB f)))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ((GoB f) * ((len (GoB f)),(width (GoB f)))) `2 <= b2 } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) 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) `))
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) `))
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) `))
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) `))
(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) `))
Int (cell ((GoB f),B2,(B1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),B2,(B1 + 1)))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Int (cell ((GoB f),B2,(B1 + 1)))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),B2,(B1 + 1)))),((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) * (B2,(B1 + 1))) + ((GoB f) * ((B2 + 1),(B1 + 1))) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (B2,(B1 + 1))) + ((GoB f) * ((B2 + 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 `1 is V24() V25() ext-real Element of REAL
(((GoB f) * (B2,(B1 + 1))) + ((GoB f) * ((B2 + 1),(B1 + 1)))) `1 is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * (B2,(B1 + 1))) + ((GoB f) * ((B2 + 1),(B1 + 1)))) `1) is V24() V25() ext-real Element of REAL
((GoB f) * (B2,(B1 + 1))) `1 is V24() V25() ext-real Element of REAL
((GoB f) * ((B2 + 1),(B1 + 1))) `1 is V24() V25() ext-real Element of REAL
(((GoB f) * (B2,(B1 + 1))) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1) is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * (B2,(B1 + 1))) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1)) 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) `))
Down ((Int (cell ((GoB f),B2,B1))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(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) 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) `))
(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) `))
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
(((GoB f) * ((B2 + 1),(B1 + 1))) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1) is V24() V25() ext-real Element of REAL
((((GoB f) * ((B2 + 1),(B1 + 1))) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1)) / 2 is V24() V25() ext-real Element of REAL
((((GoB f) * (B2,(B1 + 1))) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1)) / 2 is V24() V25() ext-real Element of REAL
(((GoB f) * (B2,(B1 + 1))) `1) + (((GoB f) * (B2,(B1 + 1))) `1) is V24() V25() ext-real Element of REAL
((((GoB f) * (B2,(B1 + 1))) `1) + (((GoB f) * (B2,(B1 + 1))) `1)) / 2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (B2,(B1 + 1))) `1 <= b1 & b1 <= ((GoB f) * ((B2 + 1),(B1 + 1))) `1 ) } is set
B1 `2 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)
v_strip ((GoB f),B2) is Element of bool the carrier of (TOP-REAL 2)
B1 `2 is V24() V25() ext-real Element of REAL
(((GoB f) * (B2,(B1 + 1))) + ((GoB f) * ((B2 + 1),(B1 + 1)))) `2 is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * (B2,(B1 + 1))) + ((GoB f) * ((B2 + 1),(B1 + 1)))) `2) is V24() V25() ext-real Element of REAL
((GoB f) * (B2,(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
((GoB f) * ((B2 + 1),(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
(((GoB f) * (B2,(B1 + 1))) `2) + (((GoB f) * ((B2 + 1),(B1 + 1))) `2) is V24() V25() ext-real Element of REAL
(1 / 2) * ((((GoB f) * (B2,(B1 + 1))) `2) + (((GoB f) * ((B2 + 1),(B1 + 1))) `2)) is V24() V25() ext-real Element of REAL
|[((1 / 2) * ((((GoB f) * (B2,(B1 + 1))) `1) + (((GoB f) * ((B2 + 1),(B1 + 1))) `1))),((1 / 2) * ((((GoB f) * (B2,(B1 + 1))) `2) + (((GoB f) * ((B2 + 1),(B1 + 1))) `2)))]| is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
(GoB f) * (1,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
(GoB f) * (1,((B1 + 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,((B1 + 1) + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,(B1 + 1))) `2 <= b2 & b2 <= ((GoB f) * (1,((B1 + 1) + 1))) `2 ) } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (1,B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,B1)) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,B1)) `2 <= b2 & b2 <= ((GoB f) * (1,(B1 + 1))) `2 ) } is set
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (1,B1) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,B1)) `2 is V24() V25() ext-real Element of REAL
(GoB f) * (1,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,B1)) `2 <= b2 & b2 <= ((GoB f) * (1,(B1 + 1))) `2 ) } is set
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) 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) * (1,(B1 + 1))) `2 <= b2 } is set
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(GoB f) * (1,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,(B1 + 1))) `2 is V24() V25() ext-real Element of REAL
(GoB f) * (1,((B1 + 1) + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,((B1 + 1) + 1))) `2 is V24() V25() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V24() V25() ext-real Element of REAL : ( ((GoB f) * (1,(B1 + 1))) `2 <= b2 & b2 <= ((GoB f) * (1,((B1 + 1) + 1))) `2 ) } is set
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((GoB f),(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),(B1 + 1))) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) 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)) `2 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
h_strip ((GoB f),B1) is Element of bool the carrier of (TOP-REAL 2)
(h_strip ((GoB f),B1)) /\ (v_strip ((GoB f),B2)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,B1)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f),B2,(B1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,(B1 + 1))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
(cell ((GoB f),B2,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)
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,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
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
(GoB f) * ((B2 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (B2,(B1 + 1))),((GoB f) * ((B2 + 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)
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,(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
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
(GoB f) * ((B2 + 1),(B1 + 1)) is V37(2) V79() FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (B2,(B1 + 1))),((GoB f) * ((B2 + 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)
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 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
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)
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
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 + 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 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 non empty V19() V23() V24() V25() ext-real positive 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 + 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 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 non empty V19() V23() V24() V25() ext-real positive 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 + 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 non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() 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)
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))
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)
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
B1 is V7() V10( NAT ) V11( NAT ) Function-like FinSequence-like FinSequence of NAT
len B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 is V7() V10( NAT ) V11( NAT ) Function-like FinSequence-like FinSequence of NAT
len B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
dom B1 is V89() V90() V91() V92() V93() V94() Element of bool NAT
B2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 /. B2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 /. B2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),(B1 /. B2),(B1 /. B2)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 /. B2),(B1 /. B2))) 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
B1 /. B2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 /. B2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),(B1 /. B2),(B1 /. B2)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 /. B2),(B1 /. B2))) 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
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
Seg (len B1) is V89() V90() V91() V92() V93() V94() Element of bool NAT
dom B1 is V89() V90() V91() V92() V93() V94() Element of bool NAT
B1 . B2 is set
B1 . B2 is set
Q is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(len (GoB f)) + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
x is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(width (GoB f)) + 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 -' 1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
x -' 1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
bool (REAL 2) is non empty set
Seg ((len (GoB f)) + 1) is V89() V90() V91() V92() V93() V94() Element of bool NAT
Seg ((width (GoB f)) + 1) is V89() V90() V91() V92() V93() V94() Element of bool NAT
[:(Seg ((len (GoB f)) + 1)),(Seg ((width (GoB f)) + 1)):] is set
P is V19() V23() ext-real non negative set
i is V19() V23() ext-real non negative set
[P,i] is set
{P,i} is non empty V89() V90() V91() V92() V93() V94() set
{P} is non empty V89() V90() V91() V92() V93() V94() set
{{P,i},{P}} is non empty set
P -' 1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
i -' 1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),(P -' 1),(i -' 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(P -' 1),(i -' 1))) is Element of bool the carrier of (TOP-REAL 2)
K267((bool (REAL 2))) is M11( bool (REAL 2))
P is V7() V10( NAT ) V11(K267((bool (REAL 2)))) Function-like FinSequence-like tabular Matrix of (len (GoB f)) + 1,(width (GoB f)) + 1, bool (REAL 2)
Indices P is set
P is V7() V10( NAT ) V11(K267((bool (REAL 2)))) Function-like FinSequence-like tabular Matrix of (len (GoB f)) + 1,(width (GoB f)) + 1, bool (REAL 2)
Indices P is set
len P is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
dom P is V89() V90() V91() V92() V93() V94() Element of bool NAT
width P is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
Seg (width P) is V89() V90() V91() V92() V93() V94() Element of bool NAT
i is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
kx1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
P * (i,kx1) is Element of bool (REAL 2)
kx2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
kk1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
P * (kx2,kk1) is Element of bool (REAL 2)
kx2 - 1 is V24() V25() ext-real Element of REAL
kx2 -' 1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
[kx2,kk1] is set
{kx2,kk1} is non empty V89() V90() V91() V92() V93() V94() set
{kx2} is non empty V89() V90() V91() V92() V93() V94() set
{{kx2,kk1},{kx2}} is non empty set
[:(dom P),(Seg (width P)):] is set
kk1 -' 1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),(kx2 -' 1),(kk1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(kx2 -' 1),(kk1 -' 1))) is Element of bool the carrier of (TOP-REAL 2)
i -' 1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
kx1 -' 1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
i - 1 is V24() V25() ext-real Element of REAL
[i,kx1] is set
{i,kx1} is non empty V89() V90() V91() V92() V93() V94() set
{i} is non empty V89() V90() V91() V92() V93() V94() set
{{i,kx1},{i}} is non empty set
cell ((GoB f),(i -' 1),(kx1 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(i -' 1),(kx1 -' 1))) is Element of bool the carrier of (TOP-REAL 2)
kk1 - 1 is V24() V25() ext-real Element of REAL
((len (GoB f)) + 1) - 1 is V24() V25() ext-real Element of REAL
kx1 - 1 is V24() V25() ext-real Element of REAL
((width (GoB f)) + 1) - 1 is V24() V25() ext-real Element of REAL
kk2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
jj1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
ii2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
jj2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
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,x] is set
{Q,x} is non empty V89() V90() V91() V92() V93() V94() set
{Q} is non empty V89() V90() V91() V92() V93() V94() set
{{Q,x},{Q}} is non empty set
[:(dom P),(Seg (width P)):] is set
P * (Q,x) is Element of bool (REAL 2)
j is Element of bool (REAL 2)
i is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
kx1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
P * (i,kx1) is Element of bool (REAL 2)
i is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 /. i is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 /. i is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),(B1 /. i),(B1 /. i)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),(B1 /. i),(B1 /. i))) is Element of bool the carrier of (TOP-REAL 2)
kx1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
kx1 + 1 is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
kx2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
kx2 + 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 . i is set
B1 . i is set
kk1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
kk2 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
[kk1,kk2] is set
{kk1,kk2} is non empty V89() V90() V91() V92() V93() V94() set
{kk1} is non empty V89() V90() V91() V92() V93() V94() set
{{kk1,kk2},{kk1}} is non empty set
kk1 -' 1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
kk2 -' 1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
P * (kk1,kk2) is Element of bool (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
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)
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
len f is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
left_cell (f,1) is Element of bool the carrier of (TOP-REAL 2)
Int (left_cell (f,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 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)
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 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)
B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
Q is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),B1,Q) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),B1,Q)) is Element of bool the carrier of (TOP-REAL 2)
B1 -' B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 -' B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(B1 -' B1) + (B1 -' B1) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
B1 -' Q is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
((B1 -' B1) + (B1 -' B1)) + (B1 -' Q) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
Q -' B1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
(((B1 -' B1) + (B1 -' B1)) + (B1 -' Q)) + (Q -' B1) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
((((B1 -' B1) + (B1 -' B1)) + (B1 -' Q)) + (Q -' 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
x is V7() V10( NAT ) V11( NAT ) Function-like FinSequence-like FinSequence of NAT
dom x is V89() V90() V91() V92() V93() V94() Element of bool NAT
y is V7() V10( NAT ) V11( NAT ) Function-like FinSequence-like FinSequence of NAT
x . 1 is set
len x is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
x . (len x) is set
y . 1 is set
len y is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
y . (len y) is set
1 + ((((B1 -' B1) + (B1 -' B1)) + (B1 -' Q)) + (Q -' B1)) is non empty V19() V23() V24() V25() ext-real positive non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
x /. 1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
dom y is V89() V90() V91() V92() V93() V94() Element of bool NAT
y /. (len x) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
y /. 1 is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
x /. (len x) is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() 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)
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)
(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
bool the carrier of ((TOP-REAL 2) | ((L~ f) `)) is non empty set
B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
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
B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Cl B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Cl (RightComp f) is Element of bool the carrier of (TOP-REAL 2)
[#] ((TOP-REAL 2) | ((L~ f) `)) is non empty non proper closed Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Cl (RightComp f)) /\ ([#] ((TOP-REAL 2) | ((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Cl (RightComp f)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
B2 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) `))
Cl B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Cl (LeftComp f) is Element of bool the carrier of (TOP-REAL 2)
(Cl (LeftComp f)) /\ ([#] ((TOP-REAL 2) | ((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Cl (LeftComp f)) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Cl (LeftComp f)) \/ (Cl (RightComp f)) is Element of bool the carrier of (TOP-REAL 2)
((Cl (LeftComp f)) \/ (Cl (RightComp f))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
((Cl (LeftComp f)) /\ ((L~ f) `)) \/ ((Cl (RightComp f)) /\ ((L~ f) `)) is Element of bool the carrier of (TOP-REAL 2)
x is set
Cl ((LeftComp f) \/ (RightComp f)) is Element of bool the carrier of (TOP-REAL 2)
y is set
i is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
j is V19() V23() V24() V25() ext-real non negative V87() V88() V89() V90() V91() V92() V93() V94() Element of NAT
cell ((GoB f),i,j) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f),i,j)) is Element of bool the carrier of (TOP-REAL 2)
Down ((Int (cell ((GoB f),i,j))),((L~ f) `)) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
(Int (cell ((GoB f),i,j))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Cl (Down ((Int (cell ((GoB f),i,j))),((L~ f) `))) is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))
Cl (Int (cell ((GoB f),i,j))) is Element of bool the carrier of (TOP-REAL 2)
(Cl (Int (cell ((GoB f),i,j)))) /\ ((L~ f) `) is Element of bool the carrier of (TOP-REAL 2)
Q is Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | Q is strict TopSpace-like SubSpace of TOP-REAL 2
P is Element of bool the carrier of (TOP-REAL 2)
Down (P,Q) is Element of bool the carrier of ((TOP-REAL 2) | Q)
the carrier of ((TOP-REAL 2) | Q) is set
bool the carrier of ((TOP-REAL 2) | Q) is non empty set
P /\ Q is Element of bool the carrier of (TOP-REAL 2)
Cl (Down (P,Q)) is Element of bool the carrier of ((TOP-REAL 2) | Q)
Cl P is Element of bool the carrier of (TOP-REAL 2)
(Cl P) /\ Q is Element of bool the carrier of (TOP-REAL 2)
B1 is Element of bool the carrier of ((TOP-REAL 2) | ((L~ f) `))