:: 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
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact SubSpace of R^1
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 (TOP-REAL 2) is non empty functional set
K6( the carrier of (TOP-REAL 2)) is non empty set
K479() is non empty strict TopSpace-like T_0 T_1 T_2 compact V212() pathwise_connected pseudocompact TopStruct
the carrier of K479() is non empty V45() V46() V47() set
RealSpace is non empty strict Reflexive discerning V129() triangle Discerning V212() MetrStruct
the carrier of R^1 is non empty V45() V46() V47() set
{} is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() set
the empty Function-like functional V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() set is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() 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 (TOP-REAL 2),REAL) is non empty V33() V34() V35() set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is non empty set
ExtREAL is non empty V46() V66() set
0 is empty natural V11() real ext-real non positive non negative Function-like functional V43() V44() V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() Element of NAT
[.0,1.] is V45() V46() V47() V66() closed Element of K6(REAL)
real_dist is non empty Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
the carrier of RealSpace is non empty V45() V46() V47() set
TopSpaceMetr RealSpace is TopStruct
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
{} REAL is empty proper Function-like functional V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() Element of K6(REAL)
Cl ({} REAL) 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 (TOP-REAL T) is non empty functional set
K6( the carrier of (TOP-REAL T)) is non empty set
f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
P is functional Element of K6( the carrier of (TOP-REAL T))
(TOP-REAL T) | P is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T
the carrier of ((TOP-REAL T) | P) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL T) | P)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL T) | P))) is non empty set
R is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL T) | P) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL T) | P)))
R . 0 is set
R . 1 is set
rng R is Element of K6( the carrier of ((TOP-REAL T) | P))
K6( the carrier of ((TOP-REAL T) | P)) is non empty set
r is non empty functional Element of K6( the carrier of (TOP-REAL T))
(TOP-REAL T) | r is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T
[#] ((TOP-REAL T) | r) is non empty non proper open closed dense non boundary Element of K6( the carrier of ((TOP-REAL T) | r))
the carrier of ((TOP-REAL T) | r) is non empty set
K6( the carrier of ((TOP-REAL T) | r)) is non empty set
{} (TOP-REAL T) is empty proper Function-like functional V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() open closed boundary nowhere_dense compact V180( TOP-REAL T) circled Element of K6( the carrier of (TOP-REAL T))
{} (TOP-REAL T) is empty proper Function-like functional V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() open closed boundary nowhere_dense compact V180( TOP-REAL T) circled Element of K6( the carrier of (TOP-REAL T))
T is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
Euclid T is non empty strict Reflexive discerning V129() triangle Discerning MetrStruct
the carrier of (Euclid T) 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 (TOP-REAL T) 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),(Pitag_dist 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 (TOP-REAL T) is non empty functional set
f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
K524(((R * f) + (- (R * f))),(R * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
0. (TOP-REAL T) is Relation-like Function-like V33() V34() V35() V69(T) V70() V88( TOP-REAL T) Element of the carrier of (TOP-REAL T)
the ZeroF of (TOP-REAL T) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
(0. (TOP-REAL T)) + (R * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
K524((0. (TOP-REAL T)),(R * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((R - P) * f) + (0. (TOP-REAL T)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
K524(((R - P) * f),(0. (TOP-REAL T))) 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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T) is non empty functional set
f is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
LSeg (f,g) is non empty functional V231( TOP-REAL T) Element of K6( the carrier of (TOP-REAL T))
K6( the carrier of (TOP-REAL T)) is non empty set
{ (((1 - b₁) * f) + (b₁ * g)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(TOP-REAL T) | (LSeg (f,g)) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T
the carrier of ((TOP-REAL T) | (LSeg (f,g))) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL T) | (LSeg (f,g)))) is non empty set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL T) | (LSeg (f,g))))) is non empty set
REAL T is non empty V72() M12( REAL )
Euclid T is non empty strict Reflexive discerning V129() triangle Discerning MetrStruct
the carrier of (Euclid T) is non empty set
K6( the carrier of (Euclid T)) is non empty set
O is Element of K6( the carrier of (Euclid T))
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
K524(((1 - PP) * f),(PP * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
g is Relation-like Function-like set
dom g is set
rng g is set
OO is set
PP is set
g . PP is set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
K524(((1 - PQ1) * f),(PQ1 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
[#] ((TOP-REAL T) | (LSeg (f,g))) is non empty non proper open closed dense non boundary Element of K6( the carrier of ((TOP-REAL T) | (LSeg (f,g))))
K6( the carrier of ((TOP-REAL T) | (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 ((TOP-REAL T) | (LSeg (f,g))) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL T) | (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
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (Euclid T))
(Euclid T) | g is non empty strict Reflexive discerning V129() triangle Discerning SubSpace of Euclid T
TopSpaceMetr ((Euclid T) | g) is TopStruct
g is V11() real ext-real Element of the carrier of I[01]
OO . g is Element of the carrier of ((TOP-REAL T) | (LSeg (f,g)))
g1 is a_neighborhood of OO . g
Closed-Interval-MSpace (0,1) is non empty strict Reflexive discerning V129() triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (0,1)) is non empty set
Int g1 is open Element of K6( the carrier of ((TOP-REAL T) | (LSeg (f,g))))
K6( the carrier of ((TOP-REAL T) | (LSeg (f,g)))) is non empty set
f1 is Element of K6( the carrier of ((TOP-REAL T) | (LSeg (f,g))))
[#] ((TOP-REAL T) | (LSeg (f,g))) is non empty non proper open closed dense non boundary Element of K6( the carrier of ((TOP-REAL T) | (LSeg (f,g))))
the carrier of ((Euclid T) | g) is non empty set
t is Element of the carrier of ((Euclid T) | g)
FFx is V11() real ext-real set
Ball (t,FFx) is Element of K6( the carrier of ((Euclid T) | g))
K6( the carrier of ((Euclid T) | 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
(Pitag_dist T) . (P,R) is V11() real ext-real Element of REAL
hh / ((Pitag_dist T) . (P,R)) is V11() real ext-real Element of REAL
GPQ is Element of the carrier of (Closed-Interval-MSpace (0,1))
Ball (GPQ,(hh / ((Pitag_dist T) . (P,R)))) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
K6( the carrier of (Closed-Interval-MSpace (0,1))) is non empty set
TopSpaceMetr (Closed-Interval-MSpace (0,1)) is TopStruct
a9 is V45() V46() V47() Element of K6( the carrier of I[01])
MetrStruct(# (REAL T),(Pitag_dist T) #) is strict MetrStruct
PP is Element of the carrier of (Euclid T)
PQ1 is Element of the carrier of (Euclid T)
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 ((TOP-REAL T) | (LSeg (f,g))))
Ball (t,hh) is Element of K6( the carrier of ((Euclid T) | g))
cc is Element of the carrier of (Euclid T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (Closed-Interval-MSpace (0,1))
dist (GPQ,u9) is V11() real ext-real Element of REAL
the distance of (Closed-Interval-MSpace (0,1)) is non empty Relation-like K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Closed-Interval-MSpace (0,1))) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Closed-Interval-MSpace (0,1))),REAL))
K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Closed-Interval-MSpace (0,1))) is non empty set
K7(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Closed-Interval-MSpace (0,1))),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Closed-Interval-MSpace (0,1))),REAL)) is non empty set
the distance of (Closed-Interval-MSpace (0,1)) . (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 / ((Pitag_dist T) . (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 ((TOP-REAL T) | (LSeg (f,g))))
aa is Element of the carrier of ((Euclid T) | g)
aa9 is Element of the carrier of (Euclid T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 / ((Pitag_dist T) . (P,R))) * (hh / (hh / ((Pitag_dist T) . (P,R)))) is V11() real ext-real Element of REAL
the distance of (Euclid T) is non empty Relation-like K7( the carrier of (Euclid T), the carrier of (Euclid T)) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7( the carrier of (Euclid T), the carrier of (Euclid T)),REAL))
K7( the carrier of (Euclid T), the carrier of (Euclid T)) is non empty set
K7(K7( the carrier of (Euclid T), the carrier of (Euclid T)),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of (Euclid T), the carrier of (Euclid T)),REAL)) is non empty set
the distance of (Euclid T) . (cc,aa9) is V11() real ext-real Element of REAL
the distance of ((Euclid T) | g) is non empty Relation-like K7( the carrier of ((Euclid T) | g), the carrier of ((Euclid T) | g)) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7( the carrier of ((Euclid T) | g), the carrier of ((Euclid T) | g)),REAL))
K7( the carrier of ((Euclid T) | g), the carrier of ((Euclid T) | g)) is non empty set
K7(K7( the carrier of ((Euclid T) | g), the carrier of ((Euclid T) | g)),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of ((Euclid T) | g), the carrier of ((Euclid T) | g)),REAL)) is non empty set
the distance of ((Euclid T) | 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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
K524(((1 - PP) * f),(PP * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
[#] ((TOP-REAL T) | (LSeg (f,g))) is non empty non proper open closed dense non boundary Element of K6( the carrier of ((TOP-REAL T) | (LSeg (f,g))))
K6( the carrier of ((TOP-REAL T) | (LSeg (f,g)))) is non empty set
rng OO is Element of K6( the carrier of ((TOP-REAL T) | (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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
K530(g,0) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
((1 - 0) * f) + (0 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
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 (TOP-REAL T)
K524(f,(0 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
0. (TOP-REAL T) is Relation-like Function-like V33() V34() V35() V69(T) V70() V88( TOP-REAL T) Element of the carrier of (TOP-REAL T)
the ZeroF of (TOP-REAL T) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
f + (0. (TOP-REAL T)) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
K524(f,(0. (TOP-REAL T))) 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 (TOP-REAL T)
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 (TOP-REAL T)
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 (TOP-REAL T)
K524(((1 - 1) * f),(1 * g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V70() M11( REAL )
(0. (TOP-REAL T)) + (1 * g) is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
K524((0. (TOP-REAL T)),(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 (TOP-REAL T) is non empty functional set
g is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
P is Relation-like Function-like V33() V34() V35() V69(T) V70() Element of the carrier of (TOP-REAL T)
LSeg (g,P) is non empty functional V231( TOP-REAL T) Element of K6( the carrier of (TOP-REAL T))
K6( the carrier of (TOP-REAL T)) is non empty set
{ (((1 - b₁) * g) + (b₁ * P)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(TOP-REAL T) | (LSeg (g,P)) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T
the carrier of ((TOP-REAL T) | (LSeg (g,P))) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL T) | (LSeg (g,P)))) is non empty set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL T) | (LSeg (g,P))))) is non empty set
r is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL T) | (LSeg (g,P))) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL T) | (LSeg (g,P)))))
r . 0 is set
r . 1 is set
rng r is Element of K6( the carrier of ((TOP-REAL T) | (LSeg (g,P))))
K6( the carrier of ((TOP-REAL T) | (LSeg (g,P)))) is non empty set
[#] ((TOP-REAL T) | (LSeg (g,P))) is non empty non proper open closed dense non boundary Element of K6( the carrier of ((TOP-REAL T) | (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 (TOP-REAL T)) is non empty set
K6(K7( the carrier of I[01], the carrier of (TOP-REAL T))) is non empty set
O is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL T) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL T)))
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
TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V146() V171() V172() V173() V174() V175() V176() V177() strict pathwise_connected RLTopStruct
the carrier of (TOP-REAL T) is non empty functional set
K6( the carrier of (TOP-REAL T)) is non empty set
the non empty functional closed compact Element of K6( the carrier of (TOP-REAL T)) is non empty functional closed compact Element of K6( the carrier of (TOP-REAL T))
(TOP-REAL T) | the non empty functional closed compact Element of K6( the carrier of (TOP-REAL T)) 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 (TOP-REAL 2)
f is Relation-like Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
g is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL 2) -valued Function-like total quasi_total continuous Path of T,f
rng g is functional Element of K6( the carrier of (TOP-REAL 2))
P is non empty TopSpace-like T_0 T_1 T_2 compact pseudocompact SubSpace of TOP-REAL 2
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
{ b₁ where b₁ is V11() real ext-real Element of the carrier of RealSpace : not O <= dist (g,b₁) } 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
{ b₁ where b₁ is V11() real ext-real Element of the carrier of RealSpace : not O <= dist (P,b₁) } 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
g is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
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 (TopSpaceMetr RealSpace) is open Element of K6(K6( the carrier of (TopSpaceMetr RealSpace)))
the carrier of (TopSpaceMetr RealSpace) is set
K6( the carrier of (TopSpaceMetr RealSpace)) is non empty set
K6(K6( the carrier of (TopSpaceMetr RealSpace))) 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))
f is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
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))
f is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
f | [.0,1.] is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
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)
f is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
f | [.0,1.] is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,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
f is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
f | [.0,1.] is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,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
f is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
f | [.0,1.] is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
g is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
Closed-Interval-MSpace (g,P) is non empty strict Reflexive discerning V129() triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (g,P)) 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 (Closed-Interval-MSpace (g,P))
Ball (R,f) is Element of K6( the carrier of (Closed-Interval-MSpace (g,P)))
K6( the carrier of (Closed-Interval-MSpace (g,P))) is non empty set
g is set
{ b₁ where b₁ is Element of the carrier of (Closed-Interval-MSpace (g,P)) : not f <= dist (R,b₁) } is set
OO is Element of the carrier of (Closed-Interval-MSpace (g,P))
dist (R,OO) is V11() real ext-real Element of REAL
PQ1 is Element of the carrier of (Closed-Interval-MSpace (g,P))
g is Element of the carrier of (Closed-Interval-MSpace (g,P))
dist (PQ1,g) is V11() real ext-real Element of REAL
the distance of (Closed-Interval-MSpace (g,P)) is non empty Relation-like K7( the carrier of (Closed-Interval-MSpace (g,P)), the carrier of (Closed-Interval-MSpace (g,P))) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7( the carrier of (Closed-Interval-MSpace (g,P)), the carrier of (Closed-Interval-MSpace (g,P))),REAL))
K7( the carrier of (Closed-Interval-MSpace (g,P)), the carrier of (Closed-Interval-MSpace (g,P))) is non empty set
K7(K7( the carrier of (Closed-Interval-MSpace (g,P)), the carrier of (Closed-Interval-MSpace (g,P))),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of (Closed-Interval-MSpace (g,P)), the carrier of (Closed-Interval-MSpace (g,P))),REAL)) is non empty set
the distance of (Closed-Interval-MSpace (g,P)) . (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 (Closed-Interval-MSpace (g,P))
dist (R,PP) is V11() real ext-real Element of REAL
the distance of (Closed-Interval-MSpace (g,P)) is non empty Relation-like K7( the carrier of (Closed-Interval-MSpace (g,P)), the carrier of (Closed-Interval-MSpace (g,P))) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7( the carrier of (Closed-Interval-MSpace (g,P)), the carrier of (Closed-Interval-MSpace (g,P))),REAL))
K7( the carrier of (Closed-Interval-MSpace (g,P)), the carrier of (Closed-Interval-MSpace (g,P))) is non empty set
K7(K7( the carrier of (Closed-Interval-MSpace (g,P)), the carrier of (Closed-Interval-MSpace (g,P))),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of (Closed-Interval-MSpace (g,P)), the carrier of (Closed-Interval-MSpace (g,P))),REAL)) is non empty set
the distance of (Closed-Interval-MSpace (g,P)) . (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
Closed-Interval-MSpace (T,f) is non empty strict Reflexive discerning V129() triangle Discerning SubSpace of RealSpace
Family_open_set (Closed-Interval-MSpace (T,f)) is Element of K6(K6( the carrier of (Closed-Interval-MSpace (T,f))))
the carrier of (Closed-Interval-MSpace (T,f)) is non empty set
K6( the carrier of (Closed-Interval-MSpace (T,f))) is non empty set
K6(K6( the carrier of (Closed-Interval-MSpace (T,f)))) 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 (Closed-Interval-MSpace (T,f)))
[.T,f.] is V45() V46() V47() V66() closed Element of K6(REAL)
O is Element of the carrier of (Closed-Interval-MSpace (T,f))
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( T <= b₁ & b₁ <= 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 (Closed-Interval-MSpace (T,f)))
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
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= r - (min ((r - T),g)) & not r + (min ((r - T),g)) <= b₁ ) } is set
PQ1 is V11() real ext-real Element of REAL
r + (r - T) is V11() real ext-real Element of REAL
(min ((r - T),g)) + T is V11() real ext-real Element of REAL
Ball (O,(min ((r - T),g))) is Element of K6( the carrier of (Closed-Interval-MSpace (T,f)))
T + f is V11() real ext-real Element of REAL
(T + f) / 2 is V11() real ext-real Element of REAL
f - r is V11() real ext-real Element of REAL
min ((f - r),g) is V11() real ext-real Element of REAL
OO is V11() real ext-real Element of REAL
r - (min ((f - r),g)) is V11() real ext-real Element of REAL
r + (min ((f - r),g)) is V11() real ext-real Element of REAL
].(r - (min ((f - r),g))),(r + (min ((f - r),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
((T + f) / 2) * 2 is V11() real ext-real Element of REAL
2 * r is V11() real ext-real Element of REAL
(T + f) - f is V11() real ext-real Element of REAL
(2 * r) - f is V11() real ext-real Element of REAL
PP is set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= r - (min ((f - r),g)) & not r + (min ((f - r),g)) <= b₁ ) } is set
PQ1 is V11() real ext-real Element of REAL
r - (f - r) is V11() real ext-real Element of REAL
Ball (O,(min ((f - r),g))) is Element of K6( the carrier of (Closed-Interval-MSpace (T,f)))
T + f is V11() real ext-real Element of REAL
(T + f) / 2 is V11() real ext-real Element of REAL
g is V45() V46() V47() open Neighbourhood of r
T is V45() V46() V47() open Element of K6(REAL)
f is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
[.f,g.] is V45() V46() V47() V66() closed Element of K6(REAL)
P is V11() real ext-real set
f - P is V11() real ext-real Element of REAL
f + P is V11() real ext-real Element of REAL
].(f - P),(f + P).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
P / 2 is V11() real ext-real Element of REAL
f - 0 is V11() real ext-real Element of REAL
f - (P / 2) is V11() real ext-real Element of REAL
f + 0 is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= f - P & not f + P <= b₁ ) } is set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( f <= b₁ & b₁ <= g ) } is set
R is V11() real ext-real Element of REAL
P is V11() real ext-real set
g - P is V11() real ext-real Element of REAL
g + P is V11() real ext-real Element of REAL
].(g - P),(g + P).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
P / 2 is V11() real ext-real Element of REAL
g + (P / 2) is V11() real ext-real Element of REAL
g + 0 is V11() real ext-real Element of REAL
g - 0 is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= g - P & not g + P <= b₁ ) } is set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( f <= b₁ & b₁ <= g ) } is set
R is V11() real ext-real Element of REAL
T is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
Closed-Interval-MSpace (T,f) is non empty strict Reflexive discerning V129() triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (T,f)) is non empty set
K6( the carrier of (Closed-Interval-MSpace (T,f))) is non empty set
Family_open_set (Closed-Interval-MSpace (T,f)) is Element of K6(K6( the carrier of (Closed-Interval-MSpace (T,f))))
K6(K6( the carrier of (Closed-Interval-MSpace (T,f)))) is non empty set
g is V45() V46() V47() Element of K6(REAL)
P is Element of K6( the carrier of (Closed-Interval-MSpace (T,f)))
R is Element of the carrier of (Closed-Interval-MSpace (T,f))
r is V11() real ext-real Element of REAL
O is V45() V46() V47() open Neighbourhood of r
g is V11() real ext-real set
r - g is V11() real ext-real Element of REAL
r + g is V11() real ext-real Element of REAL
].(r - g),(r + g).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
g is V11() real ext-real Element of REAL
Ball (R,g) is Element of K6( the carrier of (Closed-Interval-MSpace (T,f)))
OO is set
{ b₁ where b₁ is Element of the carrier of (Closed-Interval-MSpace (T,f)) : not g <= dist (R,b₁) } is set
PP is Element of the carrier of (Closed-Interval-MSpace (T,f))
dist (R,PP) is V11() real ext-real Element of REAL
the distance of (Closed-Interval-MSpace (T,f)) is non empty Relation-like K7( the carrier of (Closed-Interval-MSpace (T,f)), the carrier of (Closed-Interval-MSpace (T,f))) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7( the carrier of (Closed-Interval-MSpace (T,f)), the carrier of (Closed-Interval-MSpace (T,f))),REAL))
K7( the carrier of (Closed-Interval-MSpace (T,f)), the carrier of (Closed-Interval-MSpace (T,f))) is non empty set
K7(K7( the carrier of (Closed-Interval-MSpace (T,f)), the carrier of (Closed-Interval-MSpace (T,f))),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of (Closed-Interval-MSpace (T,f)), the carrier of (Closed-Interval-MSpace (T,f))),REAL)) is non empty set
the distance of (Closed-Interval-MSpace (T,f)) . (R,PP) is V11() real ext-real Element of REAL
real_dist . (R,PP) is set
g1 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
real_dist . (g1,g) is V11() real ext-real Element of REAL
PQ1 is V11() real ext-real Element of REAL
PQ1 - r is V11() real ext-real Element of REAL
abs (PQ1 - r) is V11() real ext-real Element of REAL
OO is set
PP is V11() real ext-real Element of REAL
PP - r is V11() real ext-real Element of REAL
abs (PP - r) is V11() real ext-real Element of REAL
real_dist . (PP,r) is V11() real ext-real Element of REAL
g is Element of the carrier of (Closed-Interval-MSpace (T,f))
PQ1 is Element of the carrier of (Closed-Interval-MSpace (T,f))
dist (g,PQ1) is V11() real ext-real Element of REAL
the distance of (Closed-Interval-MSpace (T,f)) is non empty Relation-like K7( the carrier of (Closed-Interval-MSpace (T,f)), the carrier of (Closed-Interval-MSpace (T,f))) -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7(K7( the carrier of (Closed-Interval-MSpace (T,f)), the carrier of (Closed-Interval-MSpace (T,f))),REAL))
K7( the carrier of (Closed-Interval-MSpace (T,f)), the carrier of (Closed-Interval-MSpace (T,f))) is non empty set
K7(K7( the carrier of (Closed-Interval-MSpace (T,f)), the carrier of (Closed-Interval-MSpace (T,f))),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of (Closed-Interval-MSpace (T,f)), the carrier of (Closed-Interval-MSpace (T,f))),REAL)) is non empty set
the distance of (Closed-Interval-MSpace (T,f)) . (g,PQ1) is V11() real ext-real Element of REAL
real_dist . (g,PQ1) is set
T is V11() real ext-real set
f is V11() real ext-real set
g is V11() real ext-real set
Closed-Interval-TSpace (T,f) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (T,f)) is non empty V45() V46() V47() set
[.T,f.] is V45() V46() V47() V66() closed Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( T <= b₁ & b₁ <= f ) } is set
P is V11() real ext-real Element of REAL
T is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
Closed-Interval-TSpace (T,f) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (T,f)) is non empty V45() V46() V47() set
g is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
Closed-Interval-TSpace (g,P) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (g,P)) is non empty V45() V46() V47() set
K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))) is non empty V33() V34() V35() set
K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P)))) is non empty set
R is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,f)) -defined the carrier of (Closed-Interval-TSpace (g,P)) -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))))
R . T is V11() real ext-real set
R . f is V11() real ext-real set
r is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
O is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
g is V11() real ext-real Element of REAL
dom R is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
K6( the carrier of (Closed-Interval-TSpace (T,f))) is non empty set
O . g is V11() real ext-real set
R . r is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
(O . g) - g is V11() real ext-real Element of REAL
P - (O . g) is V11() real ext-real Element of REAL
min (((O . g) - g),(P - (O . g))) is V11() real ext-real Element of REAL
PP is V45() V46() V47() open Neighbourhood of O . g
Closed-Interval-MSpace (g,P) is non empty strict Reflexive discerning V129() triangle Discerning SubSpace of RealSpace
TopSpaceMetr (Closed-Interval-MSpace (g,P)) is TopStruct
the topology of (Closed-Interval-TSpace (g,P)) is non empty open Element of K6(K6( the carrier of (Closed-Interval-TSpace (g,P))))
K6( the carrier of (Closed-Interval-TSpace (g,P))) is non empty set
K6(K6( the carrier of (Closed-Interval-TSpace (g,P)))) is non empty set
Family_open_set (Closed-Interval-MSpace (g,P)) is Element of K6(K6( the carrier of (Closed-Interval-MSpace (g,P))))
the carrier of (Closed-Interval-MSpace (g,P)) is non empty set
K6( the carrier of (Closed-Interval-MSpace (g,P))) is non empty set
K6(K6( the carrier of (Closed-Interval-MSpace (g,P)))) is non empty set
P - P is V11() real ext-real Element of REAL
(O . g) - (min (((O . g) - g),(P - (O . g)))) is V11() real ext-real Element of REAL
(O . g) + (min (((O . g) - g),(P - (O . g)))) is V11() real ext-real Element of REAL
].((O . g) - (min (((O . g) - g),(P - (O . g))))),((O . g) + (min (((O . g) - g),(P - (O . g))))).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
PQ1 is V45() V46() V47() open Neighbourhood of O . g
g is V45() V46() V47() open Neighbourhood of O . g
].g,P.[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
g1 is set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= (O . g) - (min (((O . g) - g),(P - (O . g)))) & not (O . g) + (min (((O . g) - g),(P - (O . g)))) <= b₁ ) } is set
GPQ is V11() real ext-real Element of REAL
(O . g) + (P - (O . g)) is V11() real ext-real Element of REAL
g + (min (((O . g) - g),(P - (O . g)))) is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= g & not P <= b₁ ) } is set
[.g,P.] is V45() V46() V47() V66() closed Element of K6(REAL)
the carrier of (TopSpaceMetr (Closed-Interval-MSpace (g,P))) is set
g1 is Element of K6( the carrier of (Closed-Interval-MSpace (g,P)))
GPQ is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
Ex is V45() V46() V47() a_neighborhood of g
f1 is V45() V46() V47() a_neighborhood of r
R .: f1 is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
t is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
Closed-Interval-MSpace (T,f) is non empty strict Reflexive discerning V129() triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (T,f)) is non empty set
TopSpaceMetr (Closed-Interval-MSpace (T,f)) is TopStruct
the carrier of (TopSpaceMetr (Closed-Interval-MSpace (T,f))) is set
K6( the carrier of (Closed-Interval-MSpace (T,f))) is non empty set
[.T,f.] is V45() V46() V47() V66() closed Element of K6(REAL)
hh is V45() V46() V47() Element of K6(REAL)
the topology of (Closed-Interval-TSpace (T,f)) is non empty open Element of K6(K6( the carrier of (Closed-Interval-TSpace (T,f))))
K6(K6( the carrier of (Closed-Interval-TSpace (T,f)))) is non empty set
Family_open_set (Closed-Interval-MSpace (T,f)) is Element of K6(K6( the carrier of (Closed-Interval-MSpace (T,f))))
K6(K6( the carrier of (Closed-Interval-MSpace (T,f)))) is non empty set
FFx is Element of K6( the carrier of (Closed-Interval-MSpace (T,f)))
ll is V45() V46() V47() open Neighbourhood of g
O .: ll is V45() V46() V47() Element of K6(REAL)
O .: f1 is V45() V46() V47() Element of K6(REAL)
T is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
Closed-Interval-TSpace (T,f) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (T,f)) is non empty V45() V46() V47() set
g is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
Closed-Interval-TSpace (g,P) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (g,P)) is non empty V45() V46() V47() set
K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))) is non empty V33() V34() V35() set
K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P)))) is non empty set
R is V11() real ext-real Element of REAL
[.T,f.] is V45() V46() V47() V66() closed Element of K6(REAL)
r is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,f)) -defined the carrier of (Closed-Interval-TSpace (g,P)) -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))))
r . T is V11() real ext-real set
r . f is V11() real ext-real set
O is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
g is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
g | [.T,f.] is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
dom g 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
(dom g) /\ [.T,f.] is V45() V46() V47() Element of K6(REAL)
g . R is V11() real ext-real set
OO is V45() V46() V47() open Neighbourhood of g . R
[.g,P.] is V45() V46() V47() V66() closed Element of K6(REAL)
OO /\ [.g,P.] is V45() V46() V47() Element of K6(REAL)
PP is V45() V46() V47() Element of K6( the carrier of RealSpace)
the topology of (TopSpaceMetr RealSpace) is open Element of K6(K6( the carrier of (TopSpaceMetr RealSpace)))
the carrier of (TopSpaceMetr RealSpace) is set
K6( the carrier of (TopSpaceMetr RealSpace)) is non empty set
K6(K6( the carrier of (TopSpaceMetr RealSpace))) is non empty set
OO /\ the carrier of (Closed-Interval-TSpace (g,P)) is V45() V46() V47() Element of K6(REAL)
K6( the carrier of (Closed-Interval-TSpace (g,P))) is non empty set
[#] (Closed-Interval-TSpace (g,P)) is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
OO /\ ([#] (Closed-Interval-TSpace (g,P))) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
g is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
the topology of (Closed-Interval-TSpace (g,P)) is non empty open Element of K6(K6( the carrier of (Closed-Interval-TSpace (g,P))))
K6(K6( the carrier of (Closed-Interval-TSpace (g,P)))) is non empty set
g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
g1 is V45() V46() V47() a_neighborhood of g
GPQ is V45() V46() V47() a_neighborhood of O
r .: GPQ is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
K6( the carrier of (Closed-Interval-TSpace (T,f))) is non empty set
Ex is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
the topology of (Closed-Interval-TSpace (T,f)) is non empty open Element of K6(K6( the carrier of (Closed-Interval-TSpace (T,f))))
K6(K6( the carrier of (Closed-Interval-TSpace (T,f)))) is non empty set
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
[#] (Closed-Interval-TSpace (T,f)) is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
f1 is V45() V46() V47() Element of K6( the carrier of R^1)
f1 /\ ([#] (Closed-Interval-TSpace (T,f))) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
t is V45() V46() V47() Element of K6( the carrier of RealSpace)
FFx is V45() V46() V47() Element of K6(REAL)
hh is V45() V46() V47() open Neighbourhood of R
g .: hh is V45() V46() V47() Element of K6(REAL)
ll is set
a9 is V11() real ext-real Element of REAL
cc is V11() real ext-real Element of REAL
g . cc is V11() real ext-real set
g . R is V11() real ext-real set
OO is V45() V46() V47() open Neighbourhood of g . R
[#] (Closed-Interval-TSpace (g,P)) is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
K6( the carrier of (Closed-Interval-TSpace (g,P))) is non empty set
OO /\ ([#] (Closed-Interval-TSpace (g,P))) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
PP is V45() V46() V47() Element of K6( the carrier of RealSpace)
the topology of (TopSpaceMetr RealSpace) is open Element of K6(K6( the carrier of (TopSpaceMetr RealSpace)))
the carrier of (TopSpaceMetr RealSpace) is set
K6( the carrier of (TopSpaceMetr RealSpace)) is non empty set
K6(K6( the carrier of (TopSpaceMetr RealSpace))) is non empty set
g is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
the topology of (Closed-Interval-TSpace (g,P)) is non empty open Element of K6(K6( the carrier of (Closed-Interval-TSpace (g,P))))
K6(K6( the carrier of (Closed-Interval-TSpace (g,P)))) is non empty set
g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
g1 is V45() V46() V47() a_neighborhood of g
GPQ is V45() V46() V47() a_neighborhood of O
r .: GPQ is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
K6( the carrier of (Closed-Interval-TSpace (T,f))) is non empty set
Ex is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
the topology of (Closed-Interval-TSpace (T,f)) is non empty open Element of K6(K6( the carrier of (Closed-Interval-TSpace (T,f))))
K6(K6( the carrier of (Closed-Interval-TSpace (T,f)))) is non empty set
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
[#] (Closed-Interval-TSpace (T,f)) is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
f1 is V45() V46() V47() Element of K6( the carrier of R^1)
f1 /\ ([#] (Closed-Interval-TSpace (T,f))) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
t is V45() V46() V47() Element of K6( the carrier of RealSpace)
FFx is V45() V46() V47() Element of K6(REAL)
hh is V45() V46() V47() open Neighbourhood of R
g .: hh is V45() V46() V47() Element of K6(REAL)
ll is set
a9 is V11() real ext-real Element of REAL
cc is V11() real ext-real Element of REAL
g . cc is V11() real ext-real set
T is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
Closed-Interval-TSpace (T,f) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (T,f)) is non empty V45() V46() V47() set
g is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
Closed-Interval-TSpace (g,P) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (g,P)) is non empty V45() V46() V47() set
K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))) is non empty V33() V34() V35() set
K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P)))) is non empty set
[.T,f.] is V45() V46() V47() V66() closed Element of K6(REAL)
R is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,f)) -defined the carrier of (Closed-Interval-TSpace (g,P)) -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))))
R . T is V11() real ext-real set
R . f is V11() real ext-real set
r is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
r | [.T,f.] is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (r | [.T,f.]) is V45() V46() V47() Element of K6(REAL)
O is V11() real ext-real set
g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
T is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
Closed-Interval-TSpace (T,f) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (T,f)) is non empty V45() V46() V47() set
g is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
Closed-Interval-TSpace (g,P) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (g,P)) is non empty V45() V46() V47() set
K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))) is non empty V33() V34() V35() set
K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P)))) is non empty set
R is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,f)) -defined the carrier of (Closed-Interval-TSpace (g,P)) -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))))
R . T is V11() real ext-real set
R . f is V11() real ext-real set
[.T,f.] is V45() V46() V47() V66() closed Element of K6(REAL)
dom R is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
K6( the carrier of (Closed-Interval-TSpace (T,f))) is non empty set
rng R is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
K6( the carrier of (Closed-Interval-TSpace (g,P))) is non empty set
K7([.T,f.],REAL) is V33() V34() V35() set
K6(K7([.T,f.],REAL)) is non empty set
r is Relation-like [.T,f.] -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7([.T,f.],REAL))
O is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
O | [.T,f.] is Relation-like REAL -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(REAL,REAL))
[.T,f.] /\ (dom R) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
[.T,f.] /\ the carrier of (Closed-Interval-TSpace (T,f)) is V45() V46() V47() Element of K6(REAL)
g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
R . g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
R . g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
OO is V11() real ext-real Element of REAL
PP is V11() real ext-real Element of REAL
PQ1 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
dom O is V45() V46() V47() Element of K6(REAL)
[.T,f.] /\ (dom O) is V45() V46() V47() Element of K6(REAL)
g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
OO is V11() real ext-real Element of REAL
g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
PP is V11() real ext-real Element of REAL
PQ1 is V11() real ext-real Element of REAL
R . g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
g is V11() real ext-real Element of REAL
R . g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
dom O is V45() V46() V47() Element of K6(REAL)
[.T,f.] /\ (dom O) is V45() V46() V47() Element of K6(REAL)
g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
OO is V11() real ext-real Element of REAL
g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
PP is V11() real ext-real Element of REAL
PQ1 is V11() real ext-real Element of REAL
R . g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
g is V11() real ext-real Element of REAL
R . g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
K7( the carrier of I[01], the carrier of I[01]) is non empty V33() V34() V35() set
K6(K7( the carrier of I[01], the carrier of I[01])) is non empty set
T is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like one-to-one total quasi_total V33() V34() V35() continuous Element of K6(K7( the carrier of I[01], the carrier of I[01]))
T . 0 is V11() real ext-real set
T . 1 is V11() real ext-real set
f is V11() real ext-real Element of the carrier of I[01]
P is V11() real ext-real Element of REAL
g is V11() real ext-real Element of the carrier of I[01]
R is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
T . f is V11() real ext-real Element of the carrier of I[01]
O is V11() real ext-real Element of REAL
T . g is V11() real ext-real Element of the carrier of I[01]
T is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
Closed-Interval-TSpace (T,f) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (T,f)) is non empty V45() V46() V47() set
g is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
Closed-Interval-TSpace (g,P) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (g,P)) is non empty V45() V46() V47() set
K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))) is non empty V33() V34() V35() set
K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P)))) is non empty set
K6( the carrier of (Closed-Interval-TSpace (T,f))) is non empty set
R is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,f)) -defined the carrier of (Closed-Interval-TSpace (g,P)) -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))))
R . T is V11() real ext-real set
R . f is V11() real ext-real set
r is non empty V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
R .: r is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
K6( the carrier of (Closed-Interval-TSpace (g,P))) is non empty set
O is V45() V46() V47() Element of K6( the carrier of R^1)
g is V45() V46() V47() Element of K6( the carrier of R^1)
[#] O is V45() V46() V47() Element of K6(REAL)
lower_bound ([#] O) is V11() real ext-real Element of REAL
R . (lower_bound ([#] O)) is V11() real ext-real set
[#] g is V45() V46() V47() Element of K6(REAL)
lower_bound ([#] g) is V11() real ext-real Element of REAL
[#] (Closed-Interval-TSpace (g,P)) is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
[#] R^1 is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of R^1)
[#] (Closed-Interval-TSpace (T,f)) is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
OO is V11() real ext-real Element of REAL
PP is V11() real ext-real set
R .: ([#] O) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
dom R is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
PQ1 is set
R . PQ1 is V11() real ext-real set
g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
g1 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
Ex is V11() real ext-real Element of REAL
GPQ is V11() real ext-real Element of REAL
R . g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
R . g1 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
t is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
PP is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
dom R is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
PP is V11() real ext-real set
OO + PP is V11() real ext-real Element of REAL
OO + 0 is V11() real ext-real Element of REAL
T is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
Closed-Interval-TSpace (T,f) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (T,f)) is non empty V45() V46() V47() set
g is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
Closed-Interval-TSpace (g,P) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (g,P)) is non empty V45() V46() V47() set
K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))) is non empty V33() V34() V35() set
K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P)))) is non empty set
K6( the carrier of (Closed-Interval-TSpace (T,f))) is non empty set
R is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,f)) -defined the carrier of (Closed-Interval-TSpace (g,P)) -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))))
R . T is V11() real ext-real set
R . f is V11() real ext-real set
r is non empty V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
O is non empty V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
R .: r is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
K6( the carrier of (Closed-Interval-TSpace (g,P))) is non empty set
g is V45() V46() V47() Element of K6( the carrier of R^1)
g is V45() V46() V47() Element of K6( the carrier of R^1)
[#] g is V45() V46() V47() Element of K6(REAL)
upper_bound ([#] g) is V11() real ext-real Element of REAL
R . (upper_bound ([#] g)) is V11() real ext-real set
[#] g is V45() V46() V47() Element of K6(REAL)
upper_bound ([#] g) is V11() real ext-real Element of REAL
[#] (Closed-Interval-TSpace (g,P)) is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
[#] R^1 is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of R^1)
[#] (Closed-Interval-TSpace (T,f)) is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
PP is V11() real ext-real Element of REAL
PQ1 is V11() real ext-real set
R .: ([#] g) is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
dom R is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
g is set
R . g is V11() real ext-real set
g1 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
GPQ is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
Ex is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
R . g1 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
R . GPQ is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
t is V11() real ext-real Element of REAL
FFx is V11() real ext-real Element of REAL
PQ1 is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
dom R is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
PQ1 is V11() real ext-real set
PP - PQ1 is V11() real ext-real Element of REAL
PP - 0 is V11() real ext-real Element of REAL
T is V11() real ext-real set
f is V11() real ext-real set
[.T,f.] is V45() V46() V47() V66() closed Element of K6(REAL)
lower_bound [.T,f.] is V11() real ext-real Element of REAL
upper_bound [.T,f.] is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( T <= b₁ & b₁ <= f ) } is set
P is V11() real ext-real set
T + P is V11() real ext-real set
P is V11() real ext-real set
f - P is V11() real ext-real set
P is V11() real ext-real set
R is V11() real ext-real Element of REAL
P is ext-real set
R is V11() real ext-real Element of REAL
P is ext-real set
R is V11() real ext-real Element of REAL
P is V11() real ext-real set
R is V11() real ext-real Element of REAL
T is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
Closed-Interval-TSpace (T,f) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (T,f)) is non empty V45() V46() V47() set
g is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
Closed-Interval-TSpace (g,P) is non empty strict TopSpace-like V212() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (g,P)) is non empty V45() V46() V47() set
K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))) is non empty V33() V34() V35() set
K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P)))) is non empty set
r is V11() real ext-real Element of REAL
R is V11() real ext-real Element of REAL
O is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
[.R,r.] is V45() V46() V47() V66() closed Element of K6(REAL)
[.O,g.] is V45() V46() V47() V66() closed Element of K6(REAL)
g is non empty Relation-like the carrier of (Closed-Interval-TSpace (T,f)) -defined the carrier of (Closed-Interval-TSpace (g,P)) -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7( the carrier of (Closed-Interval-TSpace (T,f)), the carrier of (Closed-Interval-TSpace (g,P))))
g . T is V11() real ext-real set
g . f is V11() real ext-real set
g . R is V11() real ext-real set
g . r is V11() real ext-real set
g .: [.R,r.] is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
K6( the carrier of (Closed-Interval-TSpace (g,P))) is non empty set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( T <= b₁ & b₁ <= f ) } is set
[.T,f.] is V45() V46() V47() V66() closed Element of K6(REAL)
[.g,P.] is V45() V46() V47() V66() closed Element of K6(REAL)
OO is set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( O <= b₁ & b₁ <= g ) } is set
PP is V11() real ext-real Element of REAL
rng g is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
[#] (Closed-Interval-TSpace (g,P)) is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
g " is non empty Relation-like the carrier of (Closed-Interval-TSpace (g,P)) -defined the carrier of (Closed-Interval-TSpace (T,f)) -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7( the carrier of (Closed-Interval-TSpace (g,P)), the carrier of (Closed-Interval-TSpace (T,f))))
K7( the carrier of (Closed-Interval-TSpace (g,P)), the carrier of (Closed-Interval-TSpace (T,f))) is non empty V33() V34() V35() set
K6(K7( the carrier of (Closed-Interval-TSpace (g,P)), the carrier of (Closed-Interval-TSpace (T,f)))) is non empty set
dom (g ") is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
(g ") . PP is V11() real ext-real set
rng (g ") is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
K6( the carrier of (Closed-Interval-TSpace (T,f))) is non empty set
[#] (Closed-Interval-TSpace (T,f)) is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
PQ1 is V11() real ext-real Element of REAL
g " is Relation-like Function-like set
(g ") . PP is set
dom g is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
g . g is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
g1 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
g . g1 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
GPQ is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
g . GPQ is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
t is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
Ex is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
f1 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
ll is V11() real ext-real Element of REAL
hh is V11() real ext-real Element of REAL
FFx is V11() real ext-real Element of REAL
ll is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( R <= b₁ & b₁ <= r ) } is set
g . PQ1 is V11() real ext-real set
OO is set
dom g is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (T,f)))
K6( the carrier of (Closed-Interval-TSpace (T,f))) is non empty set
PP is set
g . PP is V11() real ext-real set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( R <= b₁ & b₁ <= r ) } is set
PQ1 is V11() real ext-real Element of REAL
g . PQ1 is V11() real ext-real set
rng g is V45() V46() V47() Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
[#] (Closed-Interval-TSpace (g,P)) is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of (Closed-Interval-TSpace (g,P)))
g1 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
g . g1 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
GPQ is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
g . GPQ is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
Ex is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,f))
g . Ex is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (g,P))
g is V11() real ext-real Element of REAL
t is V11() real ext-real Element of REAL
FFx is V11() real ext-real Element of REAL
FFx is V11() real ext-real Element of REAL
f1 is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( O <= b₁ & b₁ <= g ) } is set
T is functional Element of K6( the carrier of (TOP-REAL 2))
f is functional Element of K6( the carrier of (TOP-REAL 2))
T /\ f is functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | T is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | T) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | T)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | T))) is non empty set
g is Relation-like Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
P is Relation-like Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
R is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | R is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | R) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | R)) is non empty set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | R))) is non empty set
r is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | R) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | R)))
r . 0 is set
r . 1 is set
[#] ((TOP-REAL 2) | R) is non empty non proper open closed dense non boundary Element of K6( the carrier of ((TOP-REAL 2) | R))
K6( the carrier of ((TOP-REAL 2) | R)) is non empty set
R /\ f is functional Element of K6( the carrier of (TOP-REAL 2))
O is non empty Element of K6( the carrier of ((TOP-REAL 2) | R))
OO is set
PP is functional Element of K6( the carrier of (TOP-REAL 2))
{} ((TOP-REAL 2) | R) is empty proper Function-like functional V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() open closed boundary nowhere_dense compact Element of K6( the carrier of ((TOP-REAL 2) | R))
g is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | g is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | g) is non empty set
K6( the carrier of ((TOP-REAL 2) | g)) is non empty set
g is non empty functional Element of K6( the carrier of (TOP-REAL 2))
g /\ g is functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (g /\ g) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
PQ1 is non empty Element of K6( the carrier of ((TOP-REAL 2) | g))
((TOP-REAL 2) | g) | PQ1 is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of (TOP-REAL 2) | g
r " is non empty Relation-like the carrier of ((TOP-REAL 2) | R) -defined the carrier of I[01] -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7( the carrier of ((TOP-REAL 2) | R), the carrier of I[01]))
K7( the carrier of ((TOP-REAL 2) | R), the carrier of I[01]) is non empty V33() V34() V35() set
K6(K7( the carrier of ((TOP-REAL 2) | R), the carrier of I[01])) is non empty set
rng r is Element of K6( the carrier of ((TOP-REAL 2) | R))
[#] I[01] is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is non empty set
[#] R^1 is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of R^1)
(r ") .: O is V45() V46() V47() Element of K6( the carrier of I[01])
GPQ is V45() V46() V47() Element of K6( the carrier of R^1)
Ex is V45() V46() V47() Element of K6( the carrier of I[01])
[#] GPQ is V45() V46() V47() Element of K6(REAL)
lower_bound ([#] GPQ) is V11() real ext-real Element of REAL
r . (lower_bound ([#] GPQ)) is set
dom (r ") is Element of K6( the carrier of ((TOP-REAL 2) | R))
(r ") . OO is V11() real ext-real set
dom r is V45() V46() V47() Element of K6( the carrier of I[01])
t is V11() real ext-real Element of REAL
r . t is set
f1 is Relation-like Function-like set
f1 " is Relation-like Function-like set
(r ") . (r . t) is V11() real ext-real set
rng (r ") is V45() V46() V47() Element of K6( the carrier of I[01])
(r ") " is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | R) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | R)))
g1 is Relation-like Function-like set
g1 " is Relation-like Function-like set
t is set
(r ") . t is V11() real ext-real set
T is functional Element of K6( the carrier of (TOP-REAL 2))
f is functional Element of K6( the carrier of (TOP-REAL 2))
T /\ f is functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | T is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | T) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | T)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | T))) is non empty set
g is Relation-like Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
P is Relation-like Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
R is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | R is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | R) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | R)) is non empty set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | R))) is non empty set
r is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | R) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | R)))
r . 0 is set
r . 1 is set
[#] ((TOP-REAL 2) | R) is non empty non proper open closed dense non boundary Element of K6( the carrier of ((TOP-REAL 2) | R))
K6( the carrier of ((TOP-REAL 2) | R)) is non empty set
R /\ f is functional Element of K6( the carrier of (TOP-REAL 2))
O is non empty Element of K6( the carrier of ((TOP-REAL 2) | R))
OO is set
PP is functional Element of K6( the carrier of (TOP-REAL 2))
{} ((TOP-REAL 2) | R) is empty proper Function-like functional V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() open closed boundary nowhere_dense compact Element of K6( the carrier of ((TOP-REAL 2) | R))
g is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | g is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | g) is non empty set
K6( the carrier of ((TOP-REAL 2) | g)) is non empty set
g is non empty functional Element of K6( the carrier of (TOP-REAL 2))
g /\ g is functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (g /\ g) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
PQ1 is non empty Element of K6( the carrier of ((TOP-REAL 2) | g))
((TOP-REAL 2) | g) | PQ1 is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of (TOP-REAL 2) | g
r " is non empty Relation-like the carrier of ((TOP-REAL 2) | R) -defined the carrier of I[01] -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7( the carrier of ((TOP-REAL 2) | R), the carrier of I[01]))
K7( the carrier of ((TOP-REAL 2) | R), the carrier of I[01]) is non empty V33() V34() V35() set
K6(K7( the carrier of ((TOP-REAL 2) | R), the carrier of I[01])) is non empty set
rng r is Element of K6( the carrier of ((TOP-REAL 2) | R))
rng (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])
(r ") " is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | R) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | R)))
g1 is Relation-like Function-like set
g1 " is Relation-like Function-like set
[#] R^1 is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of R^1)
(r ") .: O is V45() V46() V47() Element of K6( the carrier of I[01])
GPQ is V45() V46() V47() Element of K6( the carrier of R^1)
Ex is V45() V46() V47() Element of K6( the carrier of I[01])
[#] GPQ is V45() V46() V47() Element of K6(REAL)
upper_bound ([#] GPQ) is V11() real ext-real Element of REAL
r . (upper_bound ([#] GPQ)) is set
dom (r ") is Element of K6( the carrier of ((TOP-REAL 2) | R))
(r ") . OO is V11() real ext-real set
dom r is V45() V46() V47() Element of K6( the carrier of I[01])
t is V11() real ext-real Element of REAL
r . t is set
f1 is Relation-like Function-like set
f1 " is Relation-like Function-like set
(r ") . (r . t) is V11() real ext-real set
t is set
(r ") . t is V11() real ext-real set
{0} is non empty V45() V46() V47() V48() V49() V50() finite V56() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
T is V45() V46() V47() finite bounded_below bounded_above real-bounded Element of K6(REAL)
TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) is non empty strict TopStruct
T is V45() V46() V47() Element of K6(REAL)
f is V45() V46() V47() Element of K6( the carrier of R^1)
T ` is V45() V46() V47() Element of K6(REAL)
REAL \ T is V45() V46() V47() set
(T `) ` is V45() V46() V47() Element of K6(REAL)
REAL \ (T `) is V45() V46() V47() set
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
[#] R^1 is non empty non proper V45() V46() V47() open closed dense non boundary Element of K6( the carrier of R^1)
([#] R^1) \ f is V45() V46() V47() Element of K6( the carrier of R^1)
f ` is V45() V46() V47() Element of K6( the carrier of R^1)
the carrier of R^1 \ f is V45() V46() V47() set
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
T ` is V45() V46() V47() Element of K6(REAL)
REAL \ T is V45() V46() V47() set
(T `) ` is V45() V46() V47() Element of K6(REAL)
REAL \ (T `) is V45() V46() V47() set
T is V45() V46() V47() Element of K6(REAL)
Cl T is V45() V46() V47() Element of K6(REAL)
f is V45() V46() V47() Element of K6( the carrier of R^1)
Cl f is V45() V46() V47() closed Element of K6( the carrier of R^1)
g is set
P is V45() V46() V47() Element of K6( the carrier of R^1)
R is V45() V46() V47() Element of K6(REAL)
T /\ R is V45() V46() V47() Element of K6(REAL)
g is set
P is V45() V46() V47() open Element of K6(REAL)
P /\ T is V45() V46() V47() Element of K6(REAL)
R is V45() V46() V47() Element of K6( the carrier of R^1)
T is V11() real ext-real set
f is V11() real ext-real set
[.T,f.] is V45() V46() V47() V66() closed Element of K6(REAL)
g is V45() V46() V47() Element of K6(REAL)
T is V45() V46() V47() Element of K6(REAL)
f is V45() V46() V47() Element of K6( the carrier of R^1)
g is empty proper Function-like functional V45() V46() V47() V48() V49() V50() V51() finite V56() bounded_below bounded_above real-bounded V66() open closed boundary nowhere_dense compact Element of K6( the carrier of R^1)
g is non empty V45() V46() V47() bounded_below bounded_above real-bounded Element of K6(REAL)
inf g is V11() real ext-real set
sup g is V11() real ext-real set
P is V11() real ext-real set
R is V11() real ext-real set
[.P,R.] is V45() V46() V47() V66() compact closed Element of K6(REAL)
Closed-Interval-TSpace (P,R) is non empty strict TopSpace-like V212() SubSpace of R^1
r is V45() V46() V47() Element of K6( the carrier of R^1)
R^1 | r is strict TopSpace-like V212() SubSpace of R^1
[#] f is V45() V46() V47() Element of K6(REAL)
T is V45() V46() V47() Element of K6(REAL)
T is V11() real ext-real set
f is V11() real ext-real set
].T,f.[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
Cl ].T,f.[ is V45() V46() V47() Element of K6(REAL)
[.T,f.] is V45() V46() V47() V66() compact closed Element of K6(REAL)
P is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
g + P is V11() real ext-real Element of REAL
(g + P) / 2 is V11() real ext-real Element of REAL
R is set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= T & not f <= b₁ ) } is set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( T <= b₁ & b₁ <= f ) } is set
r is V11() real ext-real Element of REAL
].g,P.[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
O is V45() V46() V47() open Element of K6(REAL)
O /\ ].T,f.[ is V45() V46() V47() Element of K6(REAL)
g is V11() real ext-real set
T - g is V11() real ext-real set
T + g is V11() real ext-real set
].(T - g),(T + g).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
T - 0 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
T - g is V11() real ext-real Element of REAL
T + g is V11() real ext-real Element of REAL
].(T - g),(T + g).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= T - g & not T + g <= b₁ ) } is set
T + 0 is V11() real ext-real Element of REAL
g + g is V11() real ext-real Element of REAL
g + (g + g) is V11() real ext-real Element of REAL
(g + (g + g)) / 2 is V11() real ext-real Element of REAL
T + (T + g) is V11() real ext-real Element of REAL
(T + (T + g)) / 2 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)
T + f is V11() real ext-real set
(T + f) / 2 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 Element of K6(REAL)
O /\ ].T,f.[ is V45() V46() V47() Element of K6(REAL)
g is V11() real ext-real set
f - g is V11() real ext-real set
f + g is V11() real ext-real set
].(f - g),(f + g).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
f - 0 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
f - g is V11() real ext-real Element of REAL
f + g is V11() real ext-real Element of REAL
f + 0 is V11() real ext-real Element of REAL
].(f - g),(f + g).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= f - g & not f + g <= b₁ ) } is set
P - g is V11() real ext-real Element of REAL
P + (P - g) is V11() real ext-real Element of REAL
(P + (P - g)) / 2 is V11() real ext-real Element of REAL
f + (f - g) is V11() real ext-real Element of REAL
(f + (f - g)) / 2 is V11() real ext-real Element of REAL
P + g is V11() real ext-real Element of REAL
].(P - g),(P + g).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
T + f is V11() real ext-real set
(T + f) / 2 is V11() real ext-real Element of REAL
P - g is V11() real ext-real Element of REAL
P + g is V11() real ext-real Element of REAL
].(P - g),(P + g).[ is V45() V46() V47() non left_end non right_end V66() open Element of K6(REAL)
{T} is non empty V45() V46() V47() finite left_end right_end bounded_below bounded_above real-bounded compact closed Element of K6(REAL)
T is TopStruct
the carrier of T is set
K7( the carrier of T,REAL) is V33() V34() V35() set
K6(K7( the carrier of T,REAL)) is non empty set
K7( the carrier of T, the carrier of R^1) is V33() V34() V35() set
K6(K7( the carrier of T, the carrier of R^1)) is non empty set
f is Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7( the carrier of T,REAL))
g is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total V33() V34() V35() Element of K6(K7( the carrier of T, the carrier of R^1))
P is V45() V46() V47() Element of K6( the carrier of R^1)
g " P is Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
R is V45() V46() V47() Element of K6(REAL)
P is V45() V46() V47() Element of K6(REAL)
f " P is Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
R is V45() V46() V47() Element of K6( the carrier of R^1)