:: JORDAN5B semantic presentation

REAL is V45() V46() V47() V51() V63() V64() V66() set

NAT is V45() V46() V47() V48() V49() V50() V51() V63() Element of K19(REAL)

K19(REAL) is set

COMPLEX is V45() V51() set

RAT is V45() V46() V47() V48() V51() set

INT is V45() V46() V47() V48() V49() V51() set

omega is V45() V46() V47() V48() V49() V50() V51() V63() set

K19(omega) is set

K19(NAT) is set

K20(COMPLEX,COMPLEX) is V33() set

K19(K20(COMPLEX,COMPLEX)) is set

K20(COMPLEX,REAL) is V33() V34() V35() set

K19(K20(COMPLEX,REAL)) is set

I[01] is non empty strict TopSpace-like V145() TopStruct

the carrier of I[01] is non empty V45() V46() V47() set

1 is non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() Element of NAT

K20(1,1) is RAT -valued INT -valued V33() V34() V35() V36() set

K19(K20(1,1)) is set

K20(K20(1,1),1) is RAT -valued INT -valued V33() V34() V35() V36() set

K19(K20(K20(1,1),1)) is set

K20(K20(1,1),REAL) is V33() V34() V35() set

K19(K20(K20(1,1),REAL)) is set

K20(REAL,REAL) is V33() V34() V35() set

K20(K20(REAL,REAL),REAL) is V33() V34() V35() set

K19(K20(K20(REAL,REAL),REAL)) is set

2 is non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() Element of NAT

K20(2,2) is RAT -valued INT -valued V33() V34() V35() V36() set

K20(K20(2,2),REAL) is V33() V34() V35() set

K19(K20(K20(2,2),REAL)) is set

RealSpace is non empty strict Reflexive discerning V138() triangle Discerning V145() MetrStruct

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

0 is Function-like functional empty natural V28() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() V63() V66() Element of NAT

the Function-like functional empty V45() V46() V47() V48() V49() V50() V51() V63() V66() set is Function-like functional empty V45() V46() V47() V48() V49() V50() V51() V63() V66() set

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

the carrier of (Closed-Interval-TSpace (0,1)) is non empty V45() V46() V47() set

K19(K20(REAL,REAL)) is set

TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() RLTopStruct

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

K238( the carrier of (TOP-REAL 2)) is M12( the carrier of (TOP-REAL 2))

K19( the carrier of (TOP-REAL 2)) is set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is V33() set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set

K20(RAT,RAT) is RAT -valued V33() V34() V35() set

K19(K20(RAT,RAT)) is set

K20(K20(RAT,RAT),RAT) is RAT -valued V33() V34() V35() set

K19(K20(K20(RAT,RAT),RAT)) is set

K20(INT,INT) is RAT -valued INT -valued V33() V34() V35() set

K19(K20(INT,INT)) is set

K20(K20(INT,INT),INT) is RAT -valued INT -valued V33() V34() V35() set

K19(K20(K20(INT,INT),INT)) is set

K20(NAT,NAT) is RAT -valued INT -valued V33() V34() V35() V36() set

K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued V33() V34() V35() V36() set

K19(K20(K20(NAT,NAT),NAT)) is set

K692() is non empty V160() L10()

the carrier of K692() is non empty set

K697() is non empty L10()

K698() is non empty V160() M29(K697())

K699() is non empty V160() V236() V272() M32(K697(),K698())

K701() is non empty V160() V236() V238() V240() L10()

K702() is non empty V160() V236() V272() M29(K701())

{} is Function-like functional empty V45() V46() V47() V48() V49() V50() V51() V63() V66() set

[.0,1.] is V45() V46() V47() V66() Element of K19(REAL)

0[01] is V28() real ext-real Element of the carrier of I[01]

1[01] is V28() real ext-real Element of the carrier of I[01]

TopSpaceMetr RealSpace is TopStruct

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

the carrier of I[01] is non empty V45() V46() V47() set

(#) (0,1) is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

(0,1) (#) is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

K20( the carrier of I[01], the carrier of I[01]) is V33() V34() V35() set

K19(K20( the carrier of I[01], the carrier of I[01])) is set

len {} is V67() set

f is natural V28() real ext-real set

f -' 1 is natural V28() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

f - 0 is V28() real ext-real Element of REAL

f - 1 is V28() real ext-real Element of REAL

f is natural V28() real ext-real set

f + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

j is natural V28() real ext-real set

j -' f is natural V28() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

(f + 1) -' f is natural V28() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

f is natural V28() real ext-real set

j is natural V28() real ext-real set

j -' f is natural V28() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

(j -' f) + 1 is non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() Element of NAT

j -' 1 is natural V28() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

(j -' 1) + 1 is non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() Element of NAT

f is V28() real ext-real set

1 - f is V28() real ext-real Element of REAL

1 - 1 is V28() real ext-real Element of REAL

1 - 0 is non empty V28() real ext-real positive non negative Element of REAL

f is V28() real ext-real set

1 - f is V28() real ext-real Element of REAL

f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

f `2 is V28() real ext-real Element of REAL

j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

j `2 is V28() real ext-real Element of REAL

P is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

LSeg (f,j) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))

{ (((1 - b

P `2 is V28() real ext-real Element of REAL

p is V28() real ext-real Element of REAL

1 - p is V28() real ext-real Element of REAL

(1 - p) * f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K677(f,(1 - p)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

p * j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K677(j,p) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

((1 - p) * f) + (p * j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K671(((1 - p) * f),(p * j)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

((1 - p) * f) `1 is V28() real ext-real Element of REAL

(p * j) `1 is V28() real ext-real Element of REAL

(((1 - p) * f) `1) + ((p * j) `1) is V28() real ext-real Element of REAL

((1 - p) * f) `2 is V28() real ext-real Element of REAL

(p * j) `2 is V28() real ext-real Element of REAL

(((1 - p) * f) `2) + ((p * j) `2) is V28() real ext-real Element of REAL

|[((((1 - p) * f) `1) + ((p * j) `1)),((((1 - p) * f) `2) + ((p * j) `2))]| is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

f `1 is V28() real ext-real Element of REAL

(1 - p) * (f `1) is V28() real ext-real Element of REAL

(1 - p) * (f `2) is V28() real ext-real Element of REAL

|[((1 - p) * (f `1)),((1 - p) * (f `2))]| is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

j `1 is V28() real ext-real Element of REAL

p * (j `1) is V28() real ext-real Element of REAL

p * (j `2) is V28() real ext-real Element of REAL

|[(p * (j `1)),(p * (j `2))]| is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

((1 - p) * (f `2)) + ((p * j) `2) is V28() real ext-real Element of REAL

((1 - p) * (f `2)) + (p * (j `2)) is V28() real ext-real Element of REAL

1 - (1 - p) is V28() real ext-real Element of REAL

(1 - (1 - p)) * (f `2) is V28() real ext-real Element of REAL

1 * f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K677(f,1) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

0. (TOP-REAL 2) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like V87( TOP-REAL 2) Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

(1 * f) + (0. (TOP-REAL 2)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K671((1 * f),(0. (TOP-REAL 2))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

f + (0. (TOP-REAL 2)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K671(f,(0. (TOP-REAL 2))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

f `1 is V28() real ext-real Element of REAL

j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

j `1 is V28() real ext-real Element of REAL

P is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

LSeg (f,j) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))

{ (((1 - b

P `1 is V28() real ext-real Element of REAL

p is V28() real ext-real Element of REAL

1 - p is V28() real ext-real Element of REAL

(1 - p) * f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K677(f,(1 - p)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

p * j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K677(j,p) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

((1 - p) * f) + (p * j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K671(((1 - p) * f),(p * j)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

((1 - p) * f) `1 is V28() real ext-real Element of REAL

(p * j) `1 is V28() real ext-real Element of REAL

(((1 - p) * f) `1) + ((p * j) `1) is V28() real ext-real Element of REAL

((1 - p) * f) `2 is V28() real ext-real Element of REAL

(p * j) `2 is V28() real ext-real Element of REAL

(((1 - p) * f) `2) + ((p * j) `2) is V28() real ext-real Element of REAL

|[((((1 - p) * f) `1) + ((p * j) `1)),((((1 - p) * f) `2) + ((p * j) `2))]| is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

(1 - p) * (f `1) is V28() real ext-real Element of REAL

f `2 is V28() real ext-real Element of REAL

(1 - p) * (f `2) is V28() real ext-real Element of REAL

|[((1 - p) * (f `1)),((1 - p) * (f `2))]| is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

p * (j `1) is V28() real ext-real Element of REAL

j `2 is V28() real ext-real Element of REAL

p * (j `2) is V28() real ext-real Element of REAL

|[(p * (j `1)),(p * (j `2))]| is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

((1 - p) * (f `1)) + ((p * j) `1) is V28() real ext-real Element of REAL

((1 - p) * (f `1)) + (p * (j `1)) is V28() real ext-real Element of REAL

1 - (1 - p) is V28() real ext-real Element of REAL

(1 - (1 - p)) * (f `1) is V28() real ext-real Element of REAL

1 * f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K677(f,1) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

0. (TOP-REAL 2) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like V87( TOP-REAL 2) Element of the carrier of (TOP-REAL 2)

the ZeroF of (TOP-REAL 2) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

(1 * f) + (0. (TOP-REAL 2)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K671((1 * f),(0. (TOP-REAL 2))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

f + (0. (TOP-REAL 2)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K671(f,(0. (TOP-REAL 2))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

f is V28() real ext-real Element of the carrier of I[01]

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 natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

L~ f is functional Element of K19( the carrier of (TOP-REAL 2))

f /. 1 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

f /. (len f) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

j is functional non empty Element of K19( 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

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

K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | j))) is set

P is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | j) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | j)))

P . 0 is set

P . 1 is set

p is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

p + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

LSeg (f,p) is functional Element of K19( the carrier of (TOP-REAL 2))

f /. p is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

f /. (p + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

1 / 2 is V28() real ext-real non negative Element of REAL

Closed-Interval-TSpace ((1 / 2),1) is non empty strict TopSpace-like V145() SubSpace of R^1

the carrier of (Closed-Interval-TSpace ((1 / 2),1)) is non empty V45() V46() V47() set

[.(1 / 2),1.] is V45() V46() V47() V66() Element of K19(REAL)

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

[#] (Closed-Interval-TSpace (0,(1 / 2))) is non empty non proper V45() V46() V47() closed Element of K19( the carrier of (Closed-Interval-TSpace (0,(1 / 2))))

the carrier of (Closed-Interval-TSpace (0,(1 / 2))) is non empty V45() V46() V47() set

K19( the carrier of (Closed-Interval-TSpace (0,(1 / 2)))) is set

[.0,(1 / 2).] is V45() V46() V47() V66() Element of K19(REAL)

[#] (Closed-Interval-TSpace ((1 / 2),1)) is non empty non proper V45() V46() V47() closed Element of K19( the carrier of (Closed-Interval-TSpace ((1 / 2),1)))

K19( the carrier of (Closed-Interval-TSpace ((1 / 2),1))) is set

(len f) - 2 is V28() real ext-real Element of REAL

f | (len 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)

Seg (len f) is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)

f | (Seg (len f)) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))

K20(NAT, the carrier of (TOP-REAL 2)) is set

K19(K20(NAT, the carrier of (TOP-REAL 2))) is set

dom f is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)

f | (dom f) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))

0 + 2 is non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() Element of NAT

f | (0 + 2) 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 | (0 + 2)) is functional Element of K19( the carrier of (TOP-REAL 2))

f /. (0 + 2) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

f | 2 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 | 2) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

gg is functional non empty Element of K19( the carrier of (TOP-REAL 2))

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

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

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

K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | gg))) is set

c

c

LSeg (f,c

f /. c

f /. (c

P is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | gg) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | gg)))

P . 0 is set

P . 1 is set

1 + 1 is non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() Element of NAT

(1 + 1) - 1 is V28() real ext-real Element of REAL

dom (f | 2) is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)

(f | 2) /. 1 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

(f | 2) . 1 is Relation-like Function-like set

(f | 2) /. 2 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

(f | 2) . 2 is Relation-like Function-like set

rng P is Element of K19( the carrier of ((TOP-REAL 2) | gg))

K19( the carrier of ((TOP-REAL 2) | gg)) is set

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

L~ (f | 2) is functional Element of K19( the carrier of (TOP-REAL 2))

<*((f | 2) /. 1),((f | 2) /. 2)*> 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 | 2) /. 1),((f | 2) /. 2)*> is functional Element of K19( the carrier of (TOP-REAL 2))

LSeg (((f | 2) /. 1),((f | 2) /. 2)) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))

{ (((1 - b

f /. 2 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

LSeg ((f /. 1),(f /. 2)) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))

{ (((1 - b

LSeg (f,1) is functional Element of K19( the carrier of (TOP-REAL 2))

P .: [.0,1.] is Element of K19( the carrier of ((TOP-REAL 2) | gg))

gg is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

gg + 2 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

f | (gg + 2) 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 | (gg + 2)) is functional Element of K19( the carrier of (TOP-REAL 2))

f /. (gg + 2) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

gg + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

(gg + 1) + 2 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

f | ((gg + 1) + 2) 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 | ((gg + 1) + 2)) is functional Element of K19( the carrier of (TOP-REAL 2))

f /. ((gg + 1) + 2) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

(gg + 2) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

c

(TOP-REAL 2) | c

the carrier of ((TOP-REAL 2) | c

K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | c

K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | c

c

(TOP-REAL 2) | c

the carrier of ((TOP-REAL 2) | c

K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | c

K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | c

len (f | ((gg + 1) + 2)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

(gg + 1) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

3 is non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() Element of NAT

gg + 3 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

f | (gg + 3) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)

dom (f | (gg + 3)) is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)

(f | (gg + 3)) /. (gg + 2) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

P is functional non empty Element of K19( 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

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

K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set

g is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

g + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

LSeg (f,g) is functional Element of K19( the carrier of (TOP-REAL 2))

f /. g is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

f /. (g + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

r2 is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

r2 . 0 is set

r2 . 1 is set

rng r2 is Element of K19( the carrier of ((TOP-REAL 2) | P))

K19( the carrier of ((TOP-REAL 2) | P)) is set

(TOP-REAL 2) | H

[#] ((TOP-REAL 2) | H

the carrier of ((TOP-REAL 2) | H

K19( the carrier of ((TOP-REAL 2) | H

dom r2 is V45() V46() V47() Element of K19( the carrier of I[01])

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

[#] I[01] is non empty non proper V45() V46() V47() closed Element of K19( the carrier of I[01])

L~ (f | (gg + 3)) is functional Element of K19( the carrier of (TOP-REAL 2))

r2 /" is Relation-like the carrier of ((TOP-REAL 2) | P) -defined the carrier of I[01] -valued Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20( the carrier of ((TOP-REAL 2) | P), the carrier of I[01]))

K20( the carrier of ((TOP-REAL 2) | P), the carrier of I[01]) is V33() V34() V35() set

K19(K20( the carrier of ((TOP-REAL 2) | P), the carrier of I[01])) is set

(r2 /") . (f /. (gg + 2)) is V28() real ext-real set

r2 " is Relation-like Function-like set

(r2 ") . (f /. (gg + 2)) is set

len (f | (gg + 2)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

dom (f | (gg + 2)) is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)

r2 . ((r2 /") . (f /. (gg + 2))) is set

SEG is V28() real ext-real Element of REAL

f /. ((gg + 2) + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

(f | (gg + 2)) /. (gg + 2) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

(f | (gg + 2)) /. 1 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

hh is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | c

hh . 0 is set

hh . 1 is set

LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))

{ (((1 - b

(TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1)))) is non empty strict TopSpace-like SubSpace of TOP-REAL 2

the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1))))) is non empty set

K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1)))))) is set

K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1))))))) is set

A is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1))))) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1)))))))

A . 0 is set

A . 1 is set

P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))) is Relation-like the carrier of (Closed-Interval-TSpace (0,(1 / 2))) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20( the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of (Closed-Interval-TSpace (0,1))))

K20( the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of (Closed-Interval-TSpace (0,1))) is V33() V34() V35() set

K19(K20( the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of (Closed-Interval-TSpace (0,1)))) is set

P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))) is Relation-like the carrier of (Closed-Interval-TSpace ((1 / 2),1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20( the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of (Closed-Interval-TSpace (0,1))))

K20( the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of (Closed-Interval-TSpace (0,1))) is V33() V34() V35() set

K19(K20( the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of (Closed-Interval-TSpace (0,1)))) is set

hh * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is Relation-like the carrier of (Closed-Interval-TSpace (0,(1 / 2))) -defined the carrier of ((TOP-REAL 2) | c

K20( the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of ((TOP-REAL 2) | c

K19(K20( the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of ((TOP-REAL 2) | c

A * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is Relation-like the carrier of (Closed-Interval-TSpace ((1 / 2),1)) -defined the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1))))) -valued Function-like Element of K19(K20( the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1)))))))

K20( the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1)))))) is set

K19(K20( the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1))))))) is set

dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is V45() V46() V47() Element of K19( the carrier of (Closed-Interval-TSpace (0,(1 / 2))))

dom hh is V45() V46() V47() Element of K19( the carrier of I[01])

rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) is V45() V46() V47() Element of K19( the carrier of (Closed-Interval-TSpace (0,1)))

K19( the carrier of (Closed-Interval-TSpace (0,1))) is set

rng (hh * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) is Element of K19( the carrier of ((TOP-REAL 2) | c

K19( the carrier of ((TOP-REAL 2) | c

rng hh is Element of K19( the carrier of ((TOP-REAL 2) | c

[#] ((TOP-REAL 2) | c

dom (hh * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) is V45() V46() V47() Element of K19( the carrier of (Closed-Interval-TSpace (0,(1 / 2))))

F1 is Relation-like the carrier of (Closed-Interval-TSpace (0,(1 / 2))) -defined the carrier of ((TOP-REAL 2) | c

rng F1 is Element of K19( the carrier of ((TOP-REAL 2) | c

dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is V45() V46() V47() Element of K19( the carrier of (Closed-Interval-TSpace ((1 / 2),1)))

dom A is V45() V46() V47() Element of K19( the carrier of I[01])

rng (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) is V45() V46() V47() Element of K19( the carrier of (Closed-Interval-TSpace (0,1)))

dom (A * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) is V45() V46() V47() Element of K19( the carrier of (Closed-Interval-TSpace ((1 / 2),1)))

F19 is Relation-like the carrier of (Closed-Interval-TSpace ((1 / 2),1)) -defined the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1))))) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1)))))))

rng F19 is Element of K19( the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1))))))

K19( the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1)))))) is set

[#] ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1))))) is non empty non proper closed Element of K19( the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1))))))

F1 +* F19 is Relation-like Function-like set

H

dom F1 is V45() V46() V47() Element of K19( the carrier of (Closed-Interval-TSpace (0,(1 / 2))))

T1 is TopSpace-like V145() SubSpace of I[01]

the carrier of T1 is V45() V46() V47() set

K20( the carrier of T1, the carrier of ((TOP-REAL 2) | P)) is set

K19(K20( the carrier of T1, the carrier of ((TOP-REAL 2) | P))) is set

dom F19 is V45() V46() V47() Element of K19( the carrier of (Closed-Interval-TSpace ((1 / 2),1)))

T2 is TopSpace-like V145() SubSpace of I[01]

the carrier of T2 is V45() V46() V47() set

K20( the carrier of T2, the carrier of ((TOP-REAL 2) | P)) is set

K19(K20( the carrier of T2, the carrier of ((TOP-REAL 2) | P))) is set

{ b

{ b

dom (F1 +* F19) is set

[.0,(1 / 2).] \/ [.(1 / 2),1.] is V45() V46() V47() Element of K19(REAL)

(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . (1 / 2) is V28() real ext-real set

(0,(1 / 2)) (#) is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,(1 / 2)))

(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . ((0,(1 / 2)) (#)) is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . (1 / 2) is V28() real ext-real set

(#) ((1 / 2),1) is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace ((1 / 2),1))

(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . ((#) ((1 / 2),1)) is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

F1 . (1 / 2) is set

F19 . (1 / 2) is set

[.0,(1 / 2).] /\ [.(1 / 2),1.] is V45() V46() V47() V66() Element of K19(REAL)

[.(1 / 2),(1 / 2).] is V45() V46() V47() V66() Element of K19(REAL)

(dom F1) /\ (dom F19) is V45() V46() V47() Element of K19( the carrier of (Closed-Interval-TSpace ((1 / 2),1)))

{(1 / 2)} is non empty V45() V46() V47() Element of K19(REAL)

H

FF is set

{ (LSeg ((f | (gg + 2)),b

union { (LSeg ((f | (gg + 2)),b

GF is set

ppp is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

LSeg ((f | (gg + 2)),ppp) is functional Element of K19( the carrier of (TOP-REAL 2))

ppp + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

1 + 1 is non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() Element of NAT

gg + (1 + 1) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

1 + ppp is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

f /. ppp is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

f /. (ppp + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

Seg (len (f | (gg + 2))) is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)

(f | (gg + 2)) /. ppp is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

(f | (gg + 2)) /. (ppp + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

LSeg (f,ppp) is functional Element of K19( the carrier of (TOP-REAL 2))

LSeg ((f /. ppp),(f /. (ppp + 1))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))

{ (((1 - b

LSeg (f,(gg + 2)) is functional Element of K19( the carrier of (TOP-REAL 2))

(LSeg ((f | (gg + 2)),ppp)) /\ (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1)))) is functional Element of K19( the carrier of (TOP-REAL 2))

f /. (gg + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

f /. ((gg + 1) + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

1 + gg is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

1 + (gg + 1) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

(f | (gg + 2)) /. (gg + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

(f | (gg + 2)) /. ((gg + 1) + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

LSeg (f,(gg + 1)) is functional Element of K19( the carrier of (TOP-REAL 2))

LSeg ((f /. (gg + 1)),(f /. ((gg + 1) + 1))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))

{ (((1 - b

LSeg ((f | (gg + 2)),(gg + 1)) is functional Element of K19( the carrier of (TOP-REAL 2))

LSeg (f,((gg + 1) + 1)) is functional Element of K19( the carrier of (TOP-REAL 2))

(LSeg (f,(gg + 1))) /\ (LSeg (f,((gg + 1) + 1))) is functional Element of K19( the carrier of (TOP-REAL 2))

{(f /. ((gg + 1) + 1))} is functional non empty set

Seg (gg + 2) is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)

(f | (gg + 2)) /. ((gg + 1) + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

LSeg ((f | (gg + 2)),(gg + 1)) is functional Element of K19( the carrier of (TOP-REAL 2))

{ (LSeg ((f | (gg + 2)),b

union { (LSeg ((f | (gg + 2)),b

{(f /. (gg + 2))} is functional non empty set

F1 .: ((dom F1) /\ (dom F19)) is Element of K19( the carrier of ((TOP-REAL 2) | c

Im (F1,(1 / 2)) is set

{(1 / 2)} is non empty V45() V46() V47() set

F1 .: {(1 / 2)} is set

rng (F1 +* F19) is set

[#] (Closed-Interval-TSpace (0,1)) is non empty non proper V45() V46() V47() closed Element of K19( the carrier of (Closed-Interval-TSpace (0,1)))

(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . 0 is V28() real ext-real set

(#) (0,(1 / 2)) is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,(1 / 2)))

(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . ((#) (0,(1 / 2))) is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) /" is Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,(1 / 2))) -valued Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,(1 / 2)))))

K20( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,(1 / 2)))) is V33() V34() V35() set

K19(K20( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,(1 / 2))))) is set

((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) /") . 0 is V28() real ext-real set

(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) " is Relation-like Function-like set

((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . 0 is set

((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) /") . 1 is V28() real ext-real set

((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . 1 is set

(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . 1 is V28() real ext-real set

((1 / 2),1) (#) is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace ((1 / 2),1))

(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . (((1 / 2),1) (#)) is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

F19 .: [.(1 / 2),1.] is Element of K19( the carrier of ((TOP-REAL 2) | (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1))))))

FF is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

FF . (1 / 2) is set

GF is set

FF .: [.(1 / 2),1.] is Element of K19( the carrier of ((TOP-REAL 2) | P))

GF is set

dom FF is V45() V46() V47() Element of K19( the carrier of I[01])

ppp is set

FF . ppp is set

F19 . ppp is set

GF is set

ppp is set

F19 . ppp is set

dom FF is V45() V46() V47() Element of K19( the carrier of I[01])

FF . ppp is set

(r2 /") * FF is Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20( the carrier of I[01], the carrier of I[01]))

K20( the carrier of I[01], the carrier of I[01]) is V33() V34() V35() set

K19(K20( the carrier of I[01], the carrier of I[01])) is set

dom FF is V45() V46() V47() Element of K19( the carrier of I[01])

FF . 0 is set

F1 . 0 is set

FF . 1 is set

F19 . 1 is set

(r2 /") . (f /. 1) is V28() real ext-real set

(r2 ") . (f /. 1) is set

((r2 /") * FF) . 0 is V28() real ext-real set

(r2 /") . (f /. ((gg + 2) + 1)) is V28() real ext-real set

(r2 ") . (f /. ((gg + 2) + 1)) is set

((r2 /") * FF) . 1 is V28() real ext-real set

g11 is Relation-like the carrier of T1 -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like total quasi_total Element of K19(K20( the carrier of T1, the carrier of ((TOP-REAL 2) | P)))

g22 is Relation-like the carrier of T2 -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like total quasi_total Element of K19(K20( the carrier of T2, the carrier of ((TOP-REAL 2) | P)))

[#] T1 is non proper V45() V46() V47() closed Element of K19( the carrier of T1)

K19( the carrier of T1) is set

[#] T2 is non proper V45() V46() V47() closed Element of K19( the carrier of T2)

K19( the carrier of T2) is set

([#] T1) \/ ([#] T2) is V45() V46() V47() set

([#] T1) /\ ([#] T2) is V45() V46() V47() Element of K19( the carrier of T2)

ppp is V28() real ext-real Element of the carrier of I[01]

{ppp} is non empty V45() V46() V47() Element of K19(REAL)

(dom F1) \ (dom F19) is V45() V46() V47() Element of K19( the carrier of (Closed-Interval-TSpace (0,(1 / 2))))

r1 is set

r2 is set

F19 . r1 is set

F1 . r2 is set

c

FF is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

dom ((r2 /") * FF) is V45() V46() V47() Element of K19( the carrier of I[01])

rng ((r2 /") * FF) is V45() V46() V47() Element of K19( the carrier of I[01])

((r2 /") * FF) /" is Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20( the carrier of I[01], the carrier of I[01]))

dom (((r2 /") * FF) /") is V45() V46() V47() Element of K19( the carrier of I[01])

rng FF is Element of K19( the carrier of ((TOP-REAL 2) | P))

(r2 /") * FF is Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20( the carrier of I[01], the carrier of I[01]))

r2 * ((r2 /") * FF) is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

(r2 /") (#) r2 is Relation-like Function-like set

FF (#) ((r2 /") (#) r2) is Relation-like Function-like set

id (rng r2) is Relation-like rng r2 -defined rng r2 -valued Function-like one-to-one total quasi_total Element of K19(K20((rng r2),(rng r2)))

K20((rng r2),(rng r2)) is set

K19(K20((rng r2),(rng r2))) is set

(id (rng r2)) * FF is Relation-like the carrier of I[01] -defined rng r2 -valued Function-like Element of K19(K20( the carrier of I[01],(rng r2)))

K20( the carrier of I[01],(rng r2)) is set

K19(K20( the carrier of I[01],(rng r2))) is set

((r2 /") * FF) . (1 / 2) is V28() real ext-real set

FF . (1 / 2) is set

(r2 /") . (FF . (1 / 2)) is V28() real ext-real set

[.SEG,1.] is V45() V46() V47() V66() Element of K19(REAL)

((r2 /") * FF) .: [.(1 / 2),1.] is V45() V46() V47() Element of K19( the carrier of I[01])

r1 is set

{ b

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

(((r2 /") * FF) /") . r2 is V28() real ext-real set

rng (((r2 /") * FF) /") is V45() V46() V47() Element of K19( the carrier of I[01])

((r2 /") * FF) . ((((r2 /") * FF) /") . r2) is V28() real ext-real set

((r2 /") * FF) " is Relation-like Function-like set

(((r2 /") * FF) ") . r2 is set

((r2 /") * FF) . ((((r2 /") * FF) ") . r2) is V28() real ext-real set

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

f1 is V28() real ext-real Element of the carrier of I[01]

((r2 /") * FF) . f1 is V28() real ext-real Element of the carrier of I[01]

f2 is V28() real ext-real Element of the carrier of I[01]

((r2 /") * FF) . f2 is V28() real ext-real Element of the carrier of I[01]

r29 is V28() real ext-real Element of the carrier of I[01]

e1 is V28() real ext-real Element of the carrier of I[01]

r19 is V28() real ext-real Element of the carrier of I[01]

((r2 /") * FF) . r19 is V28() real ext-real Element of the carrier of I[01]

e2 is V28() real ext-real Element of REAL

l1 is V28() real ext-real Element of REAL

l2 is V28() real ext-real Element of REAL

e2 is V28() real ext-real Element of REAL

r1 is set

r2 is set

((r2 /") * FF) . r2 is V28() real ext-real set

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

((r2 /") * FF) . 1[01] is V28() real ext-real Element of the carrier of I[01]

f2 is V28() real ext-real Element of the carrier of I[01]

((r2 /") * FF) . f2 is V28() real ext-real Element of the carrier of I[01]

f1 is V28() real ext-real Element of the carrier of I[01]

((r2 /") * FF) . f1 is V28() real ext-real Element of the carrier of I[01]

f2 is V28() real ext-real Element of the carrier of I[01]

r19 is V28() real ext-real Element of the carrier of I[01]

r29 is V28() real ext-real Element of the carrier of I[01]

e2 is V28() real ext-real Element of REAL

e1 is V28() real ext-real Element of REAL

l1 is V28() real ext-real Element of REAL

{ b

r2 .: [.SEG,1.] is Element of K19( the carrier of ((TOP-REAL 2) | P))

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

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

[.r1,r2.] is V45() V46() V47() V66() Element of K19(REAL)

hh .: [.r1,r2.] is Element of K19( the carrier of ((TOP-REAL 2) | c

hh . r1 is set

hh . r2 is set

((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) /") . r1 is V28() real ext-real set

((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) /") . r2 is V28() real ext-real set

((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r1 is set

((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) ") . r2 is set

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

r19 is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) /") . r19 is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,(1 / 2)))

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

r29 is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) /") . r29 is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,(1 / 2)))

(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f1 is V28() real ext-real set

(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f2 is V28() real ext-real set

[.f1,f2.] is V45() V46() V47() V66() Element of K19(REAL)

(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) .: [.f1,f2.] is V45() V46() V47() Element of K19( the carrier of (Closed-Interval-TSpace (0,1)))

e1 is V28() real ext-real Element of REAL

e2 is V28() real ext-real Element of REAL

F1 .: [.f1,f2.] is Element of K19( the carrier of ((TOP-REAL 2) | c

FF .: [.f1,f2.] is Element of K19( the carrier of ((TOP-REAL 2) | P))

e1 is set

e2 is set

F1 . e2 is set

FF . e2 is set

FF . e2 is set

FF . e2 is set

FF . e2 is set

dom FF is V45() V46() V47() Element of K19( the carrier of I[01])

e1 is set

dom FF is V45() V46() V47() Element of K19( the carrier of I[01])

e2 is set

FF . e2 is set

F1 . e2 is set

F1 . e2 is set

F1 . e2 is set

F1 . e2 is set

((r2 /") * FF) . f1 is V28() real ext-real set

((r2 /") * FF) . f2 is V28() real ext-real set

{ b

l1 is V28() real ext-real Element of REAL

l2 is V28() real ext-real Element of REAL

f19 is V28() real ext-real Element of the carrier of I[01]

((r2 /") * FF) . f19 is V28() real ext-real Element of the carrier of I[01]

f29 is V28() real ext-real Element of the carrier of I[01]

((r2 /") * FF) . f29 is V28() real ext-real Element of the carrier of I[01]

[.l1,l2.] is V45() V46() V47() V66() Element of K19(REAL)

r2 .: [.l1,l2.] is Element of K19( the carrier of ((TOP-REAL 2) | P))

((r2 /") * FF) .: [.f1,f2.] is V45() V46() V47() Element of K19( the carrier of I[01])

r2 .: (((r2 /") * FF) .: [.f1,f2.]) is Element of K19( the carrier of ((TOP-REAL 2) | P))

FF . f19 is Element of the carrier of ((TOP-REAL 2) | P)

hh . r19 is set

F1 . f19 is set

(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f19 is V28() real ext-real set

hh . ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f19) is set

FF . f29 is Element of the carrier of ((TOP-REAL 2) | P)

hh . r29 is set

F1 . f29 is set

(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f29 is V28() real ext-real set

hh . ((P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . f29) is set

r2 . l1 is set

r2 . l2 is set

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

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

[.r1,r2.] is V45() V46() V47() V66() Element of K19(REAL)

r2 .: [.r1,r2.] is Element of K19( the carrier of ((TOP-REAL 2) | P))

r2 . r1 is set

r2 . r2 is set

q is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

q + 2 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

f | (q + 2) 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 | (q + 2)) is functional Element of K19( the carrier of (TOP-REAL 2))

f /. (q + 2) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

gg is functional non empty Element of K19( the carrier of (TOP-REAL 2))

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

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

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

K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | gg))) is set

K19( the carrier of I[01]) 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)

f /. 1 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

len f is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

f /. (len f) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

L~ f is functional Element of K19( the carrier of (TOP-REAL 2))

j is functional non empty Element of K19( 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

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

K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | j))) is set

P is functional non empty Element of K19( 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

p is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | j) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | j)))

p . 0 is set

p . 1 is set

q is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

q + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT

LSeg (f,q) is functional Element of K19( the carrier of (TOP-REAL 2))

gg is non empty V45() V46() V47() Element of K19( the carrier of I[01])

p .: gg is Element of K19( the carrier of ((TOP-REAL 2) | j))

K19( the carrier of ((TOP-REAL 2) | j)) is set

I[01] | gg is non empty strict TopSpace-like V145() SubSpace of I[01]

the carrier of (I[01] | gg) is non empty V45() V46() V47() set

K20( the carrier of (I[01] | gg), the carrier of ((TOP-REAL 2) | P)) is set

K19(K20( the carrier of (I[01] | gg), the carrier of ((TOP-REAL 2) | P))) is set

p | gg is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | j) -valued Function-like Element of K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | j)))

f /. q is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

f /. (q + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

P is V28() real ext-real Element of REAL

c

[.c

p .: [.c

p . c

p . P is set

{ b

g is non empty V45() V46() V47() Element of K19( the carrier of I[01])

I[01] | g is non empty strict TopSpace-like V145() SubSpace of I[01]

the carrier of (I[01] | g) is non empty V45() V46() V47() set

[#] (I[01] | g) is non empty non proper V45() V46() V47() closed Element of K19( the carrier of (I[01] | g))

K19( the carrier of (I[01] | g)) is set

dom p is V45() V46() V47() Element of K19( the carrier of I[01])

[#] I[01] is non empty non proper V45() V46() V47() closed Element of K19( the carrier of I[01])

K20( the carrier of (I[01] | g), the carrier of ((TOP-REAL 2) | j)) is set

K19(K20( the carrier of (I[01] | g), the carrier of ((TOP-REAL 2) | j))) is set

SEG is non empty Element of K19( the carrier of ((TOP-REAL 2) | j))

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

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

[#] (((TOP-REAL 2) | j) | SEG) is non empty non proper closed Element of K19( the carrier of (((TOP-REAL 2) | j) | SEG))

K19( the carrier of (((TOP-REAL 2) | j) | SEG)) is set

gg is Relation-like the carrier of (I[01] | g) -defined the carrier of ((TOP-REAL 2) | j) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (I[01] | g), the carrier of ((TOP-REAL 2) | j)))

rng gg is Element of K19( the carrier of ((TOP-REAL 2) | j))

SEG is set

dom gg is V45() V46() V47() Element of K19( the carrier of (I[01] | g))

hh9 is set

gg . hh9 is set

(dom p) /\ g is V45() V46() V47() Element of K19( the carrier of I[01])

p . hh9 is set

SEG is non empty Element of K19( the carrier of ((TOP-REAL 2) | j))

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

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

K20( the carrier of (I[01] | g), the carrier of (((TOP-REAL 2) | j) | SEG)) is set

K19(K20( the carrier of (I[01] | g), the carrier of (((TOP-REAL 2) | j) | SEG))) is set

hh9 is Relation-like the carrier of (I[01] | g) -defined the carrier of (((TOP-REAL 2) | j) | SEG) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (I[01] | g), the carrier of (((TOP-REAL 2) | j) | SEG)))

K20( the carrier of (I[01] | g), the carrier of ((TOP-REAL 2) | P)) is set

K19(K20( the carrier of (I[01] | g), the carrier of ((TOP-REAL 2) | P))) is set

hh is Relation-like the carrier of (I[01] | g) -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (I[01] | g), the carrier of ((TOP-REAL 2) | P)))

dom hh is V45() V46() V47() Element of K19( the carrier of (I[01] | g))

rng hh is Element of K19( the carrier of ((TOP-REAL 2) | P))

K19( the carrier of ((TOP-REAL 2) | P)) is set

hh .: (dom hh) is Element of K19( the carrier of ((TOP-REAL 2) | P))

[#] (((TOP-REAL 2) | j) | SEG) is non empty non proper closed Element of K19( the carrier of (((TOP-REAL 2) | j) | SEG))

K19( the carrier of (((TOP-REAL 2) | j) | SEG)) is set

Closed-Interval-TSpace (c

A is strict TopSpace-like V145() SubSpace of I[01]

[#] A is non proper V45() V46() V47() closed Element of K19( the carrier of A)

the carrier of A is V45() V46() V47() set

K19( the carrier of A) is set

[#] (Closed-Interval-TSpace (c

the carrier of (Closed-Interval-TSpace (c

K19( the carrier of (Closed-Interval-TSpace (c

Ex1 is V45() V46() V47() Element of K19( the carrier of A)

f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

P is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

LSeg (f,j) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))

{ (((1 - b

p is V28() real ext-real Element of REAL

1 - p is V28() real ext-real Element of REAL

(1 - p) * f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K677(f,(1 - p)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

p * j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K677(j,p) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

((1 - p) * f) + (p * j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K671(((1 - p) * f),(p * j)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

q is V28() real ext-real Element of REAL

1 - q is V28() real ext-real Element of REAL

(1 - q) * f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K677(f,(1 - q)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

q * j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K677(j,q) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

((1 - q) * f) + (q * j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K671(((1 - q) * f),(q * j)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

P is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

LSeg (j,P) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))

{ (((1 - b

p is V28() real ext-real Element of REAL

1 - p is V28() real ext-real Element of REAL

(1 - p) * j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K677(j,(1 - p)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

p * P is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K677(P,p) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL

((1 - p) * j) + (p * P) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)

K671(((1 - p) * j),(p * P)) is Relation-like NAT -defined REAL