:: JORDAN5C semantic presentation

REAL is V142() V143() V144() V148() set
NAT is V142() V143() V144() V145() V146() V147() V148() Element of K6(REAL)
K6(REAL) is set
NAT is V142() V143() V144() V145() V146() V147() V148() set
K6(NAT) is set
K6(NAT) is set
1 is non empty V10() V11() V12() ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() 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 V10() V11() V12() ext-real positive non negative V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
K7(2,2) is set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is set
COMPLEX is V142() V148() set
RAT is V142() V143() V144() V145() V148() set
INT is V142() V143() V144() V145() V146() V148() set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V108() V154() V155() V156() V157() V158() V159() V160() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty functional set
K6( the carrier of (TOP-REAL 2)) is set
K409() is non empty strict TopSpace-like TopStruct
the carrier of K409() is non empty set
K207() is V84() L7()
R^1 is TopSpace-like TopStruct
0 is empty V10() V11() V12() ext-real non positive non negative Function-like functional V79() V80() V142() V143() V144() V145() V146() V147() V148() Element of NAT
the empty Function-like functional V142() V143() V144() V145() V146() V147() V148() set is empty Function-like functional V142() V143() V144() V145() V146() V147() V148() set
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like SubSpace of R^1
the carrier of (Closed-Interval-TSpace (0,1)) is non empty set
{} is empty Function-like functional V142() V143() V144() V145() V146() V147() V148() set
[.0,1.] is V142() V143() V144() Element of K6(REAL)
K410() is Element of the carrier of K409()
K411() is Element of the carrier of K409()
I[01] is non empty strict TopSpace-like SubSpace of R^1
the carrier of I[01] is non empty set
K6( the carrier of K409()) is set
(#) (0,1) is Element of the carrier of (Closed-Interval-TSpace (0,1))
(0,1) (#) is Element of the carrier of (Closed-Interval-TSpace (0,1))
K7( the carrier of I[01], the carrier of I[01]) is set
K6(K7( the carrier of I[01], the carrier of I[01])) is set
f is functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | f is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is 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
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
p4 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
P . 0 is set
P . 1 is set
i is V11() V12() ext-real Element of REAL
P . i is set
Q is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
Q . 0 is set
Q . 1 is set
p1 is V11() V12() ext-real Element of REAL
Q . p1 is set
j is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | j is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | j) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | j)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | j))) is set
p2 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | j) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | j)))
dom p2 is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
rng p2 is Element of K6( the carrier of ((TOP-REAL 2) | j))
K6( the carrier of ((TOP-REAL 2) | j)) is set
[#] ((TOP-REAL 2) | f) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | f))
K6( the carrier of ((TOP-REAL 2) | f)) is set
p2 /" is non empty Relation-like the carrier of ((TOP-REAL 2) | j) -defined the carrier of I[01] -valued Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | j), the carrier of I[01]))
K7( the carrier of ((TOP-REAL 2) | j), the carrier of I[01]) is set
K6(K7( the carrier of ((TOP-REAL 2) | j), the carrier of I[01])) is set
p2 " is Relation-like Function-like set
(p2 /") . p3 is set
(p2 /") . q2 is set
H is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | j) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | j)))
(p2 /") * H is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of I[01]))
x19 is V11() V12() ext-real Element of REAL
Q . x19 is set
((p2 /") * H) . x19 is set
x1 is Element of the carrier of I[01]
((p2 /") * H) . x1 is Element of the carrier of I[01]
rng H is Element of K6( the carrier of ((TOP-REAL 2) | j))
dom H is Element of K6( the carrier of I[01])
((p2 /") * H) . 1 is set
dom (p2 /") is Element of K6( the carrier of ((TOP-REAL 2) | j))
dom ((p2 /") * H) is Element of K6( the carrier of I[01])
((p2 /") * H) . 0 is set
x2 is V11() V12() ext-real Element of REAL
p2 * ((p2 /") * H) is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | j) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | j)))
p2 * (p2 /") is non empty Relation-like the carrier of ((TOP-REAL 2) | j) -defined the carrier of ((TOP-REAL 2) | j) -valued Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | j), the carrier of ((TOP-REAL 2) | j)))
K7( the carrier of ((TOP-REAL 2) | j), the carrier of ((TOP-REAL 2) | j)) is set
K6(K7( the carrier of ((TOP-REAL 2) | j), the carrier of ((TOP-REAL 2) | j))) is set
H (#) (p2 * (p2 /")) is Relation-like Function-like set
id (rng p2) is Relation-like rng p2 -defined rng p2 -valued Function-like one-to-one total quasi_total Element of K6(K7((rng p2),(rng p2)))
K7((rng p2),(rng p2)) is set
K6(K7((rng p2),(rng p2))) is set
H (#) (id (rng p2)) is Relation-like Function-like set
id (rng H) is Relation-like rng H -defined rng H -valued Function-like one-to-one total quasi_total Element of K6(K7((rng H),(rng H)))
K7((rng H),(rng H)) is set
K6(K7((rng H),(rng H))) is set
(id (rng H)) * H is Relation-like the carrier of I[01] -defined rng H -valued Function-like Element of K6(K7( the carrier of I[01],(rng H)))
K7( the carrier of I[01],(rng H)) is set
K6(K7( the carrier of I[01],(rng H))) is set
p2 . (((p2 /") * H) . x19) is set
H . x19 is set
((p2 /") * H) . p1 is set
(p2 /") . p4 is set
x29 is Element of the carrier of I[01]
((p2 /") * H) . x29 is Element of the carrier of I[01]
f is functional Element of K6( the carrier of (TOP-REAL 2))
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
f /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | f is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is 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
p4 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
P . 0 is set
P . 1 is set
i is V11() V12() ext-real Element of REAL
P . i is set
j is V11() V12() ext-real Element of REAL
P . j is set
Q is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
Q . 0 is set
Q . 1 is set
p1 is V11() V12() ext-real Element of REAL
Q . p1 is set
p4 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
i is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
i . 0 is set
i . 1 is set
rng i is Element of K6( the carrier of ((TOP-REAL 2) | f))
K6( the carrier of ((TOP-REAL 2) | f)) is set
[#] ((TOP-REAL 2) | f) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | f))
dom i is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
j is set
i . j is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
Q is V11() V12() ext-real Element of REAL
p1 is set
i . p1 is set
p2 is V11() V12() ext-real Element of REAL
f is functional Element of K6( the carrier of (TOP-REAL 2))
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
{q2} is non empty functional set
(f,q1,p3,p4) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /\ {q2} is functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | f is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is 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
P is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
P . 0 is set
P . 1 is set
i is V11() V12() ext-real Element of REAL
P . i is set
j is V11() V12() ext-real Element of REAL
P . j is set
dom P is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
f /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
f is functional Element of K6( the carrier of (TOP-REAL 2))
f /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(f,q1,q2,p3) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | f is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is 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
p4 is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
p4 . 0 is set
p4 . 1 is set
P is V11() V12() ext-real Element of REAL
p4 . P is set
i is V11() V12() ext-real Element of REAL
p4 . i is set
dom p4 is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
f is functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | f is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is 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
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
p4 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
P . 0 is set
P . 1 is set
i is V11() V12() ext-real Element of REAL
P . i is set
Q is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
Q . 0 is set
Q . 1 is set
p1 is V11() V12() ext-real Element of REAL
Q . p1 is set
j is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | j is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | j) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | j)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | j))) is set
p2 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | j) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | j)))
H is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | j) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | j)))
p2 /" is non empty Relation-like the carrier of ((TOP-REAL 2) | j) -defined the carrier of I[01] -valued Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | j), the carrier of I[01]))
K7( the carrier of ((TOP-REAL 2) | j), the carrier of I[01]) is set
K6(K7( the carrier of ((TOP-REAL 2) | j), the carrier of I[01])) is set
(p2 /") * H is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of I[01]))
x19 is V11() V12() ext-real Element of REAL
Q . x19 is set
((p2 /") * H) . x19 is set
x1 is Element of the carrier of I[01]
((p2 /") * H) . x1 is Element of the carrier of I[01]
rng H is Element of K6( the carrier of ((TOP-REAL 2) | j))
K6( the carrier of ((TOP-REAL 2) | j)) is set
[#] ((TOP-REAL 2) | f) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | f))
K6( the carrier of ((TOP-REAL 2) | f)) is set
dom p2 is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
rng p2 is Element of K6( the carrier of ((TOP-REAL 2) | j))
p2 " is Relation-like Function-like set
(p2 /") . q2 is set
(p2 /") . p3 is set
dom H is Element of K6( the carrier of I[01])
((p2 /") * H) . 0 is set
((p2 /") * H) . 1 is set
x2 is V11() V12() ext-real Element of REAL
dom (p2 /") is Element of K6( the carrier of ((TOP-REAL 2) | j))
dom ((p2 /") * H) is Element of K6( the carrier of I[01])
p2 * ((p2 /") * H) is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | j) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | j)))
p2 * (p2 /") is non empty Relation-like the carrier of ((TOP-REAL 2) | j) -defined the carrier of ((TOP-REAL 2) | j) -valued Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | j), the carrier of ((TOP-REAL 2) | j)))
K7( the carrier of ((TOP-REAL 2) | j), the carrier of ((TOP-REAL 2) | j)) is set
K6(K7( the carrier of ((TOP-REAL 2) | j), the carrier of ((TOP-REAL 2) | j))) is set
H (#) (p2 * (p2 /")) is Relation-like Function-like set
id (rng p2) is Relation-like rng p2 -defined rng p2 -valued Function-like one-to-one total quasi_total Element of K6(K7((rng p2),(rng p2)))
K7((rng p2),(rng p2)) is set
K6(K7((rng p2),(rng p2))) is set
H (#) (id (rng p2)) is Relation-like Function-like set
id (rng H) is Relation-like rng H -defined rng H -valued Function-like one-to-one total quasi_total Element of K6(K7((rng H),(rng H)))
K7((rng H),(rng H)) is set
K6(K7((rng H),(rng H))) is set
(id (rng H)) * H is Relation-like the carrier of I[01] -defined rng H -valued Function-like Element of K6(K7( the carrier of I[01],(rng H)))
K7( the carrier of I[01],(rng H)) is set
K6(K7( the carrier of I[01],(rng H))) is set
p2 . (((p2 /") * H) . x19) is set
H . x19 is set
((p2 /") * H) . p1 is set
(p2 /") . p4 is set
x29 is Element of the carrier of I[01]
((p2 /") * H) . x29 is Element of the carrier of I[01]
f is functional Element of K6( the carrier of (TOP-REAL 2))
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
f /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | f is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is 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
p4 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
P . 0 is set
P . 1 is set
i is V11() V12() ext-real Element of REAL
P . i is set
j is V11() V12() ext-real Element of REAL
P . j is set
Q is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
Q . 0 is set
Q . 1 is set
p1 is V11() V12() ext-real Element of REAL
Q . p1 is set
p4 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
i is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
i . 0 is set
i . 1 is set
rng i is Element of K6( the carrier of ((TOP-REAL 2) | f))
K6( the carrier of ((TOP-REAL 2) | f)) is set
[#] ((TOP-REAL 2) | f) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | f))
dom i is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
j is set
i . j is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
Q is V11() V12() ext-real Element of REAL
p1 is set
i . p1 is set
p2 is V11() V12() ext-real Element of REAL
f is functional Element of K6( the carrier of (TOP-REAL 2))
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
{q2} is non empty functional set
(f,q1,p3,p4) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /\ {q2} is functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | f is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is 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
P is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
P . 0 is set
P . 1 is set
i is V11() V12() ext-real Element of REAL
P . i is set
dom P is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
j is V11() V12() ext-real Element of REAL
P . j is set
f /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
f is functional Element of K6( the carrier of (TOP-REAL 2))
f /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(f,q1,q2,p3) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | f is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is 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
p4 is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
p4 . 0 is set
p4 . 1 is set
P is V11() V12() ext-real Element of REAL
p4 . P is set
i is V11() V12() ext-real Element of REAL
p4 . i is set
dom p4 is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
f is functional Element of K6( the carrier of (TOP-REAL 2))
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(f,q1,q2,p3) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(f,q1,q2,p3) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
f is functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | f is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is 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
q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
P . 0 is set
P . 1 is set
i is V11() V12() ext-real Element of REAL
P . i is set
j is V11() V12() ext-real Element of REAL
P . j is set
Q is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | Q is non empty strict TopSpace-like SubSpace of TOP-REAL 2
[#] ((TOP-REAL 2) | Q) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | Q))
the carrier of ((TOP-REAL 2) | Q) is non empty set
K6( the carrier of ((TOP-REAL 2) | Q)) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | Q)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | Q))) is set
p1 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | Q) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | Q)))
p1 . j is set
H is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | Q) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | Q)))
H . 0 is set
H . 1 is set
x19 is V11() V12() ext-real Element of REAL
H . x19 is set
x1 is V11() V12() ext-real Element of REAL
H . x1 is set
H /" is non empty Relation-like the carrier of ((TOP-REAL 2) | Q) -defined the carrier of I[01] -valued Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | Q), the carrier of I[01]))
K7( the carrier of ((TOP-REAL 2) | Q), the carrier of I[01]) is set
K6(K7( the carrier of ((TOP-REAL 2) | Q), the carrier of I[01])) is set
(H /") * p1 is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of I[01]))
((H /") * p1) . i is set
((H /") * p1) . j is set
p2 is Element of the carrier of I[01]
((H /") * p1) . p2 is Element of the carrier of I[01]
H is Element of the carrier of I[01]
((H /") * p1) . H is Element of the carrier of I[01]
dom p1 is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
dom H is Element of K6( the carrier of I[01])
rng H is Element of K6( the carrier of ((TOP-REAL 2) | Q))
[#] ((TOP-REAL 2) | f) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | f))
K6( the carrier of ((TOP-REAL 2) | f)) is set
H " is Relation-like Function-like set
(H /") . q1 is set
((H /") * p1) . 0 is set
(H /") . p3 is set
(H /") . p4 is set
(H /") . q2 is set
((H /") * p1) . 1 is set
F is V11() V12() ext-real Element of REAL
x2 is V11() V12() ext-real Element of REAL
f is functional Element of K6( the carrier of (TOP-REAL 2))
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | p4 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p4) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4))) is set
P is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)))
P . 0 is set
P . 1 is set
i is V11() V12() ext-real Element of REAL
P . i is set
j is V11() V12() ext-real Element of REAL
P . j is set
f is functional Element of K6( the carrier of (TOP-REAL 2))
q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | p4 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p4) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4))) is set
P is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)))
P . 0 is set
P . 1 is set
i is V11() V12() ext-real Element of REAL
P . i is set
j is V11() V12() ext-real Element of REAL
P . j is set
P is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)))
P . 0 is set
P . 1 is set
i is V11() V12() ext-real Element of REAL
P . i is set
j is V11() V12() ext-real Element of REAL
P . j is set
f is functional Element of K6( the carrier of (TOP-REAL 2))
q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f is functional Element of K6( the carrier of (TOP-REAL 2))
q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | f is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is 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
P is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
P . 0 is set
P . 1 is set
dom P is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
rng P is Element of K6( the carrier of ((TOP-REAL 2) | f))
K6( the carrier of ((TOP-REAL 2) | f)) is set
[#] ((TOP-REAL 2) | f) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | f))
i is set
P . i is set
j is set
P . j is set
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Q is V11() V12() ext-real Element of REAL
p1 is V11() V12() ext-real Element of REAL
f is functional Element of K6( the carrier of (TOP-REAL 2))
q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(TOP-REAL 2) | f is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is 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
i is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
i . 0 is set
i . 1 is set
j is V11() V12() ext-real Element of REAL
i . j is set
Q is V11() V12() ext-real Element of REAL
i . Q is set
rng i is Element of K6( the carrier of ((TOP-REAL 2) | f))
K6( the carrier of ((TOP-REAL 2) | f)) is set
[#] ((TOP-REAL 2) | f) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | f))
dom i is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
p1 is set
i . p1 is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
p2 is V11() V12() ext-real Element of REAL
f is functional Element of K6( the carrier of (TOP-REAL 2))
q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
i is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
i . 0 is set
i . 1 is set
rng i is Element of K6( the carrier of ((TOP-REAL 2) | P))
K6( the carrier of ((TOP-REAL 2) | P)) is set
[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))
dom i is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
j is set
i . j is set
Q is set
i . Q is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
p1 is V11() V12() ext-real Element of REAL
p2 is V11() V12() ext-real Element of REAL
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
(L~ f) /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
((L~ f),q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | (L~ f) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (L~ f)) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (L~ f))) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (L~ f)))) is set
P is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (L~ f)) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (L~ f))))
P . 0 is set
P . 1 is set
i is V11() V12() ext-real Element of REAL
P . i is set
j is V11() V12() ext-real Element of REAL
P . j is set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
(L~ f) /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
((L~ f),q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | (L~ f) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (L~ f)) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (L~ f))) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (L~ f)))) is set
P is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (L~ f)) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (L~ f))))
P . 0 is set
P . 1 is set
i is V11() V12() ext-real Element of REAL
P . i is set
j is V11() V12() ext-real Element of REAL
P . j is set
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
LSeg (q2,p3) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
f is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(TOP-REAL 2) | (LSeg (q2,p3)) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (LSeg (q2,p3))) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg (q2,p3)))) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg (q2,p3))))) is set
P is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (LSeg (q2,p3))) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg (q2,p3)))))
P . 0 is set
P . 1 is set
i is V11() V12() ext-real Element of REAL
1 - i is V11() V12() ext-real Element of REAL
(1 - i) * q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
i * p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
((1 - i) * q2) + (i * p3) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
j is V11() V12() ext-real Element of REAL
1 - j is V11() V12() ext-real Element of REAL
(1 - j) * q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
j * p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
((1 - j) * q2) + (j * p3) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P . j is set
P . i is set
f is functional Element of K6( the carrier of (TOP-REAL 2))
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
f /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(f,q1,q2,p3) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(f,q1,p3,q2) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(f,q1,q2,p3) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(f,q1,p3,q2) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | p4 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p4) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4))) is set
(p4,q1,p3,q2) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
L[01] (((0,1) (#)),((#) (0,1))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued 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
i is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)))
i . 0 is set
i . 1 is set
j is V11() V12() ext-real Element of REAL
i . j is set
1 - j is V11() V12() ext-real Element of REAL
i * (L[01] (((0,1) (#)),((#) (0,1)))) is Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | p4)))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | p4)) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | p4))) is set
dom i is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
rng (L[01] (((0,1) (#)),((#) (0,1)))) is Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
K6( the carrier of (Closed-Interval-TSpace (0,1))) is set
dom (i * (L[01] (((0,1) (#)),((#) (0,1))))) is Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
dom (L[01] (((0,1) (#)),((#) (0,1)))) is Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
1 - 1 is V11() V12() ext-real Element of REAL
1 - 0 is V11() V12() ext-real Element of REAL
p2 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)))
dom p2 is Element of K6( the carrier of I[01])
(L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) is Element of the carrier of (Closed-Interval-TSpace (0,1))
p2 . 0 is set
(L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) is Element of the carrier of (Closed-Interval-TSpace (0,1))
p2 . 1 is set
H is V11() V12() ext-real Element of REAL
i . H is set
1 - H is V11() V12() ext-real Element of REAL
H is Element of the carrier of (Closed-Interval-TSpace (0,1))
(L[01] (((0,1) (#)),((#) (0,1)))) . H is Element of the carrier of (Closed-Interval-TSpace (0,1))
1 - (1 - j) is V11() V12() ext-real Element of REAL
(1 - (1 - j)) * 1 is V11() V12() ext-real Element of REAL
(1 - j) * 0 is V11() V12() ext-real Element of REAL
((1 - (1 - j)) * 1) + ((1 - j) * 0) is V11() V12() ext-real Element of REAL
p2 . (1 - j) is set
x19 is Element of the carrier of (Closed-Interval-TSpace (0,1))
(L[01] (((0,1) (#)),((#) (0,1)))) . x19 is Element of the carrier of (Closed-Interval-TSpace (0,1))
1 - (1 - H) is V11() V12() ext-real Element of REAL
(1 - (1 - H)) * 1 is V11() V12() ext-real Element of REAL
(1 - H) * 0 is V11() V12() ext-real Element of REAL
((1 - (1 - H)) * 1) + ((1 - H) * 0) is V11() V12() ext-real Element of REAL
p2 . x19 is set
(p4,q1,p3,q2) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
L[01] (((0,1) (#)),((#) (0,1))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued 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
i is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)))
i . 0 is set
i . 1 is set
j is V11() V12() ext-real Element of REAL
i . j is set
i * (L[01] (((0,1) (#)),((#) (0,1)))) is Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | p4)))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | p4)) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | p4))) is set
dom i is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
rng (L[01] (((0,1) (#)),((#) (0,1)))) is Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
K6( the carrier of (Closed-Interval-TSpace (0,1))) is set
dom (i * (L[01] (((0,1) (#)),((#) (0,1))))) is Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
dom (L[01] (((0,1) (#)),((#) (0,1)))) is Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
p1 is V11() V12() ext-real Element of REAL
i . p1 is set
1 - j is V11() V12() ext-real Element of REAL
1 - p1 is V11() V12() ext-real Element of REAL
1 - 0 is V11() V12() ext-real Element of REAL
1 - 1 is V11() V12() ext-real Element of REAL
H is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)))
dom H is Element of K6( the carrier of I[01])
H is Element of the carrier of (Closed-Interval-TSpace (0,1))
(L[01] (((0,1) (#)),((#) (0,1)))) . H is Element of the carrier of (Closed-Interval-TSpace (0,1))
1 - (1 - j) is V11() V12() ext-real Element of REAL
(1 - (1 - j)) * 1 is V11() V12() ext-real Element of REAL
(1 - j) * 0 is V11() V12() ext-real Element of REAL
((1 - (1 - j)) * 1) + ((1 - j) * 0) is V11() V12() ext-real Element of REAL
H . (1 - j) is set
x19 is Element of the carrier of (Closed-Interval-TSpace (0,1))
(L[01] (((0,1) (#)),((#) (0,1)))) . x19 is Element of the carrier of (Closed-Interval-TSpace (0,1))
1 - (1 - p1) is V11() V12() ext-real Element of REAL
(1 - (1 - p1)) * 1 is V11() V12() ext-real Element of REAL
(1 - p1) * 0 is V11() V12() ext-real Element of REAL
((1 - (1 - p1)) * 1) + ((1 - p1) * 0) is V11() V12() ext-real Element of REAL
H . x19 is set
(L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) is Element of the carrier of (Closed-Interval-TSpace (0,1))
H . 0 is set
(L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) is Element of the carrier of (Closed-Interval-TSpace (0,1))
H . 1 is set
p4 /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
((L~ f),q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
q2 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,q2) is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (q2 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
((LSeg (f,q2)),q1,(f /. q2),(f /. (q2 + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
p4 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(p4,q1,(f /. q2),(f /. (q2 + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(p3,q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(L~ f) /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
dom f is V142() V143() V144() V145() V146() V147() Element of K6(NAT)
(TOP-REAL 2) | p3 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p3) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p3)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p3))) is set
j is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p3) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p3)))
j . 0 is set
j . 1 is set
rng j is Element of K6( the carrier of ((TOP-REAL 2) | p3))
K6( the carrier of ((TOP-REAL 2) | p3)) is set
[#] ((TOP-REAL 2) | p3) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | p3))
dom j is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
Q is set
j . Q is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
p1 is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | p4 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p4) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4))) is set
H is V11() V12() ext-real Element of REAL
p2 is V11() V12() ext-real Element of REAL
[.p2,H.] is V142() V143() V144() Element of K6(REAL)
j .: [.p2,H.] is Element of K6( the carrier of ((TOP-REAL 2) | p3))
j . p2 is set
j . H is set
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : ( p2 <= b₁ & b₁ <= H ) } is set
H is non empty Element of K6( the carrier of I[01])
I[01] | H is non empty strict TopSpace-like SubSpace of I[01]
the carrier of (I[01] | H) is non empty set
K7( the carrier of (I[01] | H), the carrier of ((TOP-REAL 2) | p4)) is set
K6(K7( the carrier of (I[01] | H), the carrier of ((TOP-REAL 2) | p4))) is set
j | H is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p3) -valued Function-like Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p3)))
x19 is non empty Relation-like the carrier of (I[01] | H) -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like total quasi_total Element of K6(K7( the carrier of (I[01] | H), the carrier of ((TOP-REAL 2) | p4)))
id H is non empty Relation-like H -defined H -valued Function-like one-to-one total quasi_total Element of K6(K7(H,H))
K7(H,H) is set
K6(K7(H,H)) is set
j * (id H) is Relation-like H -defined the carrier of ((TOP-REAL 2) | p3) -valued Function-like Element of K6(K7(H, the carrier of ((TOP-REAL 2) | p3)))
K7(H, the carrier of ((TOP-REAL 2) | p3)) is set
K6(K7(H, the carrier of ((TOP-REAL 2) | p3))) is set
Closed-Interval-TSpace (p2,H) is non empty strict TopSpace-like SubSpace of R^1
x1 is strict TopSpace-like SubSpace of I[01]
[#] x1 is non proper closed Element of K6( the carrier of x1)
the carrier of x1 is set
K6( the carrier of x1) is set
x19 /" is non empty Relation-like the carrier of ((TOP-REAL 2) | p4) -defined the carrier of (I[01] | H) -valued Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | p4), the carrier of (I[01] | H)))
K7( the carrier of ((TOP-REAL 2) | p4), the carrier of (I[01] | H)) is set
K6(K7( the carrier of ((TOP-REAL 2) | p4), the carrier of (I[01] | H))) is set
(dom j) /\ H is Element of K6( the carrier of I[01])
dom x19 is Element of K6( the carrier of (I[01] | H))
K6( the carrier of (I[01] | H)) is set
x19 . H is set
x29 is non empty Element of K6( the carrier of ((TOP-REAL 2) | p3))
((TOP-REAL 2) | p3) | x29 is non empty strict TopSpace-like SubSpace of (TOP-REAL 2) | p3
the carrier of (((TOP-REAL 2) | p3) | x29) is non empty set
[#] (((TOP-REAL 2) | p3) | x29) is non empty non proper closed Element of K6( the carrier of (((TOP-REAL 2) | p3) | x29))
K6( the carrier of (((TOP-REAL 2) | p3) | x29)) is set
F is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)))
F . 0 is set
F . 1 is set
s1 is V11() V12() ext-real Element of REAL
F . s1 is set
s2 is non empty Element of K6( the carrier of ((TOP-REAL 2) | p3))
((TOP-REAL 2) | p3) | s2 is non empty strict TopSpace-like SubSpace of (TOP-REAL 2) | p3
x2 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | x2 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
x19 . p2 is set
[#] (I[01] | H) is non empty non proper closed Element of K6( the carrier of (I[01] | H))
rng x19 is Element of K6( the carrier of ((TOP-REAL 2) | p4))
K6( the carrier of ((TOP-REAL 2) | p4)) is set
x19 .: (dom x19) is Element of K6( the carrier of ((TOP-REAL 2) | p4))
[#] (((TOP-REAL 2) | p3) | s2) is non empty non proper closed Element of K6( the carrier of (((TOP-REAL 2) | p3) | s2))
the carrier of (((TOP-REAL 2) | p3) | s2) is non empty set
K6( the carrier of (((TOP-REAL 2) | p3) | s2)) is set
ppi is V11() V12() ext-real Element of REAL
F . ppi is set
(x19 /") * F is non empty Relation-like the carrier of I[01] -defined the carrier of (I[01] | H) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (I[01] | H)))
K7( the carrier of I[01], the carrier of (I[01] | H)) is set
K6(K7( the carrier of I[01], the carrier of (I[01] | H))) is set
rng F is Element of K6( the carrier of ((TOP-REAL 2) | p4))
[#] ((TOP-REAL 2) | x2) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | x2))
the carrier of ((TOP-REAL 2) | x2) is non empty set
K6( the carrier of ((TOP-REAL 2) | x2)) is set
((x19 /") * F) . ppi is set
dom (x19 /") is Element of K6( the carrier of ((TOP-REAL 2) | p4))
rng ((x19 /") * F) is Element of K6( the carrier of (I[01] | H))
rng (x19 /") is Element of K6( the carrier of (I[01] | H))
the carrier of (Closed-Interval-TSpace (p2,H)) is non empty set
x19 " is Relation-like Function-like set
dom F is Element of K6( the carrier of I[01])
dom ((x19 /") * F) is Element of K6( the carrier of I[01])
K2 is set
j . K2 is set
j " is Relation-like Function-like set
(j ") . (F . ppi) is set
j /" is non empty Relation-like the carrier of ((TOP-REAL 2) | p3) -defined the carrier of I[01] -valued Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | p3), the carrier of I[01]))
K7( the carrier of ((TOP-REAL 2) | p3), the carrier of I[01]) is set
K6(K7( the carrier of ((TOP-REAL 2) | p3), the carrier of I[01])) is set
(j /") . (F . ppi) is set
dom (id H) is Element of K6(H)
K6(H) is set
dom (j /") is Element of K6( the carrier of ((TOP-REAL 2) | p3))
j . (((x19 /") * F) . ppi) is set
((x19 /") * F) (#) j is Relation-like Function-like set
(((x19 /") * F) (#) j) . ppi is set
(x19 /") (#) j is Relation-like Function-like set
F (#) ((x19 /") (#) j) is Relation-like Function-like set
(F (#) ((x19 /") (#) j)) . ppi is set
j * (x19 /") is Relation-like the carrier of ((TOP-REAL 2) | p4) -defined the carrier of ((TOP-REAL 2) | p3) -valued Function-like Element of K6(K7( the carrier of ((TOP-REAL 2) | p4), the carrier of ((TOP-REAL 2) | p3)))
K7( the carrier of ((TOP-REAL 2) | p4), the carrier of ((TOP-REAL 2) | p3)) is set
K6(K7( the carrier of ((TOP-REAL 2) | p4), the carrier of ((TOP-REAL 2) | p3))) is set
(j * (x19 /")) . (F . ppi) is set
(id H) " is Relation-like Function-like one-to-one set
(j ") (#) ((id H) ") is Relation-like Function-like set
((j ") (#) ((id H) ")) (#) j is Relation-like Function-like set
(((j ") (#) ((id H) ")) (#) j) . (F . ppi) is set
(j /") (#) ((id H) ") is Relation-like Function-like set
((j /") (#) ((id H) ")) (#) j is Relation-like Function-like set
(((j /") (#) ((id H) ")) (#) j) . (F . ppi) is set
((id H) ") (#) j is Relation-like Function-like set
(j /") (#) (((id H) ") (#) j) is Relation-like Function-like set
((j /") (#) (((id H) ") (#) j)) . (F . ppi) is set
(j /") (#) (j * (id H)) is Relation-like Function-like set
((j /") (#) (j * (id H))) . (F . ppi) is set
(j * (id H)) . ((j /") . (F . ppi)) is set
(id H) . ((j /") . (F . ppi)) is set
j . ((id H) . ((j /") . (F . ppi))) is set
j . ((j ") . (F . ppi)) is set
((x19 /") * F) . 1 is set
(x19 /") . (f /. (q2 + 1)) is set
((x19 /") * F) . 0 is set
(x19 /") . (f /. q2) is set
E is V11() V12() ext-real Element of REAL
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (p2,H))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (p2,H)))) is set
X1 is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (p2,H)) -valued Function-like total quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (p2,H))))
Poz is Element of the carrier of (Closed-Interval-TSpace (0,1))
X1 . Poz is Element of the carrier of (Closed-Interval-TSpace (p2,H))
j . p1 is set
X2 is set
j . X2 is set
x19 . p1 is set
(x19 ") . (F . s1) is set
(x19 /") . (F . s1) is set
pi1 is Element of the carrier of (Closed-Interval-TSpace (0,1))
X1 . pi1 is Element of the carrier of (Closed-Interval-TSpace (p2,H))
(LSeg (f,q2)) /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
LSeg ((f /. q2),(f /. (q2 + 1))) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
((L~ f),q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
q2 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,q2) is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (q2 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
((LSeg (f,q2)),q1,(f /. q2),(f /. (q2 + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
p4 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(p4,q1,(f /. q2),(f /. (q2 + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(p3,q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(L~ f) /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
dom f is V142() V143() V144() V145() V146() V147() Element of K6(NAT)
(TOP-REAL 2) | p3 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p3) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p3)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p3))) is set
j is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p3) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p3)))
j . 0 is set
j . 1 is set
rng j is Element of K6( the carrier of ((TOP-REAL 2) | p3))
K6( the carrier of ((TOP-REAL 2) | p3)) is set
[#] ((TOP-REAL 2) | p3) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | p3))
dom j is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
Q is set
j . Q is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
p1 is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | p4 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p4) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4))) is set
H is V11() V12() ext-real Element of REAL
p2 is V11() V12() ext-real Element of REAL
[.p2,H.] is V142() V143() V144() Element of K6(REAL)
j .: [.p2,H.] is Element of K6( the carrier of ((TOP-REAL 2) | p3))
j . p2 is set
j . H is set
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : ( p2 <= b₁ & b₁ <= H ) } is set
Closed-Interval-TSpace (p2,H) is non empty strict TopSpace-like SubSpace of R^1
H is non empty Element of K6( the carrier of I[01])
x19 is strict TopSpace-like SubSpace of I[01]
[#] x19 is non proper closed Element of K6( the carrier of x19)
the carrier of x19 is set
K6( the carrier of x19) is set
I[01] | H is non empty strict TopSpace-like SubSpace of I[01]
[#] (Closed-Interval-TSpace (p2,H)) is non empty non proper closed Element of K6( the carrier of (Closed-Interval-TSpace (p2,H)))
the carrier of (Closed-Interval-TSpace (p2,H)) is non empty set
K6( the carrier of (Closed-Interval-TSpace (p2,H))) is set
x1 is Element of K6( the carrier of x19)
x29 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)))
x29 . 0 is set
x29 . 1 is set
x2 is V11() V12() ext-real Element of REAL
x29 . x2 is set
x1 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | x1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | x1) is non empty set
[#] ((TOP-REAL 2) | x1) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | x1))
K6( the carrier of ((TOP-REAL 2) | x1)) is set
F is non empty Element of K6( the carrier of ((TOP-REAL 2) | x1))
rng x29 is Element of K6( the carrier of ((TOP-REAL 2) | p4))
K6( the carrier of ((TOP-REAL 2) | p4)) is set
s1 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | s1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
[#] ((TOP-REAL 2) | s1) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | s1))
the carrier of ((TOP-REAL 2) | s1) is non empty set
K6( the carrier of ((TOP-REAL 2) | s1)) is set
j | H is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p3) -valued Function-like Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p3)))
the carrier of (I[01] | H) is non empty set
[#] (I[01] | H) is non empty non proper closed Element of K6( the carrier of (I[01] | H))
K6( the carrier of (I[01] | H)) is set
K7( the carrier of (I[01] | H), the carrier of ((TOP-REAL 2) | p3)) is set
K6(K7( the carrier of (I[01] | H), the carrier of ((TOP-REAL 2) | p3))) is set
pi1 is V11() V12() ext-real Element of REAL
x29 . pi1 is set
ppi is non empty Relation-like the carrier of (I[01] | H) -defined the carrier of ((TOP-REAL 2) | p3) -valued Function-like total quasi_total Element of K6(K7( the carrier of (I[01] | H), the carrier of ((TOP-REAL 2) | p3)))
rng ppi is Element of K6( the carrier of ((TOP-REAL 2) | p3))
Poz is set
dom ppi is Element of K6( the carrier of (I[01] | H))
G is set
ppi . G is set
(dom j) /\ H is Element of K6( the carrier of I[01])
j . G is set
((TOP-REAL 2) | x1) | F is non empty strict TopSpace-like SubSpace of (TOP-REAL 2) | x1
the carrier of (((TOP-REAL 2) | x1) | F) is non empty set
[#] (((TOP-REAL 2) | x1) | F) is non empty non proper closed Element of K6( the carrier of (((TOP-REAL 2) | x1) | F))
K6( the carrier of (((TOP-REAL 2) | x1) | F)) is set
Poz is non empty Element of K6( the carrier of ((TOP-REAL 2) | x1))
((TOP-REAL 2) | x1) | Poz is non empty strict TopSpace-like SubSpace of (TOP-REAL 2) | x1
the carrier of (((TOP-REAL 2) | x1) | Poz) is non empty set
K7( the carrier of (I[01] | H), the carrier of (((TOP-REAL 2) | x1) | Poz)) is set
K6(K7( the carrier of (I[01] | H), the carrier of (((TOP-REAL 2) | x1) | Poz))) is set
K7( the carrier of (I[01] | H), the carrier of ((TOP-REAL 2) | s1)) is set
K6(K7( the carrier of (I[01] | H), the carrier of ((TOP-REAL 2) | s1))) is set
G is non empty Relation-like the carrier of (I[01] | H) -defined the carrier of (((TOP-REAL 2) | x1) | Poz) -valued Function-like total quasi_total Element of K6(K7( the carrier of (I[01] | H), the carrier of (((TOP-REAL 2) | x1) | Poz)))
K1 is non empty Relation-like the carrier of (I[01] | H) -defined the carrier of ((TOP-REAL 2) | s1) -valued Function-like total quasi_total Element of K6(K7( the carrier of (I[01] | H), the carrier of ((TOP-REAL 2) | s1)))
dom K1 is Element of K6( the carrier of (I[01] | H))
rng K1 is Element of K6( the carrier of ((TOP-REAL 2) | s1))
K1 .: (dom K1) is Element of K6( the carrier of ((TOP-REAL 2) | s1))
[#] (((TOP-REAL 2) | x1) | Poz) is non empty non proper closed Element of K6( the carrier of (((TOP-REAL 2) | x1) | Poz))
K6( the carrier of (((TOP-REAL 2) | x1) | Poz)) is set
K1 /" is non empty Relation-like the carrier of ((TOP-REAL 2) | s1) -defined the carrier of (I[01] | H) -valued Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | s1), the carrier of (I[01] | H)))
K7( the carrier of ((TOP-REAL 2) | s1), the carrier of (I[01] | H)) is set
K6(K7( the carrier of ((TOP-REAL 2) | s1), the carrier of (I[01] | H))) is set
(K1 /") * x29 is Relation-like the carrier of I[01] -defined the carrier of (I[01] | H) -valued Function-like Element of K6(K7( the carrier of I[01], the carrier of (I[01] | H)))
K7( the carrier of I[01], the carrier of (I[01] | H)) is set
K6(K7( the carrier of I[01], the carrier of (I[01] | H))) is set
dom (K1 /") is Element of K6( the carrier of ((TOP-REAL 2) | s1))
rng ((K1 /") * x29) is Element of K6( the carrier of (I[01] | H))
rng (K1 /") is Element of K6( the carrier of (I[01] | H))
dom x29 is Element of K6( the carrier of I[01])
dom ((K1 /") * x29) is Element of K6( the carrier of I[01])
E is set
j . E is set
K1 " is Relation-like Function-like set
j " is Relation-like Function-like set
(j ") . (x29 . pi1) is set
j . p1 is set
X1 is set
j . X1 is set
K1 . p1 is set
(K1 ") . (x29 . x2) is set
(K1 /") . (x29 . x2) is set
id H is non empty Relation-like H -defined H -valued Function-like one-to-one total quasi_total Element of K6(K7(H,H))
K7(H,H) is set
K6(K7(H,H)) is set
j * (id H) is Relation-like H -defined the carrier of ((TOP-REAL 2) | p3) -valued Function-like Element of K6(K7(H, the carrier of ((TOP-REAL 2) | p3)))
K7(H, the carrier of ((TOP-REAL 2) | p3)) is set
K6(K7(H, the carrier of ((TOP-REAL 2) | p3))) is set
((K1 /") * x29) . pi1 is set
ss9 is V11() V12() ext-real Element of REAL
j /" is non empty Relation-like the carrier of ((TOP-REAL 2) | p3) -defined the carrier of I[01] -valued Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | p3), the carrier of I[01]))
K7( the carrier of ((TOP-REAL 2) | p3), the carrier of I[01]) is set
K6(K7( the carrier of ((TOP-REAL 2) | p3), the carrier of I[01])) is set
(j /") . (x29 . pi1) is set
dom (id H) is Element of K6(H)
K6(H) is set
dom (j /") is Element of K6( the carrier of ((TOP-REAL 2) | p3))
j . (((K1 /") * x29) . pi1) is set
((K1 /") * x29) (#) j is Relation-like Function-like set
(((K1 /") * x29) (#) j) . pi1 is set
(K1 /") (#) j is Relation-like Function-like set
x29 (#) ((K1 /") (#) j) is Relation-like Function-like set
(x29 (#) ((K1 /") (#) j)) . pi1 is set
j * (K1 /") is Relation-like the carrier of ((TOP-REAL 2) | s1) -defined the carrier of ((TOP-REAL 2) | p3) -valued Function-like Element of K6(K7( the carrier of ((TOP-REAL 2) | s1), the carrier of ((TOP-REAL 2) | p3)))
K7( the carrier of ((TOP-REAL 2) | s1), the carrier of ((TOP-REAL 2) | p3)) is set
K6(K7( the carrier of ((TOP-REAL 2) | s1), the carrier of ((TOP-REAL 2) | p3))) is set
(j * (K1 /")) . (x29 . pi1) is set
(K1 ") (#) j is Relation-like Function-like set
((K1 ") (#) j) . (x29 . pi1) is set
(id H) " is Relation-like Function-like one-to-one set
(j ") (#) ((id H) ") is Relation-like Function-like set
((j ") (#) ((id H) ")) (#) j is Relation-like Function-like set
(((j ") (#) ((id H) ")) (#) j) . (x29 . pi1) is set
(j /") (#) ((id H) ") is Relation-like Function-like set
((j /") (#) ((id H) ")) (#) j is Relation-like Function-like set
(((j /") (#) ((id H) ")) (#) j) . (x29 . pi1) is set
((id H) ") (#) j is Relation-like Function-like set
(j /") (#) (((id H) ") (#) j) is Relation-like Function-like set
((j /") (#) (((id H) ") (#) j)) . (x29 . pi1) is set
(j /") (#) (j * (id H)) is Relation-like Function-like set
((j /") (#) (j * (id H))) . (x29 . pi1) is set
(j * (id H)) . ((j /") . (x29 . pi1)) is set
(id H) . ((j /") . (x29 . pi1)) is set
j . ((id H) . ((j /") . (x29 . pi1))) is set
(id H) . ((j ") . (x29 . pi1)) is set
j . ((id H) . ((j ") . (x29 . pi1))) is set
j . ((j ") . (x29 . pi1)) is set
(dom j) /\ H is Element of K6( the carrier of I[01])
K1 . H is set
K1 . p2 is set
((K1 /") * x29) . 1 is set
(K1 /") . (f /. (q2 + 1)) is set
((K1 /") * x29) . 0 is set
(K1 /") . (f /. q2) is set
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (p2,H))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (p2,H)))) is set
H is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (p2,H)) -valued Function-like total quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (p2,H))))
X1 is Element of the carrier of (Closed-Interval-TSpace (0,1))
H . X1 is Element of the carrier of (Closed-Interval-TSpace (p2,H))
X2 is Element of the carrier of (Closed-Interval-TSpace (0,1))
H . X2 is Element of the carrier of (Closed-Interval-TSpace (p2,H))
(LSeg (f,q2)) /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
LSeg ((f /. q2),(f /. (q2 + 1))) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
q1 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,q1) is functional closed Element of K6( the carrier of (TOP-REAL 2))
((L~ f),(LSeg (f,q1)),(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
f /. (q1 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
LSeg ((f /. q1),(f /. (q1 + 1))) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
((L~ f),q2,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(q2,q2,(f /. q1),(f /. (q1 + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
q1 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,q1) is functional closed Element of K6( the carrier of (TOP-REAL 2))
((L~ f),(LSeg (f,q1)),(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (q1 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
f /. q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
LSeg ((f /. q1),(f /. (q1 + 1))) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
((L~ f),q2,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(q2,q2,(f /. q1),(f /. (q1 + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
q1 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (q1 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
dom f is V142() V143() V144() V145() V146() V147() Element of K6(NAT)
i is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | i is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | i) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | i)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | i))) is set
j is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | i) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | i)))
j . 0 is set
j . 1 is set
Q is V11() V12() ext-real Element of REAL
j . Q is set
p1 is V11() V12() ext-real Element of REAL
j . p1 is set
dom j is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
LSeg (f,q1) is functional closed Element of K6( the carrier of (TOP-REAL 2))
H is V11() V12() ext-real Element of REAL
p2 is V11() V12() ext-real Element of REAL
[.p2,H.] is V142() V143() V144() Element of K6(REAL)
j .: [.p2,H.] is Element of K6( the carrier of ((TOP-REAL 2) | i))
K6( the carrier of ((TOP-REAL 2) | i)) is set
j . p2 is set
j . H is set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
q2 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is V10() ext-real set
q1 + p3 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
p4 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
P is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
q1 + P is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. (q1 + P) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
q1 + (P + 1) is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. (q1 + (P + 1)) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(q1 + P) + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
q1 + 0 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. (q1 + 0) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
dom f is V142() V143() V144() V145() V146() V147() Element of K6(NAT)
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,p3) is functional closed Element of K6( the carrier of (TOP-REAL 2))
p3 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (p3 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
((LSeg (f,p3)),q1,(f /. p3),(f /. (p3 + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(p4,q1,(f /. p3),(f /. (p3 + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
dom f is V142() V143() V144() V145() V146() V147() Element of K6(NAT)
(TOP-REAL 2) | p4 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p4) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4))) is set
Q is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)))
Q . 0 is set
Q . 1 is set
p1 is V11() V12() ext-real Element of REAL
Q . p1 is set
p2 is V11() V12() ext-real Element of REAL
Q . p2 is set
LSeg ((f /. p3),(f /. (p3 + 1))) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
((L~ f),q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,p3) is functional closed Element of K6( the carrier of (TOP-REAL 2))
p3 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (p3 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(LSeg (f,p3)) /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
p4 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(p4,q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(P,q1,(f /. p3),(f /. (p3 + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,p3) is functional closed Element of K6( the carrier of (TOP-REAL 2))
p3 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (p3 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
((LSeg (f,p3)),q1,(f /. p3),(f /. (p3 + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(p4,q1,(f /. p3),(f /. (p3 + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
dom f is V142() V143() V144() V145() V146() V147() Element of K6(NAT)
(TOP-REAL 2) | p4 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p4) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4))) is set
Q is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)))
Q . 0 is set
Q . 1 is set
p1 is V11() V12() ext-real Element of REAL
Q . p1 is set
p2 is V11() V12() ext-real Element of REAL
Q . p2 is set
LSeg ((f /. p3),(f /. (p3 + 1))) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
((L~ f),q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,p3) is functional closed Element of K6( the carrier of (TOP-REAL 2))
p3 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (p3 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(LSeg (f,p3)) /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
p4 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(p4,q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(P,q1,(f /. p3),(f /. (p3 + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
q2 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,q2) is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
dom f is V142() V143() V144() V145() V146() V147() Element of K6(NAT)
i is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | i is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | i) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | i)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | i))) is set
j is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | i) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | i)))
j . 0 is set
j . 1 is set
Q is V11() V12() ext-real Element of REAL
j . Q is set
p1 is V11() V12() ext-real Element of REAL
j . p1 is set
dom j is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
f /. (q2 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
H is V11() V12() ext-real Element of REAL
p2 is V11() V12() ext-real Element of REAL
[.p2,H.] is V142() V143() V144() Element of K6(REAL)
j .: [.p2,H.] is Element of K6( the carrier of ((TOP-REAL 2) | i))
K6( the carrier of ((TOP-REAL 2) | i)) is set
j . p2 is set
j . H is set
H is set
j . H is set
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : ( p2 <= b₁ & b₁ <= H ) } is set
x19 is V11() V12() ext-real Element of REAL
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
q2 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,q2) is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. (q2 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | p3 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p3) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p3)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p3))) is set
j is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p3) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p3)))
j . 0 is set
j . 1 is set
Q is V11() V12() ext-real Element of REAL
j . Q is set
p1 is V11() V12() ext-real Element of REAL
j . p1 is set
dom j is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
f /. q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
H is V11() V12() ext-real Element of REAL
p2 is V11() V12() ext-real Element of REAL
[.p2,H.] is V142() V143() V144() Element of K6(REAL)
j .: [.p2,H.] is Element of K6( the carrier of ((TOP-REAL 2) | p3))
K6( the carrier of ((TOP-REAL 2) | p3)) is set
j . p2 is set
j . H is set
H is set
j . H is set
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : ( p2 <= b₁ & b₁ <= H ) } is set
x19 is V11() V12() ext-real Element of REAL
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
((L~ f),q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,p3) is functional closed Element of K6( the carrier of (TOP-REAL 2))
p3 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
p4 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,p4) is functional closed Element of K6( the carrier of (TOP-REAL 2))
p4 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (p3 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(P,q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(L~ f) /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
f /. (p4 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is functional Element of K6( the carrier of (TOP-REAL 2))
((L~ f),q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,p3) is functional closed Element of K6( the carrier of (TOP-REAL 2))
p3 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
p4 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,p4) is functional closed Element of K6( the carrier of (TOP-REAL 2))
p4 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (p3 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(P,q1,(f /. 1),(f /. (len f))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. p4 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(L~ f) /\ q1 is functional Element of K6( the carrier of (TOP-REAL 2))
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p3 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,p3) is functional closed Element of K6( the carrier of (TOP-REAL 2))
p3 + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. p3 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (p3 + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p4 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | p4 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p4) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4))) is set
i is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)))
i . 0 is set
i . 1 is set
Q is V11() V12() ext-real Element of REAL
j is V11() V12() ext-real Element of REAL
[.j,Q.] is V142() V143() V144() Element of K6(REAL)
i .: [.j,Q.] is Element of K6( the carrier of ((TOP-REAL 2) | p4))
K6( the carrier of ((TOP-REAL 2) | p4)) is set
i . j is set
i . Q is set
(#) (j,Q) is Element of the carrier of (Closed-Interval-TSpace (j,Q))
Closed-Interval-TSpace (j,Q) is non empty strict TopSpace-like SubSpace of R^1
the carrier of (Closed-Interval-TSpace (j,Q)) is non empty set
(j,Q) (#) is Element of the carrier of (Closed-Interval-TSpace (j,Q))
L[01] (((#) (j,Q)),((j,Q) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (j,Q)) -valued Function-like total quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (j,Q))))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (j,Q))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (j,Q)))) is set
rng (L[01] (((#) (j,Q)),((j,Q) (#)))) is Element of K6( the carrier of (Closed-Interval-TSpace (j,Q)))
K6( the carrier of (Closed-Interval-TSpace (j,Q))) is set
[#] (Closed-Interval-TSpace (j,Q)) is non empty non proper closed Element of K6( the carrier of (Closed-Interval-TSpace (j,Q)))
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : ( j <= b₁ & b₁ <= Q ) } is set
K6( the carrier of I[01]) is set
p2 is non empty Element of K6( the carrier of I[01])
I[01] | p2 is non empty strict TopSpace-like SubSpace of I[01]
the carrier of (I[01] | p2) is non empty set
P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
K7( the carrier of (I[01] | p2), the carrier of ((TOP-REAL 2) | P)) is set
K6(K7( the carrier of (I[01] | p2), the carrier of ((TOP-REAL 2) | P))) is set
i | p2 is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p4) -valued Function-like Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | p4)))
H is non empty Relation-like the carrier of (I[01] | p2) -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like total quasi_total Element of K6(K7( the carrier of (I[01] | p2), the carrier of ((TOP-REAL 2) | P)))
H * (L[01] (((#) (j,Q)),((j,Q) (#)))) is Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | P)))
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | P)) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL 2) | P))) is set
dom H is Element of K6( the carrier of (I[01] | p2))
K6( the carrier of (I[01] | p2)) is set
[#] (I[01] | p2) is non empty non proper closed Element of K6( the carrier of (I[01] | p2))
rng (H * (L[01] (((#) (j,Q)),((j,Q) (#))))) is Element of K6( the carrier of ((TOP-REAL 2) | P))
K6( the carrier of ((TOP-REAL 2) | P)) is set
rng H is Element of K6( the carrier of ((TOP-REAL 2) | P))
(TOP-REAL 2) | (LSeg (f,p3)) is strict TopSpace-like SubSpace of TOP-REAL 2
[#] ((TOP-REAL 2) | (LSeg (f,p3))) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (LSeg (f,p3))))
the carrier of ((TOP-REAL 2) | (LSeg (f,p3))) is set
K6( the carrier of ((TOP-REAL 2) | (LSeg (f,p3)))) is set
(L[01] (((#) (j,Q)),((j,Q) (#)))) . 1 is set
(L[01] (((#) (j,Q)),((j,Q) (#)))) . ((0,1) (#)) is Element of the carrier of (Closed-Interval-TSpace (j,Q))
dom (H * (L[01] (((#) (j,Q)),((j,Q) (#))))) is Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
K6( the carrier of (Closed-Interval-TSpace (0,1))) is set
dom (L[01] (((#) (j,Q)),((j,Q) (#)))) is Element of K6( the carrier of (Closed-Interval-TSpace (0,1)))
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
x19 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
rng x19 is Element of K6( the carrier of ((TOP-REAL 2) | P))
dom x19 is Element of K6( the carrier of I[01])
x1 is set
x19 . x1 is set
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
x29 is V11() V12() ext-real Element of REAL
(L[01] (((#) (j,Q)),((j,Q) (#)))) . x29 is set
x19 . 1 is set
H . Q is set
(L[01] (((#) (j,Q)),((j,Q) (#)))) . 0 is set
(L[01] (((#) (j,Q)),((j,Q) (#)))) . ((#) (0,1)) is Element of the carrier of (Closed-Interval-TSpace (j,Q))
x2 is set
x19 . x2 is set
F is V11() V12() ext-real Element of REAL
(L[01] (((#) (j,Q)),((j,Q) (#)))) . F is set
s1 is Element of the carrier of (Closed-Interval-TSpace (0,1))
(L[01] (((#) (j,Q)),((j,Q) (#)))) . s1 is Element of the carrier of (Closed-Interval-TSpace (j,Q))
s2 is Element of the carrier of (Closed-Interval-TSpace (0,1))
(L[01] (((#) (j,Q)),((j,Q) (#)))) . s2 is Element of the carrier of (Closed-Interval-TSpace (j,Q))
H . ((L[01] (((#) (j,Q)),((j,Q) (#)))) . F) is set
i . ((L[01] (((#) (j,Q)),((j,Q) (#)))) . F) is set
Poz is TopSpace-like SubSpace of I[01]
the carrier of Poz is set
G is TopSpace-like SubSpace of I[01]
the carrier of G is set
H . ((L[01] (((#) (j,Q)),((j,Q) (#)))) . x29) is set
i . ((L[01] (((#) (j,Q)),((j,Q) (#)))) . x29) is set
pi1 is V11() V12() ext-real Element of REAL
x19 . 0 is set
H . j is set
ppi is V11() V12() ext-real Element of REAL
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is functional closed Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
len f is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. (len f) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q1 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
q2 is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
i is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,i) is functional closed Element of K6( the carrier of (TOP-REAL 2))
j is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,j) is functional closed Element of K6( the carrier of (TOP-REAL 2))
i + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
j + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. i is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (i + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
Q is V10() ext-real set
(j + 1) + Q is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
f /. (j + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
p1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
(j + 1) + p1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
f /. ((j + 1) + p1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
dom f is V142() V143() V144() V145() V146() V147() Element of K6(NAT)
LSeg ((f /. i),(f /. (i + 1))) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
i is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
i + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,i) is functional closed Element of K6( the carrier of (TOP-REAL 2))
j is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
j + 1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
LSeg (f,j) is functional closed Element of K6( the carrier of (TOP-REAL 2))
Q is V10() ext-real set
(i + 1) + Q is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
p1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
(i + 1) + p1 is V10() V11() V12() ext-real V79() V80() V142() V143() V144() V145() V146() V147() Element of NAT
P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
f /. (i + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. ((i + 1) + p1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. i is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
f /. (i + 1) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
dom f is V142() V143() V144() V145() V146() V147() Element of K6(NAT)
LSeg ((f /. i),(f /. (i + 1))) is functional closed compact Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (LSeg ((f /. i),(f /. (i + 1)))) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (LSeg ((f /. i),(f /. (i + 1))))) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((f /. i),(f /. (i + 1)))))) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((f /. i),(f /. (i + 1))))))) is set
H is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (LSeg ((f /. i),(f /. (i + 1))))) -valued Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((f /. i),(f /. (i + 1)))))))
H . 0 is set
H . 1 is set
Q is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | Q is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | Q) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | Q)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | Q))) is set
P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
H is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | Q) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | Q)))
rng H is Element of K6( the carrier of ((TOP-REAL 2) | Q))
K6( the carrier of ((TOP-REAL 2) | Q)) is set
(TOP-REAL 2) | (LSeg (f,i)) is strict TopSpace-like SubSpace of TOP-REAL 2
[#] ((TOP-REAL 2) | (LSeg (f,i))) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (LSeg (f,i))))
the carrier of ((TOP-REAL 2) | (LSeg (f,i))) is set
K6( the carrier of ((TOP-REAL 2) | (LSeg (f,i)))) is set
dom H is Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
x19 is set
H . x19 is set
[#] I[01] is non empty non proper closed Element of K6( the carrier of I[01])
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
x1 is V11() V12() ext-real Element of REAL
x29 is set
H . x29 is set
x2 is V11() V12() ext-real Element of REAL
1 - x2 is V11() V12() ext-real Element of REAL
(1 - x2) * (f /. i) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
x2 * (f /. (i + 1)) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
((1 - x2) * (f /. i)) + (x2 * (f /. (i + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
1 - x1 is V11() V12() ext-real Element of REAL
(1 - x1) * (f /. i) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
x1 * (f /. (i + 1)) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
((1 - x1) * (f /. i)) + (x1 * (f /. (i + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
H . 0 is set
1 - 0 is V11() V12() ext-real Element of REAL
(1 - 0) * (f /. i) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
0 * (f /. (i + 1)) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
((1 - 0) * (f /. i)) + (0 * (f /. (i + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(f /. i) + (0 * (f /. (i + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
0. (TOP-REAL 2) is Relation-like Function-like V43(2) V52( TOP-REAL 2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(f /. i) + (0. (TOP-REAL 2)) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
F is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
F . 0 is set
F . 1 is set
s1 is V11() V12() ext-real Element of REAL
F . s1 is set
s2 is V11() V12() ext-real Element of REAL
F . s2 is set
pi1 is V11() V12() ext-real Element of REAL
ppi is V11() V12() ext-real Element of REAL
[.ppi,pi1.] is V142() V143() V144() Element of K6(REAL)
F .: [.ppi,pi1.] is Element of K6( the carrier of ((TOP-REAL 2) | P))
K6( the carrier of ((TOP-REAL 2) | P)) is set
F . ppi is set
F . pi1 is set
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : ( ppi <= b₁ & b₁ <= pi1 ) } is set
Poz is non empty Element of K6( the carrier of I[01])
I[01] | Poz is non empty strict TopSpace-like SubSpace of I[01]
the carrier of (I[01] | Poz) is non empty set
K7( the carrier of (I[01] | Poz), the carrier of ((TOP-REAL 2) | Q)) is set
K6(K7( the carrier of (I[01] | Poz), the carrier of ((TOP-REAL 2) | Q))) is set
F | Poz is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
G is non empty Relation-like the carrier of (I[01] | Poz) -defined the carrier of ((TOP-REAL 2) | Q) -valued Function-like total quasi_total Element of K6(K7( the carrier of (I[01] | Poz), the carrier of ((TOP-REAL 2) | Q)))
dom F is Element of K6( the carrier of I[01])
Closed-Interval-TSpace (ppi,pi1) is non empty strict TopSpace-like SubSpace of R^1
K1 is TopSpace-like SubSpace of I[01]
the carrier of K1 is set
[#] (I[01] | Poz) is non empty non proper closed Element of K6( the carrier of (I[01] | Poz))
K6( the carrier of (I[01] | Poz)) is set
K2 is TopSpace-like SubSpace of I[01]
the carrier of K2 is set
the carrier of (Closed-Interval-TSpace (ppi,pi1)) is non empty set
K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (ppi,pi1))) is set
K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (ppi,pi1)))) is set
G /" is non empty Relation-like the carrier of ((TOP-REAL 2) | Q) -defined the carrier of (I[01] | Poz) -valued Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | Q), the carrier of (I[01] | Poz)))
K7( the carrier of ((TOP-REAL 2) | Q), the carrier of (I[01] | Poz)) is set
K6(K7( the carrier of ((TOP-REAL 2) | Q), the carrier of (I[01] | Poz))) is set
(G /") * H is non empty Relation-like the carrier of I[01] -defined the carrier of (I[01] | Poz) -valued Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (I[01] | Poz)))
K7( the carrier of I[01], the carrier of (I[01] | Poz)) is set
K6(K7( the carrier of I[01], the carrier of (I[01] | Poz))) is set
rng G is Element of K6( the carrier of ((TOP-REAL 2) | Q))
G " is Relation-like Function-like set
x is set
F . x is set
G . s2 is set
dom G is Element of K6( the carrier of (I[01] | Poz))
x is set
F . x is set
H . x2 is set
(G /") . (H . x2) is set
E is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (ppi,pi1)) -valued Function-like total quasi_total Element of K6(K7( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (ppi,pi1))))
E . x2 is set
X2 is Element of the carrier of (Closed-Interval-TSpace (0,1))
E . X2 is Element of the carrier of (Closed-Interval-TSpace (ppi,pi1))
x is set
F . x is set
G . s1 is set
H . 1 is set
1 - 1 is V11() V12() ext-real Element of REAL
(1 - 1) * (f /. i) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
1 * (f /. (i + 1)) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
((1 - 1) * (f /. i)) + (1 * (f /. (i + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(0. (TOP-REAL 2)) + (1 * (f /. (i + 1))) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
(0. (TOP-REAL 2)) + (f /. (i + 1)) is Relation-like Function-like V43(2) FinSequence-like V134() Element of the carrier of (TOP-REAL 2)
H . x1 is set
(G /") . (H . x1) is set
E . x1 is set
X1 is Element of the carrier of (Closed-Interval-TSpace (0,1))
E . X1 is Element of the carrier of (Closed-Interval-TSpace (ppi,pi1))
G . pi1 is set
(G /") . (H . 1) is set
E . 1 is set
G . ppi is set
(G /") . (H . 0) is set
E . 0 is set