:: 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₁) * f) + (b₁ * j)) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
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₁) * f) + (b₁ * j)) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
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₇ is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
c₇ + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
LSeg (f,c₇) is functional Element of K19( the carrier of (TOP-REAL 2))
f /. c₇ is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
f /. (c₇ + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
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) /. 1)) + (b₁ * ((f | 2) /. 2))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
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₁) * (f /. 1)) + (b₁ * (f /. 2))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
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₇ is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | c₇ is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | c₇) is non empty set
K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₇)) is set
K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₇))) is set
c₇ is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | c₇ is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | c₇) is non empty set
K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₇)) is set
K19(K20( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₇))) is set
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₁(gg + 1) is strict TopSpace-like SubSpace of TOP-REAL 2
[#] ((TOP-REAL 2) | H₁(gg + 1)) is non proper closed Element of K19( the carrier of ((TOP-REAL 2) | H₁(gg + 1)))
the carrier of ((TOP-REAL 2) | H₁(gg + 1)) is set
K19( the carrier of ((TOP-REAL 2) | H₁(gg + 1))) is set
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₇) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of I[01], 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₁) * (f /. (gg + 2))) + (b₁ * (f /. ((gg + 2) + 1)))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(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₇) -valued Function-like Element of K19(K20( the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of ((TOP-REAL 2) | c₇)))
K20( the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of ((TOP-REAL 2) | c₇)) is set
K19(K20( the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of ((TOP-REAL 2) | c₇))) is set
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₇)) is set
rng hh is Element of K19( the carrier of ((TOP-REAL 2) | c₇))
[#] ((TOP-REAL 2) | c₇) is non empty non proper closed Element of K19( the carrier of ((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₇) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (Closed-Interval-TSpace (0,(1 / 2))), 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₁(gg) \/ (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1)))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
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₁ where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 / 2 ) } is set
{ b₁ where b₁ is V28() real ext-real Element of REAL : ( 1 / 2 <= b₁ & b₁ <= 1 ) } is set
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₁(gg) /\ (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1)))) is functional Element of K19( the carrier of (TOP-REAL 2))
FF is set
{ (LSeg ((f | (gg + 2)),b₁)) where b₁ is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (f | (gg + 2)) ) } is set
union { (LSeg ((f | (gg + 2)),b₁)) where b₁ is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (f | (gg + 2)) ) } is set
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₁) * (f /. ppp)) + (b₁ * (f /. (ppp + 1)))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
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₁) * (f /. (gg + 1))) + (b₁ * (f /. ((gg + 1) + 1)))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
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₁)) where b₁ is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (f | (gg + 2)) ) } is set
union { (LSeg ((f | (gg + 2)),b₁)) where b₁ is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (f | (gg + 2)) ) } is set
{(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₇ /\ (LSeg ((f /. (gg + 2)),(f /. ((gg + 2) + 1)))) is functional Element of K19( the carrier of (TOP-REAL 2))
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₁ where b₁ is V28() real ext-real Element of REAL : ( SEG <= b₁ & b₁ <= 1 ) } is set
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₁ where b₁ is V28() real ext-real Element of REAL : ( SEG <= b₁ & b₁ <= 1 ) } is set
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₁ where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
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₇ is V28() real ext-real Element of REAL
[.c₇,P.] is V45() V46() V47() V66() Element of K19(REAL)
p .: [.c₇,P.] is Element of K19( the carrier of ((TOP-REAL 2) | j))
p . c₇ is set
p . P is set
{ b₁ where b₁ is V28() real ext-real Element of REAL : ( c₇ <= b₁ & b₁ <= P ) } is set
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₇,P) is non empty strict TopSpace-like V145() SubSpace of R^1
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₇,P)) is non empty non proper V45() V46() V47() closed Element of K19( the carrier of (Closed-Interval-TSpace (c₇,P)))
the carrier of (Closed-Interval-TSpace (c₇,P)) is non empty V45() V46() V47() set
K19( the carrier of (Closed-Interval-TSpace (c₇,P))) is set
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₁) * f) + (b₁ * j)) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
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₁) * j) + (b₁ * P)) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
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 -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) * j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(j,(1 - q)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
q * P is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(P,q) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((1 - q) * j) + (q * P) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K671(((1 - q) * j),(q * P)) 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)
- j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K673(j) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
(((1 - p) * j) + (p * 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) * j) + (p * P)),(- j)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
(((1 - p) * j) + (p * P)) - j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K675((((1 - p) * j) + (p * P)),j) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
(p * P) - j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K675((p * P),j) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((1 - p) * j) + ((p * 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) * j),((p * P) - j)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
(- j) + (p * P) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K671((- j),(p * P)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((1 - p) * j) + ((- 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),((- j) + (p * P))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((1 - p) * j) + (- j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K671(((1 - p) * j),(- j)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
(((1 - p) * j) + (- 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) + (- j)),(p * P)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((1 - p) * j) - j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K675(((1 - p) * j),j) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
(((1 - p) * j) - 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) - j),(p * 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)
K673((p * P)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((((1 - p) * j) - j) + (p * P)) + (- (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) - j) + (p * P)),(- (p * P))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((((1 - p) * j) - j) + (p * P)) - (p * P) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K675(((((1 - p) * j) - j) + (p * P)),(p * P)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
(p * P) - (p * P) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K675((p * P),(p * P)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
(((1 - p) * j) - j) + ((p * P) - (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) - j),((p * P) - (p * P))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
(((1 - p) * j) - j) + (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 - p) * j) - j),(0. (TOP-REAL 2))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
1 * j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(j,1) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((1 - p) * j) - (1 * j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K675(((1 - p) * j),(1 * j)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
(1 - p) - 1 is V28() real ext-real Element of REAL
((1 - p) - 1) * 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) - 1)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
- p is V28() real ext-real Element 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
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
- (p * j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K673((p * j)) 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)
K673((- (p * P))) 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)
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 (j,P) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * j) + (b₁ * P)) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
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 -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) * j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(j,(1 - q)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
q * P is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(P,q) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((1 - q) * j) + (q * P) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K671(((1 - q) * j),(q * P)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
1 * P is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(P,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)
(0. (TOP-REAL 2)) + (1 * P) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K671((0. (TOP-REAL 2)),(1 * P)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
1 - 1 is V28() real ext-real Element of REAL
(1 - 1) * j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(j,(1 - 1)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((1 - 1) * j) + (1 * P) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K671(((1 - 1) * j),(1 * P)) 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)
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)
p is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
q 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₁) * f) + (b₁ * j)) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
gg is V28() real ext-real Element of REAL
1 - gg is V28() real ext-real Element of REAL
(1 - gg) * f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(f,(1 - gg)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
gg * j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(j,gg) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((1 - gg) * f) + (gg * j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K671(((1 - gg) * f),(gg * j)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
c₇ is V28() real ext-real Element of REAL
1 - c₇ is V28() real ext-real Element of REAL
(1 - c₇) * f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(f,(1 - c₇)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
c₇ * j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(j,c₇) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((1 - c₇) * f) + (c₇ * j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K671(((1 - c₇) * f),(c₇ * j)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence 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
g is V28() real ext-real Element of REAL
1 - g is V28() real ext-real Element of REAL
(1 - g) * f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(f,(1 - g)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
g * j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(j,g) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((1 - g) * f) + (g * j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K671(((1 - g) * f),(g * j)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
r2 is V28() real ext-real Element of REAL
1 - r2 is V28() real ext-real Element of REAL
(1 - r2) * f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(f,(1 - r2)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
r2 * j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K677(j,r2) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() FinSequence-like FinSequence of REAL
((1 - r2) * f) + (r2 * j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
K671(((1 - r2) * f),(r2 * j)) 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)
j 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₁) * f) + (b₁ * j)) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2) : ( LE f,b₁,f,j & LE b₁,j,f,j ) } is set
P is set
p is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
P is set
p is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
f is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
TOP-REAL f 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 f) is functional non empty set
K19( the carrier of (TOP-REAL f)) is set
j is functional Element of K19( the carrier of (TOP-REAL f))
P is Relation-like Function-like V33() V34() V35() V69(f) FinSequence-like Element of the carrier of (TOP-REAL f)
p is Relation-like Function-like V33() V34() V35() V69(f) FinSequence-like Element of the carrier of (TOP-REAL f)
(TOP-REAL f) | j is strict TopSpace-like SubSpace of TOP-REAL f
the carrier of ((TOP-REAL f) | j) is set
K20( the carrier of I[01], the carrier of ((TOP-REAL f) | j)) is set
K19(K20( the carrier of I[01], the carrier of ((TOP-REAL f) | j))) is set
q is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL f) | j) -valued Function-like quasi_total Element of K19(K20( the carrier of I[01], the carrier of ((TOP-REAL f) | j)))
q . 0 is set
q . 1 is set
L[01] (((0,1) (#)),((#) (0,1))) is Relation-like the carrier of (Closed-Interval-TSpace (0,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 (0,1)), the carrier of (Closed-Interval-TSpace (0,1))))
K20( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1))) is V33() V34() V35() set
K19(K20( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)))) is set
q * (L[01] (((0,1) (#)),((#) (0,1)))) is Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of ((TOP-REAL f) | j) -valued Function-like Element of K19(K20( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL f) | j)))
K20( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL f) | j)) is set
K19(K20( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of ((TOP-REAL f) | j))) is set
(L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) is V28() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
dom q 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])
rng (L[01] (((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
dom (q * (L[01] (((0,1) (#)),((#) (0,1))))) is V45() V46() V47() Element of K19( the carrier of (Closed-Interval-TSpace (0,1)))
dom (L[01] (((0,1) (#)),((#) (0,1)))) is V45() V46() V47() Element of K19( the carrier of (Closed-Interval-TSpace (0,1)))
P is functional non empty Element of K19( the carrier of (TOP-REAL f))
(TOP-REAL f) | P is non empty strict TopSpace-like SubSpace of TOP-REAL f
the carrier of ((TOP-REAL f) | P) is non empty set
K20( the carrier of I[01], the carrier of ((TOP-REAL f) | P)) is set
K19(K20( the carrier of I[01], the carrier of ((TOP-REAL f) | P))) is set
g is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL f) | P) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of I[01], the carrier of ((TOP-REAL f) | P)))
g . 0 is set
g . 1 is set
f is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
j 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 j is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
LSeg (j,f) is functional Element of K19( the carrier of (TOP-REAL 2))
j /. f is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
j /. (f + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
P is functional Element of K19( the carrier of (TOP-REAL 2))
dom j is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)
LSeg ((j /. f),(j /. (f + 1))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (j /. f)) + (b₁ * (j /. (f + 1)))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. 1 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
j is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
mid (f,j,(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)
L~ (mid (f,j,(len f))) is functional Element of K19( the carrier of (TOP-REAL 2))
len (mid (f,j,(len f))) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
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 ((mid (f,j,(len f))),P) is functional Element of K19( the carrier of (TOP-REAL 2))
dom (mid (f,j,(len f))) is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)
j -' 1 is natural V28() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /^ (j -' 1) 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 /^ (j -' 1)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
dom (f /^ (j -' 1)) is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)
(len f) - (j -' 1) is V28() real ext-real Element of REAL
(j -' 1) + P is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
P + (j -' 1) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
dom f is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)
(f /^ (j -' 1)) /. P is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(f /^ (j -' 1)) . P is Relation-like Function-like set
f . ((j -' 1) + P) is Relation-like Function-like set
f /. ((j -' 1) + P) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(j -' 1) + (P + 1) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(P + 1) + (j -' 1) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(f /^ (j -' 1)) /. (P + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(f /^ (j -' 1)) . (P + 1) is Relation-like Function-like set
f . ((j -' 1) + (P + 1)) is Relation-like Function-like set
f /. ((j -' 1) + (P + 1)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
((j -' 1) + P) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
LSeg ((f /. ((j -' 1) + P)),(f /. ((j -' 1) + (P + 1)))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. ((j -' 1) + P))) + (b₁ * (f /. ((j -' 1) + (P + 1))))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (f,((j -' 1) + P)) is functional Element of K19( the carrier of (TOP-REAL 2))
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
LSeg (f,1) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,1)) /\ (LSeg (f,((j -' 1) + P))) is functional Element of K19( the carrier of (TOP-REAL 2))
2 -' 1 is natural V28() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(2 -' 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 /. (1 + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
{(f /. (1 + 1))} is functional non empty set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is 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 set
j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
L_Cut (f,j) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
<*j*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like special FinSequence of the carrier of (TOP-REAL 2)
L~ f is functional Element of K19( the carrier of (TOP-REAL 2))
Rev 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~ (Rev f) is functional Element of K19( the carrier of (TOP-REAL 2))
Rev (Rev 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_Cut ((Rev (Rev f)),j) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
R_Cut ((Rev f),j) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
Rev (R_Cut ((Rev f),j)) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
(Rev f) . 1 is Relation-like Function-like 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 Element of K19( 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 set
j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
L_Cut (f,j) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
Index (j,(L_Cut (f,j))) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
len (L_Cut (f,j)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
dom (L_Cut (f,j)) is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)
(L_Cut (f,j)) /. 1 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(L_Cut (f,j)) . 1 is Relation-like Function-like 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 Element of K19( 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 set
j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
L_Cut (f,j) 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~ (L_Cut (f,j)) is functional Element of K19( the carrier of (TOP-REAL 2))
len (L_Cut (f,j)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(L_Cut (f,j)) . 1 is Relation-like Function-like 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 Element of K19( the carrier of (TOP-REAL 2))
f . 1 is Relation-like Function-like set
j is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
R_Cut (f,j) 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~ (R_Cut (f,j)) is functional Element of K19( the carrier of (TOP-REAL 2))
len (R_Cut (f,j)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(R_Cut (f,j)) . (len (R_Cut (f,j))) is Relation-like Function-like 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 Element of K19( 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)
B_Cut (f,j,j) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
<*j*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like special FinSequence of the carrier of (TOP-REAL 2)
Index (j,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(Index (j,f)) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
len f is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
dom f is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)
LSeg (f,(Index (j,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
f /. (Index (j,f)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
f /. ((Index (j,f)) + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((f /. (Index (j,f))),(f /. ((Index (j,f)) + 1))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. (Index (j,f)))) + (b₁ * (f /. ((Index (j,f)) + 1)))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
L_Cut (f,j) 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_Cut (f,j)) . 1 is Relation-like Function-like set
R_Cut ((L_Cut (f,j)),j) 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 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 Element of K19( 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 set
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)
L_Cut (f,P) 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~ (L_Cut (f,P)) is functional Element of K19( the carrier of (TOP-REAL 2))
L_Cut (f,j) 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~ (L_Cut (f,j)) is functional Element of K19( the carrier of (TOP-REAL 2))
Index (j,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(Index (j,f)) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
LSeg (f,(Index (j,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
f /. (Index (j,f)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
f /. ((Index (j,f)) + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((f /. (Index (j,f))),(f /. ((Index (j,f)) + 1))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. (Index (j,f)))) + (b₁ * (f /. ((Index (j,f)) + 1)))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
dom f is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)
Index (P,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
Index (P,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
Index (P,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
Index (P,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is functional Element of K19( 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 set
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)
L_Cut (f,P) 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~ (L_Cut (f,P)) is functional Element of K19( the carrier of (TOP-REAL 2))
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
Index (j,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(Index (j,f)) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
Index (P,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
<*P*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like special FinSequence of the carrier of (TOP-REAL 2)
mid (f,(len 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)
<*P*> ^ (mid (f,(len 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)
f /. (len f) 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 NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like special FinSequence of the carrier of (TOP-REAL 2)
<*P*> ^ <*(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)
<*P,(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)
<*P,j*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
rng (L_Cut (f,P)) is functional Element of K19( the carrier of (TOP-REAL 2))
{j,P} is functional non empty set
len (L_Cut (f,P)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is 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 set
L~ f is functional Element of K19( 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)
L_Cut (f,P) 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~ (L_Cut (f,P)) is functional Element of K19( the carrier of (TOP-REAL 2))
L_Cut (f,j) 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~ (L_Cut (f,j)) is functional Element of K19( 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 Element of K19( 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)
Index (P,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
Index (j,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. (Index (j,f)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(Index (j,f)) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. ((Index (j,f)) + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
B_Cut (f,j,P) 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~ (B_Cut (f,j,P)) is functional Element of K19( the carrier of (TOP-REAL 2))
L_Cut (f,j) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
R_Cut ((L_Cut (f,j)),P) 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~ (L_Cut (f,j)) is functional Element of K19( the carrier of (TOP-REAL 2))
len (L_Cut (f,j)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
L~ (L_Cut (f,j)) is functional Element of K19( the carrier of (TOP-REAL 2))
len (L_Cut (f,j)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
len (L_Cut (f,j)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
len (L_Cut (f,j)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
L~ (L_Cut (f,j)) is functional Element of K19( the carrier of (TOP-REAL 2))
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 ((L_Cut (f,j)),p) is functional Element of K19( the carrier of (TOP-REAL 2))
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 ((L_Cut (f,j)),q) is functional Element of K19( 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 Element of K19( 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)
B_Cut (f,j,P) 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~ (B_Cut (f,j,P)) is functional Element of K19( the carrier of (TOP-REAL 2))
<*j*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like special FinSequence of the carrier of (TOP-REAL 2)
len (B_Cut (f,j,P)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
Index (P,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
Index (j,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. (Index (j,f)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(Index (j,f)) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. ((Index (j,f)) + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
Index (P,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
Index (j,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. (Index (j,f)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(Index (j,f)) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. ((Index (j,f)) + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
L_Cut (f,P) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
R_Cut ((L_Cut (f,P)),j) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
Rev (R_Cut ((L_Cut (f,P)),j)) 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
LSeg (f,(Index (j,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
LSeg ((f /. (Index (j,f))),(f /. ((Index (j,f)) + 1))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. (Index (j,f)))) + (b₁ * (f /. ((Index (j,f)) + 1)))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
dom f is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)
(Index (j,f)) + 0 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. (Index (P,f)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(Index (P,f)) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. ((Index (P,f)) + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
B_Cut (f,P,j) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
Rev (B_Cut (f,P,j)) 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~ (B_Cut (f,P,j)) is functional Element of K19( the carrier of (TOP-REAL 2))
Index (P,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
Index (j,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. (Index (j,f)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(Index (j,f)) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. ((Index (j,f)) + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() FinSequence-like V204( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
GoB f is Relation-like non empty-yielding NAT -defined K238( the carrier of (TOP-REAL 2)) -valued Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the carrier of (TOP-REAL 2))
len (GoB f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
width (GoB f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(GoB f) * (1,(width (GoB f))) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(GoB f) * ((len (GoB f)),(width (GoB f))) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
j is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
P is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(GoB f) * (j,(width (GoB f))) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (j,(width (GoB f))))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * ((GoB f) * (1,(width (GoB f))))) + (b₁ * ((GoB f) * (j,(width (GoB f)))))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(GoB f) * (P,(width (GoB f))) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (P,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f))))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * ((GoB f) * (P,(width (GoB f))))) + (b₁ * ((GoB f) * ((len (GoB f)),(width (GoB f)))))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (j,(width (GoB f)))))) /\ (LSeg (((GoB f) * (P,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))))) is functional Element of K19( the carrier of (TOP-REAL 2))
gg is set
((GoB f) * (1,(width (GoB f)))) `1 is V28() real ext-real Element of REAL
((GoB f) * (j,(width (GoB f)))) `1 is V28() real ext-real Element of REAL
c₇ is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
c₇ `1 is V28() real ext-real Element of REAL
((GoB f) * (P,(width (GoB f)))) `1 is V28() real ext-real Element of REAL
((GoB f) * ((len (GoB f)),(width (GoB f)))) `1 is V28() real ext-real Element of REAL
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() FinSequence-like V204( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
GoB f is Relation-like non empty-yielding NAT -defined K238( the carrier of (TOP-REAL 2)) -valued Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the carrier of (TOP-REAL 2))
width (GoB f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
len (GoB f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(GoB f) * ((len (GoB f)),1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(GoB f) * ((len (GoB f)),(width (GoB f))) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
j is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
P is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(GoB f) * ((len (GoB f)),j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),j))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * ((GoB f) * ((len (GoB f)),1))) + (b<sub>1</sub> * ((GoB f) * ((len (GoB f)),j)))) where b<sub>1</sub> is V28() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
(GoB f) * ((len (GoB f)),P) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * ((len (GoB f)),P)),((GoB f) * ((len (GoB f)),(width (GoB f))))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * ((GoB f) * ((len (GoB f)),P))) + (b<sub>1</sub> * ((GoB f) * ((len (GoB f)),(width (GoB f)))))) where b<sub>1</sub> is V28() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
(LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),j)))) /\ (LSeg (((GoB f) * ((len (GoB f)),P)),((GoB f) * ((len (GoB f)),(width (GoB f)))))) is functional Element of K19( the carrier of (TOP-REAL 2))
gg is set
((GoB f) * ((len (GoB f)),1)) `2 is V28() real ext-real Element of REAL
((GoB f) * ((len (GoB f)),j)) `2 is V28() real ext-real Element of REAL
c<sub>7</sub> is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
c<sub>7</sub> `2 is V28() real ext-real Element of REAL
((GoB f) * ((len (GoB f)),P)) `2 is V28() real ext-real Element of REAL
((GoB f) * ((len (GoB f)),(width (GoB f)))) `2 is V28() real 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)
f /. 1 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
L_Cut (f,(f /. 1)) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
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
len f is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
dom f is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)
f . 1 is Relation-like Function-like set
Index ((f /. 1),f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. (1 + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
f . (1 + 1) is Relation-like Function-like set
<*(f /. 1)*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like special FinSequence of the carrier of (TOP-REAL 2)
(Index ((f /. 1),f)) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
mid (f,((Index ((f /. 1),f)) + 1),(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)
<*(f /. 1)*> ^ (mid (f,((Index ((f /. 1),f)) + 1),(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)
mid (f,1,(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)
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
f /. (len f) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
R_Cut (f,(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)
L~ f is functional Element of K19( the carrier of (TOP-REAL 2))
Rev 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)
(Rev f) /. 1 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
Rev (R_Cut (f,(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)
Rev (Rev (R_Cut (f,(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)
L_Cut ((Rev f),(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)
Rev (L_Cut ((Rev f),(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)
Rev (Rev 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 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 Element of K19( 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)
Index (j,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. (Index (j,f)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(Index (j,f)) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. ((Index (j,f)) + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg ((f /. (Index (j,f))),(f /. ((Index (j,f)) + 1))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. (Index (j,f)))) + (b₁ * (f /. ((Index (j,f)) + 1)))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
len f is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
LSeg (f,(Index (j,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. 1 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
j is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
LSeg (f,j) is functional Element of K19( the carrier of (TOP-REAL 2))
dom f is V45() V46() V47() V48() V49() V50() V63() Element of K19(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
LSeg (f,1) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,1)) /\ (LSeg (f,j)) is functional Element of K19( the carrier of (TOP-REAL 2))
1 + 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 /. 2 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
{(f /. 2)} is functional non empty set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() FinSequence-like V204( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
GoB f is Relation-like non empty-yielding NAT -defined K238( the carrier of (TOP-REAL 2)) -valued Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the carrier of (TOP-REAL 2))
width (GoB f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
len (GoB f) 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 V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(GoB f) * (1,j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(GoB f) * ((len (GoB f)),j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (1,j)),((GoB f) * ((len (GoB f)),j))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * ((GoB f) * (1,j))) + (b₁ * ((GoB f) * ((len (GoB f)),j)))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
P is functional Element of K19( the carrier of (TOP-REAL 2))
((GoB f) * (1,j)) `2 is V28() real ext-real Element of REAL
((GoB f) * ((len (GoB f)),j)) `2 is V28() real ext-real Element of REAL
((GoB f) * (1,j)) `1 is V28() real ext-real Element of REAL
((GoB f) * ((len (GoB f)),j)) `1 is V28() real ext-real Element of REAL
X_axis f is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() FinSequence-like FinSequence of REAL
Incr (X_axis f) is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V37() V39() FinSequence-like FinSequence of REAL
Y_axis f is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() FinSequence-like FinSequence of REAL
Incr (Y_axis f) is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V37() V39() FinSequence-like FinSequence of REAL
GoB ((Incr (X_axis f)),(Incr (Y_axis f))) is Relation-like non empty-yielding NAT -defined K238( the carrier of (TOP-REAL 2)) -valued Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the carrier of (TOP-REAL 2))
[1,j] is set
{1,j} is non empty V45() V46() V47() V48() V49() V50() V61() V63() set
{1} is non empty V45() V46() V47() V48() V49() V50() V61() V63() set
{{1,j},{1}} is non empty set
Indices (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) is set
[(len (GoB f)),j] is set
{(len (GoB f)),j} is non empty V45() V46() V47() V48() V49() V50() V61() V63() set
{(len (GoB f))} is non empty V45() V46() V47() V48() V49() V50() V61() V63() set
{{(len (GoB f)),j},{(len (GoB f))}} is non empty set
(GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) * (1,j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(Incr (X_axis f)) . 1 is V28() real ext-real set
(Incr (Y_axis f)) . j is V28() real ext-real set
|[((Incr (X_axis f)) . 1),((Incr (Y_axis f)) . j)]| is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) * ((len (GoB f)),j) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(Incr (X_axis f)) . (len (GoB f)) is V28() real ext-real set
|[((Incr (X_axis f)) . (len (GoB f))),((Incr (Y_axis f)) . j)]| is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
len (Incr (X_axis f)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
dom (Incr (X_axis f)) is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)
<*((GoB f) * (1,j)),((GoB f) * ((len (GoB f)),j))*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
gg 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 gg is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
L~ gg is functional Element of K19( the carrier of (TOP-REAL 2))
gg /. 1 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
gg /. (len gg) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant non empty V12() FinSequence-like V204( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
GoB f is Relation-like non empty-yielding NAT -defined K238( the carrier of (TOP-REAL 2)) -valued Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the carrier of (TOP-REAL 2))
len (GoB f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
width (GoB f) 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 V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
(GoB f) * (j,1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(GoB f) * (j,(width (GoB f))) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (((GoB f) * (j,1)),((GoB f) * (j,(width (GoB f))))) is functional non empty compact V231( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * ((GoB f) * (j,1))) + (b₁ * ((GoB f) * (j,(width (GoB f)))))) where b₁ is V28() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
P is functional Element of K19( the carrier of (TOP-REAL 2))
((GoB f) * (j,1)) `1 is V28() real ext-real Element of REAL
((GoB f) * (j,(width (GoB f)))) `1 is V28() real ext-real Element of REAL
((GoB f) * (j,1)) `2 is V28() real ext-real Element of REAL
((GoB f) * (j,(width (GoB f)))) `2 is V28() real ext-real Element of REAL
X_axis f is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() FinSequence-like FinSequence of REAL
Incr (X_axis f) is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V37() V39() FinSequence-like FinSequence of REAL
Y_axis f is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() FinSequence-like FinSequence of REAL
Incr (Y_axis f) is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V37() V39() FinSequence-like FinSequence of REAL
GoB ((Incr (X_axis f)),(Incr (Y_axis f))) is Relation-like non empty-yielding NAT -defined K238( the carrier of (TOP-REAL 2)) -valued Function-like FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K238( the carrier of (TOP-REAL 2))
[j,1] is set
{j,1} is non empty V45() V46() V47() V48() V49() V50() V61() V63() set
{j} is non empty V45() V46() V47() V48() V49() V50() V61() V63() set
{{j,1},{j}} is non empty set
Indices (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) is set
[j,(width (GoB f))] is set
{j,(width (GoB f))} is non empty V45() V46() V47() V48() V49() V50() V61() V63() set
{{j,(width (GoB f))},{j}} is non empty set
(GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) * (j,1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(Incr (X_axis f)) . j is V28() real ext-real set
(Incr (Y_axis f)) . 1 is V28() real ext-real set
|[((Incr (X_axis f)) . j),((Incr (Y_axis f)) . 1)]| is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) * (j,(width (GoB f))) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(Incr (Y_axis f)) . (width (GoB f)) is V28() real ext-real set
|[((Incr (X_axis f)) . j),((Incr (Y_axis f)) . (width (GoB f)))]| is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
len (Incr (Y_axis f)) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
dom (Incr (Y_axis f)) is V45() V46() V47() V48() V49() V50() V63() Element of K19(NAT)
<*((GoB f) * (j,1)),((GoB f) * (j,(width (GoB 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)
gg 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 gg is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
L~ gg is functional Element of K19( the carrier of (TOP-REAL 2))
gg /. 1 is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
gg /. (len gg) 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)
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 Element of K19( 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)
Index (P,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
Index (j,f) is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. (Index (j,f)) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
(Index (j,f)) + 1 is natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() Element of NAT
f /. ((Index (j,f)) + 1) is Relation-like Function-like V33() V34() V35() V69(2) FinSequence-like Element of the carrier of (TOP-REAL 2)
B_Cut (f,j,P) 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~ (B_Cut (f,j,P)) is functional Element of K19( the carrier of (TOP-REAL 2))