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

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

(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

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

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,