:: JORDAN1H semantic presentation

REAL is non empty non trivial non finite non empty-membered V69() V70() V71() V75() set
NAT is non empty non trivial ordinal non finite cardinal limit_cardinal non empty-membered V69() V70() V71() V72() V73() V74() V75() Element of bool REAL
bool REAL is non empty non trivial non finite non empty-membered set
COMPLEX is non empty non trivial non finite non empty-membered V69() V75() set
omega is non empty non trivial ordinal non finite cardinal limit_cardinal non empty-membered V69() V70() V71() V72() V73() V74() V75() set
bool omega is non empty non trivial non finite non empty-membered set
bool NAT is non empty non trivial non finite non empty-membered set
RAT is non empty non trivial non finite non empty-membered V69() V70() V71() V72() V75() set
INT is non empty non trivial non finite non empty-membered V69() V70() V71() V72() V73() V75() set
is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool is non empty non trivial non finite non empty-membered set
{} is set

1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
{{},1} is finite set
K386() is set
bool K386() is set
K387() is Element of bool K386()

bool [:1,1:] is finite V32() set

bool [:[:1,1:],1:] is finite V32() set
[:[:1,1:],REAL:] is Relation-like V59() V60() V61() set
bool [:[:1,1:],REAL:] is set
is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool is non empty non trivial non finite non empty-membered set
2 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

[:[:2,2:],REAL:] is Relation-like V59() V60() V61() set
bool [:[:2,2:],REAL:] is set
TOP-REAL 2 is non empty non trivial TopSpace-like T_2 V156() V181() V182() V183() V184() V185() V186() V187() strict add-continuous Mult-continuous RLTopStruct
the carrier of () is non empty non trivial functional non empty-membered set
the carrier of () * is non empty functional FinSequence-membered FinSequenceSet of the carrier of ()
[: the carrier of (),REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool [: the carrier of (),REAL:] is non empty non trivial non finite non empty-membered set
bool the carrier of () is set
is non empty non trivial Relation-like non finite non empty-membered V59() set
bool is non empty non trivial non finite non empty-membered set
is non empty non trivial Relation-like non finite non empty-membered V59() set
bool is non empty non trivial non finite non empty-membered set
is non empty non trivial Relation-like RAT -valued non finite non empty-membered V59() V60() V61() set
bool is non empty non trivial non finite non empty-membered set
is non empty non trivial Relation-like RAT -valued non finite non empty-membered V59() V60() V61() set
bool is non empty non trivial non finite non empty-membered set
is non empty non trivial Relation-like RAT -valued INT -valued non finite non empty-membered V59() V60() V61() set
bool is non empty non trivial non finite non empty-membered set
is non empty non trivial Relation-like RAT -valued INT -valued non finite non empty-membered V59() V60() V61() set
bool is non empty non trivial non finite non empty-membered set
is non empty non trivial Relation-like RAT -valued INT -valued non finite non empty-membered V59() V60() V61() V62() set
is non empty non trivial Relation-like RAT -valued INT -valued non finite non empty-membered V59() V60() V61() V62() set
bool is non empty non trivial non finite non empty-membered set
is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool is non empty non trivial non finite non empty-membered set

3 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
4 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
0 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
proj1 is Relation-like the carrier of () -defined REAL -valued Function-like V43( the carrier of (), REAL ) V59() V60() V61() Element of bool [: the carrier of (),REAL:]
proj2 is Relation-like the carrier of () -defined REAL -valued Function-like V43( the carrier of (), REAL ) V59() V60() V61() Element of bool [: the carrier of (),REAL:]
dom {} is set
rng {} is set
C is non empty non empty-membered set

n is non empty set

rng is non empty trivial finite 1 -element set

bool (C *) is set

n is set
dom (rngs C) is set
dom C is set
(rngs C) . n is set

rng (C . n) is set

{ (((1 - b1) * C) + (b1 * n)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
{C,n} is functional finite V32() set
(LSeg (C,n)) \ {C,n} is functional Element of bool the carrier of ()
Cl ((LSeg (C,n)) \ {C,n}) is functional Element of bool the carrier of ()

Pitag_dist 2 is Relation-like [:(REAL 2),(REAL 2):] -defined REAL -valued Function-like V43([:(REAL 2),(REAL 2):], REAL ) V59() V60() V61() Element of bool [:[:(REAL 2),(REAL 2):],REAL:]
[:(REAL 2),(REAL 2):] is Relation-like set
[:[:(REAL 2),(REAL 2):],REAL:] is Relation-like V59() V60() V61() set
bool [:[:(REAL 2),(REAL 2):],REAL:] is set
MetrStruct(# (REAL 2),() #) is strict MetrStruct
the carrier of () is non empty set
i1 is functional Element of bool the carrier of ()
the topology of () is Element of bool (bool the carrier of ())
bool (bool the carrier of ()) is set
TopStruct(# the carrier of (), the topology of () #) is strict TopStruct

the carrier of () is set
bool the carrier of () is set
j2 is Element of bool the carrier of ()
G is Element of the carrier of ()
j2 is V11() real ext-real set
Ball (G,j2) is Element of bool the carrier of ()
bool the carrier of () is set
j4 is V11() real ext-real Element of REAL
j4 / 2 is V11() real ext-real Element of REAL
f is Element of the carrier of ()
dist (G,f) is V11() real ext-real Element of REAL
(dist (G,f)) / 2 is V11() real ext-real Element of REAL
min ((j4 / 2),((dist (G,f)) / 2)) is V11() real ext-real set
(min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)) is V11() real ext-real Element of REAL
1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) is V11() real ext-real Element of REAL
(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of ()
(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of ()
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of ()
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
i0 is Element of the carrier of ()

K268(i1) is Relation-like Function-like V59() set
K38(1) is V11() real integer ext-real non positive set

K239(j,K268(i1)) is Relation-like Function-like set
dist (G,i0) is V11() real ext-real Element of REAL

K239(j0,K268(i)) is Relation-like Function-like set
|.(j0 - i).| is V11() real ext-real non negative Element of REAL
(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
j - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) is Relation-like Function-like V59() set
K38(1) * ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j) is Relation-like Function-like set
K239(j,K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j))) is Relation-like Function-like set
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
(j - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)) is Relation-like Function-like V59() set
K38(1) * (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like Function-like set
K239((j - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1))) is Relation-like Function-like set
|.((j - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)).| is V11() real ext-real non negative Element of REAL

(1 * j) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
K239((1 * j),K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j))) is Relation-like Function-like set
((1 * j) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
K239(((1 * j) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1))) is Relation-like Function-like set
|.(((1 * j) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)).| is V11() real ext-real non negative Element of REAL
- 1 is V11() real integer ext-real non positive Element of REAL
(- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) is V11() real ext-real Element of REAL
((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
(1 * j) + (((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
((1 * j) + (((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
K239(((1 * j) + (((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j)),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1))) is Relation-like Function-like set
|.(((1 * j) + (((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)).| is V11() real ext-real non negative Element of REAL
- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) is V11() real ext-real Element of REAL
1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) is V11() real ext-real Element of REAL
(1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))))) * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
((1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))))) * j) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
K239(((1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))))) * j),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1))) is Relation-like Function-like set
|.(((1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))))) * j) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)).| is V11() real ext-real non negative Element of REAL
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
(- 1) * ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) is V11() real ext-real Element of REAL
((- 1) * ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j) + (((- 1) * ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
|.((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j) + (((- 1) * ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * i1)).| is V11() real ext-real non negative Element of REAL

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * ((- 1) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * ((- 1) * i1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
|.((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * ((- 1) * i1))).| is V11() real ext-real non negative Element of REAL

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j + ((- 1) * i1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
|.(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j + ((- 1) * i1))).| is V11() real ext-real non negative Element of REAL

((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j + (- i1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
|.(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j + (- i1))).| is V11() real ext-real non negative Element of REAL
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j - i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
|.(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j - i1)).| is V11() real ext-real non negative Element of REAL
abs ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) is V11() real ext-real Element of REAL

|.j1.| is V11() real ext-real non negative Element of REAL
(abs ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * |.j1.| is V11() real ext-real Element of REAL
|.(j - i1).| is V11() real ext-real non negative Element of REAL
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * |.(j - i1).| is V11() real ext-real Element of REAL
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (dist (G,f)) is V11() real ext-real Element of REAL
j4 / 1 is V11() real ext-real Element of REAL
Ball (G,j4) is Element of bool the carrier of ()
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of ()
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * C) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of ()
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) is V11() real ext-real Element of REAL
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of ()
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
(dist (G,f)) / 1 is V11() real ext-real Element of REAL
(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of ()
(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of ()
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of ()
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of ()
(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) is Relation-like Function-like V59() set
K38(1) * (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like Function-like set
K239((((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n))) is Relation-like Function-like set
(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of ()
(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C)) is Relation-like Function-like V59() set
K38(1) * ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) is Relation-like Function-like set
K239((((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)),K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C))) is Relation-like Function-like set

{ (((1 - b1) * C) + (b1 * n)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
{C,n} is functional finite V32() set
(LSeg (C,n)) \ {C,n} is functional Element of bool the carrier of ()
Cl ((LSeg (C,n)) \ {C,n}) is functional Element of bool the carrier of ()
Cl (LSeg (C,n)) is functional connected bounded convex Element of bool the carrier of ()
G is set
((LSeg (C,n)) \ {C,n}) \/ {C,n} is set
C is functional Element of bool the carrier of ()
Cl C is functional Element of bool the carrier of ()

{ (((1 - b1) * n) + (b1 * G)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
{n,G} is functional finite V32() set
(LSeg (n,G)) \ {n,G} is functional Element of bool the carrier of ()
Cl ((LSeg (n,G)) \ {n,G}) is functional Element of bool the carrier of ()
{ [b1,b2] where b1, b2 is V11() real ext-real Element of REAL : b1 <= b2 } is set
n is set
G is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
[G,f] is set
{G,f} is finite V69() V70() V71() set
{G} is non empty trivial finite 1 -element V69() V70() V71() set
{{G,f},{G}} is finite V32() set

C is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
[C,n] is set
{C,n} is finite V69() V70() V71() set
{C} is non empty trivial finite 1 -element V69() V70() V71() set
{{C,n},{C}} is finite V32() set
G is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
[G,f] is set
{G,f} is finite V69() V70() V71() set
{G} is non empty trivial finite 1 -element V69() V70() V71() set
{{G,f},{G}} is finite V32() set
C is set
[C,C] is set
{C,C} is finite set
{C} is non empty trivial finite 1 -element set
{{C,C},{C}} is finite V32() set
n is V11() real ext-real Element of REAL
C is set
n is set
[C,n] is set
{C,n} is finite set
{C} is non empty trivial finite 1 -element set
{{C,n},{C}} is finite V32() set
[n,C] is set
{n,C} is finite set
{n} is non empty trivial finite 1 -element set
{{n,C},{n}} is finite V32() set
G is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
C is set
n is set
G is set
[C,n] is set
{C,n} is finite set
{C} is non empty trivial finite 1 -element set
{{C,n},{C}} is finite V32() set
[n,G] is set
{n,G} is finite set
{n} is non empty trivial finite 1 -element set
{{n,G},{n}} is finite V32() set
[C,G] is set
{C,G} is finite set
{{C,G},{C}} is finite V32() set
f is V11() real ext-real Element of REAL
i1 is V11() real ext-real Element of REAL
j2 is V11() real ext-real Element of REAL
C is set
n is set
[C,n] is set
{C,n} is finite set
{C} is non empty trivial finite 1 -element set
{{C,n},{C}} is finite V32() set
[n,C] is set
{n,C} is finite set
{n} is non empty trivial finite 1 -element set
{{n,C},{n}} is finite V32() set
G is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
field () is set
dom () is set
rng () is V69() V70() V71() set
(dom ()) \/ (rng ()) is set
REAL \/ REAL is V69() V70() V71() set
dom () is V69() V70() V71() Element of bool REAL
C is set
n is V11() real ext-real Element of REAL
[n,n] is set
{n,n} is finite V69() V70() V71() set
{n} is non empty trivial finite 1 -element V69() V70() V71() set
{{n,n},{n}} is finite V32() set
C is finite V69() V70() V71() Element of bool REAL

G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom (SgmX ((),C)) is finite set
f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(SgmX ((),C)) . f is V11() real ext-real Element of REAL
(SgmX ((),C)) . G is V11() real ext-real Element of REAL
dom (SgmX ((),C)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
(SgmX ((),C)) /. G is V11() real ext-real Element of REAL
(SgmX ((),C)) /. f is V11() real ext-real Element of REAL
[((SgmX ((),C)) . G),((SgmX ((),C)) . f)] is set
{((SgmX ((),C)) . G),((SgmX ((),C)) . f)} is finite V69() V70() V71() set
{((SgmX ((),C)) . G)} is non empty trivial finite 1 -element V69() V70() V71() set
{{((SgmX ((),C)) . G),((SgmX ((),C)) . f)},{((SgmX ((),C)) . G)}} is finite V32() set

rng C is finite V69() V70() V71() Element of bool REAL

n is finite V69() V70() V71() Element of bool REAL

rng (SgmX ((),n)) is finite V69() V70() V71() Element of bool REAL

len G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
card (rng C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
C is finite V69() V70() V71() Element of bool REAL

C is non empty set
bool C is set
[:C,C:] is Relation-like set
bool [:C,C:] is set
n is finite Element of bool C
card n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

len (SgmX (G,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
field G is set
dom G is set
rng G is set
(dom G) \/ (rng G) is set

is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool is non empty non trivial non finite non empty-membered set
len () is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom () is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
dom C is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

() . G is V11() real ext-real Element of REAL
n . G is V11() real ext-real Element of REAL

(C /. G) `1 is V11() real ext-real Element of REAL
(C /. G) . 1 is V11() real ext-real Element of REAL
proj1 . (C . G) is V11() real ext-real Element of REAL
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool is non empty non trivial non finite non empty-membered set
len () is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom () is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
dom C is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

() . G is V11() real ext-real Element of REAL
n . G is V11() real ext-real Element of REAL

(C /. G) `2 is V11() real ext-real Element of REAL
(C /. G) . 2 is V11() real ext-real Element of REAL
proj2 . (C . G) is V11() real ext-real Element of REAL
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
C is non empty set

bool C is set

bool (C *) is set
{ } is set
f is set

rng i1 is finite Element of bool C
union { } is set
C is non empty with_non-empty_elements non empty-membered set

(C,n) is finite Element of bool C
bool C is set

dom (rngs n) is set
dom n is non empty finite V69() V70() V71() V72() V73() V74() Element of bool NAT

Union (rngs n) is set
G is non empty with_non-empty_elements non empty-membered set
union G is non empty set
C is non empty set

width n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Seg () is finite width n -element V69() V70() V71() V72() V73() V74() Element of bool NAT
(C,n) is finite Element of bool C
bool C is set
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

rng (Col (n,G)) is finite Element of bool C
f is set
dom (Col (n,G)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
i1 is set
(Col (n,G)) . i1 is set
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (Col (n,G)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j2,G] is set
{j2,G} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,G},{j2}} is finite V32() set
Indices n is set
{ (n * (b1,b2)) where b1, b2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT : [b1,b2] in Indices n } is set
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
(Col (n,G)) . j2 is set
n * (j2,G) is Element of C
C is non empty set

dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
(C,n) is finite Element of bool C
bool C is set
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

width n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

rng (Line (n,G)) is finite Element of bool C
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f is set
dom (Line (n,G)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
i1 is set
(Line (n,G)) . i1 is set
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (Line (n,G)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[G,j2] is set
{G,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{G} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{G,j2},{G}} is finite V32() set
Indices n is set
{ (n * (b1,b2)) where b1, b2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT : [b1,b2] in Indices n } is set
Seg () is finite width n -element V69() V70() V71() V72() V73() V74() Element of bool NAT
(Line (n,G)) . j2 is set
n * (G,j2) is Element of C

len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
( the carrier of (),C) is functional finite closed bounded compact Element of bool the carrier of ()
proj1 .: ( the carrier of (),C) is finite V69() V70() V71() Element of bool REAL
card (proj1 .: ( the carrier of (),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Seg () is finite width C -element V69() V70() V71() V72() V73() V74() Element of bool NAT

(len C) -tuples_on the carrier of () is functional FinSequence-membered FinSequenceSet of the carrier of ()

rng n is finite V69() V70() V71() Element of bool REAL
card (rng n) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (Col (C,1)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool is non empty non trivial non finite non empty-membered set
rng (proj1 * (Col (C,1))) is finite V69() V70() V71() Element of bool REAL
rng (Col (C,1)) is functional finite closed bounded compact Element of bool the carrier of ()
proj1 .: (rng (Col (C,1))) is finite V69() V70() V71() Element of bool REAL

( the carrier of (),C) is functional finite closed bounded compact Element of bool the carrier of ()
proj1 .: ( the carrier of (),C) is finite V69() V70() V71() Element of bool REAL
card (proj1 .: ( the carrier of (),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
dom C is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
rng n is finite set
G is set
Indices C is set
{ (C * (b1,b2)) where b1, b2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT : [b1,b2] in Indices C } is set
f is set

i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

j2 `1 is V11() real ext-real Element of REAL
j2 . 1 is V11() real ext-real Element of REAL

(C * (i1,1)) `1 is V11() real ext-real Element of REAL
(C * (i1,1)) . 1 is V11() real ext-real Element of REAL
proj1 . (C * (i1,1)) is V11() real ext-real Element of REAL
n . i1 is set
card (dom C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
( the carrier of (),C) is functional finite closed bounded compact Element of bool the carrier of ()
proj1 .: ( the carrier of (),C) is finite V69() V70() V71() Element of bool REAL
card (proj1 .: ( the carrier of (),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
( the carrier of (),C) is functional finite closed bounded compact Element of bool the carrier of ()
proj2 .: ( the carrier of (),C) is finite V69() V70() V71() Element of bool REAL
card (proj2 .: ( the carrier of (),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom C is finite V69() V70() V71() V72() V73() V74() Element of bool NAT

() -tuples_on the carrier of () is functional FinSequence-membered FinSequenceSet of the carrier of ()

rng n is finite V69() V70() V71() Element of bool REAL
card (rng n) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (Line (C,1)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool is non empty non trivial non finite non empty-membered set
rng (proj2 * (Line (C,1))) is finite V69() V70() V71() Element of bool REAL
rng (Line (C,1)) is functional finite closed bounded compact Element of bool the carrier of ()
proj2 .: (rng (Line (C,1))) is finite V69() V70() V71() Element of bool REAL

( the carrier of (),C) is functional finite closed bounded compact Element of bool the carrier of ()
proj2 .: ( the carrier of (),C) is finite V69() V70() V71() Element of bool REAL
card (proj2 .: ( the carrier of (),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Seg () is finite width C -element V69() V70() V71() V72() V73() V74() Element of bool NAT
rng n is finite set
G is set
Indices C is set
{ (C * (b1,b2)) where b1, b2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT : [b1,b2] in Indices C } is set
f is set

i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT

j2 `2 is V11() real ext-real Element of REAL
j2 . 2 is V11() real ext-real Element of REAL

(C * (1,j2)) `2 is V11() real ext-real Element of REAL
(C * (1,j2)) . 2 is V11() real ext-real Element of REAL
proj2 . (C * (1,j2)) is V11() real ext-real Element of REAL
n . j2 is set
card (Seg ()) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
( the carrier of (),C) is functional finite closed bounded compact Element of bool the carrier of ()
proj2 .: ( the carrier of (),C) is finite V69() V70() V71() Element of bool REAL
card (proj2 .: ( the carrier of (),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega

len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
LSeg (n,G) is functional Element of bool the carrier of ()
left_cell (n,G,C) is functional Element of bool the carrier of ()
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Indices C is set

f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[f,i1] is set
{f,i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{f} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{f,i1},{f}