:: 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

(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

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

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

(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

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

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

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

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

PQ1 is V11() real ext-real