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
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= p1 } is set
{ b1 where b1 is V11() real ext-real Element of REAL : not p1 <= b1 } is set
{ b1 where b1 is V11() real ext-real Element of REAL : not p1 <= b1 } \/ { b1 where b1 is V11() real ext-real Element of REAL : not b1 <= p1 } is set
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
{ b1 where b1 is V11() real ext-real Element of REAL : not p1 <= b1 } /\ { b1 where b1 is V11() real ext-real Element of REAL : not b1 <= p1 } is set
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
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= p1 } /\ S is V166() V167() V168() Element of K6( the carrier of R^1)
p4 is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not p1 <= b1 } /\ S is V166() V167() V168() Element of K6( the carrier of R^1)
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
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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