REAL is non empty V36() V146() V147() V148() V152() V181() set
NAT is V146() V147() V148() V149() V150() V151() V152() V181() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V36() V146() V152() set
omega is V146() V147() V148() V149() V150() V151() V152() V181() set
K6(omega) is set
K6(NAT) is set
1 is non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
K7(1,1) is set
K6(K7(1,1)) is set
K7(K7(1,1),1) is set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
K7(2,2) is set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is set
RAT is non empty V36() V146() V147() V148() V149() V152() set
INT is non empty V36() V146() V147() V148() V149() V150() V152() set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() RLTopStruct
the carrier of (TOP-REAL 2) is non empty functional set
K6( the carrier of (TOP-REAL 2)) is set
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 compact V200() TopStruct
the carrier of I[01] is non empty V146() V147() V148() set
RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V200() MetrStruct
R^1 is non empty strict TopSpace-like V200() TopStruct
0 is empty natural V11() real ext-real non positive non negative V83() V84() V146() V147() V148() V149() V150() V151() V152() Element of NAT
the empty V146() V147() V148() V149() V150() V151() V152() set is empty V146() V147() V148() V149() V150() V151() V152() set
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V200() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (0,1)) is non empty V146() V147() V148() set
K7( the carrier of (TOP-REAL 2),REAL) is set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(COMPLEX,REAL) is set
K6(K7(COMPLEX,REAL)) is set
K537() is non empty V114() L10()
the carrier of K537() is non empty set
K542() is non empty V114() V211() V212() V213() V215() V241() V242() V243() V244() V245() V246() L10()
K543() is non empty V114() V213() V215() V244() V245() V246() M23(K542())
K544() is non empty V114() V211() V213() V215() V244() V245() V246() V247() M26(K542(),K543())
K546() is non empty V114() V211() V213() V215() L10()
K547() is non empty V114() V211() V213() V215() V247() M23(K546())
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is set
K7(K7(NAT,NAT),NAT) is set
K6(K7(K7(NAT,NAT),NAT)) is set
{} is empty V146() V147() V148() V149() V150() V151() V152() set
K608(RealSpace) is TopStruct
the carrier of R^1 is non empty V146() V147() V148() set
K6( the carrier of R^1) is set
real_dist is V22() V25(K7(REAL,REAL)) V26( REAL ) Function-like total quasi_total Element of K6(K7(K7(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 compact V200() SubSpace of R^1
the carrier of I[01] is non empty V146() V147() V148() set
K7( the carrier of I[01], the carrier of R^1) is set
K6(K7( the carrier of I[01], the carrier of R^1)) is set
K7( the carrier of (TOP-REAL 2), the carrier of R^1) is set
K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1)) is set
proj1 is non empty V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
0[01] is V11() real ext-real Element of the carrier of I[01]
(#) (0,1) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
1[01] is V11() real ext-real Element of the carrier of I[01]
(0,1) (#) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
[.0,1.] is V146() V147() V148() Element of K6(REAL)
C is V11() real ext-real set
r is V11() real ext-real set
C + r is V11() real ext-real set
(C + r) / 2 is V11() real ext-real Element of REAL
C is non empty TopSpace-like TopStruct
the carrier of C is non empty set
K6( the carrier of C) is set
r is Element of K6( the carrier of C)
C | r is strict TopSpace-like SubSpace of C
the carrier of (C | r) is set
K6( the carrier of (C | r)) is set
x is Element of K6( the carrier of (C | r))
fs is Element of K6( the carrier of C)
fs /\ r is Element of K6( the carrier of C)
[#] (C | r) is non proper closed Element of K6( the carrier of (C | r))
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
K6( the carrier of r) is set
C is non empty TopSpace-like TopStruct
the carrier of C is non empty set
K7( the carrier of C, the carrier of r) is set
K6(K7( the carrier of C, the carrier of r)) is set
x is non empty Element of K6( the carrier of r)
r | x is non empty strict TopSpace-like SubSpace of r
the carrier of (r | x) is non empty set
K7( the carrier of C, the carrier of (r | x)) is set
K6(K7( the carrier of C, the carrier of (r | x))) is set
fs is non empty V22() V25( the carrier of C) V26( the carrier of (r | x)) Function-like total quasi_total Element of K6(K7( the carrier of C, the carrier of (r | x)))
[#] (r | x) is non empty non proper closed Element of K6( the carrier of (r | x))
K6( the carrier of (r | x)) is set
P29 is non empty V22() V25( the carrier of C) V26( the carrier of r) Function-like total quasi_total Element of K6(K7( the carrier of C, the carrier of r))
f is Element of K6( the carrier of r)
P29 " f is Element of K6( the carrier of C)
K6( the carrier of C) is set
f /\ x is Element of K6( the carrier of r)
f1 is Element of K6( the carrier of (r | x))
P29 " x is Element of K6( the carrier of C)
dom P29 is Element of K6( the carrier of C)
(P29 " f) /\ (P29 " x) is Element of K6( the carrier of C)
fs " f1 is Element of K6( the carrier of C)
C is V11() real ext-real set
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : C <= b1 `1 } is set
r is Element of K6( the carrier of (TOP-REAL 2))
Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)
r ` is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : not C <= b1 `1 } is set
x is set
the carrier of (TOP-REAL 2) \ r is Element of K6( the carrier of (TOP-REAL 2))
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `1 is V11() real ext-real Element of REAL
x is set
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `1 is V11() real ext-real Element of REAL
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 `1 is V11() real ext-real Element of REAL
the carrier of (TOP-REAL 2) \ r is Element of K6( the carrier of (TOP-REAL 2))
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `1 is V11() real ext-real Element of REAL
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : not C <= b1 /. 1 } is set
x is set
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `1 is V11() real ext-real Element of REAL
fs /. 1 is V11() real ext-real Element of REAL
x is set
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs /. 1 is V11() real ext-real Element of REAL
fs `1 is V11() real ext-real Element of REAL
x is Element of K6( the carrier of (TOP-REAL 2))
C is V11() real ext-real set
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `1 <= C } is set
r is Element of K6( the carrier of (TOP-REAL 2))
Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)
r ` is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : not b1 `1 <= C } is set
x is set
the carrier of (TOP-REAL 2) \ r is Element of K6( the carrier of (TOP-REAL 2))
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `1 is V11() real ext-real Element of REAL
x is set
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `1 is V11() real ext-real Element of REAL
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 `1 is V11() real ext-real Element of REAL
the carrier of (TOP-REAL 2) \ r is Element of K6( the carrier of (TOP-REAL 2))
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `1 is V11() real ext-real Element of REAL
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : not b1 /. 1 <= C } is set
x is set
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `1 is V11() real ext-real Element of REAL
fs /. 1 is V11() real ext-real Element of REAL
x is set
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs /. 1 is V11() real ext-real Element of REAL
fs `1 is V11() real ext-real Element of REAL
x is Element of K6( the carrier of (TOP-REAL 2))
C is V11() real ext-real set
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `1 = C } is set
r is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : C <= b1 `1 } is set
x is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `1 <= C } is set
fs is Element of K6( the carrier of (TOP-REAL 2))
x /\ fs is Element of K6( the carrier of (TOP-REAL 2))
P29 is set
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f `1 is V11() real ext-real Element of REAL
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f `1 is V11() real ext-real Element of REAL
P29 is set
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f `1 is V11() real ext-real Element of REAL
f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f1 `1 is V11() real ext-real Element of REAL
C is V11() real ext-real set
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : C <= b1 `2 } is set
r is Element of K6( the carrier of (TOP-REAL 2))
Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)
r ` is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : not C <= b1 `2 } is set
x is set
the carrier of (TOP-REAL 2) \ r is Element of K6( the carrier of (TOP-REAL 2))
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `2 is V11() real ext-real Element of REAL
x is set
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `2 is V11() real ext-real Element of REAL
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 `2 is V11() real ext-real Element of REAL
the carrier of (TOP-REAL 2) \ r is Element of K6( the carrier of (TOP-REAL 2))
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `2 is V11() real ext-real Element of REAL
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : not C <= b1 /. 2 } is set
x is set
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `2 is V11() real ext-real Element of REAL
fs /. 2 is V11() real ext-real Element of REAL
x is set
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs /. 2 is V11() real ext-real Element of REAL
fs `2 is V11() real ext-real Element of REAL
x is Element of K6( the carrier of (TOP-REAL 2))
C is V11() real ext-real set
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `2 <= C } is set
r is Element of K6( the carrier of (TOP-REAL 2))
Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)
r ` is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : not b1 `2 <= C } is set
x is set
the carrier of (TOP-REAL 2) \ r is Element of K6( the carrier of (TOP-REAL 2))
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `2 is V11() real ext-real Element of REAL
x is set
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `2 is V11() real ext-real Element of REAL
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 `2 is V11() real ext-real Element of REAL
the carrier of (TOP-REAL 2) \ r is Element of K6( the carrier of (TOP-REAL 2))
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `2 is V11() real ext-real Element of REAL
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : not b1 /. 2 <= C } is set
x is set
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs `2 is V11() real ext-real Element of REAL
fs /. 2 is V11() real ext-real Element of REAL
x is set
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs /. 2 is V11() real ext-real Element of REAL
fs `2 is V11() real ext-real Element of REAL
x is Element of K6( the carrier of (TOP-REAL 2))
C is V11() real ext-real set
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `2 = C } is set
r is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : C <= b1 `2 } is set
x is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `2 <= C } is set
fs is Element of K6( the carrier of (TOP-REAL 2))
x /\ fs is Element of K6( the carrier of (TOP-REAL 2))
P29 is set
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f `2 is V11() real ext-real Element of REAL
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f `2 is V11() real ext-real Element of REAL
P29 is set
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f `2 is V11() real ext-real Element of REAL
f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f1 `2 is V11() real ext-real Element of REAL
C is natural V11() real ext-real V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
TOP-REAL C is non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() RLTopStruct
the carrier of (TOP-REAL C) is non empty functional set
K6( the carrier of (TOP-REAL C)) is set
r is Element of K6( the carrier of (TOP-REAL C))
x is V22() V26( REAL ) Function-like V43(C) FinSequence-like V138() Element of the carrier of (TOP-REAL C)
fs is V22() V26( REAL ) Function-like V43(C) FinSequence-like V138() Element of the carrier of (TOP-REAL C)
(TOP-REAL C) | r is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL C
the carrier of ((TOP-REAL C) | r) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL C) | r)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL C) | r))) is set
P29 is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL C) | r)) Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL C) | r)))
P29 . 0 is set
P29 . 1 is set
f is non empty Element of K6( the carrier of (TOP-REAL C))
(TOP-REAL C) | f is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL C
the carrier of ((TOP-REAL C) | f) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL C) | f)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL C) | f))) is set
[#] I[01] is non empty non proper closed V146() V147() V148() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
rng P29 is Element of K6( the carrier of ((TOP-REAL C) | r))
K6( the carrier of ((TOP-REAL C) | r)) is set
[#] ((TOP-REAL C) | r) is non proper closed Element of K6( the carrier of ((TOP-REAL C) | r))
dom P29 is V146() V147() V148() Element of K6( the carrier of I[01])
P29 .: ([#] I[01]) is Element of K6( the carrier of ((TOP-REAL C) | r))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C is Element of K6( the carrier of (TOP-REAL 2))
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
r `1 is V11() real ext-real Element of REAL
x `1 is V11() real ext-real Element of REAL
(r `1) + (x `1) is V11() real ext-real Element of REAL
((r `1) + (x `1)) / 2 is V11() real ext-real Element of REAL
fs is non empty Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | fs is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | fs) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | fs)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | fs))) is set
P29 is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | fs)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | fs)))
P29 . 0 is set
P29 . 1 is set
f is non empty V22() V25( the carrier of (TOP-REAL 2)) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))
Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)
(TOP-REAL 2) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | C) is set
[#] ((TOP-REAL 2) | C) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | C))
K6( the carrier of ((TOP-REAL 2) | C)) is set
K7( the carrier of I[01], the carrier of (TOP-REAL 2)) is set
K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2))) is set
f1 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (TOP-REAL 2)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
K7( the carrier of I[01], the carrier of R^1) is set
K6(K7( the carrier of I[01], the carrier of R^1)) is set
f * P29 is V22() V25( the carrier of I[01]) V26( the carrier of R^1) Function-like Element of K6(K7( the carrier of I[01], the carrier of R^1))
dom P29 is V146() V147() V148() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
f2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of R^1))
f2 . 0 is set
f . (P29 . 0) is set
r /. 1 is V11() real ext-real Element of REAL
f2 . 1 is set
f . (P29 . 1) is set
x /. 1 is V11() real ext-real Element of REAL
proj11 is V11() real ext-real Element of REAL
f2 . proj11 is set
P29 . proj11 is set
f . (P29 . proj11) is set
proj12 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
proj12 /. 1 is V11() real ext-real Element of REAL
proj12 `1 is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
r is Element of K6( the carrier of (TOP-REAL 2))
C /\ r is Element of K6( the carrier of (TOP-REAL 2))
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x `1 is V11() real ext-real Element of REAL
fs `1 is V11() real ext-real Element of REAL
(x `1) + (fs `1) is V11() real ext-real Element of REAL
((x `1) + (fs `1)) / 2 is V11() real ext-real Element of REAL
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((x `1) + (fs `1)) / 2 } is set
f is non empty V22() V25( the carrier of (TOP-REAL 2)) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))
Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)
dom f is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
[#] ((TOP-REAL 2) | C) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | C))
the carrier of ((TOP-REAL 2) | C) is set
K6( the carrier of ((TOP-REAL 2) | C)) is set
f1 is non empty Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | f1 is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f1) is non empty set
f | C is V22() V25( the carrier of (TOP-REAL 2)) V26( the carrier of R^1) Function-like Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))
dom (f | C) is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) /\ C is Element of K6( the carrier of (TOP-REAL 2))
rng (f | C) is V146() V147() V148() Element of K6( the carrier of R^1)
K7( the carrier of ((TOP-REAL 2) | C), the carrier of R^1) is set
K6(K7( the carrier of ((TOP-REAL 2) | C), the carrier of R^1)) is set
K7( the carrier of ((TOP-REAL 2) | f1), the carrier of R^1) is set
K6(K7( the carrier of ((TOP-REAL 2) | f1), the carrier of R^1)) is set
f2 is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | C), the carrier of R^1))
proj11 is non empty V22() V25( the carrier of ((TOP-REAL 2) | f1)) V26( the carrier of R^1) Function-like total quasi_total continuous Element of K6(K7( the carrier of ((TOP-REAL 2) | f1), the carrier of R^1))
proj12 is Element of the carrier of ((TOP-REAL 2) | C)
proj11 . proj12 is set
f . x is V11() real ext-real Element of the carrier of R^1
x /. 1 is V11() real ext-real Element of REAL
g1 is Element of the carrier of ((TOP-REAL 2) | C)
proj11 . g1 is set
f . fs is V11() real ext-real Element of the carrier of R^1
fs /. 1 is V11() real ext-real Element of REAL
P29 is Element of K6( the carrier of (TOP-REAL 2))
g is Element of the carrier of ((TOP-REAL 2) | C)
proj11 . g is set
f . g is set
P19 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P19 /. 1 is V11() real ext-real Element of REAL
P19 `1 is V11() real ext-real Element of REAL
g is Element of the carrier of ((TOP-REAL 2) | C)
proj11 . g is set
f . g is set
P19 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P19 /. 1 is V11() real ext-real Element of REAL
P19 `1 is V11() real ext-real Element of REAL
g is Element of K6( the carrier of (TOP-REAL 2))
P19 is Element of K6( the carrier of (TOP-REAL 2))
C is Element of K6( the carrier of (TOP-REAL 2))
r is Element of K6( the carrier of (TOP-REAL 2))
C /\ r is Element of K6( the carrier of (TOP-REAL 2))
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x `2 is V11() real ext-real Element of REAL
fs `2 is V11() real ext-real Element of REAL
(x `2) + (fs `2) is V11() real ext-real Element of REAL
((x `2) + (fs `2)) / 2 is V11() real ext-real Element of REAL
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `2 = ((x `2) + (fs `2)) / 2 } is set
P29 is non empty V22() V25( the carrier of (TOP-REAL 2)) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))
Seg 2 is V146() V147() V148() V149() V150() V151() Element of K6(NAT)
dom P29 is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
[#] ((TOP-REAL 2) | C) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | C))
the carrier of ((TOP-REAL 2) | C) is set
K6( the carrier of ((TOP-REAL 2) | C)) is set
f is non empty Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | f is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is non empty set
P29 | C is V22() V25( the carrier of (TOP-REAL 2)) V26( the carrier of R^1) Function-like Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))
dom (P29 | C) is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) /\ C is Element of K6( the carrier of (TOP-REAL 2))
rng (P29 | C) is V146() V147() V148() Element of K6( the carrier of R^1)
K7( the carrier of ((TOP-REAL 2) | C), the carrier of R^1) is set
K6(K7( the carrier of ((TOP-REAL 2) | C), the carrier of R^1)) is set
K7( the carrier of ((TOP-REAL 2) | f), the carrier of R^1) is set
K6(K7( the carrier of ((TOP-REAL 2) | f), the carrier of R^1)) is set
f1 is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | C), the carrier of R^1))
f2 is non empty V22() V25( the carrier of ((TOP-REAL 2) | f)) V26( the carrier of R^1) Function-like total quasi_total continuous Element of K6(K7( the carrier of ((TOP-REAL 2) | f), the carrier of R^1))
proj11 is Element of the carrier of ((TOP-REAL 2) | C)
f2 . proj11 is set
P29 . x is V11() real ext-real Element of the carrier of R^1
x /. 2 is V11() real ext-real Element of REAL
proj12 is Element of the carrier of ((TOP-REAL 2) | C)
f2 . proj12 is set
P29 . fs is V11() real ext-real Element of the carrier of R^1
fs /. 2 is V11() real ext-real Element of REAL
g1 is Element of K6( the carrier of (TOP-REAL 2))
g is Element of the carrier of ((TOP-REAL 2) | C)
f2 . g is set
P29 . g is set
P19 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P19 /. 2 is V11() real ext-real Element of REAL
P19 `2 is V11() real ext-real Element of REAL
g is Element of the carrier of ((TOP-REAL 2) | C)
f2 . g is set
P29 . g is set
P19 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P19 /. 2 is V11() real ext-real Element of REAL
P19 `2 is V11() real ext-real Element of REAL
g is Element of K6( the carrier of (TOP-REAL 2))
P19 is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
r `1 is V11() real ext-real Element of REAL
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x `1 is V11() real ext-real Element of REAL
(r `1) + (x `1) is V11() real ext-real Element of REAL
((r `1) + (x `1)) / 2 is V11() real ext-real Element of REAL
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((r `1) + (x `1)) / 2 } is set
C is Element of K6( the carrier of (TOP-REAL 2))
fs is set
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 `1 is V11() real ext-real Element of REAL
fs is Element of K6( the carrier of (TOP-REAL 2))
First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f is Element of K6( the carrier of (TOP-REAL 2))
First_Point (C,r,x,f) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f is set
f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f1 `1 is V11() real ext-real Element of REAL
f is Element of K6( the carrier of (TOP-REAL 2))
First_Point (C,r,x,f) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
r `2 is V11() real ext-real Element of REAL
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x `2 is V11() real ext-real Element of REAL
(r `2) + (x `2) is V11() real ext-real Element of REAL
((r `2) + (x `2)) / 2 is V11() real ext-real Element of REAL
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `2 = ((r `2) + (x `2)) / 2 } is set
C is Element of K6( the carrier of (TOP-REAL 2))
fs is set
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 `2 is V11() real ext-real Element of REAL
fs is Element of K6( the carrier of (TOP-REAL 2))
First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f is Element of K6( the carrier of (TOP-REAL 2))
First_Point (C,r,x,f) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f is set
f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f1 `2 is V11() real ext-real Element of REAL
f is Element of K6( the carrier of (TOP-REAL 2))
First_Point (C,r,x,f) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
r `1 is V11() real ext-real Element of REAL
x `1 is V11() real ext-real Element of REAL
(r `1) + (x `1) is V11() real ext-real Element of REAL
((r `1) + (x `1)) / 2 is V11() real ext-real Element of REAL
{ H1(b1) where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
fs is Element of K6( the carrier of (TOP-REAL 2))
First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C /\ fs is Element of K6( the carrier of (TOP-REAL 2))
r `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
(r `2) + (x `2) is V11() real ext-real Element of REAL
((r `2) + (x `2)) / 2 is V11() real ext-real Element of REAL
{ H1(b1) where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : S2[b1] } is set
P29 is Element of K6( the carrier of (TOP-REAL 2))
First_Point (C,r,x,P29) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C /\ P29 is Element of K6( the carrier of (TOP-REAL 2))
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
r `1 is V11() real ext-real Element of REAL
x `1 is V11() real ext-real Element of REAL
(r `1) + (x `1) is V11() real ext-real Element of REAL
((r `1) + (x `1)) / 2 is V11() real ext-real Element of REAL
{ H1(b1) where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
fs is Element of K6( the carrier of (TOP-REAL 2))
C /\ fs is Element of K6( the carrier of (TOP-REAL 2))
First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 `1 is V11() real ext-real Element of REAL
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((r `1) + (x `1)) / 2 } is set
fs is Element of K6( the carrier of (TOP-REAL 2))
First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C /\ fs is Element of K6( the carrier of (TOP-REAL 2))
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
r `2 is V11() real ext-real Element of REAL
x `2 is V11() real ext-real Element of REAL
(r `2) + (x `2) is V11() real ext-real Element of REAL
((r `2) + (x `2)) / 2 is V11() real ext-real Element of REAL
{ H1(b1) where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : S1[b1] } is set
fs is Element of K6( the carrier of (TOP-REAL 2))
C /\ fs is Element of K6( the carrier of (TOP-REAL 2))
First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 `2 is V11() real ext-real Element of REAL
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `2 = ((r `2) + (x `2)) / 2 } is set
fs is Element of K6( the carrier of (TOP-REAL 2))
First_Point (C,r,x,fs) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C /\ fs is Element of K6( the carrier of (TOP-REAL 2))
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | C) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | C)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | C))) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | C)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | C))) is set
f1 is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | C)) Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | C)))
f1 . 0 is set
f1 . 1 is set
f2 is V11() real ext-real Element of REAL
f1 . f2 is set
proj11 is V11() real ext-real Element of REAL
f1 . proj11 is set
1 - f2 is V11() real ext-real Element of REAL
1 - 0 is non empty V11() real ext-real positive non negative Element of REAL
1 - proj11 is V11() real ext-real Element of REAL
1 - 1 is V11() real ext-real Element of REAL
L[01] (((0,1) (#)),((#) (0,1))) is non empty V22() V25( the carrier of (Closed-Interval-TSpace (0,1))) V26( the carrier of (Closed-Interval-TSpace (0,1))) Function-like total quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)))) is set
f1 * (L[01] (((0,1) (#)),((#) (0,1)))) is V22() V25( the carrier of (Closed-Interval-TSpace (0,1))) V26( the carrier of ((TOP-REAL 2) | C)) Function-like Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | C)))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | C)) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | C))) is set
(L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
dom f1 is V146() V147() V148() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper closed V146() V147() V148() Element of K6( the carrier of I[01])
rng (L[01] (((0,1) (#)),((#) (0,1)))) is V146() V147() V148() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
K6( the carrier of (Closed-Interval-TSpace (0,1))) is set
dom (f1 * (L[01] (((0,1) (#)),((#) (0,1))))) is V146() V147() V148() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
dom (L[01] (((0,1) (#)),((#) (0,1)))) is V146() V147() V148() Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
f is non empty Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | f is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f))) is set
g is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | f)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
dom g is V146() V147() V148() Element of K6( the carrier of I[01])
g . 0 is set
g . 1 is set
P19 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(L[01] (((0,1) (#)),((#) (0,1)))) . P19 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
1 - (1 - f2) is V11() real ext-real Element of REAL
(1 - (1 - f2)) * 1 is V11() real ext-real Element of REAL
(1 - f2) * 0 is V11() real ext-real Element of REAL
((1 - (1 - f2)) * 1) + ((1 - f2) * 0) is V11() real ext-real Element of REAL
r1 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(L[01] (((0,1) (#)),((#) (0,1)))) . r1 is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
1 - (1 - proj11) is V11() real ext-real Element of REAL
(1 - (1 - proj11)) * 1 is V11() real ext-real Element of REAL
(1 - proj11) * 0 is V11() real ext-real Element of REAL
((1 - (1 - proj11)) * 1) + ((1 - proj11) * 0) is V11() real ext-real Element of REAL
g . (1 - f2) is set
g . (1 - proj11) is set
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE b1,fs,C,r,x } is set
P29 is set
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE fs,b1,C,r,x } is set
P29 is set
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE b1,fs,C,r,x } is set
P29 is set
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE fs,b1,C,r,x } is set
P29 is set
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x,r) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE b1,r,C,r,x } is set
{r} is non empty set
fs is set
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is set
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x,x) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE b1,x,C,r,x } is set
fs is set
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x,x) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE x,b1,C,r,x } is set
{x} is non empty set
fs is set
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is set
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x,r) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE r,b1,C,r,x } is set
fs is set
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE fs,b1,C,r,x } is set
(C,x,r,fs) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE b1,fs,C,x,r } is set
P29 is set
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 is set
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE fs,b1,C,r,x } is set
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x,P29) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE b1,P29,C,r,x } is set
(C,r,x,fs) /\ (C,r,x,P29) is Element of K6( the carrier of (TOP-REAL 2))
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x,fs,P29) is Element of K6( the carrier of (TOP-REAL 2))
(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE fs,b1,C,r,x } is set
(C,r,x,P29) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE b1,P29,C,r,x } is set
(C,r,x,fs) /\ (C,r,x,P29) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : ( LE fs,b1,C,r,x & LE b1,P29,C,r,x ) } is set
f is set
f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f2 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f is set
f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
f1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C is Element of K6( the carrier of (TOP-REAL 2))
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE b1,fs,C,r,x } is set
(C,x,r,fs) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE fs,b1,C,x,r } is set
P29 is set
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 is set
f is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
C is Element of K6( the carrier of (TOP-REAL 2))
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
fs is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
P29 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(C,r,x,fs,P29) is Element of K6( the carrier of (TOP-REAL 2))
(C,r,x,fs) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE fs,b1,C,r,x } is set
(C,r,x,P29) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE b1,P29,C,r,x } is set
(C,r,x,fs) /\ (C,r,x,P29) is Element of K6( the carrier of (TOP-REAL 2))
(C,x,r,P29,fs) is Element of K6( the carrier of (TOP-REAL 2))
(C,x,r,P29) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE P29,b1,C,x,r } is set
(C,x,r,fs) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : LE b1,fs,C,x,r } is set
(C,x,r,P29) /\ (C,x,r,fs) is Element of K6( the carrier of (TOP-REAL 2))
C is V11() real ext-real set
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `1 = C } is set
r is set
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x `1 is V11() real ext-real Element of REAL
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `2 = C } is set
r is set
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x `2 is V11() real ext-real Element of REAL
C is V11() real ext-real set
(C) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `1 = C } is set
r is V11() real ext-real set
(r) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `2 = r } is set
C is V11() real ext-real set
(C) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `1 = C } is set
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
r `1 is V11() real ext-real Element of REAL
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x `1 is V11() real ext-real Element of REAL
C is V11() real ext-real set
(C) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `2 = C } is set
r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
r `2 is V11() real ext-real Element of REAL
x is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
x `2 is V11() real ext-real Element of REAL
C is Element of K6( the carrier of (TOP-REAL 2))
W-min C is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
W-bound C is V11() real ext-real Element of REAL
(TOP-REAL 2) | C is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))
the carrier of ((TOP-REAL 2) | C) is set
K7( the carrier of ((TOP-REAL 2) | C),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | C),REAL)) is set
lower_bound (proj1 | C) is V11() real ext-real Element of REAL
(proj1 | C) .: the carrier of ((TOP-REAL 2) | C) is V146() V147() V148() Element of K6(REAL)
lower_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
W-most C is Element of K6( the carrier of (TOP-REAL 2))
SW-corner C is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
S-bound C is V11() real ext-real Element of REAL
proj2 is non empty V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
proj2 | C is V22() V25( the carrier of ((TOP-REAL 2) | C)) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | C),REAL))
lower_bound (proj2 | C) is V11() real ext-real Element of REAL
(proj2 | C) .: the carrier of ((TOP-REAL 2) | C) is V146() V147() V148() Element of K6(REAL)
lower_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
|[(W-bound C),(S-bound C)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
NW-corner C is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
N-bound C is V11() real ext-real Element of REAL
upper_bound (proj2 | C) is V11() real ext-real Element of REAL
upper_bound ((proj2 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
|[(W-bound C),(N-bound C)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner C),(NW-corner C)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner C),(NW-corner C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (W-most C) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 | (W-most C) is V22() V25( the carrier of ((TOP-REAL 2) | (W-most C))) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL))
the carrier of ((TOP-REAL 2) | (W-most C)) is set
K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (W-most C)),REAL)) is set
lower_bound (proj2 | (W-most C)) is V11() real ext-real Element of REAL
(proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C)) is V146() V147() V148() Element of K6(REAL)
lower_bound ((proj2 | (W-most C)) .: the carrier of ((TOP-REAL 2) | (W-most C))) is V11() real ext-real Element of REAL
|[(W-bound C),(lower_bound (proj2 | (W-most C)))]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
E-max C is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
E-bound C is V11() real ext-real Element of REAL
upper_bound (proj1 | C) is V11() real ext-real Element of REAL
upper_bound ((proj1 | C) .: the carrier of ((TOP-REAL 2) | C)) is V11() real ext-real Element of REAL
E-most C is Element of K6( the carrier of (TOP-REAL 2))
SE-corner C is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
|[(E-bound C),(S-bound C)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
NE-corner C is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
|[(E-bound C),(N-bound C)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner C),(NE-corner C)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SE-corner C),(NE-corner C))) /\ C is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (E-most C) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 | (E-most C) is V22() V25( the carrier of ((TOP-REAL 2) | (E-most C))) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL))
the carrier of ((TOP-REAL 2) | (E-most C)) is set
K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (E-most C)),REAL)) is set
upper_bound (proj2 | (E-most C)) is V11() real ext-real Element of REAL
(proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C)) is V146() V147() V148() Element of K6(REAL)
upper_bound ((proj2 | (E-most C)) .: the carrier of ((TOP-REAL 2) | (E-most C))) is V11() real ext-real Element of REAL
|[(E-bound C),(upper_bound (proj2 | (E-most C)))]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
{(W-min C),(E-max C)} is non empty set
(W-bound C) + (E-bound C) is V11() real ext-real Element of REAL
((W-bound C) + (E-bound C)) / 2 is V11() real ext-real Element of REAL
((((W-bound C) + (E-bound C)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((W-bound C) + (E-bound C)) / 2 } is set
r is non empty closed compact being_simple_closed_curve Element of K6( the carrier of (TOP-REAL 2))
W-min r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
W-bound r is V11() real ext-real Element of REAL
(TOP-REAL 2) | r is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj1 | r is non empty V22() V25( the carrier of ((TOP-REAL 2) | r)) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | r),REAL))
the carrier of ((TOP-REAL 2) | r) is non empty set
K7( the carrier of ((TOP-REAL 2) | r),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | r),REAL)) is set
lower_bound (proj1 | r) is V11() real ext-real Element of REAL
(proj1 | r) .: the carrier of ((TOP-REAL 2) | r) is non empty V146() V147() V148() Element of K6(REAL)
lower_bound ((proj1 | r) .: the carrier of ((TOP-REAL 2) | r)) is V11() real ext-real Element of REAL
W-most r is Element of K6( the carrier of (TOP-REAL 2))
SW-corner r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
S-bound r is V11() real ext-real Element of REAL
proj2 | r is non empty V22() V25( the carrier of ((TOP-REAL 2) | r)) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | r),REAL))
lower_bound (proj2 | r) is V11() real ext-real Element of REAL
(proj2 | r) .: the carrier of ((TOP-REAL 2) | r) is non empty V146() V147() V148() Element of K6(REAL)
lower_bound ((proj2 | r) .: the carrier of ((TOP-REAL 2) | r)) is V11() real ext-real Element of REAL
|[(W-bound r),(S-bound r)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
NW-corner r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
N-bound r is V11() real ext-real Element of REAL
upper_bound (proj2 | r) is V11() real ext-real Element of REAL
upper_bound ((proj2 | r) .: the carrier of ((TOP-REAL 2) | r)) is V11() real ext-real Element of REAL
|[(W-bound r),(N-bound r)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
LSeg ((SW-corner r),(NW-corner r)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SW-corner r),(NW-corner r))) /\ r is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (W-most r) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 | (W-most r) is V22() V25( the carrier of ((TOP-REAL 2) | (W-most r))) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | (W-most r)),REAL))
the carrier of ((TOP-REAL 2) | (W-most r)) is set
K7( the carrier of ((TOP-REAL 2) | (W-most r)),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (W-most r)),REAL)) is set
lower_bound (proj2 | (W-most r)) is V11() real ext-real Element of REAL
(proj2 | (W-most r)) .: the carrier of ((TOP-REAL 2) | (W-most r)) is V146() V147() V148() Element of K6(REAL)
lower_bound ((proj2 | (W-most r)) .: the carrier of ((TOP-REAL 2) | (W-most r))) is V11() real ext-real Element of REAL
|[(W-bound r),(lower_bound (proj2 | (W-most r)))]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
E-max r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
E-bound r is V11() real ext-real Element of REAL
upper_bound (proj1 | r) is V11() real ext-real Element of REAL
upper_bound ((proj1 | r) .: the carrier of ((TOP-REAL 2) | r)) is V11() real ext-real Element of REAL
E-most r is Element of K6( the carrier of (TOP-REAL 2))
SE-corner r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
|[(E-bound r),(S-bound r)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
NE-corner r is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
|[(E-bound r),(N-bound r)]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
LSeg ((SE-corner r),(NE-corner r)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg ((SE-corner r),(NE-corner r))) /\ r is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (E-most r) is strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
proj2 | (E-most r) is V22() V25( the carrier of ((TOP-REAL 2) | (E-most r))) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | (E-most r)),REAL))
the carrier of ((TOP-REAL 2) | (E-most r)) is set
K7( the carrier of ((TOP-REAL 2) | (E-most r)),REAL) is set
K6(K7( the carrier of ((TOP-REAL 2) | (E-most r)),REAL)) is set
upper_bound (proj2 | (E-most r)) is V11() real ext-real Element of REAL
(proj2 | (E-most r)) .: the carrier of ((TOP-REAL 2) | (E-most r)) is V146() V147() V148() Element of K6(REAL)
upper_bound ((proj2 | (E-most r)) .: the carrier of ((TOP-REAL 2) | (E-most r))) is V11() real ext-real Element of REAL
|[(E-bound r),(upper_bound (proj2 | (E-most r)))]| is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
{(W-min r),(E-max r)} is non empty set
x is non empty Element of K6( the carrier of (TOP-REAL 2))
fs is non empty Element of K6( the carrier of (TOP-REAL 2))
x \/ fs is non empty Element of K6( the carrier of (TOP-REAL 2))
x /\ fs is Element of K6( the carrier of (TOP-REAL 2))
P29 is non empty Element of K6( the carrier of (TOP-REAL 2))
f is non empty Element of K6( the carrier of (TOP-REAL 2))
(E-max r) `1 is V11() real ext-real Element of REAL
(W-bound r) + (E-bound r) is V11() real ext-real Element of REAL
((W-bound r) + (E-bound r)) / 2 is V11() real ext-real Element of REAL
((((W-bound r) + (E-bound r)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
{ b1 where b1 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2) : b1 `1 = ((W-bound r) + (E-bound r)) / 2 } is set
P29 /\ ((((W-bound r) + (E-bound r)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
f /\ ((((W-bound r) + (E-bound r)) / 2)) is Element of K6( the carrier of (TOP-REAL 2))
f1 is non empty Element of K6( the carrier of (TOP-REAL 2))
(W-min r) `1 is V11() real ext-real Element of REAL
((W-min r) `1) + ((E-max r) `1) is V11() real ext-real Element of REAL
(((W-min r) `1) + ((E-max r) `1)) / 2 is V11() real ext-real Element of REAL
proj11 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
proj11 `1 is V11() real ext-real Element of REAL
f2 is non empty Element of K6( the carrier of (TOP-REAL 2))
proj12 is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
proj12 `1 is V11() real ext-real Element of REAL
First_Point (P29,(W-min r),(E-max r),((((W-bound r) + (E-bound r)) / 2))) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(First_Point (P29,(W-min r),(E-max r),((((W-bound r) + (E-bound r)) / 2)))) `2 is V11() real ext-real Element of REAL
Last_Point (f,(E-max r),(W-min r),((((W-bound r) + (E-bound r)) / 2))) is V22() V26( REAL ) Function-like V43(2) FinSequence-like V138() Element of the carrier of (TOP-REAL 2)
(Last_Point (f,(E-max r),(W-min r),((((W-bound r) + (E-bound r)) / 2)))) `2 is V11() real ext-real Element of REAL
First_Point (P29,(W-min r),(E-max r),((