:: JORDAN2B semantic presentation

REAL is non empty V35() V130() V131() V132() V136() set
NAT is V130() V131() V132() V133() V134() V135() V136() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V35() V130() V136() set
omega is V130() V131() V132() V133() V134() V135() V136() set
K6(omega) is set
K6(NAT) is set
K196(NAT) is V50() set
K336() is V118() TopStruct
the carrier of K336() is V130() V131() V132() set
1 is non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
K7(1,1) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
RAT is non empty V35() V130() V131() V132() V133() V136() set
INT is non empty V35() V130() V131() V132() V133() V134() V136() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is complex-yielding V120() V121() set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is complex-yielding V120() V121() set
K7(K7(REAL,REAL),REAL) is complex-yielding V120() V121() set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
K7(2,2) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K7(K7(2,2),REAL) is complex-yielding V120() V121() set
K6(K7(K7(2,2),REAL)) is set
RealSpace is non empty strict Reflexive discerning V111() triangle Discerning V118() MetrStruct
R^1 is non empty strict TopSpace-like V118() TopStruct
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL 2) is non empty set
K7( the carrier of (TOP-REAL 2),REAL) is complex-yielding V120() V121() set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is set
K6( the carrier of (TOP-REAL 2)) is set
K7(COMPLEX,COMPLEX) is complex-yielding set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-yielding set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is RAT -valued complex-yielding V120() V121() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is RAT -valued complex-yielding V120() V121() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is RAT -valued INT -valued complex-yielding V120() V121() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is RAT -valued INT -valued complex-yielding V120() V121() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7(K7(NAT,NAT),NAT)) is set
K627() is non empty V155() L10()
the carrier of K627() is non empty set
K632() is non empty V155() V199() V200() V201() V203() V229() V230() V231() V232() V233() V234() L10()
K633() is non empty V155() V201() V203() V232() V233() V234() M22(K632())
K634() is non empty V155() V199() V201() V203() V232() V233() V234() V235() M25(K632(),K633())
K636() is non empty V155() V199() V201() V203() L10()
K637() is non empty V155() V199() V201() V203() V235() M22(K636())
{} is empty functional FinSequence-membered V130() V131() V132() V133() V134() V135() V136() set
0 is empty natural V11() real ext-real non positive non negative functional FinSequence-membered V51() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
3 is non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
the carrier of RealSpace is non empty V130() V131() V132() set
TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct
the carrier of R^1 is non empty V130() V131() V132() set
real_dist is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
Seg 1 is non empty V35() V42(1) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
proj1 is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj2 is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
p is natural V11() real ext-real set
TOP-REAL p is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL p) is non empty set
r1 is natural V11() real ext-real set
r2 is Relation-like NAT -defined Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
REAL p is non empty functional FinSequence-membered FinSequenceSet of REAL
p -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p } is set
g is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL *
len g is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
g /. r1 is V11() real ext-real Element of REAL
p is natural V11() real ext-real set
TOP-REAL p is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL p) is non empty set
r1 is Relation-like NAT -defined Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
r2 is set
rng r1 is V130() V131() V132() set
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r1 is natural V11() real ext-real set
TOP-REAL r1 is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL r1) is non empty set
K7( the carrier of (TOP-REAL r1), the carrier of R^1) is complex-yielding V120() V121() set
K6(K7( the carrier of (TOP-REAL r1), the carrier of R^1)) is set
REAL r1 is non empty functional FinSequence-membered FinSequenceSet of REAL
r1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = r1 } is set
r2 is set
g is Relation-like NAT -defined REAL -valued Function-like V35() V42(r1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL r1)
r is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
f1 is V11() real ext-real Element of REAL
r /. p is V11() real ext-real Element of REAL
u is Relation-like NAT -defined REAL -valued Function-like V35() V42(r1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL r1)
u /. p is V11() real ext-real Element of REAL
K7((REAL r1),REAL) is complex-yielding V120() V121() set
K6(K7((REAL r1),REAL)) is set
r2 is non empty Relation-like REAL r1 -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7((REAL r1),REAL))
r2 is non empty Relation-like REAL r1 -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7((REAL r1),REAL))
g is non empty Relation-like the carrier of (TOP-REAL r1) -defined the carrier of R^1 -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7( the carrier of (TOP-REAL r1), the carrier of R^1))
f1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(r1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL r1)
g . f1 is V11() real ext-real Element of the carrier of R^1
f1 /. p is V11() real ext-real Element of REAL
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
Seg p is V35() V42(p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
TOP-REAL p is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
0. (TOP-REAL p) is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like V62( TOP-REAL p) complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
the carrier of (TOP-REAL p) is non empty set
the ZeroF of (TOP-REAL p) is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
r1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(0. (TOP-REAL p)) /. r1 is V11() real ext-real Element of REAL
0* p is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
REAL p is non empty functional FinSequence-membered FinSequenceSet of REAL
p -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p } is set
p |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
K131((Seg p),0) is Relation-like Seg p -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() V122() Element of K6(K7((Seg p),{0}))
{0} is non empty V130() V131() V132() V133() V134() V135() set
K7((Seg p),{0}) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7((Seg p),{0})) is set
len (0* p) is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
dom (0* p) is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
(0* p) /. r1 is V11() real ext-real Element of REAL
(0* p) . r1 is V11() real ext-real set
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
TOP-REAL p is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL p) is non empty set
Seg p is V35() V42(p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r1 is V11() real ext-real set
r2 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
r1 * r2 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
r1 * r2 is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
K605(r1) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K564() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K129(K564(),r1,(id REAL)) is set
r2 (#) K605(r1) is Relation-like complex-yielding V120() V121() set
g is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(r1 * r2) /. g is V11() real ext-real Element of REAL
r2 /. g is V11() real ext-real Element of REAL
r1 * (r2 /. g) is V11() real ext-real Element of REAL
REAL p is non empty functional FinSequence-membered FinSequenceSet of REAL
p -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p } is set
f1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
len f1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
Seg (len f1) is V35() V42( len f1) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
dom f1 is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
u is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
len u is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
dom u is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
r . g is V11() real ext-real set
u . g is V11() real ext-real set
r1 * r is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
r (#) K605(r1) is Relation-like complex-yielding V120() V121() set
(r1 * r) . g is V11() real ext-real set
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
TOP-REAL p is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL p) is non empty set
Seg p is V35() V42(p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
- r1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
- r1 is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
K560() is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
r1 (#) K560() is Relation-like complex-yielding V120() V121() set
- 1 is V11() real ext-real non positive set
(- 1) * r1 is Relation-like Function-like set
K605((- 1)) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K564() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K129(K564(),(- 1),(id REAL)) is set
r1 (#) K605((- 1)) is Relation-like complex-yielding V120() V121() set
r2 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(- r1) /. r2 is V11() real ext-real Element of REAL
r1 /. r2 is V11() real ext-real Element of REAL
- (r1 /. r2) is V11() real ext-real Element of REAL
REAL p is non empty functional FinSequence-membered FinSequenceSet of REAL
p -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p } is set
g is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
len g is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
dom g is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
f1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
f1 . r2 is V11() real ext-real set
r is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
len r is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
dom r is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r . r2 is V11() real ext-real set
- f1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
f1 (#) K560() is Relation-like complex-yielding V120() V121() set
(- 1) * f1 is Relation-like Function-like set
f1 (#) K605((- 1)) is Relation-like complex-yielding V120() V121() set
(- f1) . r2 is V11() real ext-real set
- 1 is V11() real ext-real non positive Element of REAL
(- 1) * (r1 /. r2) is V11() real ext-real Element of REAL
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
TOP-REAL p is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL p) is non empty set
Seg p is V35() V42(p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
r2 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
r1 + r2 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
r1 + r2 is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
K562() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K127(K562(),r1,r2) is set
g is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(r1 + r2) /. g is V11() real ext-real Element of REAL
r1 /. g is V11() real ext-real Element of REAL
r2 /. g is V11() real ext-real Element of REAL
(r1 /. g) + (r2 /. g) is V11() real ext-real Element of REAL
REAL p is non empty functional FinSequence-membered FinSequenceSet of REAL
p -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p } is set
f1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
u is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
s1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
len s1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
Seg (len s1) is V35() V42( len s1) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
dom s1 is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
len u is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
dom u is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
P is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
P . g is V11() real ext-real set
len f1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
dom f1 is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
r . g is V11() real ext-real set
s1 . g is V11() real ext-real set
r + P is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
K127(K562(),r,P) is set
(r + P) . g is V11() real ext-real set
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
TOP-REAL p is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL p) is non empty set
Seg p is V35() V42(p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
r2 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
r1 - r2 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
r1 - r2 is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
K563() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K562() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K560() is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K562() * ((id REAL),K560()) is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K127(K563(),r1,r2) is set
K420(r2) is Relation-like Function-like complex-yielding set
r2 (#) K560() is Relation-like complex-yielding V120() V121() set
- 1 is V11() real ext-real non positive set
(- 1) * r2 is Relation-like Function-like set
K605((- 1)) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K564() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K129(K564(),(- 1),(id REAL)) is set
r2 (#) K605((- 1)) is Relation-like complex-yielding V120() V121() set
K391(r1,K420(r2)) is Relation-like Function-like set
g is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(r1 - r2) /. g is V11() real ext-real Element of REAL
r1 /. g is V11() real ext-real Element of REAL
r2 /. g is V11() real ext-real Element of REAL
(r1 /. g) - (r2 /. g) is V11() real ext-real Element of REAL
REAL p is non empty functional FinSequence-membered FinSequenceSet of REAL
p -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p } is set
f1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
u is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
len u is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
Seg (len u) is V35() V42( len u) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
dom u is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
len f1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
dom f1 is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
r . g is V11() real ext-real set
s1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
len s1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
dom s1 is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
P is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
P . g is V11() real ext-real set
s1 . g is V11() real ext-real set
r - P is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
K127(K563(),r,P) is set
K420(P) is Relation-like Function-like complex-yielding set
P (#) K560() is Relation-like complex-yielding V120() V121() set
(- 1) * P is Relation-like Function-like set
P (#) K605((- 1)) is Relation-like complex-yielding V120() V121() set
K391(r,K420(P)) is Relation-like Function-like set
(r - P) . g is V11() real ext-real set
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
0* p is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
REAL p is non empty functional FinSequence-membered FinSequenceSet of REAL
p -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p } is set
p |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
Seg p is V35() V42(p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
K131((Seg p),0) is Relation-like Seg p -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() V122() Element of K6(K7((Seg p),{0}))
{0} is non empty V130() V131() V132() V133() V134() V135() set
K7((Seg p),{0}) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7((Seg p),{0})) is set
r1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
0* r1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(r1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL r1
REAL r1 is non empty functional FinSequence-membered FinSequenceSet of REAL
r1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = r1 } is set
r1 |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V35() V42(r1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of r1 -tuples_on REAL
Seg r1 is V35() V42(r1) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
K131((Seg r1),0) is Relation-like Seg r1 -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() V122() Element of K6(K7((Seg r1),{0}))
K7((Seg r1),{0}) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7((Seg r1),{0})) is set
(0* r1) | p is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
len (0* r1) is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
len ((0* r1) | p) is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r2 is natural V11() real ext-real set
((0* r1) | p) . r2 is V11() real ext-real set
(0* p) . r2 is V11() real ext-real set
(r1 |-> 0) . r2 is V11() real ext-real set
len (0* p) is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
0* p is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
REAL p is non empty functional FinSequence-membered FinSequenceSet of REAL
p -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p } is set
p |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
Seg p is V35() V42(p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
K131((Seg p),0) is Relation-like Seg p -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() V122() Element of K6(K7((Seg p),{0}))
{0} is non empty V130() V131() V132() V133() V134() V135() set
K7((Seg p),{0}) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7((Seg p),{0})) is set
r1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(0* p) /^ r1 is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
p -' r1 is natural V11() real ext-real non negative V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
0* (p -' r1) is Relation-like NAT -defined REAL -valued Function-like V35() V42(p -' r1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL (p -' r1)
REAL (p -' r1) is non empty functional FinSequence-membered FinSequenceSet of REAL
(p -' r1) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p -' r1 } is set
(p -' r1) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V35() V42(p -' r1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of (p -' r1) -tuples_on REAL
Seg (p -' r1) is V35() V42(p -' r1) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
K131((Seg (p -' r1)),0) is Relation-like Seg (p -' r1) -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() V122() Element of K6(K7((Seg (p -' r1)),{0}))
K7((Seg (p -' r1)),{0}) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7((Seg (p -' r1)),{0})) is set
len ((0* p) /^ r1) is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
len (0* p) is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(len (0* p)) -' r1 is natural V11() real ext-real non negative V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r2 is natural V11() real ext-real set
((0* p) /^ r1) . r2 is V11() real ext-real set
(0* (p -' r1)) . r2 is V11() real ext-real set
r1 - r1 is V11() real ext-real set
p - r1 is V11() real ext-real set
r2 + r1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(p - r1) + r1 is V11() real ext-real set
dom ((0* p) /^ r1) is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
(p |-> 0) . (r2 + r1) is V11() real ext-real set
<*> REAL is empty Relation-like NAT -defined REAL -valued Function-like functional V35() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V120() V121() V122() V130() V131() V132() V133() V134() V135() V136() FinSequence of REAL
(<*> REAL) . r2 is natural V11() real ext-real set
len (0* (p -' r1)) is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
0* p is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
REAL p is non empty functional FinSequence-membered FinSequenceSet of REAL
p -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p } is set
p |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
Seg p is V35() V42(p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
K131((Seg p),0) is Relation-like Seg p -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() V122() Element of K6(K7((Seg p),{0}))
{0} is non empty V130() V131() V132() V133() V134() V135() set
K7((Seg p),{0}) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7((Seg p),{0})) is set
Sum (0* p) is V11() real ext-real Element of REAL
K562() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K197(REAL,(0* p),K562()) is V11() real ext-real Element of REAL
p * 0 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
Seg r1 is V35() V42(r1) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
0* r1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(r1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL r1
REAL r1 is non empty functional FinSequence-membered FinSequenceSet of REAL
r1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = r1 } is set
r1 |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V35() V42(r1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of r1 -tuples_on REAL
K131((Seg r1),0) is Relation-like Seg r1 -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() V122() Element of K6(K7((Seg r1),{0}))
{0} is non empty V130() V131() V132() V133() V134() V135() set
K7((Seg r1),{0}) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7((Seg r1),{0})) is set
r2 is V11() real ext-real Element of REAL
(0* r1) +* (p,r2) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
Sum ((0* r1) +* (p,r2)) is V11() real ext-real Element of REAL
K562() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K197(REAL,((0* r1) +* (p,r2)),K562()) is V11() real ext-real Element of REAL
len (0* r1) is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
dom (0* r1) is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
g is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
g +* (p,r2) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (g +* (p,r2)) is V11() real ext-real Element of REAL
K197(REAL,(g +* (p,r2)),K562()) is V11() real ext-real Element of REAL
p -' 1 is natural V11() real ext-real non negative V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
g | (p -' 1) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
<*r2*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
(g | (p -' 1)) ^ <*r2*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
g /^ p is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
((g | (p -' 1)) ^ <*r2*>) ^ (g /^ p) is non empty Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (((g | (p -' 1)) ^ <*r2*>) ^ (g /^ p)) is V11() real ext-real Element of REAL
K197(REAL,(((g | (p -' 1)) ^ <*r2*>) ^ (g /^ p)),K562()) is V11() real ext-real Element of REAL
(0* r1) | (p -' 1) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
((0* r1) | (p -' 1)) ^ <*r2*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (((0* r1) | (p -' 1)) ^ <*r2*>) is V11() real ext-real Element of REAL
K197(REAL,(((0* r1) | (p -' 1)) ^ <*r2*>),K562()) is V11() real ext-real Element of REAL
(0* r1) /^ p is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
Sum ((0* r1) /^ p) is V11() real ext-real Element of REAL
K197(REAL,((0* r1) /^ p),K562()) is V11() real ext-real Element of REAL
(Sum (((0* r1) | (p -' 1)) ^ <*r2*>)) + (Sum ((0* r1) /^ p)) is V11() real ext-real Element of REAL
Sum ((0* r1) | (p -' 1)) is V11() real ext-real Element of REAL
K197(REAL,((0* r1) | (p -' 1)),K562()) is V11() real ext-real Element of REAL
Sum <*r2*> is V11() real ext-real Element of REAL
K197(REAL,<*r2*>,K562()) is V11() real ext-real Element of REAL
(Sum ((0* r1) | (p -' 1))) + (Sum <*r2*>) is V11() real ext-real Element of REAL
((Sum ((0* r1) | (p -' 1))) + (Sum <*r2*>)) + (Sum ((0* r1) /^ p)) is V11() real ext-real Element of REAL
(Sum ((0* r1) | (p -' 1))) + r2 is V11() real ext-real Element of REAL
((Sum ((0* r1) | (p -' 1))) + r2) + (Sum ((0* r1) /^ p)) is V11() real ext-real Element of REAL
0* (p -' 1) is Relation-like NAT -defined REAL -valued Function-like V35() V42(p -' 1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL (p -' 1)
REAL (p -' 1) is non empty functional FinSequence-membered FinSequenceSet of REAL
(p -' 1) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p -' 1 } is set
(p -' 1) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V35() V42(p -' 1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of (p -' 1) -tuples_on REAL
Seg (p -' 1) is V35() V42(p -' 1) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
K131((Seg (p -' 1)),0) is Relation-like Seg (p -' 1) -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() V122() Element of K6(K7((Seg (p -' 1)),{0}))
K7((Seg (p -' 1)),{0}) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7((Seg (p -' 1)),{0})) is set
Sum (0* (p -' 1)) is V11() real ext-real Element of REAL
K197(REAL,(0* (p -' 1)),K562()) is V11() real ext-real Element of REAL
(Sum (0* (p -' 1))) + r2 is V11() real ext-real Element of REAL
((Sum (0* (p -' 1))) + r2) + (Sum ((0* r1) /^ p)) is V11() real ext-real Element of REAL
0 + r2 is V11() real ext-real Element of REAL
(0 + r2) + (Sum ((0* r1) /^ p)) is V11() real ext-real Element of REAL
r1 -' p is natural V11() real ext-real non negative V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
0* (r1 -' p) is Relation-like NAT -defined REAL -valued Function-like V35() V42(r1 -' p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL (r1 -' p)
REAL (r1 -' p) is non empty functional FinSequence-membered FinSequenceSet of REAL
(r1 -' p) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = r1 -' p } is set
(r1 -' p) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V35() V42(r1 -' p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of (r1 -' p) -tuples_on REAL
Seg (r1 -' p) is V35() V42(r1 -' p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
K131((Seg (r1 -' p)),0) is Relation-like Seg (r1 -' p) -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() V122() Element of K6(K7((Seg (r1 -' p)),{0}))
K7((Seg (r1 -' p)),{0}) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7((Seg (r1 -' p)),{0})) is set
Sum (0* (r1 -' p)) is V11() real ext-real Element of REAL
K197(REAL,(0* (r1 -' p)),K562()) is V11() real ext-real Element of REAL
(0 + r2) + (Sum (0* (r1 -' p))) is V11() real ext-real Element of REAL
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
REAL p is non empty functional FinSequence-membered FinSequenceSet of REAL
p -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p } is set
TOP-REAL p is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL p) is non empty set
Seg p is V35() V42(p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
|.r1.| is V11() real ext-real non negative Element of REAL
sqr r1 is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
r1 (#) sqrreal is Relation-like complex-yielding V120() V121() set
mlt (r1,r1) is Relation-like Function-like set
K564() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K127(K564(),r1,r1) is set
Sum (sqr r1) is V11() real ext-real Element of REAL
K562() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K197(REAL,(sqr r1),K562()) is V11() real ext-real Element of REAL
sqrt (Sum (sqr r1)) is V11() real ext-real Element of REAL
|.r1.| ^2 is V11() real ext-real Element of REAL
|.r1.| * |.r1.| is V11() real ext-real non negative set
r2 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
g is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r2 /. g is V11() real ext-real Element of REAL
(r2 /. g) ^2 is V11() real ext-real Element of REAL
(r2 /. g) * (r2 /. g) is V11() real ext-real set
0* p is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
p |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
K131((Seg p),0) is Relation-like Seg p -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() V122() Element of K6(K7((Seg p),{0}))
{0} is non empty V130() V131() V132() V133() V134() V135() set
K7((Seg p),{0}) is RAT -valued INT -valued complex-yielding V120() V121() V122() set
K6(K7((Seg p),{0})) is set
(0* p) +* (g,((r2 /. g) ^2)) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
Sum ((0* p) +* (g,((r2 /. g) ^2))) is V11() real ext-real Element of REAL
K197(REAL,((0* p) +* (g,((r2 /. g) ^2))),K562()) is V11() real ext-real Element of REAL
len (0* p) is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
len ((0* p) +* (g,((r2 /. g) ^2))) is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
f1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
len f1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
sqr r1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
Sum (sqr r1) is V11() real ext-real Element of REAL
K197(REAL,(sqr r1),K562()) is V11() real ext-real Element of REAL
len r1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of p -tuples_on REAL
u is natural V11() real ext-real set
f1 . u is V11() real ext-real set
r . u is V11() real ext-real set
dom r1 is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r1 /. u is V11() real ext-real Element of REAL
r1 . u is V11() real ext-real set
dom (0* p) is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
Seg (len (0* p)) is V35() V42( len (0* p)) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
dom f1 is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
f1 /. g is V11() real ext-real Element of REAL
r1 /. g is V11() real ext-real Element of REAL
(r1 /. g) ^2 is V11() real ext-real Element of REAL
(r1 /. g) * (r1 /. g) is V11() real ext-real set
dom (0* p) is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
Seg (len (0* p)) is V35() V42( len (0* p)) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
dom r1 is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r1 /. u is V11() real ext-real Element of REAL
r1 . u is V11() real ext-real set
(r1 /. u) ^2 is V11() real ext-real Element of REAL
(r1 /. u) * (r1 /. u) is V11() real ext-real set
dom f1 is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
f1 /. u is V11() real ext-real Element of REAL
(0* p) /. u is V11() real ext-real Element of REAL
(p |-> 0) . u is V11() real ext-real set
Sum f1 is V11() real ext-real Element of REAL
K197(REAL,f1,K562()) is V11() real ext-real Element of REAL
Sum r is V11() real ext-real Element of REAL
K197(REAL,r,K562()) is V11() real ext-real Element of REAL
sqrt (Sum (sqr r1)) is V11() real ext-real Element of REAL
(sqrt (Sum (sqr r1))) ^2 is V11() real ext-real Element of REAL
(sqrt (Sum (sqr r1))) * (sqrt (Sum (sqr r1))) is V11() real ext-real set
sqrt ((r2 /. g) ^2) is V11() real ext-real Element of REAL
sqrt ((sqrt (Sum (sqr r1))) ^2) is V11() real ext-real Element of REAL
abs (r2 /. g) is V11() real ext-real Element of REAL
abs (abs (r2 /. g)) is V11() real ext-real Element of REAL
abs (sqrt (Sum (sqr r1))) is V11() real ext-real Element of REAL
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
TOP-REAL p is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL p) is non empty set
K6( the carrier of (TOP-REAL p)) is set
Seg p is V35() V42(p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r1 is V11() real ext-real set
r2 is Element of K6( the carrier of (TOP-REAL p))
g is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p) : not r1 <= b₁ /. g } is set
the topology of (TOP-REAL p) is Element of K6(K6( the carrier of (TOP-REAL p)))
K6(K6( the carrier of (TOP-REAL p))) is set
TopStruct(# the carrier of (TOP-REAL p), the topology of (TOP-REAL p) #) is strict TopStruct
Euclid p is non empty strict Reflexive discerning V111() triangle Discerning MetrStruct
REAL p is non empty functional FinSequence-membered FinSequenceSet of REAL
p -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p } is set
Pitag_dist p is Relation-like K7((REAL p),(REAL p)) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7((REAL p),(REAL p)),REAL))
K7((REAL p),(REAL p)) is set
K7(K7((REAL p),(REAL p)),REAL) is complex-yielding V120() V121() set
K6(K7(K7((REAL p),(REAL p)),REAL)) is set
MetrStruct(# (REAL p),(Pitag_dist p) #) is strict MetrStruct
TopSpaceMetr (Euclid p) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid p)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid p))) is set
the carrier of (Euclid p) is non empty set
u is Element of the carrier of (Euclid p)
f1 is V11() real ext-real Element of REAL
P is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
P /. g is V11() real ext-real Element of REAL
f1 - (P /. g) is V11() real ext-real Element of REAL
(f1 - (P /. g)) / 2 is V11() real ext-real Element of REAL
Ball (u,((f1 - (P /. g)) / 2)) is Element of K6( the carrier of (Euclid p))
K6( the carrier of (Euclid p)) is set
z is set
{ b₁ where b₁ is Element of the carrier of (Euclid p) : not (f1 - (P /. g)) / 2 <= dist (u,b₁) } is set
r1 is Element of the carrier of (Euclid p)
dist (u,r1) is V11() real ext-real Element of REAL
q is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
q is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
(Pitag_dist p) . (r1,u) is set
dist (r1,u) is V11() real ext-real Element of REAL
pqn is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
pen is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
pqn - pen is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
K563() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K562() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K560() is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K562() * ((id REAL),K560()) is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K127(K563(),pqn,pen) is set
K420(pen) is Relation-like Function-like complex-yielding set
pen (#) K560() is Relation-like complex-yielding V120() V121() set
- 1 is V11() real ext-real non positive set
(- 1) * pen is Relation-like Function-like set
K605((- 1)) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K564() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K129(K564(),(- 1),(id REAL)) is set
pen (#) K605((- 1)) is Relation-like complex-yielding V120() V121() set
K391(pqn,K420(pen)) is Relation-like Function-like set
|.(pqn - pen).| is V11() real ext-real non negative Element of REAL
sqr (pqn - pen) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
(pqn - pen) (#) sqrreal is Relation-like complex-yielding V120() V121() set
mlt ((pqn - pen),(pqn - pen)) is Relation-like Function-like set
K127(K564(),(pqn - pen),(pqn - pen)) is set
Sum (sqr (pqn - pen)) is V11() real ext-real Element of REAL
K197(REAL,(sqr (pqn - pen)),K562()) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (pqn - pen))) is V11() real ext-real Element of REAL
q - q is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
q - q is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
K127(K563(),q,q) is set
K420(q) is Relation-like Function-like complex-yielding set
q (#) K560() is Relation-like complex-yielding V120() V121() set
(- 1) * q is Relation-like Function-like set
q (#) K605((- 1)) is Relation-like complex-yielding V120() V121() set
K391(q,K420(q)) is Relation-like Function-like set
(q - q) /. g is V11() real ext-real Element of REAL
qq is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
|.qq.| is V11() real ext-real non negative Element of REAL
sqr qq is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
qq (#) sqrreal is Relation-like complex-yielding V120() V121() set
mlt (qq,qq) is Relation-like Function-like set
K127(K564(),qq,qq) is set
Sum (sqr qq) is V11() real ext-real Element of REAL
K197(REAL,(sqr qq),K562()) is V11() real ext-real Element of REAL
sqrt (Sum (sqr qq)) is V11() real ext-real Element of REAL
q /. g is V11() real ext-real Element of REAL
q /. g is V11() real ext-real Element of REAL
(q /. g) - (q /. g) is V11() real ext-real Element of REAL
(P /. g) + ((f1 - (P /. g)) / 2) is V11() real ext-real Element of REAL
f1 - ((f1 - (P /. g)) / 2) is V11() real ext-real Element of REAL
r is Element of K6( the carrier of (TopSpaceMetr (Euclid p)))
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
TOP-REAL p is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL p) is non empty set
K6( the carrier of (TOP-REAL p)) is set
Seg p is V35() V42(p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r1 is V11() real ext-real set
r2 is Element of K6( the carrier of (TOP-REAL p))
g is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p) : not b₁ /. g <= r1 } is set
the topology of (TOP-REAL p) is Element of K6(K6( the carrier of (TOP-REAL p)))
K6(K6( the carrier of (TOP-REAL p))) is set
TopStruct(# the carrier of (TOP-REAL p), the topology of (TOP-REAL p) #) is strict TopStruct
Euclid p is non empty strict Reflexive discerning V111() triangle Discerning MetrStruct
REAL p is non empty functional FinSequence-membered FinSequenceSet of REAL
p -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = p } is set
Pitag_dist p is Relation-like K7((REAL p),(REAL p)) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7((REAL p),(REAL p)),REAL))
K7((REAL p),(REAL p)) is set
K7(K7((REAL p),(REAL p)),REAL) is complex-yielding V120() V121() set
K6(K7(K7((REAL p),(REAL p)),REAL)) is set
MetrStruct(# (REAL p),(Pitag_dist p) #) is strict MetrStruct
TopSpaceMetr (Euclid p) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid p)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid p))) is set
the carrier of (Euclid p) is non empty set
u is Element of the carrier of (Euclid p)
f1 is V11() real ext-real Element of REAL
P is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
P /. g is V11() real ext-real Element of REAL
(P /. g) - f1 is V11() real ext-real Element of REAL
((P /. g) - f1) / 2 is V11() real ext-real Element of REAL
Ball (u,(((P /. g) - f1) / 2)) is Element of K6( the carrier of (Euclid p))
K6( the carrier of (Euclid p)) is set
z is set
{ b₁ where b₁ is Element of the carrier of (Euclid p) : not ((P /. g) - f1) / 2 <= dist (u,b₁) } is set
r1 is Element of the carrier of (Euclid p)
dist (u,r1) is V11() real ext-real Element of REAL
q is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
q is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
(Pitag_dist p) . (u,r1) is set
pen is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
pqn is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
pen - pqn is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
K563() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K562() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K560() is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K562() * ((id REAL),K560()) is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K127(K563(),pen,pqn) is set
K420(pqn) is Relation-like Function-like complex-yielding set
pqn (#) K560() is Relation-like complex-yielding V120() V121() set
- 1 is V11() real ext-real non positive set
(- 1) * pqn is Relation-like Function-like set
K605((- 1)) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K564() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K129(K564(),(- 1),(id REAL)) is set
pqn (#) K605((- 1)) is Relation-like complex-yielding V120() V121() set
K391(pen,K420(pqn)) is Relation-like Function-like set
|.(pen - pqn).| is V11() real ext-real non negative Element of REAL
sqr (pen - pqn) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
(pen - pqn) (#) sqrreal is Relation-like complex-yielding V120() V121() set
mlt ((pen - pqn),(pen - pqn)) is Relation-like Function-like set
K127(K564(),(pen - pqn),(pen - pqn)) is set
Sum (sqr (pen - pqn)) is V11() real ext-real Element of REAL
K197(REAL,(sqr (pen - pqn)),K562()) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (pen - pqn))) is V11() real ext-real Element of REAL
q - q is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
q - q is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
K127(K563(),q,q) is set
K420(q) is Relation-like Function-like complex-yielding set
q (#) K560() is Relation-like complex-yielding V120() V121() set
(- 1) * q is Relation-like Function-like set
q (#) K605((- 1)) is Relation-like complex-yielding V120() V121() set
K391(q,K420(q)) is Relation-like Function-like set
(q - q) /. g is V11() real ext-real Element of REAL
qq is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL p
|.qq.| is V11() real ext-real non negative Element of REAL
sqr qq is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
qq (#) sqrreal is Relation-like complex-yielding V120() V121() set
mlt (qq,qq) is Relation-like Function-like set
K127(K564(),qq,qq) is set
Sum (sqr qq) is V11() real ext-real Element of REAL
K197(REAL,(sqr qq),K562()) is V11() real ext-real Element of REAL
sqrt (Sum (sqr qq)) is V11() real ext-real Element of REAL
q /. g is V11() real ext-real Element of REAL
q /. g is V11() real ext-real Element of REAL
(q /. g) - (q /. g) is V11() real ext-real Element of REAL
(((P /. g) - f1) / 2) + (q /. g) is V11() real ext-real Element of REAL
((q /. g) - (q /. g)) + (q /. g) is V11() real ext-real Element of REAL
(q /. g) + (((P /. g) - f1) / 2) is V11() real ext-real Element of REAL
((q /. g) + (((P /. g) - f1) / 2)) - (((P /. g) - f1) / 2) is V11() real ext-real Element of REAL
(q /. g) - (((P /. g) - f1) / 2) is V11() real ext-real Element of REAL
(P /. g) - (((P /. g) - f1) / 2) is V11() real ext-real Element of REAL
f1 + (((P /. g) - f1) / 2) is V11() real ext-real Element of REAL
r is Element of K6( the carrier of (TopSpaceMetr (Euclid p)))
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
TOP-REAL p is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL p) is non empty set
K6( the carrier of (TOP-REAL p)) is set
Seg p is V35() V42(p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r1 is Element of K6( the carrier of (TOP-REAL p))
r2 is V11() real ext-real set
g is V11() real ext-real set
f1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p) : ( not b₁ /. f1 <= r2 & not g <= b₁ /. f1 ) } is set
{ b₁ where b₁ is Relation-like NAT -defined Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p) : not b₁ /. f1 <= r2 } is set
{ b₁ where b₁ is Relation-like NAT -defined Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p) : not g <= b₁ /. f1 } is set
{ b₁ where b₁ is Relation-like NAT -defined Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p) : not b₁ /. f1 <= r2 } /\ { b₁ where b₁ is Relation-like NAT -defined Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p) : not g <= b₁ /. f1 } is set
r is set
u is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
u /. f1 is V11() real ext-real Element of REAL
P is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
P /. f1 is V11() real ext-real Element of REAL
r is set
u is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
u /. f1 is V11() real ext-real Element of REAL
u is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
u /. f1 is V11() real ext-real Element of REAL
r is set
u is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
u /. f1 is V11() real ext-real Element of REAL
u is set
P is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
P /. f1 is V11() real ext-real Element of REAL
u is Element of K6( the carrier of (TOP-REAL p))
r is Element of K6( the carrier of (TOP-REAL p))
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
TOP-REAL p is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL p) is non empty set
K7( the carrier of (TOP-REAL p), the carrier of R^1) is complex-yielding V120() V121() set
K6(K7( the carrier of (TOP-REAL p), the carrier of R^1)) is set
r1 is V11() real ext-real set
r2 is V11() real ext-real set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= r1 & not r2 <= b₁ ) } is set
g is non empty Relation-like the carrier of (TOP-REAL p) -defined the carrier of R^1 -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7( the carrier of (TOP-REAL p), the carrier of R^1))
g " { b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= r1 & not r2 <= b₁ ) } is Element of K6( the carrier of (TOP-REAL p))
K6( the carrier of (TOP-REAL p)) is set
f1 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p) : ( not b₁ /. f1 <= r1 & not r2 <= b₁ /. f1 ) } is set
r is set
g . r is V11() real ext-real set
u is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
g . u is V11() real ext-real Element of the carrier of R^1
u /. f1 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
dom g is Element of K6( the carrier of (TOP-REAL p))
r is set
u is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p)
u /. f1 is V11() real ext-real Element of REAL
g . r is V11() real ext-real set
p is non empty TopSpace-like TopStruct
the carrier of p is non empty set
r1 is non empty Reflexive discerning V111() triangle Discerning MetrStruct
TopSpaceMetr r1 is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr r1) is non empty set
K7( the carrier of p, the carrier of (TopSpaceMetr r1)) is set
K6(K7( the carrier of p, the carrier of (TopSpaceMetr r1))) is set
the carrier of r1 is non empty set
K6( the carrier of (TopSpaceMetr r1)) is set
r2 is non empty Relation-like the carrier of p -defined the carrier of (TopSpaceMetr r1) -valued Function-like total quasi_total Element of K6(K7( the carrier of p, the carrier of (TopSpaceMetr r1)))
g is Element of K6( the carrier of (TopSpaceMetr r1))
r2 " g is Element of K6( the carrier of p)
K6( the carrier of p) is set
f1 is set
dom r2 is Element of K6( the carrier of p)
r2 . f1 is set
r is Element of the carrier of r1
u is V11() real ext-real set
Ball (r,u) is Element of K6( the carrier of r1)
K6( the carrier of r1) is set
P is V11() real ext-real Element of REAL
Ball (r,P) is Element of K6( the carrier of r1)
s1 is Element of K6( the carrier of (TopSpaceMetr r1))
r2 " s1 is Element of K6( the carrier of p)
r2 " (Ball (r,P)) is Element of K6( the carrier of p)
r is Element of K6( the carrier of p)
u is Element of K6( the carrier of p)
[#] (TopSpaceMetr r1) is non empty non proper Element of K6( the carrier of (TopSpaceMetr r1))
p is V11() real ext-real Element of the carrier of RealSpace
r2 is V11() real ext-real set
r1 is V11() real ext-real set
Ball (p,r1) is V130() V131() V132() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is set
r2 - r1 is V11() real ext-real set
r2 + r1 is V11() real ext-real set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= r2 - r1 & not r2 + r1 <= b₁ ) } is set
{ b₁ where b₁ is V11() real ext-real Element of the carrier of RealSpace : not r1 <= dist (p,b₁) } is set
g is set
f1 is V11() real ext-real Element of the carrier of RealSpace
dist (p,f1) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
r2 - r is V11() real ext-real Element of REAL
abs (r2 - r) is V11() real ext-real Element of REAL
r1 + r is V11() real ext-real Element of REAL
(r2 - r) + r is V11() real ext-real Element of REAL
(r1 + r) - r1 is V11() real ext-real Element of REAL
- r1 is V11() real ext-real set
(- r1) + r is V11() real ext-real Element of REAL
r - r1 is V11() real ext-real Element of REAL
(r - r1) + r1 is V11() real ext-real Element of REAL
g is set
f1 is V11() real ext-real Element of REAL
(r2 + r1) - r1 is V11() real ext-real set
f1 - r1 is V11() real ext-real Element of REAL
r2 - f1 is V11() real ext-real Element of REAL
- r1 is V11() real ext-real set
f1 + (- r1) is V11() real ext-real Element of REAL
(f1 + (- r1)) - f1 is V11() real ext-real Element of REAL
f1 + r1 is V11() real ext-real Element of REAL
(r2 - r1) + r1 is V11() real ext-real set
(f1 + r1) - f1 is V11() real ext-real Element of REAL
abs (r2 - f1) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of the carrier of RealSpace
dist (p,r) is V11() real ext-real Element of REAL
p is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
TOP-REAL p is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL p) is non empty set
K7( the carrier of (TOP-REAL p), the carrier of R^1) is complex-yielding V120() V121() set
K6(K7( the carrier of (TOP-REAL p), the carrier of R^1)) is set
Seg p is V35() V42(p) V130() V131() V132() V133() V134() V135() Element of K6(NAT)
r1 is non empty Relation-like the carrier of (TOP-REAL p) -defined the carrier of R^1 -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7( the carrier of (TOP-REAL p), the carrier of R^1))
r2 is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
the carrier of (TopSpaceMetr RealSpace) is non empty set
K7( the carrier of (TOP-REAL p), the carrier of (TopSpaceMetr RealSpace)) is set
K6(K7( the carrier of (TOP-REAL p), the carrier of (TopSpaceMetr RealSpace))) is set
K6( the carrier of (TopSpaceMetr RealSpace)) is set
g is non empty Relation-like the carrier of (TOP-REAL p) -defined the carrier of (TopSpaceMetr RealSpace) -valued Function-like total quasi_total Element of K6(K7( the carrier of (TOP-REAL p), the carrier of (TopSpaceMetr RealSpace)))
f1 is V11() real ext-real set
r is V11() real ext-real Element of the carrier of RealSpace
Ball (r,f1) is V130() V131() V132() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is set
u is Element of K6( the carrier of (TopSpaceMetr RealSpace))
g " u is Element of K6( the carrier of (TOP-REAL p))
K6( the carrier of (TOP-REAL p)) is set
P is V11() real ext-real Element of REAL
P - f1 is V11() real ext-real Element of REAL
P + f1 is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= P - f1 & not P + f1 <= b₁ ) } is set
r1 " (Ball (r,f1)) is Element of K6( the carrier of (TOP-REAL p))
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() V42(p) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL p) : ( not b₁ /. r2 <= P - f1 & not P + f1 <= b₁ /. r2 ) } is set
p is V11() real ext-real Element of REAL
<*p*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
abs <*p*> is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
absreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
<*p*> (#) absreal is Relation-like complex-yielding V120() V121() set
abs p is V11() real ext-real Element of REAL
<*(abs p)*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
rng <*p*> is V130() V131() V132() Element of K6(REAL)
dom absreal is V130() V131() V132() Element of K6(REAL)
r1 is set
{p} is non empty V130() V131() V132() set
dom <*p*> is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
absreal * <*p*> is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
dom (absreal * <*p*>) is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
dom (abs <*p*>) is V130() V131() V132() V133() V134() V135() Element of K6(NAT)
len (abs <*p*>) is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
len <*(abs p)*> is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r1 is natural V11() real ext-real set
<*(abs p)*> . r1 is V11() real ext-real set
(abs <*p*>) . r1 is V11() real ext-real set
<*p*> . 1 is V11() real ext-real set
REAL 1 is non empty functional FinSequence-membered FinSequenceSet of REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 1 } is set
TOP-REAL 1 is non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() L15()
the carrier of (TOP-REAL 1) is non empty set
p is Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 1 } is set
REAL 1 is non empty functional FinSequence-membered FinSequenceSet of REAL
r1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of 1 -tuples_on REAL
r2 is V11() real ext-real Element of REAL
<*r2*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
p is V11() real ext-real set
<*p*> is non empty Relation-like NAT -defined Function-like V35() V42(1) FinSequence-like FinSubsequence-like set
r1 is V11() real ext-real Element of REAL
<*r1*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
REAL 1 is non empty functional FinSequence-membered FinSequenceSet of REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 1 } is set
p is V11() real ext-real set
(p) is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
r1 is V11() real ext-real Element of REAL
r1 * (p) is Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
r1 * (p) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
K605(r1) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K564() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K129(K564(),r1,(id REAL)) is set
(p) (#) K605(r1) is Relation-like complex-yielding V120() V121() set
r1 * p is V11() real ext-real Element of REAL
((r1 * p)) is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
p is V11() real ext-real set
r1 is V11() real ext-real set
p + r1 is V11() real ext-real set
((p + r1)) is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
(p) is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
(r1) is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
(p) + (r1) is Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
(p) + (r1) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
K562() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K127(K562(),(p),(r1)) is set
p is V11() real ext-real set
(p) is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
r1 is V11() real ext-real set
(r1) is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
K6( the carrier of R^1) is set
p is V130() V131() V132() Element of K6( the carrier of R^1)
r1 is V11() real ext-real set
{ b₁ where b₁ is V11() real ext-real Element of REAL : not r1 <= b₁ } is set
r2 is V11() real ext-real Element of the carrier of RealSpace
g is V11() real ext-real Element of REAL
r1 - g is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
Ball (r2,f1) is V130() V131() V132() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is set
r is set
{ b₁ where b₁ is V11() real ext-real Element of the carrier of RealSpace : not f1 <= dist (r2,b₁) } is set
P is V11() real ext-real Element of the carrier of RealSpace
u is V11() real ext-real Element of REAL
real_dist . (u,g) is V11() real ext-real Element of REAL
s1 is V11() real ext-real Element of the carrier of RealSpace
dist (r2,s1) is V11() real ext-real Element of REAL
u - g is V11() real ext-real Element of REAL
abs (u - g) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
p is V130() V131() V132() Element of K6( the carrier of R^1)
r1 is V11() real ext-real set
{ b₁ where b₁ is V11() real ext-real Element of REAL : not b₁ <= r1 } is set
r2 is V11() real ext-real Element of the carrier of RealSpace
g is V11() real ext-real Element of REAL
g - r1 is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
Ball (r2,f1) is V130() V131() V132() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is set
r is set
{ b₁ where b₁ is V11() real ext-real Element of the carrier of RealSpace : not f1 <= dist (r2,b₁) } is set
P is V11() real ext-real Element of the carrier of RealSpace
u is V11() real ext-real Element of REAL
real_dist . (g,u) is V11() real ext-real Element of REAL
s1 is V11() real ext-real Element of the carrier of RealSpace
dist (r2,s1) is V11() real ext-real Element of REAL
g - u is V11() real ext-real Element of REAL
abs (g - u) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
p is V130() V131() V132() Element of K6( the carrier of R^1)
r1 is V11() real ext-real set
r2 is V11() real ext-real set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= r1 & not r2 <= b₁ ) } is set
{ b₁ where b₁ is V11() real ext-real Element of REAL : not b₁ <= r1 } is set
g is set
f1 is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : not r2 <= b₁ } is set
f1 is set
r is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : not b₁ <= r1 } /\ { b₁ where b₁ is V11() real ext-real Element of REAL : not r2 <= b₁ } is set
r is set
u is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
r is set
u is V11() real ext-real Element of REAL
u is V11() real ext-real Element of REAL
g is V130() V131() V132() Element of K6( the carrier of R^1)
f1 is V130() V131() V132() Element of K6( the carrier of R^1)
Euclid 1 is non empty strict Reflexive discerning V111() triangle Discerning MetrStruct
REAL 1 is non empty functional FinSequence-membered FinSequenceSet of REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 1 } is set
Pitag_dist 1 is Relation-like K7((REAL 1),(REAL 1)) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7((REAL 1),(REAL 1)),REAL))
K7((REAL 1),(REAL 1)) is set
K7(K7((REAL 1),(REAL 1)),REAL) is complex-yielding V120() V121() set
K6(K7(K7((REAL 1),(REAL 1)),REAL)) is set
MetrStruct(# (REAL 1),(Pitag_dist 1) #) is strict MetrStruct
the carrier of (Euclid 1) is non empty set
p is Element of the carrier of (Euclid 1)
r2 is V11() real ext-real set
<*r2*> is non empty Relation-like NAT -defined Function-like V35() V42(1) FinSequence-like FinSubsequence-like set
r1 is V11() real ext-real set
Ball (p,r1) is Element of K6( the carrier of (Euclid 1))
K6( the carrier of (Euclid 1)) is set
r2 - r1 is V11() real ext-real set
r2 + r1 is V11() real ext-real set
{ <*b₁*> where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= r2 - r1 & not r2 + r1 <= b₁ ) } is set
g is V11() real ext-real Element of REAL
g - r1 is V11() real ext-real Element of REAL
g + r1 is V11() real ext-real Element of REAL
{ <*b₁*> where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= g - r1 & not g + r1 <= b₁ ) } is set
{ b₁ where b₁ is Element of the carrier of (Euclid 1) : not r1 <= dist (p,b₁) } is set
f1 is set
r is Element of the carrier of (Euclid 1)
dist (p,r) is V11() real ext-real Element of REAL
s1 is V11() real ext-real Element of REAL
<*s1*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
<*g*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
<*g*> - <*s1*> is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
K563() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K562() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K560() is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K562() * ((id REAL),K560()) is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K127(K563(),<*g*>,<*s1*>) is set
K420(<*s1*>) is Relation-like Function-like complex-yielding set
<*s1*> (#) K560() is Relation-like complex-yielding V120() V121() set
- 1 is V11() real ext-real non positive set
(- 1) * <*s1*> is Relation-like Function-like set
K605((- 1)) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K564() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K129(K564(),(- 1),(id REAL)) is set
<*s1*> (#) K605((- 1)) is Relation-like complex-yielding V120() V121() set
K391(<*g*>,K420(<*s1*>)) is Relation-like Function-like set
g - s1 is V11() real ext-real Element of REAL
<*(g - s1)*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
sqr (<*g*> - <*s1*>) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
(<*g*> - <*s1*>) (#) sqrreal is Relation-like complex-yielding V120() V121() set
mlt ((<*g*> - <*s1*>),(<*g*> - <*s1*>)) is Relation-like Function-like set
K127(K564(),(<*g*> - <*s1*>),(<*g*> - <*s1*>)) is set
(g - s1) ^2 is V11() real ext-real Element of REAL
(g - s1) * (g - s1) is V11() real ext-real set
<*((g - s1) ^2)*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (sqr (<*g*> - <*s1*>)) is V11() real ext-real Element of REAL
K197(REAL,(sqr (<*g*> - <*s1*>)),K562()) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (<*g*> - <*s1*>))) is V11() real ext-real Element of REAL
abs (g - s1) is V11() real ext-real Element of REAL
u is Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL 1
P is Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL 1
(Pitag_dist 1) . (u,P) is V11() real ext-real Element of REAL
|.(<*g*> - <*s1*>).| is V11() real ext-real non negative Element of REAL
r1 + s1 is V11() real ext-real Element of REAL
(g - s1) + s1 is V11() real ext-real Element of REAL
(r1 + s1) - r1 is V11() real ext-real Element of REAL
- r1 is V11() real ext-real set
(- r1) + s1 is V11() real ext-real Element of REAL
s1 - r1 is V11() real ext-real Element of REAL
(s1 - r1) + r1 is V11() real ext-real Element of REAL
<*g*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
r is set
u is V11() real ext-real Element of REAL
<*u*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
(g + r1) - r1 is V11() real ext-real Element of REAL
u - r1 is V11() real ext-real Element of REAL
g - u is V11() real ext-real Element of REAL
- r1 is V11() real ext-real set
u + (- r1) is V11() real ext-real Element of REAL
(u + (- r1)) - u is V11() real ext-real Element of REAL
<*g*> - <*u*> is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
K563() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K562() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K560() is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K562() * ((id REAL),K560()) is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K127(K563(),<*g*>,<*u*>) is set
K420(<*u*>) is Relation-like Function-like complex-yielding set
<*u*> (#) K560() is Relation-like complex-yielding V120() V121() set
- 1 is V11() real ext-real non positive set
(- 1) * <*u*> is Relation-like Function-like set
K605((- 1)) is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
K564() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7(REAL,REAL),REAL))
K129(K564(),(- 1),(id REAL)) is set
<*u*> (#) K605((- 1)) is Relation-like complex-yielding V120() V121() set
K391(<*g*>,K420(<*u*>)) is Relation-like Function-like set
<*(g - u)*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
sqr (<*g*> - <*u*>) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(REAL,REAL))
(<*g*> - <*u*>) (#) sqrreal is Relation-like complex-yielding V120() V121() set
mlt ((<*g*> - <*u*>),(<*g*> - <*u*>)) is Relation-like Function-like set
K127(K564(),(<*g*> - <*u*>),(<*g*> - <*u*>)) is set
(g - u) ^2 is V11() real ext-real Element of REAL
(g - u) * (g - u) is V11() real ext-real set
<*((g - u) ^2)*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
Sum (sqr (<*g*> - <*u*>)) is V11() real ext-real Element of REAL
K197(REAL,(sqr (<*g*> - <*u*>)),K562()) is V11() real ext-real Element of REAL
u + r1 is V11() real ext-real Element of REAL
(g - r1) + r1 is V11() real ext-real Element of REAL
(u + r1) - u is V11() real ext-real Element of REAL
abs (g - u) is V11() real ext-real Element of REAL
|.(<*g*> - <*u*>).| is V11() real ext-real non negative Element of REAL
sqrt (Sum (sqr (<*g*> - <*u*>))) is V11() real ext-real Element of REAL
the distance of (Euclid 1) is Relation-like K7( the carrier of (Euclid 1), the carrier of (Euclid 1)) -defined REAL -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7(K7( the carrier of (Euclid 1), the carrier of (Euclid 1)),REAL))
K7( the carrier of (Euclid 1), the carrier of (Euclid 1)) is set
K7(K7( the carrier of (Euclid 1), the carrier of (Euclid 1)),REAL) is complex-yielding V120() V121() set
K6(K7(K7( the carrier of (Euclid 1), the carrier of (Euclid 1)),REAL)) is set
s1 is Element of the carrier of (Euclid 1)
the distance of (Euclid 1) . (p,s1) is V11() real ext-real Element of REAL
dist (p,s1) is V11() real ext-real Element of REAL
f1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL 1
P is Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of REAL 1
(Pitag_dist 1) . (f1,P) is V11() real ext-real Element of REAL
K7( the carrier of (TOP-REAL 1), the carrier of R^1) is complex-yielding V120() V121() set
K6(K7( the carrier of (TOP-REAL 1), the carrier of R^1)) is set
p is non empty Relation-like the carrier of (TOP-REAL 1) -defined the carrier of R^1 -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7( the carrier of (TOP-REAL 1), the carrier of R^1))
dom p is Element of K6( the carrier of (TOP-REAL 1))
K6( the carrier of (TOP-REAL 1)) is set
rng p is V130() V131() V132() Element of K6( the carrier of R^1)
r1 is set
r2 is V11() real ext-real Element of REAL
<*r2*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
len <*r2*> is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(r2) is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
p . (r2) is V11() real ext-real Element of the carrier of R^1
(r2) /. 1 is V11() real ext-real Element of REAL
<*r2*> . 1 is V11() real ext-real set
[#] (TOP-REAL 1) is non empty non proper Element of K6( the carrier of (TOP-REAL 1))
[#] R^1 is non empty non proper V130() V131() V132() Element of K6( the carrier of R^1)
the topology of (TOP-REAL 1) is Element of K6(K6( the carrier of (TOP-REAL 1)))
K6(K6( the carrier of (TOP-REAL 1))) is set
TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is strict TopStruct
TopSpaceMetr (Euclid 1) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid 1)) is non empty set
K7( the carrier of R^1, the carrier of (TopSpaceMetr (Euclid 1))) is set
K6(K7( the carrier of R^1, the carrier of (TopSpaceMetr (Euclid 1)))) is set
p /" is non empty Relation-like the carrier of R^1 -defined the carrier of (TOP-REAL 1) -valued Function-like total quasi_total Element of K6(K7( the carrier of R^1, the carrier of (TOP-REAL 1)))
K7( the carrier of R^1, the carrier of (TOP-REAL 1)) is set
K6(K7( the carrier of R^1, the carrier of (TOP-REAL 1))) is set
r2 is set
p . r2 is V11() real ext-real set
g is set
p . g is V11() real ext-real set
f1 is Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
u is V11() real ext-real Element of REAL
<*u*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
len <*u*> is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r is Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
P is V11() real ext-real Element of REAL
<*P*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
len <*P*> is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
p . r is V11() real ext-real Element of the carrier of R^1
r /. 1 is V11() real ext-real Element of REAL
<*P*> . 1 is V11() real ext-real set
p . f1 is V11() real ext-real Element of the carrier of R^1
f1 /. 1 is V11() real ext-real Element of REAL
<*u*> . 1 is V11() real ext-real set
r2 is non empty Relation-like the carrier of R^1 -defined the carrier of (TopSpaceMetr (Euclid 1)) -valued Function-like total quasi_total Element of K6(K7( the carrier of R^1, the carrier of (TopSpaceMetr (Euclid 1))))
f1 is set
r is V11() real ext-real Element of REAL
<*r*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
u is Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
p . u is V11() real ext-real Element of the carrier of R^1
u /. 1 is V11() real ext-real Element of REAL
K6( the carrier of (TopSpaceMetr (Euclid 1))) is set
r is V11() real ext-real set
u is Element of the carrier of (Euclid 1)
Ball (u,r) is Element of K6( the carrier of (Euclid 1))
K6( the carrier of (Euclid 1)) is set
P is Element of K6( the carrier of (TopSpaceMetr (Euclid 1)))
r2 " P is V130() V131() V132() Element of K6( the carrier of R^1)
s1 is V11() real ext-real Element of REAL
<*s1*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
f1 is non empty Relation-like the carrier of (TOP-REAL 1) -defined the carrier of R^1 -valued Function-like total quasi_total complex-yielding V120() V121() Element of K6(K7( the carrier of (TOP-REAL 1), the carrier of R^1))
dom f1 is Element of K6( the carrier of (TOP-REAL 1))
s1 - r is V11() real ext-real Element of REAL
s1 + r is V11() real ext-real Element of REAL
{ <*b₁*> where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= s1 - r & not s1 + r <= b₁ ) } is set
f1 .: (Ball (u,r)) is V130() V131() V132() Element of K6( the carrier of R^1)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= s1 - r & not s1 + r <= b₁ ) } is set
z is set
r1 is set
f1 . r1 is V11() real ext-real set
q is V11() real ext-real Element of REAL
<*q*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
len <*q*> is natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() Element of NAT
q is Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
q /. 1 is V11() real ext-real Element of REAL
<*q*> . 1 is V11() real ext-real set
z is set
r1 is V11() real ext-real Element of REAL
<*r1*> is non empty Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
q is Relation-like NAT -defined REAL -valued Function-like V35() V42(1) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 1)
q /. 1 is V11() real ext-real Element of REAL
f1 . <*r1*> is V11() real ext-real set
g is non empty Relation-like the carrier of R^1 -defined the carrier of (TOP-REAL 1) -valued Function-like total quasi_total Element of K6(K7( the carrier of R^1, the carrier of (TOP-REAL 1)))
f1 " is Relation-like Function-like set
g " (Ball (u,r)) is V130() V131() V132() Element of K6( the carrier of R^1)
r1 is non empty Relation-like the carrier of R^1 -defined the carrier of (TopSpaceMetr (Euclid 1)) -valued Function-like total quasi_total Element of K6(K7( the carrier of R^1, the carrier of (TopSpaceMetr (Euclid 1))))
p is Relation-like NAT -defined REAL -valued Function-like V35() V42(2) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p /. 1 is V11() real ext-real Element of REAL
p `1 is V11() real ext-real Element of REAL
K529(p,1) is V11() real ext-real Element of REAL
p /. 2 is V11() real ext-real Element of REAL
p `2 is V11() real ext-real Element of REAL
K529(p,2) is V11() real ext-real Element of REAL
r1 is V11() real ext-real Element of REAL
r2 is V11() real ext-real Element of REAL
<*r1,r2*> is non empty Relation-like NAT -defined Function-like V35() V42(2) FinSequence-like FinSubsequence-like set
g is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() FinSequence of REAL
g /. 2 is V11() real ext-real Element of REAL
g /. 1 is V11() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like V35() V42(2) FinSequence-like FinSubsequence-like complex-yielding V120() V121() Element of the carrier of (TOP-REAL 2)
p /. 1 is V11() real ext-real Element of REAL
proj1 . p is V11() real ext-real Element of REAL
p /. 2 is V11() real ext-real Element of REAL
proj2 . p is V11() real ext-real Element of REAL
p `2 is V11() real ext-real Element of REAL
K529(p,2) is V11() real ext-real Element of REAL
p `1 is V11() real ext-real Element of REAL
K529(p,1) is V11() real ext-real Element of REAL