REAL is non empty V34() V165() V166() V167() V171() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V165() V166() V167() V168() V169() V170() V171() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V34() V165() V171() set
omega is non empty epsilon-transitive epsilon-connected ordinal V165() V166() V167() V168() V169() V170() V171() set
K6(omega) is set
K6(NAT) is set
RAT is non empty V34() V165() V166() V167() V168() V171() set
INT is non empty V34() V165() V166() V167() V168() V169() V171() set
K7(REAL,REAL) is set
K6(K7(REAL,REAL)) is set
K387() is non empty V114() L9()
the U1 of K387() is non empty set
K392() is non empty V114() V136() V137() V138() V140() V187() V188() V189() V190() V191() V192() L9()
K393() is non empty V114() V138() V140() V190() V191() V192() M17(K392())
K394() is non empty V114() V136() V138() V140() V190() V191() V192() V193() M20(K392(),K393())
K396() is non empty V114() V136() V138() V140() L9()
K397() is non empty V114() V136() V138() V140() V193() M17(K396())
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
K7(1,1) is set
K6(K7(1,1)) is set
K7(K7(1,1),1) is set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is set
K6(K7(K7(1,1),REAL)) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
K7(2,2) is set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V112() V177() V178() V210() V211() V212() V213() V214() V215() V216() strict add-continuous Mult-continuous RLTopStruct
the U1 of (TOP-REAL 2) is non empty set
K7( the U1 of (TOP-REAL 2),REAL) is set
K6(K7( the U1 of (TOP-REAL 2),REAL)) is set
K6( the U1 of (TOP-REAL 2)) is set
K358( the U1 of (TOP-REAL 2)) is M14( the U1 of (TOP-REAL 2))
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V165() V166() V167() V168() V169() V170() V171() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V165() V166() V167() V168() V169() V170() V171() set
0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
proj1 is V21() V24( the U1 of (TOP-REAL 2)) V25( REAL ) Function-like V46( the U1 of (TOP-REAL 2), REAL ) V227( TOP-REAL 2) Element of K6(K7( the U1 of (TOP-REAL 2),REAL))
proj2 is V21() V24( the U1 of (TOP-REAL 2)) V25( REAL ) Function-like V46( the U1 of (TOP-REAL 2), REAL ) V227( TOP-REAL 2) Element of K6(K7( the U1 of (TOP-REAL 2),REAL))
2 * 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(2 * 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
3 div 2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
2 * 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(2 * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
1 div 2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
n is V21() Function-like FinSequence-like set
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(len n) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
((len n) div 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
n is V21() Function-like FinSequence-like set
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(len n) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
((len n) div 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
2 * (n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(2 * (n)) - 1 is V11() real ext-real Element of REAL
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
2 * C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(2 * C) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(2 * C) mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(2 * C) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
((2 * C) div 2) + (1 div 2) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
2 * (((2 * C) div 2) + (1 div 2)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(2 * (((2 * C) div 2) + (1 div 2))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
2 * ((len n) div 2) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(2 * 1) - 1 is V11() real ext-real Element of REAL
(2 * ((len n) div 2)) + ((2 * 1) - 1) is V11() real ext-real Element of REAL
n is V21() Function-like FinSequence-like set
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(len n) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
((len n) div 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
2 * (n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(2 * (n)) - 2 is V11() real ext-real Element of REAL
2 * ((len n) div 2) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(2 * ((len n) div 2)) + (2 * 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
((2 * ((len n) div 2)) + (2 * 1)) - 2 is V11() real ext-real Element of REAL
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
2 * C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
the non empty V2() V21() V24( NAT ) V25( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like V231( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2) is non empty V2() V21() V24( NAT ) V25( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like V231( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
L~ the non empty V2() V21() V24( NAT ) V25( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like V231( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2) is non empty boundary connected bounded being_simple_closed_curve compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
n is non empty Element of K6( the U1 of (TOP-REAL 2))
N-most n is Element of K6( the U1 of (TOP-REAL 2))
NW-corner n is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
W-bound n is V11() real ext-real Element of REAL
(TOP-REAL 2) | n is strict SubSpace of TOP-REAL 2
proj1 | n is V21() V24( the U1 of ((TOP-REAL 2) | n)) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | n), REAL ) V227((TOP-REAL 2) | n) Element of K6(K7( the U1 of ((TOP-REAL 2) | n),REAL))
the U1 of ((TOP-REAL 2) | n) is set
K7( the U1 of ((TOP-REAL 2) | n),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | n),REAL)) is set
K471(((TOP-REAL 2) | n),(proj1 | n)) is V11() real ext-real Element of REAL
N-bound n is V11() real ext-real Element of REAL
proj2 | n is V21() V24( the U1 of ((TOP-REAL 2) | n)) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | n), REAL ) V227((TOP-REAL 2) | n) Element of K6(K7( the U1 of ((TOP-REAL 2) | n),REAL))
K472(((TOP-REAL 2) | n),(proj2 | n)) is V11() real ext-real Element of REAL
|[(W-bound n),(N-bound n)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
NE-corner n is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
E-bound n is V11() real ext-real Element of REAL
K472(((TOP-REAL 2) | n),(proj1 | n)) is V11() real ext-real Element of REAL
|[(E-bound n),(N-bound n)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
LSeg ((NW-corner n),(NE-corner n)) is boundary connected horizontal Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((NW-corner n),(NE-corner n))) /\ n is Element of K6( the U1 of (TOP-REAL 2))
C is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
C `2 is V11() real ext-real Element of REAL
(NE-corner n) `2 is V11() real ext-real Element of REAL
(NW-corner n) `2 is V11() real ext-real Element of REAL
n is non empty Element of K6( the U1 of (TOP-REAL 2))
E-most n is Element of K6( the U1 of (TOP-REAL 2))
SE-corner n is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
E-bound n is V11() real ext-real Element of REAL
(TOP-REAL 2) | n is strict SubSpace of TOP-REAL 2
proj1 | n is V21() V24( the U1 of ((TOP-REAL 2) | n)) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | n), REAL ) V227((TOP-REAL 2) | n) Element of K6(K7( the U1 of ((TOP-REAL 2) | n),REAL))
the U1 of ((TOP-REAL 2) | n) is set
K7( the U1 of ((TOP-REAL 2) | n),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | n),REAL)) is set
K472(((TOP-REAL 2) | n),(proj1 | n)) is V11() real ext-real Element of REAL
S-bound n is V11() real ext-real Element of REAL
proj2 | n is V21() V24( the U1 of ((TOP-REAL 2) | n)) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | n), REAL ) V227((TOP-REAL 2) | n) Element of K6(K7( the U1 of ((TOP-REAL 2) | n),REAL))
K471(((TOP-REAL 2) | n),(proj2 | n)) is V11() real ext-real Element of REAL
|[(E-bound n),(S-bound n)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
NE-corner n is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
N-bound n is V11() real ext-real Element of REAL
K472(((TOP-REAL 2) | n),(proj2 | n)) is V11() real ext-real Element of REAL
|[(E-bound n),(N-bound n)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner n),(NE-corner n)) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SE-corner n),(NE-corner n))) /\ n is Element of K6( the U1 of (TOP-REAL 2))
C is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
(SE-corner n) `1 is V11() real ext-real Element of REAL
(NE-corner n) `1 is V11() real ext-real Element of REAL
n is non empty Element of K6( the U1 of (TOP-REAL 2))
S-most n is Element of K6( the U1 of (TOP-REAL 2))
SW-corner n is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
W-bound n is V11() real ext-real Element of REAL
(TOP-REAL 2) | n is strict SubSpace of TOP-REAL 2
proj1 | n is V21() V24( the U1 of ((TOP-REAL 2) | n)) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | n), REAL ) V227((TOP-REAL 2) | n) Element of K6(K7( the U1 of ((TOP-REAL 2) | n),REAL))
the U1 of ((TOP-REAL 2) | n) is set
K7( the U1 of ((TOP-REAL 2) | n),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | n),REAL)) is set
K471(((TOP-REAL 2) | n),(proj1 | n)) is V11() real ext-real Element of REAL
S-bound n is V11() real ext-real Element of REAL
proj2 | n is V21() V24( the U1 of ((TOP-REAL 2) | n)) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | n), REAL ) V227((TOP-REAL 2) | n) Element of K6(K7( the U1 of ((TOP-REAL 2) | n),REAL))
K471(((TOP-REAL 2) | n),(proj2 | n)) is V11() real ext-real Element of REAL
|[(W-bound n),(S-bound n)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
SE-corner n is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
E-bound n is V11() real ext-real Element of REAL
K472(((TOP-REAL 2) | n),(proj1 | n)) is V11() real ext-real Element of REAL
|[(E-bound n),(S-bound n)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner n),(SE-corner n)) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner n),(SE-corner n))) /\ n is Element of K6( the U1 of (TOP-REAL 2))
C is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
C `2 is V11() real ext-real Element of REAL
(SE-corner n) `2 is V11() real ext-real Element of REAL
(SW-corner n) `2 is V11() real ext-real Element of REAL
n is non empty Element of K6( the U1 of (TOP-REAL 2))
W-most n is Element of K6( the U1 of (TOP-REAL 2))
SW-corner n is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
W-bound n is V11() real ext-real Element of REAL
(TOP-REAL 2) | n is strict SubSpace of TOP-REAL 2
proj1 | n is V21() V24( the U1 of ((TOP-REAL 2) | n)) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | n), REAL ) V227((TOP-REAL 2) | n) Element of K6(K7( the U1 of ((TOP-REAL 2) | n),REAL))
the U1 of ((TOP-REAL 2) | n) is set
K7( the U1 of ((TOP-REAL 2) | n),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | n),REAL)) is set
K471(((TOP-REAL 2) | n),(proj1 | n)) is V11() real ext-real Element of REAL
S-bound n is V11() real ext-real Element of REAL
proj2 | n is V21() V24( the U1 of ((TOP-REAL 2) | n)) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | n), REAL ) V227((TOP-REAL 2) | n) Element of K6(K7( the U1 of ((TOP-REAL 2) | n),REAL))
K471(((TOP-REAL 2) | n),(proj2 | n)) is V11() real ext-real Element of REAL
|[(W-bound n),(S-bound n)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
NW-corner n is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
N-bound n is V11() real ext-real Element of REAL
K472(((TOP-REAL 2) | n),(proj2 | n)) is V11() real ext-real Element of REAL
|[(W-bound n),(N-bound n)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner n),(NW-corner n)) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner n),(NW-corner n))) /\ n is Element of K6( the U1 of (TOP-REAL 2))
C is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
(SW-corner n) `1 is V11() real ext-real Element of REAL
(NW-corner n) `1 is V11() real ext-real Element of REAL
n is Element of K6( the U1 of (TOP-REAL 2))
BDD n is Element of K6( the U1 of (TOP-REAL 2))
n ` is Element of K6( the U1 of (TOP-REAL 2))
n is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
n `1 is V11() real ext-real Element of REAL
Vertical_Line (n `1) is Element of K6( the U1 of (TOP-REAL 2))
{ b1 where b1 is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2) : n `1 = b1 `1 } is set
n is V11() real ext-real set
Vertical_Line n is Element of K6( the U1 of (TOP-REAL 2))
C is V11() real ext-real set
|[n,C]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
|[n,C]| `1 is V11() real ext-real Element of REAL
n is V11() real ext-real set
Vertical_Line n is Element of K6( the U1 of (TOP-REAL 2))
{ b1 where b1 is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2) : b1 `1 = n } is set
C is Element of K6( the U1 of (TOP-REAL 2))
x is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
f is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
x `1 is V11() real ext-real Element of REAL
f `1 is V11() real ext-real Element of REAL
p is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
p `1 is V11() real ext-real Element of REAL
p is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
p `1 is V11() real ext-real Element of REAL
n is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
n `1 is V11() real ext-real Element of REAL
proj2 . n is V11() real ext-real Element of REAL
C is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
proj2 . C is V11() real ext-real Element of REAL
[.(proj2 . n),(proj2 . C).] is V165() V166() V167() Element of K6(REAL)
LSeg (n,C) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
x is V11() real ext-real set
|[(n `1),x]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
|[(n `1),x]| `2 is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
n `2 is V11() real ext-real Element of REAL
|[(n `1),x]| `1 is V11() real ext-real Element of REAL
n is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
n `2 is V11() real ext-real Element of REAL
proj1 . n is V11() real ext-real Element of REAL
C is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
C `2 is V11() real ext-real Element of REAL
proj1 . C is V11() real ext-real Element of REAL
[.(proj1 . n),(proj1 . C).] is V165() V166() V167() Element of K6(REAL)
LSeg (n,C) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
x is V11() real ext-real set
|[x,(n `2)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
|[x,(n `2)]| `1 is V11() real ext-real Element of REAL
C `1 is V11() real ext-real Element of REAL
n `1 is V11() real ext-real Element of REAL
|[x,(n `2)]| `2 is V11() real ext-real Element of REAL
n is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
C is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
LSeg (n,C) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
x is V11() real ext-real set
Vertical_Line x is Element of K6( the U1 of (TOP-REAL 2))
{ b1 where b1 is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2) : b1 `1 = x } is set
n `1 is V11() real ext-real Element of REAL
C `1 is V11() real ext-real Element of REAL
f is set
p is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
p `1 is V11() real ext-real Element of REAL
n is Element of K6( the U1 of (TOP-REAL 2))
C is Element of K6( the U1 of (TOP-REAL 2))
proj2 .: n is V165() V166() V167() Element of K6(REAL)
proj2 .: C is V165() V166() V167() Element of K6(REAL)
x is set
f is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
f `2 is V11() real ext-real Element of REAL
proj2 . f is V11() real ext-real Element of REAL
n is V11() real ext-real set
Vertical_Line n is Element of K6( the U1 of (TOP-REAL 2))
C is Element of K6( the U1 of (TOP-REAL 2))
x is Element of K6( the U1 of (TOP-REAL 2))
proj2 .: C is V165() V166() V167() Element of K6(REAL)
proj2 .: x is V165() V166() V167() Element of K6(REAL)
f is set
p is V11() real ext-real Element of REAL
p is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
proj2 . p is V11() real ext-real Element of REAL
p `1 is V11() real ext-real Element of REAL
a is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
proj2 . a is V11() real ext-real Element of REAL
a `1 is V11() real ext-real Element of REAL
a `2 is V11() real ext-real Element of REAL
|[(p `1),(a `2)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
|[(p `1),p]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
p `2 is V11() real ext-real Element of REAL
|[(p `1),(p `2)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
len x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
width x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x * (n,C) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
x * (n,1) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
x * (n,(width x)) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
LSeg ((x * (n,1)),(x * (n,(width x)))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(x * (n,C)) `2 is V11() real ext-real Element of REAL
(x * (n,(width x))) `2 is V11() real ext-real Element of REAL
(x * (n,1)) `1 is V11() real ext-real Element of REAL
(x * (n,(width x))) `1 is V11() real ext-real Element of REAL
(x * (n,C)) `1 is V11() real ext-real Element of REAL
(x * (n,1)) `2 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
len x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
width x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x * (n,C) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
x * (1,C) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
x * ((len x),C) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
LSeg ((x * (1,C)),(x * ((len x),C))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(x * (n,C)) `1 is V11() real ext-real Element of REAL
(x * ((len x),C)) `1 is V11() real ext-real Element of REAL
(x * (1,C)) `2 is V11() real ext-real Element of REAL
(x * ((len x),C)) `2 is V11() real ext-real Element of REAL
(x * (n,C)) `2 is V11() real ext-real Element of REAL
(x * (1,C)) `1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
p is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
width p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
len p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
p * (x,n) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(p * (x,n)) `1 is V11() real ext-real Element of REAL
p * (f,C) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(p * (f,C)) `1 is V11() real ext-real Element of REAL
p * (f,n) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(p * (f,n)) `1 is V11() real ext-real Element of REAL
p * (f,1) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(p * (f,1)) `1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
p is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
len p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
width p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
p * (n,x) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(p * (n,x)) `2 is V11() real ext-real Element of REAL
p * (C,f) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(p * (C,f)) `2 is V11() real ext-real Element of REAL
p * (n,f) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(p * (n,f)) `2 is V11() real ext-real Element of REAL
p * (1,f) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(p * (1,f)) `2 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
width C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C * (n,(width C)) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * (n,(width C))) `2 is V11() real ext-real Element of REAL
x is non empty V2() V21() V24( NAT ) V25( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like V231( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
L~ x is non empty boundary connected bounded being_simple_closed_curve compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
N-bound (L~ x) is V11() real ext-real Element of REAL
(TOP-REAL 2) | (L~ x) is strict compact SubSpace of TOP-REAL 2
proj2 | (L~ x) is V21() V24( the U1 of ((TOP-REAL 2) | (L~ x))) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (L~ x)), REAL ) V227((TOP-REAL 2) | (L~ x)) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL))
the U1 of ((TOP-REAL 2) | (L~ x)) is set
K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL)) is set
K472(((TOP-REAL 2) | (L~ x)),(proj2 | (L~ x))) is V11() real ext-real Element of REAL
N-min (L~ x) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
N-most (L~ x) is non empty bounded compact Element of K6( the U1 of (TOP-REAL 2))
NW-corner (L~ x) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
W-bound (L~ x) is V11() real ext-real Element of REAL
proj1 | (L~ x) is V21() V24( the U1 of ((TOP-REAL 2) | (L~ x))) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (L~ x)), REAL ) V227((TOP-REAL 2) | (L~ x)) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL))
K471(((TOP-REAL 2) | (L~ x)),(proj1 | (L~ x))) is V11() real ext-real Element of REAL
|[(W-bound (L~ x)),(N-bound (L~ x))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ x) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
E-bound (L~ x) is V11() real ext-real Element of REAL
K472(((TOP-REAL 2) | (L~ x)),(proj1 | (L~ x))) is V11() real ext-real Element of REAL
|[(E-bound (L~ x)),(N-bound (L~ x))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
LSeg ((NW-corner (L~ x)),(NE-corner (L~ x))) is boundary connected horizontal Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((NW-corner (L~ x)),(NE-corner (L~ x)))) /\ (L~ x) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (N-most (L~ x)) is strict compact SubSpace of TOP-REAL 2
proj1 | (N-most (L~ x)) is V21() V24( the U1 of ((TOP-REAL 2) | (N-most (L~ x)))) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (N-most (L~ x))), REAL ) V227((TOP-REAL 2) | (N-most (L~ x))) Element of K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ x))),REAL))
the U1 of ((TOP-REAL 2) | (N-most (L~ x))) is set
K7( the U1 of ((TOP-REAL 2) | (N-most (L~ x))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ x))),REAL)) is set
K471(((TOP-REAL 2) | (N-most (L~ x))),(proj1 | (N-most (L~ x)))) is V11() real ext-real Element of REAL
|[K471(((TOP-REAL 2) | (N-most (L~ x))),(proj1 | (N-most (L~ x)))),(N-bound (L~ x))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
rng x is V2() Element of K6( the U1 of (TOP-REAL 2))
dom x is V2() V165() V166() V167() V168() V169() V170() Element of K6(NAT)
f is set
x . f is set
Indices C is set
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x /. p is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
[p,a] is set
{p,a} is V165() V166() V167() V168() V169() V170() set
{p} is V165() V166() V167() V168() V169() V170() set
{{p,a},{p}} is set
C * (p,a) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(N-min (L~ x)) `2 is V11() real ext-real Element of REAL
(C * (p,a)) `2 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
width C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C * (1,n) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * (1,n)) `1 is V11() real ext-real Element of REAL
x is non empty V2() V21() V24( NAT ) V25( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like V231( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
L~ x is non empty boundary connected bounded being_simple_closed_curve compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
W-bound (L~ x) is V11() real ext-real Element of REAL
(TOP-REAL 2) | (L~ x) is strict compact SubSpace of TOP-REAL 2
proj1 | (L~ x) is V21() V24( the U1 of ((TOP-REAL 2) | (L~ x))) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (L~ x)), REAL ) V227((TOP-REAL 2) | (L~ x)) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL))
the U1 of ((TOP-REAL 2) | (L~ x)) is set
K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL)) is set
K471(((TOP-REAL 2) | (L~ x)),(proj1 | (L~ x))) is V11() real ext-real Element of REAL
W-min (L~ x) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
W-most (L~ x) is non empty bounded compact Element of K6( the U1 of (TOP-REAL 2))
SW-corner (L~ x) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
S-bound (L~ x) is V11() real ext-real Element of REAL
proj2 | (L~ x) is V21() V24( the U1 of ((TOP-REAL 2) | (L~ x))) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (L~ x)), REAL ) V227((TOP-REAL 2) | (L~ x)) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL))
K471(((TOP-REAL 2) | (L~ x)),(proj2 | (L~ x))) is V11() real ext-real Element of REAL
|[(W-bound (L~ x)),(S-bound (L~ x))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ x) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
N-bound (L~ x) is V11() real ext-real Element of REAL
K472(((TOP-REAL 2) | (L~ x)),(proj2 | (L~ x))) is V11() real ext-real Element of REAL
|[(W-bound (L~ x)),(N-bound (L~ x))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ x)),(NW-corner (L~ x))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ x)),(NW-corner (L~ x)))) /\ (L~ x) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ x)) is strict compact SubSpace of TOP-REAL 2
proj2 | (W-most (L~ x)) is V21() V24( the U1 of ((TOP-REAL 2) | (W-most (L~ x)))) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (W-most (L~ x))), REAL ) V227((TOP-REAL 2) | (W-most (L~ x))) Element of K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ x))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ x))) is set
K7( the U1 of ((TOP-REAL 2) | (W-most (L~ x))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ x))),REAL)) is set
K471(((TOP-REAL 2) | (W-most (L~ x))),(proj2 | (W-most (L~ x)))) is V11() real ext-real Element of REAL
|[(W-bound (L~ x)),K471(((TOP-REAL 2) | (W-most (L~ x))),(proj2 | (W-most (L~ x))))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
rng x is V2() Element of K6( the U1 of (TOP-REAL 2))
dom x is V2() V165() V166() V167() V168() V169() V170() Element of K6(NAT)
f is set
x . f is set
Indices C is set
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x /. p is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
[p,a] is set
{p,a} is V165() V166() V167() V168() V169() V170() set
{p} is V165() V166() V167() V168() V169() V170() set
{{p,a},{p}} is set
C * (p,a) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(W-min (L~ x)) `1 is V11() real ext-real Element of REAL
(C * (p,a)) `1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C * (n,1) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * (n,1)) `2 is V11() real ext-real Element of REAL
x is non empty V2() V21() V24( NAT ) V25( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like V231( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
L~ x is non empty boundary connected bounded being_simple_closed_curve compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
S-bound (L~ x) is V11() real ext-real Element of REAL
(TOP-REAL 2) | (L~ x) is strict compact SubSpace of TOP-REAL 2
proj2 | (L~ x) is V21() V24( the U1 of ((TOP-REAL 2) | (L~ x))) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (L~ x)), REAL ) V227((TOP-REAL 2) | (L~ x)) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL))
the U1 of ((TOP-REAL 2) | (L~ x)) is set
K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL)) is set
K471(((TOP-REAL 2) | (L~ x)),(proj2 | (L~ x))) is V11() real ext-real Element of REAL
S-min (L~ x) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
S-most (L~ x) is non empty bounded compact Element of K6( the U1 of (TOP-REAL 2))
SW-corner (L~ x) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
W-bound (L~ x) is V11() real ext-real Element of REAL
proj1 | (L~ x) is V21() V24( the U1 of ((TOP-REAL 2) | (L~ x))) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (L~ x)), REAL ) V227((TOP-REAL 2) | (L~ x)) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL))
K471(((TOP-REAL 2) | (L~ x)),(proj1 | (L~ x))) is V11() real ext-real Element of REAL
|[(W-bound (L~ x)),(S-bound (L~ x))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
SE-corner (L~ x) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
E-bound (L~ x) is V11() real ext-real Element of REAL
K472(((TOP-REAL 2) | (L~ x)),(proj1 | (L~ x))) is V11() real ext-real Element of REAL
|[(E-bound (L~ x)),(S-bound (L~ x))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
LSeg ((SW-corner (L~ x)),(SE-corner (L~ x))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ x)),(SE-corner (L~ x)))) /\ (L~ x) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (S-most (L~ x)) is strict compact SubSpace of TOP-REAL 2
proj1 | (S-most (L~ x)) is V21() V24( the U1 of ((TOP-REAL 2) | (S-most (L~ x)))) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (S-most (L~ x))), REAL ) V227((TOP-REAL 2) | (S-most (L~ x))) Element of K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ x))),REAL))
the U1 of ((TOP-REAL 2) | (S-most (L~ x))) is set
K7( the U1 of ((TOP-REAL 2) | (S-most (L~ x))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ x))),REAL)) is set
K471(((TOP-REAL 2) | (S-most (L~ x))),(proj1 | (S-most (L~ x)))) is V11() real ext-real Element of REAL
|[K471(((TOP-REAL 2) | (S-most (L~ x))),(proj1 | (S-most (L~ x)))),(S-bound (L~ x))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
rng x is V2() Element of K6( the U1 of (TOP-REAL 2))
dom x is V2() V165() V166() V167() V168() V169() V170() Element of K6(NAT)
f is set
x . f is set
Indices C is set
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x /. p is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
[p,a] is set
{p,a} is V165() V166() V167() V168() V169() V170() set
{p} is V165() V166() V167() V168() V169() V170() set
{{p,a},{p}} is set
C * (p,a) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
width C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(S-min (L~ x)) `2 is V11() real ext-real Element of REAL
(C * (p,a)) `2 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
width C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C * ((len C),n) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * ((len C),n)) `1 is V11() real ext-real Element of REAL
x is non empty V2() V21() V24( NAT ) V25( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like V231( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
L~ x is non empty boundary connected bounded being_simple_closed_curve compact non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
E-bound (L~ x) is V11() real ext-real Element of REAL
(TOP-REAL 2) | (L~ x) is strict compact SubSpace of TOP-REAL 2
proj1 | (L~ x) is V21() V24( the U1 of ((TOP-REAL 2) | (L~ x))) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (L~ x)), REAL ) V227((TOP-REAL 2) | (L~ x)) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL))
the U1 of ((TOP-REAL 2) | (L~ x)) is set
K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL)) is set
K472(((TOP-REAL 2) | (L~ x)),(proj1 | (L~ x))) is V11() real ext-real Element of REAL
E-min (L~ x) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
E-most (L~ x) is non empty bounded compact Element of K6( the U1 of (TOP-REAL 2))
SE-corner (L~ x) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
S-bound (L~ x) is V11() real ext-real Element of REAL
proj2 | (L~ x) is V21() V24( the U1 of ((TOP-REAL 2) | (L~ x))) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (L~ x)), REAL ) V227((TOP-REAL 2) | (L~ x)) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ x)),REAL))
K471(((TOP-REAL 2) | (L~ x)),(proj2 | (L~ x))) is V11() real ext-real Element of REAL
|[(E-bound (L~ x)),(S-bound (L~ x))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ x) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
N-bound (L~ x) is V11() real ext-real Element of REAL
K472(((TOP-REAL 2) | (L~ x)),(proj2 | (L~ x))) is V11() real ext-real Element of REAL
|[(E-bound (L~ x)),(N-bound (L~ x))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ x)),(NE-corner (L~ x))) is boundary connected Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SE-corner (L~ x)),(NE-corner (L~ x)))) /\ (L~ x) is Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ x)) is strict compact SubSpace of TOP-REAL 2
proj2 | (E-most (L~ x)) is V21() V24( the U1 of ((TOP-REAL 2) | (E-most (L~ x)))) V25( REAL ) Function-like V46( the U1 of ((TOP-REAL 2) | (E-most (L~ x))), REAL ) V227((TOP-REAL 2) | (E-most (L~ x))) Element of K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ x))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ x))) is set
K7( the U1 of ((TOP-REAL 2) | (E-most (L~ x))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ x))),REAL)) is set
K471(((TOP-REAL 2) | (E-most (L~ x))),(proj2 | (E-most (L~ x)))) is V11() real ext-real Element of REAL
|[(E-bound (L~ x)),K471(((TOP-REAL 2) | (E-most (L~ x))),(proj2 | (E-most (L~ x))))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
rng x is V2() Element of K6( the U1 of (TOP-REAL 2))
dom x is V2() V165() V166() V167() V168() V169() V170() Element of K6(NAT)
f is set
x . f is set
Indices C is set
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x /. p is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
[p,a] is set
{p,a} is V165() V166() V167() V168() V169() V170() set
{p} is V165() V166() V167() V168() V169() V170() set
{{p,a},{p}} is set
C * (p,a) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(E-min (L~ x)) `1 is V11() real ext-real Element of REAL
(C * (p,a)) `1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
len x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
width x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
cell (x,n,C) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell (x,n,C)) is Element of K6( the U1 of (TOP-REAL 2))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
len x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
width x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
cell (x,n,C) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell (x,n,C)) is Element of K6( the U1 of (TOP-REAL 2))
Cl (Int (cell (x,n,C))) is Element of K6( the U1 of (TOP-REAL 2))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
cell (C,n,0) is Element of K6( the U1 of (TOP-REAL 2))
C * (1,1) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * (1,1)) `1 is V11() real ext-real Element of REAL
(C * (1,1)) `2 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( b1 <= (C * (1,1)) `1 & b2 <= (C * (1,1)) `2 ) } is set
x is V11() real ext-real Element of REAL
- x is V11() real ext-real Element of REAL
min ((- x),((C * (1,1)) `1)) is V11() real ext-real Element of REAL
min ((- x),((C * (1,1)) `2)) is V11() real ext-real Element of REAL
|[(min ((- x),((C * (1,1)) `1))),(min ((- x),((C * (1,1)) `2)))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
f is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
|.f.| is V11() real ext-real non negative Element of REAL
f `1 is V11() real ext-real Element of REAL
abs (f `1) is V11() real ext-real Element of REAL
abs (- x) is V11() real ext-real Element of REAL
- (- x) is V11() real ext-real Element of REAL
C * (n,1) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * (n,1)) `1 is V11() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C * ((n + 1),1) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * ((n + 1),1)) `1 is V11() real ext-real Element of REAL
C * (1,1) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * (1,1)) `2 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( (C * (n,1)) `1 <= b1 & b1 <= (C * ((n + 1),1)) `1 & b2 <= (C * (1,1)) `2 ) } is set
x is V11() real ext-real Element of REAL
- x is V11() real ext-real Element of REAL
min ((- x),((C * (1,1)) `2)) is V11() real ext-real Element of REAL
|[((C * (n,1)) `1),(min ((- x),((C * (1,1)) `2)))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
f is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
|.f.| is V11() real ext-real non negative Element of REAL
width C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
f `2 is V11() real ext-real Element of REAL
abs (f `2) is V11() real ext-real Element of REAL
abs (- x) is V11() real ext-real Element of REAL
- (- x) is V11() real ext-real Element of REAL
C * ((len C),1) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * ((len C),1)) `1 is V11() real ext-real Element of REAL
C * (1,1) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * (1,1)) `2 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( (C * ((len C),1)) `1 <= b1 & b2 <= (C * (1,1)) `2 ) } is set
x is V11() real ext-real Element of REAL
max (x,((C * ((len C),1)) `1)) is V11() real ext-real Element of REAL
|[(max (x,((C * ((len C),1)) `1))),((C * (1,1)) `2)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
f is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
|.f.| is V11() real ext-real non negative Element of REAL
f `1 is V11() real ext-real Element of REAL
abs (f `1) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
width C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
cell (C,n,(width C)) is Element of K6( the U1 of (TOP-REAL 2))
cell (C,0,(width C)) is Element of K6( the U1 of (TOP-REAL 2))
C * (1,1) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * (1,1)) `1 is V11() real ext-real Element of REAL
C * (1,(width C)) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * (1,(width C))) `2 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( b1 <= (C * (1,1)) `1 & (C * (1,(width C))) `2 <= b2 ) } is set
x is V11() real ext-real Element of REAL
- x is V11() real ext-real Element of REAL
min ((- x),((C * (1,1)) `1)) is V11() real ext-real Element of REAL
|[(min ((- x),((C * (1,1)) `1))),((C * (1,(width C))) `2)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
f is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
|.f.| is V11() real ext-real non negative Element of REAL
f `1 is V11() real ext-real Element of REAL
abs (f `1) is V11() real ext-real Element of REAL
abs (- x) is V11() real ext-real Element of REAL
- (- x) is V11() real ext-real Element of REAL
C * (n,1) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * (n,1)) `1 is V11() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C * ((n + 1),1) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * ((n + 1),1)) `1 is V11() real ext-real Element of REAL
C * (1,(width C)) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * (1,(width C))) `2 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( (C * (n,1)) `1 <= b1 & b1 <= (C * ((n + 1),1)) `1 & (C * (1,(width C))) `2 <= b2 ) } is set
x is V11() real ext-real Element of REAL
max (x,((C * (1,(width C))) `2)) is V11() real ext-real Element of REAL
|[((C * (n,1)) `1),(max (x,((C * (1,(width C))) `2)))]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
f is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
|.f.| is V11() real ext-real non negative Element of REAL
f `2 is V11() real ext-real Element of REAL
abs (f `2) is V11() real ext-real Element of REAL
cell (C,(len C),(width C)) is Element of K6( the U1 of (TOP-REAL 2))
C * ((len C),1) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * ((len C),1)) `1 is V11() real ext-real Element of REAL
C * (1,(width C)) is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
(C * (1,(width C))) `2 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( (C * ((len C),1)) `1 <= b1 & (C * (1,(width C))) `2 <= b2 ) } is set
x is V11() real ext-real Element of REAL
max (x,((C * ((len C),1)) `1)) is V11() real ext-real Element of REAL
|[(max (x,((C * ((len C),1)) `1))),((C * (1,(width C))) `2)]| is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
f is V21() Function-like V41(2) FinSequence-like V157() Element of the U1 of (TOP-REAL 2)
|.f.| is V11() real ext-real non negative Element of REAL
f `1 is V11() real ext-real Element of REAL
abs (f `1) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
2 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(2 |^ n) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is non empty Element of K6( the U1 of (TOP-REAL 2))
Gauge (C,n) is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
width (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
len (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x is non empty Element of K6( the U1 of (TOP-REAL 2))
Gauge (x,C) is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
len (Gauge (x,C)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
Gauge (x,n) is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
len (Gauge (x,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
2 |^ C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
2 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(2 |^ n) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
(2 |^ C) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
x is non empty Element of K6( the U1 of (TOP-REAL 2))
Gauge (x,n) is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column FinSequence of K358( the U1 of (TOP-REAL 2))
len (Gauge (x,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V16() V99() V165() V166() V167() V168() V169() V170() Element of NAT
Gauge (x,C) is V21() non empty-yielding V24( NAT ) V25(K358( the U1 of (TOP-REAL 2))) Fun