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
{ b1 where b1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b1 `1 = q & n <= b1 `2 & b1 `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 - b1) * |[q,n]|) + (b1 * |[q,f]|)) where b1 is V22() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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
{ b1 where b1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b1 `2 = q & n <= b1 `1 & b1 `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 - b1) * |[n,q]|) + (b1 * |[f,q]|)) where b1 is V22() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * |[f,q]|) + (b1 * |[f,r]|)) where b1 is V22() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
{ b1 where b1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b1 `1 = f & q <= b1 `2 & b1 `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
{ b1 where b1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b1 `1 = f & r <= b1 `2 & b1 `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 - b1) * |[f,q]|) + (b1 * |[r,q]|)) where b1 is V22() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
{ b1 where b1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b1 `2 = q & f <= b1 `1 & b1 `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
{ b1 where b1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b1 `2 = q & r <= b1 `1 & b1 `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 - b1) * n) + (b1 * f)) where b1 is V22() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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
{ b1 where b1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b1 `2 = n `2 & n `1 <= b1 `1 & b1 `1 <= f `1 ) } is set
{ b1 where b1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b1 `2 = n `2 & f `1 <= b1 `1 & b1 `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 - b1) * n) + (b1 * f)) where b1 is V22() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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
{ b1 where b1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b1 `1 = n `1 & n `2 <= b1 `2 & b1 `2 <= f `2 ) } is set
{ b1 where b1 is V44(2) FinSequence-like V129() Element of the carrier of (TOP-REAL 2) : ( b1 `1 = n `1 & f `2 <= b1 `2 & b1 `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 - b1) * n) + (b1 * f)) where b1 is V22() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * f) + (b1 * q)) where b1 is V22() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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,b1)) where b1 is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b1 & b1 + 1 <= len r ) } is set
union { (LSeg (r,b1)) where b1 is ordinal natural V22() real ext-real non negative V33() V34() V137() V138() V139() V140() V141() V142() Element of NAT : ( 1 <= b1 & b1 + 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 - b1) * ((n | q) /. f)) + (b1 * ((n | q) /. (f + 1)))) where b1 is V22() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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