:: JORDAN6 semantic presentation

REAL is non empty V36() V146() V147() V148() V152() V181() set

NAT is V146() V147() V148() V149() V150() V151() V152() V181() Element of K6(REAL)

K6(REAL) is set

COMPLEX is non empty V36() V146() V152() set

omega is V146() V147() V148() V149() V150() V151() V152() V181() set

K6(omega) is set

K6(NAT) is set

1 is non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT

K7(1,1) is set

K6(K7(1,1)) is set

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

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

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

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

K7(REAL,REAL) is set

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

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

2 is non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT

K7(2,2) is set

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

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

RAT is non empty V36() V146() V147() V148() V149() V152() set

INT is non empty V36() V146() V147() V148() V149() V150() V152() set

K6(K7(REAL,REAL)) is set

TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() RLTopStruct

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

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

I[01] is non empty strict TopSpace-like T_0 T_1 T_2 compact V200() TopStruct

the carrier of I[01] is non empty V146() V147() V148() set

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

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

0 is empty natural V11() real ext-real non positive non negative V83() V84() V146() V147() V148() V149() V150() V151() V152() Element of NAT

the empty V146() V147() V148() V149() V150() V151() V152() set is empty V146() V147() V148() V149() V150() V151() V152() set

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

the carrier of (Closed-Interval-TSpace (0,1)) is non empty V146() V147() V148() set

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

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

K7(COMPLEX,COMPLEX) is set

K6(K7(COMPLEX,COMPLEX)) is set

K7(COMPLEX,REAL) is set

K6(K7(COMPLEX,REAL)) is set

K537() is non empty V114() L10()

the carrier of K537() is non empty set

K542() is non empty V114() V211() V212() V213() V215() V241() V242() V243() V244() V245() V246() L10()

K543() is non empty V114() V213() V215() V244() V245() V246() M23(K542())

K544() is non empty V114() V211() V213() V215() V244() V245() V246() V247() M26(K542(),K543())

K546() is non empty V114() V211() V213() V215() L10()

K547() is non empty V114() V211() V213() V215() V247() M23(K546())

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

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

K7(RAT,RAT) is set

K6(K7(RAT,RAT)) is set

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

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

K7(INT,INT) is set

K6(K7(INT,INT)) is set

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

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

K7(NAT,NAT) is set

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

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

{} is empty V146() V147() V148() V149() V150() V151() V152() set

K608(RealSpace) is TopStruct

the carrier of R^1 is non empty V146() V147() V148() set

K6( the carrier of R^1) is set

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

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

the carrier of I[01] is non empty V146() V147() V148() set

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

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

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

K6(K7( the carrier of (TOP-REAL 2), 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))

0[01] is V11() real ext-real Element of the carrier of I[01]

(#) (0,1) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

1[01] is V11() real ext-real Element of the carrier of I[01]

(0,1) (#) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

[.0,1.] is V146() V147() V148() Element of K6(REAL)

C is V11() real ext-real set

r is V11() real ext-real set

C + r is V11() real ext-real set

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

C is non empty TopSpace-like TopStruct

the carrier of C is non empty set

K6( the carrier of C) is set

r is Element of K6( the carrier of C)

C | r is strict TopSpace-like SubSpace of C

the carrier of (C | r) is set

K6( the carrier of (C | r)) is set

x is Element of K6( the carrier of (C | r))

fs is Element of K6( the carrier of C)

fs /\ r is Element of K6( the carrier of C)

[#] (C | r) is non proper closed Element of K6( the carrier of (C | r))

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

K6( the carrier of r) is set

C is non empty TopSpace-like TopStruct

the carrier of C is non empty set

K7( the carrier of C, the carrier of r) is set

K6(K7( the carrier of C, the carrier of r)) is set

x is non empty Element of K6( the carrier of r)

r | x is non empty strict TopSpace-like SubSpace of r

the carrier of (r | x) is non empty set

K7( the carrier of C, the carrier of (r | x)) is set

K6(K7( the carrier of C, the carrier of (r | x))) is set

fs is non empty V22() V25( the carrier of C) V26( the carrier of (r | x)) Function-like total quasi_total Element of K6(K7( the carrier of C, the carrier of (r | x)))

[#] (r | x) is non empty non proper closed Element of K6( the carrier of (r | x))

K6( the carrier of (r | x)) is set

P29 is non empty V22() V25( the carrier of C) V26( the carrier of r) Function-like total quasi_total Element of K6(K7( the carrier of C, the carrier of r))

f is Element of K6( the carrier of r)

P29 " f is Element of K6( the carrier of C)

K6( the carrier of C) is set

f /\ x is Element of K6( the carrier of r)

f1 is Element of K6( the carrier of (r | x))

P29 " x is Element of K6( the carrier of C)

dom P29 is Element of K6( the carrier of C)

(P29 " f) /\ (P29 " x) is Element of K6( the carrier of C)

fs " f1 is Element of K6( the carrier of C)

C is V11() real ext-real set

{ b

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

Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)

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

{ b

x is set

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

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

x is set

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

{ b

x is set

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

fs /. 1 is V11() real ext-real Element of REAL

x is set

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs /. 1 is V11() real ext-real Element of REAL

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

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

C is V11() real ext-real set

{ b

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

Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)

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

{ b

x is set

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

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

x is set

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

{ b

x is set

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

fs /. 1 is V11() real ext-real Element of REAL

x is set

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs /. 1 is V11() real ext-real Element of REAL

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

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

C is V11() real ext-real set

{ b

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

{ b

{ b

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

{ b

{ b

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

x /\ fs is Element of K6( the carrier of (TOP-REAL 2))

P29 is set

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

P29 is set

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

C is V11() real ext-real set

{ b

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

Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)

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

{ b

x is set

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

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

x is set

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

{ b

x is set

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

x is set

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

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

C is V11() real ext-real set

{ b

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

Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)

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

{ b

x is set

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

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

x is set

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

{ b

x is set

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

x is set

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

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

C is V11() real ext-real set

{ b

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

{ b

{ b

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

{ b

{ b

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

x /\ fs is Element of K6( the carrier of (TOP-REAL 2))

P29 is set

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

P29 is set

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

C is natural V11() real ext-real V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT

TOP-REAL C is non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() RLTopStruct

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

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

r is Element of K6( the carrier of (TOP-REAL C))

x is V22() V26( REAL ) Function-like V43(C) FinSequence-like V138() Element of the carrier of (TOP-REAL C)

fs is V22() V26( REAL ) Function-like V43(C) FinSequence-like V138() Element of the carrier of (TOP-REAL C)

(TOP-REAL C) | r is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL C

the carrier of ((TOP-REAL C) | r) is set

K7( the carrier of I[01], the carrier of ((TOP-REAL C) | r)) is set

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

P29 is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL C) | r)) Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL C) | r)))

P29 . 0 is set

P29 . 1 is set

f is non empty Element of K6( the carrier of (TOP-REAL C))

(TOP-REAL C) | f is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL C

the carrier of ((TOP-REAL C) | f) is non empty set

K7( the carrier of I[01], the carrier of ((TOP-REAL C) | f)) is set

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

[#] I[01] is non empty non proper closed V146() V147() V148() Element of K6( the carrier of I[01])

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

rng P29 is Element of K6( the carrier of ((TOP-REAL C) | r))

K6( the carrier of ((TOP-REAL C) | r)) is set

[#] ((TOP-REAL C) | r) is non proper closed Element of K6( the carrier of ((TOP-REAL C) | r))

dom P29 is V146() V147() V148() Element of K6( the carrier of I[01])

P29 .: ([#] I[01]) is Element of K6( the carrier of ((TOP-REAL C) | r))

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

(r `1) + (x `1) is V11() real ext-real Element of REAL

((r `1) + (x `1)) / 2 is V11() real ext-real Element of REAL

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

(TOP-REAL 2) | fs is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

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

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

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

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

P29 . 0 is set

P29 . 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))

Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)

(TOP-REAL 2) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

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

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

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

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

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

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

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

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

f * P29 is V22() V25( the carrier of I[01]) V26( the carrier of R^1) Function-like Element of K6(K7( the carrier of I[01], the carrier of R^1))

dom P29 is V146() V147() V148() Element of K6( the carrier of I[01])

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

f2 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))

f2 . 0 is set

f . (P29 . 0) is set

r /. 1 is V11() real ext-real Element of REAL

f2 . 1 is set

f . (P29 . 1) is set

x /. 1 is V11() real ext-real Element of REAL

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

f2 . proj11 is set

P29 . proj11 is set

f . (P29 . proj11) is set

proj12 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

proj12 /. 1 is V11() real ext-real Element of REAL

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

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

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

C /\ r is Element of K6( the carrier of (TOP-REAL 2))

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

(x `1) + (fs `1) is V11() real ext-real Element of REAL

((x `1) + (fs `1)) / 2 is V11() real ext-real Element of REAL

{ b

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

Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)

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

(TOP-REAL 2) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

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

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

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

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

(TOP-REAL 2) | f1 is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

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

f | C is V22() 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))

dom (f | C) is Element of K6( the carrier of (TOP-REAL 2))

the carrier of (TOP-REAL 2) /\ C is Element of K6( the carrier of (TOP-REAL 2))

rng (f | C) is V146() V147() V148() Element of K6( the carrier of R^1)

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

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

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

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

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

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

proj12 is Element of the carrier of ((TOP-REAL 2) | C)

proj11 . proj12 is set

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

x /. 1 is V11() real ext-real Element of REAL

g1 is Element of the carrier of ((TOP-REAL 2) | C)

proj11 . g1 is set

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

fs /. 1 is V11() real ext-real Element of REAL

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

g is Element of the carrier of ((TOP-REAL 2) | C)

proj11 . g is set

f . g is set

P19 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

P19 /. 1 is V11() real ext-real Element of REAL

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

g is Element of the carrier of ((TOP-REAL 2) | C)

proj11 . g is set

f . g is set

P19 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

P19 /. 1 is V11() real ext-real Element of REAL

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

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

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

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

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

C /\ r is Element of K6( the carrier of (TOP-REAL 2))

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

(x `2) + (fs `2) is V11() real ext-real Element of REAL

((x `2) + (fs `2)) / 2 is V11() real ext-real Element of REAL

{ b

P29 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))

Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)

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

(TOP-REAL 2) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

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

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

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

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

(TOP-REAL 2) | f is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

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

P29 | C is V22() 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))

dom (P29 | C) is Element of K6( the carrier of (TOP-REAL 2))

the carrier of (TOP-REAL 2) /\ C is Element of K6( the carrier of (TOP-REAL 2))

rng (P29 | C) is V146() V147() V148() Element of K6( the carrier of R^1)

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

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

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

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

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

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

proj11 is Element of the carrier of ((TOP-REAL 2) | C)

f2 . proj11 is set

P29 . x is V11() real ext-real Element of the carrier of R^1

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

proj12 is Element of the carrier of ((TOP-REAL 2) | C)

f2 . proj12 is set

P29 . fs is V11() real ext-real Element of the carrier of R^1

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

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

g is Element of the carrier of ((TOP-REAL 2) | C)

f2 . g is set

P29 . g is set

P19 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

g is Element of the carrier of ((TOP-REAL 2) | C)

f2 . g is set

P29 . g is set

P19 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

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

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

(r `1) + (x `1) is V11() real ext-real Element of REAL

((r `1) + (x `1)) / 2 is V11() real ext-real Element of REAL

{ b

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

fs is set

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

First_Point (C,r,x,f) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

f is set

f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

First_Point (C,r,x,f) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

(r `2) + (x `2) is V11() real ext-real Element of REAL

((r `2) + (x `2)) / 2 is V11() real ext-real Element of REAL

{ b

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

fs is set

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

First_Point (C,r,x,f) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

f is set

f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

First_Point (C,r,x,f) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

(r `1) + (x `1) is V11() real ext-real Element of REAL

((r `1) + (x `1)) / 2 is V11() real ext-real Element of REAL

{ H

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

First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

C /\ fs is Element of K6( the carrier of (TOP-REAL 2))

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

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

(r `2) + (x `2) is V11() real ext-real Element of REAL

((r `2) + (x `2)) / 2 is V11() real ext-real Element of REAL

{ H

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

First_Point (C,r,x,P29) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

C /\ P29 is Element of K6( the carrier of (TOP-REAL 2))

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

(r `1) + (x `1) is V11() real ext-real Element of REAL

((r `1) + (x `1)) / 2 is V11() real ext-real Element of REAL

{ H

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

C /\ fs is Element of K6( the carrier of (TOP-REAL 2))

First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

{ b

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

First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

C /\ fs is Element of K6( the carrier of (TOP-REAL 2))

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

(r `2) + (x `2) is V11() real ext-real Element of REAL

((r `2) + (x `2)) / 2 is V11() real ext-real Element of REAL

{ H

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

C /\ fs is Element of K6( the carrier of (TOP-REAL 2))

First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

{ b

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

First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

C /\ fs is Element of K6( the carrier of (TOP-REAL 2))

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(TOP-REAL 2) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

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

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

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

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

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

f1 is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | C)) Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | C)))

f1 . 0 is set

f1 . 1 is set

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

f1 . f2 is set

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

f1 . proj11 is set

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

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

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

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

L[01] (((0,1) (#)),((#) (0,1))) is non empty V22() V25( the carrier of (Closed-Interval-TSpace (0,1))) V26( the carrier of (Closed-Interval-TSpace (0,1))) Function-like total quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))))

K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))) is set

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

f1 * (L[01] (((0,1) (#)),((#) (0,1)))) is V22() V25( the carrier of (Closed-Interval-TSpace (0,1))) V26( the carrier of ((TOP-REAL 2) | C)) Function-like Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | C)))

K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | C)) is set

K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | C))) is set

(L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

(L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

dom f1 is V146() V147() V148() Element of K6( the carrier of I[01])

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

[#] I[01] is non empty non proper closed V146() V147() V148() Element of K6( the carrier of I[01])

rng (L[01] (((0,1) (#)),((#) (0,1)))) is V146() V147() V148() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))

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

dom (f1 * (L[01] (((0,1) (#)),((#) (0,1))))) is V146() V147() V148() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))

dom (L[01] (((0,1) (#)),((#) (0,1)))) is V146() V147() V148() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))

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

(TOP-REAL 2) | f is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

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

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

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

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

dom g is V146() V147() V148() Element of K6( the carrier of I[01])

g . 0 is set

g . 1 is set

P19 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

(L[01] (((0,1) (#)),((#) (0,1)))) . P19 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

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

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

(1 - f2) * 0 is V11() real ext-real Element of REAL

((1 - (1 - f2)) * 1) + ((1 - f2) * 0) is V11() real ext-real Element of REAL

r1 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

(L[01] (((0,1) (#)),((#) (0,1)))) . r1 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

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

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

(1 - proj11) * 0 is V11() real ext-real Element of REAL

((1 - (1 - proj11)) * 1) + ((1 - proj11) * 0) is V11() real ext-real Element of REAL

g . (1 - f2) is set

g . (1 - proj11) is set

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

{ b

P29 is set

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

{ b

P29 is set

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))

{ b

P29 is set

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))

{ b

P29 is set

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x,r) is Element of K6( the carrier of (TOP-REAL 2))

{ b

{r} is non empty set

fs is set

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is set

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x,x) is Element of K6( the carrier of (TOP-REAL 2))

{ b

fs is set

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x,x) is Element of K6( the carrier of (TOP-REAL 2))

{ b

{x} is non empty set

fs is set

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is set

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x,r) is Element of K6( the carrier of (TOP-REAL 2))

{ b

fs is set

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))

{ b

(C,x,r,fs) is Element of K6( the carrier of (TOP-REAL 2))

{ b

P29 is set

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

P29 is set

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))

{ b

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x,P29) is Element of K6( the carrier of (TOP-REAL 2))

{ b

(C,r,x,fs) /\ (C,r,x,P29) is Element of K6( the carrier of (TOP-REAL 2))

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x,fs,P29) is Element of K6( the carrier of (TOP-REAL 2))

(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))

{ b

(C,r,x,P29) is Element of K6( the carrier of (TOP-REAL 2))

{ b

(C,r,x,fs) /\ (C,r,x,P29) is Element of K6( the carrier of (TOP-REAL 2))

{ b

f is set

f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

f2 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

f is set

f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))

{ b

(C,x,r,fs) is Element of K6( the carrier of (TOP-REAL 2))

{ b

P29 is set

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

P29 is set

f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(C,r,x,fs,P29) is Element of K6( the carrier of (TOP-REAL 2))

(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))

{ b

(C,r,x,P29) is Element of K6( the carrier of (TOP-REAL 2))

{ b

(C,r,x,fs) /\ (C,r,x,P29) is Element of K6( the carrier of (TOP-REAL 2))

(C,x,r,P29,fs) is Element of K6( the carrier of (TOP-REAL 2))

(C,x,r,P29) is Element of K6( the carrier of (TOP-REAL 2))

{ b

(C,x,r,fs) is Element of K6( the carrier of (TOP-REAL 2))

{ b

(C,x,r,P29) /\ (C,x,r,fs) is Element of K6( the carrier of (TOP-REAL 2))

C is V11() real ext-real set

{ b

r is set

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

{ b

r is set

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

C is V11() real ext-real set

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

{ b

r is V11() real ext-real set

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

{ b

C is V11() real ext-real set

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

{ b

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

C is V11() real ext-real set

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

{ b

r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

W-min C is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

W-bound C is V11() real ext-real Element of REAL

(TOP-REAL 2) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

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

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

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

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

lower_bound (proj1 | C) is V11() real ext-real Element of REAL

(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V146() V147() V148() Element of K6(REAL)

lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

W-most C is Element of K6( the carrier of (TOP-REAL 2))

SW-corner C is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

S-bound C is V11() real ext-real Element of REAL

proj2 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))

proj2 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))

lower_bound (proj2 | C) is V11() real ext-real Element of REAL

(proj2 | C) .: the carrier of ((TOP-REAL 2) | C) is V146() V147() V148() Element of K6(REAL)

lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(W-bound C),(S-bound C)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

NW-corner C is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

N-bound C is V11() real ext-real Element of REAL

upper_bound (proj2 | C) is V11() real ext-real Element of REAL

upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

|[(W-bound C),(N-bound C)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

LSeg ((SW-corner C),(NW-corner C)) is Element of K6( the carrier of (TOP-REAL 2))

(LSeg ((SW-corner C),(NW-corner C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (W-most C) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

proj2 | (W-most C) is V22() V25( the carrier of ((TOP-REAL 2) | (W-most C))) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL))

the carrier of ((TOP-REAL 2) | (W-most C)) is set

K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL) is set

K6(K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL)) is set

lower_bound (proj2 | (W-most C)) is V11() real ext-real Element of REAL

(proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C)) is V146() V147() V148() Element of K6(REAL)

lower_bound ((proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C))) is V11() real ext-real Element of REAL

|[(W-bound C),(lower_bound (proj2 | (W-most C)))]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

E-max C is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

E-bound C is V11() real ext-real Element of REAL

upper_bound (proj1 | C) is V11() real ext-real Element of REAL

upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL

E-most C is Element of K6( the carrier of (TOP-REAL 2))

SE-corner C is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

|[(E-bound C),(S-bound C)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

NE-corner C is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

|[(E-bound C),(N-bound C)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

LSeg ((SE-corner C),(NE-corner C)) is Element of K6( the carrier of (TOP-REAL 2))

(LSeg ((SE-corner C),(NE-corner C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (E-most C) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

proj2 | (E-most C) is V22() V25( the carrier of ((TOP-REAL 2) | (E-most C))) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL))

the carrier of ((TOP-REAL 2) | (E-most C)) is set

K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL) is set

K6(K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL)) is set

upper_bound (proj2 | (E-most C)) is V11() real ext-real Element of REAL

(proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C)) is V146() V147() V148() Element of K6(REAL)

upper_bound ((proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C))) is V11() real ext-real Element of REAL

|[(E-bound C),(upper_bound (proj2 | (E-most C)))]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

{(W-min C),(E-max C)} is non empty set

(W-bound C) + (E-bound C) is V11() real ext-real Element of REAL

((W-bound C) + (E-bound C)) / 2 is V11() real ext-real Element of REAL

((((W-bound C) + (E-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))

{ b

r is non empty closed compact being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))

W-min r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

W-bound r is V11() real ext-real Element of REAL

(TOP-REAL 2) | r is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

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

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

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

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

lower_bound (proj1 | r) is V11() real ext-real Element of REAL

(proj1 | r) .: the carrier of ((TOP-REAL 2) | r) is non empty V146() V147() V148() Element of K6(REAL)

lower_bound ((proj1 | r) .: the carrier of ((TOP-REAL 2) | r)) is V11() real ext-real Element of REAL

W-most r is Element of K6( the carrier of (TOP-REAL 2))

SW-corner r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

S-bound r is V11() real ext-real Element of REAL

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

lower_bound (proj2 | r) is V11() real ext-real Element of REAL

(proj2 | r) .: the carrier of ((TOP-REAL 2) | r) is non empty V146() V147() V148() Element of K6(REAL)

lower_bound ((proj2 | r) .: the carrier of ((TOP-REAL 2) | r)) is V11() real ext-real Element of REAL

|[(W-bound r),(S-bound r)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

NW-corner r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

N-bound r is V11() real ext-real Element of REAL

upper_bound (proj2 | r) is V11() real ext-real Element of REAL

upper_bound ((proj2 | r) .: the carrier of ((TOP-REAL 2) | r)) is V11() real ext-real Element of REAL

|[(W-bound r),(N-bound r)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

LSeg ((SW-corner r),(NW-corner r)) is Element of K6( the carrier of (TOP-REAL 2))

(LSeg ((SW-corner r),(NW-corner r))) /\ r is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (W-most r) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

proj2 | (W-most r) is V22() V25( the carrier of ((TOP-REAL 2) | (W-most r))) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most r)),REAL))

the carrier of ((TOP-REAL 2) | (W-most r)) is set

K7( the carrier of ((TOP-REAL 2) | (W-most r)),REAL) is set

K6(K7( the carrier of ((TOP-REAL 2) | (W-most r)),REAL)) is set

lower_bound (proj2 | (W-most r)) is V11() real ext-real Element of REAL

(proj2 | (W-most r)) .: the carrier of ((TOP-REAL 2) | (W-most r)) is V146() V147() V148() Element of K6(REAL)

lower_bound ((proj2 | (W-most r)) .: the carrier of ((TOP-REAL 2) | (W-most r))) is V11() real ext-real Element of REAL

|[(W-bound r),(lower_bound (proj2 | (W-most r)))]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

E-max r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

E-bound r is V11() real ext-real Element of REAL

upper_bound (proj1 | r) is V11() real ext-real Element of REAL

upper_bound ((proj1 | r) .: the carrier of ((TOP-REAL 2) | r)) is V11() real ext-real Element of REAL

E-most r is Element of K6( the carrier of (TOP-REAL 2))

SE-corner r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

|[(E-bound r),(S-bound r)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

NE-corner r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

|[(E-bound r),(N-bound r)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

LSeg ((SE-corner r),(NE-corner r)) is Element of K6( the carrier of (TOP-REAL 2))

(LSeg ((SE-corner r),(NE-corner r))) /\ r is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (E-most r) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

proj2 | (E-most r) is V22() V25( the carrier of ((TOP-REAL 2) | (E-most r))) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most r)),REAL))

the carrier of ((TOP-REAL 2) | (E-most r)) is set

K7( the carrier of ((TOP-REAL 2) | (E-most r)),REAL) is set

K6(K7( the carrier of ((TOP-REAL 2) | (E-most r)),REAL)) is set

upper_bound (proj2 | (E-most r)) is V11() real ext-real Element of REAL

(proj2 | (E-most r)) .: the carrier of ((TOP-REAL 2) | (E-most r)) is V146() V147() V148() Element of K6(REAL)

upper_bound ((proj2 | (E-most r)) .: the carrier of ((TOP-REAL 2) | (E-most r))) is V11() real ext-real Element of REAL

|[(E-bound r),(upper_bound (proj2 | (E-most r)))]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

{(W-min r),(E-max r)} is non empty set

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

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

x \/ fs is non empty Element of K6( the carrier of (TOP-REAL 2))

x /\ fs is Element of K6( the carrier of (TOP-REAL 2))

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

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

(E-max r) `1 is V11() real ext-real Element of REAL

(W-bound r) + (E-bound r) is V11() real ext-real Element of REAL

((W-bound r) + (E-bound r)) / 2 is V11() real ext-real Element of REAL

((((W-bound r) + (E-bound r)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))

{ b

P29 /\ ((((W-bound r) + (E-bound r)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))

f /\ ((((W-bound r) + (E-bound r)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))

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

(W-min r) `1 is V11() real ext-real Element of REAL

((W-min r) `1) + ((E-max r) `1) is V11() real ext-real Element of REAL

(((W-min r) `1) + ((E-max r) `1)) / 2 is V11() real ext-real Element of REAL

proj11 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

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

proj12 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

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

First_Point (P29,(W-min r),(E-max r),((((W-bound r) + (E-bound r)) / 2))) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(First_Point (P29,(W-min r),(E-max r),((((W-bound r) + (E-bound r)) / 2)))) `2 is V11() real ext-real Element of REAL

Last_Point (f,(E-max r),(W-min r),((((W-bound r) + (E-bound r)) / 2))) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)

(Last_Point (f,(E-max r),(W-min r),((((W-bound r) + (E-bound r)) / 2)))) `2 is V11() real ext-real Element of REAL

First_Point (P29,(W-min r),(E-max r),((