REAL is complex-membered ext-real-membered real-membered V153() set
NAT is V12() ordinal V32() cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V153() Element of K19(REAL)
K19(REAL) is non empty set
COMPLEX is complex-membered V153() set
RAT is complex-membered ext-real-membered real-membered rational-membered V153() set
INT is complex-membered ext-real-membered real-membered rational-membered integer-membered V153() set
K20(COMPLEX,COMPLEX) is Relation-like V137() set
K19(K20(COMPLEX,COMPLEX)) is non empty set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like V137() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K20(REAL,REAL) is Relation-like V137() V138() V139() set
K19(K20(REAL,REAL)) is non empty set
K20(K20(REAL,REAL),REAL) is Relation-like V137() V138() V139() set
K19(K20(K20(REAL,REAL),REAL)) is non empty set
K20(RAT,RAT) is Relation-like RAT -valued V137() V138() V139() set
K19(K20(RAT,RAT)) is non empty set
K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued V137() V138() V139() set
K19(K20(K20(RAT,RAT),RAT)) is non empty set
K20(INT,INT) is Relation-like RAT -valued INT -valued V137() V138() V139() set
K19(K20(INT,INT)) is non empty set
K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued V137() V138() V139() set
K19(K20(K20(INT,INT),INT)) is non empty set
K20(NAT,NAT) is Relation-like RAT -valued INT -valued V137() V138() V139() V140() set
K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V137() V138() V139() V140() set
K19(K20(K20(NAT,NAT),NAT)) is non empty set
omega is V12() ordinal V32() cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V153() set
K19(omega) is non empty V12() V32() set
1 is non empty V21() ordinal natural real V30() V31() V32() cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
K20(1,1) is Relation-like RAT -valued INT -valued non empty V32() V137() V138() V139() V140() set
K19(K20(1,1)) is non empty V32() V36() set
K20(K20(1,1),1) is Relation-like RAT -valued INT -valued non empty V32() V137() V138() V139() V140() set
K19(K20(K20(1,1),1)) is non empty V32() V36() set
K20(K20(1,1),REAL) is Relation-like V137() V138() V139() set
K19(K20(K20(1,1),REAL)) is non empty set
2 is non empty V21() ordinal natural real V30() V31() V32() cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
K20(2,2) is Relation-like RAT -valued INT -valued non empty V32() V137() V138() V139() V140() set
K20(K20(2,2),REAL) is Relation-like V137() V138() V139() set
K19(K20(K20(2,2),REAL)) is non empty set
K19(NAT) is non empty V12() V32() set
K383() is non empty V93() L9()
the carrier of K383() is non empty set
K388() is non empty L9()
K389() is non empty V93() M13(K388())
K390() is non empty V93() V115() V175() M16(K388(),K389())
K392() is non empty V93() V115() V117() V119() L9()
K393() is non empty V93() V115() V175() M13(K392())
{} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V21() ordinal natural real V32() V33() V36() cardinal {} -element ext-real non positive non negative V137() V138() V139() V140() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V153() Function-yielding V275() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued set
{{},1} is non empty V32() V36() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
TOP-REAL 2 is non empty V46() V90() V91() V160() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V188() TopSpace-like T_0 T_1 T_2 strict add-continuous Mult-continuous V310() V311() finite-dimensional RLTopStruct
the carrier of (TOP-REAL 2) is functional non empty V12() complex-functions-membered ext-real-functions-membered real-functions-membered set
I[01] is non empty strict TopSpace-like real-membered TopStruct
the carrier of I[01] is non empty complex-membered ext-real-membered real-membered set
RealSpace is strict real-membered MetrStruct
R^1 is non empty strict TopSpace-like real-membered TopStruct
the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set
K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is Relation-like non empty set
K19(K20( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2))) is non empty set
I[01] is non empty strict TopSpace-like real-membered SubSpace of R^1
K706(I[01],I[01]) is non empty strict TopSpace-like TopStruct
the carrier of K706(I[01],I[01]) is non empty set
K878() is non empty strict TopSpace-like real-membered V308() SubSpace of R^1
the carrier of K878() is non empty complex-membered ext-real-membered real-membered set
K19( the carrier of K878()) is non empty set
K19(K19( the carrier of K878())) is non empty set
Tunit_circle 2 is TopSpace-like T_0 T_1 T_2 V310() V311() SubSpace of TOP-REAL 2
the carrier of (Tunit_circle 2) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K20( the carrier of K878(), the carrier of (Tunit_circle 2)) is Relation-like set
K19(K20( the carrier of K878(), the carrier of (Tunit_circle 2))) is non empty set
CircleMap is Relation-like the carrier of K878() -defined the carrier of (Tunit_circle 2) -valued Function-like quasi_total Function-yielding V275() complex-functions-valued ext-real-functions-valued real-functions-valued Element of K19(K20( the carrier of K878(), the carrier of (Tunit_circle 2)))
c[10] is Relation-like Function-like V137() V138() V139() Element of the carrier of (Tunit_circle 2)
Topen_unit_circle c[10] is strict TopSpace-like T_0 T_1 T_2 V310() V311() SubSpace of Tunit_circle 2
the carrier of (Topen_unit_circle c[10]) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V21() ordinal natural real V30() V31() V32() V33() V36() cardinal {} -element ext-real non positive non negative V137() V138() V139() V140() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V153() Function-yielding V275() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued Element of NAT
K872(0,1) is complex-membered ext-real-membered real-membered Element of K19(REAL)
R^1 K872(0,1) is complex-membered ext-real-membered real-membered Element of K19( the carrier of K878())
K878() | (R^1 K872(0,1)) is strict TopSpace-like real-membered SubSpace of K878()
the carrier of (K878() | (R^1 K872(0,1))) is complex-membered ext-real-membered real-membered set
K20( the carrier of (Topen_unit_circle c[10]), the carrier of (K878() | (R^1 K872(0,1)))) is Relation-like V137() V138() V139() set
K19(K20( the carrier of (Topen_unit_circle c[10]), the carrier of (K878() | (R^1 K872(0,1))))) is non empty set
c[-10] is Relation-like Function-like V137() V138() V139() Element of the carrier of (Tunit_circle 2)
Topen_unit_circle c[-10] is strict TopSpace-like T_0 T_1 T_2 V310() V311() SubSpace of Tunit_circle 2
the carrier of (Topen_unit_circle c[-10]) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
1 / 2 is non empty V21() real ext-real positive non negative Element of REAL
2 " is non empty V21() real ext-real positive non negative set
1 * (2 ") is non empty V21() real ext-real positive non negative set
3 is non empty V21() ordinal natural real V30() V31() V32() cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
3 / 2 is non empty V21() real ext-real positive non negative Element of REAL
3 * (2 ") is non empty V21() real ext-real positive non negative set
K872((1 / 2),(3 / 2)) is complex-membered ext-real-membered real-membered Element of K19(REAL)
R^1 K872((1 / 2),(3 / 2)) is complex-membered ext-real-membered real-membered Element of K19( the carrier of K878())
K878() | (R^1 K872((1 / 2),(3 / 2))) is strict TopSpace-like real-membered SubSpace of K878()
the carrier of (K878() | (R^1 K872((1 / 2),(3 / 2)))) is complex-membered ext-real-membered real-membered set
K20( the carrier of (Topen_unit_circle c[-10]), the carrier of (K878() | (R^1 K872((1 / 2),(3 / 2))))) is Relation-like V137() V138() V139() set
K19(K20( the carrier of (Topen_unit_circle c[-10]), the carrier of (K878() | (R^1 K872((1 / 2),(3 / 2)))))) is non empty set
K20(NAT,REAL) is Relation-like V137() V138() V139() set
K19(K20(NAT,REAL)) is non empty set
K20(COMPLEX,REAL) is Relation-like V137() V138() V139() set
K19(K20(COMPLEX,REAL)) is non empty set
REAL 0 is functional non empty V78() complex-functions-membered ext-real-functions-membered real-functions-membered M10( REAL )
TOP-REAL 0 is non empty V46() V47() 1 -element V90() V91() V160() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V188() TopSpace-like T_0 T_1 T_2 strict add-continuous Mult-continuous compact real-membered V310() V311() finite-dimensional RLTopStruct
0. (TOP-REAL 0) is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V21() ordinal natural real V32() V33() V36() cardinal 0 -element V48( TOP-REAL 0) V76() ext-real non positive non negative V137() V138() V139() V140() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V153() Function-yielding V275() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued Element of the carrier of (TOP-REAL 0)
the carrier of (TOP-REAL 0) is functional non empty V12() V32() 1 -element complex-membered ext-real-membered real-membered complex-functions-membered ext-real-functions-membered real-functions-membered set
the ZeroF of (TOP-REAL 0) is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V21() ordinal natural real V32() V33() V36() cardinal 0 -element V76() ext-real non positive non negative V137() V138() V139() V140() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V153() Function-yielding V275() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued Element of the carrier of (TOP-REAL 0)
{(0. (TOP-REAL 0))} is functional non empty V12() V32() V36() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered complex-functions-membered set
- 1 is non empty V21() real ext-real non positive negative Element of REAL
n is V21() ordinal natural real V32() cardinal ext-real non negative set
TOP-REAL n is non empty V90() V91() V160() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V188() TopSpace-like T_0 T_1 T_2 strict add-continuous Mult-continuous V310() V311() finite-dimensional RLTopStruct
the carrier of (TOP-REAL n) is functional non empty complex-functions-membered ext-real-functions-membered real-functions-membered set
T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
cB - T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
- T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K364(T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K246((TOP-REAL n),cB,(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
the U6 of (TOP-REAL n) is Relation-like K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) -defined the carrier of (TOP-REAL n) -valued Function-like non empty V14(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n))) quasi_total Function-yielding V275() complex-functions-valued ext-real-functions-valued real-functions-valued Element of K19(K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)))
K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) is Relation-like non empty set
K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)) is Relation-like non empty set
K19(K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n))) is non empty set
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),cB,(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(cB,(- T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366(cB,T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
S is V21() real ext-real set
1 - S is V21() real ext-real Element of REAL
- S is V21() real ext-real set
1 + (- S) is V21() real ext-real set
(1 - S) * T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(T,(1 - S)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
S * cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(cB,S) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
((1 - S) * T) + (S * cB) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),((1 - S) * T),(S * cB)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(((1 - S) * T),(S * cB)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(((1 - S) * T) + (S * cB)) - T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),(((1 - S) * T) + (S * cB)),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(((1 - S) * T) + (S * cB)),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((((1 - S) * T) + (S * cB)),(- T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366((((1 - S) * T) + (S * cB)),T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
S * (cB - T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368((cB - T),S) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
((1 - S) * T) - T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),((1 - S) * T),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),((1 - S) * T),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(((1 - S) * T),(- T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366(((1 - S) * T),T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(S * cB) + (((1 - S) * T) - T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(S * cB),(((1 - S) * T) - T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((S * cB),(((1 - S) * T) - T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
1 * T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(T,1) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
S * T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(T,S) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(1 * T) - (S * T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
- (S * T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K364((S * T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K246((TOP-REAL n),(1 * T),(- (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(1 * T),(- (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((1 * T),(- (S * T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366((1 * T),(S * T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
((1 * T) - (S * T)) - T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),((1 * T) - (S * T)),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),((1 * T) - (S * T)),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(((1 * T) - (S * T)),(- T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366(((1 * T) - (S * T)),T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(S * cB) + (((1 * T) - (S * T)) - T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(S * cB),(((1 * T) - (S * T)) - T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((S * cB),(((1 * T) - (S * T)) - T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
T - (S * T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),T,(- (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),T,(- (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(T,(- (S * T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366(T,(S * T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(T - (S * T)) - T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),(T - (S * T)),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(T - (S * T)),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((T - (S * T)),(- T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366((T - (S * T)),T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(S * cB) + ((T - (S * T)) - T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(S * cB),((T - (S * T)) - T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((S * cB),((T - (S * T)) - T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
T + (- (S * T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
(T + (- (S * T))) + (- T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(T + (- (S * T))),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((T + (- (S * T))),(- T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(S * cB) + ((T + (- (S * T))) + (- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(S * cB),((T + (- (S * T))) + (- T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((S * cB),((T + (- (S * T))) + (- T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
T + (- T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),T,(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(T,(- T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(T + (- T)) + (- (S * T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(T + (- T)),(- (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((T + (- T)),(- (S * T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(S * cB) + ((T + (- T)) + (- (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(S * cB),((T + (- T)) + (- (S * T)))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((S * cB),((T + (- T)) + (- (S * T)))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
T - T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),T,(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K366(T,T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(T - T) - (S * T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),(T - T),(- (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(T - T),(- (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((T - T),(- (S * T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366((T - T),(S * T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(S * cB) + ((T - T) - (S * T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(S * cB),((T - T) - (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((S * cB),((T - T) - (S * T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
0. (TOP-REAL n) is Relation-like Function-like n -element V48( TOP-REAL n) V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
(0. (TOP-REAL n)) - (S * T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),(0. (TOP-REAL n)),(- (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(0. (TOP-REAL n)),(- (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((0. (TOP-REAL n)),(- (S * T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366((0. (TOP-REAL n)),(S * T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(S * cB) + ((0. (TOP-REAL n)) - (S * T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(S * cB),((0. (TOP-REAL n)) - (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((S * cB),((0. (TOP-REAL n)) - (S * T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(S * cB) - (S * T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),(S * cB),(- (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(S * cB),(- (S * T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((S * cB),(- (S * T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366((S * cB),(S * T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
n is V21() ordinal natural real V32() cardinal ext-real non negative set
TOP-REAL n is non empty V90() V91() V160() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V188() TopSpace-like T_0 T_1 T_2 strict add-continuous Mult-continuous V310() V311() finite-dimensional RLTopStruct
the carrier of (TOP-REAL n) is functional non empty complex-functions-membered ext-real-functions-membered real-functions-membered set
0. (TOP-REAL n) is Relation-like Function-like n -element V48( TOP-REAL n) V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
halfline ((0. (TOP-REAL n)),T) is functional closed complex-functions-membered ext-real-functions-membered real-functions-membered Element of K19( the carrier of (TOP-REAL n))
K19( the carrier of (TOP-REAL n)) is non empty set
{ (((1 - b1) * (0. (TOP-REAL n))) + (b1 * T)) where b1 is V21() real ext-real Element of REAL : 0 <= b1 } is set
cB is V21() real ext-real set
cB * T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(T,cB) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
1 - cB is V21() real ext-real Element of REAL
- cB is V21() real ext-real set
1 + (- cB) is V21() real ext-real set
(1 - cB) * (0. (TOP-REAL n)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368((0. (TOP-REAL n)),(1 - cB)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(0. (TOP-REAL n)) + (cB * T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
the U6 of (TOP-REAL n) is Relation-like K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) -defined the carrier of (TOP-REAL n) -valued Function-like non empty V14(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n))) quasi_total Function-yielding V275() complex-functions-valued ext-real-functions-valued real-functions-valued Element of K19(K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)))
K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) is Relation-like non empty set
K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)) is Relation-like non empty set
K19(K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n))) is non empty set
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(0. (TOP-REAL n)),(cB * T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((0. (TOP-REAL n)),(cB * T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
n is V21() ordinal natural real V32() cardinal ext-real non negative set
TOP-REAL n is non empty V90() V91() V160() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V188() TopSpace-like T_0 T_1 T_2 strict add-continuous Mult-continuous V310() V311() finite-dimensional RLTopStruct
the carrier of (TOP-REAL n) is functional non empty complex-functions-membered ext-real-functions-membered real-functions-membered set
T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
cB - T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
- T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K364(T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K246((TOP-REAL n),cB,(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
the U6 of (TOP-REAL n) is Relation-like K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) -defined the carrier of (TOP-REAL n) -valued Function-like non empty V14(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n))) quasi_total Function-yielding V275() complex-functions-valued ext-real-functions-valued real-functions-valued Element of K19(K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)))
K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) is Relation-like non empty set
K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)) is Relation-like non empty set
K19(K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n))) is non empty set
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),cB,(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(cB,(- T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366(cB,T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
S is V21() real ext-real set
1 - S is V21() real ext-real Element of REAL
- S is V21() real ext-real set
1 + (- S) is V21() real ext-real set
(1 - S) * T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(T,(1 - S)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
S * cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(cB,S) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
((1 - S) * T) + (S * cB) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),((1 - S) * T),(S * cB)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(((1 - S) * T),(S * cB)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
S * (cB - T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368((cB - T),S) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
T + (S * (cB - T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),T,(S * (cB - T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(T,(S * (cB - T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(((1 - S) * T) + (S * cB)) - T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),(((1 - S) * T) + (S * cB)),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(((1 - S) * T) + (S * cB)),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((((1 - S) * T) + (S * cB)),(- T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366((((1 - S) * T) + (S * cB)),T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
((((1 - S) * T) + (S * cB)) - T) + T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),((((1 - S) * T) + (S * cB)) - T),T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(((((1 - S) * T) + (S * cB)) - T),T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
T - T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),T,(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),T,(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(T,(- T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366(T,T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(((1 - S) * T) + (S * cB)) - (T - T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
- (T - T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K364((T - T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K246((TOP-REAL n),(((1 - S) * T) + (S * cB)),(- (T - T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(((1 - S) * T) + (S * cB)),(- (T - T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((((1 - S) * T) + (S * cB)),(- (T - T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366((((1 - S) * T) + (S * cB)),(T - T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
0. (TOP-REAL n) is Relation-like Function-like n -element V48( TOP-REAL n) V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
(((1 - S) * T) + (S * cB)) - (0. (TOP-REAL n)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
- (0. (TOP-REAL n)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K364((0. (TOP-REAL n))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K246((TOP-REAL n),(((1 - S) * T) + (S * cB)),(- (0. (TOP-REAL n)))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(((1 - S) * T) + (S * cB)),(- (0. (TOP-REAL n)))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((((1 - S) * T) + (S * cB)),(- (0. (TOP-REAL n)))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366((((1 - S) * T) + (S * cB)),(0. (TOP-REAL n))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
n is V21() ordinal natural real V32() cardinal ext-real non negative set
TOP-REAL n is non empty V90() V91() V160() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V188() TopSpace-like T_0 T_1 T_2 strict add-continuous Mult-continuous V310() V311() finite-dimensional RLTopStruct
the carrier of (TOP-REAL n) is functional non empty complex-functions-membered ext-real-functions-membered real-functions-membered set
T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
T - cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
- cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K364(cB) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K246((TOP-REAL n),T,(- cB)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
the U6 of (TOP-REAL n) is Relation-like K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) -defined the carrier of (TOP-REAL n) -valued Function-like non empty V14(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n))) quasi_total Function-yielding V275() complex-functions-valued ext-real-functions-valued real-functions-valued Element of K19(K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)))
K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) is Relation-like non empty set
K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)) is Relation-like non empty set
K19(K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n))) is non empty set
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),T,(- cB)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(T,(- cB)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366(T,cB) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
|.(T - cB).| is V21() real ext-real non negative Element of REAL
S is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
halfline (cB,S) is functional closed complex-functions-membered ext-real-functions-membered real-functions-membered Element of K19( the carrier of (TOP-REAL n))
K19( the carrier of (TOP-REAL n)) is non empty set
{ (((1 - b1) * cB) + (b1 * S)) where b1 is V21() real ext-real Element of REAL : 0 <= b1 } is set
s is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
s - cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),s,(- cB)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),s,(- cB)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(s,(- cB)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366(s,cB) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
|.(s - cB).| is V21() real ext-real non negative Element of REAL
S - cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),S,(- cB)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),S,(- cB)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(S,(- cB)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366(S,cB) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
|.(S - cB).| is V21() real ext-real non negative Element of REAL
Ts is V21() real ext-real set
1 - Ts is V21() real ext-real Element of REAL
- Ts is V21() real ext-real set
1 + (- Ts) is V21() real ext-real set
(1 - Ts) * cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(cB,(1 - Ts)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
Ts * S is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(S,Ts) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
((1 - Ts) * cB) + (Ts * S) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),((1 - Ts) * cB),(Ts * S)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(((1 - Ts) * cB),(Ts * S)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
abs Ts is V21() real ext-real Element of REAL
Ts * (S - cB) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368((S - cB),Ts) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(abs Ts) * |.(S - cB).| is V21() real ext-real Element of REAL
F is V21() real ext-real set
1 - F is V21() real ext-real Element of REAL
- F is V21() real ext-real set
1 + (- F) is V21() real ext-real set
(1 - F) * cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(cB,(1 - F)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
F * S is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(S,F) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
((1 - F) * cB) + (F * S) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),((1 - F) * cB),(F * S)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(((1 - F) * cB),(F * S)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
F * (S - cB) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368((S - cB),F) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
abs F is V21() real ext-real Element of REAL
(abs F) * |.(S - cB).| is V21() real ext-real Element of REAL
{cB} is functional non empty V12() V32() 1 -element closed compact complex-functions-membered ext-real-functions-membered real-functions-membered affinely-independent Element of K19( the carrier of (TOP-REAL n))
n is V21() ordinal natural real V32() cardinal ext-real non negative set
TOP-REAL n is non empty V90() V91() V160() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V188() TopSpace-like T_0 T_1 T_2 strict add-continuous Mult-continuous V310() V311() finite-dimensional RLTopStruct
the carrier of (TOP-REAL n) is functional non empty complex-functions-membered ext-real-functions-membered real-functions-membered set
K19( the carrier of (TOP-REAL n)) is non empty set
Euclid n is non empty strict Reflexive discerning V65() triangle V310() V311() MetrStruct
the carrier of (Euclid n) is functional non empty complex-functions-membered ext-real-functions-membered real-functions-membered set
T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
halfline (T,cB) is functional closed complex-functions-membered ext-real-functions-membered real-functions-membered Element of K19( the carrier of (TOP-REAL n))
{ (((1 - b1) * T) + (b1 * cB)) where b1 is V21() real ext-real Element of REAL : 0 <= b1 } is set
s is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K19( the carrier of (TOP-REAL n))
s /\ (halfline (T,cB)) is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K19( the carrier of (TOP-REAL n))
Fr s is functional closed complex-functions-membered ext-real-functions-membered real-functions-membered Element of K19( the carrier of (TOP-REAL n))
(Fr s) /\ (halfline (T,cB)) is functional closed complex-functions-membered ext-real-functions-membered real-functions-membered Element of K19( the carrier of (TOP-REAL n))
A is Relation-like Function-like V137() V138() V139() Element of the carrier of (Euclid n)
FR is Relation-like Function-like V137() V138() V139() Element of the carrier of (Euclid n)
dist (A,FR) is V21() real ext-real non negative Element of REAL
K19( the carrier of (Euclid n)) is non empty set
dist (FR,A) is V21() real ext-real non negative Element of REAL
cB - T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
- T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K364(T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K246((TOP-REAL n),cB,(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
the U6 of (TOP-REAL n) is Relation-like K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) -defined the carrier of (TOP-REAL n) -valued Function-like non empty V14(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n))) quasi_total Function-yielding V275() complex-functions-valued ext-real-functions-valued real-functions-valued Element of K19(K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)))
K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) is Relation-like non empty set
K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)) is Relation-like non empty set
K19(K20(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n))) is non empty set
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),cB,(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(cB,(- T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366(cB,T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
|.(cB - T).| is V21() real ext-real non negative Element of REAL
F is functional bounded complex-functions-membered ext-real-functions-membered real-functions-membered Element of K19( the carrier of (Euclid n))
diameter F is V21() real ext-real Element of REAL
{ b1 where b1 is V21() real ext-real Element of REAL : ( ((1 - b1) * T) + (b1 * cB) in F & {} <= b1 ) } is set
(diameter F) + 1 is V21() real ext-real Element of REAL
h is set
H is V21() real ext-real Element of REAL
1 - H is V21() real ext-real Element of REAL
- H is V21() real ext-real set
1 + (- H) is V21() real ext-real set
(1 - H) * T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(T,(1 - H)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
H * cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(cB,H) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
((1 - H) * T) + (H * cB) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),((1 - H) * T),(H * cB)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(((1 - H) * T),(H * cB)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
1 * T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(T,1) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
{} * cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(cB,{}) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
0. (TOP-REAL n) is Relation-like Function-like n -element V48( TOP-REAL n) V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
1 - {} is non empty V21() real ext-real positive non negative Element of REAL
- {} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V21() ordinal natural real V32() V33() V36() cardinal {} -element ext-real non positive non negative V137() V138() V139() V140() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V153() Function-yielding V275() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued set
1 + (- {}) is non empty V21() ordinal natural real V32() cardinal ext-real positive non negative set
(1 - {}) * T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(T,(1 - {})) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
((1 - {}) * T) + ({} * cB) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),((1 - {}) * T),({} * cB)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(((1 - {}) * T),({} * cB)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(diameter F) + {} is V21() real ext-real Element of REAL
H is ext-real set
h is non empty complex-membered ext-real-membered real-membered set
hfh is V21() real ext-real Element of REAL
1 - hfh is V21() real ext-real Element of REAL
- hfh is V21() real ext-real set
1 + (- hfh) is V21() real ext-real set
(1 - hfh) * T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(T,(1 - hfh)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
hfh * cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(cB,hfh) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
((1 - hfh) * T) + (hfh * cB) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),((1 - hfh) * T),(hfh * cB)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(((1 - hfh) * T),(hfh * cB)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(((1 - hfh) * T) + (hfh * cB)) - T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),(((1 - hfh) * T) + (hfh * cB)),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(((1 - hfh) * T) + (hfh * cB)),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((((1 - hfh) * T) + (hfh * cB)),(- T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366((((1 - hfh) * T) + (hfh * cB)),T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
hfh * (cB - T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368((cB - T),hfh) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
x is Relation-like Function-like V137() V138() V139() Element of the carrier of (Euclid n)
dist (x,A) is V21() real ext-real non negative Element of REAL
|.(hfh * (cB - T)).| is V21() real ext-real non negative Element of REAL
abs hfh is V21() real ext-real Element of REAL
(abs hfh) * |.(cB - T).| is V21() real ext-real Element of REAL
hfh * (dist (FR,A)) is V21() real ext-real Element of REAL
(hfh * (dist (FR,A))) / (dist (FR,A)) is V21() real ext-real Element of REAL
(dist (FR,A)) " is V21() real ext-real non negative set
(hfh * (dist (FR,A))) * ((dist (FR,A)) ") is V21() real ext-real set
(dist (FR,A)) / (dist (FR,A)) is V21() real ext-real non negative Element of REAL
(dist (FR,A)) * ((dist (FR,A)) ") is V21() real ext-real non negative set
hfh * ((dist (FR,A)) / (dist (FR,A))) is V21() real ext-real Element of REAL
hfh * 1 is V21() real ext-real Element of REAL
((diameter F) + 1) / (dist (FR,A)) is V21() real ext-real Element of REAL
((diameter F) + 1) * ((dist (FR,A)) ") is V21() real ext-real set
((diameter F) + 1) / (dist (A,FR)) is V21() real ext-real Element of REAL
(dist (A,FR)) " is V21() real ext-real non negative set
((diameter F) + 1) * ((dist (A,FR)) ") is V21() real ext-real set
sup h is ext-real set
H is V21() real ext-real Element of REAL
1 - H is V21() real ext-real Element of REAL
- H is V21() real ext-real set
1 + (- H) is V21() real ext-real set
(1 - H) * T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(T,(1 - H)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
H * cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(cB,H) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
((1 - H) * T) + (H * cB) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),((1 - H) * T),(H * cB)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(((1 - H) * T),(H * cB)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
x is Relation-like Function-like V137() V138() V139() Element of the carrier of (Euclid n)
hx is V21() real ext-real set
hx / |.(cB - T).| is V21() real ext-real Element of REAL
|.(cB - T).| " is V21() real ext-real non negative set
hx * (|.(cB - T).| ") is V21() real ext-real set
TS is ext-real set
I is V21() real ext-real Element of REAL
1 - I is V21() real ext-real Element of REAL
- I is V21() real ext-real set
1 + (- I) is V21() real ext-real set
(1 - I) * T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(T,(1 - I)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
I * cB is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368(cB,I) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
((1 - I) * T) + (I * cB) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),((1 - I) * T),(I * cB)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(((1 - I) * T),(I * cB)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
H - I is V21() real ext-real Element of REAL
H + (- I) is V21() real ext-real set
abs (H - I) is V21() real ext-real Element of REAL
nN0 is Relation-like Function-like V137() V138() V139() Element of the carrier of (Euclid n)
I * (cB - T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368((cB - T),I) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
T + (I * (cB - T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),T,(I * (cB - T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(T,(I * (cB - T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(((1 - H) * T) + (H * cB)) - (T + (I * (cB - T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
- (T + (I * (cB - T))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K364((T + (I * (cB - T)))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K246((TOP-REAL n),(((1 - H) * T) + (H * cB)),(- (T + (I * (cB - T))))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(((1 - H) * T) + (H * cB)),(- (T + (I * (cB - T))))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((((1 - H) * T) + (H * cB)),(- (T + (I * (cB - T))))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366((((1 - H) * T) + (H * cB)),(T + (I * (cB - T)))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(((1 - H) * T) + (H * cB)) - T is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),(((1 - H) * T) + (H * cB)),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(((1 - H) * T) + (H * cB)),(- T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((((1 - H) * T) + (H * cB)),(- T)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366((((1 - H) * T) + (H * cB)),T) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
((((1 - H) * T) + (H * cB)) - T) - (I * (cB - T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
- (I * (cB - T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K364((I * (cB - T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K246((TOP-REAL n),((((1 - H) * T) + (H * cB)) - T),(- (I * (cB - T)))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),((((1 - H) * T) + (H * cB)) - T),(- (I * (cB - T)))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362(((((1 - H) * T) + (H * cB)) - T),(- (I * (cB - T)))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366(((((1 - H) * T) + (H * cB)) - T),(I * (cB - T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
H * (cB - T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368((cB - T),H) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(H * (cB - T)) - (I * (cB - T)) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K246((TOP-REAL n),(H * (cB - T)),(- (I * (cB - T)))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K196( the carrier of (TOP-REAL n), the U6 of (TOP-REAL n),(H * (cB - T)),(- (I * (cB - T)))) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K362((H * (cB - T)),(- (I * (cB - T)))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
K366((H * (cB - T)),(I * (cB - T))) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
(H - I) * (cB - T) is Relation-like Function-like n -element V76() V137() V138() V139() Element of the carrier of (TOP-REAL n)
K368((cB - T),(H - I)) is Relation-like NAT -defined REAL -valued Function-like V76() V137() V138() V139() M7( REAL )
dist (x,nN0) is V21() real ext-real non negative Element of REAL
|.((H - I) * (cB - T)).| is V21() real ext-real non negative Element of REAL
(H - I) * |.(cB - T).| is V21() real ext-real Element of REAL
H - (hx / |.(cB - T).|) is V21() real ext-real Element of REAL
- (hx / |.(cB - T).|) is V21() real ext-real set
H + (- (hx / |.(cB - T).|)) is V21() real ext-real set
H - {} is V21() real ext-real Element of REAL
H + (- {}) is V21() real ext-real set
the topology of (TOP-REAL n) is non empty open Element of K19(K19( the carrier of (TOP-REAL n)))
K19(K19( the carrier of (TOP-REAL n))) is non empty set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is non empty set
hx is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K19( the carrier of (TOP-REAL n))
FrA is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
the topology of (TopSpaceMetr (Euclid n)) is non empty open Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
K19(K19( the carrier of (TopSpaceMetr (Euclid n)))) is non empty set
TS is V21() real ext-real set
Ball (x,TS) is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K19( the carrier of (Euclid n))
TS / |.(cB - T).| is V21() real ext-real Element of REAL
|.(cB - T).| " is V21() real ext-real non negative set
TS * (|.(cB - T).| ") is V21() real ext-real set
(TS / |.(cB - T).|) / 2 is V21() real ext-real Element of REAL
(TS / |.(cB - T).|) * (2 ") is V21() real ext-real set
H + ((TS / |.(cB - T).|) / 2) is V21() real ext-real Element of REAL
b is Relation-like Function-like V137() V138() V139() Element of the carrier of (Euclid n)
dist (x,b) is V21() real ext-real non negative Element of REAL
(TS / |.(cB - T).|) * |.(cB - T).| is V21() real ext-real Element of REAL
|.(cB - T).| / |.(cB