:: JORDAN5A semantic presentation

REAL is non empty V2() V45() V46() V47() V51() non finite non bounded_below non bounded_above V66() set
NAT is V45() V46() V47() V48() V49() V50() V51() bounded_below Element of K6(REAL)
K6(REAL) is non empty set

R^1 is non empty strict TopSpace-like V212() TopStruct
the carrier of I[01] is non empty V45() V46() V47() set
COMPLEX is non empty V2() V45() V51() non finite set
RAT is non empty V2() V45() V46() V47() V48() V51() non finite set
INT is non empty V2() V45() V46() V47() V48() V49() V51() non finite set
omega is V45() V46() V47() V48() V49() V50() V51() bounded_below set
K6(omega) is non empty set
K6(NAT) is non empty set
K7(COMPLEX,COMPLEX) is non empty V33() set
K6(K7(COMPLEX,COMPLEX)) is non empty set
K7(COMPLEX,REAL) is non empty V33() V34() V35() set
K6(K7(COMPLEX,REAL)) is non empty set
K7(REAL,REAL) is non empty V33() V34() V35() set
K6(K7(REAL,REAL)) is non empty set
1 is non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
K7(1,1) is non empty RAT -valued INT -valued V33() V34() V35() V36() set
K6(K7(1,1)) is non empty set
K7(K7(1,1),1) is non empty RAT -valued INT -valued V33() V34() V35() V36() set
K6(K7(K7(1,1),1)) is non empty set
K7(K7(1,1),REAL) is non empty V33() V34() V35() set
K6(K7(K7(1,1),REAL)) is non empty set
K7(K7(REAL,REAL),REAL) is non empty V33() V34() V35() set
K6(K7(K7(REAL,REAL),REAL)) is non empty set
2 is non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
K7(2,2) is non empty RAT -valued INT -valued V33() V34() V35() V36() set
K7(K7(2,2),REAL) is non empty V33() V34() V35() set
K6(K7(K7(2,2),REAL)) is non empty set
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict RLTopStruct
the carrier of () is non empty functional set
K6( the carrier of ()) is non empty set

the carrier of K479() is non empty V45() V46() V47() set

the carrier of R^1 is non empty V45() V46() V47() set

{{},1} is non empty finite set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty V33() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K7(RAT,RAT) is non empty RAT -valued V33() V34() V35() set
K6(K7(RAT,RAT)) is non empty set
K7(K7(RAT,RAT),RAT) is non empty RAT -valued V33() V34() V35() set
K6(K7(K7(RAT,RAT),RAT)) is non empty set
K7(INT,INT) is non empty RAT -valued INT -valued V33() V34() V35() set
K6(K7(INT,INT)) is non empty set
K7(K7(INT,INT),INT) is non empty RAT -valued INT -valued V33() V34() V35() set
K6(K7(K7(INT,INT),INT)) is non empty set
K7(NAT,NAT) is RAT -valued INT -valued V33() V34() V35() V36() set
K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued V33() V34() V35() V36() set
K6(K7(K7(NAT,NAT),NAT)) is non empty set
K7( the carrier of (),REAL) is non empty V33() V34() V35() set
K6(K7( the carrier of (),REAL)) is non empty set
ExtREAL is non empty V46() V66() set

[.0,1.] is V45() V46() V47() V66() closed Element of K6(REAL)

the carrier of RealSpace is non empty V45() V46() V47() set

K6( the carrier of R^1) is non empty set
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V212() SubSpace of R^1

Cl () is V45() V46() V47() Element of K6(REAL)
T is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict RLTopStruct
the carrier of () is non empty functional set
K6( the carrier of ()) is non empty set
f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
P is functional Element of K6( the carrier of ())

the carrier of (() | P) is set
K7( the carrier of I[01], the carrier of (() | P)) is set
K6(K7( the carrier of I[01], the carrier of (() | P))) is non empty set
R is Relation-like the carrier of I[01] -defined the carrier of (() | P) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of (() | P)))
R . 0 is set
R . 1 is set
rng R is Element of K6( the carrier of (() | P))
K6( the carrier of (() | P)) is non empty set
r is non empty functional Element of K6( the carrier of ())
() | r is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T
[#] (() | r) is non empty non proper open closed dense non boundary Element of K6( the carrier of (() | r))
the carrier of (() | r) is non empty set
K6( the carrier of (() | r)) is non empty set

T is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT

the carrier of () is non empty set
REAL T is non empty V72() M12( REAL )
TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict RLTopStruct
the carrier of () is non empty functional set
Pitag_dist T is non empty Relation-like K7((REAL T),(REAL T)) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7((REAL T),(REAL T)),REAL))
K7((REAL T),(REAL T)) is non empty set
K7(K7((REAL T),(REAL T)),REAL) is non empty V33() V34() V35() set
K6(K7(K7((REAL T),(REAL T)),REAL)) is non empty set
MetrStruct(# (REAL T),() #) is strict MetrStruct
T is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict RLTopStruct
the carrier of () is non empty functional set
f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
P is V11() real ext-real set
1 - P is V11() real ext-real Element of REAL
(1 - P) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(1 - P)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
P * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,P) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - P) * f) + (P * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 - P) * f),(P * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
R is V11() real ext-real set
1 - R is V11() real ext-real Element of REAL
(1 - R) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(1 - R)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
R * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,R) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - R) * f) + (R * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 - R) * f),(R * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
1 * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,1) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
P * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,P) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
- (P * f) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K526((P * f)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(- (P * f)) + (P * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((- (P * f)),(P * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(1 * f) + ((- (P * f)) + (P * g)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((1 * f),((- (P * f)) + (P * g))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(1 * f) + (- (P * f)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((1 * f),(- (P * f))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 * f) + (- (P * f))) + (P * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 * f) + (- (P * f))),(P * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(1 * f) - (P * f) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528((1 * f),(P * f)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 * f) - (P * f)) + (P * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 * f) - (P * f)),(P * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
R * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,R) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(1 * f) - (R * f) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528((1 * f),(R * f)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 * f) - (R * f)) + (R * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 * f) - (R * f)),(R * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
- (R * f) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K526((R * f)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(1 * f) + (- (R * f)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((1 * f),(- (R * f))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 * f) + (- (R * f))) + (R * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 * f) + (- (R * f))),(R * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(- (R * f)) + (R * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((- (R * f)),(R * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(1 * f) + ((- (R * f)) + (R * g)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((1 * f),((- (R * f)) + (R * g))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
R - P is V11() real ext-real set
(R - P) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(R - P)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((R - P) * f) + (P * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((R - P) * f),(P * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(R * f) - (P * f) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528((R * f),(P * f)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((R * f) - (P * f)) + (P * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((R * f) - (P * f)),(P * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(R * f) + (- (P * f)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((R * f),(- (P * f))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((R * f) + (- (P * f))) + (P * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((R * f) + (- (P * f))),(P * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(R * f) + ((- (P * f)) + (P * g)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((R * f),((- (P * f)) + (P * g))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(R * f) + ((- (R * f)) + (R * g)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((R * f),((- (R * f)) + (R * g))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(R * f) + (- (R * f)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((R * f),(- (R * f))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((R * f) + (- (R * f))) + (R * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((R * f) + (- (R * f))),(R * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
0. () is Relation-like Function-like V33() V34() V35() V69(T) V70() V88( TOP-REAL T) Element of the carrier of ()
the ZeroF of () is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
(0. ()) + (R * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((0. ()),(R * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((R - P) * f) + (0. ()) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((R - P) * f),(0. ())) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(P * g) - (P * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528((P * g),(P * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((R - P) * f) + ((P * g) - (P * g)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((R - P) * f),((P * g) - (P * g))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(R * g) - (P * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528((R * g),(P * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(R - P) * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,(R - P)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
T is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict RLTopStruct
the carrier of () is non empty functional set
f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
LSeg (f,g) is non empty functional V231( TOP-REAL T) Element of K6( the carrier of ())
K6( the carrier of ()) is non empty set
{ (((1 - b1) * f) + (b1 * g)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
() | (LSeg (f,g)) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T
the carrier of (() | (LSeg (f,g))) is non empty set
K7( the carrier of I[01], the carrier of (() | (LSeg (f,g)))) is non empty set
K6(K7( the carrier of I[01], the carrier of (() | (LSeg (f,g))))) is non empty set
REAL T is non empty V72() M12( REAL )

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
O is Element of K6( the carrier of ())
g is set
OO is V11() real ext-real Element of REAL
1 - OO is V11() real ext-real Element of REAL
(1 - OO) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(1 - OO)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
OO * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,OO) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - OO) * f) + (OO * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 - OO) * f),(OO * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
PP is V11() real ext-real Element of REAL
1 - PP is V11() real ext-real Element of REAL
(1 - PP) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(1 - PP)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
PP * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,PP) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - PP) * f) + (PP * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 - PP) * f),(PP * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )

dom g is set
rng g is set
OO is set
PP is set
g . PP is set
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
PQ1 is V11() real ext-real Element of REAL
1 - PQ1 is V11() real ext-real Element of REAL
(1 - PQ1) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(1 - PQ1)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
PQ1 * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,PQ1) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - PQ1) * f) + (PQ1 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 - PQ1) * f),(PQ1 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
[#] (() | (LSeg (f,g))) is non empty non proper open closed dense non boundary Element of K6( the carrier of (() | (LSeg (f,g))))
K6( the carrier of (() | (LSeg (f,g)))) is non empty set
PP is set
OO is non empty Relation-like the carrier of I[01] -defined the carrier of (() | (LSeg (f,g))) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (() | (LSeg (f,g)))))
dom OO is V45() V46() V47() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is non empty set
PQ1 is set
OO . PP is set
OO . PQ1 is set
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
g is V11() real ext-real Element of REAL
1 - g is V11() real ext-real Element of REAL
(1 - g) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(1 - g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
g * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,g) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - g) * f) + (g * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 - g) * f),(g * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
g1 is V11() real ext-real Element of REAL
1 - g1 is V11() real ext-real Element of REAL
(1 - g1) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(1 - g1)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
g1 * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,g1) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - g1) * f) + (g1 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 - g1) * f),(g1 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
g is non empty Element of K6( the carrier of ())

TopSpaceMetr (() | g) is TopStruct
g is V11() real ext-real Element of the carrier of I[01]
OO . g is Element of the carrier of (() | (LSeg (f,g)))
g1 is a_neighborhood of OO . g

the carrier of () is non empty set
Int g1 is open Element of K6( the carrier of (() | (LSeg (f,g))))
K6( the carrier of (() | (LSeg (f,g)))) is non empty set
f1 is Element of K6( the carrier of (() | (LSeg (f,g))))
[#] (() | (LSeg (f,g))) is non empty non proper open closed dense non boundary Element of K6( the carrier of (() | (LSeg (f,g))))
the carrier of (() | g) is non empty set
t is Element of the carrier of (() | g)
FFx is V11() real ext-real set
Ball (t,FFx) is Element of K6( the carrier of (() | g))
K6( the carrier of (() | g)) is non empty set
hh is V11() real ext-real Element of REAL
Pitag_dist T is non empty Relation-like K7((REAL T),(REAL T)) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7((REAL T),(REAL T)),REAL))
K7((REAL T),(REAL T)) is non empty set
K7(K7((REAL T),(REAL T)),REAL) is non empty V33() V34() V35() set
K6(K7(K7((REAL T),(REAL T)),REAL)) is non empty set
P is V69(T) Element of REAL T
R is V69(T) Element of REAL T
() . (P,R) is V11() real ext-real Element of REAL
hh / (() . (P,R)) is V11() real ext-real Element of REAL
GPQ is Element of the carrier of ()
Ball (GPQ,(hh / (() . (P,R)))) is Element of K6( the carrier of ())
K6( the carrier of ()) is non empty set

a9 is V45() V46() V47() Element of K6( the carrier of I[01])
MetrStruct(# (REAL T),() #) is strict MetrStruct
PP is Element of the carrier of ()
PQ1 is Element of the carrier of ()
dist (PP,PQ1) is V11() real ext-real Element of REAL
Int a9 is V45() V46() V47() open Element of K6( the carrier of I[01])
H is V45() V46() V47() a_neighborhood of g
OO .: H is Element of K6( the carrier of (() | (LSeg (f,g))))
Ball (t,hh) is Element of K6( the carrier of (() | g))
cc is Element of the carrier of ()
a is set
u is set
OO . u is set
Ex is V11() real ext-real Element of REAL
1 - Ex is V11() real ext-real Element of REAL
(1 - Ex) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(1 - Ex)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
Ex * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,Ex) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - Ex) * f) + (Ex * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 - Ex) * f),(Ex * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
u9 is Element of the carrier of ()
dist (GPQ,u9) is V11() real ext-real Element of REAL
the distance of () is non empty Relation-like K7( the carrier of (), the carrier of ()) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7( the carrier of (), the carrier of ()),REAL))
K7( the carrier of (), the carrier of ()) is non empty set
K7(K7( the carrier of (), the carrier of ()),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of (), the carrier of ()),REAL)) is non empty set
the distance of () . (GPQ,u9) is V11() real ext-real Element of REAL
the distance of RealSpace is non empty Relation-like K7( the carrier of RealSpace, the carrier of RealSpace) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL))
K7( the carrier of RealSpace, the carrier of RealSpace) is non empty V33() V34() V35() set
K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL)) is non empty set
W99 is V11() real ext-real Element of the carrier of RealSpace
u99 is V11() real ext-real Element of the carrier of RealSpace
the distance of RealSpace . (W99,u99) is V11() real ext-real Element of REAL
dist (W99,u99) is V11() real ext-real Element of REAL
u1 is V11() real ext-real Element of REAL
Ex - u1 is V11() real ext-real Element of REAL
abs (Ex - u1) is V11() real ext-real Element of REAL
u1 - Ex is V11() real ext-real Element of REAL
- (u1 - Ex) is V11() real ext-real Element of REAL
abs (- (u1 - Ex)) is V11() real ext-real Element of REAL
abs (u1 - Ex) is V11() real ext-real Element of REAL
hh / (hh / (() . (P,R))) is V11() real ext-real Element of REAL
P - R is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V69(T) V70() M13( REAL , REAL T)
|.(P - R).| is V11() real ext-real non negative Element of REAL
rng OO is Element of K6( the carrier of (() | (LSeg (f,g))))
aa is Element of the carrier of (() | g)
aa9 is Element of the carrier of ()
aa1 is V69(T) Element of REAL T
1 - u1 is V11() real ext-real Element of REAL
(1 - u1) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(1 - u1)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
u1 * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,u1) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - u1) * f) + (u1 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 - u1) * f),(u1 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
WW1 is V69(T) Element of REAL T
WW1 - aa1 is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V69(T) V70() M13( REAL , REAL T)
(((1 - Ex) * f) + (Ex * g)) - (((1 - u1) * f) + (u1 * g)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528((((1 - Ex) * f) + (Ex * g)),(((1 - u1) * f) + (u1 * g))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(Ex * g) + ((1 - Ex) * f) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((Ex * g),((1 - Ex) * f)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((Ex * g) + ((1 - Ex) * f)) - ((1 - u1) * f) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528(((Ex * g) + ((1 - Ex) * f)),((1 - u1) * f)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(((Ex * g) + ((1 - Ex) * f)) - ((1 - u1) * f)) - (u1 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528((((Ex * g) + ((1 - Ex) * f)) - ((1 - u1) * f)),(u1 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - Ex) * f) - ((1 - u1) * f) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528(((1 - Ex) * f),((1 - u1) * f)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(Ex * g) + (((1 - Ex) * f) - ((1 - u1) * f)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((Ex * g),(((1 - Ex) * f) - ((1 - u1) * f))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((Ex * g) + (((1 - Ex) * f) - ((1 - u1) * f))) - (u1 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528(((Ex * g) + (((1 - Ex) * f) - ((1 - u1) * f))),(u1 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(1 - Ex) - (1 - u1) is V11() real ext-real Element of REAL
((1 - Ex) - (1 - u1)) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,((1 - Ex) - (1 - u1))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(Ex * g) + (((1 - Ex) - (1 - u1)) * f) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((Ex * g),(((1 - Ex) - (1 - u1)) * f)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((Ex * g) + (((1 - Ex) - (1 - u1)) * f)) - (u1 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528(((Ex * g) + (((1 - Ex) - (1 - u1)) * f)),(u1 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(u1 - Ex) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(u1 - Ex)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(Ex * g) - (u1 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528((Ex * g),(u1 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((u1 - Ex) * f) + ((Ex * g) - (u1 * g)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((u1 - Ex) * f),((Ex * g) - (u1 * g))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(Ex - u1) * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,(Ex - u1)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((u1 - Ex) * f) + ((Ex - u1) * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((u1 - Ex) * f),((Ex - u1) * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(- (u1 - Ex)) * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,(- (u1 - Ex))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((u1 - Ex) * f) + ((- (u1 - Ex)) * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((u1 - Ex) * f),((- (u1 - Ex)) * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(u1 - Ex) * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,(u1 - Ex)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
- ((u1 - Ex) * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K526(((u1 - Ex) * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((u1 - Ex) * f) + (- ((u1 - Ex) * g)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((u1 - Ex) * f),(- ((u1 - Ex) * g))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((u1 - Ex) * f) - ((u1 - Ex) * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528(((u1 - Ex) * f),((u1 - Ex) * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
f - g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K528(f,g) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(u1 - Ex) * (f - g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530((f - g),(u1 - Ex)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(u1 - Ex) * (P - R) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V69(T) V70() M13( REAL , REAL T)
|.(WW1 - aa1).| is V11() real ext-real non negative Element of REAL
(abs (u1 - Ex)) * |.(P - R).| is V11() real ext-real Element of REAL
(hh / (() . (P,R))) * (hh / (hh / (() . (P,R)))) is V11() real ext-real Element of REAL
the distance of () is non empty Relation-like K7( the carrier of (), the carrier of ()) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7( the carrier of (), the carrier of ()),REAL))
K7( the carrier of (), the carrier of ()) is non empty set
K7(K7( the carrier of (), the carrier of ()),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of (), the carrier of ()),REAL)) is non empty set
the distance of () . (cc,aa9) is V11() real ext-real Element of REAL
the distance of (() | g) is non empty Relation-like K7( the carrier of (() | g), the carrier of (() | g)) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7( the carrier of (() | g), the carrier of (() | g)),REAL))
K7( the carrier of (() | g), the carrier of (() | g)) is non empty set
K7(K7( the carrier of (() | g), the carrier of (() | g)),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of (() | g), the carrier of (() | g)),REAL)) is non empty set
the distance of (() | g) . (t,aa) is V11() real ext-real Element of REAL
dist (t,aa) is V11() real ext-real Element of REAL
OO . 0 is set
OO . 1 is set
PP is V11() real ext-real Element of REAL
OO . PP is set
1 - PP is V11() real ext-real Element of REAL
(1 - PP) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(1 - PP)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
PP * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,PP) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - PP) * f) + (PP * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 - PP) * f),(PP * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
[#] (() | (LSeg (f,g))) is non empty non proper open closed dense non boundary Element of K6( the carrier of (() | (LSeg (f,g))))
K6( the carrier of (() | (LSeg (f,g)))) is non empty set
rng OO is Element of K6( the carrier of (() | (LSeg (f,g))))
PP is set
PQ1 is V11() real ext-real Element of REAL
1 - PQ1 is V11() real ext-real Element of REAL
(1 - PQ1) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(1 - PQ1)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
PQ1 * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,PQ1) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - PQ1) * f) + (PQ1 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 - PQ1) * f),(PQ1 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
OO . PQ1 is set
[#] I[01] is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of I[01])
1 - 0 is non empty V11() real ext-real positive non negative Element of REAL
(1 - 0) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(1 - 0)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
0 * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()

((1 - 0) * f) + (0 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 - 0) * f),(0 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
f + (0 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(f,(0 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
0. () is Relation-like Function-like V33() V34() V35() V69(T) V70() V88( TOP-REAL T) Element of the carrier of ()
the ZeroF of () is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
f + (0. ()) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(f,(0. ())) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
1 - 1 is V11() real ext-real Element of REAL
(1 - 1) * f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(f,(1 - 1)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
1 * g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K530(g,1) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - 1) * f) + (1 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524(((1 - 1) * f),(1 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(0. ()) + (1 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
K524((0. ()),(1 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
T is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict RLTopStruct
the carrier of () is non empty functional set
g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
P is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of ()
LSeg (g,P) is non empty functional V231( TOP-REAL T) Element of K6( the carrier of ())
K6( the carrier of ()) is non empty set
{ (((1 - b1) * g) + (b1 * P)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
() | (LSeg (g,P)) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T
the carrier of (() | (LSeg (g,P))) is non empty set
K7( the carrier of I[01], the carrier of (() | (LSeg (g,P)))) is non empty set
K6(K7( the carrier of I[01], the carrier of (() | (LSeg (g,P))))) is non empty set
r is non empty Relation-like the carrier of I[01] -defined the carrier of (() | (LSeg (g,P))) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (() | (LSeg (g,P)))))
r . 0 is set
r . 1 is set
rng r is Element of K6( the carrier of (() | (LSeg (g,P))))
K6( the carrier of (() | (LSeg (g,P)))) is non empty set
[#] (() | (LSeg (g,P))) is non empty non proper open closed dense non boundary Element of K6( the carrier of (() | (LSeg (g,P))))
dom r is V45() V46() V47() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is non empty set
K7( the carrier of I[01], the carrier of ()) is non empty set
K6(K7( the carrier of I[01], the carrier of ())) is non empty set
O is non empty Relation-like the carrier of I[01] -defined the carrier of () -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ()))
T is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict RLTopStruct
T is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT

the carrier of () is non empty functional set
K6( the carrier of ()) is non empty set
the non empty functional closed compact Element of K6( the carrier of ()) is non empty functional closed compact Element of K6( the carrier of ())
() | the non empty functional closed compact Element of K6( the carrier of ()) is non empty strict TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL T
g is non empty TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T
T is Relation-like Function-like V33() V34() V35() V69(2) V70() Element of the carrier of ()
f is Relation-like Function-like V33() V34() V35() V69(2) V70() Element of the carrier of ()
g is non empty Relation-like the carrier of I[01] -defined the carrier of () -valued Function-like total quasi_total continuous Path of T,f
rng g is functional Element of K6( the carrier of ())

the carrier of P is non empty set
K7( the carrier of I[01], the carrier of P) is non empty set
K6(K7( the carrier of I[01], the carrier of P)) is non empty set
[#] P is non empty non proper open closed dense non boundary Element of K6( the carrier of P)
K6( the carrier of P) is non empty set
R is non empty Relation-like the carrier of I[01] -defined the carrier of P -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of P))
dom R is V45() V46() V47() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is non empty set
[#] I[01] is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of I[01])
Family_open_set RealSpace is Element of K6(K6( the carrier of RealSpace))
K6( the carrier of RealSpace) is non empty set
K6(K6( the carrier of RealSpace)) is non empty set
T is V45() V46() V47() Element of K6(REAL)
g is V11() real ext-real Element of the carrier of RealSpace
P is V11() real ext-real Element of REAL
R is V45() V46() V47() open Neighbourhood of P
r is V11() real ext-real set
P - r is V11() real ext-real Element of REAL
P + r is V11() real ext-real Element of REAL
].(P - r),(P + r).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
O is V11() real ext-real Element of REAL
Ball (g,O) is V45() V46() V47() Element of K6( the carrier of RealSpace)
g is set
OO is V11() real ext-real Element of REAL
g is V11() real ext-real Element of the carrier of RealSpace
OO - P is V11() real ext-real Element of REAL
abs (OO - P) is V11() real ext-real Element of REAL
real_dist . (OO,P) is V11() real ext-real Element of REAL
g is V11() real ext-real Element of the carrier of RealSpace
dist (g,g) is V11() real ext-real Element of REAL
real_dist . (P,OO) is V11() real ext-real Element of REAL
PQ1 is V11() real ext-real Element of REAL
PP is V11() real ext-real Element of REAL
real_dist . (PQ1,PP) is V11() real ext-real Element of REAL
g is set
{ b1 where b1 is V11() real ext-real Element of the carrier of RealSpace : not O <= dist (g,b1) } is set
g is V11() real ext-real Element of the carrier of RealSpace
dist (g,g) is V11() real ext-real Element of REAL
PQ1 is V11() real ext-real Element of REAL
PP is V11() real ext-real Element of REAL
real_dist . (PQ1,PP) is V11() real ext-real Element of REAL
OO is V11() real ext-real Element of REAL
OO - P is V11() real ext-real Element of REAL
abs (OO - P) is V11() real ext-real Element of REAL
f is V45() V46() V47() Element of K6( the carrier of RealSpace)
T is V45() V46() V47() Element of K6(REAL)
f is V11() real ext-real set
g is V11() real ext-real Element of REAL
P is V11() real ext-real Element of the carrier of RealSpace
R is V11() real ext-real Element of REAL
Ball (P,R) is V45() V46() V47() Element of K6( the carrier of RealSpace)
O is V11() real ext-real Element of REAL
g - O is V11() real ext-real Element of REAL
g + O is V11() real ext-real Element of REAL
].(g - O),(g + O).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
r is V45() V46() V47() Element of K6(REAL)
g is set
g is V11() real ext-real Element of REAL
PP is V11() real ext-real Element of the carrier of RealSpace
g - g is V11() real ext-real Element of REAL
abs (g - g) is V11() real ext-real Element of REAL
real_dist . (g,g) is V11() real ext-real Element of REAL
OO is V11() real ext-real Element of the carrier of RealSpace
dist (PP,OO) is V11() real ext-real Element of REAL
real_dist . (g,g) is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
PQ1 is V11() real ext-real Element of REAL
real_dist . (g,PQ1) is V11() real ext-real Element of REAL
g is set
{ b1 where b1 is V11() real ext-real Element of the carrier of RealSpace : not O <= dist (P,b1) } is set
g is V11() real ext-real Element of the carrier of RealSpace
dist (P,g) is V11() real ext-real Element of REAL
PQ1 is V11() real ext-real Element of REAL
PP is V11() real ext-real Element of REAL
real_dist . (PQ1,PP) is V11() real ext-real Element of REAL
OO is V11() real ext-real Element of REAL
OO - g is V11() real ext-real Element of REAL
abs (OO - g) is V11() real ext-real Element of REAL
r is V45() V46() V47() Element of K6(REAL)
g is V11() real ext-real Element of REAL
g - g is V11() real ext-real Element of REAL
g + g is V11() real ext-real Element of REAL
].(g - g),(g + g).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
O is V45() V46() V47() open Neighbourhood of g
R is V45() V46() V47() open Neighbourhood of g
T is V45() V46() V47() Element of K6(REAL)
f is V45() V46() V47() Element of K6(REAL)
K7( the carrier of R^1, the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of R^1, the carrier of R^1)) is non empty set
T is non empty Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7( the carrier of R^1, the carrier of R^1))
f is V11() real ext-real Element of the carrier of R^1

P is V11() real ext-real Element of REAL
g . P is V11() real ext-real set
T . f is V11() real ext-real Element of the carrier of R^1
r is V45() V46() V47() open Neighbourhood of g . P
g is V45() V46() V47() Element of K6( the carrier of RealSpace)
the topology of is open Element of K6(K6( the carrier of ))
the carrier of is set
K6( the carrier of ) is non empty set
K6(K6( the carrier of )) is non empty set
O is V45() V46() V47() Element of K6( the carrier of R^1)
R is V11() real ext-real Element of the carrier of R^1
g is V45() V46() V47() a_neighborhood of R
OO is V45() V46() V47() a_neighborhood of f
T .: OO is V45() V46() V47() Element of K6( the carrier of R^1)
PP is V45() V46() V47() Element of K6( the carrier of R^1)
the topology of R^1 is non empty open Element of K6(K6( the carrier of R^1))
K6(K6( the carrier of R^1)) is non empty set
PQ1 is V45() V46() V47() Element of K6(REAL)
g is V45() V46() V47() open Neighbourhood of P
g .: g is V45() V46() V47() Element of K6(REAL)
g .: OO is V45() V46() V47() Element of K6(REAL)
T is non empty Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like total quasi_total V33() V34() V35() continuous Element of K6(K7( the carrier of R^1, the carrier of R^1))

dom f is V45() V46() V47() Element of K6(REAL)
g is V11() real ext-real set
P is V11() real ext-real Element of REAL
R is V11() real ext-real Element of the carrier of R^1
T is non empty Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like one-to-one total quasi_total V33() V34() V35() continuous Element of K6(K7( the carrier of R^1, the carrier of R^1))

dom T is V45() V46() V47() Element of K6( the carrier of R^1)
T is non empty Relation-like the carrier of R^1 -defined the carrier of R^1 -valued Function-like one-to-one total quasi_total V33() V34() V35() continuous Element of K6(K7( the carrier of R^1, the carrier of R^1))
dom T is V45() V46() V47() Element of K6( the carrier of R^1)
[.0,1.] /\ (dom T) is V45() V46() V47() Element of K6( the carrier of R^1)
[.0,1.] /\ the carrier of R^1 is V45() V46() V47() Element of K6(REAL)

g is V11() real ext-real Element of the carrier of I[01]
R is V11() real ext-real Element of REAL
P is V11() real ext-real Element of the carrier of I[01]
r is V11() real ext-real Element of REAL
O is V11() real ext-real Element of REAL
T . g is V11() real ext-real set
g is V11() real ext-real Element of REAL
T . P is V11() real ext-real set
g is V11() real ext-real Element of the carrier of I[01]
PP is V11() real ext-real Element of REAL
OO is V11() real ext-real Element of the carrier of I[01]
PQ1 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
T . g is V11() real ext-real set
g1 is V11() real ext-real Element of REAL
T . OO is V11() real ext-real set

g is V11() real ext-real Element of the carrier of I[01]
R is V11() real ext-real Element of REAL
P is V11() real ext-real Element of the carrier of I[01]
r is V11() real ext-real Element of REAL
O is V11() real ext-real Element of REAL
T . g is V11() real ext-real set
g is V11() real ext-real Element of REAL
T . P is V11() real ext-real set
g is V11() real ext-real Element of the carrier of I[01]
PP is V11() real ext-real Element of REAL
OO is V11() real ext-real Element of the carrier of I[01]
PQ1 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
T . g is V11() real ext-real set
g1 is V11() real ext-real Element of REAL
T . OO is V11() real ext-real set

g is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL

the carrier of () is non empty set
T is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
T - f is V11() real ext-real Element of REAL
T + f is V11() real ext-real Element of REAL
].(T - f),(T + f).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
[.g,P.] is V45() V46() V47() V66() closed Element of K6(REAL)
R is Element of the carrier of ()
Ball (R,f) is Element of K6( the carrier of ())
K6( the carrier of ()) is non empty set
g is set
{ b1 where b1 is Element of the carrier of () : not f <= dist (R,b1) } is set
OO is Element of the carrier of ()
dist (R,OO) is V11() real ext-real Element of REAL
PQ1 is Element of the carrier of ()
g is Element of the carrier of ()
dist (PQ1,g) is V11() real ext-real Element of REAL
the distance of () is non empty Relation-like K7( the carrier of (), the carrier of ()) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7( the carrier of (), the carrier of ()),REAL))
K7( the carrier of (), the carrier of ()) is non empty set
K7(K7( the carrier of (), the carrier of ()),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of (), the carrier of ()),REAL)) is non empty set
the distance of () . (PQ1,g) is V11() real ext-real Element of REAL
real_dist . (PQ1,g) is set
GPQ is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
real_dist . (GPQ,g1) is V11() real ext-real Element of REAL
PP is V11() real ext-real Element of REAL
PP - T is V11() real ext-real Element of REAL
abs (PP - T) is V11() real ext-real Element of REAL
g is set
OO is V11() real ext-real Element of REAL
OO - T is V11() real ext-real Element of REAL
abs (OO - T) is V11() real ext-real Element of REAL
real_dist . (OO,T) is V11() real ext-real Element of REAL
PP is Element of the carrier of ()
dist (R,PP) is V11() real ext-real Element of REAL
the distance of () is non empty Relation-like K7( the carrier of (), the carrier of ()) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7( the carrier of (), the carrier of ()),REAL))
K7( the carrier of (), the carrier of ()) is non empty set
K7(K7( the carrier of (), the carrier of ()),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of (), the carrier of ()),REAL)) is non empty set
the distance of () . (R,PP) is V11() real ext-real Element of REAL
real_dist . (R,PP) is set
f is V11() real ext-real Element of REAL
T is V11() real ext-real Element of REAL

Family_open_set () is Element of K6(K6( the carrier of ()))
the carrier of () is non empty set
K6( the carrier of ()) is non empty set
K6(K6( the carrier of ())) is non empty set
g is V45() V46() V47() Element of K6(REAL)
R is V11() real ext-real set
r is V11() real ext-real Element of REAL
P is Element of K6( the carrier of ())
[.T,f.] is V45() V46() V47() V66() closed Element of K6(REAL)
O is Element of the carrier of ()
{ b1 where b1 is V11() real ext-real Element of REAL : ( T <= b1 & b1 <= f ) } is set
r - T is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
Ball (O,g) is Element of K6( the carrier of ())
T + f is V11() real ext-real Element of REAL
(T + f) / 2 is V11() real ext-real Element of REAL
min ((r - T),g) is V11() real ext-real Element of REAL
OO is V11() real ext-real Element of REAL
r - (min ((r - T),g)) is V11() real ext-real Element of REAL
r + (min ((r - T),g)) is V11() real ext-real Element of REAL
].(r - (min ((r - T),g))),(r + (min ((r - T),g))).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
OO is V45() V46() V47() open Neighbourhood of r
2 * r is V11() real ext-real Element of REAL
2 * ((T + f) / 2) is V11() real ext-real Element of REAL
(2 * r) - T is V11() real ext-real Element of REAL
(T + f) - T is V11() real ext-real Element of REAL
PP is set
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= r - (min ((r - T),g)) & not r + (min ((r - T),g)) <= b1 ) } is set
PQ1 is V11() real ext-real