:: TOPREAL5 semantic presentation

REAL is non empty V36() V166() V167() V168() V172() set

NAT is V166() V167() V168() V169() V170() V171() V172() Element of K6(REAL)

K6(REAL) is set

omega is V166() V167() V168() V169() V170() V171() V172() set

K6(omega) is set

K231() is non empty strict TopSpace-like V114() TopStruct

the carrier of K231() is non empty V166() V167() V168() set

1 is non empty natural V11() real ext-real positive V118() V119() V166() V167() V168() V169() V170() V171() 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 V118() V119() V166() V167() V168() V169() V170() V171() Element of NAT

K7(2,2) is set

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

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

K259() is V100() V114() L7()

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

K6(NAT) is set

COMPLEX is non empty V36() V166() V172() set

RAT is non empty V36() V166() V167() V168() V169() V172() set

INT is non empty V36() V166() V167() V168() V169() V170() V172() set

K6(K7(REAL,REAL)) is set

TOP-REAL 2 is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() V190() V226() V227() L15()

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 set

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

K7(COMPLEX,COMPLEX) is set

K6(K7(COMPLEX,COMPLEX)) is set

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

K541() is non empty V134() L10()

the carrier of K541() is non empty set

K546() is non empty V134() V206() V207() V208() V210() V236() V237() V238() V239() V240() V241() L10()

K547() is non empty V134() V208() V210() V239() V240() V241() M21(K546())

K548() is non empty V134() V206() V208() V210() V239() V240() V241() V242() M24(K546(),K547())

K550() is non empty V134() V206() V208() V210() L10()

K551() is non empty V134() V206() V208() V210() V242() M21(K550())

{} is empty V166() V167() V168() V169() V170() V171() V172() set

0 is empty natural V11() real ext-real V118() V119() V166() V167() V168() V169() V170() V171() V172() Element of NAT

[.0,1.] is V166() V167() V168() Element of K6(REAL)

K564(K259()) is TopStruct

the carrier of R^1 is non empty V166() V167() V168() set

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

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

the carrier of I[01] is non empty V166() V167() V168() set

K258() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total V33(K7(REAL,REAL), REAL ) Element of K6(K7(K7(REAL,REAL),REAL))

G7(REAL,K258()) is V100() L7()

proj1 is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like total V33( the carrier of (TOP-REAL 2), REAL ) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

proj2 is non empty Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like total V33( the carrier of (TOP-REAL 2), REAL ) Element of K6(K7( the carrier of (TOP-REAL 2),REAL))

K6( the carrier of R^1) is set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

p1 is non empty TopSpace-like TopStruct

the carrier of p1 is non empty set

K7( the carrier of S, the carrier of p1) is set

K6(K7( the carrier of S, the carrier of p1)) is set

p1 is non empty TopSpace-like TopStruct

the carrier of p1 is non empty set

K7( the carrier of p1, the carrier of p1) is set

K6(K7( the carrier of p1, the carrier of p1)) is set

p2 is non empty Relation-like the carrier of S -defined the carrier of p1 -valued Function-like total V33( the carrier of S, the carrier of p1) continuous Element of K6(K7( the carrier of S, the carrier of p1))

P1 is non empty Relation-like the carrier of p1 -defined the carrier of p1 -valued Function-like total V33( the carrier of p1, the carrier of p1) continuous Element of K6(K7( the carrier of p1, the carrier of p1))

P1 * p2 is non empty Relation-like the carrier of S -defined the carrier of S -defined the carrier of p1 -valued the carrier of p1 -valued Function-like total total V33( the carrier of S, the carrier of p1) V33( the carrier of S, the carrier of p1) continuous Element of K6(K7( the carrier of S, the carrier of p1))

K7( the carrier of S, the carrier of p1) is set

K6(K7( the carrier of S, the carrier of p1)) is set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

K6( the carrier of S) is set

p1 is Element of K6( the carrier of S)

p2 is Element of K6( the carrier of S)

p1 is Element of K6( the carrier of S)

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

p1 /\ p1 is Element of K6( the carrier of S)

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

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

P1 is Element of K6( the carrier of S)

P2 is Element of K6( the carrier of S)

P1 \/ P2 is Element of K6( the carrier of S)

{} S is empty closed V166() V167() V168() V169() V170() V171() V172() Element of K6( the carrier of S)

f2 is Element of K6( the carrier of S)

g2 is Element of K6( the carrier of S)

f2 \/ g2 is Element of K6( the carrier of S)

f2 is Element of K6( the carrier of S)

g2 is Element of K6( the carrier of S)

f2 \/ g2 is Element of K6( the carrier of S)

S is V11() real ext-real set

p1 is V11() real ext-real set

Closed-Interval-TSpace (S,p1) is non empty strict TopSpace-like V114() SubSpace of R^1

[#] (Closed-Interval-TSpace (S,p1)) is non empty non proper closed V166() V167() V168() Element of K6( the carrier of (Closed-Interval-TSpace (S,p1)))

the carrier of (Closed-Interval-TSpace (S,p1)) is non empty V166() V167() V168() set

K6( the carrier of (Closed-Interval-TSpace (S,p1))) is set

S is V166() V167() V168() Element of K6( the carrier of R^1)

p1 is V11() real ext-real set

p1 is V11() real ext-real set

p2 is V11() real ext-real set

p1 is V11() real ext-real set

p2 is V11() real ext-real set

{ b

{ b

{ b

f2 is set

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

f2 is set

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

g2 is set

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

{ b

r2 is set

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

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

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

{ b

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

{ b

g2 is V166() V167() V168() Element of K6( the carrier of R^1)

f2 is V166() V167() V168() Element of K6( the carrier of R^1)

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

K7( the carrier of S, the carrier of R^1) is set

K6(K7( the carrier of S, the carrier of R^1)) is set

p1 is Element of the carrier of S

p1 is Element of the carrier of S

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

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

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

f2 is non empty Relation-like the carrier of S -defined the carrier of R^1 -valued Function-like total V33( the carrier of S, the carrier of R^1) continuous Element of K6(K7( the carrier of S, the carrier of R^1))

f2 . p1 is set

f2 . p1 is set

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

K6( the carrier of S) is set

f2 .: ([#] S) is V166() V167() V168() Element of K6( the carrier of R^1)

g2 is set

f2 . g2 is set

dom f2 is Element of K6( the carrier of S)

g2 is Element of the carrier of S

f2 . g2 is set

g2 is Element of the carrier of S

f2 . g2 is set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

K6( the carrier of S) is set

K7( the carrier of S, the carrier of R^1) is set

K6(K7( the carrier of S, the carrier of R^1)) is set

p1 is Element of the carrier of S

p1 is Element of the carrier of S

p2 is Element of K6( the carrier of S)

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

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

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

g2 is non empty Relation-like the carrier of S -defined the carrier of R^1 -valued Function-like total V33( the carrier of S, the carrier of R^1) continuous Element of K6(K7( the carrier of S, the carrier of R^1))

g2 . p1 is set

g2 . p1 is set

g2 .: p2 is V166() V167() V168() Element of K6( the carrier of R^1)

r2 is set

g2 . r2 is set

dom g2 is Element of K6( the carrier of S)

r2 is Element of the carrier of S

g2 . r2 is set

r2 is Element of the carrier of S

g2 . r2 is set

S is V11() real ext-real set

p1 is V11() real ext-real set

Closed-Interval-TSpace (S,p1) is non empty strict TopSpace-like V114() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (S,p1)) is non empty V166() V167() V168() set

K7( the carrier of (Closed-Interval-TSpace (S,p1)), the carrier of R^1) is set

K6(K7( the carrier of (Closed-Interval-TSpace (S,p1)), the carrier of R^1)) is set

p1 is V11() real ext-real set

p2 is V11() real ext-real set

P1 is non empty Relation-like the carrier of (Closed-Interval-TSpace (S,p1)) -defined the carrier of R^1 -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (S,p1)), the carrier of R^1) continuous Element of K6(K7( the carrier of (Closed-Interval-TSpace (S,p1)), the carrier of R^1))

P1 . S is set

P1 . p1 is set

P2 is V11() real ext-real set

[#] (Closed-Interval-TSpace (S,p1)) is non empty non proper closed V166() V167() V168() Element of K6( the carrier of (Closed-Interval-TSpace (S,p1)))

K6( the carrier of (Closed-Interval-TSpace (S,p1))) is set

P1 .: ([#] (Closed-Interval-TSpace (S,p1))) is V166() V167() V168() Element of K6( the carrier of R^1)

dom P1 is V166() V167() V168() Element of K6( the carrier of (Closed-Interval-TSpace (S,p1)))

[.S,p1.] is V166() V167() V168() Element of K6(REAL)

g2 is set

P1 . g2 is set

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

f2 is V166() V167() V168() Element of K6( the carrier of R^1)

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

P1 . f2 is set

S is V11() real ext-real set

p1 is V11() real ext-real set

Closed-Interval-TSpace (S,p1) is non empty strict TopSpace-like V114() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (S,p1)) is non empty V166() V167() V168() set

K7( the carrier of (Closed-Interval-TSpace (S,p1)), the carrier of R^1) is set

K6(K7( the carrier of (Closed-Interval-TSpace (S,p1)), the carrier of R^1)) is set

p1 is V11() real ext-real set

p2 is V11() real ext-real set

[.S,p1.] is V166() V167() V168() Element of K6(REAL)

P1 is non empty Relation-like the carrier of (Closed-Interval-TSpace (S,p1)) -defined the carrier of R^1 -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (S,p1)), the carrier of R^1) continuous Element of K6(K7( the carrier of (Closed-Interval-TSpace (S,p1)), the carrier of R^1))

P1 . S is set

P1 . p1 is set

P2 is V11() real ext-real set

dom P1 is V166() V167() V168() Element of K6( the carrier of (Closed-Interval-TSpace (S,p1)))

K6( the carrier of (Closed-Interval-TSpace (S,p1))) is set

[#] (Closed-Interval-TSpace (S,p1)) is non empty non proper closed V166() V167() V168() Element of K6( the carrier of (Closed-Interval-TSpace (S,p1)))

P1 .: ([#] (Closed-Interval-TSpace (S,p1))) is V166() V167() V168() Element of K6( the carrier of R^1)

f2 is set

P1 . f2 is set

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

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

P1 . f2 is set

S is V11() real ext-real set

p1 is V11() real ext-real set

Closed-Interval-TSpace (S,p1) is non empty strict TopSpace-like V114() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (S,p1)) is non empty V166() V167() V168() set

K7( the carrier of (Closed-Interval-TSpace (S,p1)), the carrier of R^1) is set

K6(K7( the carrier of (Closed-Interval-TSpace (S,p1)), the carrier of R^1)) is set

p1 is non empty Relation-like the carrier of (Closed-Interval-TSpace (S,p1)) -defined the carrier of R^1 -valued Function-like total V33( the carrier of (Closed-Interval-TSpace (S,p1)), the carrier of R^1) continuous Element of K6(K7( the carrier of (Closed-Interval-TSpace (S,p1)), the carrier of R^1))

p1 . S is set

p1 . p1 is set

p2 is V11() real ext-real set

P1 is V11() real ext-real set

p2 * P1 is V11() real ext-real 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

S is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like total V33( the carrier of I[01], the carrier of R^1) Element of K6(K7( the carrier of I[01], the carrier of R^1))

S . 0 is set

S . 1 is set

p1 is V11() real ext-real set

p1 is V11() real ext-real set

p1 + p1 is V11() real ext-real set

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

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

S . p2 is set

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

S . P1 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

S is non empty Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like total V33( the carrier of (TOP-REAL 2), the carrier of R^1) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))

Seg 2 is V166() V167() V168() V169() V170() V171() Element of K6(NAT)

p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

S . p1 is set

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

S is non empty Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like total V33( the carrier of (TOP-REAL 2), the carrier of R^1) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))

Seg 2 is V166() V167() V168() V169() V170() V171() Element of K6(NAT)

p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

S . p1 is set

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

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

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

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

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

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

p1 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p1) -valued Function-like total V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | p1)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p1)))

proj1 | p1 is non empty Relation-like the carrier of ((TOP-REAL 2) | p1) -defined REAL -valued Function-like total V33( the carrier of ((TOP-REAL 2) | p1), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | p1),REAL))

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

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

(proj1 | p1) * p1 is non empty Relation-like the carrier of I[01] -defined REAL -valued Function-like total V33( the carrier of I[01], REAL ) Element of K6(K7( the carrier of I[01],REAL))

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

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

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

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

p2 is Relation-like Function-like set

rng p2 is set

S is non empty Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like total V33( the carrier of (TOP-REAL 2), the carrier of R^1) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))

S | ((TOP-REAL 2) | p1) is non empty Relation-like the carrier of ((TOP-REAL 2) | p1) -defined the carrier of R^1 -valued Function-like total V33( the carrier of ((TOP-REAL 2) | p1), the carrier of R^1) Element of K6(K7( the carrier of ((TOP-REAL 2) | p1), the carrier of R^1))

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

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

S | p1 is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))

P2 is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like total V33( the carrier of I[01], the carrier of R^1) continuous Element of K6(K7( the carrier of I[01], the carrier of R^1))

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

p1 . f2 is set

P2 . f2 is set

g2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

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

dom p2 is set

p2 . f2 is set

(dom proj1) /\ p1 is Element of K6( the carrier of (TOP-REAL 2))

(proj1 | p1) . g2 is set

proj1 . g2 is set

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

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

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

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

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

p1 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p1) -valued Function-like total V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | p1)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p1)))

proj2 | p1 is non empty Relation-like the carrier of ((TOP-REAL 2) | p1) -defined REAL -valued Function-like total V33( the carrier of ((TOP-REAL 2) | p1), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | p1),REAL))

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

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

(proj2 | p1) * p1 is non empty Relation-like the carrier of I[01] -defined REAL -valued Function-like total V33( the carrier of I[01], REAL ) Element of K6(K7( the carrier of I[01],REAL))

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

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

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

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

p2 is Relation-like Function-like set

rng p2 is set

S is non empty Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like total V33( the carrier of (TOP-REAL 2), the carrier of R^1) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))

S | ((TOP-REAL 2) | p1) is non empty Relation-like the carrier of ((TOP-REAL 2) | p1) -defined the carrier of R^1 -valued Function-like total V33( the carrier of ((TOP-REAL 2) | p1), the carrier of R^1) Element of K6(K7( the carrier of ((TOP-REAL 2) | p1), the carrier of R^1))

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

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

S | p1 is Relation-like the carrier of (TOP-REAL 2) -defined the carrier of R^1 -valued Function-like Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))

P2 is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like total V33( the carrier of I[01], the carrier of R^1) continuous Element of K6(K7( the carrier of I[01], the carrier of R^1))

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

p1 . f2 is set

P2 . f2 is set

g2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

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

dom p2 is set

p2 . f2 is set

(dom proj2) /\ p1 is Element of K6( the carrier of (TOP-REAL 2))

(proj2 | p1) . g2 is set

proj2 . g2 is set

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

].0,1.[ is V166() V167() V168() Element of K6(REAL)

{0,1} is non empty V166() V167() V168() V169() V170() V171() set

].0,1.[ \/ {0,1} is non empty V166() V167() V168() set

p1 is V11() real ext-real set

p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

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

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

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

{p1,p2} is non empty set

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

p2 `2 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

|[(p2 `1),(p2 `2)]| is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

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

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

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

f2 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P2) -valued Function-like total V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | P2)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P2)))

f2 . 0 is set

f2 . 1 is set

g2 is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like total V33( the carrier of I[01], the carrier of R^1) Element of K6(K7( the carrier of I[01], the carrier of R^1))

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

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

g2 . 1 is set

g2 . 0 is set

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

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

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

g2 . r2 is set

{ b

dom f2 is V166() V167() V168() Element of K6( the carrier of I[01])

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

f2 . r2 is set

rng f2 is Element of K6( the carrier of ((TOP-REAL 2) | P2))

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

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

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

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

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

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

f1 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P1) -valued Function-like total V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | P1)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P1)))

f1 . 0 is set

f1 . 1 is set

g1 is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like total V33( the carrier of I[01], the carrier of R^1) Element of K6(K7( the carrier of I[01], the carrier of R^1))

g1 . 1 is set

g1 . 0 is set

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

g1 . r1 is set

dom f1 is V166() V167() V168() Element of K6( the carrier of I[01])

f1 . r1 is set

rng f1 is Element of K6( the carrier of ((TOP-REAL 2) | P1))

p3 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

p4 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

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

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

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

(1 / 2) * p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p1,(1 / 2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

(1 / 2) * p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p2,(1 / 2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((1 / 2) * p1) + ((1 / 2) * p2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K520(((1 / 2) * p1),((1 / 2) * p2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

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

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

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

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

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

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

((1 / 2) * p1) + ((1 / 2) * p1) is V11() real ext-real Element of REAL

2 " is V11() real ext-real positive Element of REAL

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

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

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

(2 ") * p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p1,(2 ")) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

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

(((2 ") * p1) `1) + ((2 ") * (p2 `1)) is V11() real ext-real Element of REAL

(2 ") * p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p2,(2 ")) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

(((2 ") * p1) `1) + (((2 ") * p2) `1) is V11() real ext-real Element of REAL

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

1 * p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p1,1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

(1 * p1) - ((1 / 2) * p1) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K524((1 * p1),((1 / 2) * p1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

(((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p1) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K524((((1 / 2) * p1) + ((1 / 2) * p2)),((1 / 2) * p1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((1 / 2) * p1) - ((1 / 2) * p1) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K524(((1 / 2) * p1),((1 / 2) * p1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((1 / 2) * p2) + (((1 / 2) * p1) - ((1 / 2) * p1)) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K520(((1 / 2) * p2),(((1 / 2) * p1) - ((1 / 2) * p1))) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

0. (TOP-REAL 2) is Relation-like REAL -valued Function-like V43(2) V52( TOP-REAL 2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

((1 / 2) * p2) + (0. (TOP-REAL 2)) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K520(((1 / 2) * p2),(0. (TOP-REAL 2))) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

(1 - (1 / 2)) * p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p1,(1 - (1 / 2))) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

(1 / 2) * p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p1,(1 / 2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

(1 / 2) * p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p2,(1 / 2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((1 / 2) * p1) + ((1 / 2) * p2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K520(((1 / 2) * p1),((1 / 2) * p2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

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

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

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

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

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

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

((1 / 2) * p1) + ((1 / 2) * p1) is V11() real ext-real Element of REAL

2 " is V11() real ext-real positive Element of REAL

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

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

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

(2 ") * p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p1,(2 ")) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

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

(((2 ") * p1) `1) + ((2 ") * (p2 `1)) is V11() real ext-real Element of REAL

(2 ") * p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p2,(2 ")) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

(((2 ") * p1) `1) + (((2 ") * p2) `1) is V11() real ext-real Element of REAL

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

1 * p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p2,1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

(1 * p2) - ((1 / 2) * p2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K524((1 * p2),((1 / 2) * p2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

(((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K524((((1 / 2) * p1) + ((1 / 2) * p2)),((1 / 2) * p2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((1 / 2) * p2) - ((1 / 2) * p2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K524(((1 / 2) * p2),((1 / 2) * p2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((1 / 2) * p1) + (((1 / 2) * p2) - ((1 / 2) * p2)) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K520(((1 / 2) * p1),(((1 / 2) * p2) - ((1 / 2) * p2))) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

0. (TOP-REAL 2) is Relation-like REAL -valued Function-like V43(2) V52( TOP-REAL 2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

((1 / 2) * p1) + (0. (TOP-REAL 2)) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K520(((1 / 2) * p1),(0. (TOP-REAL 2))) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

(1 - (1 / 2)) * p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p2,(1 - (1 / 2))) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

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

].0,1.[ is V166() V167() V168() Element of K6(REAL)

{0,1} is non empty V166() V167() V168() V169() V170() V171() set

].0,1.[ \/ {0,1} is non empty V166() V167() V168() set

p1 is V11() real ext-real set

p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

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

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

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

{p1,p2} is non empty set

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

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

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

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

|[(p2 `1),(p2 `2)]| is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

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

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

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

f2 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P2) -valued Function-like total V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | P2)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P2)))

f2 . 0 is set

f2 . 1 is set

g2 is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like total V33( the carrier of I[01], the carrier of R^1) Element of K6(K7( the carrier of I[01], the carrier of R^1))

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

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

g2 . 1 is set

g2 . 0 is set

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

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

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

g2 . r2 is set

{ b

dom f2 is V166() V167() V168() Element of K6( the carrier of I[01])

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

f2 . r2 is set

rng f2 is Element of K6( the carrier of ((TOP-REAL 2) | P2))

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

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

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

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

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

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

f1 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P1) -valued Function-like total V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | P1)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P1)))

f1 . 0 is set

f1 . 1 is set

g1 is non empty Relation-like the carrier of I[01] -defined the carrier of R^1 -valued Function-like total V33( the carrier of I[01], the carrier of R^1) Element of K6(K7( the carrier of I[01], the carrier of R^1))

g1 . 1 is set

g1 . 0 is set

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

g1 . r1 is set

dom f1 is V166() V167() V168() Element of K6( the carrier of I[01])

f1 . r1 is set

rng f1 is Element of K6( the carrier of ((TOP-REAL 2) | P1))

p3 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

p4 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

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

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

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

(1 / 2) * p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p1,(1 / 2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

(1 / 2) * p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p2,(1 / 2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((1 / 2) * p1) + ((1 / 2) * p2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K520(((1 / 2) * p1),((1 / 2) * p2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

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

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

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

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

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

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

((1 / 2) * p1) + ((1 / 2) * p1) is V11() real ext-real Element of REAL

2 " is V11() real ext-real positive Element of REAL

(2 ") * (p1 `2) is V11() real ext-real Element of REAL

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

((2 ") * (p1 `2)) + ((p2 `2) / 2) is V11() real ext-real Element of REAL

(2 ") * p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p1,(2 ")) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((2 ") * p1) `2 is V11() real ext-real Element of REAL

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

(((2 ") * p1) `2) + ((2 ") * (p2 `2)) is V11() real ext-real Element of REAL

(2 ") * p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p2,(2 ")) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

(((2 ") * p1) `2) + (((2 ") * p2) `2) is V11() real ext-real Element of REAL

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

1 * p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p1,1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

(1 * p1) - ((1 / 2) * p1) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K524((1 * p1),((1 / 2) * p1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

(((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p1) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K524((((1 / 2) * p1) + ((1 / 2) * p2)),((1 / 2) * p1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((1 / 2) * p1) - ((1 / 2) * p1) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K524(((1 / 2) * p1),((1 / 2) * p1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((1 / 2) * p2) + (((1 / 2) * p1) - ((1 / 2) * p1)) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K520(((1 / 2) * p2),(((1 / 2) * p1) - ((1 / 2) * p1))) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

0. (TOP-REAL 2) is Relation-like REAL -valued Function-like V43(2) V52( TOP-REAL 2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

((1 / 2) * p2) + (0. (TOP-REAL 2)) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K520(((1 / 2) * p2),(0. (TOP-REAL 2))) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

(1 - (1 / 2)) * p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p1,(1 - (1 / 2))) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

(1 / 2) * p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p1,(1 / 2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

(1 / 2) * p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p2,(1 / 2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((1 / 2) * p1) + ((1 / 2) * p2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K520(((1 / 2) * p1),((1 / 2) * p2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

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

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

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

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

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

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

((1 / 2) * p1) + ((1 / 2) * p1) is V11() real ext-real Element of REAL

2 " is V11() real ext-real positive Element of REAL

(2 ") * (p1 `2) is V11() real ext-real Element of REAL

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

((2 ") * (p1 `2)) + ((p2 `2) / 2) is V11() real ext-real Element of REAL

(2 ") * p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p1,(2 ")) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((2 ") * p1) `2 is V11() real ext-real Element of REAL

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

(((2 ") * p1) `2) + ((2 ") * (p2 `2)) is V11() real ext-real Element of REAL

(2 ") * p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p2,(2 ")) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

(((2 ") * p1) `2) + (((2 ") * p2) `2) is V11() real ext-real Element of REAL

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

1 * p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p2,1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

(1 * p2) - ((1 / 2) * p2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K524((1 * p2),((1 / 2) * p2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

(((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K524((((1 / 2) * p1) + ((1 / 2) * p2)),((1 / 2) * p2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((1 / 2) * p2) - ((1 / 2) * p2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K524(((1 / 2) * p2),((1 / 2) * p2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

((1 / 2) * p1) + (((1 / 2) * p2) - ((1 / 2) * p2)) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K520(((1 / 2) * p1),(((1 / 2) * p2) - ((1 / 2) * p2))) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

0. (TOP-REAL 2) is Relation-like REAL -valued Function-like V43(2) V52( TOP-REAL 2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

((1 / 2) * p1) + (0. (TOP-REAL 2)) is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K520(((1 / 2) * p1),(0. (TOP-REAL 2))) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

(1 - (1 / 2)) * p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

K526(p2,(1 - (1 / 2))) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

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

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

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

p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

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

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

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

p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

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

S-min S is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

N-max S is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

(TOP-REAL 2) | (S-most S) is strict TopSpace-like SubSpace of TOP-REAL 2

proj1 | (S-most S) is Relation-like the carrier of ((TOP-REAL 2) | (S-most S)) -defined REAL -valued Function-like total V33( the carrier of ((TOP-REAL 2) | (S-most S)), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (S-most S)),REAL))

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

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

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

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

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

|[(lower_bound (proj1 | (S-most S))),(S-bound S)]| is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

N-most S is Element of K6( the carrier of (TOP-REAL 2))

(TOP-REAL 2) | (N-most S) is strict TopSpace-like SubSpace of TOP-REAL 2

proj1 | (N-most S) is Relation-like the carrier of ((TOP-REAL 2) | (N-most S)) -defined REAL -valued Function-like total V33( the carrier of ((TOP-REAL 2) | (N-most S)), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (N-most S)),REAL))

the carrier of ((TOP-REAL 2) | (N-most S)) is set

K7( the carrier of ((TOP-REAL 2) | (N-most S)),REAL) is set

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

upper_bound (proj1 | (N-most S)) is V11() real ext-real Element of REAL

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

|[(upper_bound (proj1 | (N-most S))),(N-bound S)]| is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

W-min S is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

E-max S is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

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

(TOP-REAL 2) | (W-most S) is strict TopSpace-like SubSpace of TOP-REAL 2

proj2 | (W-most S) is Relation-like the carrier of ((TOP-REAL 2) | (W-most S)) -defined REAL -valued Function-like total V33( the carrier of ((TOP-REAL 2) | (W-most S)), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most S)),REAL))

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

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

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

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

|[(W-bound S),(lower_bound (proj2 | (W-most S)))]| is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

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

(TOP-REAL 2) | (E-most S) is strict TopSpace-like SubSpace of TOP-REAL 2

proj2 | (E-most S) is Relation-like the carrier of ((TOP-REAL 2) | (E-most S)) -defined REAL -valued Function-like total V33( the carrier of ((TOP-REAL 2) | (E-most S)), REAL ) Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most S)),REAL))

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

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

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

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

|[(E-bound S),(upper_bound (proj2 | (E-most S)))]| is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

p1 is set

p1 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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

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

p2 is Relation-like REAL -valued Function-like V43(2) FinSequence-like V158() Element of the carrier of (TOP-REAL 2)

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