:: TOPREAL3 semantic presentation

REAL is non empty V37() V137() V138() V139() V143() set
NAT is V137() V138() V139() V140() V141() V142() V143() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V37() V137() V143() set
RAT is non empty V37() V137() V138() V139() V140() V143() set
INT is non empty V37() V137() V138() V139() V140() V141() V143() set
K20(COMPLEX,COMPLEX) is complex-yielding set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-yielding set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(REAL,REAL) is complex-yielding V128() V129() set
K19(K20(REAL,REAL)) is set
K20(K20(REAL,REAL),REAL) is complex-yielding V128() V129() set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is RAT -valued complex-yielding V128() V129() set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is RAT -valued complex-yielding V128() V129() set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is RAT -valued INT -valued complex-yielding V128() V129() set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is RAT -valued INT -valued complex-yielding V128() V129() set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is RAT -valued INT -valued complex-yielding V128() V129() V130() set
K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued complex-yielding V128() V129() V130() set
K19(K20(K20(NAT,NAT),NAT)) is set
omega is V137() V138() V139() V140() V141() V142() V143() set
K19(omega) is set
K19(NAT) is set
1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
K20(1,1) is RAT -valued INT -valued complex-yielding V128() V129() V130() set
K19(K20(1,1)) is set
K20(K20(1,1),1) is RAT -valued INT -valued complex-yielding V128() V129() V130() set
K19(K20(K20(1,1),1)) is set
K20(K20(1,1),REAL) is complex-yielding V128() V129() set
K19(K20(K20(1,1),REAL)) is set
2 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
K20(2,2) is RAT -valued INT -valued complex-yielding V128() V129() V130() set
K20(K20(2,2),REAL) is complex-yielding V128() V129() set
K19(K20(K20(2,2),REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V103() V149() V150() V151() V152() V153() V154() V155() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K19( the carrier of (TOP-REAL 2)) is set
{} is functional empty FinSequence-membered V137() V138() V139() V140() V141() V142() V143() set
the functional empty FinSequence-membered V137() V138() V139() V140() V141() V142() V143() set is functional empty FinSequence-membered V137() V138() V139() V140() V141() V142() V143() set
3 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
0 is functional empty ordinal natural V22() real ext-real non positive non negative V33() V34() FinSequence-membered V137() V138() V139() V140() V141() V142() V143() Element of NAT
sqrreal is Relation-like REAL -defined REAL -valued Function-like V30( REAL , REAL ) complex-yielding V128() V129() Element of K19(K20(REAL,REAL))
absreal is Relation-like REAL -defined REAL -valued Function-like V30( REAL , REAL ) complex-yielding V128() V129() Element of K19(K20(REAL,REAL))
diffreal is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V30(K20(REAL,REAL), REAL ) complex-yielding V128() V129() Element of K19(K20(K20(REAL,REAL),REAL))
K175() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V30(K20(REAL,REAL), REAL ) complex-yielding V128() V129() Element of K19(K20(K20(REAL,REAL),REAL))
id REAL is Relation-like REAL -defined REAL -valued non empty total complex-yielding V128() V129() Element of K19(K20(REAL,REAL))
K173() is Relation-like REAL -defined REAL -valued Function-like V30( REAL , REAL ) complex-yielding V128() V129() Element of K19(K20(REAL,REAL))
K258(REAL,K175(),(id REAL),K173()) is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V30(K20(REAL,REAL), REAL ) complex-yielding V128() V129() Element of K19(K20(K20(REAL,REAL),REAL))
Euclid 2 is non empty strict Reflexive discerning V86() triangle MetrStruct
REAL 2 is functional non empty FinSequence-membered FinSequenceSet of REAL
2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist 2 is Relation-like K20((REAL 2),(REAL 2)) -defined REAL -valued Function-like V30(K20((REAL 2),(REAL 2)), REAL ) complex-yielding V128() V129() Element of K19(K20(K20((REAL 2),(REAL 2)),REAL))
K20((REAL 2),(REAL 2)) is set
K20(K20((REAL 2),(REAL 2)),REAL) is complex-yielding V128() V129() set
K19(K20(K20((REAL 2),(REAL 2)),REAL)) is set
MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct
the carrier of (Euclid 2) is non empty set
n is set
f is set
q is set
<*n,f,q*> is Relation-like NAT -defined Function-like non empty V37() V44(3) FinSequence-like FinSubsequence-like set
dom <*n,f,q*> is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
len <*n,f,q*> is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n + f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (n,f) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(n + f) `1 is V22() real ext-real Element of REAL
K434((n + f),1) is V22() real ext-real Element of REAL
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
(n `1) + (f `1) is V22() real ext-real Element of REAL
(n + f) `2 is V22() real ext-real Element of REAL
K434((n + f),2) is V22() real ext-real Element of REAL
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
(n `2) + (f `2) is V22() real ext-real Element of REAL
|[((n `1) + (f `1)),((n `2) + (f `2))]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n - f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
- f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
K312((TOP-REAL 2),n,(- f)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (n,(- f)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(n - f) `1 is V22() real ext-real Element of REAL
K434((n - f),1) is V22() real ext-real Element of REAL
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
(n `1) - (f `1) is V22() real ext-real Element of REAL
(n - f) `2 is V22() real ext-real Element of REAL
K434((n - f),2) is V22() real ext-real Element of REAL
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
(n `2) - (f `2) is V22() real ext-real Element of REAL
|[((n `1) - (f `1)),((n `2) - (f `2))]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V22() real ext-real set
f * n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(f * n) `1 is V22() real ext-real Element of REAL
K434((f * n),1) is V22() real ext-real Element of REAL
f * (n `1) is V22() real ext-real Element of REAL
(f * n) `2 is V22() real ext-real Element of REAL
K434((f * n),2) is V22() real ext-real Element of REAL
f * (n `2) is V22() real ext-real Element of REAL
|[(f * (n `1)),(f * (n `2))]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n + f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (n,f) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n - f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
- f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
K312((TOP-REAL 2),n,(- f)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) . (n,(- f)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
q is V22() real ext-real set
r is V22() real ext-real set
<*q,r*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
u is V22() real ext-real set
q + u is V22() real ext-real set
q - u is V22() real ext-real set
v is V22() real ext-real set
<*u,v*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
r + v is V22() real ext-real set
<*(q + u),(r + v)*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
r - v is V22() real ext-real set
<*(q - u),(r - v)*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
|[q,r]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[q,r]| `1 is V22() real ext-real Element of REAL
K434(|[q,r]|,1) is V22() real ext-real Element of REAL
|[q,r]| `2 is V22() real ext-real Element of REAL
K434(|[q,r]|,2) is V22() real ext-real Element of REAL
|[u,v]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[u,v]| `1 is V22() real ext-real Element of REAL
K434(|[u,v]|,1) is V22() real ext-real Element of REAL
|[u,v]| `2 is V22() real ext-real Element of REAL
K434(|[u,v]|,2) is V22() real ext-real Element of REAL
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
|[(f `1),(f `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
(n `1) - (f `1) is V22() real ext-real Element of REAL
((n `1) - (f `1)) ^2 is V22() real ext-real Element of REAL
((n `1) - (f `1)) * ((n `1) - (f `1)) is V22() real ext-real set
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
(n `2) - (f `2) is V22() real ext-real Element of REAL
((n `2) - (f `2)) ^2 is V22() real ext-real Element of REAL
((n `2) - (f `2)) * ((n `2) - (f `2)) is V22() real ext-real set
(((n `1) - (f `1)) ^2) + (((n `2) - (f `2)) ^2) is V22() real ext-real Element of REAL
sqrt ((((n `1) - (f `1)) ^2) + (((n `2) - (f `2)) ^2)) is V22() real ext-real Element of REAL
q is Element of the carrier of (Euclid 2)
r is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (q,r) is set
|[(n `1),(n `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
<*(f `1),(f `2)*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
u is Relation-like NAT -defined REAL -valued Function-like V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL 2
v is Relation-like NAT -defined REAL -valued Function-like V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL 2
u - v is Relation-like NAT -defined REAL -valued Function-like V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL 2
K211(diffreal,u,v) is set
K355(v) is Relation-like Function-like complex-yielding set
v * K173() is Relation-like complex-yielding V128() V129() set
- 1 is V22() real ext-real non positive set
(- 1) * v is Relation-like Function-like set
(- 1) multreal is Relation-like REAL -defined REAL -valued Function-like V30( REAL , REAL ) complex-yielding V128() V129() Element of K19(K20(REAL,REAL))
K177() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V30(K20(REAL,REAL), REAL ) complex-yielding V128() V129() Element of K19(K20(K20(REAL,REAL),REAL))
K213(K177(),(- 1),(id REAL)) is set
v * ((- 1) multreal) is Relation-like complex-yielding V128() V129() set
K326(u,K355(v)) is Relation-like Function-like set
diffreal . ((n `1),(f `1)) is V22() real ext-real Element of REAL
diffreal . ((n `2),(f `2)) is V22() real ext-real Element of REAL
<*(diffreal . ((n `1),(f `1))),(diffreal . ((n `2),(f `2)))*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
<*((n `1) - (f `1)),(diffreal . ((n `2),(f `2)))*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
<*((n `1) - (f `1)),((n `2) - (f `2))*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
abs (u - v) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of 2 -tuples_on REAL
(u - v) * absreal is Relation-like complex-yielding V128() V129() set
absreal . ((n `1) - (f `1)) is V22() real ext-real set
absreal . ((n `2) - (f `2)) is V22() real ext-real set
<*(absreal . ((n `1) - (f `1))),(absreal . ((n `2) - (f `2)))*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
abs ((n `1) - (f `1)) is V22() real ext-real Element of REAL
<*(abs ((n `1) - (f `1))),(absreal . ((n `2) - (f `2)))*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
abs ((n `2) - (f `2)) is V22() real ext-real Element of REAL
<*(abs ((n `1) - (f `1))),(abs ((n `2) - (f `2)))*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
sqr (abs (u - v)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of 2 -tuples_on REAL
(abs (u - v)) * sqrreal is Relation-like complex-yielding V128() V129() set
mlt ((abs (u - v)),(abs (u - v))) is Relation-like Function-like set
K211(K177(),(abs (u - v)),(abs (u - v))) is set
sqrreal . (abs ((n `1) - (f `1))) is V22() real ext-real set
sqrreal . (abs ((n `2) - (f `2))) is V22() real ext-real set
<*(sqrreal . (abs ((n `1) - (f `1)))),(sqrreal . (abs ((n `2) - (f `2))))*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
(abs ((n `1) - (f `1))) ^2 is V22() real ext-real Element of REAL
(abs ((n `1) - (f `1))) * (abs ((n `1) - (f `1))) is V22() real ext-real set
<*((abs ((n `1) - (f `1))) ^2),(sqrreal . (abs ((n `2) - (f `2))))*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
(abs ((n `2) - (f `2))) ^2 is V22() real ext-real Element of REAL
(abs ((n `2) - (f `2))) * (abs ((n `2) - (f `2))) is V22() real ext-real set
<*((abs ((n `1) - (f `1))) ^2),((abs ((n `2) - (f `2))) ^2)*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
<*(((n `1) - (f `1)) ^2),((abs ((n `2) - (f `2))) ^2)*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
<*(((n `1) - (f `1)) ^2),(((n `2) - (f `2)) ^2)*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
|.(u - v).| is V22() real ext-real non negative Element of REAL
sqr (u - v) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
(u - v) * sqrreal is Relation-like complex-yielding V128() V129() set
mlt ((u - v),(u - v)) is Relation-like Function-like set
K211(K177(),(u - v),(u - v)) is set
Sum (sqr (u - v)) is V22() real ext-real Element of REAL
sqrt (Sum (sqr (u - v))) is V22() real ext-real Element of REAL
Sum (sqr (abs (u - v))) is V22() real ext-real Element of REAL
sqrt (Sum (sqr (abs (u - v)))) is V22() real ext-real Element of REAL
n is ordinal natural V22() real ext-real non negative set
TOP-REAL n is non empty TopSpace-like V103() V149() V150() V151() V152() V153() V154() V155() strict RLTopStruct
the carrier of (TOP-REAL n) is non empty set
Euclid n is non empty strict Reflexive discerning V86() triangle MetrStruct
REAL n is functional non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist n is Relation-like K20((REAL n),(REAL n)) -defined REAL -valued Function-like V30(K20((REAL n),(REAL n)), REAL ) complex-yielding V128() V129() Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is set
K20(K20((REAL n),(REAL n)),REAL) is complex-yielding V128() V129() set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
n is V22() real ext-real set
f is V22() real ext-real set
q is V22() real ext-real set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = q & n <= b<sub>1</sub> `2 & b₁ `2 <= f ) } is set
|[q,n]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[q,f]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (|[q,n]|,|[q,f]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * |[q,n]|) + (b<sub>1</sub> * |[q,f]|)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
|[q,n]| `1 is V22() real ext-real Element of REAL
K434(|[q,n]|,1) is V22() real ext-real Element of REAL
n - n is V22() real ext-real set
f - n is V22() real ext-real set
|[q,f]| `2 is V22() real ext-real Element of REAL
K434(|[q,f]|,2) is V22() real ext-real Element of REAL
|[q,n]| `2 is V22() real ext-real Element of REAL
K434(|[q,n]|,2) is V22() real ext-real Element of REAL
|[q,f]| `1 is V22() real ext-real Element of REAL
K434(|[q,f]|,1) is V22() real ext-real Element of REAL
{|[q,n]|} is non empty set
x is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
x is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
(qp `2) - n is V22() real ext-real Element of REAL
((qp `2) - n) / (f - n) is V22() real ext-real Element of REAL
1 - (((qp `2) - n) / (f - n)) is V22() real ext-real Element of REAL
1 * (f - n) is V22() real ext-real Element of REAL
(1 * (f - n)) - ((qp `2) - n) is V22() real ext-real Element of REAL
((1 * (f - n)) - ((qp `2) - n)) / (f - n) is V22() real ext-real Element of REAL
f - (qp `2) is V22() real ext-real Element of REAL
(f - (qp `2)) / (f - n) is V22() real ext-real Element of REAL
(f - n) / (f - n) is V22() real ext-real Element of COMPLEX
(1 - (((qp `2) - n) / (f - n))) * |[q,n]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(((qp `2) - n) / (f - n)) * |[q,f]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - (((qp `2) - n) / (f - n))) * |[q,n]|) + ((((qp `2) - n) / (f - n)) * |[q,f]|) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (((1 - (((qp `2) - n) / (f - n))) * |[q,n]|),((((qp `2) - n) / (f - n)) * |[q,f]|)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(((1 - (((qp `2) - n) / (f - n))) * |[q,n]|) + ((((qp `2) - n) / (f - n)) * |[q,f]|)) `1 is V22() real ext-real Element of REAL
K434((((1 - (((qp `2) - n) / (f - n))) * |[q,n]|) + ((((qp `2) - n) / (f - n)) * |[q,f]|)),1) is V22() real ext-real Element of REAL
((1 - (((qp `2) - n) / (f - n))) * |[q,n]|) `1 is V22() real ext-real Element of REAL
K434(((1 - (((qp `2) - n) / (f - n))) * |[q,n]|),1) is V22() real ext-real Element of REAL
((((qp `2) - n) / (f - n)) * |[q,f]|) `1 is V22() real ext-real Element of REAL
K434(((((qp `2) - n) / (f - n)) * |[q,f]|),1) is V22() real ext-real Element of REAL
(((1 - (((qp `2) - n) / (f - n))) * |[q,n]|) `1) + (((((qp `2) - n) / (f - n)) * |[q,f]|) `1) is V22() real ext-real Element of REAL
(1 - (((qp `2) - n) / (f - n))) * (|[q,n]| `1) is V22() real ext-real Element of REAL
((1 - (((qp `2) - n) / (f - n))) * (|[q,n]| `1)) + (((((qp `2) - n) / (f - n)) * |[q,f]|) `1) is V22() real ext-real Element of REAL
(1 - (((qp `2) - n) / (f - n))) * q is V22() real ext-real Element of REAL
(((qp `2) - n) / (f - n)) * q is V22() real ext-real Element of REAL
((1 - (((qp `2) - n) / (f - n))) * q) + ((((qp `2) - n) / (f - n)) * q) is V22() real ext-real Element of REAL
(((1 - (((qp `2) - n) / (f - n))) * |[q,n]|) + ((((qp `2) - n) / (f - n)) * |[q,f]|)) `2 is V22() real ext-real Element of REAL
K434((((1 - (((qp `2) - n) / (f - n))) * |[q,n]|) + ((((qp `2) - n) / (f - n)) * |[q,f]|)),2) is V22() real ext-real Element of REAL
((1 - (((qp `2) - n) / (f - n))) * |[q,n]|) `2 is V22() real ext-real Element of REAL
K434(((1 - (((qp `2) - n) / (f - n))) * |[q,n]|),2) is V22() real ext-real Element of REAL
((((qp `2) - n) / (f - n)) * |[q,f]|) `2 is V22() real ext-real Element of REAL
K434(((((qp `2) - n) / (f - n)) * |[q,f]|),2) is V22() real ext-real Element of REAL
(((1 - (((qp `2) - n) / (f - n))) * |[q,n]|) `2) + (((((qp `2) - n) / (f - n)) * |[q,f]|) `2) is V22() real ext-real Element of REAL
(1 - (((qp `2) - n) / (f - n))) * (|[q,n]| `2) is V22() real ext-real Element of REAL
((1 - (((qp `2) - n) / (f - n))) * (|[q,n]| `2)) + (((((qp `2) - n) / (f - n)) * |[q,f]|) `2) is V22() real ext-real Element of REAL
(((qp `2) - n) / (f - n)) * (|[q,f]| `2) is V22() real ext-real Element of REAL
((1 - (((qp `2) - n) / (f - n))) * (|[q,n]| `2)) + ((((qp `2) - n) / (f - n)) * (|[q,f]| `2)) is V22() real ext-real Element of REAL
(f - (qp `2)) * (|[q,n]| `2) is V22() real ext-real Element of REAL
((f - (qp `2)) * (|[q,n]| `2)) / (f - n) is V22() real ext-real Element of REAL
(((f - (qp `2)) * (|[q,n]| `2)) / (f - n)) + ((((qp `2) - n) / (f - n)) * (|[q,f]| `2)) is V22() real ext-real Element of REAL
((qp `2) - n) * (|[q,f]| `2) is V22() real ext-real Element of REAL
(((qp `2) - n) * (|[q,f]| `2)) / (f - n) is V22() real ext-real Element of REAL
(((f - (qp `2)) * (|[q,n]| `2)) / (f - n)) + ((((qp `2) - n) * (|[q,f]| `2)) / (f - n)) is V22() real ext-real Element of REAL
f * n is V22() real ext-real set
(qp `2) * n is V22() real ext-real Element of REAL
(f * n) - ((qp `2) * n) is V22() real ext-real Element of REAL
((qp `2) - n) * f is V22() real ext-real Element of REAL
((f * n) - ((qp `2) * n)) + (((qp `2) - n) * f) is V22() real ext-real Element of REAL
(((f * n) - ((qp `2) * n)) + (((qp `2) - n) * f)) / (f - n) is V22() real ext-real Element of REAL
(qp `2) * (f - n) is V22() real ext-real Element of REAL
((qp `2) * (f - n)) / (f - n) is V22() real ext-real Element of REAL
(qp `2) * ((f - n) / (f - n)) is V22() real ext-real Element of REAL
(qp `2) * 1 is V22() real ext-real Element of REAL
x is set
qp is V22() real ext-real Element of REAL
1 - qp is V22() real ext-real Element of REAL
(1 - qp) * |[q,n]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp * |[q,f]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - qp) * |[q,n]|) + (qp * |[q,f]|) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (((1 - qp) * |[q,n]|),(qp * |[q,f]|)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n + 0 is V22() real ext-real Element of REAL
qp * (f - n) is V22() real ext-real Element of REAL
n + (qp * (f - n)) is V22() real ext-real Element of REAL
1 * (f - n) is V22() real ext-real Element of REAL
(f - n) + n is V22() real ext-real set
(((1 - qp) * |[q,n]|) + (qp * |[q,f]|)) `2 is V22() real ext-real Element of REAL
K434((((1 - qp) * |[q,n]|) + (qp * |[q,f]|)),2) is V22() real ext-real Element of REAL
((1 - qp) * |[q,n]|) `2 is V22() real ext-real Element of REAL
K434(((1 - qp) * |[q,n]|),2) is V22() real ext-real Element of REAL
(qp * |[q,f]|) `2 is V22() real ext-real Element of REAL
K434((qp * |[q,f]|),2) is V22() real ext-real Element of REAL
(((1 - qp) * |[q,n]|) `2) + ((qp * |[q,f]|) `2) is V22() real ext-real Element of REAL
(1 - qp) * (|[q,n]| `2) is V22() real ext-real Element of REAL
((1 - qp) * (|[q,n]| `2)) + ((qp * |[q,f]|) `2) is V22() real ext-real Element of REAL
1 * n is V22() real ext-real Element of REAL
qp * n is V22() real ext-real Element of REAL
(1 * n) - (qp * n) is V22() real ext-real Element of REAL
qp * f is V22() real ext-real Element of REAL
((1 * n) - (qp * n)) + (qp * f) is V22() real ext-real Element of REAL
(((1 - qp) * |[q,n]|) + (qp * |[q,f]|)) `1 is V22() real ext-real Element of REAL
K434((((1 - qp) * |[q,n]|) + (qp * |[q,f]|)),1) is V22() real ext-real Element of REAL
((1 - qp) * |[q,n]|) `1 is V22() real ext-real Element of REAL
K434(((1 - qp) * |[q,n]|),1) is V22() real ext-real Element of REAL
(qp * |[q,f]|) `1 is V22() real ext-real Element of REAL
K434((qp * |[q,f]|),1) is V22() real ext-real Element of REAL
(((1 - qp) * |[q,n]|) `1) + ((qp * |[q,f]|) `1) is V22() real ext-real Element of REAL
(1 - qp) * (|[q,n]| `1) is V22() real ext-real Element of REAL
((1 - qp) * (|[q,n]| `1)) + ((qp * |[q,f]|) `1) is V22() real ext-real Element of REAL
(1 - qp) * q is V22() real ext-real Element of REAL
qp * q is V22() real ext-real Element of REAL
((1 - qp) * q) + (qp * q) is V22() real ext-real Element of REAL
1 * q is V22() real ext-real Element of REAL
n is V22() real ext-real set
f is V22() real ext-real set
q is V22() real ext-real set
{ b<sub>1</sub> where b<sub>1</sub> is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `2 = q & n <= b₁ `1 & b<sub>1</sub> `1 <= f ) } is set
|[n,q]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[f,q]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (|[n,q]|,|[f,q]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[n,q]|) + (b₁ * |[f,q]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
|[n,q]| `1 is V22() real ext-real Element of REAL
K434(|[n,q]|,1) is V22() real ext-real Element of REAL
n - n is V22() real ext-real set
f - n is V22() real ext-real set
|[f,q]| `2 is V22() real ext-real Element of REAL
K434(|[f,q]|,2) is V22() real ext-real Element of REAL
|[n,q]| `2 is V22() real ext-real Element of REAL
K434(|[n,q]|,2) is V22() real ext-real Element of REAL
|[f,q]| `1 is V22() real ext-real Element of REAL
K434(|[f,q]|,1) is V22() real ext-real Element of REAL
{|[n,q]|} is non empty set
x is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
x is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
(qp `1) - n is V22() real ext-real Element of REAL
((qp `1) - n) / (f - n) is V22() real ext-real Element of REAL
1 - (((qp `1) - n) / (f - n)) is V22() real ext-real Element of REAL
1 * (f - n) is V22() real ext-real Element of REAL
(1 * (f - n)) - ((qp `1) - n) is V22() real ext-real Element of REAL
((1 * (f - n)) - ((qp `1) - n)) / (f - n) is V22() real ext-real Element of REAL
f - (qp `1) is V22() real ext-real Element of REAL
(f - (qp `1)) / (f - n) is V22() real ext-real Element of REAL
(f - n) / (f - n) is V22() real ext-real Element of COMPLEX
(1 - (((qp `1) - n) / (f - n))) * |[n,q]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(((qp `1) - n) / (f - n)) * |[f,q]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - (((qp `1) - n) / (f - n))) * |[n,q]|) + ((((qp `1) - n) / (f - n)) * |[f,q]|) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (((1 - (((qp `1) - n) / (f - n))) * |[n,q]|),((((qp `1) - n) / (f - n)) * |[f,q]|)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(((1 - (((qp `1) - n) / (f - n))) * |[n,q]|) + ((((qp `1) - n) / (f - n)) * |[f,q]|)) `2 is V22() real ext-real Element of REAL
K434((((1 - (((qp `1) - n) / (f - n))) * |[n,q]|) + ((((qp `1) - n) / (f - n)) * |[f,q]|)),2) is V22() real ext-real Element of REAL
((1 - (((qp `1) - n) / (f - n))) * |[n,q]|) `2 is V22() real ext-real Element of REAL
K434(((1 - (((qp `1) - n) / (f - n))) * |[n,q]|),2) is V22() real ext-real Element of REAL
((((qp `1) - n) / (f - n)) * |[f,q]|) `2 is V22() real ext-real Element of REAL
K434(((((qp `1) - n) / (f - n)) * |[f,q]|),2) is V22() real ext-real Element of REAL
(((1 - (((qp `1) - n) / (f - n))) * |[n,q]|) `2) + (((((qp `1) - n) / (f - n)) * |[f,q]|) `2) is V22() real ext-real Element of REAL
(1 - (((qp `1) - n) / (f - n))) * (|[n,q]| `2) is V22() real ext-real Element of REAL
((1 - (((qp `1) - n) / (f - n))) * (|[n,q]| `2)) + (((((qp `1) - n) / (f - n)) * |[f,q]|) `2) is V22() real ext-real Element of REAL
(1 - (((qp `1) - n) / (f - n))) * q is V22() real ext-real Element of REAL
(((qp `1) - n) / (f - n)) * q is V22() real ext-real Element of REAL
((1 - (((qp `1) - n) / (f - n))) * q) + ((((qp `1) - n) / (f - n)) * q) is V22() real ext-real Element of REAL
(((1 - (((qp `1) - n) / (f - n))) * |[n,q]|) + ((((qp `1) - n) / (f - n)) * |[f,q]|)) `1 is V22() real ext-real Element of REAL
K434((((1 - (((qp `1) - n) / (f - n))) * |[n,q]|) + ((((qp `1) - n) / (f - n)) * |[f,q]|)),1) is V22() real ext-real Element of REAL
((1 - (((qp `1) - n) / (f - n))) * |[n,q]|) `1 is V22() real ext-real Element of REAL
K434(((1 - (((qp `1) - n) / (f - n))) * |[n,q]|),1) is V22() real ext-real Element of REAL
((((qp `1) - n) / (f - n)) * |[f,q]|) `1 is V22() real ext-real Element of REAL
K434(((((qp `1) - n) / (f - n)) * |[f,q]|),1) is V22() real ext-real Element of REAL
(((1 - (((qp `1) - n) / (f - n))) * |[n,q]|) `1) + (((((qp `1) - n) / (f - n)) * |[f,q]|) `1) is V22() real ext-real Element of REAL
(1 - (((qp `1) - n) / (f - n))) * (|[n,q]| `1) is V22() real ext-real Element of REAL
((1 - (((qp `1) - n) / (f - n))) * (|[n,q]| `1)) + (((((qp `1) - n) / (f - n)) * |[f,q]|) `1) is V22() real ext-real Element of REAL
(((qp `1) - n) / (f - n)) * (|[f,q]| `1) is V22() real ext-real Element of REAL
((1 - (((qp `1) - n) / (f - n))) * (|[n,q]| `1)) + ((((qp `1) - n) / (f - n)) * (|[f,q]| `1)) is V22() real ext-real Element of REAL
(f - (qp `1)) * (|[n,q]| `1) is V22() real ext-real Element of REAL
((f - (qp `1)) * (|[n,q]| `1)) / (f - n) is V22() real ext-real Element of REAL
(((f - (qp `1)) * (|[n,q]| `1)) / (f - n)) + ((((qp `1) - n) / (f - n)) * (|[f,q]| `1)) is V22() real ext-real Element of REAL
((qp `1) - n) * (|[f,q]| `1) is V22() real ext-real Element of REAL
(((qp `1) - n) * (|[f,q]| `1)) / (f - n) is V22() real ext-real Element of REAL
(((f - (qp `1)) * (|[n,q]| `1)) / (f - n)) + ((((qp `1) - n) * (|[f,q]| `1)) / (f - n)) is V22() real ext-real Element of REAL
f * n is V22() real ext-real set
(qp `1) * n is V22() real ext-real Element of REAL
(f * n) - ((qp `1) * n) is V22() real ext-real Element of REAL
((qp `1) - n) * f is V22() real ext-real Element of REAL
((f * n) - ((qp `1) * n)) + (((qp `1) - n) * f) is V22() real ext-real Element of REAL
(((f * n) - ((qp `1) * n)) + (((qp `1) - n) * f)) / (f - n) is V22() real ext-real Element of REAL
(qp `1) * (f - n) is V22() real ext-real Element of REAL
((qp `1) * (f - n)) / (f - n) is V22() real ext-real Element of REAL
(qp `1) * ((f - n) / (f - n)) is V22() real ext-real Element of REAL
(qp `1) * 1 is V22() real ext-real Element of REAL
x is set
qp is V22() real ext-real Element of REAL
1 - qp is V22() real ext-real Element of REAL
(1 - qp) * |[n,q]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp * |[f,q]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - qp) * |[n,q]|) + (qp * |[f,q]|) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (((1 - qp) * |[n,q]|),(qp * |[f,q]|)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n + 0 is V22() real ext-real Element of REAL
qp * (f - n) is V22() real ext-real Element of REAL
n + (qp * (f - n)) is V22() real ext-real Element of REAL
1 * (f - n) is V22() real ext-real Element of REAL
(f - n) + n is V22() real ext-real set
(((1 - qp) * |[n,q]|) + (qp * |[f,q]|)) `1 is V22() real ext-real Element of REAL
K434((((1 - qp) * |[n,q]|) + (qp * |[f,q]|)),1) is V22() real ext-real Element of REAL
((1 - qp) * |[n,q]|) `1 is V22() real ext-real Element of REAL
K434(((1 - qp) * |[n,q]|),1) is V22() real ext-real Element of REAL
(qp * |[f,q]|) `1 is V22() real ext-real Element of REAL
K434((qp * |[f,q]|),1) is V22() real ext-real Element of REAL
(((1 - qp) * |[n,q]|) `1) + ((qp * |[f,q]|) `1) is V22() real ext-real Element of REAL
(1 - qp) * (|[n,q]| `1) is V22() real ext-real Element of REAL
((1 - qp) * (|[n,q]| `1)) + ((qp * |[f,q]|) `1) is V22() real ext-real Element of REAL
1 * n is V22() real ext-real Element of REAL
qp * n is V22() real ext-real Element of REAL
(1 * n) - (qp * n) is V22() real ext-real Element of REAL
qp * f is V22() real ext-real Element of REAL
((1 * n) - (qp * n)) + (qp * f) is V22() real ext-real Element of REAL
(((1 - qp) * |[n,q]|) + (qp * |[f,q]|)) `2 is V22() real ext-real Element of REAL
K434((((1 - qp) * |[n,q]|) + (qp * |[f,q]|)),2) is V22() real ext-real Element of REAL
((1 - qp) * |[n,q]|) `2 is V22() real ext-real Element of REAL
K434(((1 - qp) * |[n,q]|),2) is V22() real ext-real Element of REAL
(qp * |[f,q]|) `2 is V22() real ext-real Element of REAL
K434((qp * |[f,q]|),2) is V22() real ext-real Element of REAL
(((1 - qp) * |[n,q]|) `2) + ((qp * |[f,q]|) `2) is V22() real ext-real Element of REAL
(1 - qp) * (|[n,q]| `2) is V22() real ext-real Element of REAL
((1 - qp) * (|[n,q]| `2)) + ((qp * |[f,q]|) `2) is V22() real ext-real Element of REAL
(1 - qp) * q is V22() real ext-real Element of REAL
qp * q is V22() real ext-real Element of REAL
((1 - qp) * q) + (qp * q) is V22() real ext-real Element of REAL
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
f is V22() real ext-real set
q is V22() real ext-real set
|[f,q]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
r is V22() real ext-real set
|[f,r]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (|[f,q]|,|[f,r]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * |[f,q]|) + (b<sub>1</sub> * |[f,r]|)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
{ b<sub>1</sub> where b<sub>1</sub> is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = f & q <= b₁ `2 & b<sub>1</sub> `2 <= r ) } is set
u is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
u `1 is V22() real ext-real Element of REAL
K434(u,1) is V22() real ext-real Element of REAL
u `2 is V22() real ext-real Element of REAL
K434(u,2) is V22() real ext-real Element of REAL
{|[f,q]|} is non empty set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f & r <= b<sub>1</sub> `2 & b₁ `2 <= q ) } is set
u is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
u `1 is V22() real ext-real Element of REAL
K434(u,1) is V22() real ext-real Element of REAL
u `2 is V22() real ext-real Element of REAL
K434(u,2) is V22() real ext-real Element of REAL
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V22() real ext-real set
q is V22() real ext-real set
|[f,q]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
r is V22() real ext-real set
|[r,q]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (|[f,q]|,|[r,q]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[f,q]|) + (b₁ * |[r,q]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = q & f <= b<sub>1</sub> `1 & b₁ `1 <= r ) } is set
u is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
u `2 is V22() real ext-real Element of REAL
K434(u,2) is V22() real ext-real Element of REAL
u `1 is V22() real ext-real Element of REAL
K434(u,1) is V22() real ext-real Element of REAL
{|[f,q]|} is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `2 = q & r <= b₁ `1 & b<sub>1</sub> `1 <= f ) } is set
u is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
u `2 is V22() real ext-real Element of REAL
K434(u,2) is V22() real ext-real Element of REAL
u `1 is V22() real ext-real Element of REAL
K434(u,1) is V22() real ext-real Element of REAL
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
(n `1) + (f `1) is V22() real ext-real Element of REAL
((n `1) + (f `1)) / 2 is V22() real ext-real Element of REAL
|[(((n `1) + (f `1)) / 2),(n `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (n,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * n) + (b<sub>1</sub> * f)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
|[(n `1),(n `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[(f `1),(n `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[(((n `1) + (f `1)) / 2),(n `2)]| `1 is V22() real ext-real Element of REAL
K434(|[(((n `1) + (f `1)) / 2),(n `2)]|,1) is V22() real ext-real Element of REAL
|[(((n `1) + (f `1)) / 2),(n `2)]| `2 is V22() real ext-real Element of REAL
K434(|[(((n `1) + (f `1)) / 2),(n `2)]|,2) is V22() real ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `2 = n `2 & n `1 <= b₁ `1 & b<sub>1</sub> `1 <= f `1 ) } is set
{ b<sub>1</sub> where b<sub>1</sub> is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `2 = n `2 & f `1 <= b₁ `1 & b<sub>1</sub> `1 <= n `1 ) } is set
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
(n `2) + (f `2) is V22() real ext-real Element of REAL
((n `2) + (f `2)) / 2 is V22() real ext-real Element of REAL
|[(n `1),(((n `2) + (f `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (n,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
|[(n `1),(n `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[(n `1),(f `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[(n `1),(((n `2) + (f `2)) / 2)]| `1 is V22() real ext-real Element of REAL
K434(|[(n `1),(((n `2) + (f `2)) / 2)]|,1) is V22() real ext-real Element of REAL
|[(n `1),(((n `2) + (f `2)) / 2)]| `2 is V22() real ext-real Element of REAL
K434(|[(n `1),(((n `2) + (f `2)) / 2)]|,2) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = n `1 & n `2 <= b<sub>1</sub> `2 & b₁ `2 <= f `2 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = n `1 & f `2 <= b<sub>1</sub> `2 & b₁ `2 <= n `2 ) } is set
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
<*n,f,q*> is Relation-like NAT -defined Function-like non empty V37() V44(3) FinSequence-like FinSubsequence-like set
r is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
u is ordinal natural V22() real ext-real non negative set
v is ordinal natural V22() real ext-real non negative set
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (r,v) is Element of K19( the carrier of (TOP-REAL 2))
0 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
1 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
1 + u is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
2 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
v + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
len r is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
LSeg (n,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
<*n,f,q*> is Relation-like NAT -defined Function-like non empty V37() V44(3) FinSequence-like FinSubsequence-like set
LSeg (f,q) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * f) + (b₁ * q)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (n,f)) \/ (LSeg (f,q)) is Element of K19( the carrier of (TOP-REAL 2))
r is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ r is Element of K19( the carrier of (TOP-REAL 2))
len r is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
{ (LSeg (r,b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len r ) } is set
union { (LSeg (r,b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len r ) } is set
2 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
r /. 3 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
r /. 1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
r /. 2 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
1 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
dom r is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
{(LSeg (n,f)),(LSeg (f,q))} is non empty set
v is set
x is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (r,x) is Element of K19( the carrier of (TOP-REAL 2))
x + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
v is set
LSeg (r,1) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (r,2) is Element of K19( the carrier of (TOP-REAL 2))
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
f + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (n,f) is Element of K19( the carrier of (TOP-REAL 2))
q is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n | q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom (n | q) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
LSeg ((n | q),f) is Element of K19( the carrier of (TOP-REAL 2))
len (n | q) is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
(n | q) /. f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(n | q) /. (f + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
Seg q is V37() V44(q) V137() V138() V139() V140() V141() V142() Element of K19(NAT)
n | (Seg q) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
dom n is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
(dom n) /\ (Seg q) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
len n is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n /. f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n /. (f + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
LSeg (((n | q) /. f),((n | q) /. (f + 1))) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * ((n | q) /. f)) + (b₁ * ((n | q) /. (f + 1)))) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom n is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
n ^ f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg ((n ^ f),q) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (n,q) is Element of K19( the carrier of (TOP-REAL 2))
len n is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
dom (n ^ f) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
len (n ^ f) is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n /. q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n /. (q + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(n ^ f) /. q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(n ^ f) /. (q + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
LSeg ((n /. q),(n /. (q + 1))) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (n /. q)) + (b₁ * (n /. (q + 1)))) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
n is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
TOP-REAL n is non empty TopSpace-like V103() V149() V150() V151() V152() V153() V154() V155() strict RLTopStruct
the carrier of (TOP-REAL n) is non empty set
f is Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL n)
L~ f is Element of K19( the carrier of (TOP-REAL n))
K19( the carrier of (TOP-REAL n)) is set
len f is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
{ (LSeg (f,b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
union { (LSeg (f,b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
q is ordinal natural V22() real ext-real non negative set
LSeg (f,q) is Element of K19( the carrier of (TOP-REAL n))
r is set
q + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ n is Element of K19( the carrier of (TOP-REAL 2))
len n is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
{ (LSeg (n,b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len n ) } is set
union { (LSeg (n,b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len n ) } is set
f is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n | f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (n | f) is Element of K19( the carrier of (TOP-REAL 2))
len (n | f) is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
{ (LSeg ((n | f),b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (n | f) ) } is set
union { (LSeg ((n | f),b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (n | f) ) } is set
v is set
Seg f is V37() V44(f) V137() V138() V139() V140() V141() V142() Element of K19(NAT)
n | (Seg f) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
dom n is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
Seg (len n) is V37() V44( len n) V137() V138() V139() V140() V141() V142() Element of K19(NAT)
x is set
qp is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg ((n | f),qp) is Element of K19( the carrier of (TOP-REAL 2))
qp + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
dom (n | f) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
(dom n) /\ (Seg f) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
LSeg (n,qp) is Element of K19( the carrier of (TOP-REAL 2))
0 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
dom (n | f) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
(dom n) /\ {} is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
Seg (len (n | f)) is V37() V44( len (n | f)) V137() V138() V139() V140() V141() V142() Element of K19(NAT)
(dom n) /\ (Seg f) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
dom (n | f) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
pp1 is set
(n | f) . pp1 is set
n . pp1 is set
n is V22() real ext-real set
f is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
TOP-REAL f is non empty TopSpace-like V103() V149() V150() V151() V152() V153() V154() V155() strict RLTopStruct
the carrier of (TOP-REAL f) is non empty set
Euclid f is non empty strict Reflexive discerning V86() triangle MetrStruct
REAL f is functional non empty FinSequence-membered FinSequenceSet of REAL
f -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist f is Relation-like K20((REAL f),(REAL f)) -defined REAL -valued Function-like V30(K20((REAL f),(REAL f)), REAL ) complex-yielding V128() V129() Element of K19(K20(K20((REAL f),(REAL f)),REAL))
K20((REAL f),(REAL f)) is set
K20(K20((REAL f),(REAL f)),REAL) is complex-yielding V128() V129() set
K19(K20(K20((REAL f),(REAL f)),REAL)) is set
MetrStruct(# (REAL f),(Pitag_dist f) #) is strict MetrStruct
the carrier of (Euclid f) is non empty set
q is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
r is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
LSeg (q,r) is Element of K19( the carrier of (TOP-REAL f))
K19( the carrier of (TOP-REAL f)) is set
{ (((1 - b₁) * q) + (b₁ * r)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
u is Element of the carrier of (Euclid f)
Ball (u,n) is Element of K19( the carrier of (Euclid f))
K19( the carrier of (Euclid f)) is set
v is Element of the carrier of (Euclid f)
dist (v,u) is V22() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of (Euclid f) : not n <= dist (u,b₁) } is set
qp is set
x is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
p1p is V22() real ext-real Element of REAL
1 - p1p is V22() real ext-real Element of REAL
(1 - p1p) * q is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
p1p * r is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
((1 - p1p) * q) + (p1p * r) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) is Relation-like K20( the carrier of (TOP-REAL f), the carrier of (TOP-REAL f)) -defined the carrier of (TOP-REAL f) -valued Function-like V30(K20( the carrier of (TOP-REAL f), the carrier of (TOP-REAL f)), the carrier of (TOP-REAL f)) Element of K19(K20(K20( the carrier of (TOP-REAL f), the carrier of (TOP-REAL f)), the carrier of (TOP-REAL f)))
K20( the carrier of (TOP-REAL f), the carrier of (TOP-REAL f)) is set
K20(K20( the carrier of (TOP-REAL f), the carrier of (TOP-REAL f)), the carrier of (TOP-REAL f)) is set
K19(K20(K20( the carrier of (TOP-REAL f), the carrier of (TOP-REAL f)), the carrier of (TOP-REAL f))) is set
the U7 of (TOP-REAL f) . (((1 - p1p) * q),(p1p * r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
abs p1p is V22() real ext-real Element of REAL
p1q is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
(Pitag_dist f) . (x,p1q) is V22() real ext-real Element of REAL
x - p1q is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
K211(diffreal,x,p1q) is set
K355(p1q) is Relation-like Function-like complex-yielding set
p1q * K173() is Relation-like complex-yielding V128() V129() set
- 1 is V22() real ext-real non positive set
(- 1) * p1q is Relation-like Function-like set
(- 1) multreal is Relation-like REAL -defined REAL -valued Function-like V30( REAL , REAL ) complex-yielding V128() V129() Element of K19(K20(REAL,REAL))
K177() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V30(K20(REAL,REAL), REAL ) complex-yielding V128() V129() Element of K19(K20(K20(REAL,REAL),REAL))
K213(K177(),(- 1),(id REAL)) is set
p1q * ((- 1) multreal) is Relation-like complex-yielding V128() V129() set
K326(x,K355(p1q)) is Relation-like Function-like set
|.(x - p1q).| is V22() real ext-real non negative Element of REAL
sqr (x - p1q) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
(x - p1q) * sqrreal is Relation-like complex-yielding V128() V129() set
mlt ((x - p1q),(x - p1q)) is Relation-like Function-like set
K211(K177(),(x - p1q),(x - p1q)) is set
Sum (sqr (x - p1q)) is V22() real ext-real Element of REAL
sqrt (Sum (sqr (x - p1q))) is V22() real ext-real Element of REAL
u4 is Element of the carrier of (Euclid f)
(Pitag_dist f) . (u,u4) is set
dist (u,u4) is V22() real ext-real Element of REAL
u3 is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
(Pitag_dist f) . (x,u3) is V22() real ext-real Element of REAL
x - u3 is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
K211(diffreal,x,u3) is set
K355(u3) is Relation-like Function-like complex-yielding set
u3 * K173() is Relation-like complex-yielding V128() V129() set
(- 1) * u3 is Relation-like Function-like set
u3 * ((- 1) multreal) is Relation-like complex-yielding V128() V129() set
K326(x,K355(u3)) is Relation-like Function-like set
|.(x - u3).| is V22() real ext-real non negative Element of REAL
sqr (x - u3) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
(x - u3) * sqrreal is Relation-like complex-yielding V128() V129() set
mlt ((x - u3),(x - u3)) is Relation-like Function-like set
K211(K177(),(x - u3),(x - u3)) is set
Sum (sqr (x - u3)) is V22() real ext-real Element of REAL
sqrt (Sum (sqr (x - u3))) is V22() real ext-real Element of REAL
- u3 is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
x + (- u3) is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
K211(K175(),x,(- u3)) is set
|.(x + (- u3)).| is V22() real ext-real non negative Element of REAL
sqr (x + (- u3)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
(x + (- u3)) * sqrreal is Relation-like complex-yielding V128() V129() set
mlt ((x + (- u3)),(x + (- u3))) is Relation-like Function-like set
K211(K177(),(x + (- u3)),(x + (- u3))) is set
Sum (sqr (x + (- u3))) is V22() real ext-real Element of REAL
sqrt (Sum (sqr (x + (- u3)))) is V22() real ext-real Element of REAL
a is Element of the carrier of (Euclid f)
dist (u,a) is V22() real ext-real Element of REAL
abs (1 - p1p) is V22() real ext-real Element of REAL
a is Element of the carrier of (Euclid f)
dist (u,a) is V22() real ext-real Element of REAL
u2 is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
(Pitag_dist f) . (x,u2) is V22() real ext-real Element of REAL
x - u2 is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
K211(diffreal,x,u2) is set
K355(u2) is Relation-like Function-like complex-yielding set
u2 * K173() is Relation-like complex-yielding V128() V129() set
(- 1) * u2 is Relation-like Function-like set
u2 * ((- 1) multreal) is Relation-like complex-yielding V128() V129() set
K326(x,K355(u2)) is Relation-like Function-like set
|.(x - u2).| is V22() real ext-real non negative Element of REAL
sqr (x - u2) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
(x - u2) * sqrreal is Relation-like complex-yielding V128() V129() set
mlt ((x - u2),(x - u2)) is Relation-like Function-like set
K211(K177(),(x - u2),(x - u2)) is set
Sum (sqr (x - u2)) is V22() real ext-real Element of REAL
sqrt (Sum (sqr (x - u2))) is V22() real ext-real Element of REAL
(1 - p1p) * n is V22() real ext-real Element of REAL
- u2 is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
x + (- u2) is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
K211(K175(),x,(- u2)) is set
|.(x + (- u2)).| is V22() real ext-real non negative Element of REAL
sqr (x + (- u2)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
(x + (- u2)) * sqrreal is Relation-like complex-yielding V128() V129() set
mlt ((x + (- u2)),(x + (- u2))) is Relation-like Function-like set
K211(K177(),(x + (- u2)),(x + (- u2))) is set
Sum (sqr (x + (- u2))) is V22() real ext-real Element of REAL
sqrt (Sum (sqr (x + (- u2)))) is V22() real ext-real Element of REAL
(abs (1 - p1p)) * |.(x + (- u2)).| is V22() real ext-real Element of REAL
(abs p1p) * |.(x + (- u3)).| is V22() real ext-real Element of REAL
p1p * n is V22() real ext-real Element of REAL
((1 - p1p) * n) + (p1p * n) is V22() real ext-real Element of REAL
((abs (1 - p1p)) * |.(x + (- u2)).|) + ((abs p1p) * |.(x + (- u3)).|) is V22() real ext-real Element of REAL
pp1 is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
pp1 - q is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
- q is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
K312((TOP-REAL f),pp1,(- q)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . (pp1,(- q)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
pp1 - (((1 - p1p) * q) + (p1p * r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
- (((1 - p1p) * q) + (p1p * r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
K312((TOP-REAL f),pp1,(- (((1 - p1p) * q) + (p1p * r)))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . (pp1,(- (((1 - p1p) * q) + (p1p * r)))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(1 - p1p) * (x - u2) is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
(1 - p1p) multreal is Relation-like REAL -defined REAL -valued Function-like V30( REAL , REAL ) complex-yielding V128() V129() Element of K19(K20(REAL,REAL))
K213(K177(),(1 - p1p),(id REAL)) is set
(x - u2) * ((1 - p1p) multreal) is Relation-like complex-yielding V128() V129() set
(1 - p1p) * (pp1 - q) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
pp1 - r is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
- r is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
K312((TOP-REAL f),pp1,(- r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . (pp1,(- r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
p1p * (x - u3) is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
p1p multreal is Relation-like REAL -defined REAL -valued Function-like V30( REAL , REAL ) complex-yielding V128() V129() Element of K19(K20(REAL,REAL))
K213(K177(),p1p,(id REAL)) is set
(x - u3) * (p1p multreal) is Relation-like complex-yielding V128() V129() set
p1p * (pp1 - r) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(1 - p1p) + p1p is V22() real ext-real Element of REAL
((1 - p1p) + p1p) * pp1 is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(((1 - p1p) + p1p) * pp1) - (((1 - p1p) * q) + (p1p * r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
K312((TOP-REAL f),(((1 - p1p) + p1p) * pp1),(- (((1 - p1p) * q) + (p1p * r)))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . ((((1 - p1p) + p1p) * pp1),(- (((1 - p1p) * q) + (p1p * r)))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(1 - p1p) * pp1 is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
p1p * pp1 is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
((1 - p1p) * pp1) + (p1p * pp1) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . (((1 - p1p) * pp1),(p1p * pp1)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(((1 - p1p) * pp1) + (p1p * pp1)) - (((1 - p1p) * q) + (p1p * r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
K312((TOP-REAL f),(((1 - p1p) * pp1) + (p1p * pp1)),(- (((1 - p1p) * q) + (p1p * r)))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . ((((1 - p1p) * pp1) + (p1p * pp1)),(- (((1 - p1p) * q) + (p1p * r)))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(((1 - p1p) * pp1) + (p1p * pp1)) + (- (((1 - p1p) * q) + (p1p * r))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
- ((1 - p1p) * q) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(- ((1 - p1p) * q)) - (p1p * r) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
- (p1p * r) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
K312((TOP-REAL f),(- ((1 - p1p) * q)),(- (p1p * r))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . ((- ((1 - p1p) * q)),(- (p1p * r))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(((1 - p1p) * pp1) + (p1p * pp1)) + ((- ((1 - p1p) * q)) - (p1p * r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . ((((1 - p1p) * pp1) + (p1p * pp1)),((- ((1 - p1p) * q)) - (p1p * r))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(((1 - p1p) * pp1) + (p1p * pp1)) + (- ((1 - p1p) * q)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . ((((1 - p1p) * pp1) + (p1p * pp1)),(- ((1 - p1p) * q))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
((((1 - p1p) * pp1) + (p1p * pp1)) + (- ((1 - p1p) * q))) + (- (p1p * r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . (((((1 - p1p) * pp1) + (p1p * pp1)) + (- ((1 - p1p) * q))),(- (p1p * r))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
((1 - p1p) * pp1) + (- ((1 - p1p) * q)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . (((1 - p1p) * pp1),(- ((1 - p1p) * q))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(((1 - p1p) * pp1) + (- ((1 - p1p) * q))) + (p1p * pp1) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . ((((1 - p1p) * pp1) + (- ((1 - p1p) * q))),(p1p * pp1)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
((((1 - p1p) * pp1) + (- ((1 - p1p) * q))) + (p1p * pp1)) + (- (p1p * r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . (((((1 - p1p) * pp1) + (- ((1 - p1p) * q))) + (p1p * pp1)),(- (p1p * r))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(1 - p1p) * (- q) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
((1 - p1p) * pp1) + ((1 - p1p) * (- q)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . (((1 - p1p) * pp1),((1 - p1p) * (- q))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(((1 - p1p) * pp1) + ((1 - p1p) * (- q))) + (p1p * pp1) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . ((((1 - p1p) * pp1) + ((1 - p1p) * (- q))),(p1p * pp1)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
((((1 - p1p) * pp1) + ((1 - p1p) * (- q))) + (p1p * pp1)) + (- (p1p * r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . (((((1 - p1p) * pp1) + ((1 - p1p) * (- q))) + (p1p * pp1)),(- (p1p * r))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
pp1 + (- q) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(1 - p1p) * (pp1 + (- q)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
((1 - p1p) * (pp1 + (- q))) + (p1p * pp1) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . (((1 - p1p) * (pp1 + (- q))),(p1p * pp1)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(((1 - p1p) * (pp1 + (- q))) + (p1p * pp1)) + (- (p1p * r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . ((((1 - p1p) * (pp1 + (- q))) + (p1p * pp1)),(- (p1p * r))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(p1p * pp1) + (- (p1p * r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . ((p1p * pp1),(- (p1p * r))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
((1 - p1p) * (pp1 + (- q))) + ((p1p * pp1) + (- (p1p * r))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . (((1 - p1p) * (pp1 + (- q))),((p1p * pp1) + (- (p1p * r)))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
p1p * (- r) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
(p1p * pp1) + (p1p * (- r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . ((p1p * pp1),(p1p * (- r))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
((1 - p1p) * (pp1 + (- q))) + ((p1p * pp1) + (p1p * (- r))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . (((1 - p1p) * (pp1 + (- q))),((p1p * pp1) + (p1p * (- r)))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
((1 - p1p) * (pp1 - q)) + (p1p * (pp1 - r)) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
the U7 of (TOP-REAL f) . (((1 - p1p) * (pp1 - q)),(p1p * (pp1 - r))) is V44(f) FinSequence-like V129() Element of the carrier of (TOP-REAL f)
((1 - p1p) * (x - u2)) + (p1p * (x - u3)) is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
K211(K175(),((1 - p1p) * (x - u2)),(p1p * (x - u3))) is set
|.((1 - p1p) * (x - u2)).| is V22() real ext-real non negative Element of REAL
sqr ((1 - p1p) * (x - u2)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
((1 - p1p) * (x - u2)) * sqrreal is Relation-like complex-yielding V128() V129() set
mlt (((1 - p1p) * (x - u2)),((1 - p1p) * (x - u2))) is Relation-like Function-like set
K211(K177(),((1 - p1p) * (x - u2)),((1 - p1p) * (x - u2))) is set
Sum (sqr ((1 - p1p) * (x - u2))) is V22() real ext-real Element of REAL
sqrt (Sum (sqr ((1 - p1p) * (x - u2)))) is V22() real ext-real Element of REAL
|.(p1p * (x - u3)).| is V22() real ext-real non negative Element of REAL
sqr (p1p * (x - u3)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
(p1p * (x - u3)) * sqrreal is Relation-like complex-yielding V128() V129() set
mlt ((p1p * (x - u3)),(p1p * (x - u3))) is Relation-like Function-like set
K211(K177(),(p1p * (x - u3)),(p1p * (x - u3))) is set
Sum (sqr (p1p * (x - u3))) is V22() real ext-real Element of REAL
sqrt (Sum (sqr (p1p * (x - u3)))) is V22() real ext-real Element of REAL
|.((1 - p1p) * (x - u2)).| + |.(p1p * (x - u3)).| is V22() real ext-real non negative Element of REAL
(1 - p1p) * (x + (- u2)) is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
(x + (- u2)) * ((1 - p1p) multreal) is Relation-like complex-yielding V128() V129() set
|.((1 - p1p) * (x + (- u2))).| is V22() real ext-real non negative Element of REAL
sqr ((1 - p1p) * (x + (- u2))) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
((1 - p1p) * (x + (- u2))) * sqrreal is Relation-like complex-yielding V128() V129() set
mlt (((1 - p1p) * (x + (- u2))),((1 - p1p) * (x + (- u2)))) is Relation-like Function-like set
K211(K177(),((1 - p1p) * (x + (- u2))),((1 - p1p) * (x + (- u2)))) is set
Sum (sqr ((1 - p1p) * (x + (- u2)))) is V22() real ext-real Element of REAL
sqrt (Sum (sqr ((1 - p1p) * (x + (- u2))))) is V22() real ext-real Element of REAL
p1p * (x + (- u3)) is Relation-like NAT -defined REAL -valued Function-like V37() V44(f) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL f
(x + (- u3)) * (p1p multreal) is Relation-like complex-yielding V128() V129() set
|.(p1p * (x + (- u3))).| is V22() real ext-real non negative Element of REAL
sqr (p1p * (x + (- u3))) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
(p1p * (x + (- u3))) * sqrreal is Relation-like complex-yielding V128() V129() set
mlt ((p1p * (x + (- u3))),(p1p * (x + (- u3)))) is Relation-like Function-like set
K211(K177(),(p1p * (x + (- u3))),(p1p * (x + (- u3)))) is set
Sum (sqr (p1p * (x + (- u3)))) is V22() real ext-real Element of REAL
sqrt (Sum (sqr (p1p * (x + (- u3))))) is V22() real ext-real Element of REAL
|.((1 - p1p) * (x + (- u2))).| + |.(p1p * (x + (- u3))).| is V22() real ext-real non negative Element of REAL
((abs (1 - p1p)) * |.(x + (- u2)).|) + |.(p1p * (x + (- u3))).| is V22() real ext-real Element of REAL
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
r is V22() real ext-real set
u is V22() real ext-real set
|[r,u]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
v is V22() real ext-real set
|[v,u]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
x is V22() real ext-real set
|[v,x]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
qp is V22() real ext-real set
pp1 is Element of the carrier of (Euclid 2)
Ball (pp1,qp) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
p1p is Relation-like NAT -defined REAL -valued Function-like V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL 2
qp1 is Relation-like NAT -defined REAL -valued Function-like V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL 2
(Pitag_dist 2) . (p1p,qp1) is V22() real ext-real Element of REAL
p1p - qp1 is Relation-like NAT -defined REAL -valued Function-like V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL 2
K211(diffreal,p1p,qp1) is set
K355(qp1) is Relation-like Function-like complex-yielding set
qp1 * K173() is Relation-like complex-yielding V128() V129() set
- 1 is V22() real ext-real non positive set
(- 1) * qp1 is Relation-like Function-like set
(- 1) multreal is Relation-like REAL -defined REAL -valued Function-like V30( REAL , REAL ) complex-yielding V128() V129() Element of K19(K20(REAL,REAL))
K177() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V30(K20(REAL,REAL), REAL ) complex-yielding V128() V129() Element of K19(K20(K20(REAL,REAL),REAL))
K213(K177(),(- 1),(id REAL)) is set
qp1 * ((- 1) multreal) is Relation-like complex-yielding V128() V129() set
K326(p1p,K355(qp1)) is Relation-like Function-like set
|.(p1p - qp1).| is V22() real ext-real non negative Element of REAL
sqr (p1p - qp1) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
(p1p - qp1) * sqrreal is Relation-like complex-yielding V128() V129() set
mlt ((p1p - qp1),(p1p - qp1)) is Relation-like Function-like set
K211(K177(),(p1p - qp1),(p1p - qp1)) is set
Sum (sqr (p1p - qp1)) is V22() real ext-real Element of REAL
sqrt (Sum (sqr (p1p - qp1))) is V22() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of (Euclid 2) : not qp <= dist (pp1,b₁) } is set
b is Element of the carrier of (Euclid 2)
dist (pp1,b) is V22() real ext-real Element of REAL
p1q is Relation-like NAT -defined REAL -valued Function-like V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL 2
(Pitag_dist 2) . (p1p,p1q) is V22() real ext-real Element of REAL
p1p - p1q is Relation-like NAT -defined REAL -valued Function-like V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL 2
K211(diffreal,p1p,p1q) is set
K355(p1q) is Relation-like Function-like complex-yielding set
p1q * K173() is Relation-like complex-yielding V128() V129() set
(- 1) * p1q is Relation-like Function-like set
p1q * ((- 1) multreal) is Relation-like complex-yielding V128() V129() set
K326(p1p,K355(p1q)) is Relation-like Function-like set
|.(p1p - p1q).| is V22() real ext-real non negative Element of REAL
sqr (p1p - p1q) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
(p1p - p1q) * sqrreal is Relation-like complex-yielding V128() V129() set
mlt ((p1p - p1q),(p1p - p1q)) is Relation-like Function-like set
K211(K177(),(p1p - p1q),(p1p - p1q)) is set
Sum (sqr (p1p - p1q)) is V22() real ext-real Element of REAL
sqrt (Sum (sqr (p1p - p1q))) is V22() real ext-real Element of REAL
b is Element of the carrier of (Euclid 2)
dist (pp1,b) is V22() real ext-real Element of REAL
u3 is V22() real ext-real Element of REAL
a is V22() real ext-real Element of REAL
u3 - a is V22() real ext-real Element of REAL
(u3 - a) ^2 is V22() real ext-real Element of REAL
(u3 - a) * (u3 - a) is V22() real ext-real set
sqrreal . (u3 - a) is V22() real ext-real set
u2 is V22() real ext-real Element of REAL
u4 is V22() real ext-real Element of REAL
u2 - u4 is V22() real ext-real Element of REAL
sqrreal . (u2 - u4) is V22() real ext-real set
(sqrreal . (u2 - u4)) + 0 is V22() real ext-real Element of REAL
(sqrreal . (u2 - u4)) + (sqrreal . (u3 - a)) is V22() real ext-real set
n - q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
- q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
K312((TOP-REAL 2),n,(- q)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (n,(- q)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
u3 - u3 is V22() real ext-real Element of REAL
<*(u2 - u4),(u3 - u3)*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
sqr (p1p - p1q) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of 2 -tuples_on REAL
sqrreal . (u3 - u3) is V22() real ext-real set
<*(sqrreal . (u2 - u4)),(sqrreal . (u3 - u3))*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
Sum (sqr (p1p - p1q)) is V22() real ext-real Element of REAL
sqrreal . 0 is V22() real ext-real set
(sqrreal . (u2 - u4)) + (sqrreal . 0) is V22() real ext-real set
0 ^2 is V22() real ext-real Element of REAL
0 * 0 is functional empty ordinal natural V22() real ext-real non positive non negative FinSequence-membered V137() V138() V139() V140() V141() V142() V143() set
(sqrreal . (u2 - u4)) + (0 ^2) is V22() real ext-real Element of REAL
n - f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
- f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
K312((TOP-REAL 2),n,(- f)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) . (n,(- f)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
<*(u2 - u4),(u3 - a)*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
sqr (p1p - qp1) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of 2 -tuples_on REAL
<*(sqrreal . (u2 - u4)),(sqrreal . (u3 - a))*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set
sqrt ((sqrreal . (u2 - u4)) + (sqrreal . (u3 - a))) is V22() real ext-real set
(u2 - u4) ^2 is V22() real ext-real Element of REAL
(u2 - u4) * (u2 - u4) is V22() real ext-real set
n is V22() real ext-real set
f is V22() real ext-real set
|[n,f]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
q is V22() real ext-real set
r is V22() real ext-real set
|[n,r]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
f + r is V22() real ext-real set
(f + r) / 2 is V22() real ext-real Element of REAL
|[n,((f + r) / 2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
u is Element of the carrier of (Euclid 2)
Ball (u,q) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
LSeg (|[n,f]|,|[n,r]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[n,f]|) + (b₁ * |[n,r]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
|[n,f]| `2 is V22() real ext-real Element of REAL
K434(|[n,f]|,2) is V22() real ext-real Element of REAL
|[n,r]| `2 is V22() real ext-real Element of REAL
K434(|[n,r]|,2) is V22() real ext-real Element of REAL
|[n,((f + r) / 2)]| `2 is V22() real ext-real Element of REAL
K434(|[n,((f + r) / 2)]|,2) is V22() real ext-real Element of REAL
1 / 2 is V22() real ext-real non negative Element of REAL
1 - (1 / 2) is V22() real ext-real Element of REAL
(1 - (1 / 2)) * (|[n,f]| `2) is V22() real ext-real Element of REAL
(1 / 2) * (|[n,r]| `2) is V22() real ext-real Element of REAL
((1 - (1 / 2)) * (|[n,f]| `2)) + ((1 / 2) * (|[n,r]| `2)) is V22() real ext-real Element of REAL
(1 - (1 / 2)) * |[n,f]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - (1 / 2)) * |[n,f]|) `2 is V22() real ext-real Element of REAL
K434(((1 - (1 / 2)) * |[n,f]|),2) is V22() real ext-real Element of REAL
(((1 - (1 / 2)) * |[n,f]|) `2) + ((1 / 2) * (|[n,r]| `2)) is V22() real ext-real Element of REAL
(1 / 2) * |[n,r]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 / 2) * |[n,r]|) `2 is V22() real ext-real Element of REAL
K434(((1 / 2) * |[n,r]|),2) is V22() real ext-real Element of REAL
(((1 - (1 / 2)) * |[n,f]|) `2) + (((1 / 2) * |[n,r]|) `2) is V22() real ext-real Element of REAL
((1 - (1 / 2)) * |[n,f]|) + ((1 / 2) * |[n,r]|) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (((1 - (1 / 2)) * |[n,f]|),((1 / 2) * |[n,r]|)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(((1 - (1 / 2)) * |[n,f]|) + ((1 / 2) * |[n,r]|)) `2 is V22() real ext-real Element of REAL
K434((((1 - (1 / 2)) * |[n,f]|) + ((1 / 2) * |[n,r]|)),2) is V22() real ext-real Element of REAL
|[n,f]| `1 is V22() real ext-real Element of REAL
K434(|[n,f]|,1) is V22() real ext-real Element of REAL
|[n,r]| `1 is V22() real ext-real Element of REAL
K434(|[n,r]|,1) is V22() real ext-real Element of REAL
|[n,((f + r) / 2)]| `1 is V22() real ext-real Element of REAL
K434(|[n,((f + r) / 2)]|,1) is V22() real ext-real Element of REAL
(1 - (1 / 2)) * (|[n,f]| `1) is V22() real ext-real Element of REAL
(1 / 2) * (|[n,r]| `1) is V22() real ext-real Element of REAL
((1 - (1 / 2)) * (|[n,f]| `1)) + ((1 / 2) * (|[n,r]| `1)) is V22() real ext-real Element of REAL
((1 - (1 / 2)) * |[n,f]|) `1 is V22() real ext-real Element of REAL
K434(((1 - (1 / 2)) * |[n,f]|),1) is V22() real ext-real Element of REAL
(((1 - (1 / 2)) * |[n,f]|) `1) + ((1 / 2) * (|[n,r]| `1)) is V22() real ext-real Element of REAL
((1 / 2) * |[n,r]|) `1 is V22() real ext-real Element of REAL
K434(((1 / 2) * |[n,r]|),1) is V22() real ext-real Element of REAL
(((1 - (1 / 2)) * |[n,f]|) `1) + (((1 / 2) * |[n,r]|) `1) is V22() real ext-real Element of REAL
(((1 - (1 / 2)) * |[n,f]|) + ((1 / 2) * |[n,r]|)) `1 is V22() real ext-real Element of REAL
K434((((1 - (1 / 2)) * |[n,f]|) + ((1 / 2) * |[n,r]|)),1) is V22() real ext-real Element of REAL
n is V22() real ext-real set
f is V22() real ext-real set
|[n,f]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
q is V22() real ext-real set
r is V22() real ext-real set
|[r,f]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
n + r is V22() real ext-real set
(n + r) / 2 is V22() real ext-real Element of REAL
|[((n + r) / 2),f]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
u is Element of the carrier of (Euclid 2)
Ball (u,q) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
LSeg (|[n,f]|,|[r,f]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[n,f]|) + (b₁ * |[r,f]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
|[n,f]| `1 is V22() real ext-real Element of REAL
K434(|[n,f]|,1) is V22() real ext-real Element of REAL
|[r,f]| `1 is V22() real ext-real Element of REAL
K434(|[r,f]|,1) is V22() real ext-real Element of REAL
|[((n + r) / 2),f]| `1 is V22() real ext-real Element of REAL
K434(|[((n + r) / 2),f]|,1) is V22() real ext-real Element of REAL
1 / 2 is V22() real ext-real non negative Element of REAL
1 - (1 / 2) is V22() real ext-real Element of REAL
(1 - (1 / 2)) * (|[n,f]| `1) is V22() real ext-real Element of REAL
(1 / 2) * (|[r,f]| `1) is V22() real ext-real Element of REAL
((1 - (1 / 2)) * (|[n,f]| `1)) + ((1 / 2) * (|[r,f]| `1)) is V22() real ext-real Element of REAL
(1 - (1 / 2)) * |[n,f]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - (1 / 2)) * |[n,f]|) `1 is V22() real ext-real Element of REAL
K434(((1 - (1 / 2)) * |[n,f]|),1) is V22() real ext-real Element of REAL
(((1 - (1 / 2)) * |[n,f]|) `1) + ((1 / 2) * (|[r,f]| `1)) is V22() real ext-real Element of REAL
(1 / 2) * |[r,f]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 / 2) * |[r,f]|) `1 is V22() real ext-real Element of REAL
K434(((1 / 2) * |[r,f]|),1) is V22() real ext-real Element of REAL
(((1 - (1 / 2)) * |[n,f]|) `1) + (((1 / 2) * |[r,f]|) `1) is V22() real ext-real Element of REAL
((1 - (1 / 2)) * |[n,f]|) + ((1 / 2) * |[r,f]|) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (((1 - (1 / 2)) * |[n,f]|),((1 / 2) * |[r,f]|)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(((1 - (1 / 2)) * |[n,f]|) + ((1 / 2) * |[r,f]|)) `1 is V22() real ext-real Element of REAL
K434((((1 - (1 / 2)) * |[n,f]|) + ((1 / 2) * |[r,f]|)),1) is V22() real ext-real Element of REAL
|[n,f]| `2 is V22() real ext-real Element of REAL
K434(|[n,f]|,2) is V22() real ext-real Element of REAL
|[r,f]| `2 is V22() real ext-real Element of REAL
K434(|[r,f]|,2) is V22() real ext-real Element of REAL
|[((n + r) / 2),f]| `2 is V22() real ext-real Element of REAL
K434(|[((n + r) / 2),f]|,2) is V22() real ext-real Element of REAL
(1 - (1 / 2)) * (|[n,f]| `2) is V22() real ext-real Element of REAL
(1 / 2) * (|[r,f]| `2) is V22() real ext-real Element of REAL
((1 - (1 / 2)) * (|[n,f]| `2)) + ((1 / 2) * (|[r,f]| `2)) is V22() real ext-real Element of REAL
((1 - (1 / 2)) * |[n,f]|) `2 is V22() real ext-real Element of REAL
K434(((1 - (1 / 2)) * |[n,f]|),2) is V22() real ext-real Element of REAL
(((1 - (1 / 2)) * |[n,f]|) `2) + ((1 / 2) * (|[r,f]| `2)) is V22() real ext-real Element of REAL
((1 / 2) * |[r,f]|) `2 is V22() real ext-real Element of REAL
K434(((1 / 2) * |[r,f]|),2) is V22() real ext-real Element of REAL
(((1 - (1 / 2)) * |[n,f]|) `2) + (((1 / 2) * |[r,f]|) `2) is V22() real ext-real Element of REAL
(((1 - (1 / 2)) * |[n,f]|) + ((1 / 2) * |[r,f]|)) `2 is V22() real ext-real Element of REAL
K434((((1 - (1 / 2)) * |[n,f]|) + ((1 / 2) * |[r,f]|)),2) is V22() real ext-real Element of REAL
n is V22() real ext-real set
f is V22() real ext-real set
|[n,f]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
q is V22() real ext-real set
r is V22() real ext-real set
|[r,f]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
u is V22() real ext-real set
|[r,u]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[n,u]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
v is Element of the carrier of (Euclid 2)
Ball (v,q) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
x is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
x `1 is V22() real ext-real Element of REAL
K434(x,1) is V22() real ext-real Element of REAL
|[n,u]| `1 is V22() real ext-real Element of REAL
K434(|[n,u]|,1) is V22() real ext-real Element of REAL
(x `1) - (|[n,u]| `1) is V22() real ext-real Element of REAL
((x `1) - (|[n,u]| `1)) ^2 is V22() real ext-real Element of REAL
((x `1) - (|[n,u]| `1)) * ((x `1) - (|[n,u]| `1)) is V22() real ext-real set
x `2 is V22() real ext-real Element of REAL
K434(x,2) is V22() real ext-real Element of REAL
|[n,u]| `2 is V22() real ext-real Element of REAL
K434(|[n,u]|,2) is V22() real ext-real Element of REAL
(x `2) - (|[n,u]| `2) is V22() real ext-real Element of REAL
((x `2) - (|[n,u]| `2)) ^2 is V22() real ext-real Element of REAL
((x `2) - (|[n,u]| `2)) * ((x `2) - (|[n,u]| `2)) is V22() real ext-real set
(((x `1) - (|[n,u]| `1)) ^2) + (((x `2) - (|[n,u]| `2)) ^2) is V22() real ext-real Element of REAL
|[n,f]| `1 is V22() real ext-real Element of REAL
K434(|[n,f]|,1) is V22() real ext-real Element of REAL
(x `1) - (|[n,f]| `1) is V22() real ext-real Element of REAL
((x `1) - (|[n,f]| `1)) ^2 is V22() real ext-real Element of REAL
((x `1) - (|[n,f]| `1)) * ((x `1) - (|[n,f]| `1)) is V22() real ext-real set
|[n,f]| `2 is V22() real ext-real Element of REAL
K434(|[n,f]|,2) is V22() real ext-real Element of REAL
(x `2) - (|[n,f]| `2) is V22() real ext-real Element of REAL
((x `2) - (|[n,f]| `2)) ^2 is V22() real ext-real Element of REAL
((x `2) - (|[n,f]| `2)) * ((x `2) - (|[n,f]| `2)) is V22() real ext-real set
(((x `1) - (|[n,f]| `1)) ^2) + (((x `2) - (|[n,f]| `2)) ^2) is V22() real ext-real Element of REAL
|[r,u]| `1 is V22() real ext-real Element of REAL
K434(|[r,u]|,1) is V22() real ext-real Element of REAL
(x `1) - (|[r,u]| `1) is V22() real ext-real Element of REAL
((x `1) - (|[r,u]| `1)) ^2 is V22() real ext-real Element of REAL
((x `1) - (|[r,u]| `1)) * ((x `1) - (|[r,u]| `1)) is V22() real ext-real set
|[r,u]| `2 is V22() real ext-real Element of REAL
K434(|[r,u]|,2) is V22() real ext-real Element of REAL
(x `2) - (|[r,u]| `2) is V22() real ext-real Element of REAL
((x `2) - (|[r,u]| `2)) ^2 is V22() real ext-real Element of REAL
((x `2) - (|[r,u]| `2)) * ((x `2) - (|[r,u]| `2)) is V22() real ext-real set
(((x `1) - (|[r,u]| `1)) ^2) + (((x `2) - (|[r,u]| `2)) ^2) is V22() real ext-real Element of REAL
|[r,f]| `1 is V22() real ext-real Element of REAL
K434(|[r,f]|,1) is V22() real ext-real Element of REAL
(x `1) - (|[r,f]| `1) is V22() real ext-real Element of REAL
((x `1) - (|[r,f]| `1)) ^2 is V22() real ext-real Element of REAL
((x `1) - (|[r,f]| `1)) * ((x `1) - (|[r,f]| `1)) is V22() real ext-real set
|[r,f]| `2 is V22() real ext-real Element of REAL
K434(|[r,f]|,2) is V22() real ext-real Element of REAL
(x `2) - (|[r,f]| `2) is V22() real ext-real Element of REAL
((x `2) - (|[r,f]| `2)) ^2 is V22() real ext-real Element of REAL
((x `2) - (|[r,f]| `2)) * ((x `2) - (|[r,f]| `2)) is V22() real ext-real set
(((x `1) - (|[r,f]| `1)) ^2) + (((x `2) - (|[r,f]| `2)) ^2) is V22() real ext-real Element of REAL
p1q is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (v,p1q) is set
dist (v,p1q) is V22() real ext-real Element of REAL
sqrt ((((x `1) - (|[n,u]| `1)) ^2) + (((x `2) - (|[n,u]| `2)) ^2)) is V22() real ext-real Element of REAL
q * q is V22() real ext-real set
(sqrt ((((x `1) - (|[n,u]| `1)) ^2) + (((x `2) - (|[n,u]| `2)) ^2))) ^2 is V22() real ext-real Element of REAL
(sqrt ((((x `1) - (|[n,u]| `1)) ^2) + (((x `2) - (|[n,u]| `2)) ^2))) * (sqrt ((((x `1) - (|[n,u]| `1)) ^2) + (((x `2) - (|[n,u]| `2)) ^2))) is V22() real ext-real set
q ^2 is V22() real ext-real set
u3 is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (v,u3) is set
dist (v,u3) is V22() real ext-real Element of REAL
sqrt ((((x `1) - (|[r,u]| `1)) ^2) + (((x `2) - (|[r,u]| `2)) ^2)) is V22() real ext-real Element of REAL
(sqrt ((((x `1) - (|[r,u]| `1)) ^2) + (((x `2) - (|[r,u]| `2)) ^2))) ^2 is V22() real ext-real Element of REAL
(sqrt ((((x `1) - (|[r,u]| `1)) ^2) + (((x `2) - (|[r,u]| `2)) ^2))) * (sqrt ((((x `1) - (|[r,u]| `1)) ^2) + (((x `2) - (|[r,u]| `2)) ^2))) is V22() real ext-real set
u4 is Element of the carrier of (Euclid 2)
(Pitag_dist 2) . (v,u4) is set
dist (v,u4) is V22() real ext-real Element of REAL
sqrt ((((x `1) - (|[n,f]| `1)) ^2) + (((x `2) - (|[n,f]| `2)) ^2)) is V22() real ext-real Element of REAL
((((x `1) - (|[r,u]| `1)) ^2) + (((x `2) - (|[r,u]| `2)) ^2)) + ((((x `1) - (|[n,f]| `1)) ^2) + (((x `2) - (|[n,f]| `2)) ^2)) is V22() real ext-real Element of REAL
((((x `1) - (|[n,u]| `1)) ^2) + (((x `2) - (|[n,u]| `2)) ^2)) + ((((x `1) - (|[r,f]| `1)) ^2) + (((x `2) - (|[r,f]| `2)) ^2)) is V22() real ext-real Element of REAL
(q ^2) + ((((x `1) - (|[r,f]| `1)) ^2) + (((x `2) - (|[r,f]| `2)) ^2)) is V22() real ext-real Element of REAL
(sqrt ((((x `1) - (|[n,f]| `1)) ^2) + (((x `2) - (|[n,f]| `2)) ^2))) ^2 is V22() real ext-real Element of REAL
(sqrt ((((x `1) - (|[n,f]| `1)) ^2) + (((x `2) - (|[n,f]| `2)) ^2))) * (sqrt ((((x `1) - (|[n,f]| `1)) ^2) + (((x `2) - (|[n,f]| `2)) ^2))) is V22() real ext-real set
(q ^2) + (q ^2) is V22() real ext-real set
((q ^2) + (q ^2)) - (q ^2) is V22() real ext-real set
sqrt (q ^2) is V22() real ext-real set
sqrt ((((x `1) - (|[r,f]| `1)) ^2) + (((x `2) - (|[r,f]| `2)) ^2)) is V22() real ext-real Element of REAL
u2 is Element of the carrier of (Euclid 2)
dist (v,u2) is V22() real ext-real Element of REAL
(Pitag_dist 2) . (v,u2) is set
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
n /. 1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
len n is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
(len n) - 1 is V22() real ext-real Element of REAL
f is V22() real ext-real set
q is Element of the carrier of (Euclid 2)
Ball (q,f) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
r is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n /. r is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
r - 1 is V22() real ext-real Element of REAL
1 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
u is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n /. (u + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
LSeg (n,u) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (n,u)) /\ (Ball (q,f)) is Element of K19( the carrier of (Euclid 2))
r + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
LSeg (n,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * n) + (b<sub>1</sub> * f)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
{f} is non empty set
q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
q `2 is V22() real ext-real Element of REAL
K434(q,2) is V22() real ext-real Element of REAL
|[(f `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (f,|[(f `1),(q `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * f) + (b₁ * |[(f `1),(q `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (|[(f `1),(q `2)]|,q) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[(f `1),(q `2)]|) + (b₁ * q)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (f,|[(f `1),(q `2)]|)) \/ (LSeg (|[(f `1),(q `2)]|,q)) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,|[(f `1),(q `2)]|)) \/ (LSeg (|[(f `1),(q `2)]|,q))) /\ (LSeg (n,f)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[(f `1),(q `2)]|,q)) /\ (LSeg (n,f)) is Element of K19( the carrier of (TOP-REAL 2))
the Element of (LSeg (|[(f `1),(q `2)]|,q)) /\ (LSeg (n,f)) is Element of (LSeg (|[(f `1),(q `2)]|,q)) /\ (LSeg (n,f))
pp1 is V22() real ext-real Element of REAL
1 - pp1 is V22() real ext-real Element of REAL
(1 - pp1) * |[(f `1),(q `2)]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
pp1 * q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - pp1) * |[(f `1),(q `2)]|) + (pp1 * q) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (((1 - pp1) * |[(f `1),(q `2)]|),(pp1 * q)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
p1p is V22() real ext-real Element of REAL
1 - p1p is V22() real ext-real Element of REAL
(1 - p1p) * n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
p1p * f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - p1p) * n) + (p1p * f) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) . (((1 - p1p) * n),(p1p * f)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(((1 - pp1) * |[(f `1),(q `2)]|) + (pp1 * q)) `2 is V22() real ext-real Element of REAL
K434((((1 - pp1) * |[(f `1),(q `2)]|) + (pp1 * q)),2) is V22() real ext-real Element of REAL
((1 - pp1) * |[(f `1),(q `2)]|) `2 is V22() real ext-real Element of REAL
K434(((1 - pp1) * |[(f `1),(q `2)]|),2) is V22() real ext-real Element of REAL
(pp1 * q) `2 is V22() real ext-real Element of REAL
K434((pp1 * q),2) is V22() real ext-real Element of REAL
(((1 - pp1) * |[(f `1),(q `2)]|) `2) + ((pp1 * q) `2) is V22() real ext-real Element of REAL
|[(f `1),(q `2)]| `2 is V22() real ext-real Element of REAL
K434(|[(f `1),(q `2)]|,2) is V22() real ext-real Element of REAL
(1 - pp1) * (|[(f `1),(q `2)]| `2) is V22() real ext-real Element of REAL
((1 - pp1) * (|[(f `1),(q `2)]| `2)) + ((pp1 * q) `2) is V22() real ext-real Element of REAL
pp1 * (q `2) is V22() real ext-real Element of REAL
((1 - pp1) * (|[(f `1),(q `2)]| `2)) + (pp1 * (q `2)) is V22() real ext-real Element of REAL
(1 - pp1) * (q `2) is V22() real ext-real Element of REAL
((1 - pp1) * (q `2)) + (pp1 * (q `2)) is V22() real ext-real Element of REAL
(((1 - p1p) * n) + (p1p * f)) `2 is V22() real ext-real Element of REAL
K434((((1 - p1p) * n) + (p1p * f)),2) is V22() real ext-real Element of REAL
((1 - p1p) * n) `2 is V22() real ext-real Element of REAL
K434(((1 - p1p) * n),2) is V22() real ext-real Element of REAL
(p1p * f) `2 is V22() real ext-real Element of REAL
K434((p1p * f),2) is V22() real ext-real Element of REAL
(((1 - p1p) * n) `2) + ((p1p * f) `2) is V22() real ext-real Element of REAL
(1 - p1p) * (n `2) is V22() real ext-real Element of REAL
((1 - p1p) * (n `2)) + ((p1p * f) `2) is V22() real ext-real Element of REAL
p1p * (f `2) is V22() real ext-real Element of REAL
((1 - p1p) * (n `2)) + (p1p * (f `2)) is V22() real ext-real Element of REAL
(LSeg (f,|[(f `1),(q `2)]|)) /\ (LSeg (n,f)) is Element of K19( the carrier of (TOP-REAL 2))
qp is set
pp1 is V22() real ext-real Element of REAL
1 - pp1 is V22() real ext-real Element of REAL
(1 - pp1) * f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
pp1 * |[(f `1),(q `2)]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - pp1) * f) + (pp1 * |[(f `1),(q `2)]|) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (((1 - pp1) * f),(pp1 * |[(f `1),(q `2)]|)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
p1p is V22() real ext-real Element of REAL
1 - p1p is V22() real ext-real Element of REAL
(1 - p1p) * n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
p1p * f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - p1p) * n) + (p1p * f) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) . (((1 - p1p) * n),(p1p * f)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(((1 - p1p) * n) + (p1p * f)) `2 is V22() real ext-real Element of REAL
K434((((1 - p1p) * n) + (p1p * f)),2) is V22() real ext-real Element of REAL
((1 - p1p) * n) `2 is V22() real ext-real Element of REAL
K434(((1 - p1p) * n),2) is V22() real ext-real Element of REAL
(p1p * f) `2 is V22() real ext-real Element of REAL
K434((p1p * f),2) is V22() real ext-real Element of REAL
(((1 - p1p) * n) `2) + ((p1p * f) `2) is V22() real ext-real Element of REAL
(1 - p1p) * (n `2) is V22() real ext-real Element of REAL
((1 - p1p) * (n `2)) + ((p1p * f) `2) is V22() real ext-real Element of REAL
p1p * (f `2) is V22() real ext-real Element of REAL
((1 - p1p) * (n `2)) + (p1p * (f `2)) is V22() real ext-real Element of REAL
(((1 - pp1) * f) + (pp1 * |[(f `1),(q `2)]|)) `1 is V22() real ext-real Element of REAL
K434((((1 - pp1) * f) + (pp1 * |[(f `1),(q `2)]|)),1) is V22() real ext-real Element of REAL
((1 - pp1) * f) `1 is V22() real ext-real Element of REAL
K434(((1 - pp1) * f),1) is V22() real ext-real Element of REAL
(pp1 * |[(f `1),(q `2)]|) `1 is V22() real ext-real Element of REAL
K434((pp1 * |[(f `1),(q `2)]|),1) is V22() real ext-real Element of REAL
(((1 - pp1) * f) `1) + ((pp1 * |[(f `1),(q `2)]|) `1) is V22() real ext-real Element of REAL
(1 - pp1) * (f `1) is V22() real ext-real Element of REAL
((1 - pp1) * (f `1)) + ((pp1 * |[(f `1),(q `2)]|) `1) is V22() real ext-real Element of REAL
|[(f `1),(q `2)]| `1 is V22() real ext-real Element of REAL
K434(|[(f `1),(q `2)]|,1) is V22() real ext-real Element of REAL
pp1 * (|[(f `1),(q `2)]| `1) is V22() real ext-real Element of REAL
((1 - pp1) * (f `1)) + (pp1 * (|[(f `1),(q `2)]| `1)) is V22() real ext-real Element of REAL
pp1 * (f `1) is V22() real ext-real Element of REAL
((1 - pp1) * (f `1)) + (pp1 * (f `1)) is V22() real ext-real Element of REAL
(((1 - pp1) * f) + (pp1 * |[(f `1),(q `2)]|)) `2 is V22() real ext-real Element of REAL
K434((((1 - pp1) * f) + (pp1 * |[(f `1),(q `2)]|)),2) is V22() real ext-real Element of REAL
|[((((1 - pp1) * f) + (pp1 * |[(f `1),(q `2)]|)) `1),((((1 - pp1) * f) + (pp1 * |[(f `1),(q `2)]|)) `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
qp is set
((LSeg (f,|[(f `1),(q `2)]|)) /\ (LSeg (n,f))) \/ ((LSeg (|[(f `1),(q `2)]|,q)) /\ (LSeg (n,f))) is Element of K19( the carrier of (TOP-REAL 2))
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
LSeg (n,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{f} is non empty set
q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
q `1 is V22() real ext-real Element of REAL
K434(q,1) is V22() real ext-real Element of REAL
|[(q `1),(f `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (f,|[(q `1),(f `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * f) + (b<sub>1</sub> * |[(q `1),(f `2)]|)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
LSeg (|[(q `1),(f `2)]|,q) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * |[(q `1),(f `2)]|) + (b<sub>1</sub> * q)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
(LSeg (f,|[(q `1),(f `2)]|)) \/ (LSeg (|[(q `1),(f `2)]|,q)) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,|[(q `1),(f `2)]|)) \/ (LSeg (|[(q `1),(f `2)]|,q))) /\ (LSeg (n,f)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[(q `1),(f `2)]|,q)) /\ (LSeg (n,f)) is Element of K19( the carrier of (TOP-REAL 2))
the Element of (LSeg (|[(q `1),(f `2)]|,q)) /\ (LSeg (n,f)) is Element of (LSeg (|[(q `1),(f `2)]|,q)) /\ (LSeg (n,f))
pp1 is V22() real ext-real Element of REAL
1 - pp1 is V22() real ext-real Element of REAL
(1 - pp1) * |[(q `1),(f `2)]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
pp1 * q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - pp1) * |[(q `1),(f `2)]|) + (pp1 * q) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (((1 - pp1) * |[(q `1),(f `2)]|),(pp1 * q)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
p1p is V22() real ext-real Element of REAL
1 - p1p is V22() real ext-real Element of REAL
(1 - p1p) * n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
p1p * f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - p1p) * n) + (p1p * f) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) . (((1 - p1p) * n),(p1p * f)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(((1 - pp1) * |[(q `1),(f `2)]|) + (pp1 * q)) `1 is V22() real ext-real Element of REAL
K434((((1 - pp1) * |[(q `1),(f `2)]|) + (pp1 * q)),1) is V22() real ext-real Element of REAL
((1 - pp1) * |[(q `1),(f `2)]|) `1 is V22() real ext-real Element of REAL
K434(((1 - pp1) * |[(q `1),(f `2)]|),1) is V22() real ext-real Element of REAL
(pp1 * q) `1 is V22() real ext-real Element of REAL
K434((pp1 * q),1) is V22() real ext-real Element of REAL
(((1 - pp1) * |[(q `1),(f `2)]|) `1) + ((pp1 * q) `1) is V22() real ext-real Element of REAL
|[(q `1),(f `2)]| `1 is V22() real ext-real Element of REAL
K434(|[(q `1),(f `2)]|,1) is V22() real ext-real Element of REAL
(1 - pp1) * (|[(q `1),(f `2)]| `1) is V22() real ext-real Element of REAL
((1 - pp1) * (|[(q `1),(f `2)]| `1)) + ((pp1 * q) `1) is V22() real ext-real Element of REAL
pp1 * (q `1) is V22() real ext-real Element of REAL
((1 - pp1) * (|[(q `1),(f `2)]| `1)) + (pp1 * (q `1)) is V22() real ext-real Element of REAL
(1 - pp1) * (q `1) is V22() real ext-real Element of REAL
((1 - pp1) * (q `1)) + (pp1 * (q `1)) is V22() real ext-real Element of REAL
(((1 - p1p) * n) + (p1p * f)) `1 is V22() real ext-real Element of REAL
K434((((1 - p1p) * n) + (p1p * f)),1) is V22() real ext-real Element of REAL
((1 - p1p) * n) `1 is V22() real ext-real Element of REAL
K434(((1 - p1p) * n),1) is V22() real ext-real Element of REAL
(p1p * f) `1 is V22() real ext-real Element of REAL
K434((p1p * f),1) is V22() real ext-real Element of REAL
(((1 - p1p) * n) `1) + ((p1p * f) `1) is V22() real ext-real Element of REAL
(1 - p1p) * (n `1) is V22() real ext-real Element of REAL
((1 - p1p) * (n `1)) + ((p1p * f) `1) is V22() real ext-real Element of REAL
p1p * (f `1) is V22() real ext-real Element of REAL
((1 - p1p) * (n `1)) + (p1p * (f `1)) is V22() real ext-real Element of REAL
(LSeg (f,|[(q `1),(f `2)]|)) /\ (LSeg (n,f)) is Element of K19( the carrier of (TOP-REAL 2))
qp is set
pp1 is V22() real ext-real Element of REAL
1 - pp1 is V22() real ext-real Element of REAL
(1 - pp1) * f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
pp1 * |[(q `1),(f `2)]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - pp1) * f) + (pp1 * |[(q `1),(f `2)]|) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (((1 - pp1) * f),(pp1 * |[(q `1),(f `2)]|)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
p1p is V22() real ext-real Element of REAL
1 - p1p is V22() real ext-real Element of REAL
(1 - p1p) * n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
p1p * f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - p1p) * n) + (p1p * f) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) . (((1 - p1p) * n),(p1p * f)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(((1 - p1p) * n) + (p1p * f)) `1 is V22() real ext-real Element of REAL
K434((((1 - p1p) * n) + (p1p * f)),1) is V22() real ext-real Element of REAL
((1 - p1p) * n) `1 is V22() real ext-real Element of REAL
K434(((1 - p1p) * n),1) is V22() real ext-real Element of REAL
(p1p * f) `1 is V22() real ext-real Element of REAL
K434((p1p * f),1) is V22() real ext-real Element of REAL
(((1 - p1p) * n) `1) + ((p1p * f) `1) is V22() real ext-real Element of REAL
(1 - p1p) * (n `1) is V22() real ext-real Element of REAL
((1 - p1p) * (n `1)) + ((p1p * f) `1) is V22() real ext-real Element of REAL
p1p * (f `1) is V22() real ext-real Element of REAL
((1 - p1p) * (n `1)) + (p1p * (f `1)) is V22() real ext-real Element of REAL
(((1 - pp1) * f) + (pp1 * |[(q `1),(f `2)]|)) `2 is V22() real ext-real Element of REAL
K434((((1 - pp1) * f) + (pp1 * |[(q `1),(f `2)]|)),2) is V22() real ext-real Element of REAL
((1 - pp1) * f) `2 is V22() real ext-real Element of REAL
K434(((1 - pp1) * f),2) is V22() real ext-real Element of REAL
(pp1 * |[(q `1),(f `2)]|) `2 is V22() real ext-real Element of REAL
K434((pp1 * |[(q `1),(f `2)]|),2) is V22() real ext-real Element of REAL
(((1 - pp1) * f) `2) + ((pp1 * |[(q `1),(f `2)]|) `2) is V22() real ext-real Element of REAL
(1 - pp1) * (f `2) is V22() real ext-real Element of REAL
((1 - pp1) * (f `2)) + ((pp1 * |[(q `1),(f `2)]|) `2) is V22() real ext-real Element of REAL
|[(q `1),(f `2)]| `2 is V22() real ext-real Element of REAL
K434(|[(q `1),(f `2)]|,2) is V22() real ext-real Element of REAL
pp1 * (|[(q `1),(f `2)]| `2) is V22() real ext-real Element of REAL
((1 - pp1) * (f `2)) + (pp1 * (|[(q `1),(f `2)]| `2)) is V22() real ext-real Element of REAL
pp1 * (f `2) is V22() real ext-real Element of REAL
((1 - pp1) * (f `2)) + (pp1 * (f `2)) is V22() real ext-real Element of REAL
(((1 - pp1) * f) + (pp1 * |[(q `1),(f `2)]|)) `1 is V22() real ext-real Element of REAL
K434((((1 - pp1) * f) + (pp1 * |[(q `1),(f `2)]|)),1) is V22() real ext-real Element of REAL
|[((((1 - pp1) * f) + (pp1 * |[(q `1),(f `2)]|)) `1),((((1 - pp1) * f) + (pp1 * |[(q `1),(f `2)]|)) `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
qp is set
((LSeg (f,|[(q `1),(f `2)]|)) /\ (LSeg (n,f))) \/ ((LSeg (|[(q `1),(f `2)]|,q)) /\ (LSeg (n,f))) is Element of K19( the carrier of (TOP-REAL 2))
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
|[(n `1),(f `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (n,|[(n `1),(f `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(n `1),(f `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (|[(n `1),(f `2)]|,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[(n `1),(f `2)]|) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (n,|[(n `1),(f `2)]|)) /\ (LSeg (|[(n `1),(f `2)]|,f)) is Element of K19( the carrier of (TOP-REAL 2))
{|[(n `1),(f `2)]|} is non empty set
v is set
x is V22() real ext-real Element of REAL
1 - x is V22() real ext-real Element of REAL
(1 - x) * n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
x * |[(n `1),(f `2)]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - x) * n) + (x * |[(n `1),(f `2)]|) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (((1 - x) * n),(x * |[(n `1),(f `2)]|)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp is V22() real ext-real Element of REAL
1 - qp is V22() real ext-real Element of REAL
(1 - qp) * |[(n `1),(f `2)]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp * f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - qp) * |[(n `1),(f `2)]|) + (qp * f) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) . (((1 - qp) * |[(n `1),(f `2)]|),(qp * f)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(((1 - x) * n) + (x * |[(n `1),(f `2)]|)) `1 is V22() real ext-real Element of REAL
K434((((1 - x) * n) + (x * |[(n `1),(f `2)]|)),1) is V22() real ext-real Element of REAL
((1 - x) * n) `1 is V22() real ext-real Element of REAL
K434(((1 - x) * n),1) is V22() real ext-real Element of REAL
(x * |[(n `1),(f `2)]|) `1 is V22() real ext-real Element of REAL
K434((x * |[(n `1),(f `2)]|),1) is V22() real ext-real Element of REAL
(((1 - x) * n) `1) + ((x * |[(n `1),(f `2)]|) `1) is V22() real ext-real Element of REAL
(1 - x) * (n `1) is V22() real ext-real Element of REAL
((1 - x) * (n `1)) + ((x * |[(n `1),(f `2)]|) `1) is V22() real ext-real Element of REAL
|[(n `1),(f `2)]| `1 is V22() real ext-real Element of REAL
K434(|[(n `1),(f `2)]|,1) is V22() real ext-real Element of REAL
x * (|[(n `1),(f `2)]| `1) is V22() real ext-real Element of REAL
((1 - x) * (n `1)) + (x * (|[(n `1),(f `2)]| `1)) is V22() real ext-real Element of REAL
x * (n `1) is V22() real ext-real Element of REAL
((1 - x) * (n `1)) + (x * (n `1)) is V22() real ext-real Element of REAL
(((1 - x) * n) + (x * |[(n `1),(f `2)]|)) `2 is V22() real ext-real Element of REAL
K434((((1 - x) * n) + (x * |[(n `1),(f `2)]|)),2) is V22() real ext-real Element of REAL
((1 - qp) * |[(n `1),(f `2)]|) `2 is V22() real ext-real Element of REAL
K434(((1 - qp) * |[(n `1),(f `2)]|),2) is V22() real ext-real Element of REAL
(qp * f) `2 is V22() real ext-real Element of REAL
K434((qp * f),2) is V22() real ext-real Element of REAL
(((1 - qp) * |[(n `1),(f `2)]|) `2) + ((qp * f) `2) is V22() real ext-real Element of REAL
|[(n `1),(f `2)]| `2 is V22() real ext-real Element of REAL
K434(|[(n `1),(f `2)]|,2) is V22() real ext-real Element of REAL
(1 - qp) * (|[(n `1),(f `2)]| `2) is V22() real ext-real Element of REAL
((1 - qp) * (|[(n `1),(f `2)]| `2)) + ((qp * f) `2) is V22() real ext-real Element of REAL
qp * (f `2) is V22() real ext-real Element of REAL
((1 - qp) * (|[(n `1),(f `2)]| `2)) + (qp * (f `2)) is V22() real ext-real Element of REAL
(1 - qp) * (f `2) is V22() real ext-real Element of REAL
((1 - qp) * (f `2)) + (qp * (f `2)) is V22() real ext-real Element of REAL
v is set
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
|[(f `1),(n `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (n,|[(f `1),(n `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(f `1),(n `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (|[(f `1),(n `2)]|,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[(f `1),(n `2)]|) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (n,|[(f `1),(n `2)]|)) /\ (LSeg (|[(f `1),(n `2)]|,f)) is Element of K19( the carrier of (TOP-REAL 2))
{|[(f `1),(n `2)]|} is non empty set
v is set
x is V22() real ext-real Element of REAL
1 - x is V22() real ext-real Element of REAL
(1 - x) * n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
x * |[(f `1),(n `2)]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - x) * n) + (x * |[(f `1),(n `2)]|) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) is Relation-like K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) -defined the carrier of (TOP-REAL 2) -valued Function-like V30(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) Element of K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)))
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2)) is set
K19(K20(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)), the carrier of (TOP-REAL 2))) is set
the U7 of (TOP-REAL 2) . (((1 - x) * n),(x * |[(f `1),(n `2)]|)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp is V22() real ext-real Element of REAL
1 - qp is V22() real ext-real Element of REAL
(1 - qp) * |[(f `1),(n `2)]| is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp * f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((1 - qp) * |[(f `1),(n `2)]|) + (qp * f) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
the U7 of (TOP-REAL 2) . (((1 - qp) * |[(f `1),(n `2)]|),(qp * f)) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(((1 - x) * n) + (x * |[(f `1),(n `2)]|)) `2 is V22() real ext-real Element of REAL
K434((((1 - x) * n) + (x * |[(f `1),(n `2)]|)),2) is V22() real ext-real Element of REAL
((1 - x) * n) `2 is V22() real ext-real Element of REAL
K434(((1 - x) * n),2) is V22() real ext-real Element of REAL
(x * |[(f `1),(n `2)]|) `2 is V22() real ext-real Element of REAL
K434((x * |[(f `1),(n `2)]|),2) is V22() real ext-real Element of REAL
(((1 - x) * n) `2) + ((x * |[(f `1),(n `2)]|) `2) is V22() real ext-real Element of REAL
(1 - x) * (n `2) is V22() real ext-real Element of REAL
((1 - x) * (n `2)) + ((x * |[(f `1),(n `2)]|) `2) is V22() real ext-real Element of REAL
|[(f `1),(n `2)]| `2 is V22() real ext-real Element of REAL
K434(|[(f `1),(n `2)]|,2) is V22() real ext-real Element of REAL
x * (|[(f `1),(n `2)]| `2) is V22() real ext-real Element of REAL
((1 - x) * (n `2)) + (x * (|[(f `1),(n `2)]| `2)) is V22() real ext-real Element of REAL
(1 - x) * (|[(f `1),(n `2)]| `2) is V22() real ext-real Element of REAL
((1 - x) * (|[(f `1),(n `2)]| `2)) + (x * (|[(f `1),(n `2)]| `2)) is V22() real ext-real Element of REAL
(((1 - x) * n) + (x * |[(f `1),(n `2)]|)) `1 is V22() real ext-real Element of REAL
K434((((1 - x) * n) + (x * |[(f `1),(n `2)]|)),1) is V22() real ext-real Element of REAL
((1 - qp) * |[(f `1),(n `2)]|) `1 is V22() real ext-real Element of REAL
K434(((1 - qp) * |[(f `1),(n `2)]|),1) is V22() real ext-real Element of REAL
(qp * f) `1 is V22() real ext-real Element of REAL
K434((qp * f),1) is V22() real ext-real Element of REAL
(((1 - qp) * |[(f `1),(n `2)]|) `1) + ((qp * f) `1) is V22() real ext-real Element of REAL
|[(f `1),(n `2)]| `1 is V22() real ext-real Element of REAL
K434(|[(f `1),(n `2)]|,1) is V22() real ext-real Element of REAL
(1 - qp) * (|[(f `1),(n `2)]| `1) is V22() real ext-real Element of REAL
((1 - qp) * (|[(f `1),(n `2)]| `1)) + ((qp * f) `1) is V22() real ext-real Element of REAL
qp * (f `1) is V22() real ext-real Element of REAL
((1 - qp) * (|[(f `1),(n `2)]| `1)) + (qp * (f `1)) is V22() real ext-real Element of REAL
qp * (|[(f `1),(n `2)]| `1) is V22() real ext-real Element of REAL
((1 - qp) * (|[(f `1),(n `2)]| `1)) + (qp * (|[(f `1),(n `2)]| `1)) is V22() real ext-real Element of REAL
v is set
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
(n `2) + (f `2) is V22() real ext-real Element of REAL
((n `2) + (f `2)) / 2 is V22() real ext-real Element of REAL
|[(n `1),(((n `2) + (f `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (n,|[(n `1),(((n `2) + (f `2)) / 2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(n `1),(((n `2) + (f `2)) / 2)]|)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
LSeg (|[(n `1),(((n `2) + (f `2)) / 2)]|,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[(n `1),(((n `2) + (f `2)) / 2)]|) + (b<sub>1</sub> * f)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
(LSeg (n,|[(n `1),(((n `2) + (f `2)) / 2)]|)) /\ (LSeg (|[(n `1),(((n `2) + (f `2)) / 2)]|,f)) is Element of K19( the carrier of (TOP-REAL 2))
{|[(n `1),(((n `2) + (f `2)) / 2)]|} is non empty set
v is set
|[(n `1),(n `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (|[(n `1),(n `2)]|,|[(n `1),(((n `2) + (f `2)) / 2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * |[(n `1),(n `2)]|) + (b<sub>1</sub> * |[(n `1),(((n `2) + (f `2)) / 2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
|[(f `1),(((n `2) + (f `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[(f `1),(f `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (|[(f `1),(((n `2) + (f `2)) / 2)]|,|[(f `1),(f `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[(f `1),(((n `2) + (f `2)) / 2)]|) + (b<sub>1</sub> * |[(f `1),(f `2)]|)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
{ b<sub>1</sub> where b<sub>1</sub> is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = n `1 & n `2 <= b₁ `2 & b<sub>1</sub> `2 <= ((n `2) + (f `2)) / 2 ) } is set
x is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
x `1 is V22() real ext-real Element of REAL
K434(x,1) is V22() real ext-real Element of REAL
x `2 is V22() real ext-real Element of REAL
K434(x,2) is V22() real ext-real Element of REAL
|[(n `1),(((n `2) + (f `2)) / 2)]| `2 is V22() real ext-real Element of REAL
K434(|[(n `1),(((n `2) + (f `2)) / 2)]|,2) is V22() real ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = f `1 & ((n `2) + (f `2)) / 2 <= b<sub>1</sub> `2 & b₁ `2 <= f `2 ) } is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
|[(n `1),(((n `2) + (f `2)) / 2)]| `1 is V22() real ext-real Element of REAL
K434(|[(n `1),(((n `2) + (f `2)) / 2)]|,1) is V22() real ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = n `1 & ((n `2) + (f `2)) / 2 <= b<sub>1</sub> `2 & b₁ `2 <= n `2 ) } is set
x is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
x `1 is V22() real ext-real Element of REAL
K434(x,1) is V22() real ext-real Element of REAL
x `2 is V22() real ext-real Element of REAL
K434(x,2) is V22() real ext-real Element of REAL
|[(n `1),(((n `2) + (f `2)) / 2)]| `2 is V22() real ext-real Element of REAL
K434(|[(n `1),(((n `2) + (f `2)) / 2)]|,2) is V22() real ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = f `1 & f `2 <= b₁ `2 & b<sub>1</sub> `2 <= ((n `2) + (f `2)) / 2 ) } is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
|[(n `1),(((n `2) + (f `2)) / 2)]| `1 is V22() real ext-real Element of REAL
K434(|[(n `1),(((n `2) + (f `2)) / 2)]|,1) is V22() real ext-real Element of REAL
v is set
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
(n `1) + (f `1) is V22() real ext-real Element of REAL
((n `1) + (f `1)) / 2 is V22() real ext-real Element of REAL
|[(((n `1) + (f `1)) / 2),(n `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (n,|[(((n `1) + (f `1)) / 2),(n `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * n) + (b<sub>1</sub> * |[(((n `1) + (f `1)) / 2),(n `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (|[(((n `1) + (f `1)) / 2),(n `2)]|,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * |[(((n `1) + (f `1)) / 2),(n `2)]|) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (n,|[(((n `1) + (f `1)) / 2),(n `2)]|)) /\ (LSeg (|[(((n `1) + (f `1)) / 2),(n `2)]|,f)) is Element of K19( the carrier of (TOP-REAL 2))
{|[(((n `1) + (f `1)) / 2),(n `2)]|} is non empty set
v is set
|[(n `1),(n `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (|[(n `1),(n `2)]|,|[(((n `1) + (f `1)) / 2),(n `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[(n `1),(n `2)]|) + (b₁ * |[(((n `1) + (f `1)) / 2),(n `2)]|)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
|[(((n `1) + (f `1)) / 2),(f `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[(f `1),(f `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (|[(((n `1) + (f `1)) / 2),(f `2)]|,|[(f `1),(f `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * |[(((n `1) + (f `1)) / 2),(f `2)]|) + (b₁ * |[(f `1),(f `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = n `2 & n `1 <= b<sub>1</sub> `1 & b₁ `1 <= ((n `1) + (f `1)) / 2 ) } is set
x is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
x `2 is V22() real ext-real Element of REAL
K434(x,2) is V22() real ext-real Element of REAL
x `1 is V22() real ext-real Element of REAL
K434(x,1) is V22() real ext-real Element of REAL
|[(((n `1) + (f `1)) / 2),(n `2)]| `1 is V22() real ext-real Element of REAL
K434(|[(((n `1) + (f `1)) / 2),(n `2)]|,1) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & ((n `1) + (f `1)) / 2 <= b₁ `1 & b<sub>1</sub> `1 <= f `1 ) } is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
|[(((n `1) + (f `1)) / 2),(n `2)]| `2 is V22() real ext-real Element of REAL
K434(|[(((n `1) + (f `1)) / 2),(n `2)]|,2) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = n `2 & ((n `1) + (f `1)) / 2 <= b₁ `1 & b<sub>1</sub> `1 <= n `1 ) } is set
x is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
x `2 is V22() real ext-real Element of REAL
K434(x,2) is V22() real ext-real Element of REAL
x `1 is V22() real ext-real Element of REAL
K434(x,1) is V22() real ext-real Element of REAL
|[(((n `1) + (f `1)) / 2),(n `2)]| `1 is V22() real ext-real Element of REAL
K434(|[(((n `1) + (f `1)) / 2),(n `2)]|,1) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & f `1 <= b<sub>1</sub> `1 & b₁ `1 <= ((n `1) + (f `1)) / 2 ) } is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
|[(((n `1) + (f `1)) / 2),(n `2)]| `2 is V22() real ext-real Element of REAL
K434(|[(((n `1) + (f `1)) / 2),(n `2)]|,2) is V22() real ext-real Element of REAL
v is set
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom n is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
f is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n | f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
Seg f is V37() V44(f) V137() V138() V139() V140() V141() V142() Element of K19(NAT)
n | (Seg f) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
dom (n | f) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
(dom n) /\ (Seg f) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
q is set
dom (n | f) is set
(n | f) . q is set
r is set
(n | f) . r is set
n . q is set
n . r is set
len (n | f) is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
len n is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
Seg (len n) is V37() V44( len n) V137() V138() V139() V140() V141() V142() Element of K19(NAT)
q is ordinal natural V22() real ext-real non negative set
q + 2 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg ((n | f),q) is Element of K19( the carrier of (TOP-REAL 2))
q + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg ((n | f),(q + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((n | f),q)) /\ (LSeg ((n | f),(q + 1))) is Element of K19( the carrier of (TOP-REAL 2))
(n | f) /. (q + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
{((n | f) /. (q + 1))} is non empty set
(q + 1) + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (n,(q + 1)) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (n,q) is Element of K19( the carrier of (TOP-REAL 2))
n /. (q + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
{(n /. (q + 1))} is non empty set
r is ordinal natural V22() real ext-real non negative set
q is ordinal natural V22() real ext-real non negative set
q + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg ((n | f),q) is Element of K19( the carrier of (TOP-REAL 2))
LSeg ((n | f),r) is Element of K19( the carrier of (TOP-REAL 2))
r + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (n,q) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (n,r) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (n,q)) /\ (LSeg (n,r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((n | f),q)) /\ (LSeg ((n | f),r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((n | f),q)) /\ (LSeg ((n | f),r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((n | f),q)) /\ (LSeg ((n | f),r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((n | f),q)) /\ (LSeg ((n | f),r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((n | f),q)) /\ (LSeg ((n | f),r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((n | f),q)) /\ (LSeg ((n | f),r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((n | f),q)) /\ (LSeg ((n | f),r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((n | f),q)) /\ (LSeg ((n | f),r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((n | f),q)) /\ (LSeg ((n | f),r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((n | f),q)) /\ (LSeg ((n | f),r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((n | f),q)) /\ (LSeg ((n | f),r)) is Element of K19( the carrier of (TOP-REAL 2))
q is ordinal natural V22() real ext-real non negative set
q + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
(n | f) /. q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((n | f) /. q) `1 is V22() real ext-real Element of REAL
K434(((n | f) /. q),1) is V22() real ext-real Element of REAL
(n | f) /. (q + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
((n | f) /. (q + 1)) `1 is V22() real ext-real Element of REAL
K434(((n | f) /. (q + 1)),1) is V22() real ext-real Element of REAL
((n | f) /. q) `2 is V22() real ext-real Element of REAL
K434(((n | f) /. q),2) is V22() real ext-real Element of REAL
((n | f) /. (q + 1)) `2 is V22() real ext-real Element of REAL
K434(((n | f) /. (q + 1)),2) is V22() real ext-real Element of REAL
n /. q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n /. (q + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
|[(n `1),(f `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
<*n,|[(n `1),(f `2)]|,f*> is Relation-like NAT -defined Function-like non empty V37() V44(3) FinSequence-like FinSubsequence-like set
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
len q is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q /. (len q) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
1 + 2 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q /. 2 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
q /. 3 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
u is ordinal natural V22() real ext-real non negative set
u + 2 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (q,u) is Element of K19( the carrier of (TOP-REAL 2))
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (q,(u + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,u)) /\ (LSeg (q,(u + 1))) is Element of K19( the carrier of (TOP-REAL 2))
q /. (u + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
{(q /. (u + 1))} is non empty set
LSeg (n,|[(n `1),(f `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(n `1),(f `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (q,2) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (n,|[(n `1),(f `2)]|)) /\ (LSeg (q,2)) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[(n `1),(f `2)]|,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[(n `1),(f `2)]|) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (n,|[(n `1),(f `2)]|)) /\ (LSeg (|[(n `1),(f `2)]|,f)) is Element of K19( the carrier of (TOP-REAL 2))
v is ordinal natural V22() real ext-real non negative set
u is ordinal natural V22() real ext-real non negative set
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (q,u) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,v) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,u)) /\ (LSeg (q,v)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,u)) /\ (LSeg (q,v)) is Element of K19( the carrier of (TOP-REAL 2))
u is ordinal natural V22() real ext-real non negative set
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q /. u is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(q /. u) `1 is V22() real ext-real Element of REAL
K434((q /. u),1) is V22() real ext-real Element of REAL
q /. (u + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(q /. (u + 1)) `1 is V22() real ext-real Element of REAL
K434((q /. (u + 1)),1) is V22() real ext-real Element of REAL
(q /. u) `2 is V22() real ext-real Element of REAL
K434((q /. u),2) is V22() real ext-real Element of REAL
(q /. (u + 1)) `2 is V22() real ext-real Element of REAL
K434((q /. (u + 1)),2) is V22() real ext-real Element of REAL
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
|[(f `1),(n `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
<*n,|[(f `1),(n `2)]|,f*> is Relation-like NAT -defined Function-like non empty V37() V44(3) FinSequence-like FinSubsequence-like set
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
len q is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q /. (len q) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
1 + 2 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q /. 2 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
q /. 3 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
u is ordinal natural V22() real ext-real non negative set
u + 2 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (q,u) is Element of K19( the carrier of (TOP-REAL 2))
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (q,(u + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,u)) /\ (LSeg (q,(u + 1))) is Element of K19( the carrier of (TOP-REAL 2))
q /. (u + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
{(q /. (u + 1))} is non empty set
LSeg (n,|[(f `1),(n `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(f `1),(n `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (q,2) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (n,|[(f `1),(n `2)]|)) /\ (LSeg (q,2)) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[(f `1),(n `2)]|,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[(f `1),(n `2)]|) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (n,|[(f `1),(n `2)]|)) /\ (LSeg (|[(f `1),(n `2)]|,f)) is Element of K19( the carrier of (TOP-REAL 2))
v is ordinal natural V22() real ext-real non negative set
u is ordinal natural V22() real ext-real non negative set
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (q,u) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,v) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,u)) /\ (LSeg (q,v)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,u)) /\ (LSeg (q,v)) is Element of K19( the carrier of (TOP-REAL 2))
u is ordinal natural V22() real ext-real non negative set
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q /. u is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(q /. u) `1 is V22() real ext-real Element of REAL
K434((q /. u),1) is V22() real ext-real Element of REAL
q /. (u + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(q /. (u + 1)) `1 is V22() real ext-real Element of REAL
K434((q /. (u + 1)),1) is V22() real ext-real Element of REAL
(q /. u) `2 is V22() real ext-real Element of REAL
K434((q /. u),2) is V22() real ext-real Element of REAL
(q /. (u + 1)) `2 is V22() real ext-real Element of REAL
K434((q /. (u + 1)),2) is V22() real ext-real Element of REAL
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
(n `2) + (f `2) is V22() real ext-real Element of REAL
((n `2) + (f `2)) / 2 is V22() real ext-real Element of REAL
|[(n `1),(((n `2) + (f `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
<*n,|[(n `1),(((n `2) + (f `2)) / 2)]|,f*> is Relation-like NAT -defined Function-like non empty V37() V44(3) FinSequence-like FinSubsequence-like set
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
len q is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q /. (len q) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
|[(n `1),(((n `2) + (f `2)) / 2)]| `2 is V22() real ext-real Element of REAL
K434(|[(n `1),(((n `2) + (f `2)) / 2)]|,2) is V22() real ext-real Element of REAL
1 + 2 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q /. 2 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
q /. 3 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
u is ordinal natural V22() real ext-real non negative set
u + 2 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (q,u) is Element of K19( the carrier of (TOP-REAL 2))
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (q,(u + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,u)) /\ (LSeg (q,(u + 1))) is Element of K19( the carrier of (TOP-REAL 2))
q /. (u + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
{(q /. (u + 1))} is non empty set
LSeg (n,|[(n `1),(((n `2) + (f `2)) / 2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(n `1),(((n `2) + (f `2)) / 2)]|)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
LSeg (q,2) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (n,|[(n `1),(((n `2) + (f `2)) / 2)]|)) /\ (LSeg (q,2)) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[(n `1),(((n `2) + (f `2)) / 2)]|,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * |[(n `1),(((n `2) + (f `2)) / 2)]|) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (n,|[(n `1),(((n `2) + (f `2)) / 2)]|)) /\ (LSeg (|[(n `1),(((n `2) + (f `2)) / 2)]|,f)) is Element of K19( the carrier of (TOP-REAL 2))
v is ordinal natural V22() real ext-real non negative set
u is ordinal natural V22() real ext-real non negative set
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (q,u) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,v) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,u)) /\ (LSeg (q,v)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,u)) /\ (LSeg (q,v)) is Element of K19( the carrier of (TOP-REAL 2))
u is ordinal natural V22() real ext-real non negative set
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q /. u is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(q /. u) `1 is V22() real ext-real Element of REAL
K434((q /. u),1) is V22() real ext-real Element of REAL
q /. (u + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(q /. (u + 1)) `1 is V22() real ext-real Element of REAL
K434((q /. (u + 1)),1) is V22() real ext-real Element of REAL
(q /. u) `2 is V22() real ext-real Element of REAL
K434((q /. u),2) is V22() real ext-real Element of REAL
(q /. (u + 1)) `2 is V22() real ext-real Element of REAL
K434((q /. (u + 1)),2) is V22() real ext-real Element of REAL
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
(n `1) + (f `1) is V22() real ext-real Element of REAL
((n `1) + (f `1)) / 2 is V22() real ext-real Element of REAL
|[(((n `1) + (f `1)) / 2),(n `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
<*n,|[(((n `1) + (f `1)) / 2),(n `2)]|,f*> is Relation-like NAT -defined Function-like non empty V37() V44(3) FinSequence-like FinSubsequence-like set
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
len q is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q /. (len q) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
|[(((n `1) + (f `1)) / 2),(n `2)]| `1 is V22() real ext-real Element of REAL
K434(|[(((n `1) + (f `1)) / 2),(n `2)]|,1) is V22() real ext-real Element of REAL
1 + 2 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q /. 2 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
q /. 3 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
u is ordinal natural V22() real ext-real non negative set
u + 2 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (q,u) is Element of K19( the carrier of (TOP-REAL 2))
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (q,(u + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,u)) /\ (LSeg (q,(u + 1))) is Element of K19( the carrier of (TOP-REAL 2))
q /. (u + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
{(q /. (u + 1))} is non empty set
LSeg (n,|[(((n `1) + (f `1)) / 2),(n `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(((n `1) + (f `1)) / 2),(n `2)]|)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
LSeg (q,2) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (n,|[(((n `1) + (f `1)) / 2),(n `2)]|)) /\ (LSeg (q,2)) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[(((n `1) + (f `1)) / 2),(n `2)]|,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * |[(((n `1) + (f `1)) / 2),(n `2)]|) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (n,|[(((n `1) + (f `1)) / 2),(n `2)]|)) /\ (LSeg (|[(((n `1) + (f `1)) / 2),(n `2)]|,f)) is Element of K19( the carrier of (TOP-REAL 2))
v is ordinal natural V22() real ext-real non negative set
u is ordinal natural V22() real ext-real non negative set
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (q,u) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,v) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,u)) /\ (LSeg (q,v)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,u)) /\ (LSeg (q,v)) is Element of K19( the carrier of (TOP-REAL 2))
u is ordinal natural V22() real ext-real non negative set
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
q /. u is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(q /. u) `1 is V22() real ext-real Element of REAL
K434((q /. u),1) is V22() real ext-real Element of REAL
q /. (u + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(q /. (u + 1)) `1 is V22() real ext-real Element of REAL
K434((q /. (u + 1)),1) is V22() real ext-real Element of REAL
(q /. u) `2 is V22() real ext-real Element of REAL
K434((q /. u),2) is V22() real ext-real Element of REAL
(q /. (u + 1)) `2 is V22() real ext-real Element of REAL
K434((q /. (u + 1)),2) is V22() real ext-real Element of REAL
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom n is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
f is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
f + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n | (f + 1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (n | (f + 1)) is Element of K19( the carrier of (TOP-REAL 2))
len (n | (f + 1)) is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
{ (LSeg ((n | (f + 1)),b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (n | (f + 1)) ) } is set
union { (LSeg ((n | (f + 1)),b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (n | (f + 1)) ) } is set
n | f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (n | f) is Element of K19( the carrier of (TOP-REAL 2))
len (n | f) is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
{ (LSeg ((n | f),b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (n | f) ) } is set
union { (LSeg ((n | f),b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (n | f) ) } is set
n /. f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n /. (f + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
LSeg ((n /. f),(n /. (f + 1))) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (n /. f)) + (b₁ * (n /. (f + 1)))) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(L~ (n | f)) \/ (LSeg ((n /. f),(n /. (f + 1)))) is Element of K19( the carrier of (TOP-REAL 2))
len n is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
Seg (f + 1) is non empty V37() V44(f + 1) V137() V138() V139() V140() V141() V142() Element of K19(NAT)
Seg (len n) is V37() V44( len n) V137() V138() V139() V140() V141() V142() Element of K19(NAT)
(dom n) /\ (Seg (f + 1)) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
n | (Seg (f + 1)) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
dom (n | (Seg (f + 1))) is set
LSeg (n,f) is Element of K19( the carrier of (TOP-REAL 2))
dom (n | (f + 1)) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
LSeg ((n | (f + 1)),f) is Element of K19( the carrier of (TOP-REAL 2))
Seg f is V37() V44(f) V137() V138() V139() V140() V141() V142() Element of K19(NAT)
(dom n) /\ (Seg f) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
n | (Seg f) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
dom (n | (Seg f)) is set
Seg (len (n | (f + 1))) is V37() V44( len (n | (f + 1))) V137() V138() V139() V140() V141() V142() Element of K19(NAT)
x is set
qp is set
pp1 is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg ((n | (f + 1)),pp1) is Element of K19( the carrier of (TOP-REAL 2))
pp1 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
dom (n | f) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
LSeg (n,pp1) is Element of K19( the carrier of (TOP-REAL 2))
LSeg ((n | f),pp1) is Element of K19( the carrier of (TOP-REAL 2))
x is set
qp is set
pp1 is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg ((n | f),pp1) is Element of K19( the carrier of (TOP-REAL 2))
pp1 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
dom (n | f) is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
LSeg (n,pp1) is Element of K19( the carrier of (TOP-REAL 2))
LSeg ((n | (f + 1)),pp1) is Element of K19( the carrier of (TOP-REAL 2))
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
L~ f is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (f,b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
union { (LSeg (f,b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
r is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
f /. r is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
(len f) - 1 is V22() real ext-real Element of REAL
1 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
u is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
u + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
f /. (u + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
LSeg (f,u) is Element of K19( the carrier of (TOP-REAL 2))
r + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (f,r) is Element of K19( the carrier of (TOP-REAL 2))
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
{n} is non empty set
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
LSeg (n,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
len q is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
{ (LSeg (q,b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len q ) } is set
union { (LSeg (q,b₁)) where b₁ is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len q ) } is set
(LSeg (n,f)) /\ (L~ q) is Element of K19( the carrier of (TOP-REAL 2))
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len n is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n /. (len n) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
LSeg (n,f) is Element of K19( the carrier of (TOP-REAL 2))
f + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
(f + 1) + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
1 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
f + (1 + 1) is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
(len n) - 1 is V22() real ext-real Element of REAL
r is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
r + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
dom n is V137() V138() V139() V140() V141() V142() Element of K19(NAT)
f + 2 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
n /. (f + 2) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
LSeg (n,(f + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (n,f)) /\ (LSeg (n,(f + 1))) is Element of K19( the carrier of (TOP-REAL 2))
n /. (f + 1) is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
{(n /. (f + 1))} is non empty set
(1 + 1) - 1 is V22() real ext-real Element of REAL
LSeg (n,r) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (n,f)) /\ (LSeg (n,r)) is Element of K19( the carrier of (TOP-REAL 2))
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
LSeg (n,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
{f} is non empty set
q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
q `1 is V22() real ext-real Element of REAL
K434(q,1) is V22() real ext-real Element of REAL
q `2 is V22() real ext-real Element of REAL
K434(q,2) is V22() real ext-real Element of REAL
LSeg (f,q) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * f) + (b₁ * q)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (n,f)) /\ (LSeg (f,q)) is Element of K19( the carrier of (TOP-REAL 2))
r is V22() real ext-real set
u is Element of the carrier of (Euclid 2)
Ball (u,r) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
|[(q `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[(n `1),(n `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[(f `1),(f `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
LSeg (q,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * q) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = q `1 & q `2 <= b<sub>1</sub> `2 & b₁ `2 <= f `2 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = q `1 & f `2 <= b<sub>1</sub> `2 & b₁ `2 <= q `2 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = q `1 & q `2 <= b<sub>1</sub> `2 & b₁ `2 <= n `2 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = q `1 & n `2 <= b<sub>1</sub> `2 & b₁ `2 <= q `2 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = q `1 & f `2 <= b<sub>1</sub> `2 & b₁ `2 <= n `2 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = q `1 & n `2 <= b<sub>1</sub> `2 & b₁ `2 <= f `2 ) } is set
LSeg (q,n) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * q) + (b₁ * n)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (n,q) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * q)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = q `2 & q `1 <= b<sub>1</sub> `1 & b₁ `1 <= f `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = q `2 & f `1 <= b<sub>1</sub> `1 & b₁ `1 <= q `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = q `2 & q `1 <= b<sub>1</sub> `1 & b₁ `1 <= n `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = q `2 & n `1 <= b<sub>1</sub> `1 & b₁ `1 <= q `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = q `2 & f `1 <= b<sub>1</sub> `1 & b₁ `1 <= n `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = q `2 & n `1 <= b<sub>1</sub> `1 & b₁ `1 <= f `1 ) } is set
LSeg (q,n) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * q) + (b₁ * n)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (n,q) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * q)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
LSeg (n,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
{f} is non empty set
q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
q `2 is V22() real ext-real Element of REAL
K434(q,2) is V22() real ext-real Element of REAL
|[(f `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
q `1 is V22() real ext-real Element of REAL
K434(q,1) is V22() real ext-real Element of REAL
LSeg (f,|[(f `1),(q `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * f) + (b<sub>1</sub> * |[(f `1),(q `2)]|)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
LSeg (|[(f `1),(q `2)]|,q) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * |[(f `1),(q `2)]|) + (b<sub>1</sub> * q)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
(LSeg (f,|[(f `1),(q `2)]|)) \/ (LSeg (|[(f `1),(q `2)]|,q)) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,|[(f `1),(q `2)]|)) \/ (LSeg (|[(f `1),(q `2)]|,q))) /\ (LSeg (n,f)) is Element of K19( the carrier of (TOP-REAL 2))
r is V22() real ext-real set
u is Element of the carrier of (Euclid 2)
Ball (u,r) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
(LSeg (f,|[(f `1),(q `2)]|)) /\ (LSeg (n,f)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[(f `1),(q `2)]|,q)) /\ (LSeg (n,f)) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,|[(f `1),(q `2)]|)) /\ (LSeg (n,f))) \/ ((LSeg (|[(f `1),(q `2)]|,q)) /\ (LSeg (n,f))) is Element of K19( the carrier of (TOP-REAL 2))
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
|[(f `1),(n `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[(q `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[(f `1),(f `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[(f `1),(q `2)]| `1 is V22() real ext-real Element of REAL
K434(|[(f `1),(q `2)]|,1) is V22() real ext-real Element of REAL
|[(f `1),(q `2)]| `2 is V22() real ext-real Element of REAL
K434(|[(f `1),(q `2)]|,2) is V22() real ext-real Element of REAL
x is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & |[(f `1),(q `2)]| `2 <= b<sub>1</sub> `2 & b₁ `2 <= n `2 ) } is set
LSeg (n,|[(f `1),(q `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(f `1),(q `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = q `2 & q `1 <= b<sub>1</sub> `1 & b₁ `1 <= f `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & f `2 <= b<sub>1</sub> `2 & b₁ `2 <= n `2 ) } is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
pp1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
pp1 `2 is V22() real ext-real Element of REAL
K434(pp1,2) is V22() real ext-real Element of REAL
pp1 `1 is V22() real ext-real Element of REAL
K434(pp1,1) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & f `2 <= b<sub>1</sub> `2 & b₁ `2 <= |[(f `1),(q `2)]| `2 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & f `2 <= b<sub>1</sub> `2 & b₁ `2 <= n `2 ) } is set
x is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & |[(f `1),(q `2)]| `2 <= b<sub>1</sub> `2 & b₁ `2 <= n `2 ) } is set
LSeg (n,|[(f `1),(q `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(f `1),(q `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = q `2 & f `1 <= b<sub>1</sub> `1 & b₁ `1 <= q `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & f `2 <= b<sub>1</sub> `2 & b₁ `2 <= n `2 ) } is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
pp1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
pp1 `2 is V22() real ext-real Element of REAL
K434(pp1,2) is V22() real ext-real Element of REAL
pp1 `1 is V22() real ext-real Element of REAL
K434(pp1,1) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & f `2 <= b<sub>1</sub> `2 & b₁ `2 <= |[(f `1),(q `2)]| `2 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & f `2 <= b<sub>1</sub> `2 & b₁ `2 <= n `2 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & n `2 <= b<sub>1</sub> `2 & b₁ `2 <= f `2 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & |[(f `1),(q `2)]| `2 <= b<sub>1</sub> `2 & b₁ `2 <= f `2 ) } is set
x is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & n `2 <= b<sub>1</sub> `2 & b₁ `2 <= |[(f `1),(q `2)]| `2 ) } is set
LSeg (n,|[(f `1),(q `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(f `1),(q `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = q `2 & q `1 <= b<sub>1</sub> `1 & b₁ `1 <= f `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & n `2 <= b<sub>1</sub> `2 & b₁ `2 <= f `2 ) } is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
pp1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
pp1 `2 is V22() real ext-real Element of REAL
K434(pp1,2) is V22() real ext-real Element of REAL
pp1 `1 is V22() real ext-real Element of REAL
K434(pp1,1) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & n `2 <= b<sub>1</sub> `2 & b₁ `2 <= f `2 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & |[(f `1),(q `2)]| `2 <= b<sub>1</sub> `2 & b₁ `2 <= f `2 ) } is set
x is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & n `2 <= b<sub>1</sub> `2 & b₁ `2 <= |[(f `1),(q `2)]| `2 ) } is set
LSeg (n,|[(f `1),(q `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(f `1),(q `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = q `2 & f `1 <= b<sub>1</sub> `1 & b₁ `1 <= q `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = f `1 & n `2 <= b<sub>1</sub> `2 & b₁ `2 <= f `2 ) } is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
pp1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
pp1 `2 is V22() real ext-real Element of REAL
K434(pp1,2) is V22() real ext-real Element of REAL
pp1 `1 is V22() real ext-real Element of REAL
K434(pp1,1) is V22() real ext-real Element of REAL
n is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
n `2 is V22() real ext-real Element of REAL
K434(n,2) is V22() real ext-real Element of REAL
f is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
f `2 is V22() real ext-real Element of REAL
K434(f,2) is V22() real ext-real Element of REAL
LSeg (n,f) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * f)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
f `1 is V22() real ext-real Element of REAL
K434(f,1) is V22() real ext-real Element of REAL
{f} is non empty set
q is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
q `1 is V22() real ext-real Element of REAL
K434(q,1) is V22() real ext-real Element of REAL
|[(q `1),(f `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
q `2 is V22() real ext-real Element of REAL
K434(q,2) is V22() real ext-real Element of REAL
LSeg (f,|[(q `1),(f `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * f) + (b<sub>1</sub> * |[(q `1),(f `2)]|)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
LSeg (|[(q `1),(f `2)]|,q) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * |[(q `1),(f `2)]|) + (b<sub>1</sub> * q)) where b<sub>1</sub> is V22() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
(LSeg (f,|[(q `1),(f `2)]|)) \/ (LSeg (|[(q `1),(f `2)]|,q)) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,|[(q `1),(f `2)]|)) \/ (LSeg (|[(q `1),(f `2)]|,q))) /\ (LSeg (n,f)) is Element of K19( the carrier of (TOP-REAL 2))
r is V22() real ext-real set
u is Element of the carrier of (Euclid 2)
Ball (u,r) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
n `1 is V22() real ext-real Element of REAL
K434(n,1) is V22() real ext-real Element of REAL
|[(n `1),(f `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
(LSeg (f,|[(q `1),(f `2)]|)) /\ (LSeg (n,f)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[(q `1),(f `2)]|,q)) /\ (LSeg (n,f)) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,|[(q `1),(f `2)]|)) /\ (LSeg (n,f))) \/ ((LSeg (|[(q `1),(f `2)]|,q)) /\ (LSeg (n,f))) is Element of K19( the carrier of (TOP-REAL 2))
|[(q `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[(f `1),(f `2)]| is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of the carrier of (TOP-REAL 2)
|[(q `1),(f `2)]| `2 is V22() real ext-real Element of REAL
K434(|[(q `1),(f `2)]|,2) is V22() real ext-real Element of REAL
|[(q `1),(f `2)]| `1 is V22() real ext-real Element of REAL
K434(|[(q `1),(f `2)]|,1) is V22() real ext-real Element of REAL
x is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & |[(q `1),(f `2)]| `1 <= b<sub>1</sub> `1 & b₁ `1 <= n `1 ) } is set
LSeg (n,|[(q `1),(f `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(q `1),(f `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (q,|[(q `1),(f `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * q) + (b₁ * |[(q `1),(f `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = q `1 & q `2 <= b<sub>1</sub> `2 & b₁ `2 <= f `2 ) } is set
LSeg (f,n) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * f) + (b₁ * n)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & f `1 <= b<sub>1</sub> `1 & b₁ `1 <= n `1 ) } is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
pp1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
pp1 `1 is V22() real ext-real Element of REAL
K434(pp1,1) is V22() real ext-real Element of REAL
pp1 `2 is V22() real ext-real Element of REAL
K434(pp1,2) is V22() real ext-real Element of REAL
x is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & |[(q `1),(f `2)]| `1 <= b<sub>1</sub> `1 & b₁ `1 <= n `1 ) } is set
LSeg (n,|[(q `1),(f `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(q `1),(f `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & f `1 <= b<sub>1</sub> `1 & b₁ `1 <= n `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = q `1 & |[(q `1),(f `2)]| `2 <= b<sub>1</sub> `2 & b₁ `2 <= q `2 ) } is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
pp1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
pp1 `2 is V22() real ext-real Element of REAL
K434(pp1,2) is V22() real ext-real Element of REAL
pp1 `1 is V22() real ext-real Element of REAL
K434(pp1,1) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & f `1 <= b<sub>1</sub> `1 & b₁ `1 <= |[(q `1),(f `2)]| `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & f `1 <= b<sub>1</sub> `1 & b₁ `1 <= n `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & n `1 <= b<sub>1</sub> `1 & b₁ `1 <= f `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & |[(q `1),(f `2)]| `1 <= b<sub>1</sub> `1 & b₁ `1 <= f `1 ) } is set
x is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & n `1 <= b<sub>1</sub> `1 & b₁ `1 <= |[(q `1),(f `2)]| `1 ) } is set
LSeg (n,|[(q `1),(f `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(q `1),(f `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = q `1 & q `2 <= b<sub>1</sub> `2 & b₁ `2 <= f `2 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & n `1 <= b<sub>1</sub> `1 & b₁ `1 <= f `1 ) } is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
pp1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
pp1 `1 is V22() real ext-real Element of REAL
K434(pp1,1) is V22() real ext-real Element of REAL
pp1 `2 is V22() real ext-real Element of REAL
K434(pp1,2) is V22() real ext-real Element of REAL
x is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & n `1 <= b<sub>1</sub> `1 & b₁ `1 <= |[(q `1),(f `2)]| `1 ) } is set
LSeg (n,|[(q `1),(f `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * n) + (b₁ * |[(q `1),(f `2)]|)) where b₁ is V22() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = f `2 & n `1 <= b<sub>1</sub> `1 & b₁ `1 <= f `1 ) } is set
{ b₁ where b₁ is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = q `1 & |[(q `1),(f `2)]| `2 <= b<sub>1</sub> `2 & b₁ `2 <= q `2 ) } is set
qp is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
qp `1 is V22() real ext-real Element of REAL
K434(qp,1) is V22() real ext-real Element of REAL
qp `2 is V22() real ext-real Element of REAL
K434(qp,2) is V22() real ext-real Element of REAL
pp1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2)
pp1 `2 is V22() real ext-real Element of REAL
K434(pp1,2) is V22() real ext-real Element of REAL
pp1 `1 is V22() real ext-real Element of REAL
K434(pp1,1) is V22() real ext-real Element of REAL
n is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
Euclid n is non empty strict Reflexive discerning V86() triangle MetrStruct
REAL n is functional non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist n is Relation-like K20((REAL n),(REAL n)) -defined REAL -valued Function-like V30(K20((REAL n),(REAL n)), REAL ) complex-yielding V128() V129() Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is set
K20(K20((REAL n),(REAL n)),REAL) is complex-yielding V128() V129() set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
len f is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() Element of REAL * : len b₁ = n } is set
n is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
TOP-REAL n is non empty TopSpace-like V103() V149() V150() V151() V152() V153() V154() V155() strict RLTopStruct
the carrier of (TOP-REAL n) is non empty set
f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-yielding V128() V129() FinSequence of REAL
len f is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT
Euclid n is non empty strict Reflexive discerning V86() triangle MetrStruct
REAL n is functional non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist n is Relation-like K20((REAL n),(REAL n)) -defined REAL -valued Function-like V30(K20((REAL n),(REAL n)), REAL ) complex-yielding V128() V129() Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is set
K20(K20((REAL n),(REAL n)),REAL) is complex-yielding V128() V129() set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set