:: JORDAN20 semantic presentation

REAL is non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() set

NAT is V143() V144() V145() V146() V147() V148() V149() bounded_below Element of K6(REAL)

K6(REAL) is set

I[01] is non empty strict TopSpace-like V200() SubSpace of R^1

R^1 is non empty strict TopSpace-like V200() TopStruct

the carrier of I[01] is non empty V143() V144() V145() set

COMPLEX is non empty V36() V143() V149() set

omega is V143() V144() V145() V146() V147() V148() V149() bounded_below set

K6(omega) is set

K6(NAT) is set

1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT

K7(1,1) is V22() set

K6(K7(1,1)) is set

K7(K7(1,1),1) is V22() set

K6(K7(K7(1,1),1)) is set

K7(K7(1,1),REAL) is V22() set

K6(K7(K7(1,1),REAL)) is set

K7(REAL,REAL) is V22() set

K7(K7(REAL,REAL),REAL) is V22() set

K6(K7(K7(REAL,REAL),REAL)) is set

2 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT

K7(2,2) is V22() set

K7(K7(2,2),REAL) is V22() set

K6(K7(K7(2,2),REAL)) is set

RAT is non empty V36() V143() V144() V145() V146() V149() set

INT is non empty V36() V143() V144() V145() V146() V147() V149() set

K6(K7(REAL,REAL)) is set

TOP-REAL 2 is non empty TopSpace-like V109() V155() V156() V157() V158() V159() V160() V161() strict RLTopStruct

the carrier of (TOP-REAL 2) is non empty set

K6( the carrier of (TOP-REAL 2)) is set

K7( the carrier of (TOP-REAL 2),REAL) is V22() set

K6(K7( the carrier of (TOP-REAL 2),REAL)) is set

{} is empty V22() non-empty empty-yielding V143() V144() V145() V146() V147() V148() V149() bounded_below V209() set

{{},1} is non empty set

K457() is non empty strict TopSpace-like V200() TopStruct

the carrier of K457() is non empty V143() V144() V145() set

RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V200() MetrStruct

K7(COMPLEX,COMPLEX) is V22() set

K6(K7(COMPLEX,COMPLEX)) is set

K7(K7(COMPLEX,COMPLEX),COMPLEX) is V22() set

K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set

K7(RAT,RAT) is V22() set

K6(K7(RAT,RAT)) is set

K7(K7(RAT,RAT),RAT) is V22() set

K6(K7(K7(RAT,RAT),RAT)) is set

K7(INT,INT) is V22() set

K6(K7(INT,INT)) is set

K7(K7(INT,INT),INT) is V22() set

K6(K7(K7(INT,INT),INT)) is set

K7(NAT,NAT) is V22() set

K7(K7(NAT,NAT),NAT) is V22() set

K6(K7(K7(NAT,NAT),NAT)) is set

K7(COMPLEX,REAL) is V22() set

K6(K7(COMPLEX,REAL)) is set

0 is empty ordinal natural V11() real ext-real non positive non negative V22() non-empty empty-yielding V80() V81() V143() V144() V145() V146() V147() V148() V149() bounded_below V209() Element of NAT

the carrier of R^1 is non empty V143() V144() V145() set

K6( the carrier of R^1) is set

proj1 is non empty V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

TopSpaceMetr RealSpace is TopStruct

Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V200() SubSpace of R^1

real_dist is V22() V25(K7(REAL,REAL)) V26( REAL ) Function-like total quasi_total Element of K6(K7(K7(REAL,REAL),REAL))

MetrStruct(# REAL,real_dist #) is strict MetrStruct

[.0,1.] is V143() V144() V145() V209() Element of K6(REAL)

K6( the carrier of I[01]) is set

the carrier of RealSpace is non empty V143() V144() V145() set

P is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

Segment (P,p1,p2,p,p) is Element of K6( the carrier of (TOP-REAL 2))

{p} is non empty set

{ b

e is set

e is set

f is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

LSeg (P,p1) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

P `1 is V11() real ext-real Element of REAL

p1 `1 is V11() real ext-real Element of REAL

p2 `1 is V11() real ext-real Element of REAL

p is V11() real ext-real Element of REAL

e is V11() real ext-real Element of REAL

1 - e is V11() real ext-real Element of REAL

(1 - e) * P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

e * p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

((1 - e) * P) + (e * p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

((1 - e) * P) `1 is V11() real ext-real Element of REAL

(e * p1) `1 is V11() real ext-real Element of REAL

(((1 - e) * P) `1) + ((e * p1) `1) is V11() real ext-real Element of REAL

e * (p1 `1) is V11() real ext-real Element of REAL

(((1 - e) * P) `1) + (e * (p1 `1)) is V11() real ext-real Element of REAL

(1 - e) * (P `1) is V11() real ext-real Element of REAL

((1 - e) * (P `1)) + (e * (p1 `1)) is V11() real ext-real Element of REAL

(1 - e) * p is V11() real ext-real Element of REAL

e * p is V11() real ext-real Element of REAL

((1 - e) * p) + (e * p) is V11() real ext-real Element of REAL

p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

LSeg (P,p1) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

P `1 is V11() real ext-real Element of REAL

p1 `1 is V11() real ext-real Element of REAL

p2 `1 is V11() real ext-real Element of REAL

p is V11() real ext-real Element of REAL

e is V11() real ext-real Element of REAL

1 - e is V11() real ext-real Element of REAL

(1 - e) * P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

e * p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

((1 - e) * P) + (e * p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

((1 - e) * P) `1 is V11() real ext-real Element of REAL

(e * p1) `1 is V11() real ext-real Element of REAL

(((1 - e) * P) `1) + ((e * p1) `1) is V11() real ext-real Element of REAL

e * (p1 `1) is V11() real ext-real Element of REAL

(((1 - e) * P) `1) + (e * (p1 `1)) is V11() real ext-real Element of REAL

(1 - e) * (P `1) is V11() real ext-real Element of REAL

((1 - e) * (P `1)) + (e * (p1 `1)) is V11() real ext-real Element of REAL

(1 - e) * p is V11() real ext-real Element of REAL

e * p is V11() real ext-real Element of REAL

((1 - e) * p) + (e * p) is V11() real ext-real Element of REAL

p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

LSeg (P,p1) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

P `1 is V11() real ext-real Element of REAL

p1 `1 is V11() real ext-real Element of REAL

p2 `1 is V11() real ext-real Element of REAL

p is V11() real ext-real Element of REAL

e is V11() real ext-real Element of REAL

1 - e is V11() real ext-real Element of REAL

(1 - e) * P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

e * p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

((1 - e) * P) + (e * p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

((1 - e) * P) `1 is V11() real ext-real Element of REAL

(e * p1) `1 is V11() real ext-real Element of REAL

(((1 - e) * P) `1) + ((e * p1) `1) is V11() real ext-real Element of REAL

e * (p1 `1) is V11() real ext-real Element of REAL

(((1 - e) * P) `1) + (e * (p1 `1)) is V11() real ext-real Element of REAL

(1 - e) * (P `1) is V11() real ext-real Element of REAL

((1 - e) * (P `1)) + (e * (p1 `1)) is V11() real ext-real Element of REAL

0 * p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

P + (0 * p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

0. (TOP-REAL 2) is V43(2) V52( TOP-REAL 2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

P + (0. (TOP-REAL 2)) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

(1 - e) * p is V11() real ext-real Element of REAL

e * p is V11() real ext-real Element of REAL

((1 - e) * p) + (e * p) is V11() real ext-real Element of REAL

p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

LSeg (P,p1) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

P `1 is V11() real ext-real Element of REAL

p1 `1 is V11() real ext-real Element of REAL

p2 `1 is V11() real ext-real Element of REAL

p is V11() real ext-real Element of REAL

e is V11() real ext-real Element of REAL

1 - e is V11() real ext-real Element of REAL

(1 - e) * P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

e * p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

((1 - e) * P) + (e * p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

((1 - e) * P) `1 is V11() real ext-real Element of REAL

(e * p1) `1 is V11() real ext-real Element of REAL

(((1 - e) * P) `1) + ((e * p1) `1) is V11() real ext-real Element of REAL

e * (p1 `1) is V11() real ext-real Element of REAL

(((1 - e) * P) `1) + (e * (p1 `1)) is V11() real ext-real Element of REAL

(1 - e) * (P `1) is V11() real ext-real Element of REAL

((1 - e) * (P `1)) + (e * (p1 `1)) is V11() real ext-real Element of REAL

0 * p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

P + (0 * p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

0. (TOP-REAL 2) is V43(2) V52( TOP-REAL 2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

P + (0. (TOP-REAL 2)) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

(1 - e) * p is V11() real ext-real Element of REAL

e * p is V11() real ext-real Element of REAL

((1 - e) * p) + (e * p) is V11() real ext-real Element of REAL

P is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

P + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT

p1 is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like being_S-Seq FinSequence of the carrier of (TOP-REAL 2)

len p1 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

LSeg (p1,P) is Element of K6( the carrier of (TOP-REAL 2))

p1 /. P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

(p1 /. P) `2 is V11() real ext-real Element of REAL

p1 /. (P + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

(p1 /. (P + 1)) `2 is V11() real ext-real Element of REAL

(p1 /. P) `1 is V11() real ext-real Element of REAL

(p1 /. (P + 1)) `1 is V11() real ext-real Element of REAL

L~ p1 is Element of K6( the carrier of (TOP-REAL 2))

p1 /. 1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p1 /. (len p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p `1 is V11() real ext-real Element of REAL

p2 `1 is V11() real ext-real Element of REAL

LSeg ((p1 /. P),(p1 /. (P + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

((p1 /. P) `1) - (p2 `1) is V11() real ext-real Element of REAL

((p1 /. P) `1) - (p `1) is V11() real ext-real Element of REAL

(((p1 /. P) `1) - (p `1)) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL

e is V11() real ext-real Element of REAL

1 - e is V11() real ext-real Element of REAL

(((p1 /. P) `1) - (p2 `1)) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL

((((p1 /. P) `1) - (p2 `1)) / (((p1 /. P) `1) - (p2 `1))) - ((((p1 /. P) `1) - (p `1)) / (((p1 /. P) `1) - (p2 `1))) is V11() real ext-real Element of REAL

(((p1 /. P) `1) - (p2 `1)) - (((p1 /. P) `1) - (p `1)) is V11() real ext-real Element of REAL

((((p1 /. P) `1) - (p2 `1)) - (((p1 /. P) `1) - (p `1))) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL

(p `1) - (p2 `1) is V11() real ext-real Element of REAL

((p `1) - (p2 `1)) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL

(1 - e) * (p1 /. P) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

e * p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

((1 - e) * (p1 /. P)) + (e * p2) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

(((1 - e) * (p1 /. P)) + (e * p2)) `1 is V11() real ext-real Element of REAL

((1 - e) * (p1 /. P)) `1 is V11() real ext-real Element of REAL

(e * p2) `1 is V11() real ext-real Element of REAL

(((1 - e) * (p1 /. P)) `1) + ((e * p2) `1) is V11() real ext-real Element of REAL

(1 - e) * ((p1 /. P) `1) is V11() real ext-real Element of REAL

((1 - e) * ((p1 /. P) `1)) + ((e * p2) `1) is V11() real ext-real Element of REAL

1 * ((p1 /. P) `1) is V11() real ext-real Element of REAL

e * ((p1 /. P) `1) is V11() real ext-real Element of REAL

(1 * ((p1 /. P) `1)) - (e * ((p1 /. P) `1)) is V11() real ext-real Element of REAL

e * (p2 `1) is V11() real ext-real Element of REAL

((1 * ((p1 /. P) `1)) - (e * ((p1 /. P) `1))) + (e * (p2 `1)) is V11() real ext-real Element of REAL

e * (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL

((p1 /. P) `1) - (e * (((p1 /. P) `1) - (p2 `1))) is V11() real ext-real Element of REAL

((p1 /. P) `1) - (((p1 /. P) `1) - (p `1)) is V11() real ext-real Element of REAL

p2 `2 is V11() real ext-real Element of REAL

(((1 - e) * (p1 /. P)) + (e * p2)) `2 is V11() real ext-real Element of REAL

((1 - e) * (p1 /. P)) `2 is V11() real ext-real Element of REAL

(e * p2) `2 is V11() real ext-real Element of REAL

(((1 - e) * (p1 /. P)) `2) + ((e * p2) `2) is V11() real ext-real Element of REAL

(1 - e) * ((p1 /. P) `2) is V11() real ext-real Element of REAL

((1 - e) * ((p1 /. P) `2)) + ((e * p2) `2) is V11() real ext-real Element of REAL

1 * ((p1 /. P) `2) is V11() real ext-real Element of REAL

e * ((p1 /. P) `2) is V11() real ext-real Element of REAL

(1 * ((p1 /. P) `2)) - (e * ((p1 /. P) `2)) is V11() real ext-real Element of REAL

e * (p2 `2) is V11() real ext-real Element of REAL

((1 * ((p1 /. P) `2)) - (e * ((p1 /. P) `2))) + (e * (p2 `2)) is V11() real ext-real Element of REAL

p `2 is V11() real ext-real Element of REAL

0 + e is V11() real ext-real Element of REAL

(1 - e) + e is V11() real ext-real Element of REAL

LSeg ((p1 /. P),p2) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

P is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

P + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT

p1 is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like being_S-Seq FinSequence of the carrier of (TOP-REAL 2)

len p1 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT

LSeg (p1,P) is Element of K6( the carrier of (TOP-REAL 2))

p1 /. P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

(p1 /. P) `2 is V11() real ext-real Element of REAL

p1 /. (P + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

(p1 /. (P + 1)) `2 is V11() real ext-real Element of REAL

(p1 /. (P + 1)) `1 is V11() real ext-real Element of REAL

(p1 /. P) `1 is V11() real ext-real Element of REAL

L~ p1 is Element of K6( the carrier of (TOP-REAL 2))

p1 /. 1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p1 /. (len p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p2 `1 is V11() real ext-real Element of REAL

p `1 is V11() real ext-real Element of REAL

LSeg ((p1 /. P),(p1 /. (P + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

((p1 /. P) `1) - (p2 `1) is V11() real ext-real Element of REAL

((p1 /. P) `1) - (p `1) is V11() real ext-real Element of REAL

(((p1 /. P) `1) - (p `1)) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL

e is V11() real ext-real Element of REAL

1 - e is V11() real ext-real Element of REAL

(((p1 /. P) `1) - (p2 `1)) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL

((((p1 /. P) `1) - (p2 `1)) / (((p1 /. P) `1) - (p2 `1))) - ((((p1 /. P) `1) - (p `1)) / (((p1 /. P) `1) - (p2 `1))) is V11() real ext-real Element of REAL

(((p1 /. P) `1) - (p2 `1)) - (((p1 /. P) `1) - (p `1)) is V11() real ext-real Element of REAL

((((p1 /. P) `1) - (p2 `1)) - (((p1 /. P) `1) - (p `1))) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL

(p `1) - (p2 `1) is V11() real ext-real Element of REAL

((p `1) - (p2 `1)) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL

(1 - e) * (p1 /. P) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

e * p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

((1 - e) * (p1 /. P)) + (e * p2) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

(((1 - e) * (p1 /. P)) + (e * p2)) `1 is V11() real ext-real Element of REAL

((1 - e) * (p1 /. P)) `1 is V11() real ext-real Element of REAL

(e * p2) `1 is V11() real ext-real Element of REAL

(((1 - e) * (p1 /. P)) `1) + ((e * p2) `1) is V11() real ext-real Element of REAL

(1 - e) * ((p1 /. P) `1) is V11() real ext-real Element of REAL

((1 - e) * ((p1 /. P) `1)) + ((e * p2) `1) is V11() real ext-real Element of REAL

1 * ((p1 /. P) `1) is V11() real ext-real Element of REAL

e * ((p1 /. P) `1) is V11() real ext-real Element of REAL

(1 * ((p1 /. P) `1)) - (e * ((p1 /. P) `1)) is V11() real ext-real Element of REAL

e * (p2 `1) is V11() real ext-real Element of REAL

((1 * ((p1 /. P) `1)) - (e * ((p1 /. P) `1))) + (e * (p2 `1)) is V11() real ext-real Element of REAL

e * (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL

((p1 /. P) `1) - (e * (((p1 /. P) `1) - (p2 `1))) is V11() real ext-real Element of REAL

((p1 /. P) `1) - (((p1 /. P) `1) - (p `1)) is V11() real ext-real Element of REAL

p2 `2 is V11() real ext-real Element of REAL

(((1 - e) * (p1 /. P)) + (e * p2)) `2 is V11() real ext-real Element of REAL

((1 - e) * (p1 /. P)) `2 is V11() real ext-real Element of REAL

(e * p2) `2 is V11() real ext-real Element of REAL

(((1 - e) * (p1 /. P)) `2) + ((e * p2) `2) is V11() real ext-real Element of REAL

(1 - e) * ((p1 /. P) `2) is V11() real ext-real Element of REAL

((1 - e) * ((p1 /. P) `2)) + ((e * p2) `2) is V11() real ext-real Element of REAL

1 * ((p1 /. P) `2) is V11() real ext-real Element of REAL

e * ((p1 /. P) `2) is V11() real ext-real Element of REAL

(1 * ((p1 /. P) `2)) - (e * ((p1 /. P) `2)) is V11() real ext-real Element of REAL

e * (p2 `2) is V11() real ext-real Element of REAL

((1 * ((p1 /. P) `2)) - (e * ((p1 /. P) `2))) + (e * (p2 `2)) is V11() real ext-real Element of REAL

p `2 is V11() real ext-real Element of REAL

0 + e is V11() real ext-real Element of REAL

(1 - e) + e is V11() real ext-real Element of REAL

LSeg ((p1 /. P),p2) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))

{ (((1 - b

P is Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p1 `1 is V11() real ext-real Element of REAL

p2 `1 is V11() real ext-real Element of REAL

e is V11() real ext-real Element of REAL

Vertical_Line e is Element of K6( the carrier of (TOP-REAL 2))

P /\ (Vertical_Line e) is Element of K6( the carrier of (TOP-REAL 2))

the Element of P /\ (Vertical_Line e) is Element of P /\ (Vertical_Line e)

{ b

Y is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

Y `1 is V11() real ext-real Element of REAL

P is non empty Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p1 `1 is V11() real ext-real Element of REAL

p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p `1 is V11() real ext-real Element of REAL

e is V11() real ext-real Element of REAL

K7( the carrier of (TOP-REAL 2), the carrier of R^1) is V22() set

K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1)) is set

(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | P) is non empty set

K7( the carrier of ((TOP-REAL 2) | P), the carrier of R^1) is V22() set

K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of R^1)) is set

f is non empty V22() V25( the carrier of (TOP-REAL 2)) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))

f | P is V22() V25( the carrier of (TOP-REAL 2)) V25(P) V25( the carrier of (TOP-REAL 2)) V26( the carrier of R^1) Function-like Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))

K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set

i is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

i . 0 is set

i . 1 is set

rng i is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))

K6( the carrier of ((TOP-REAL 2) | P)) is set

[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))

dom i is non empty V143() V144() V145() Element of K6( the carrier of I[01])

k is set

i . k is set

[#] I[01] is non empty non proper closed V143() V144() V145() Element of K6( the carrier of I[01])

pk is V11() real ext-real Element of REAL

p44 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p44 `1 is V11() real ext-real Element of REAL

{ b

( not b

p44 is set

p5 is V11() real ext-real Element of REAL

i . p5 is set

p44 is non empty V143() V144() V145() Element of K6(REAL)

p5 is set

Y3 is V11() real ext-real Element of REAL

i . Y3 is set

upper_bound p44 is V11() real ext-real Element of REAL

kk is V11() real ext-real set

k2 is V11() real ext-real Element of REAL

i . k2 is set

k2 is V11() real ext-real Element of REAL

i . k2 is set

kk is V11() real ext-real set

Y3 is V11() real ext-real Element of REAL

p5 is V143() V144() V145() Element of K6( the carrier of I[01])

i . Y3 is set

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

Y is non empty V22() V25( the carrier of ((TOP-REAL 2) | P)) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of R^1))

k2 is Element of the carrier of ((TOP-REAL 2) | P)

Y . k2 is V11() real ext-real Element of the carrier of R^1

proj1 . k2 is set

K7( the carrier of I[01], the carrier of R^1) is V22() set

K6(K7( the carrier of I[01], the carrier of R^1)) is set

Y * i is non empty V22() V25( the carrier of I[01]) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of R^1))

k2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of R^1))

dom k2 is non empty V143() V144() V145() Element of K6( the carrier of I[01])

z is ext-real set

z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

z `1 is V11() real ext-real Element of REAL

kk is set

i . kk is set

k2 is V11() real ext-real Element of REAL

Closed-Interval-MSpace (0,1) is non empty strict Reflexive discerning symmetric triangle Discerning SubSpace of RealSpace

the carrier of (Closed-Interval-MSpace (0,1)) is non empty set

(z `1) - e is V11() real ext-real Element of REAL

abs ((z `1) - e) is V11() real ext-real Element of REAL

(abs ((z `1) - e)) / 2 is V11() real ext-real Element of REAL

G5 is V11() real ext-real Element of the carrier of RealSpace

G4 is V11() real ext-real Element of REAL

Ball (G5,G4) is V143() V144() V145() Element of K6( the carrier of RealSpace)

K6( the carrier of RealSpace) is set

r0 is V143() V144() V145() Element of K6( the carrier of R^1)

(z `1) - G4 is V11() real ext-real Element of REAL

(z `1) + G4 is V11() real ext-real Element of REAL

{ b

].((z `1) - G4),((z `1) + G4).[ is V143() V144() V145() non left_end non right_end V209() Element of K6(REAL)

k2 " r0 is V143() V144() V145() Element of K6( the carrier of I[01])

TopSpaceMetr (Closed-Interval-MSpace (0,1)) is TopStruct

k2 . k2 is set

i . k2 is set

Y . (i . k2) is set

proj1 . z is V11() real ext-real Element of REAL

G2 is Element of the carrier of (Closed-Interval-MSpace (0,1))

r0 is V11() real ext-real set

Ball (G2,r0) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))

K6( the carrier of (Closed-Interval-MSpace (0,1))) is set

pk - k2 is V11() real ext-real Element of REAL

r01 is V11() real ext-real Element of REAL

min ((pk - k2),r01) is V11() real ext-real Element of REAL

s70 is V11() real ext-real Element of REAL

s70 / 2 is V11() real ext-real Element of REAL

s70 - (s70 / 2) is V11() real ext-real Element of REAL

(s70 - (s70 / 2)) + (s70 / 2) is V11() real ext-real Element of REAL

0 + (s70 / 2) is V11() real ext-real Element of REAL

k2 + s70 is V11() real ext-real Element of REAL

k2 + (s70 / 2) is V11() real ext-real Element of REAL

z is V11() real ext-real Element of the carrier of RealSpace

Ball (z,s70) is V143() V144() V145() Element of K6( the carrier of RealSpace)

k2 - s70 is V11() real ext-real Element of REAL

].(k2 - s70),(k2 + s70).[ is V143() V144() V145() non left_end non right_end V209() Element of K6(REAL)

Ball (G2,s70) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))

].(k2 - s70),(k2 + s70).[ /\ [.0,1.] is V143() V144() V145() V209() Element of K6(REAL)

s70 + k2 is V11() real ext-real Element of REAL

(pk - k2) + k2 is V11() real ext-real Element of REAL

s7 is V11() real ext-real Element of REAL

Ball (G2,r01) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))

(s70 / 2) + s70 is V11() real ext-real Element of REAL

k2 + ((s70 / 2) + s70) is V11() real ext-real Element of REAL

k2 + 0 is V11() real ext-real Element of REAL

(k2 + (s70 / 2)) + s70 is V11() real ext-real Element of REAL

(k2 - s70) + s70 is V11() real ext-real Element of REAL

k2 . (k2 + (s70 / 2)) is set

i . s7 is set

s7 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

s7 `1 is V11() real ext-real Element of REAL

k2 . s7 is set

Y . (i . s7) is set

f . s7 is V11() real ext-real Element of the carrier of R^1

((z `1) - e) / 2 is V11() real ext-real Element of REAL

(z `1) - (((z `1) - e) / 2) is V11() real ext-real Element of REAL

e / 2 is V11() real ext-real Element of REAL

(e / 2) + (e / 2) is V11() real ext-real Element of REAL

(z `1) / 2 is V11() real ext-real Element of REAL

((z `1) / 2) + (e / 2) is V11() real ext-real Element of REAL

(e / 2) - (e / 2) is V11() real ext-real Element of REAL

((z `1) / 2) - (e / 2) is V11() real ext-real Element of REAL

0 / 2 is empty V11() real ext-real non positive non negative V22() non-empty empty-yielding V143() V144() V145() V146() V147() V148() V149() bounded_below V209() Element of REAL

- ((z `1) - e) is V11() real ext-real Element of REAL

(- ((z `1) - e)) / 2 is V11() real ext-real Element of REAL

(z `1) + ((- ((z `1) - e)) / 2) is V11() real ext-real Element of REAL

(z `1) / 2 is V11() real ext-real Element of REAL

e / 2 is V11() real ext-real Element of REAL

((z `1) / 2) + (e / 2) is V11() real ext-real Element of REAL

(e / 2) + (e / 2) is V11() real ext-real Element of REAL

((z `1) / 2) - (e / 2) is V11() real ext-real Element of REAL

(e / 2) - (e / 2) is V11() real ext-real Element of REAL

((z `1) - e) / 2 is V11() real ext-real Element of REAL

0 / 2 is empty V11() real ext-real non positive non negative V22() non-empty empty-yielding V143() V144() V145() V146() V147() V148() V149() bounded_below V209() Element of REAL

s7 is V11() real ext-real Element of REAL

i . s7 is set

z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

kk is set

i . kk is set

k2 is V11() real ext-real Element of REAL

z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

z `1 is V11() real ext-real Element of REAL

Y3 - k2 is V11() real ext-real Element of REAL

(Y3 - k2) / 2 is V11() real ext-real Element of REAL

k2 + ((Y3 - k2) / 2) is V11() real ext-real Element of REAL

Y3 - ((Y3 - k2) / 2) is V11() real ext-real Element of REAL

z is V11() real ext-real set

G4 is V11() real ext-real Element of REAL

i . G4 is set

G2 is V11() real ext-real Element of REAL

i . G2 is set

G4 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

G4 `1 is V11() real ext-real Element of REAL

G5 is V11() real ext-real Element of REAL

i . G5 is set

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

kk `1 is V11() real ext-real Element of REAL

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

kk `1 is V11() real ext-real Element of REAL

k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

k2 `1 is V11() real ext-real Element of REAL

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

kk `1 is V11() real ext-real Element of REAL

kk is set

i . kk is set

k2 is V11() real ext-real Element of REAL

z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

z `1 is V11() real ext-real Element of REAL

Y3 - k2 is V11() real ext-real Element of REAL

(Y3 - k2) / 2 is V11() real ext-real Element of REAL

k2 + ((Y3 - k2) / 2) is V11() real ext-real Element of REAL

Y3 - ((Y3 - k2) / 2) is V11() real ext-real Element of REAL

z is V11() real ext-real set

G4 is V11() real ext-real Element of REAL

i . G4 is set

G2 is V11() real ext-real Element of REAL

i . G2 is set

G4 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

G4 `1 is V11() real ext-real Element of REAL

G5 is V11() real ext-real Element of REAL

i . G5 is set

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

kk `1 is V11() real ext-real Element of REAL

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

kk `1 is V11() real ext-real Element of REAL

k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

k2 `1 is V11() real ext-real Element of REAL

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

kk `1 is V11() real ext-real Element of REAL

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

kk `1 is V11() real ext-real Element of REAL

k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

k2 `1 is V11() real ext-real Element of REAL

P is non empty Element of K6( the carrier of (TOP-REAL 2))

p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p2 `1 is V11() real ext-real Element of REAL

p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p `1 is V11() real ext-real Element of REAL

e is V11() real ext-real Element of REAL

K7( the carrier of (TOP-REAL 2), the carrier of R^1) is V22() set

K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1)) is set

(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | P) is non empty set

K7( the carrier of ((TOP-REAL 2) | P), the carrier of R^1) is V22() set

K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of R^1)) is set

f is non empty V22() V25( the carrier of (TOP-REAL 2)) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))

f | P is V22() V25( the carrier of (TOP-REAL 2)) V25(P) V25( the carrier of (TOP-REAL 2)) V26( the carrier of R^1) Function-like Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))

K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set

i is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

i . 0 is set

i . 1 is set

rng i is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))

K6( the carrier of ((TOP-REAL 2) | P)) is set

[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))

dom i is non empty V143() V144() V145() Element of K6( the carrier of I[01])

k is set

i . k is set

[#] I[01] is non empty non proper closed V143() V144() V145() Element of K6( the carrier of I[01])

pk is V11() real ext-real Element of REAL

p44 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p44 `1 is V11() real ext-real Element of REAL

{ b

( not b

p44 is set

p5 is V11() real ext-real Element of REAL

i . p5 is set

p44 is non empty V143() V144() V145() Element of K6(REAL)

lower_bound p44 is V11() real ext-real Element of REAL

Y3 is V11() real ext-real set

kk is V11() real ext-real Element of REAL

i . kk is set

kk is V11() real ext-real Element of REAL

i . kk is set

Y3 is V11() real ext-real set

p5 is V11() real ext-real Element of REAL

Y is non empty V22() V25( the carrier of ((TOP-REAL 2) | P)) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of R^1))

Y3 is Element of the carrier of ((TOP-REAL 2) | P)

Y . Y3 is V11() real ext-real Element of the carrier of R^1

proj1 . Y3 is set

K7( the carrier of I[01], the carrier of R^1) is V22() set

K6(K7( the carrier of I[01], the carrier of R^1)) is set

Y * i is non empty V22() V25( the carrier of I[01]) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of R^1))

Y3 is non empty V22() V25( the carrier of I[01]) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of R^1))

dom Y3 is non empty V143() V144() V145() Element of K6( the carrier of I[01])

kk is ext-real set

kk is set

k2 is V11() real ext-real Element of REAL

i . k2 is set

i . p5 is set

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

k2 `1 is V11() real ext-real Element of REAL

z is set

i . z is set

kk is V11() real ext-real Element of REAL

Closed-Interval-MSpace (0,1) is non empty strict Reflexive discerning symmetric triangle Discerning SubSpace of RealSpace

the carrier of (Closed-Interval-MSpace (0,1)) is non empty set

(k2 `1) - e is V11() real ext-real Element of REAL

abs ((k2 `1) - e) is V11() real ext-real Element of REAL

(abs ((k2 `1) - e)) / 2 is V11() real ext-real Element of REAL

G4 is V11() real ext-real Element of the carrier of RealSpace

G2 is V11() real ext-real Element of REAL

Ball (G4,G2) is V143() V144() V145() Element of K6( the carrier of RealSpace)

K6( the carrier of RealSpace) is set

G5 is V143() V144() V145() Element of K6( the carrier of R^1)

(k2 `1) - G2 is V11() real ext-real Element of REAL

(k2 `1) + G2 is V11() real ext-real Element of REAL

{ b

].((k2 `1) - G2),((k2 `1) + G2).[ is V143() V144() V145() non left_end non right_end V209() Element of K6(REAL)

Y3 " G5 is V143() V144() V145() Element of K6( the carrier of I[01])

TopSpaceMetr (Closed-Interval-MSpace (0,1)) is TopStruct

Y3 . kk is set

i . kk is set

Y . (i . kk) is set

proj1 . k2 is V11() real ext-real Element of REAL

z is Element of the carrier of (Closed-Interval-MSpace (0,1))

r0 is V11() real ext-real set

Ball (z,r0) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))

K6( the carrier of (Closed-Interval-MSpace (0,1))) is set

kk - pk is V11() real ext-real Element of REAL

r0 is V11() real ext-real Element of REAL

min ((kk - pk),r0) is V11() real ext-real Element of REAL

k2 is V11() real ext-real Element of the carrier of RealSpace

r01 is V11() real ext-real Element of REAL

Ball (k2,r01) is V143() V144() V145() Element of K6( the carrier of RealSpace)

kk - r01 is V11() real ext-real Element of REAL

kk + r01 is V11() real ext-real Element of REAL

].(kk - r01),(kk + r01).[ is V143() V144() V145() non left_end non right_end V209() Element of K6(REAL)

Ball (z,r01) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))

].(kk - r01),(kk + r01).[ /\ [.0,1.] is V143() V144() V145() V209() Element of K6(REAL)

r01 / 2 is V11() real ext-real Element of REAL

r01 - (r01 / 2) is V11() real ext-real Element of REAL

(r01 - (r01 / 2)) + (r01 / 2) is V11() real ext-real Element of REAL

0 + (r01 / 2) is V11() real ext-real Element of REAL

kk - (r01 / 2) is V11() real ext-real Element of REAL

kk + (r01 / 2) is V11() real ext-real Element of REAL

- (r01 / 2) is V11() real ext-real Element of REAL

kk + (- (r01 / 2)) is V11() real ext-real Element of REAL

Ball (z,r0) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))

- (kk - pk) is V11() real ext-real Element of REAL

- r01 is V11() real ext-real Element of REAL

pk - kk is V11() real ext-real Element of REAL

(pk - kk) + kk is V11() real ext-real Element of REAL

(- r01) + kk is V11() real ext-real Element of REAL

- (- (r01 / 2)) is V11() real ext-real Element of REAL

kk + 0 is V11() real ext-real Element of REAL

s70 is V11() real ext-real Element of REAL

1 - 0 is non empty V11() real ext-real positive non negative Element of REAL

Y3 . (kk - (r01 / 2)) is set

i . s70 is set

s7 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

s7 `1 is V11() real ext-real Element of REAL

Y3 . s70 is set

Y . (i . s70) is set

f . s7 is V11() real ext-real Element of the carrier of R^1

((k2 `1) - e) / 2 is V11() real ext-real Element of REAL

(k2 `1) - (((k2 `1) - e) / 2) is V11() real ext-real Element of REAL

e / 2 is V11() real ext-real Element of REAL

(e / 2) + (e / 2) is V11() real ext-real Element of REAL

(k2 `1) / 2 is V11() real ext-real Element of REAL

((k2 `1) / 2) + (e / 2) is V11() real ext-real Element of REAL

(e / 2) - (e / 2) is V11() real ext-real Element of REAL

((k2 `1) / 2) - (e / 2) is V11() real ext-real Element of REAL

0 / 2 is empty V11() real ext-real non positive non negative V22() non-empty empty-yielding V143() V144() V145() V146() V147() V148() V149() bounded_below V209() Element of REAL

- ((k2 `1) - e) is V11() real ext-real Element of REAL

(- ((k2 `1) - e)) / 2 is V11() real ext-real Element of REAL

(k2 `1) + ((- ((k2 `1) - e)) / 2) is V11() real ext-real Element of REAL

(k2 `1) / 2 is V11() real ext-real Element of REAL

e / 2 is V11() real ext-real Element of REAL

((k2 `1) / 2) + (e / 2) is V11() real ext-real Element of REAL

(e / 2) + (e / 2) is V11() real ext-real Element of REAL

((k2 `1) / 2) - (e / 2) is V11() real ext-real Element of REAL

(e / 2) - (e / 2) is V11() real ext-real Element of REAL

((k2 `1) - e) / 2 is V11() real ext-real Element of REAL

0 / 2 is empty V11() real ext-real non positive non negative V22() non-empty empty-yielding V143() V144() V145() V146() V147() V148() V149() bounded_below V209() Element of REAL

s7 is V11() real ext-real Element of REAL

i . s7 is set

k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

z is set

i . z is set

kk is V11() real ext-real Element of REAL

k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

k2 `1 is V11() real ext-real Element of REAL

kk - p5 is V11() real ext-real Element of REAL

- (kk - p5) is V11() real ext-real Element of REAL

- (- (kk - p5)) is V11() real ext-real Element of REAL

p5 - kk is V11() real ext-real Element of REAL

(p5 - kk) / 2 is V11() real ext-real Element of REAL

- ((p5 - kk) / 2) is V11() real ext-real Element of REAL

p5 + (- ((p5 - kk) / 2)) is V11() real ext-real Element of REAL

k2 is V11() real ext-real set

G2 is V11() real ext-real Element of REAL

i . G2 is set

z is V11() real ext-real Element of REAL

i . z is set

kk + 0 is V11() real ext-real Element of REAL

kk + ((p5 - kk) / 2) is V11() real ext-real Element of REAL

G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

G2 `1 is V11() real ext-real Element of REAL

G4 is V11() real ext-real Element of REAL

i . G4 is set

z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

z `1 is V11() real ext-real Element of REAL

z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

z `1 is V11() real ext-real Element of REAL

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

kk `1 is V11() real ext-real Element of REAL

z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

z `1 is V11() real ext-real Element of REAL

z is set

i . z is set

kk is V11() real ext-real Element of REAL

k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

k2 `1 is V11() real ext-real Element of REAL

kk - p5 is V11() real ext-real Element of REAL

- (kk - p5) is V11() real ext-real Element of REAL

- (- (kk - p5)) is V11() real ext-real Element of REAL

p5 - kk is V11() real ext-real Element of REAL

(p5 - kk) / 2 is V11() real ext-real Element of REAL

- ((p5 - kk) / 2) is V11() real ext-real Element of REAL

p5 + (- ((p5 - kk) / 2)) is V11() real ext-real Element of REAL

k2 is V11() real ext-real set

G2 is V11() real ext-real Element of REAL

i . G2 is set

z is V11() real ext-real Element of REAL

i . z is set

kk + 0 is V11() real ext-real Element of REAL

kk + ((p5 - kk) / 2) is V11() real ext-real Element of REAL

G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

G2 `1 is V11() real ext-real Element of REAL

G4 is V11() real ext-real Element of REAL

i . G4 is set

z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

z `1 is V11() real ext-real Element of REAL

z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

z `1 is V11() real ext-real Element of REAL

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

kk `1 is V11() real ext-real Element of REAL

z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

z `1 is V11() real ext-real Element of REAL

z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

z `1 is V11() real ext-real Element of REAL

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

kk `1 is V11() real ext-real Element of REAL

[#] I[01] is non empty non proper closed V143() V144() V145() Element of K6( the carrier of I[01])

P is V143() V144() V145() Element of K6( the carrier of I[01])

p1 is V11() real ext-real Element of REAL

[.0,p1.[ is V143() V144() V145() non right_end V209() Element of K6(REAL)

[.0,p1.] is V143() V144() V145() V209() Element of K6(REAL)

p2 is V143() V144() V145() Element of K6( the carrier of R^1)

R^1 | p2 is strict TopSpace-like V200() SubSpace of R^1

[#] (R^1 | p2) is non proper closed V143() V144() V145() Element of K6( the carrier of (R^1 | p2))

the carrier of (R^1 | p2) is V143() V144() V145() set

K6( the carrier of (R^1 | p2)) is set

- 1 is V11() real ext-real non positive Element of REAL

].(- 1),p1.[ is V143() V144() V145() non left_end non right_end V209() Element of K6(REAL)

].(- 1),p1.[ /\ [.0,1.] is V143() V144() V145() V209() Element of K6(REAL)

f is set

Y is V11() real ext-real Element of REAL

f is set

Y is V11() real ext-real Element of REAL

p is V143() V144() V145() Element of K6( the carrier of (R^1 | p2))

e is V143() V144() V145() Element of K6( the carrier of R^1)

e /\ ([#] (R^1 | p2)) is V143() V144() V145() Element of K6( the carrier of (R^1 | p2))

the topology of I[01] is non empty Element of K6(K6( the carrier of I[01]))

K6(K6( the carrier of I[01])) is set

p2 is V11() real ext-real Element of REAL

p2 is V11() real ext-real set

p is V11() real ext-real Element of REAL

[#] I[01] is non empty non proper closed V143() V144() V145() Element of K6( the carrier of I[01])

P is V143() V144() V145() Element of K6( the carrier of I[01])

p1 is V11() real ext-real Element of REAL

].p1,1.] is V143() V144() V145() non left_end V209() Element of K6(REAL)

[.p1,1.] is V143() V144() V145() V209() Element of K6(REAL)

p2 is V143() V144() V145() Element of K6( the carrier of R^1)

R^1 | p2 is strict TopSpace-like V200() SubSpace of R^1

[#] (R^1 | p2) is non proper closed V143() V144() V145() Element of K6( the carrier of (R^1 | p2))

the carrier of (R^1 | p2) is V143() V144() V145() set

K6( the carrier of (R^1 | p2)) is set

].p1,2.[ is V143() V144() V145() non left_end non right_end V209() Element of K6(REAL)

].p1,2.[ /\ [.0,1.] is V143() V144() V145() V209() Element of K6(REAL)

f is set

Y is V11() real ext-real Element of REAL

f is set

Y is V11() real ext-real Element of REAL

p is V143() V144() V145() Element of K6( the carrier of (R^1 | p2))

e is V143() V144() V145() Element of K6( the carrier of R^1)

e /\ ([#] (R^1 | p2)) is V143() V144() V145() Element of K6( the carrier of (R^1 | p2))

the topology of I[01] is non empty Element of K6(K6( the carrier of I[01]))

K6(K6( the carrier of I[01])) is set

p2 is V11() real ext-real Element of REAL

p2 is V11() real ext-real set

p is V11() real ext-real Element of REAL

P is non empty Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | P) is non empty set

K6( the carrier of ((TOP-REAL 2) | P)) is set

K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set

p1 is Element of K6( the carrier of ((TOP-REAL 2) | P))

p2 is V143() V144() V145() Element of K6( the carrier of I[01])

p is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

p .: p2 is Element of K6( the carrier of ((TOP-REAL 2) | P))

e is V11() real ext-real Element of REAL

{ b

( 0 <= b

[.0,e.[ is V143() V144() V145() non right_end V209() Element of K6(REAL)

f is set

dom p is non empty V143() V144() V145() Element of K6( the carrier of I[01])

Y is set

p . Y is set

rng p is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))

i is V11() real ext-real Element of REAL

k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

pk is V11() real ext-real Element of REAL

p . pk is set

f is set

dom p is non empty V143() V144() V145() Element of K6( the carrier of I[01])

Y is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

i is V11() real ext-real Element of REAL

p . i is set

i is V11() real ext-real Element of REAL

p . i is set

P is non empty Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | P) is non empty set

K6( the carrier of ((TOP-REAL 2) | P)) is set

K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set

p1 is Element of K6( the carrier of ((TOP-REAL 2) | P))

p2 is V143() V144() V145() Element of K6( the carrier of I[01])

p is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

p .: p2 is Element of K6( the carrier of ((TOP-REAL 2) | P))

e is V11() real ext-real Element of REAL

{ b

( not b

].e,1.] is V143() V144() V145() non left_end V209() Element of K6(REAL)

f is set

dom p is non empty V143() V144() V145() Element of K6( the carrier of I[01])

Y is set

p . Y is set

rng p is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))

i is V11() real ext-real Element of REAL

k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

pk is V11() real ext-real Element of REAL

p . pk is set

f is set

Y is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

i is V11() real ext-real Element of REAL

p . i is set

i is V11() real ext-real Element of REAL

p . i is set

dom p is non empty V143() V144() V145() Element of K6( the carrier of I[01])

[#] I[01] is non empty non proper closed V143() V144() V145() Element of K6( the carrier of I[01])

P is non empty Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | P) is non empty set

K6( the carrier of ((TOP-REAL 2) | P)) is set

K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set

p1 is Element of K6( the carrier of ((TOP-REAL 2) | P))

p2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

p is V11() real ext-real Element of REAL

{ b

( 0 <= b

rng p2 is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))

[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))

p2 " is non empty V22() V25( the carrier of ((TOP-REAL 2) | P)) V26( the carrier of I[01]) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of I[01]))

K7( the carrier of ((TOP-REAL 2) | P), the carrier of I[01]) is V22() set

K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of I[01])) is set

(p2 ") " is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

[.0,p.[ is V143() V144() V145() non right_end V209() Element of K6(REAL)

e is set

f is V11() real ext-real Element of REAL

e is V143() V144() V145() Element of K6( the carrier of I[01])

rng (p2 ") is non empty V143() V144() V145() Element of K6( the carrier of I[01])

(p2 ") " is V22() Function-like set

((p2 ") ") .: e is Element of K6( the carrier of ((TOP-REAL 2) | P))

(p2 ") " e is Element of K6( the carrier of ((TOP-REAL 2) | P))

p2 .: e is Element of K6( the carrier of ((TOP-REAL 2) | P))

P is non empty Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | P) is non empty set

K6( the carrier of ((TOP-REAL 2) | P)) is set

K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set

p1 is Element of K6( the carrier of ((TOP-REAL 2) | P))

p2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

p is V11() real ext-real Element of REAL

{ b

( not b

rng p2 is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))

[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))

p2 " is non empty V22() V25( the carrier of ((TOP-REAL 2) | P)) V26( the carrier of I[01]) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of I[01]))

K7( the carrier of ((TOP-REAL 2) | P), the carrier of I[01]) is V22() set

K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of I[01])) is set

(p2 ") " is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

].p,1.] is V143() V144() V145() non left_end V209() Element of K6(REAL)

e is set

f is V11() real ext-real Element of REAL

e is V143() V144() V145() Element of K6( the carrier of I[01])

rng (p2 ") is non empty V143() V144() V145() Element of K6( the carrier of I[01])

(p2 ") " is V22() Function-like set

((p2 ") ") .: e is Element of K6( the carrier of ((TOP-REAL 2) | P))

(p2 ") " e is Element of K6( the carrier of ((TOP-REAL 2) | P))

p2 .: e is Element of K6( the carrier of ((TOP-REAL 2) | P))

P is non empty TopStruct

the carrier of P is non empty set

K6( the carrier of P) is set

K7( the carrier of I[01], the carrier of P) is V22() set

K6(K7( the carrier of I[01], the carrier of P)) is set

p1 is Element of K6( the carrier of P)

p2 is Element of K6( the carrier of P)

p1 /\ p2 is Element of K6( the carrier of P)

p1 \/ p2 is Element of K6( the carrier of P)

p is Element of the carrier of P

e is Element of the carrier of P

f is non empty V22() V25( the carrier of I[01]) V26( the carrier of P) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of P))

f . 0 is set

f . 1 is set

f is non empty V22() V25( the carrier of I[01]) V26( the carrier of P) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of P))

f . 0 is set

f . 1 is set

[#] P is non empty non proper Element of K6( the carrier of P)

f " p1 is V143() V144() V145() Element of K6( the carrier of I[01])

f " p2 is V143() V144() V145() Element of K6( the carrier of I[01])

dom f is non empty V143() V144() V145() Element of K6( the carrier of I[01])

{} I[01] is empty V22() non-empty empty-yielding closed V143() V144() V145() V146() V147() V148() V149() bounded_below V209() Element of K6( the carrier of I[01])

(f " p1) /\ (f " p2) is V143() V144() V145() Element of K6( the carrier of I[01])

f " (p1 /\ p2) is V143() V144() V145() Element of K6( the carrier of I[01])

(f " p1) \/ (f " p2) is V143() V144() V145() Element of K6( the carrier of I[01])

f " (p1 \/ p2) is V143() V144() V145() Element of K6( the carrier of I[01])

P is non empty Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | P) is non empty set

K6( the carrier of ((TOP-REAL 2) | P)) is set

p1 is Element of K6( the carrier of ((TOP-REAL 2) | P))

((TOP-REAL 2) | P) | p1 is strict TopSpace-like SubSpace of (TOP-REAL 2) | P

the carrier of (((TOP-REAL 2) | P) | p1) is set

K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | p1)) is V22() set

K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | p1))) is set

p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

e is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

{e} is non empty set

P \ {e} is Element of K6( the carrier of (TOP-REAL 2))

K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set

K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set

f is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

f . 0 is set

f . 1 is set

rng f is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))

[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))

dom f is non empty V143() V144() V145() Element of K6( the carrier of I[01])

Y is set

f . Y is set

i is V11() real ext-real Element of REAL

{ b

( not b

k is set

pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p44 is V11() real ext-real Element of REAL

f . p44 is set

p44 is V11() real ext-real Element of REAL

f . p44 is set

k is Element of K6( the carrier of ((TOP-REAL 2) | P))

pk is set

p44 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p5 is V11() real ext-real Element of REAL

f . p5 is set

p5 is V11() real ext-real Element of REAL

f . p5 is set

{ b

( 0 <= b

pk is set

p44 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

p5 is V11() real ext-real Element of REAL

f . p5 is set

p5 is V11() real ext-real Element of REAL

f . p5 is set

pk is Element of K6( the carrier of ((TOP-REAL 2) | P))

pk \/ k is Element of K6( the carrier of ((TOP-REAL 2) | P))

p44 is set

p5 is set

f . p5 is set

Y3 is V11() real ext-real Element of REAL

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

k2 is V11() real ext-real Element of REAL

f . k2 is set

kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

k2 is V11() real ext-real Element of REAL

f . k2 is set

p44 is set

p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)

Y3 is V11() real ext-real Element of REAL

f . Y3 is set

Y3 is V11() real ext-real Element of REAL

f . Y3 is set

kk is V43(2) FinSequence-like