REAL is non empty V36() V148() V149() V150() V154() V222() V223() V225() set
NAT is V148() V149() V150() V151() V152() V153() V154() V222() Element of K6(REAL)
K6(REAL) is set
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected SubSpace of R^1
R^1 is non empty strict TopSpace-like V210() TopStruct
the carrier of I[01] is non empty V148() V149() V150() set
omega is V148() V149() V150() V151() V152() V153() V154() V222() set
K6(omega) is set
1 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT
K7(1,1) is V22() V26( RAT ) V26( INT ) V138() V139() V140() V141() set
RAT is non empty V36() V148() V149() V150() V151() V154() set
INT is non empty V36() V148() V149() V150() V151() V152() V154() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V22() V26( RAT ) V26( INT ) V138() V139() V140() V141() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V22() V138() V139() V140() set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is V22() V138() V139() V140() set
K7(K7(REAL,REAL),REAL) is V22() V138() V139() V140() set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT
K7(2,2) is V22() V26( RAT ) V26( INT ) V138() V139() V140() V141() set
K7(K7(2,2),REAL) is V22() V138() V139() V140() set
K6(K7(K7(2,2),REAL)) is set
K6(NAT) is set
COMPLEX is non empty V36() V148() V154() set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected RLTopStruct
the carrier of (TOP-REAL 2) is non empty functional set
K6( the carrier of (TOP-REAL 2)) is set
K297( the carrier of (TOP-REAL 2)) is non empty functional FinSequence-membered M12( the carrier of (TOP-REAL 2))
K7( the carrier of (TOP-REAL 2),REAL) is V22() V138() V139() V140() set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is set
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected TopStruct
the carrier of I[01] is non empty V148() V149() V150() set
RealSpace is strict V210() MetrStruct
the carrier of R^1 is non empty V148() V149() V150() set
K440(I[01],I[01]) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of K440(I[01],I[01]) is non empty set
K440(R^1,R^1) is non empty strict TopSpace-like TopStruct
the carrier of K440(R^1,R^1) is non empty set
K7( the carrier of K440(R^1,R^1), the carrier of (TOP-REAL 2)) is V22() set
K6(K7( the carrier of K440(R^1,R^1), the carrier of (TOP-REAL 2))) is set
{} is empty V22() non-empty empty-yielding V25( NAT ) V26( RAT ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered V138() V139() V140() V141() V148() V149() V150() V151() V152() V153() V154() V222() V223() V224() V225() set
the empty V22() non-empty empty-yielding V25( NAT ) V26( RAT ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered V138() V139() V140() V141() V148() V149() V150() V151() V152() V153() V154() V222() V223() V224() V225() set is empty V22() non-empty empty-yielding V25( NAT ) V26( RAT ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered V138() V139() V140() V141() V148() V149() V150() V151() V152() V153() V154() V222() V223() V224() V225() set
{{},1} is non empty set
3 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT
Seg 1 is non empty V36() V43(1) V148() V149() V150() V151() V152() V153() V220() V221() V222() V223() V224() Element of K6(NAT)
0 is empty natural V11() real ext-real non positive non negative V22() non-empty empty-yielding V25( NAT ) V26( RAT ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered integer V101() V138() V139() V140() V141() V148() V149() V150() V151() V152() V153() V154() V222() V223() V224() V225() Element of NAT
Closed-Interval-MSpace (0,1) is non empty strict Reflexive discerning symmetric triangle SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (0,1)) is non empty set
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V210() SubSpace of R^1
[.0,1.] is compact V148() V149() V150() V225() Element of K6(REAL)
0[01] is V11() real ext-real Element of the carrier of I[01]
1[01] is V11() real ext-real Element of the carrier of I[01]
TopSpaceMetr (Closed-Interval-MSpace (0,1)) is TopStruct
a is set
<*a*> is non empty V22() V25( NAT ) Function-like V36() V43(1) FinSequence-like FinSubsequence-like set
b is V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
len b is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
b ^ <*a*> is non empty V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
(b ^ <*a*>) . 1 is set
b . 1 is set
<*a*> ^ b is non empty V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
(len b) + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
(<*a*> ^ b) . ((len b) + 1) is set
b . (len b) is set
dom b is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
len <*a*> is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
(len <*a*>) + (len b) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
(<*a*> ^ b) . ((len <*a*>) + (len b)) is set
a is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL
len a is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
b is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
a /. b is V11() real ext-real Element of REAL
dom a is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
c is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
d is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
1 + d is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
b + (1 + d) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
a /. (b + (1 + d)) is V11() real ext-real Element of REAL
d + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
1 + (d + 1) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
b + (1 + (d + 1)) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
a /. (b + (1 + (d + 1))) is V11() real ext-real Element of REAL
b + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
(b + 1) + d is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
(b + (1 + d)) + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
b + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
c -' (b + 1) is natural V11() real ext-real non negative integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
c - (b + 1) is V11() real ext-real integer Element of REAL
1 + (c -' (b + 1)) is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT
b + (1 + (c -' (b + 1))) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
a . b is V11() real ext-real Element of REAL
1 + 0 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT
b + (1 + 0) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
a /. (b + (1 + 0)) is V11() real ext-real Element of REAL
a /. c is V11() real ext-real Element of REAL
a . c is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
c is V11() real ext-real set
d is V11() real ext-real set
closed_inside_of_rectangle (a,b,c,d) is functional Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2) : ( a <= b1 `1 & b1 `1 <= b & c <= b1 `2 & b1 `2 <= d ) } is set
br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
LSeg (br,cr) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * br) + (b1 * cr)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
dr is set
h is V11() real ext-real Element of REAL
1 - h is V11() real ext-real Element of REAL
(1 - h) * br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
h * cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
((1 - h) * br) + (h * cr) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
((1 - h) * br) `1 is V11() real ext-real Element of REAL
((1 - h) * br) . 1 is V11() real ext-real Element of REAL
(h * cr) `1 is V11() real ext-real Element of REAL
(h * cr) . 1 is V11() real ext-real Element of REAL
(((1 - h) * br) `1) + ((h * cr) `1) is V11() real ext-real Element of REAL
((1 - h) * br) `2 is V11() real ext-real Element of REAL
((1 - h) * br) . 2 is V11() real ext-real Element of REAL
(h * cr) `2 is V11() real ext-real Element of REAL
(h * cr) . 2 is V11() real ext-real Element of REAL
(((1 - h) * br) `2) + ((h * cr) `2) is V11() real ext-real Element of REAL
|[((((1 - h) * br) `1) + ((h * cr) `1)),((((1 - h) * br) `2) + ((h * cr) `2))]| is non empty V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
cr `1 is V11() real ext-real Element of REAL
cr . 1 is V11() real ext-real Element of REAL
h * (cr `1) is V11() real ext-real Element of REAL
cr `2 is V11() real ext-real Element of REAL
cr . 2 is V11() real ext-real Element of REAL
h * (cr `2) is V11() real ext-real Element of REAL
|[(h * (cr `1)),(h * (cr `2))]| is non empty V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
br `1 is V11() real ext-real Element of REAL
br . 1 is V11() real ext-real Element of REAL
(1 - h) * (br `1) is V11() real ext-real Element of REAL
br `2 is V11() real ext-real Element of REAL
br . 2 is V11() real ext-real Element of REAL
(1 - h) * (br `2) is V11() real ext-real Element of REAL
|[((1 - h) * (br `1)),((1 - h) * (br `2))]| is non empty V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(((1 - h) * br) + (h * cr)) `2 is V11() real ext-real Element of REAL
(((1 - h) * br) + (h * cr)) . 2 is V11() real ext-real Element of REAL
((1 - h) * (br `2)) + (h * (cr `2)) is V11() real ext-real Element of REAL
Ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
Ar `1 is V11() real ext-real Element of REAL
Ar . 1 is V11() real ext-real Element of REAL
Ar `2 is V11() real ext-real Element of REAL
Ar . 2 is V11() real ext-real Element of REAL
Br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
Br `1 is V11() real ext-real Element of REAL
Br . 1 is V11() real ext-real Element of REAL
Br `2 is V11() real ext-real Element of REAL
Br . 2 is V11() real ext-real Element of REAL
(((1 - h) * br) + (h * cr)) `1 is V11() real ext-real Element of REAL
(((1 - h) * br) + (h * cr)) . 1 is V11() real ext-real Element of REAL
((1 - h) * (br `1)) + (h * (cr `1)) is V11() real ext-real Element of REAL
Ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
Ar `1 is V11() real ext-real Element of REAL
Ar . 1 is V11() real ext-real Element of REAL
Ar `2 is V11() real ext-real Element of REAL
Ar . 2 is V11() real ext-real Element of REAL
Br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
Br `1 is V11() real ext-real Element of REAL
Br . 1 is V11() real ext-real Element of REAL
Br `2 is V11() real ext-real Element of REAL
Br . 2 is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
c is V11() real ext-real set
d is V11() real ext-real set
Trectangle (a,b,c,d) is TopSpace-like SubSpace of TOP-REAL 2
closed_inside_of_rectangle (a,b,c,d) is functional convex Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d)) is strict TopSpace-like SubSpace of TOP-REAL 2
[#] (Trectangle (a,b,c,d)) is non proper closed Element of K6( the carrier of (Trectangle (a,b,c,d)))
the carrier of (Trectangle (a,b,c,d)) is set
K6( the carrier of (Trectangle (a,b,c,d))) is set
5 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT
K6( the carrier of I[01]) is set
a is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
TOP-REAL a is non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected RLTopStruct
the carrier of (TOP-REAL a) is non empty functional set
K7( the carrier of I[01], the carrier of (TOP-REAL a)) is V22() set
K6(K7( the carrier of I[01], the carrier of (TOP-REAL a))) is set
Euclid a is non empty strict Reflexive discerning symmetric triangle MetrStruct
REAL a is non empty functional FinSequence-membered M12( REAL )
K298(a,REAL) is functional FinSequence-membered M12( REAL )
Pitag_dist a is V22() V25(K7((REAL a),(REAL a))) V26( REAL ) Function-like total V33(K7((REAL a),(REAL a)), REAL ) V138() V139() V140() Element of K6(K7(K7((REAL a),(REAL a)),REAL))
K7((REAL a),(REAL a)) is V22() set
K7(K7((REAL a),(REAL a)),REAL) is V22() V138() V139() V140() set
K6(K7(K7((REAL a),(REAL a)),REAL)) is set
MetrStruct(# (REAL a),(Pitag_dist a) #) is strict MetrStruct
the carrier of (Euclid a) is non empty set
K6( the carrier of (Euclid a)) is set
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
{1} is non empty V148() V149() V150() V151() V152() V153() V220() V222() set
b is set
[.0,1.] \/ {1} is non empty V148() V149() V150() set
b is non empty V11() real ext-real positive non negative set
c is non empty V22() V25( the carrier of I[01]) V26( the carrier of (TOP-REAL a)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL a)) continuous Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL a)))
K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid a)) is V22() set
K6(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid a))) is set
d is non empty V11() real ext-real positive non negative Element of REAL
d / 2 is V11() real ext-real non negative Element of REAL
ar is non empty V22() V25( the carrier of (Closed-Interval-MSpace (0,1))) V26( the carrier of (Euclid a)) Function-like total V33( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid a)) Element of K6(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid a)))
br is V11() real ext-real Element of REAL
1 / 2 is V11() real ext-real non negative Element of REAL
min (br,(1 / 2)) is V11() real ext-real set
(min (br,(1 / 2))) / 2 is V11() real ext-real Element of REAL
2 / (min (br,(1 / 2))) is V11() real ext-real Element of REAL
[/(2 / (min (br,(1 / 2))))\] is V11() real ext-real integer set
dr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
h is Element of the carrier of (Closed-Interval-MSpace (0,1))
v is Element of the carrier of (Closed-Interval-MSpace (0,1))
dist (h,v) is V11() real ext-real Element of REAL
ar /. h is Element of the carrier of (Euclid a)
ar . h is Element of the carrier of (Euclid a)
ar /. v is Element of the carrier of (Euclid a)
ar . v is Element of the carrier of (Euclid a)
dist ((ar /. h),(ar /. v)) is V11() real ext-real Element of REAL
(2 / (min (br,(1 / 2)))) - dr is V11() real ext-real Element of REAL
1 + ((2 / (min (br,(1 / 2)))) - dr) is V11() real ext-real Element of REAL
1 + 0 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT
((min (br,(1 / 2))) / 2) * (1 + ((2 / (min (br,(1 / 2)))) - dr)) is V11() real ext-real Element of REAL
((min (br,(1 / 2))) / 2) * 1 is V11() real ext-real Element of REAL
Seg dr is V36() V43(dr) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
h is natural V11() real ext-real integer set
h - 1 is V11() real ext-real integer Element of REAL
((min (br,(1 / 2))) / 2) * (h - 1) is V11() real ext-real Element of REAL
h is V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
dom h is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
len h is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
Seg (len h) is V36() V43( len h) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
<*1*> is non empty V22() V25( NAT ) V26( REAL ) Function-like V36() V43(1) FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL
h ^ <*1*> is non empty V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
rng (h ^ <*1*>) is non empty set
v is set
len (h ^ <*1*>) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
(len h) + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
dom (h ^ <*1*>) is non empty V148() V149() V150() V151() V152() V153() V220() V222() Element of K6(NAT)
Ar is set
(h ^ <*1*>) . Ar is set
Seg (len (h ^ <*1*>)) is V36() V43( len (h ^ <*1*>)) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
Br is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
h . Br is set
Br - 1 is V11() real ext-real integer Element of REAL
((min (br,(1 / 2))) / 2) * (Br - 1) is V11() real ext-real Element of REAL
v is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL
len v is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
(len h) + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
2 / (1 / 2) is V11() real ext-real non negative Element of REAL
4 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT
4 + 1 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT
Ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
h . Ar is set
Ar + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
h . (Ar + 1) is set
Br is V11() real ext-real Element of REAL
Cr is V11() real ext-real Element of REAL
Cr - Br is V11() real ext-real Element of REAL
(Ar + 1) - 1 is V11() real ext-real integer Element of REAL
((min (br,(1 / 2))) / 2) * ((Ar + 1) - 1) is V11() real ext-real Element of REAL
Ar - 1 is V11() real ext-real integer Element of REAL
((min (br,(1 / 2))) / 2) * (Ar - 1) is V11() real ext-real Element of REAL
((min (br,(1 / 2))) / 2) * Ar is V11() real ext-real Element of REAL
(((min (br,(1 / 2))) / 2) * Ar) - (((min (br,(1 / 2))) / 2) * (Ar - 1)) is V11() real ext-real Element of REAL
0 + 1 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT
h . 1 is set
1 - 1 is V11() real ext-real integer Element of REAL
((min (br,(1 / 2))) / 2) * (1 - 1) is V11() real ext-real Element of REAL
v . 1 is V11() real ext-real Element of REAL
2 * (min (br,(1 / 2))) is V11() real ext-real Element of REAL
((min (br,(1 / 2))) / 2) * (2 / (min (br,(1 / 2)))) is V11() real ext-real Element of REAL
(2 * (min (br,(1 / 2)))) / (2 * (min (br,(1 / 2)))) is V11() real ext-real Element of REAL
dr - 1 is V11() real ext-real integer Element of REAL
((min (br,(1 / 2))) / 2) * (dr - 1) is V11() real ext-real Element of REAL
1 - (((min (br,(1 / 2))) / 2) * (dr - 1)) is V11() real ext-real Element of REAL
(2 / (min (br,(1 / 2)))) - [/(2 / (min (br,(1 / 2))))\] is V11() real ext-real Element of REAL
1 + ((2 / (min (br,(1 / 2)))) - [/(2 / (min (br,(1 / 2))))\]) is V11() real ext-real Element of REAL
((min (br,(1 / 2))) / 2) * (1 + ((2 / (min (br,(1 / 2)))) - [/(2 / (min (br,(1 / 2))))\])) is V11() real ext-real Element of REAL
h . (len h) is set
Ar is V11() real ext-real Element of REAL
1 - Ar is V11() real ext-real Element of REAL
Ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
Ar + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
v /. (Ar + 1) is V11() real ext-real Element of REAL
v /. Ar is V11() real ext-real Element of REAL
(v /. (Ar + 1)) - (v /. Ar) is V11() real ext-real Element of REAL
v . (Ar + 1) is V11() real ext-real Element of REAL
h . (Ar + 1) is set
v . Ar is V11() real ext-real Element of REAL
h . Ar is set
v . Ar is V11() real ext-real Element of REAL
h . Ar is set
v . (Ar + 1) is V11() real ext-real Element of REAL
(2 / (min (br,(1 / 2)))) + 1 is V11() real ext-real Element of REAL
((2 / (min (br,(1 / 2)))) + 1) - 1 is V11() real ext-real Element of REAL
[/(2 / (min (br,(1 / 2))))\] - 1 is V11() real ext-real integer Element of REAL
Ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
h . Ar is set
Br is V11() real ext-real Element of REAL
Ar - 1 is V11() real ext-real integer Element of REAL
((min (br,(1 / 2))) / 2) * (Ar - 1) is V11() real ext-real Element of REAL
Ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
Ar + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
v /. (Ar + 1) is V11() real ext-real Element of REAL
v /. Ar is V11() real ext-real Element of REAL
v . (Ar + 1) is V11() real ext-real Element of REAL
h . (Ar + 1) is set
v . Ar is V11() real ext-real Element of REAL
h . Ar is set
v . (Ar + 1) is V11() real ext-real Element of REAL
v . Ar is V11() real ext-real Element of REAL
h . Ar is set
dom c is non empty V148() V149() V150() Element of K6( the carrier of I[01])
Ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
v /. Ar is V11() real ext-real Element of REAL
Ar + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
v /. (Ar + 1) is V11() real ext-real Element of REAL
[.(v /. Ar),(v /. (Ar + 1)).] is compact V148() V149() V150() V225() Element of K6(REAL)
Br is V148() V149() V150() Element of K6( the carrier of I[01])
c .: Br is functional Element of K6( the carrier of (TOP-REAL a))
K6( the carrier of (TOP-REAL a)) is set
Cr is Element of K6( the carrier of (Euclid a))
diameter Cr is V11() real ext-real Element of REAL
Dr is Element of the carrier of (Euclid a)
TR is Element of the carrier of (Euclid a)
dist (Dr,TR) is V11() real ext-real Element of REAL
TR is set
c . TR is V22() Function-like set
ar is Element of the carrier of (Closed-Interval-MSpace (0,1))
(v /. (Ar + 1)) - (v /. Ar) is V11() real ext-real Element of REAL
cr is set
c . cr is V22() Function-like set
dr is Element of the carrier of (Closed-Interval-MSpace (0,1))
ar . ar is Element of the carrier of (Euclid a)
ar /. ar is Element of the carrier of (Euclid a)
ar . dr is Element of the carrier of (Euclid a)
ar /. dr is Element of the carrier of (Euclid a)
br is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
br - h is V11() real ext-real Element of REAL
abs (br - h) is V11() real ext-real Element of REAL
dist (ar,dr) is V11() real ext-real Element of REAL
rng h is set
Ar is set
Br is set
h . Br is set
Cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
h . Cr is set
Cr - 1 is V11() real ext-real integer Element of REAL
((min (br,(1 / 2))) / 2) * (Cr - 1) is V11() real ext-real Element of REAL
Dr is V11() real ext-real Element of REAL
rng <*1*> is non empty V148() V149() V150() Element of K6(REAL)
rng v is V148() V149() V150() Element of K6(REAL)
(rng h) \/ {1} is non empty set
v . (len v) is V11() real ext-real Element of REAL
a is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
TOP-REAL a is non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected RLTopStruct
the carrier of (TOP-REAL a) is non empty functional set
K6( the carrier of (TOP-REAL a)) is set
b is V22() V25( NAT ) Function-like V36() V43(a) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL a)
c is V22() V25( NAT ) Function-like V36() V43(a) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL a)
LSeg (b,c) is functional closed compact Element of K6( the carrier of (TOP-REAL a))
{ (((1 - b1) * b) + (b1 * c)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
d is functional Element of K6( the carrier of (TOP-REAL a))
ar is non empty functional Element of K6( the carrier of (TOP-REAL a))
(TOP-REAL a) | ar is non empty strict TopSpace-like SubSpace of TOP-REAL a
the carrier of ((TOP-REAL a) | ar) is non empty set
[#] ((TOP-REAL a) | ar) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL a) | ar))
K6( the carrier of ((TOP-REAL a) | ar)) is set
cr is set
dr is V22() V25( NAT ) Function-like V36() V43(a) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL a)
LSeg (dr,c) is functional closed compact Element of K6( the carrier of (TOP-REAL a))
{ (((1 - b1) * dr) + (b1 * c)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
{dr} is non empty functional set
(LSeg (dr,c)) \ {dr} is functional Element of K6( the carrier of (TOP-REAL a))
LSeg (b,dr) is functional closed compact Element of K6( the carrier of (TOP-REAL a))
{ (((1 - b1) * b) + (b1 * dr)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(LSeg (b,dr)) \ {dr} is functional Element of K6( the carrier of (TOP-REAL a))
h is Element of K6( the carrier of ((TOP-REAL a) | ar))
Br is Element of K6( the carrier of ((TOP-REAL a) | ar))
h /\ Br is Element of K6( the carrier of ((TOP-REAL a) | ar))
v is Element of K6( the carrier of ((TOP-REAL a) | ar))
Cr is set
Cr is set
Cl Br is Element of K6( the carrier of ((TOP-REAL a) | ar))
Ar is Element of K6( the carrier of ((TOP-REAL a) | ar))
Cl Ar is Element of K6( the carrier of ((TOP-REAL a) | ar))
v /\ Br is Element of K6( the carrier of ((TOP-REAL a) | ar))
(h /\ Br) \ {dr} is Element of K6( the carrier of ((TOP-REAL a) | ar))
v /\ (Cl Ar) is Element of K6( the carrier of ((TOP-REAL a) | ar))
Cl h is Element of K6( the carrier of ((TOP-REAL a) | ar))
(LSeg (b,dr)) \/ (LSeg (dr,c)) is functional Element of K6( the carrier of (TOP-REAL a))
((LSeg (b,dr)) \ {dr}) \/ {dr} is non empty set
(((LSeg (b,dr)) \ {dr}) \/ {dr}) \/ (LSeg (dr,c)) is non empty set
{dr} \/ (LSeg (dr,c)) is non empty set
((LSeg (b,dr)) \ {dr}) \/ ({dr} \/ (LSeg (dr,c))) is non empty set
v \/ Br is Element of K6( the carrier of ((TOP-REAL a) | ar))
Br \ {dr} is Element of K6( the carrier of ((TOP-REAL a) | ar))
(Br \ {dr}) \/ {dr} is non empty set
v \/ ((Br \ {dr}) \/ {dr}) is non empty set
v \/ {dr} is non empty set
(v \/ {dr}) \/ Ar is non empty set
v \/ Ar is Element of K6( the carrier of ((TOP-REAL a) | ar))
Cr is set
Cl v is Element of K6( the carrier of ((TOP-REAL a) | ar))
h /\ Ar is Element of K6( the carrier of ((TOP-REAL a) | ar))
(Cl v) /\ Ar is Element of K6( the carrier of ((TOP-REAL a) | ar))
br is Element of K6( the carrier of ((TOP-REAL a) | ar))
a is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
TOP-REAL a is non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected RLTopStruct
the carrier of (TOP-REAL a) is non empty functional set
b is V22() V25( NAT ) Function-like V36() V43(a) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL a)
c is V22() V25( NAT ) Function-like V36() V43(a) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL a)
LSeg (b,c) is functional closed compact Element of K6( the carrier of (TOP-REAL a))
K6( the carrier of (TOP-REAL a)) is set
{ (((1 - b1) * b) + (b1 * c)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
d is non empty V22() V25( the carrier of I[01]) V26( the carrier of (TOP-REAL a)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL a)) continuous Path of b,c
rng d is non empty functional Element of K6( the carrier of (TOP-REAL a))
d . 1 is V22() Function-like set
d . 0 is V22() Function-like set
[#] I[01] is non empty non proper closed V148() V149() V150() Element of K6( the carrier of I[01])
d .: ([#] I[01]) is functional Element of K6( the carrier of (TOP-REAL a))
ar is set
dom d is non empty V148() V149() V150() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
br is set
d . br is V22() Function-like set
dom d is non empty V148() V149() V150() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
the topology of (TOP-REAL 2) is non empty Element of K6(K6( the carrier of (TOP-REAL 2)))
K6(K6( the carrier of (TOP-REAL 2))) is set
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is non empty strict TopSpace-like TopStruct
Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
REAL 2 is non empty functional FinSequence-membered M12( REAL )
K298(2,REAL) is functional FinSequence-membered M12( REAL )
Pitag_dist 2 is V22() V25(K7((REAL 2),(REAL 2))) V26( REAL ) Function-like total V33(K7((REAL 2),(REAL 2)), REAL ) V138() V139() V140() Element of K6(K7(K7((REAL 2),(REAL 2)),REAL))
K7((REAL 2),(REAL 2)) is V22() set
K7(K7((REAL 2),(REAL 2)),REAL) is V22() V138() V139() V140() set
K6(K7(K7((REAL 2),(REAL 2)),REAL)) is set
MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct
TopSpaceMetr (Euclid 2) is TopStruct
[#] I[01] is non empty non proper closed V148() V149() V150() Element of K6( the carrier of I[01])
a is non empty functional Element of K6( the carrier of (TOP-REAL 2))
b is non empty functional Element of K6( the carrier of (TOP-REAL 2))
c is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
d is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
c `1 is V11() real ext-real Element of REAL
c . 1 is V11() real ext-real Element of REAL
d `1 is V11() real ext-real Element of REAL
d . 1 is V11() real ext-real Element of REAL
ar `2 is V11() real ext-real Element of REAL
ar . 2 is V11() real ext-real Element of REAL
br `2 is V11() real ext-real Element of REAL
br . 2 is V11() real ext-real Element of REAL
cr is non empty V22() V25( the carrier of I[01]) V26( the carrier of (TOP-REAL 2)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL 2)) continuous Path of c,d
rng cr is non empty functional Element of K6( the carrier of (TOP-REAL 2))
dr is non empty V22() V25( the carrier of I[01]) V26( the carrier of (TOP-REAL 2)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL 2)) continuous Path of ar,br
rng dr is non empty functional Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TopSpaceMetr (Euclid 2)) is set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is set
h is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
v is Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
min_dist_min (h,v) is V11() real ext-real Element of REAL
(min_dist_min (h,v)) / 5 is V11() real ext-real Element of REAL
cr .: the carrier of I[01] is functional Element of K6( the carrier of (TOP-REAL 2))
dr .: ([#] I[01]) is functional Element of K6( the carrier of (TOP-REAL 2))
a /\ b is functional Element of K6( the carrier of (TOP-REAL 2))
0 / 5 is empty V11() real ext-real non positive non negative V22() non-empty empty-yielding V25( NAT ) V26( RAT ) Function-like one-to-one constant functional V36() FinSequence-like FinSubsequence-like FinSequence-membered V138() V139() V140() V141() V148() V149() V150() V151() V152() V153() V154() V222() V223() V224() V225() Element of REAL
the carrier of (Euclid 2) is non empty set
K6( the carrier of (Euclid 2)) is set
Br is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL
Br . 1 is V11() real ext-real Element of REAL
len Br is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
Br . (len Br) is V11() real ext-real Element of REAL
rng Br is V148() V149() V150() Element of K6(REAL)
Cr is V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
len Cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
dom Cr is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
Cr is V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
len Cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
dom Cr is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
rng Cr is set
Dr is set
dom cr is non empty V148() V149() V150() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
TR is set
Cr . TR is set
Seg (len Cr) is V36() V43( len Cr) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
dom Br is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
Br . TR is V11() real ext-real Element of REAL
Cr . TR is set
cr . (Br . TR) is V22() Function-like set
Dr is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len Dr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
Dr . 1 is V22() Function-like set
Dr /. 1 is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
cr . 0 is V22() Function-like set
dom cr is non empty V148() V149() V150() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
ar + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
Dr /. ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
Dr /. (ar + 1) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(Dr /. ar) - (Dr /. (ar + 1)) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.((Dr /. ar) - (Dr /. (ar + 1))).| is V11() real ext-real non negative Element of REAL
Br . (ar + 1) is V11() real ext-real Element of REAL
Br /. (ar + 1) is V11() real ext-real Element of REAL
Cr . (ar + 1) is set
cr . (Br . (ar + 1)) is V22() Function-like set
TR is functional Element of K6( the carrier of (TOP-REAL 2))
E-bound TR is V11() real ext-real Element of REAL
W-bound TR is V11() real ext-real Element of REAL
(E-bound TR) - (W-bound TR) is V11() real ext-real Element of REAL
N-bound TR is V11() real ext-real Element of REAL
S-bound TR is V11() real ext-real Element of REAL
(N-bound TR) - (S-bound TR) is V11() real ext-real Element of REAL
((E-bound TR) - (W-bound TR)) + ((N-bound TR) - (S-bound TR)) is V11() real ext-real Element of REAL
(((E-bound TR) - (W-bound TR)) + ((N-bound TR) - (S-bound TR))) + 1 is V11() real ext-real Element of REAL
TR is Element of K6( the carrier of (Euclid 2))
cr is Element of the carrier of (Euclid 2)
dr is Element of the carrier of (Euclid 2)
dist (cr,dr) is V11() real ext-real Element of REAL
v is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
v `2 is V11() real ext-real Element of REAL
v . 2 is V11() real ext-real Element of REAL
h is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
h `2 is V11() real ext-real Element of REAL
h . 2 is V11() real ext-real Element of REAL
(h `2) - (v `2) is V11() real ext-real Element of REAL
abs ((h `2) - (v `2)) is V11() real ext-real Element of REAL
v `1 is V11() real ext-real Element of REAL
v . 1 is V11() real ext-real Element of REAL
h `1 is V11() real ext-real Element of REAL
h . 1 is V11() real ext-real Element of REAL
(h `1) - (v `1) is V11() real ext-real Element of REAL
abs ((h `1) - (v `1)) is V11() real ext-real Element of REAL
(abs ((h `1) - (v `1))) + (abs ((h `2) - (v `2))) is V11() real ext-real Element of REAL
h - v is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.(h - v).| is V11() real ext-real non negative Element of REAL
dom Br is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
Br . ar is V11() real ext-real Element of REAL
Br /. ar is V11() real ext-real Element of REAL
[.(Br /. ar),(Br /. (ar + 1)).] is compact V148() V149() V150() V225() Element of K6(REAL)
Cr . ar is set
cr . (Br . ar) is V22() Function-like set
cr is V148() V149() V150() Element of K6( the carrier of I[01])
dr is Element of the carrier of (Euclid 2)
cr .: cr is functional Element of K6( the carrier of (TOP-REAL 2))
c `2 is V11() real ext-real Element of REAL
c . 2 is V11() real ext-real Element of REAL
h is Element of the carrier of (Euclid 2)
cr .: [.0,1.] is functional Element of K6( the carrier of (TOP-REAL 2))
v is Element of K6( the carrier of (Euclid 2))
dist (dr,h) is V11() real ext-real Element of REAL
diameter v is V11() real ext-real Element of REAL
dom Dr is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
Dr /. TR is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(Dr /. TR) `2 is V11() real ext-real Element of REAL
(Dr /. TR) . 2 is V11() real ext-real Element of REAL
Dr . TR is V22() Function-like set
Br . TR is V11() real ext-real Element of REAL
cr . (Br . TR) is V22() Function-like set
dom Br is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
dom cr is non empty V148() V149() V150() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
Y_axis Dr is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL
dom (Y_axis Dr) is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
(Y_axis Dr) . TR is V11() real ext-real Element of REAL
len (Y_axis Dr) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
Seg (len (Y_axis Dr)) is V36() V43( len (Y_axis Dr)) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
Seg (len Dr) is V36() V43( len Dr) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
Dr /. TR is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(Dr /. TR) `2 is V11() real ext-real Element of REAL
(Dr /. TR) . 2 is V11() real ext-real Element of REAL
cr . 1 is V22() Function-like set
(Dr /. 1) `1 is V11() real ext-real Element of REAL
(Dr /. 1) . 1 is V11() real ext-real Element of REAL
Dr /. (len Dr) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(Dr /. (len Dr)) `1 is V11() real ext-real Element of REAL
(Dr /. (len Dr)) . 1 is V11() real ext-real Element of REAL
Dr . (len Dr) is V22() Function-like set
cr . (Br . (len Br)) is V22() Function-like set
cr . (Br . 1) is V22() Function-like set
TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
Dr /. TR is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(Dr /. TR) `1 is V11() real ext-real Element of REAL
(Dr /. TR) . 1 is V11() real ext-real Element of REAL
Dr . TR is V22() Function-like set
Br . TR is V11() real ext-real Element of REAL
cr . (Br . TR) is V22() Function-like set
dom Br is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
dom cr is non empty V148() V149() V150() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
X_axis Dr is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL
dom (X_axis Dr) is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
(X_axis Dr) . 1 is V11() real ext-real Element of REAL
(X_axis Dr) . (len Dr) is V11() real ext-real Element of REAL
TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
(X_axis Dr) . TR is V11() real ext-real Element of REAL
len (X_axis Dr) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
Seg (len (X_axis Dr)) is V36() V43( len (X_axis Dr)) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
Seg (len Dr) is V36() V43( len Dr) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
Dr /. TR is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(Dr /. TR) `1 is V11() real ext-real Element of REAL
(Dr /. TR) . 1 is V11() real ext-real Element of REAL
Dr . (len Dr) is V22() Function-like set
TR is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
TR . 1 is V22() Function-like set
len TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
TR . (len TR) is V22() Function-like set
X_axis TR is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL
Y_axis TR is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL
dom TR is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
TR /. (len TR) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
TR is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL
TR . 1 is V11() real ext-real Element of REAL
len TR is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
TR . (len TR) is V11() real ext-real Element of REAL
rng TR is V148() V149() V150() Element of K6(REAL)
ar is V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
len ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
dom ar is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
ar is V22() V25( NAT ) Function-like V36() FinSequence-like FinSubsequence-like set
len ar is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
dom ar is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
rng ar is set
br is set
dom dr is non empty V148() V149() V150() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
cr is set
ar . cr is set
Seg (len ar) is V36() V43( len ar) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
dr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
dom TR is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
TR . dr is V11() real ext-real Element of REAL
ar . dr is set
dr . (TR . dr) is V22() Function-like set
br is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len br is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
cr . (Br . 1) is V22() Function-like set
dom cr is non empty V148() V149() V150() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
br . (len br) is V22() Function-like set
br /. (len br) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
dr . 0 is V22() Function-like set
dom dr is non empty V148() V149() V150() Element of K6( the carrier of I[01])
h is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
h + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
br /. h is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
br /. (h + 1) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(br /. h) - (br /. (h + 1)) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.((br /. h) - (br /. (h + 1))).| is V11() real ext-real non negative Element of REAL
TR . h is V11() real ext-real Element of REAL
TR /. h is V11() real ext-real Element of REAL
Seg (len TR) is V36() V43( len TR) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
dom TR is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
TR . (h + 1) is V11() real ext-real Element of REAL
ar . (h + 1) is set
dr . (TR . (h + 1)) is V22() Function-like set
ar . h is set
dr . (TR . h) is V22() Function-like set
dr .: the carrier of I[01] is functional Element of K6( the carrier of (TOP-REAL 2))
cr is functional Element of K6( the carrier of (TOP-REAL 2))
v is non empty functional Element of K6( the carrier of (TOP-REAL 2))
E-bound v is V11() real ext-real Element of REAL
W-bound v is V11() real ext-real Element of REAL
(E-bound v) - (W-bound v) is V11() real ext-real Element of REAL
N-bound v is V11() real ext-real Element of REAL
S-bound v is V11() real ext-real Element of REAL
(N-bound v) - (S-bound v) is V11() real ext-real Element of REAL
((E-bound v) - (W-bound v)) + ((N-bound v) - (S-bound v)) is V11() real ext-real Element of REAL
(((E-bound v) - (W-bound v)) + ((N-bound v) - (S-bound v))) + 1 is V11() real ext-real Element of REAL
TR /. (h + 1) is V11() real ext-real Element of REAL
dr is Element of K6( the carrier of (Euclid 2))
g is Element of the carrier of (Euclid 2)
y is Element of the carrier of (Euclid 2)
dist (g,y) is V11() real ext-real Element of REAL
s is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
s `2 is V11() real ext-real Element of REAL
s . 2 is V11() real ext-real Element of REAL
t is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
t `2 is V11() real ext-real Element of REAL
t . 2 is V11() real ext-real Element of REAL
(t `2) - (s `2) is V11() real ext-real Element of REAL
abs ((t `2) - (s `2)) is V11() real ext-real Element of REAL
s `1 is V11() real ext-real Element of REAL
s . 1 is V11() real ext-real Element of REAL
t `1 is V11() real ext-real Element of REAL
t . 1 is V11() real ext-real Element of REAL
(t `1) - (s `1) is V11() real ext-real Element of REAL
abs ((t `1) - (s `1)) is V11() real ext-real Element of REAL
(abs ((t `1) - (s `1))) + (abs ((t `2) - (s `2))) is V11() real ext-real Element of REAL
t - s is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.(t - s).| is V11() real ext-real non negative Element of REAL
[.(TR /. h),(TR /. (h + 1)).] is compact V148() V149() V150() V225() Element of K6(REAL)
t is V148() V149() V150() Element of K6( the carrier of I[01])
g is Element of the carrier of (Euclid 2)
dr .: t is functional Element of K6( the carrier of (TOP-REAL 2))
ar `1 is V11() real ext-real Element of REAL
ar . 1 is V11() real ext-real Element of REAL
y is Element of the carrier of (Euclid 2)
dr .: [.0,1.] is functional Element of K6( the carrier of (TOP-REAL 2))
s is Element of K6( the carrier of (Euclid 2))
dist (g,y) is V11() real ext-real Element of REAL
diameter s is V11() real ext-real Element of REAL
br . (h + 1) is V22() Function-like set
dom TR is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
Seg (len TR) is V36() V43( len TR) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
br /. cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
TR . cr is V11() real ext-real Element of REAL
dr . (TR . cr) is V22() Function-like set
br . cr is V22() Function-like set
dom br is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
br /. cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(br /. cr) `1 is V11() real ext-real Element of REAL
(br /. cr) . 1 is V11() real ext-real Element of REAL
Seg (len br) is V36() V43( len br) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
TR . cr is V11() real ext-real Element of REAL
dr . (TR . cr) is V22() Function-like set
dom dr is non empty V148() V149() V150() Element of K6( the carrier of I[01])
X_axis br is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL
dom (X_axis br) is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
(X_axis br) . cr is V11() real ext-real Element of REAL
len (X_axis br) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
Seg (len (X_axis br)) is V36() V43( len (X_axis br)) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
Seg (len br) is V36() V43( len br) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
br /. cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(br /. cr) `1 is V11() real ext-real Element of REAL
(br /. cr) . 1 is V11() real ext-real Element of REAL
dr . 1 is V22() Function-like set
br /. 1 is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(br /. 1) `2 is V11() real ext-real Element of REAL
(br /. 1) . 2 is V11() real ext-real Element of REAL
(br /. (len br)) `2 is V11() real ext-real Element of REAL
(br /. (len br)) . 2 is V11() real ext-real Element of REAL
cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
br /. cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(br /. cr) `2 is V11() real ext-real Element of REAL
(br /. cr) . 2 is V11() real ext-real Element of REAL
Seg (len br) is V36() V43( len br) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
TR . cr is V11() real ext-real Element of REAL
dr . (TR . cr) is V22() Function-like set
dr . (TR . 1) is V22() Function-like set
dr . (TR . (len TR)) is V22() Function-like set
dom dr is non empty V148() V149() V150() Element of K6( the carrier of I[01])
Y_axis br is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL
dom (Y_axis br) is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
(Y_axis br) . 1 is V11() real ext-real Element of REAL
(Y_axis br) . (len br) is V11() real ext-real Element of REAL
cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
(Y_axis br) . cr is V11() real ext-real Element of REAL
len (Y_axis br) is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
Seg (len (Y_axis br)) is V36() V43( len (Y_axis br)) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
Seg (len br) is V36() V43( len br) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
br /. cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(br /. cr) `2 is V11() real ext-real Element of REAL
(br /. cr) . 2 is V11() real ext-real Element of REAL
br . 1 is V22() Function-like set
cr is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
cr . 1 is V22() Function-like set
len cr is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
cr . (len cr) is V22() Function-like set
Y_axis cr is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL
X_axis cr is V22() V25( NAT ) V26( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V138() V139() V140() FinSequence of REAL
dom cr is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
cr /. (len cr) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(X_axis TR) . (len TR) is V11() real ext-real Element of REAL
dom dr is non empty V148() V149() V150() Element of K6( the carrier of I[01])
TR /. 1 is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
cr /. 1 is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(Y_axis cr) . 1 is V11() real ext-real Element of REAL
(Y_axis cr) . (len cr) is V11() real ext-real Element of REAL
(X_axis TR) . 1 is V11() real ext-real Element of REAL
dr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
dr `1 is V11() real ext-real Element of REAL
dr . 1 is V11() real ext-real Element of REAL
c `2 is V11() real ext-real Element of REAL
c . 2 is V11() real ext-real Element of REAL
ar `1 is V11() real ext-real Element of REAL
ar . 1 is V11() real ext-real Element of REAL
LSeg (ar,br) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * ar) + (b1 * br)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
br `1 is V11() real ext-real Element of REAL
br . 1 is V11() real ext-real Element of REAL
(c `2) - (ar `2) is V11() real ext-real Element of REAL
(br `2) - (ar `2) is V11() real ext-real Element of REAL
((c `2) - (ar `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(((c `2) - (ar `2)) / ((br `2) - (ar `2))) * (br `2) is V11() real ext-real Element of REAL
((c `2) - (ar `2)) * (br `2) is V11() real ext-real Element of REAL
(((c `2) - (ar `2)) * (br `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(c `2) * (br `2) is V11() real ext-real Element of REAL
(ar `2) * (br `2) is V11() real ext-real Element of REAL
((c `2) * (br `2)) - ((ar `2) * (br `2)) is V11() real ext-real Element of REAL
(((c `2) * (br `2)) - ((ar `2) * (br `2))) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2))) is V11() real ext-real Element of REAL
((br `2) - (ar `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(((br `2) - (ar `2)) / ((br `2) - (ar `2))) - (((c `2) - (ar `2)) / ((br `2) - (ar `2))) is V11() real ext-real Element of REAL
((br `2) - (ar `2)) - ((c `2) - (ar `2)) is V11() real ext-real Element of REAL
(((br `2) - (ar `2)) - ((c `2) - (ar `2))) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(br `2) - (c `2) is V11() real ext-real Element of REAL
((br `2) - (c `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * (ar `2) is V11() real ext-real Element of REAL
((br `2) - (c `2)) * (ar `2) is V11() real ext-real Element of REAL
(((br `2) - (c `2)) * (ar `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(br `2) * (ar `2) is V11() real ext-real Element of REAL
(c `2) * (ar `2) is V11() real ext-real Element of REAL
((br `2) * (ar `2)) - ((c `2) * (ar `2)) is V11() real ext-real Element of REAL
(((br `2) * (ar `2)) - ((c `2) * (ar `2))) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) + ((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) + ((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br)) `1 is V11() real ext-real Element of REAL
(((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) + ((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br)) . 1 is V11() real ext-real Element of REAL
((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) `1 is V11() real ext-real Element of REAL
((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) . 1 is V11() real ext-real Element of REAL
((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br) `1 is V11() real ext-real Element of REAL
((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br) . 1 is V11() real ext-real Element of REAL
(((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) `1) + (((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br) `1) is V11() real ext-real Element of REAL
(1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * (ar `1) is V11() real ext-real Element of REAL
((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * (ar `1)) + (((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br) `1) is V11() real ext-real Element of REAL
(1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * (c `1) is V11() real ext-real Element of REAL
(((c `2) - (ar `2)) / ((br `2) - (ar `2))) * (c `1) is V11() real ext-real Element of REAL
((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * (c `1)) + ((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * (c `1)) is V11() real ext-real Element of REAL
(((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) + ((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br)) `2 is V11() real ext-real Element of REAL
(((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) + ((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br)) . 2 is V11() real ext-real Element of REAL
((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) `2 is V11() real ext-real Element of REAL
((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) . 2 is V11() real ext-real Element of REAL
((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br) `2 is V11() real ext-real Element of REAL
((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br) . 2 is V11() real ext-real Element of REAL
(((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) `2) + (((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br) `2) is V11() real ext-real Element of REAL
((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * (ar `2)) + (((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * br) `2) is V11() real ext-real Element of REAL
((1 - (((c `2) - (ar `2)) / ((br `2) - (ar `2)))) * (ar `2)) + ((((c `2) - (ar `2)) / ((br `2) - (ar `2))) * (br `2)) is V11() real ext-real Element of REAL
(((br `2) * (ar `2)) - ((c `2) * (ar `2))) + (((c `2) * (br `2)) - ((ar `2) * (br `2))) is V11() real ext-real Element of REAL
((((br `2) * (ar `2)) - ((c `2) * (ar `2))) + (((c `2) * (br `2)) - ((ar `2) * (br `2)))) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(c `2) * ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
((c `2) * ((br `2) - (ar `2))) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(c `2) * (((br `2) - (ar `2)) / ((br `2) - (ar `2))) is V11() real ext-real Element of REAL
(c `2) * 1 is V11() real ext-real Element of REAL
br `1 is V11() real ext-real Element of REAL
br . 1 is V11() real ext-real Element of REAL
dr is set
h is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
h `2 is V11() real ext-real Element of REAL
h . 2 is V11() real ext-real Element of REAL
(h `2) - (ar `2) is V11() real ext-real Element of REAL
(br `2) - (ar `2) is V11() real ext-real Element of REAL
((h `2) - (ar `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(((h `2) - (ar `2)) / ((br `2) - (ar `2))) * (br `2) is V11() real ext-real Element of REAL
((h `2) - (ar `2)) * (br `2) is V11() real ext-real Element of REAL
(((h `2) - (ar `2)) * (br `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(h `2) * (br `2) is V11() real ext-real Element of REAL
(ar `2) * (br `2) is V11() real ext-real Element of REAL
((h `2) * (br `2)) - ((ar `2) * (br `2)) is V11() real ext-real Element of REAL
(((h `2) * (br `2)) - ((ar `2) * (br `2))) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2))) is V11() real ext-real Element of REAL
((br `2) - (ar `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(((br `2) - (ar `2)) / ((br `2) - (ar `2))) - (((h `2) - (ar `2)) / ((br `2) - (ar `2))) is V11() real ext-real Element of REAL
((br `2) - (ar `2)) - ((h `2) - (ar `2)) is V11() real ext-real Element of REAL
(((br `2) - (ar `2)) - ((h `2) - (ar `2))) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(br `2) - (h `2) is V11() real ext-real Element of REAL
((br `2) - (h `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * (ar `2) is V11() real ext-real Element of REAL
((br `2) - (h `2)) * (ar `2) is V11() real ext-real Element of REAL
(((br `2) - (h `2)) * (ar `2)) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(br `2) * (ar `2) is V11() real ext-real Element of REAL
(h `2) * (ar `2) is V11() real ext-real Element of REAL
((br `2) * (ar `2)) - ((h `2) * (ar `2)) is V11() real ext-real Element of REAL
(((br `2) * (ar `2)) - ((h `2) * (ar `2))) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) + ((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) + ((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br)) `2 is V11() real ext-real Element of REAL
(((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) + ((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br)) . 2 is V11() real ext-real Element of REAL
((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) `2 is V11() real ext-real Element of REAL
((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) . 2 is V11() real ext-real Element of REAL
((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br) `2 is V11() real ext-real Element of REAL
((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br) . 2 is V11() real ext-real Element of REAL
(((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) `2) + (((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br) `2) is V11() real ext-real Element of REAL
((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * (ar `2)) + (((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br) `2) is V11() real ext-real Element of REAL
((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * (ar `2)) + ((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * (br `2)) is V11() real ext-real Element of REAL
(((br `2) * (ar `2)) - ((h `2) * (ar `2))) + (((h `2) * (br `2)) - ((ar `2) * (br `2))) is V11() real ext-real Element of REAL
((((br `2) * (ar `2)) - ((h `2) * (ar `2))) + (((h `2) * (br `2)) - ((ar `2) * (br `2)))) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(h `2) * ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
((h `2) * ((br `2) - (ar `2))) / ((br `2) - (ar `2)) is V11() real ext-real Element of REAL
(h `2) * (((br `2) - (ar `2)) / ((br `2) - (ar `2))) is V11() real ext-real Element of REAL
(h `2) * 1 is V11() real ext-real Element of REAL
h `1 is V11() real ext-real Element of REAL
h . 1 is V11() real ext-real Element of REAL
(((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) + ((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br)) `1 is V11() real ext-real Element of REAL
(((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) + ((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br)) . 1 is V11() real ext-real Element of REAL
((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) `1 is V11() real ext-real Element of REAL
((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) . 1 is V11() real ext-real Element of REAL
((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br) `1 is V11() real ext-real Element of REAL
((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br) . 1 is V11() real ext-real Element of REAL
(((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * ar) `1) + (((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br) `1) is V11() real ext-real Element of REAL
(1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * (ar `1) is V11() real ext-real Element of REAL
((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * (ar `1)) + (((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * br) `1) is V11() real ext-real Element of REAL
(1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * (c `1) is V11() real ext-real Element of REAL
(((h `2) - (ar `2)) / ((br `2) - (ar `2))) * (c `1) is V11() real ext-real Element of REAL
((1 - (((h `2) - (ar `2)) / ((br `2) - (ar `2)))) * (c `1)) + ((((h `2) - (ar `2)) / ((br `2) - (ar `2))) * (c `1)) is V11() real ext-real Element of REAL
dr . (TR . 1) is V22() Function-like set
dr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
dr `2 is V11() real ext-real Element of REAL
dr . 2 is V11() real ext-real Element of REAL
ar `1 is V11() real ext-real Element of REAL
ar . 1 is V11() real ext-real Element of REAL
c `2 is V11() real ext-real Element of REAL
c . 2 is V11() real ext-real Element of REAL
LSeg (c,d) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * c) + (b1 * d)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
d `2 is V11() real ext-real Element of REAL
d . 2 is V11() real ext-real Element of REAL
(ar `1) - (c `1) is V11() real ext-real Element of REAL
(d `1) - (c `1) is V11() real ext-real Element of REAL
((ar `1) - (c `1)) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(((ar `1) - (c `1)) / ((d `1) - (c `1))) * (d `1) is V11() real ext-real Element of REAL
((ar `1) - (c `1)) * (d `1) is V11() real ext-real Element of REAL
(((ar `1) - (c `1)) * (d `1)) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(ar `1) * (d `1) is V11() real ext-real Element of REAL
(c `1) * (d `1) is V11() real ext-real Element of REAL
((ar `1) * (d `1)) - ((c `1) * (d `1)) is V11() real ext-real Element of REAL
(((ar `1) * (d `1)) - ((c `1) * (d `1))) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
1 - (((ar `1) - (c `1)) / ((d `1) - (c `1))) is V11() real ext-real Element of REAL
((d `1) - (c `1)) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(((d `1) - (c `1)) / ((d `1) - (c `1))) - (((ar `1) - (c `1)) / ((d `1) - (c `1))) is V11() real ext-real Element of REAL
((d `1) - (c `1)) - ((ar `1) - (c `1)) is V11() real ext-real Element of REAL
(((d `1) - (c `1)) - ((ar `1) - (c `1))) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(d `1) - (ar `1) is V11() real ext-real Element of REAL
((d `1) - (ar `1)) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * (c `1) is V11() real ext-real Element of REAL
((d `1) - (ar `1)) * (c `1) is V11() real ext-real Element of REAL
(((d `1) - (ar `1)) * (c `1)) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(d `1) * (c `1) is V11() real ext-real Element of REAL
(ar `1) * (c `1) is V11() real ext-real Element of REAL
((d `1) * (c `1)) - ((ar `1) * (c `1)) is V11() real ext-real Element of REAL
(((d `1) * (c `1)) - ((ar `1) * (c `1))) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * c is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(((ar `1) - (c `1)) / ((d `1) - (c `1))) * d is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * c) + ((((ar `1) - (c `1)) / ((d `1) - (c `1))) * d) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * c) + ((((ar `1) - (c `1)) / ((d `1) - (c `1))) * d)) `2 is V11() real ext-real Element of REAL
(((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * c) + ((((ar `1) - (c `1)) / ((d `1) - (c `1))) * d)) . 2 is V11() real ext-real Element of REAL
((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * c) `2 is V11() real ext-real Element of REAL
((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * c) . 2 is V11() real ext-real Element of REAL
((((ar `1) - (c `1)) / ((d `1) - (c `1))) * d) `2 is V11() real ext-real Element of REAL
((((ar `1) - (c `1)) / ((d `1) - (c `1))) * d) . 2 is V11() real ext-real Element of REAL
(((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * c) `2) + (((((ar `1) - (c `1)) / ((d `1) - (c `1))) * d) `2) is V11() real ext-real Element of REAL
(1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * (c `2) is V11() real ext-real Element of REAL
((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * (c `2)) + (((((ar `1) - (c `1)) / ((d `1) - (c `1))) * d) `2) is V11() real ext-real Element of REAL
(1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * (ar `2) is V11() real ext-real Element of REAL
(((ar `1) - (c `1)) / ((d `1) - (c `1))) * (ar `2) is V11() real ext-real Element of REAL
((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * (ar `2)) + ((((ar `1) - (c `1)) / ((d `1) - (c `1))) * (ar `2)) is V11() real ext-real Element of REAL
(((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * c) + ((((ar `1) - (c `1)) / ((d `1) - (c `1))) * d)) `1 is V11() real ext-real Element of REAL
(((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * c) + ((((ar `1) - (c `1)) / ((d `1) - (c `1))) * d)) . 1 is V11() real ext-real Element of REAL
((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * c) `1 is V11() real ext-real Element of REAL
((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * c) . 1 is V11() real ext-real Element of REAL
((((ar `1) - (c `1)) / ((d `1) - (c `1))) * d) `1 is V11() real ext-real Element of REAL
((((ar `1) - (c `1)) / ((d `1) - (c `1))) * d) . 1 is V11() real ext-real Element of REAL
(((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * c) `1) + (((((ar `1) - (c `1)) / ((d `1) - (c `1))) * d) `1) is V11() real ext-real Element of REAL
((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * (c `1)) + (((((ar `1) - (c `1)) / ((d `1) - (c `1))) * d) `1) is V11() real ext-real Element of REAL
((1 - (((ar `1) - (c `1)) / ((d `1) - (c `1)))) * (c `1)) + ((((ar `1) - (c `1)) / ((d `1) - (c `1))) * (d `1)) is V11() real ext-real Element of REAL
(((d `1) * (c `1)) - ((ar `1) * (c `1))) + (((ar `1) * (d `1)) - ((c `1) * (d `1))) is V11() real ext-real Element of REAL
((((d `1) * (c `1)) - ((ar `1) * (c `1))) + (((ar `1) * (d `1)) - ((c `1) * (d `1)))) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(ar `1) * ((d `1) - (c `1)) is V11() real ext-real Element of REAL
((ar `1) * ((d `1) - (c `1))) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(ar `1) * (((d `1) - (c `1)) / ((d `1) - (c `1))) is V11() real ext-real Element of REAL
(ar `1) * 1 is V11() real ext-real Element of REAL
d `2 is V11() real ext-real Element of REAL
d . 2 is V11() real ext-real Element of REAL
dr is set
h is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
h `1 is V11() real ext-real Element of REAL
h . 1 is V11() real ext-real Element of REAL
(h `1) - (c `1) is V11() real ext-real Element of REAL
(d `1) - (c `1) is V11() real ext-real Element of REAL
((h `1) - (c `1)) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(((h `1) - (c `1)) / ((d `1) - (c `1))) * (d `1) is V11() real ext-real Element of REAL
((h `1) - (c `1)) * (d `1) is V11() real ext-real Element of REAL
(((h `1) - (c `1)) * (d `1)) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(h `1) * (d `1) is V11() real ext-real Element of REAL
(c `1) * (d `1) is V11() real ext-real Element of REAL
((h `1) * (d `1)) - ((c `1) * (d `1)) is V11() real ext-real Element of REAL
(((h `1) * (d `1)) - ((c `1) * (d `1))) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
1 - (((h `1) - (c `1)) / ((d `1) - (c `1))) is V11() real ext-real Element of REAL
((d `1) - (c `1)) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(((d `1) - (c `1)) / ((d `1) - (c `1))) - (((h `1) - (c `1)) / ((d `1) - (c `1))) is V11() real ext-real Element of REAL
((d `1) - (c `1)) - ((h `1) - (c `1)) is V11() real ext-real Element of REAL
(((d `1) - (c `1)) - ((h `1) - (c `1))) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(d `1) - (h `1) is V11() real ext-real Element of REAL
((d `1) - (h `1)) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * (c `1) is V11() real ext-real Element of REAL
((d `1) - (h `1)) * (c `1) is V11() real ext-real Element of REAL
(((d `1) - (h `1)) * (c `1)) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(d `1) * (c `1) is V11() real ext-real Element of REAL
(h `1) * (c `1) is V11() real ext-real Element of REAL
((d `1) * (c `1)) - ((h `1) * (c `1)) is V11() real ext-real Element of REAL
(((d `1) * (c `1)) - ((h `1) * (c `1))) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * c is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(((h `1) - (c `1)) / ((d `1) - (c `1))) * d is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * c) + ((((h `1) - (c `1)) / ((d `1) - (c `1))) * d) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * c) + ((((h `1) - (c `1)) / ((d `1) - (c `1))) * d)) `1 is V11() real ext-real Element of REAL
(((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * c) + ((((h `1) - (c `1)) / ((d `1) - (c `1))) * d)) . 1 is V11() real ext-real Element of REAL
((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * c) `1 is V11() real ext-real Element of REAL
((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * c) . 1 is V11() real ext-real Element of REAL
((((h `1) - (c `1)) / ((d `1) - (c `1))) * d) `1 is V11() real ext-real Element of REAL
((((h `1) - (c `1)) / ((d `1) - (c `1))) * d) . 1 is V11() real ext-real Element of REAL
(((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * c) `1) + (((((h `1) - (c `1)) / ((d `1) - (c `1))) * d) `1) is V11() real ext-real Element of REAL
((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * (c `1)) + (((((h `1) - (c `1)) / ((d `1) - (c `1))) * d) `1) is V11() real ext-real Element of REAL
((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * (c `1)) + ((((h `1) - (c `1)) / ((d `1) - (c `1))) * (d `1)) is V11() real ext-real Element of REAL
(((d `1) * (c `1)) - ((h `1) * (c `1))) + (((h `1) * (d `1)) - ((c `1) * (d `1))) is V11() real ext-real Element of REAL
((((d `1) * (c `1)) - ((h `1) * (c `1))) + (((h `1) * (d `1)) - ((c `1) * (d `1)))) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(h `1) * ((d `1) - (c `1)) is V11() real ext-real Element of REAL
((h `1) * ((d `1) - (c `1))) / ((d `1) - (c `1)) is V11() real ext-real Element of REAL
(h `1) * (((d `1) - (c `1)) / ((d `1) - (c `1))) is V11() real ext-real Element of REAL
(h `1) * 1 is V11() real ext-real Element of REAL
h `2 is V11() real ext-real Element of REAL
h . 2 is V11() real ext-real Element of REAL
(((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * c) + ((((h `1) - (c `1)) / ((d `1) - (c `1))) * d)) `2 is V11() real ext-real Element of REAL
(((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * c) + ((((h `1) - (c `1)) / ((d `1) - (c `1))) * d)) . 2 is V11() real ext-real Element of REAL
((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * c) `2 is V11() real ext-real Element of REAL
((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * c) . 2 is V11() real ext-real Element of REAL
((((h `1) - (c `1)) / ((d `1) - (c `1))) * d) `2 is V11() real ext-real Element of REAL
((((h `1) - (c `1)) / ((d `1) - (c `1))) * d) . 2 is V11() real ext-real Element of REAL
(((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * c) `2) + (((((h `1) - (c `1)) / ((d `1) - (c `1))) * d) `2) is V11() real ext-real Element of REAL
(1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * (c `2) is V11() real ext-real Element of REAL
((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * (c `2)) + (((((h `1) - (c `1)) / ((d `1) - (c `1))) * d) `2) is V11() real ext-real Element of REAL
(1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * (ar `2) is V11() real ext-real Element of REAL
(((h `1) - (c `1)) / ((d `1) - (c `1))) * (ar `2) is V11() real ext-real Element of REAL
((1 - (((h `1) - (c `1)) / ((d `1) - (c `1)))) * (ar `2)) + ((((h `1) - (c `1)) / ((d `1) - (c `1))) * (ar `2)) is V11() real ext-real Element of REAL
L~ TR is functional closed Element of K6( the carrier of (TOP-REAL 2))
L~ cr is functional closed Element of K6( the carrier of (TOP-REAL 2))
dr is set
h is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
{ (LSeg (TR,b1)) where b1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT : ( 1 <= b1 & b1 + 1 <= len TR ) } is set
union { (LSeg (TR,b1)) where b1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT : ( 1 <= b1 & b1 + 1 <= len TR ) } is set
v is set
{ (LSeg (cr,b1)) where b1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT : ( 1 <= b1 & b1 + 1 <= len cr ) } is set
union { (LSeg (cr,b1)) where b1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT : ( 1 <= b1 & b1 + 1 <= len cr ) } is set
f is set
g is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
LSeg (TR,g) is functional closed Element of K6( the carrier of (TOP-REAL 2))
g + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
TR /. g is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
TR /. (g + 1) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
LSeg ((TR /. g),(TR /. (g + 1))) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (TR /. g)) + (b1 * (TR /. (g + 1)))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
h - (TR /. g) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.(h - (TR /. g)).| is V11() real ext-real non negative Element of REAL
(TR /. g) - (TR /. (g + 1)) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.((TR /. g) - (TR /. (g + 1))).| is V11() real ext-real non negative Element of REAL
y is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
Dr /. y is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(TR /. g) - (Dr /. y) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.((TR /. g) - (Dr /. y)).| is V11() real ext-real non negative Element of REAL
t is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
LSeg (cr,t) is functional closed Element of K6( the carrier of (TOP-REAL 2))
t + 1 is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
cr /. t is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
cr /. (t + 1) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
LSeg ((cr /. t),(cr /. (t + 1))) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * (cr /. t)) + (b1 * (cr /. (t + 1)))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
h - (cr /. t) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.(h - (cr /. t)).| is V11() real ext-real non negative Element of REAL
(cr /. t) - (cr /. (t + 1)) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.((cr /. t) - (cr /. (t + 1))).| is V11() real ext-real non negative Element of REAL
h - (Dr /. y) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.(h - (Dr /. y)).| is V11() real ext-real non negative Element of REAL
|.(h - (TR /. g)).| + |.((TR /. g) - (Dr /. y)).| is V11() real ext-real non negative Element of REAL
((min_dist_min (h,v)) / 5) + ((min_dist_min (h,v)) / 5) is V11() real ext-real Element of REAL
s is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
s - h is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.(s - h).| is V11() real ext-real non negative Element of REAL
Seg (len Dr) is V36() V43( len Dr) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
Dr . y is V22() Function-like set
Br . y is V11() real ext-real Element of REAL
cr . (Br . y) is V22() Function-like set
s is natural V11() real ext-real integer V101() V148() V149() V150() V151() V152() V153() V222() Element of NAT
br /. s is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(cr /. t) - (br /. s) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.((cr /. t) - (br /. s)).| is V11() real ext-real non negative Element of REAL
Seg (len br) is V36() V43( len br) V148() V149() V150() V151() V152() V153() V222() V223() V224() Element of K6(NAT)
TR . s is V11() real ext-real Element of REAL
dr . (TR . s) is V22() Function-like set
t is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
dom Br is V148() V149() V150() V151() V152() V153() V222() Element of K6(NAT)
t1 is Element of the carrier of (Euclid 2)
c31 is Element of the carrier of (Euclid 2)
dist (t1,c31) is V11() real ext-real Element of REAL
s - t is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.(s - t).| is V11() real ext-real non negative Element of REAL
h - (br /. s) is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.(h - (br /. s)).| is V11() real ext-real non negative Element of REAL
|.(h - (cr /. t)).| + |.((cr /. t) - (br /. s)).| is V11() real ext-real non negative Element of REAL
h - t is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
|.(h - t).| is V11() real ext-real non negative Element of REAL
|.(s - h).| + |.(h - t).| is V11() real ext-real non negative Element of REAL
(((min_dist_min (h,v)) / 5) + ((min_dist_min (h,v)) / 5)) + (((min_dist_min (h,v)) / 5) + ((min_dist_min (h,v)) / 5)) is V11() real ext-real Element of REAL
(((min_dist_min (h,v)) / 5) + ((min_dist_min (h,v)) / 5)) + ((min_dist_min (h,v)) / 5) is V11() real ext-real Element of REAL
((((min_dist_min (h,v)) / 5) + ((min_dist_min (h,v)) / 5)) + ((min_dist_min (h,v)) / 5)) + ((min_dist_min (h,v)) / 5) is V11() real ext-real Element of REAL
4 is non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() Element of NAT
4 * ((min_dist_min (h,v)) / 5) is V11() real ext-real Element of REAL
5 * ((min_dist_min (h,v)) / 5) is V11() real ext-real Element of REAL
(4 * ((min_dist_min (h,v)) / 5)) - (5 * ((min_dist_min (h,v)) / 5)) is V11() real ext-real Element of REAL
4 - 5 is V11() real ext-real integer Element of REAL
(4 - 5) * ((min_dist_min (h,v)) / 5) is V11() real ext-real Element of REAL
((4 - 5) * ((min_dist_min (h,v)) / 5)) / ((min_dist_min (h,v)) / 5) is V11() real ext-real Element of REAL
K7( the carrier of I[01], the carrier of (TOP-REAL 2)) is V22() set
K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2))) is set
a is V11() real ext-real set
b is V11() real ext-real set
c is V11() real ext-real set
d is V11() real ext-real set
ar is non empty V22() V25( the carrier of I[01]) V26( the carrier of (TOP-REAL 2)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL 2)) continuous Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
br is non empty V22() V25( the carrier of I[01]) V26( the carrier of (TOP-REAL 2)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL 2)) continuous Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
rng ar is non empty functional Element of K6( the carrier of (TOP-REAL 2))
rng br is non empty functional Element of K6( the carrier of (TOP-REAL 2))
cr is V11() real ext-real Element of the carrier of I[01]
dr is V11() real ext-real Element of the carrier of I[01]
ar . cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(ar . cr) `1 is V11() real ext-real Element of REAL
(ar . cr) . 1 is V11() real ext-real Element of REAL
ar . dr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(ar . dr) `1 is V11() real ext-real Element of REAL
(ar . dr) . 1 is V11() real ext-real Element of REAL
br . cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(br . cr) `2 is V11() real ext-real Element of REAL
(br . cr) . 2 is V11() real ext-real Element of REAL
br . dr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(br . dr) `2 is V11() real ext-real Element of REAL
(br . dr) . 2 is V11() real ext-real Element of REAL
h is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | h is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | h) is non empty set
[#] ((TOP-REAL 2) | h) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | h))
K6( the carrier of ((TOP-REAL 2) | h)) is set
dom br is non empty V148() V149() V150() Element of K6( the carrier of I[01])
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | h)) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | h))) is set
v is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | h)) Function-like total V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | h)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | h)))
v . dr is Element of the carrier of ((TOP-REAL 2) | h)
v . cr is Element of the carrier of ((TOP-REAL 2) | h)
Cr is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | Cr is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | Cr) is non empty set
[#] ((TOP-REAL 2) | Cr) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | Cr))
K6( the carrier of ((TOP-REAL 2) | Cr)) is set
dom ar is non empty V148() V149() V150() Element of K6( the carrier of I[01])
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | Cr)) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | Cr))) is set
Dr is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | Cr)) Function-like total V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | Cr)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | Cr)))
Dr . dr is Element of the carrier of ((TOP-REAL 2) | Cr)
Dr . cr is Element of the carrier of ((TOP-REAL 2) | Cr)
TR is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
TR `1 is V11() real ext-real Element of REAL
TR . 1 is V11() real ext-real Element of REAL
TR is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
TR `1 is V11() real ext-real Element of REAL
TR . 1 is V11() real ext-real Element of REAL
ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
ar `1 is V11() real ext-real Element of REAL
ar . 1 is V11() real ext-real Element of REAL
dom Dr is non empty V148() V149() V150() Element of K6( the carrier of I[01])
br is set
Dr . br is set
Br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
Br `2 is V11() real ext-real Element of REAL
Br . 2 is V11() real ext-real Element of REAL
Ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
Ar `2 is V11() real ext-real Element of REAL
Ar . 2 is V11() real ext-real Element of REAL
ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
ar `2 is V11() real ext-real Element of REAL
ar . 2 is V11() real ext-real Element of REAL
dom Dr is non empty V148() V149() V150() Element of K6( the carrier of I[01])
br is set
Dr . br is set
ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
ar `2 is V11() real ext-real Element of REAL
ar . 2 is V11() real ext-real Element of REAL
dom v is non empty V148() V149() V150() Element of K6( the carrier of I[01])
br is set
v . br is set
ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
ar `1 is V11() real ext-real Element of REAL
ar . 1 is V11() real ext-real Element of REAL
dom v is non empty V148() V149() V150() Element of K6( the carrier of I[01])
br is set
v . br is set
a is V11() real ext-real set
b is V11() real ext-real set
c is V11() real ext-real set
d is V11() real ext-real set
Trectangle (a,b,c,d) is TopSpace-like convex SubSpace of TOP-REAL 2
closed_inside_of_rectangle (a,b,c,d) is functional convex Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d)) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of (Trectangle (a,b,c,d)) is set
ar is Element of the carrier of (Trectangle (a,b,c,d))
br is Element of the carrier of (Trectangle (a,b,c,d))
dr is Element of the carrier of (Trectangle (a,b,c,d))
cr is Element of the carrier of (Trectangle (a,b,c,d))
h is V22() V25( the carrier of I[01]) V26( the carrier of (Trectangle (a,b,c,d))) Function-like V33( the carrier of I[01], the carrier of (Trectangle (a,b,c,d))) Path of ar,br
v is V22() V25( the carrier of I[01]) V26( the carrier of (Trectangle (a,b,c,d))) Function-like V33( the carrier of I[01], the carrier of (Trectangle (a,b,c,d))) Path of dr,cr
Ar is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
Ar `1 is V11() real ext-real Element of REAL
Ar . 1 is V11() real ext-real Element of REAL
Br is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
Br `1 is V11() real ext-real Element of REAL
Br . 1 is V11() real ext-real Element of REAL
Cr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
Cr `2 is V11() real ext-real Element of REAL
Cr . 2 is V11() real ext-real Element of REAL
Dr is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
Dr `2 is V11() real ext-real Element of REAL
Dr . 2 is V11() real ext-real Element of REAL
h . 1[01] is Element of the carrier of (Trectangle (a,b,c,d))
v . 1[01] is Element of the carrier of (Trectangle (a,b,c,d))
TR is non empty TopSpace-like connected convex pathwise_connected SubSpace of TOP-REAL 2
the carrier of TR is non empty set
ar is Element of the carrier of TR
br is Element of the carrier of TR
dr is Element of the carrier of TR
cr is Element of the carrier of TR
h is non empty V22() V25( the carrier of I[01]) V26( the carrier of TR) Function-like total V33( the carrier of I[01], the carrier of TR) continuous Path of ar,br
h . 0 is set
h . 1 is set
v is non empty V22() V25( the carrier of I[01]) V26( the carrier of TR) Function-like total V33( the carrier of I[01], the carrier of TR) continuous Path of dr,cr
- v is non empty V22() V25( the carrier of I[01]) V26( the carrier of TR) Function-like total V33( the carrier of I[01], the carrier of TR) continuous Path of cr,dr
(- v) . 0 is set
(- v) . 1 is set
f is non empty V22() V25( the carrier of I[01]) V26( the carrier of (TOP-REAL 2)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
g is non empty V22() V25( the carrier of I[01]) V26( the carrier of (TOP-REAL 2)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
y is V11() real ext-real Element of the carrier of I[01]
f . y is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(f . y) `1 is V11() real ext-real Element of REAL
(f . y) . 1 is V11() real ext-real Element of REAL
g . y is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
(g . y) `1 is V11() real ext-real Element of REAL
(g . y) . 1 is V11() real ext-real Element of REAL
(f . y) `2 is V11() real ext-real Element of REAL
(f . y) . 2 is V11() real ext-real Element of REAL
(g . y) `2 is V11() real ext-real Element of REAL
(g . y) . 2 is V11() real ext-real Element of REAL
{ b1 where b1 is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2) : ( a <= b1 `1 & b1 `1 <= b & c <= b1 `2 & b1 `2 <= d ) } is set
(- v) . y is Element of the carrier of TR
h . y is Element of the carrier of TR
t is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
t `1 is V11() real ext-real Element of REAL
t . 1 is V11() real ext-real Element of REAL
t `2 is V11() real ext-real Element of REAL
t . 2 is V11() real ext-real Element of REAL
s is V22() V25( NAT ) Function-like V36() V43(2) FinSequence-like FinSubsequence-like V138() V139() V140() Element of the carrier of (TOP-REAL 2)
s `1 is V11() real ext-real Element of REAL
s . 1 is V11() real ext-real Element of REAL
s `2 is V11() real ext-real Element of REAL
s . 2 is V11() real ext-real Element of REAL
rng f is non empty functional Element of K6( the carrier of (TOP-REAL 2))
rng g is non empty functional Element of K6( the carrier of (TOP-REAL 2))
y is set
dom g is non empty V148() V149() V150() Element of K6( the carrier of I[01])
t is set
g . t is V22() Function-like set
dom f is non empty V148() V149() V150() Element of K6( the carrier of I[01])
s is set
f . s is V22() Function-like set
t is V11() real ext-real Element of the carrier of I[01]
1 - t is V11() real ext-real Element of REAL
s is V11() real ext-real Element of the carrier of I[01]
h . s is Element of the carrier of (Trectangle (a,b,c,d))
t1 is V11() real ext-real Element of the carrier of I[01]
v . t1 is Element of the carrier of (Trectangle (a,b,c,d))