JORDAN20

:: JORDAN20 semantic presentation

REAL is non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() set
NAT is V143() V144() V145() V146() V147() V148() V149() bounded_below Element of K6(REAL)
K6(REAL) is set
I[01] is non empty strict TopSpace-like V200() SubSpace of R^1
R^1 is non empty strict TopSpace-like V200() TopStruct
the carrier of I[01] is non empty V143() V144() V145() set
COMPLEX is non empty V36() V143() V149() set
omega is V143() V144() V145() V146() V147() V148() V149() bounded_below set
K6(omega) is set
K6(NAT) is set
1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
K7(1,1) is V22() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V22() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V22() set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is V22() set
K7(K7(REAL,REAL),REAL) is V22() set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
K7(2,2) is V22() set
K7(K7(2,2),REAL) is V22() set
K6(K7(K7(2,2),REAL)) is set
RAT is non empty V36() V143() V144() V145() V146() V149() set
INT is non empty V36() V143() V144() V145() V146() V147() V149() set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V109() V155() V156() V157() V158() V159() V160() V161() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K6( the carrier of (TOP-REAL 2)) is set
K7( the carrier of (TOP-REAL 2),REAL) is V22() set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is set
{} is empty V22() non-empty empty-yielding V143() V144() V145() V146() V147() V148() V149() bounded_below V209() set
{{},1} is non empty set
K457() is non empty strict TopSpace-like V200() TopStruct
the carrier of K457() is non empty V143() V144() V145() set
RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V200() MetrStruct
K7(COMPLEX,COMPLEX) is V22() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V22() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is V22() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V22() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V22() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V22() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V22() set
K7(K7(NAT,NAT),NAT) is V22() set
K6(K7(K7(NAT,NAT),NAT)) is set
K7(COMPLEX,REAL) is V22() set
K6(K7(COMPLEX,REAL)) is set
0 is empty ordinal natural V11() real ext-real non positive non negative V22() non-empty empty-yielding V80() V81() V143() V144() V145() V146() V147() V148() V149() bounded_below V209() Element of NAT
the carrier of R^1 is non empty V143() V144() V145() set
K6( the carrier of R^1) is set
proj1 is non empty V22() V25( the carrier of (TOP-REAL 2)) V26( REAL ) Function-like total quasi_total Element of K6(K7( the carrier of (TOP-REAL 2),REAL))
TopSpaceMetr RealSpace is TopStruct
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V200() SubSpace of R^1
real_dist is V22() V25(K7(REAL,REAL)) V26( REAL ) Function-like total quasi_total Element of K6(K7(K7(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
[.0,1.] is V143() V144() V145() V209() Element of K6(REAL)
K6( the carrier of I[01]) is set
the carrier of RealSpace is non empty V143() V144() V145() set
P is Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Segment (P,p1,p2,p,p) is Element of K6( the carrier of (TOP-REAL 2))
{p} is non empty set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,p,P,p1,p2 ) } is set
e is set
e is set
f is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg (P,p1) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * P) + (b₁ * p1)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
P `1 is V11() real ext-real Element of REAL
p1 `1 is V11() real ext-real Element of REAL
p2 `1 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
1 - e is V11() real ext-real Element of REAL
(1 - e) * P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e * p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
((1 - e) * P) + (e * p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
((1 - e) * P) `1 is V11() real ext-real Element of REAL
(e * p1) `1 is V11() real ext-real Element of REAL
(((1 - e) * P) `1) + ((e * p1) `1) is V11() real ext-real Element of REAL
e * (p1 `1) is V11() real ext-real Element of REAL
(((1 - e) * P) `1) + (e * (p1 `1)) is V11() real ext-real Element of REAL
(1 - e) * (P `1) is V11() real ext-real Element of REAL
((1 - e) * (P `1)) + (e * (p1 `1)) is V11() real ext-real Element of REAL
(1 - e) * p is V11() real ext-real Element of REAL
e * p is V11() real ext-real Element of REAL
((1 - e) * p) + (e * p) is V11() real ext-real Element of REAL
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg (P,p1) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * P) + (b₁ * p1)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
P `1 is V11() real ext-real Element of REAL
p1 `1 is V11() real ext-real Element of REAL
p2 `1 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
1 - e is V11() real ext-real Element of REAL
(1 - e) * P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e * p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
((1 - e) * P) + (e * p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
((1 - e) * P) `1 is V11() real ext-real Element of REAL
(e * p1) `1 is V11() real ext-real Element of REAL
(((1 - e) * P) `1) + ((e * p1) `1) is V11() real ext-real Element of REAL
e * (p1 `1) is V11() real ext-real Element of REAL
(((1 - e) * P) `1) + (e * (p1 `1)) is V11() real ext-real Element of REAL
(1 - e) * (P `1) is V11() real ext-real Element of REAL
((1 - e) * (P `1)) + (e * (p1 `1)) is V11() real ext-real Element of REAL
(1 - e) * p is V11() real ext-real Element of REAL
e * p is V11() real ext-real Element of REAL
((1 - e) * p) + (e * p) is V11() real ext-real Element of REAL
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg (P,p1) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * P) + (b₁ * p1)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
P `1 is V11() real ext-real Element of REAL
p1 `1 is V11() real ext-real Element of REAL
p2 `1 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
1 - e is V11() real ext-real Element of REAL
(1 - e) * P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e * p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
((1 - e) * P) + (e * p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
((1 - e) * P) `1 is V11() real ext-real Element of REAL
(e * p1) `1 is V11() real ext-real Element of REAL
(((1 - e) * P) `1) + ((e * p1) `1) is V11() real ext-real Element of REAL
e * (p1 `1) is V11() real ext-real Element of REAL
(((1 - e) * P) `1) + (e * (p1 `1)) is V11() real ext-real Element of REAL
(1 - e) * (P `1) is V11() real ext-real Element of REAL
((1 - e) * (P `1)) + (e * (p1 `1)) is V11() real ext-real Element of REAL
0 * p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
P + (0 * p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
0. (TOP-REAL 2) is V43(2) V52( TOP-REAL 2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
P + (0. (TOP-REAL 2)) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
(1 - e) * p is V11() real ext-real Element of REAL
e * p is V11() real ext-real Element of REAL
((1 - e) * p) + (e * p) is V11() real ext-real Element of REAL
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg (P,p1) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * P) + (b₁ * p1)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
P `1 is V11() real ext-real Element of REAL
p1 `1 is V11() real ext-real Element of REAL
p2 `1 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
1 - e is V11() real ext-real Element of REAL
(1 - e) * P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e * p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
((1 - e) * P) + (e * p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
((1 - e) * P) `1 is V11() real ext-real Element of REAL
(e * p1) `1 is V11() real ext-real Element of REAL
(((1 - e) * P) `1) + ((e * p1) `1) is V11() real ext-real Element of REAL
e * (p1 `1) is V11() real ext-real Element of REAL
(((1 - e) * P) `1) + (e * (p1 `1)) is V11() real ext-real Element of REAL
(1 - e) * (P `1) is V11() real ext-real Element of REAL
((1 - e) * (P `1)) + (e * (p1 `1)) is V11() real ext-real Element of REAL
0 * p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
P + (0 * p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
0. (TOP-REAL 2) is V43(2) V52( TOP-REAL 2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
P + (0. (TOP-REAL 2)) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
(1 - e) * p is V11() real ext-real Element of REAL
e * p is V11() real ext-real Element of REAL
((1 - e) * p) + (e * p) is V11() real ext-real Element of REAL
P is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
P + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
p1 is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
len p1 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
LSeg (p1,P) is Element of K6( the carrier of (TOP-REAL 2))
p1 /. P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
(p1 /. P) `2 is V11() real ext-real Element of REAL
p1 /. (P + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
(p1 /. (P + 1)) `2 is V11() real ext-real Element of REAL
(p1 /. P) `1 is V11() real ext-real Element of REAL
(p1 /. (P + 1)) `1 is V11() real ext-real Element of REAL
L~ p1 is Element of K6( the carrier of (TOP-REAL 2))
p1 /. 1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p1 /. (len p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p `1 is V11() real ext-real Element of REAL
p2 `1 is V11() real ext-real Element of REAL
LSeg ((p1 /. P),(p1 /. (P + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (p1 /. P)) + (b₁ * (p1 /. (P + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
((p1 /. P) `1) - (p2 `1) is V11() real ext-real Element of REAL
((p1 /. P) `1) - (p `1) is V11() real ext-real Element of REAL
(((p1 /. P) `1) - (p `1)) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
1 - e is V11() real ext-real Element of REAL
(((p1 /. P) `1) - (p2 `1)) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL
((((p1 /. P) `1) - (p2 `1)) / (((p1 /. P) `1) - (p2 `1))) - ((((p1 /. P) `1) - (p `1)) / (((p1 /. P) `1) - (p2 `1))) is V11() real ext-real Element of REAL
(((p1 /. P) `1) - (p2 `1)) - (((p1 /. P) `1) - (p `1)) is V11() real ext-real Element of REAL
((((p1 /. P) `1) - (p2 `1)) - (((p1 /. P) `1) - (p `1))) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL
(p `1) - (p2 `1) is V11() real ext-real Element of REAL
((p `1) - (p2 `1)) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL
(1 - e) * (p1 /. P) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e * p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
((1 - e) * (p1 /. P)) + (e * p2) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
(((1 - e) * (p1 /. P)) + (e * p2)) `1 is V11() real ext-real Element of REAL
((1 - e) * (p1 /. P)) `1 is V11() real ext-real Element of REAL
(e * p2) `1 is V11() real ext-real Element of REAL
(((1 - e) * (p1 /. P)) `1) + ((e * p2) `1) is V11() real ext-real Element of REAL
(1 - e) * ((p1 /. P) `1) is V11() real ext-real Element of REAL
((1 - e) * ((p1 /. P) `1)) + ((e * p2) `1) is V11() real ext-real Element of REAL
1 * ((p1 /. P) `1) is V11() real ext-real Element of REAL
e * ((p1 /. P) `1) is V11() real ext-real Element of REAL
(1 * ((p1 /. P) `1)) - (e * ((p1 /. P) `1)) is V11() real ext-real Element of REAL
e * (p2 `1) is V11() real ext-real Element of REAL
((1 * ((p1 /. P) `1)) - (e * ((p1 /. P) `1))) + (e * (p2 `1)) is V11() real ext-real Element of REAL
e * (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL
((p1 /. P) `1) - (e * (((p1 /. P) `1) - (p2 `1))) is V11() real ext-real Element of REAL
((p1 /. P) `1) - (((p1 /. P) `1) - (p `1)) is V11() real ext-real Element of REAL
p2 `2 is V11() real ext-real Element of REAL
(((1 - e) * (p1 /. P)) + (e * p2)) `2 is V11() real ext-real Element of REAL
((1 - e) * (p1 /. P)) `2 is V11() real ext-real Element of REAL
(e * p2) `2 is V11() real ext-real Element of REAL
(((1 - e) * (p1 /. P)) `2) + ((e * p2) `2) is V11() real ext-real Element of REAL
(1 - e) * ((p1 /. P) `2) is V11() real ext-real Element of REAL
((1 - e) * ((p1 /. P) `2)) + ((e * p2) `2) is V11() real ext-real Element of REAL
1 * ((p1 /. P) `2) is V11() real ext-real Element of REAL
e * ((p1 /. P) `2) is V11() real ext-real Element of REAL
(1 * ((p1 /. P) `2)) - (e * ((p1 /. P) `2)) is V11() real ext-real Element of REAL
e * (p2 `2) is V11() real ext-real Element of REAL
((1 * ((p1 /. P) `2)) - (e * ((p1 /. P) `2))) + (e * (p2 `2)) is V11() real ext-real Element of REAL
p `2 is V11() real ext-real Element of REAL
0 + e is V11() real ext-real Element of REAL
(1 - e) + e is V11() real ext-real Element of REAL
LSeg ((p1 /. P),p2) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (p1 /. P)) + (b₁ * p2)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
P is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
P + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
p1 is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like being_S-Seq FinSequence of the carrier of (TOP-REAL 2)
len p1 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
LSeg (p1,P) is Element of K6( the carrier of (TOP-REAL 2))
p1 /. P is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
(p1 /. P) `2 is V11() real ext-real Element of REAL
p1 /. (P + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
(p1 /. (P + 1)) `2 is V11() real ext-real Element of REAL
(p1 /. (P + 1)) `1 is V11() real ext-real Element of REAL
(p1 /. P) `1 is V11() real ext-real Element of REAL
L~ p1 is Element of K6( the carrier of (TOP-REAL 2))
p1 /. 1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p1 /. (len p1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 `1 is V11() real ext-real Element of REAL
p `1 is V11() real ext-real Element of REAL
LSeg ((p1 /. P),(p1 /. (P + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (p1 /. P)) + (b₁ * (p1 /. (P + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
((p1 /. P) `1) - (p2 `1) is V11() real ext-real Element of REAL
((p1 /. P) `1) - (p `1) is V11() real ext-real Element of REAL
(((p1 /. P) `1) - (p `1)) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
1 - e is V11() real ext-real Element of REAL
(((p1 /. P) `1) - (p2 `1)) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL
((((p1 /. P) `1) - (p2 `1)) / (((p1 /. P) `1) - (p2 `1))) - ((((p1 /. P) `1) - (p `1)) / (((p1 /. P) `1) - (p2 `1))) is V11() real ext-real Element of REAL
(((p1 /. P) `1) - (p2 `1)) - (((p1 /. P) `1) - (p `1)) is V11() real ext-real Element of REAL
((((p1 /. P) `1) - (p2 `1)) - (((p1 /. P) `1) - (p `1))) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL
(p `1) - (p2 `1) is V11() real ext-real Element of REAL
((p `1) - (p2 `1)) / (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL
(1 - e) * (p1 /. P) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e * p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
((1 - e) * (p1 /. P)) + (e * p2) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
(((1 - e) * (p1 /. P)) + (e * p2)) `1 is V11() real ext-real Element of REAL
((1 - e) * (p1 /. P)) `1 is V11() real ext-real Element of REAL
(e * p2) `1 is V11() real ext-real Element of REAL
(((1 - e) * (p1 /. P)) `1) + ((e * p2) `1) is V11() real ext-real Element of REAL
(1 - e) * ((p1 /. P) `1) is V11() real ext-real Element of REAL
((1 - e) * ((p1 /. P) `1)) + ((e * p2) `1) is V11() real ext-real Element of REAL
1 * ((p1 /. P) `1) is V11() real ext-real Element of REAL
e * ((p1 /. P) `1) is V11() real ext-real Element of REAL
(1 * ((p1 /. P) `1)) - (e * ((p1 /. P) `1)) is V11() real ext-real Element of REAL
e * (p2 `1) is V11() real ext-real Element of REAL
((1 * ((p1 /. P) `1)) - (e * ((p1 /. P) `1))) + (e * (p2 `1)) is V11() real ext-real Element of REAL
e * (((p1 /. P) `1) - (p2 `1)) is V11() real ext-real Element of REAL
((p1 /. P) `1) - (e * (((p1 /. P) `1) - (p2 `1))) is V11() real ext-real Element of REAL
((p1 /. P) `1) - (((p1 /. P) `1) - (p `1)) is V11() real ext-real Element of REAL
p2 `2 is V11() real ext-real Element of REAL
(((1 - e) * (p1 /. P)) + (e * p2)) `2 is V11() real ext-real Element of REAL
((1 - e) * (p1 /. P)) `2 is V11() real ext-real Element of REAL
(e * p2) `2 is V11() real ext-real Element of REAL
(((1 - e) * (p1 /. P)) `2) + ((e * p2) `2) is V11() real ext-real Element of REAL
(1 - e) * ((p1 /. P) `2) is V11() real ext-real Element of REAL
((1 - e) * ((p1 /. P) `2)) + ((e * p2) `2) is V11() real ext-real Element of REAL
1 * ((p1 /. P) `2) is V11() real ext-real Element of REAL
e * ((p1 /. P) `2) is V11() real ext-real Element of REAL
(1 * ((p1 /. P) `2)) - (e * ((p1 /. P) `2)) is V11() real ext-real Element of REAL
e * (p2 `2) is V11() real ext-real Element of REAL
((1 * ((p1 /. P) `2)) - (e * ((p1 /. P) `2))) + (e * (p2 `2)) is V11() real ext-real Element of REAL
p `2 is V11() real ext-real Element of REAL
0 + e is V11() real ext-real Element of REAL
(1 - e) + e is V11() real ext-real Element of REAL
LSeg ((p1 /. P),p2) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (p1 /. P)) + (b₁ * p2)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
P is Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p1 `1 is V11() real ext-real Element of REAL
p2 `1 is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
Vertical_Line e is Element of K6( the carrier of (TOP-REAL 2))
P /\ (Vertical_Line e) is Element of K6( the carrier of (TOP-REAL 2))
the Element of P /\ (Vertical_Line e) is Element of P /\ (Vertical_Line e)
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : b₁ `1 = e } is set
Y is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y `1 is V11() real ext-real Element of REAL
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p1 `1 is V11() real ext-real Element of REAL
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p `1 is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
K7( the carrier of (TOP-REAL 2), the carrier of R^1) is V22() set
K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1)) is set
(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
K7( the carrier of ((TOP-REAL 2) | P), the carrier of R^1) is V22() set
K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of R^1)) is set
f is non empty V22() V25( the carrier of (TOP-REAL 2)) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))
f | P is V22() V25( the carrier of (TOP-REAL 2)) V25(P) V25( the carrier of (TOP-REAL 2)) V26( the carrier of R^1) Function-like Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
i is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
i . 0 is set
i . 1 is set
rng i is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))
K6( the carrier of ((TOP-REAL 2) | P)) is set
[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))
dom i is non empty V143() V144() V145() Element of K6( the carrier of I[01])
k is set
i . k is set
[#] I[01] is non empty non proper closed V143() V144() V145() Element of K6( the carrier of I[01])
pk is V11() real ext-real Element of REAL
p44 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p44 `1 is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= pk & ( for b₂ being V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) holds
( not b₂ = i . b₁ or not b₂ `1 = e ) ) ) } is set
p44 is set
p5 is V11() real ext-real Element of REAL
i . p5 is set
p44 is non empty V143() V144() V145() Element of K6(REAL)
p5 is set
Y3 is V11() real ext-real Element of REAL
i . Y3 is set
upper_bound p44 is V11() real ext-real Element of REAL
kk is V11() real ext-real set
k2 is V11() real ext-real Element of REAL
i . k2 is set
k2 is V11() real ext-real Element of REAL
i . k2 is set
kk is V11() real ext-real set
Y3 is V11() real ext-real Element of REAL
p5 is V143() V144() V145() Element of K6( the carrier of I[01])
i . Y3 is set
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y is non empty V22() V25( the carrier of ((TOP-REAL 2) | P)) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of R^1))
k2 is Element of the carrier of ((TOP-REAL 2) | P)
Y . k2 is V11() real ext-real Element of the carrier of R^1
proj1 . k2 is set
K7( the carrier of I[01], the carrier of R^1) is V22() set
K6(K7( the carrier of I[01], the carrier of R^1)) is set
Y * i is non empty V22() V25( the carrier of I[01]) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of R^1))
k2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of R^1))
dom k2 is non empty V143() V144() V145() Element of K6( the carrier of I[01])
z is ext-real set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
kk is set
i . kk is set
k2 is V11() real ext-real Element of REAL
Closed-Interval-MSpace (0,1) is non empty strict Reflexive discerning symmetric triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (0,1)) is non empty set
(z `1) - e is V11() real ext-real Element of REAL
abs ((z `1) - e) is V11() real ext-real Element of REAL
(abs ((z `1) - e)) / 2 is V11() real ext-real Element of REAL
G5 is V11() real ext-real Element of the carrier of RealSpace
G4 is V11() real ext-real Element of REAL
Ball (G5,G4) is V143() V144() V145() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is set
r0 is V143() V144() V145() Element of K6( the carrier of R^1)
(z `1) - G4 is V11() real ext-real Element of REAL
(z `1) + G4 is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= (z `1) - G4 & not (z `1) + G4 <= b₁ ) } is set
].((z `1) - G4),((z `1) + G4).[ is V143() V144() V145() non left_end non right_end V209() Element of K6(REAL)
k2 " r0 is V143() V144() V145() Element of K6( the carrier of I[01])
TopSpaceMetr (Closed-Interval-MSpace (0,1)) is TopStruct
k2 . k2 is set
i . k2 is set
Y . (i . k2) is set
proj1 . z is V11() real ext-real Element of REAL
G2 is Element of the carrier of (Closed-Interval-MSpace (0,1))
r0 is V11() real ext-real set
Ball (G2,r0) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
K6( the carrier of (Closed-Interval-MSpace (0,1))) is set
pk - k2 is V11() real ext-real Element of REAL
r01 is V11() real ext-real Element of REAL
min ((pk - k2),r01) is V11() real ext-real Element of REAL
s70 is V11() real ext-real Element of REAL
s70 / 2 is V11() real ext-real Element of REAL
s70 - (s70 / 2) is V11() real ext-real Element of REAL
(s70 - (s70 / 2)) + (s70 / 2) is V11() real ext-real Element of REAL
0 + (s70 / 2) is V11() real ext-real Element of REAL
k2 + s70 is V11() real ext-real Element of REAL
k2 + (s70 / 2) is V11() real ext-real Element of REAL
z is V11() real ext-real Element of the carrier of RealSpace
Ball (z,s70) is V143() V144() V145() Element of K6( the carrier of RealSpace)
k2 - s70 is V11() real ext-real Element of REAL
].(k2 - s70),(k2 + s70).[ is V143() V144() V145() non left_end non right_end V209() Element of K6(REAL)
Ball (G2,s70) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
].(k2 - s70),(k2 + s70).[ /\ [.0,1.] is V143() V144() V145() V209() Element of K6(REAL)
s70 + k2 is V11() real ext-real Element of REAL
(pk - k2) + k2 is V11() real ext-real Element of REAL
s7 is V11() real ext-real Element of REAL
Ball (G2,r01) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
(s70 / 2) + s70 is V11() real ext-real Element of REAL
k2 + ((s70 / 2) + s70) is V11() real ext-real Element of REAL
k2 + 0 is V11() real ext-real Element of REAL
(k2 + (s70 / 2)) + s70 is V11() real ext-real Element of REAL
(k2 - s70) + s70 is V11() real ext-real Element of REAL
k2 . (k2 + (s70 / 2)) is set
i . s7 is set
s7 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
s7 `1 is V11() real ext-real Element of REAL
k2 . s7 is set
Y . (i . s7) is set
f . s7 is V11() real ext-real Element of the carrier of R^1
((z `1) - e) / 2 is V11() real ext-real Element of REAL
(z `1) - (((z `1) - e) / 2) is V11() real ext-real Element of REAL
e / 2 is V11() real ext-real Element of REAL
(e / 2) + (e / 2) is V11() real ext-real Element of REAL
(z `1) / 2 is V11() real ext-real Element of REAL
((z `1) / 2) + (e / 2) is V11() real ext-real Element of REAL
(e / 2) - (e / 2) is V11() real ext-real Element of REAL
((z `1) / 2) - (e / 2) is V11() real ext-real Element of REAL
0 / 2 is empty V11() real ext-real non positive non negative V22() non-empty empty-yielding V143() V144() V145() V146() V147() V148() V149() bounded_below V209() Element of REAL
- ((z `1) - e) is V11() real ext-real Element of REAL
(- ((z `1) - e)) / 2 is V11() real ext-real Element of REAL
(z `1) + ((- ((z `1) - e)) / 2) is V11() real ext-real Element of REAL
(z `1) / 2 is V11() real ext-real Element of REAL
e / 2 is V11() real ext-real Element of REAL
((z `1) / 2) + (e / 2) is V11() real ext-real Element of REAL
(e / 2) + (e / 2) is V11() real ext-real Element of REAL
((z `1) / 2) - (e / 2) is V11() real ext-real Element of REAL
(e / 2) - (e / 2) is V11() real ext-real Element of REAL
((z `1) - e) / 2 is V11() real ext-real Element of REAL
0 / 2 is empty V11() real ext-real non positive non negative V22() non-empty empty-yielding V143() V144() V145() V146() V147() V148() V149() bounded_below V209() Element of REAL
s7 is V11() real ext-real Element of REAL
i . s7 is set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk is set
i . kk is set
k2 is V11() real ext-real Element of REAL
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
Y3 - k2 is V11() real ext-real Element of REAL
(Y3 - k2) / 2 is V11() real ext-real Element of REAL
k2 + ((Y3 - k2) / 2) is V11() real ext-real Element of REAL
Y3 - ((Y3 - k2) / 2) is V11() real ext-real Element of REAL
z is V11() real ext-real set
G4 is V11() real ext-real Element of REAL
i . G4 is set
G2 is V11() real ext-real Element of REAL
i . G2 is set
G4 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
G4 `1 is V11() real ext-real Element of REAL
G5 is V11() real ext-real Element of REAL
i . G5 is set
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk `1 is V11() real ext-real Element of REAL
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk `1 is V11() real ext-real Element of REAL
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk `1 is V11() real ext-real Element of REAL
kk is set
i . kk is set
k2 is V11() real ext-real Element of REAL
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
Y3 - k2 is V11() real ext-real Element of REAL
(Y3 - k2) / 2 is V11() real ext-real Element of REAL
k2 + ((Y3 - k2) / 2) is V11() real ext-real Element of REAL
Y3 - ((Y3 - k2) / 2) is V11() real ext-real Element of REAL
z is V11() real ext-real set
G4 is V11() real ext-real Element of REAL
i . G4 is set
G2 is V11() real ext-real Element of REAL
i . G2 is set
G4 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
G4 `1 is V11() real ext-real Element of REAL
G5 is V11() real ext-real Element of REAL
i . G5 is set
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk `1 is V11() real ext-real Element of REAL
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk `1 is V11() real ext-real Element of REAL
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk `1 is V11() real ext-real Element of REAL
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk `1 is V11() real ext-real Element of REAL
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 `1 is V11() real ext-real Element of REAL
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p `1 is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
K7( the carrier of (TOP-REAL 2), the carrier of R^1) is V22() set
K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1)) is set
(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
K7( the carrier of ((TOP-REAL 2) | P), the carrier of R^1) is V22() set
K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of R^1)) is set
f is non empty V22() V25( the carrier of (TOP-REAL 2)) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))
f | P is V22() V25( the carrier of (TOP-REAL 2)) V25(P) V25( the carrier of (TOP-REAL 2)) V26( the carrier of R^1) Function-like Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of R^1))
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
i is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
i . 0 is set
i . 1 is set
rng i is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))
K6( the carrier of ((TOP-REAL 2) | P)) is set
[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))
dom i is non empty V143() V144() V145() Element of K6( the carrier of I[01])
k is set
i . k is set
[#] I[01] is non empty non proper closed V143() V144() V145() Element of K6( the carrier of I[01])
pk is V11() real ext-real Element of REAL
p44 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p44 `1 is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( b₁ <= 1 & pk <= b₁ & ( for b₂ being V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) holds
( not b₂ = i . b₁ or not b₂ `1 = e ) ) ) } is set
p44 is set
p5 is V11() real ext-real Element of REAL
i . p5 is set
p44 is non empty V143() V144() V145() Element of K6(REAL)
lower_bound p44 is V11() real ext-real Element of REAL
Y3 is V11() real ext-real set
kk is V11() real ext-real Element of REAL
i . kk is set
kk is V11() real ext-real Element of REAL
i . kk is set
Y3 is V11() real ext-real set
p5 is V11() real ext-real Element of REAL
Y is non empty V22() V25( the carrier of ((TOP-REAL 2) | P)) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of R^1))
Y3 is Element of the carrier of ((TOP-REAL 2) | P)
Y . Y3 is V11() real ext-real Element of the carrier of R^1
proj1 . Y3 is set
K7( the carrier of I[01], the carrier of R^1) is V22() set
K6(K7( the carrier of I[01], the carrier of R^1)) is set
Y * i is non empty V22() V25( the carrier of I[01]) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of R^1))
Y3 is non empty V22() V25( the carrier of I[01]) V26( the carrier of R^1) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of R^1))
dom Y3 is non empty V143() V144() V145() Element of K6( the carrier of I[01])
kk is ext-real set
kk is set
k2 is V11() real ext-real Element of REAL
i . k2 is set
i . p5 is set
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
z is set
i . z is set
kk is V11() real ext-real Element of REAL
Closed-Interval-MSpace (0,1) is non empty strict Reflexive discerning symmetric triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (0,1)) is non empty set
(k2 `1) - e is V11() real ext-real Element of REAL
abs ((k2 `1) - e) is V11() real ext-real Element of REAL
(abs ((k2 `1) - e)) / 2 is V11() real ext-real Element of REAL
G4 is V11() real ext-real Element of the carrier of RealSpace
G2 is V11() real ext-real Element of REAL
Ball (G4,G2) is V143() V144() V145() Element of K6( the carrier of RealSpace)
K6( the carrier of RealSpace) is set
G5 is V143() V144() V145() Element of K6( the carrier of R^1)
(k2 `1) - G2 is V11() real ext-real Element of REAL
(k2 `1) + G2 is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= (k2 `1) - G2 & not (k2 `1) + G2 <= b₁ ) } is set
].((k2 `1) - G2),((k2 `1) + G2).[ is V143() V144() V145() non left_end non right_end V209() Element of K6(REAL)
Y3 " G5 is V143() V144() V145() Element of K6( the carrier of I[01])
TopSpaceMetr (Closed-Interval-MSpace (0,1)) is TopStruct
Y3 . kk is set
i . kk is set
Y . (i . kk) is set
proj1 . k2 is V11() real ext-real Element of REAL
z is Element of the carrier of (Closed-Interval-MSpace (0,1))
r0 is V11() real ext-real set
Ball (z,r0) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
K6( the carrier of (Closed-Interval-MSpace (0,1))) is set
kk - pk is V11() real ext-real Element of REAL
r0 is V11() real ext-real Element of REAL
min ((kk - pk),r0) is V11() real ext-real Element of REAL
k2 is V11() real ext-real Element of the carrier of RealSpace
r01 is V11() real ext-real Element of REAL
Ball (k2,r01) is V143() V144() V145() Element of K6( the carrier of RealSpace)
kk - r01 is V11() real ext-real Element of REAL
kk + r01 is V11() real ext-real Element of REAL
].(kk - r01),(kk + r01).[ is V143() V144() V145() non left_end non right_end V209() Element of K6(REAL)
Ball (z,r01) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
].(kk - r01),(kk + r01).[ /\ [.0,1.] is V143() V144() V145() V209() Element of K6(REAL)
r01 / 2 is V11() real ext-real Element of REAL
r01 - (r01 / 2) is V11() real ext-real Element of REAL
(r01 - (r01 / 2)) + (r01 / 2) is V11() real ext-real Element of REAL
0 + (r01 / 2) is V11() real ext-real Element of REAL
kk - (r01 / 2) is V11() real ext-real Element of REAL
kk + (r01 / 2) is V11() real ext-real Element of REAL
- (r01 / 2) is V11() real ext-real Element of REAL
kk + (- (r01 / 2)) is V11() real ext-real Element of REAL
Ball (z,r0) is Element of K6( the carrier of (Closed-Interval-MSpace (0,1)))
- (kk - pk) is V11() real ext-real Element of REAL
- r01 is V11() real ext-real Element of REAL
pk - kk is V11() real ext-real Element of REAL
(pk - kk) + kk is V11() real ext-real Element of REAL
(- r01) + kk is V11() real ext-real Element of REAL
- (- (r01 / 2)) is V11() real ext-real Element of REAL
kk + 0 is V11() real ext-real Element of REAL
s70 is V11() real ext-real Element of REAL
1 - 0 is non empty V11() real ext-real positive non negative Element of REAL
Y3 . (kk - (r01 / 2)) is set
i . s70 is set
s7 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
s7 `1 is V11() real ext-real Element of REAL
Y3 . s70 is set
Y . (i . s70) is set
f . s7 is V11() real ext-real Element of the carrier of R^1
((k2 `1) - e) / 2 is V11() real ext-real Element of REAL
(k2 `1) - (((k2 `1) - e) / 2) is V11() real ext-real Element of REAL
e / 2 is V11() real ext-real Element of REAL
(e / 2) + (e / 2) is V11() real ext-real Element of REAL
(k2 `1) / 2 is V11() real ext-real Element of REAL
((k2 `1) / 2) + (e / 2) is V11() real ext-real Element of REAL
(e / 2) - (e / 2) is V11() real ext-real Element of REAL
((k2 `1) / 2) - (e / 2) is V11() real ext-real Element of REAL
0 / 2 is empty V11() real ext-real non positive non negative V22() non-empty empty-yielding V143() V144() V145() V146() V147() V148() V149() bounded_below V209() Element of REAL
- ((k2 `1) - e) is V11() real ext-real Element of REAL
(- ((k2 `1) - e)) / 2 is V11() real ext-real Element of REAL
(k2 `1) + ((- ((k2 `1) - e)) / 2) is V11() real ext-real Element of REAL
(k2 `1) / 2 is V11() real ext-real Element of REAL
e / 2 is V11() real ext-real Element of REAL
((k2 `1) / 2) + (e / 2) is V11() real ext-real Element of REAL
(e / 2) + (e / 2) is V11() real ext-real Element of REAL
((k2 `1) / 2) - (e / 2) is V11() real ext-real Element of REAL
(e / 2) - (e / 2) is V11() real ext-real Element of REAL
((k2 `1) - e) / 2 is V11() real ext-real Element of REAL
0 / 2 is empty V11() real ext-real non positive non negative V22() non-empty empty-yielding V143() V144() V145() V146() V147() V148() V149() bounded_below V209() Element of REAL
s7 is V11() real ext-real Element of REAL
i . s7 is set
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z is set
i . z is set
kk is V11() real ext-real Element of REAL
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
kk - p5 is V11() real ext-real Element of REAL
- (kk - p5) is V11() real ext-real Element of REAL
- (- (kk - p5)) is V11() real ext-real Element of REAL
p5 - kk is V11() real ext-real Element of REAL
(p5 - kk) / 2 is V11() real ext-real Element of REAL
- ((p5 - kk) / 2) is V11() real ext-real Element of REAL
p5 + (- ((p5 - kk) / 2)) is V11() real ext-real Element of REAL
k2 is V11() real ext-real set
G2 is V11() real ext-real Element of REAL
i . G2 is set
z is V11() real ext-real Element of REAL
i . z is set
kk + 0 is V11() real ext-real Element of REAL
kk + ((p5 - kk) / 2) is V11() real ext-real Element of REAL
G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
G2 `1 is V11() real ext-real Element of REAL
G4 is V11() real ext-real Element of REAL
i . G4 is set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk `1 is V11() real ext-real Element of REAL
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
z is set
i . z is set
kk is V11() real ext-real Element of REAL
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
kk - p5 is V11() real ext-real Element of REAL
- (kk - p5) is V11() real ext-real Element of REAL
- (- (kk - p5)) is V11() real ext-real Element of REAL
p5 - kk is V11() real ext-real Element of REAL
(p5 - kk) / 2 is V11() real ext-real Element of REAL
- ((p5 - kk) / 2) is V11() real ext-real Element of REAL
p5 + (- ((p5 - kk) / 2)) is V11() real ext-real Element of REAL
k2 is V11() real ext-real set
G2 is V11() real ext-real Element of REAL
i . G2 is set
z is V11() real ext-real Element of REAL
i . z is set
kk + 0 is V11() real ext-real Element of REAL
kk + ((p5 - kk) / 2) is V11() real ext-real Element of REAL
G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
G2 `1 is V11() real ext-real Element of REAL
G4 is V11() real ext-real Element of REAL
i . G4 is set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk `1 is V11() real ext-real Element of REAL
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk `1 is V11() real ext-real Element of REAL
[#] I[01] is non empty non proper closed V143() V144() V145() Element of K6( the carrier of I[01])
P is V143() V144() V145() Element of K6( the carrier of I[01])
p1 is V11() real ext-real Element of REAL
[.0,p1.[ is V143() V144() V145() non right_end V209() Element of K6(REAL)
[.0,p1.] is V143() V144() V145() V209() Element of K6(REAL)
p2 is V143() V144() V145() Element of K6( the carrier of R^1)
R^1 | p2 is strict TopSpace-like V200() SubSpace of R^1
[#] (R^1 | p2) is non proper closed V143() V144() V145() Element of K6( the carrier of (R^1 | p2))
the carrier of (R^1 | p2) is V143() V144() V145() set
K6( the carrier of (R^1 | p2)) is set
- 1 is V11() real ext-real non positive Element of REAL
].(- 1),p1.[ is V143() V144() V145() non left_end non right_end V209() Element of K6(REAL)
].(- 1),p1.[ /\ [.0,1.] is V143() V144() V145() V209() Element of K6(REAL)
f is set
Y is V11() real ext-real Element of REAL
f is set
Y is V11() real ext-real Element of REAL
p is V143() V144() V145() Element of K6( the carrier of (R^1 | p2))
e is V143() V144() V145() Element of K6( the carrier of R^1)
e /\ ([#] (R^1 | p2)) is V143() V144() V145() Element of K6( the carrier of (R^1 | p2))
the topology of I[01] is non empty Element of K6(K6( the carrier of I[01]))
K6(K6( the carrier of I[01])) is set
p2 is V11() real ext-real Element of REAL
p2 is V11() real ext-real set
p is V11() real ext-real Element of REAL
[#] I[01] is non empty non proper closed V143() V144() V145() Element of K6( the carrier of I[01])
P is V143() V144() V145() Element of K6( the carrier of I[01])
p1 is V11() real ext-real Element of REAL
].p1,1.] is V143() V144() V145() non left_end V209() Element of K6(REAL)
[.p1,1.] is V143() V144() V145() V209() Element of K6(REAL)
p2 is V143() V144() V145() Element of K6( the carrier of R^1)
R^1 | p2 is strict TopSpace-like V200() SubSpace of R^1
[#] (R^1 | p2) is non proper closed V143() V144() V145() Element of K6( the carrier of (R^1 | p2))
the carrier of (R^1 | p2) is V143() V144() V145() set
K6( the carrier of (R^1 | p2)) is set
].p1,2.[ is V143() V144() V145() non left_end non right_end V209() Element of K6(REAL)
].p1,2.[ /\ [.0,1.] is V143() V144() V145() V209() Element of K6(REAL)
f is set
Y is V11() real ext-real Element of REAL
f is set
Y is V11() real ext-real Element of REAL
p is V143() V144() V145() Element of K6( the carrier of (R^1 | p2))
e is V143() V144() V145() Element of K6( the carrier of R^1)
e /\ ([#] (R^1 | p2)) is V143() V144() V145() Element of K6( the carrier of (R^1 | p2))
the topology of I[01] is non empty Element of K6(K6( the carrier of I[01]))
K6(K6( the carrier of I[01])) is set
p2 is V11() real ext-real Element of REAL
p2 is V11() real ext-real set
p is V11() real ext-real Element of REAL
P is non empty Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
K6( the carrier of ((TOP-REAL 2) | P)) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
p1 is Element of K6( the carrier of ((TOP-REAL 2) | P))
p2 is V143() V144() V145() Element of K6( the carrier of I[01])
p is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
p .: p2 is Element of K6( the carrier of ((TOP-REAL 2) | P))
e is V11() real ext-real Element of REAL
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ex b₂ being V11() real ext-real Element of REAL st
( 0 <= b₂ & not e <= b₂ & b₁ = p . b₂ ) } is set
[.0,e.[ is V143() V144() V145() non right_end V209() Element of K6(REAL)
f is set
dom p is non empty V143() V144() V145() Element of K6( the carrier of I[01])
Y is set
p . Y is set
rng p is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))
i is V11() real ext-real Element of REAL
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
pk is V11() real ext-real Element of REAL
p . pk is set
f is set
dom p is non empty V143() V144() V145() Element of K6( the carrier of I[01])
Y is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
i is V11() real ext-real Element of REAL
p . i is set
i is V11() real ext-real Element of REAL
p . i is set
P is non empty Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
K6( the carrier of ((TOP-REAL 2) | P)) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
p1 is Element of K6( the carrier of ((TOP-REAL 2) | P))
p2 is V143() V144() V145() Element of K6( the carrier of I[01])
p is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
p .: p2 is Element of K6( the carrier of ((TOP-REAL 2) | P))
e is V11() real ext-real Element of REAL
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ex b₂ being V11() real ext-real Element of REAL st
( not b₂ <= e & b₂ <= 1 & b₁ = p . b₂ ) } is set
].e,1.] is V143() V144() V145() non left_end V209() Element of K6(REAL)
f is set
dom p is non empty V143() V144() V145() Element of K6( the carrier of I[01])
Y is set
p . Y is set
rng p is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))
i is V11() real ext-real Element of REAL
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
pk is V11() real ext-real Element of REAL
p . pk is set
f is set
Y is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
i is V11() real ext-real Element of REAL
p . i is set
i is V11() real ext-real Element of REAL
p . i is set
dom p is non empty V143() V144() V145() Element of K6( the carrier of I[01])
[#] I[01] is non empty non proper closed V143() V144() V145() Element of K6( the carrier of I[01])
P is non empty Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
K6( the carrier of ((TOP-REAL 2) | P)) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
p1 is Element of K6( the carrier of ((TOP-REAL 2) | P))
p2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
p is V11() real ext-real Element of REAL
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ex b₂ being V11() real ext-real Element of REAL st
( 0 <= b₂ & not p <= b₂ & b₁ = p2 . b₂ ) } is set
rng p2 is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))
[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))
p2 " is non empty V22() V25( the carrier of ((TOP-REAL 2) | P)) V26( the carrier of I[01]) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of I[01]))
K7( the carrier of ((TOP-REAL 2) | P), the carrier of I[01]) is V22() set
K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of I[01])) is set
(p2 ") " is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
[.0,p.[ is V143() V144() V145() non right_end V209() Element of K6(REAL)
e is set
f is V11() real ext-real Element of REAL
e is V143() V144() V145() Element of K6( the carrier of I[01])
rng (p2 ") is non empty V143() V144() V145() Element of K6( the carrier of I[01])
(p2 ") " is V22() Function-like set
((p2 ") ") .: e is Element of K6( the carrier of ((TOP-REAL 2) | P))
(p2 ") " e is Element of K6( the carrier of ((TOP-REAL 2) | P))
p2 .: e is Element of K6( the carrier of ((TOP-REAL 2) | P))
P is non empty Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
K6( the carrier of ((TOP-REAL 2) | P)) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
p1 is Element of K6( the carrier of ((TOP-REAL 2) | P))
p2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
p is V11() real ext-real Element of REAL
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ex b₂ being V11() real ext-real Element of REAL st
( not b₂ <= p & b₂ <= 1 & b₁ = p2 . b₂ ) } is set
rng p2 is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))
[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))
p2 " is non empty V22() V25( the carrier of ((TOP-REAL 2) | P)) V26( the carrier of I[01]) Function-like total quasi_total Element of K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of I[01]))
K7( the carrier of ((TOP-REAL 2) | P), the carrier of I[01]) is V22() set
K6(K7( the carrier of ((TOP-REAL 2) | P), the carrier of I[01])) is set
(p2 ") " is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
].p,1.] is V143() V144() V145() non left_end V209() Element of K6(REAL)
e is set
f is V11() real ext-real Element of REAL
e is V143() V144() V145() Element of K6( the carrier of I[01])
rng (p2 ") is non empty V143() V144() V145() Element of K6( the carrier of I[01])
(p2 ") " is V22() Function-like set
((p2 ") ") .: e is Element of K6( the carrier of ((TOP-REAL 2) | P))
(p2 ") " e is Element of K6( the carrier of ((TOP-REAL 2) | P))
p2 .: e is Element of K6( the carrier of ((TOP-REAL 2) | P))
P is non empty TopStruct
the carrier of P is non empty set
K6( the carrier of P) is set
K7( the carrier of I[01], the carrier of P) is V22() set
K6(K7( the carrier of I[01], the carrier of P)) is set
p1 is Element of K6( the carrier of P)
p2 is Element of K6( the carrier of P)
p1 /\ p2 is Element of K6( the carrier of P)
p1 \/ p2 is Element of K6( the carrier of P)
p is Element of the carrier of P
e is Element of the carrier of P
f is non empty V22() V25( the carrier of I[01]) V26( the carrier of P) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of P))
f . 0 is set
f . 1 is set
f is non empty V22() V25( the carrier of I[01]) V26( the carrier of P) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of P))
f . 0 is set
f . 1 is set
[#] P is non empty non proper Element of K6( the carrier of P)
f " p1 is V143() V144() V145() Element of K6( the carrier of I[01])
f " p2 is V143() V144() V145() Element of K6( the carrier of I[01])
dom f is non empty V143() V144() V145() Element of K6( the carrier of I[01])
{} I[01] is empty V22() non-empty empty-yielding closed V143() V144() V145() V146() V147() V148() V149() bounded_below V209() Element of K6( the carrier of I[01])
(f " p1) /\ (f " p2) is V143() V144() V145() Element of K6( the carrier of I[01])
f " (p1 /\ p2) is V143() V144() V145() Element of K6( the carrier of I[01])
(f " p1) \/ (f " p2) is V143() V144() V145() Element of K6( the carrier of I[01])
f " (p1 \/ p2) is V143() V144() V145() Element of K6( the carrier of I[01])
P is non empty Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
K6( the carrier of ((TOP-REAL 2) | P)) is set
p1 is Element of K6( the carrier of ((TOP-REAL 2) | P))
((TOP-REAL 2) | P) | p1 is strict TopSpace-like SubSpace of (TOP-REAL 2) | P
the carrier of (((TOP-REAL 2) | P) | p1) is set
K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | p1)) is V22() set
K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | p1))) is set
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
{e} is non empty set
P \ {e} is Element of K6( the carrier of (TOP-REAL 2))
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
f is non empty V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | P)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
f . 0 is set
f . 1 is set
rng f is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))
[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))
dom f is non empty V143() V144() V145() Element of K6( the carrier of I[01])
Y is set
f . Y is set
i is V11() real ext-real Element of REAL
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ex b₂ being V11() real ext-real Element of REAL st
( not b₂ <= i & b₂ <= 1 & b₁ = f . b₂ ) } is set
k is set
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p44 is V11() real ext-real Element of REAL
f . p44 is set
p44 is V11() real ext-real Element of REAL
f . p44 is set
k is Element of K6( the carrier of ((TOP-REAL 2) | P))
pk is set
p44 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 is V11() real ext-real Element of REAL
f . p5 is set
p5 is V11() real ext-real Element of REAL
f . p5 is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ex b₂ being V11() real ext-real Element of REAL st
( 0 <= b₂ & not i <= b₂ & b₁ = f . b₂ ) } is set
pk is set
p44 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 is V11() real ext-real Element of REAL
f . p5 is set
p5 is V11() real ext-real Element of REAL
f . p5 is set
pk is Element of K6( the carrier of ((TOP-REAL 2) | P))
pk \/ k is Element of K6( the carrier of ((TOP-REAL 2) | P))
p44 is set
p5 is set
f . p5 is set
Y3 is V11() real ext-real Element of REAL
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 is V11() real ext-real Element of REAL
f . k2 is set
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 is V11() real ext-real Element of REAL
f . k2 is set
p44 is set
p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y3 is V11() real ext-real Element of REAL
f . Y3 is set
Y3 is V11() real ext-real Element of REAL
f . Y3 is set
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 is V11() real ext-real Element of REAL
f . k2 is set
k2 is V11() real ext-real Element of REAL
f . k2 is set
p44 is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))
((TOP-REAL 2) | P) | p44 is non empty strict TopSpace-like SubSpace of (TOP-REAL 2) | P
p5 is non empty TopSpace-like TopStruct
the carrier of p5 is non empty set
[#] p5 is non empty non proper closed Element of K6( the carrier of p5)
K6( the carrier of p5) is set
k /\ p1 is Element of K6( the carrier of ((TOP-REAL 2) | P))
kk is set
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z is V11() real ext-real Element of REAL
f . z is set
z is V11() real ext-real Element of REAL
f . z is set
kk is Element of K6( the carrier of p5)
pk /\ the carrier of p5 is Element of K6( the carrier of ((TOP-REAL 2) | P))
pk /\ p1 is Element of K6( the carrier of ((TOP-REAL 2) | P))
Y3 is Element of K6( the carrier of p5)
kk \/ Y3 is Element of K6( the carrier of p5)
k /\ the carrier of p5 is Element of K6( the carrier of ((TOP-REAL 2) | P))
kk /\ Y3 is Element of K6( the carrier of p5)
k2 is V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | p1)) Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | p1)))
k2 . 0 is set
k2 . 1 is set
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
P is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
TOP-REAL P is non empty TopSpace-like V109() V155() V156() V157() V158() V159() V160() V161() strict RLTopStruct
the carrier of (TOP-REAL P) is non empty set
K6( the carrier of (TOP-REAL P)) is set
p1 is V43(P) FinSequence-like V135() Element of the carrier of (TOP-REAL P)
p2 is V43(P) FinSequence-like V135() Element of the carrier of (TOP-REAL P)
p is non empty Element of K6( the carrier of (TOP-REAL P))
e is non empty Element of K6( the carrier of (TOP-REAL P))
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Segment (P,p1,p2,p,p2) is Element of K6( the carrier of (TOP-REAL 2))
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p1,p2,e,f) is Element of K6( the carrier of (TOP-REAL 2))
(Segment (P,p1,p2,p,e)) \/ (Segment (P,p1,p2,e,f)) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p1,p2,p,f) is Element of K6( the carrier of (TOP-REAL 2))
Y is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,f,P,p1,p2 ) } is set
i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,e,P,p1,p2 ) } is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,e,P,p1,p2 ) } is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P,p1,p2 & LE b₁,f,P,p1,p2 ) } is set
Y is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,e,P,p1,p2 ) } is set
i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,f,P,p1,p2 ) } is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P,p1,p2 & LE b₁,f,P,p1,p2 ) } is set
i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,f,P,p1,p2 ) } is set
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p1,p2,e,f) is Element of K6( the carrier of (TOP-REAL 2))
(Segment (P,p1,p2,p,e)) /\ (Segment (P,p1,p2,e,f)) is Element of K6( the carrier of (TOP-REAL 2))
{e} is non empty set
i is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P,p1,p2 & LE b₁,f,P,p1,p2 ) } is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,e,P,p1,p2 ) } is set
Y is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P,p1,p2 & LE b₁,f,P,p1,p2 ) } is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,e,P,p1,p2 ) } is set
i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Segment (P,p1,p2,p1,p2) is Element of K6( the carrier of (TOP-REAL 2))
R_Segment (P,p1,p2,p1) is Element of K6( the carrier of (TOP-REAL 2))
L_Segment (P,p1,p2,p2) is Element of K6( the carrier of (TOP-REAL 2))
(R_Segment (P,p1,p2,p1)) /\ (L_Segment (P,p1,p2,p2)) is Element of K6( the carrier of (TOP-REAL 2))
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is non empty Element of K6( the carrier of (TOP-REAL 2))
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Segment (P,p2,p,e,f) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p2,p,p2,e) is Element of K6( the carrier of (TOP-REAL 2))
(Segment (P,p2,p,p2,e)) \/ (Segment (P,p2,p,e,f)) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p2,p,p2,f) is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2
[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))
the carrier of ((TOP-REAL 2) | P) is non empty set
K6( the carrier of ((TOP-REAL 2) | P)) is set
Y is non empty Element of K6( the carrier of (TOP-REAL 2))
i is set
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Segment (P,p2,p,f,p) is Element of K6( the carrier of (TOP-REAL 2))
(Segment (P,p2,p,p2,f)) \/ (Segment (P,p2,p,f,p)) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p2,p,p2,p) is Element of K6( the carrier of (TOP-REAL 2))
{e} is non empty set
P \ {e} is Element of K6( the carrier of (TOP-REAL 2))
pk is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))
((TOP-REAL 2) | P) | pk is non empty strict TopSpace-like SubSpace of (TOP-REAL 2) | P
the carrier of (((TOP-REAL 2) | P) | pk) is non empty set
Segment (p1,e,f,k,f) is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (Segment (p1,e,f,k,f)) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,k,f))) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,k,f)))) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,k,f))))) is set
p5 is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,k,f)))) Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,k,f)))))
p5 . 0 is set
p5 . 1 is set
rng p5 is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,k,f))))
K6( the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,k,f)))) is set
[#] ((TOP-REAL 2) | (Segment (p1,e,f,k,f))) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,k,f))))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p2,b₁,P,p2,p & LE b₁,e,P,p2,p ) } is set
Y3 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Segment (P,p2,p,p2,k) is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (Segment (P,p2,p,p2,k)) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,k))) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,k)))) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,k))))) is set
kk is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,k)))) Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,k)))))
kk . 0 is set
kk . 1 is set
rng kk is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,k))))
K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,k)))) is set
[#] ((TOP-REAL 2) | (Segment (P,p2,p,p2,k))) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,k))))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p2,b₁,P,p2,p & LE b₁,k,P,p2,p ) } is set
k2 is set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
dom kk is V143() V144() V145() Element of K6( the carrier of I[01])
K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)) is V22() set
K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk))) is set
K6( the carrier of (((TOP-REAL 2) | P) | pk)) is set
k2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)))
z is Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
k2 " z is V143() V144() V145() Element of K6( the carrier of I[01])
p44 is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | p44 is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p44) is set
[#] ((TOP-REAL 2) | p44) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | p44))
K6( the carrier of ((TOP-REAL 2) | p44)) is set
G2 is Element of K6( the carrier of (TOP-REAL 2))
G2 /\ ([#] ((TOP-REAL 2) | p44)) is Element of K6( the carrier of ((TOP-REAL 2) | p44))
G2 /\ ([#] ((TOP-REAL 2) | (Segment (P,p2,p,p2,k)))) is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,k))))
G4 is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,k))))
rng k2 is non empty Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
kk " G4 is V143() V144() V145() Element of K6( the carrier of I[01])
G2 /\ (Segment (P,p2,p,p2,k)) is Element of K6( the carrier of (TOP-REAL 2))
k2 " (G2 /\ (Segment (P,p2,p,p2,k))) is V143() V144() V145() Element of K6( the carrier of I[01])
k2 " G2 is V143() V144() V145() Element of K6( the carrier of I[01])
k2 " (Segment (P,p2,p,p2,k)) is V143() V144() V145() Element of K6( the carrier of I[01])
(k2 " G2) /\ (k2 " (Segment (P,p2,p,p2,k))) is V143() V144() V145() Element of K6( the carrier of I[01])
k2 " ([#] ((TOP-REAL 2) | p44)) is V143() V144() V145() Element of K6( the carrier of I[01])
(k2 " G2) /\ (k2 " ([#] ((TOP-REAL 2) | p44))) is V143() V144() V145() Element of K6( the carrier of I[01])
k2 " p44 is V143() V144() V145() Element of K6( the carrier of I[01])
(k2 " G2) /\ (k2 " p44) is V143() V144() V145() Element of K6( the carrier of I[01])
(rng k2) /\ p44 is Element of K6( the carrier of (TOP-REAL 2))
k2 " ((rng k2) /\ p44) is V143() V144() V145() Element of K6( the carrier of I[01])
(k2 " G2) /\ (k2 " ((rng k2) /\ p44)) is V143() V144() V145() Element of K6( the carrier of I[01])
[#] (((TOP-REAL 2) | P) | pk) is non empty non proper closed Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
Y3 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
kk is Element of the carrier of (((TOP-REAL 2) | P) | pk)
K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)) is V22() set
K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk))) is set
Y3 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
kk is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)))
kk . 0 is set
kk . 1 is set
kk is Element of the carrier of (((TOP-REAL 2) | P) | pk)
Y3 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
kk is Element of the carrier of (((TOP-REAL 2) | P) | pk)
Y3 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
kk is Element of the carrier of (((TOP-REAL 2) | P) | pk)
kk is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of Y3,kk
kk . 0 is set
kk . 1 is set
k2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of Y3,kk
k2 . 0 is set
k2 . 1 is set
kk is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of Y3,kk
kk . 0 is set
kk . 1 is set
(TOP-REAL 2) | (Segment (P,p2,p,f,p)) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,f,p))) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,f,p)))) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,f,p))))) is set
k2 is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,f,p)))) Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,f,p)))))
k2 . 0 is set
k2 . 1 is set
rng k2 is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,f,p))))
K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,f,p)))) is set
[#] ((TOP-REAL 2) | (Segment (P,p2,p,f,p))) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,f,p))))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f,b₁,P,p2,p & LE b₁,p,P,p2,p ) } is set
z is set
G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
dom k2 is V143() V144() V145() Element of K6( the carrier of I[01])
K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)) is V22() set
K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk))) is set
K6( the carrier of (((TOP-REAL 2) | P) | pk)) is set
z is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)))
G2 is Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
z " G2 is V143() V144() V145() Element of K6( the carrier of I[01])
p44 is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | p44 is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p44) is set
[#] ((TOP-REAL 2) | p44) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | p44))
K6( the carrier of ((TOP-REAL 2) | p44)) is set
G4 is Element of K6( the carrier of (TOP-REAL 2))
G4 /\ ([#] ((TOP-REAL 2) | p44)) is Element of K6( the carrier of ((TOP-REAL 2) | p44))
G4 /\ ([#] ((TOP-REAL 2) | (Segment (P,p2,p,f,p)))) is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,f,p))))
G5 is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,f,p))))
rng z is non empty Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
k2 " G5 is V143() V144() V145() Element of K6( the carrier of I[01])
G4 /\ (Segment (P,p2,p,f,p)) is Element of K6( the carrier of (TOP-REAL 2))
z " (G4 /\ (Segment (P,p2,p,f,p))) is V143() V144() V145() Element of K6( the carrier of I[01])
z " G4 is V143() V144() V145() Element of K6( the carrier of I[01])
z " (Segment (P,p2,p,f,p)) is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " (Segment (P,p2,p,f,p))) is V143() V144() V145() Element of K6( the carrier of I[01])
z " ([#] ((TOP-REAL 2) | p44)) is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " ([#] ((TOP-REAL 2) | p44))) is V143() V144() V145() Element of K6( the carrier of I[01])
z " p44 is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " p44) is V143() V144() V145() Element of K6( the carrier of I[01])
(rng z) /\ p44 is Element of K6( the carrier of (TOP-REAL 2))
z " ((rng z) /\ p44) is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " ((rng z) /\ p44)) is V143() V144() V145() Element of K6( the carrier of I[01])
[#] (((TOP-REAL 2) | P) | pk) is non empty non proper closed Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
k2 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
z is Element of the carrier of (((TOP-REAL 2) | P) | pk)
K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)) is V22() set
K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk))) is set
k2 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
k2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)))
k2 . 0 is set
k2 . 1 is set
z is Element of the carrier of (((TOP-REAL 2) | P) | pk)
k2 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
z is Element of the carrier of (((TOP-REAL 2) | P) | pk)
k2 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
z is Element of the carrier of (((TOP-REAL 2) | P) | pk)
k2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of k2,z
k2 . 0 is set
k2 . 1 is set
z is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of k2,z
z . 0 is set
z . 1 is set
k2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of k2,z
k2 . 0 is set
k2 . 1 is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE k,b₁,p1,e,f & LE b₁,f,p1,e,f ) } is set
z is set
G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
dom p5 is V143() V144() V145() Element of K6( the carrier of I[01])
K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)) is V22() set
K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk))) is set
K6( the carrier of (((TOP-REAL 2) | P) | pk)) is set
z is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)))
G2 is Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
z " G2 is V143() V144() V145() Element of K6( the carrier of I[01])
p44 is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | p44 is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p44) is set
[#] ((TOP-REAL 2) | p44) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | p44))
K6( the carrier of ((TOP-REAL 2) | p44)) is set
G4 is Element of K6( the carrier of (TOP-REAL 2))
G4 /\ ([#] ((TOP-REAL 2) | p44)) is Element of K6( the carrier of ((TOP-REAL 2) | p44))
G4 /\ ([#] ((TOP-REAL 2) | (Segment (p1,e,f,k,f)))) is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,k,f))))
G5 is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,k,f))))
rng z is non empty Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
p5 " G5 is V143() V144() V145() Element of K6( the carrier of I[01])
G4 /\ (Segment (p1,e,f,k,f)) is Element of K6( the carrier of (TOP-REAL 2))
z " (G4 /\ (Segment (p1,e,f,k,f))) is V143() V144() V145() Element of K6( the carrier of I[01])
z " G4 is V143() V144() V145() Element of K6( the carrier of I[01])
z " (Segment (p1,e,f,k,f)) is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " (Segment (p1,e,f,k,f))) is V143() V144() V145() Element of K6( the carrier of I[01])
z " ([#] ((TOP-REAL 2) | p44)) is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " ([#] ((TOP-REAL 2) | p44))) is V143() V144() V145() Element of K6( the carrier of I[01])
z " p44 is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " p44) is V143() V144() V145() Element of K6( the carrier of I[01])
(rng z) /\ p44 is Element of K6( the carrier of (TOP-REAL 2))
z " ((rng z) /\ p44) is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " ((rng z) /\ p44)) is V143() V144() V145() Element of K6( the carrier of I[01])
[#] (((TOP-REAL 2) | P) | pk) is non empty non proper closed Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
G2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of kk,k2
kk + G2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of Y3,k2
(kk + G2) . 1 is set
(kk + G2) . 0 is set
(kk + G2) + k2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of Y3,z
((kk + G2) + k2) . 1 is set
((kk + G2) + k2) . 0 is set
{f} is non empty set
P \ {f} is Element of K6( the carrier of (TOP-REAL 2))
pk is non empty Element of K6( the carrier of ((TOP-REAL 2) | P))
((TOP-REAL 2) | P) | pk is non empty strict TopSpace-like SubSpace of (TOP-REAL 2) | P
the carrier of (((TOP-REAL 2) | P) | pk) is non empty set
Segment (p1,e,f,e,k) is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (Segment (p1,e,f,e,k)) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,e,k))) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,e,k)))) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,e,k))))) is set
p5 is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,e,k)))) Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,e,k)))))
p5 . 0 is set
p5 . 1 is set
rng p5 is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,e,k))))
K6( the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,e,k)))) is set
[#] ((TOP-REAL 2) | (Segment (p1,e,f,e,k))) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,e,k))))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f,b₁,P,p2,p & LE b₁,p,P,p2,p ) } is set
Y3 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Segment (P,p2,p,k,p) is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | (Segment (P,p2,p,k,p)) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,k,p))) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,k,p)))) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,k,p))))) is set
kk is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,k,p)))) Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,k,p)))))
kk . 0 is set
kk . 1 is set
rng kk is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,k,p))))
K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,k,p)))) is set
[#] ((TOP-REAL 2) | (Segment (P,p2,p,k,p))) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,k,p))))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE k,b₁,P,p2,p & LE b₁,p,P,p2,p ) } is set
k2 is set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
dom kk is V143() V144() V145() Element of K6( the carrier of I[01])
K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)) is V22() set
K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk))) is set
K6( the carrier of (((TOP-REAL 2) | P) | pk)) is set
k2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)))
z is Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
k2 " z is V143() V144() V145() Element of K6( the carrier of I[01])
p44 is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | p44 is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p44) is set
[#] ((TOP-REAL 2) | p44) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | p44))
K6( the carrier of ((TOP-REAL 2) | p44)) is set
G2 is Element of K6( the carrier of (TOP-REAL 2))
G2 /\ ([#] ((TOP-REAL 2) | p44)) is Element of K6( the carrier of ((TOP-REAL 2) | p44))
G2 /\ ([#] ((TOP-REAL 2) | (Segment (P,p2,p,k,p)))) is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,k,p))))
G4 is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,k,p))))
rng k2 is non empty Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
kk " G4 is V143() V144() V145() Element of K6( the carrier of I[01])
G2 /\ (Segment (P,p2,p,k,p)) is Element of K6( the carrier of (TOP-REAL 2))
k2 " (G2 /\ (Segment (P,p2,p,k,p))) is V143() V144() V145() Element of K6( the carrier of I[01])
k2 " G2 is V143() V144() V145() Element of K6( the carrier of I[01])
k2 " (Segment (P,p2,p,k,p)) is V143() V144() V145() Element of K6( the carrier of I[01])
(k2 " G2) /\ (k2 " (Segment (P,p2,p,k,p))) is V143() V144() V145() Element of K6( the carrier of I[01])
k2 " ([#] ((TOP-REAL 2) | p44)) is V143() V144() V145() Element of K6( the carrier of I[01])
(k2 " G2) /\ (k2 " ([#] ((TOP-REAL 2) | p44))) is V143() V144() V145() Element of K6( the carrier of I[01])
k2 " p44 is V143() V144() V145() Element of K6( the carrier of I[01])
(k2 " G2) /\ (k2 " p44) is V143() V144() V145() Element of K6( the carrier of I[01])
(rng k2) /\ p44 is Element of K6( the carrier of (TOP-REAL 2))
k2 " ((rng k2) /\ p44) is V143() V144() V145() Element of K6( the carrier of I[01])
(k2 " G2) /\ (k2 " ((rng k2) /\ p44)) is V143() V144() V145() Element of K6( the carrier of I[01])
[#] (((TOP-REAL 2) | P) | pk) is non empty non proper closed Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
kk is Element of the carrier of (((TOP-REAL 2) | P) | pk)
z is Element of the carrier of (((TOP-REAL 2) | P) | pk)
K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)) is V22() set
K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk))) is set
z is Element of the carrier of (((TOP-REAL 2) | P) | pk)
kk is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)))
kk . 0 is set
kk . 1 is set
kk is Element of the carrier of (((TOP-REAL 2) | P) | pk)
kk is Element of the carrier of (((TOP-REAL 2) | P) | pk)
z is Element of the carrier of (((TOP-REAL 2) | P) | pk)
kk is Element of the carrier of (((TOP-REAL 2) | P) | pk)
z is Element of the carrier of (((TOP-REAL 2) | P) | pk)
kk is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of kk,z
kk . 0 is set
kk . 1 is set
k2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of kk,z
k2 . 0 is set
k2 . 1 is set
kk is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of kk,z
kk . 0 is set
kk . 1 is set
(TOP-REAL 2) | (Segment (P,p2,p,p2,e)) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,e))) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,e)))) is V22() set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,e))))) is set
k2 is V22() V25( the carrier of I[01]) V26( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,e)))) Function-like quasi_total Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,e)))))
k2 . 0 is set
k2 . 1 is set
rng k2 is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,e))))
K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,e)))) is set
[#] ((TOP-REAL 2) | (Segment (P,p2,p,p2,e))) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,e))))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p2,b₁,P,p2,p & LE b₁,e,P,p2,p ) } is set
z is set
G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
dom k2 is V143() V144() V145() Element of K6( the carrier of I[01])
K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)) is V22() set
K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk))) is set
K6( the carrier of (((TOP-REAL 2) | P) | pk)) is set
z is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)))
G2 is Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
z " G2 is V143() V144() V145() Element of K6( the carrier of I[01])
p44 is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | p44 is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p44) is set
[#] ((TOP-REAL 2) | p44) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | p44))
K6( the carrier of ((TOP-REAL 2) | p44)) is set
G4 is Element of K6( the carrier of (TOP-REAL 2))
G4 /\ ([#] ((TOP-REAL 2) | p44)) is Element of K6( the carrier of ((TOP-REAL 2) | p44))
G4 /\ ([#] ((TOP-REAL 2) | (Segment (P,p2,p,p2,e)))) is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,e))))
G5 is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (P,p2,p,p2,e))))
rng z is non empty Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
k2 " G5 is V143() V144() V145() Element of K6( the carrier of I[01])
G4 /\ (Segment (P,p2,p,p2,e)) is Element of K6( the carrier of (TOP-REAL 2))
z " (G4 /\ (Segment (P,p2,p,p2,e))) is V143() V144() V145() Element of K6( the carrier of I[01])
z " G4 is V143() V144() V145() Element of K6( the carrier of I[01])
z " (Segment (P,p2,p,p2,e)) is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " (Segment (P,p2,p,p2,e))) is V143() V144() V145() Element of K6( the carrier of I[01])
z " ([#] ((TOP-REAL 2) | p44)) is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " ([#] ((TOP-REAL 2) | p44))) is V143() V144() V145() Element of K6( the carrier of I[01])
z " p44 is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " p44) is V143() V144() V145() Element of K6( the carrier of I[01])
(rng z) /\ p44 is Element of K6( the carrier of (TOP-REAL 2))
z " ((rng z) /\ p44) is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " ((rng z) /\ p44)) is V143() V144() V145() Element of K6( the carrier of I[01])
[#] (((TOP-REAL 2) | P) | pk) is non empty non proper closed Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
Y3 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
k2 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)) is V22() set
K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk))) is set
k2 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
k2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)))
k2 . 0 is set
k2 . 1 is set
Y3 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
Y3 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
k2 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
Y3 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
k2 is Element of the carrier of (((TOP-REAL 2) | P) | pk)
k2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of Y3,k2
k2 . 0 is set
k2 . 1 is set
z is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of Y3,k2
z . 0 is set
z . 1 is set
k2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of Y3,k2
k2 . 0 is set
k2 . 1 is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,p1,e,f & LE b₁,k,p1,e,f ) } is set
z is set
G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
G2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
dom p5 is V143() V144() V145() Element of K6( the carrier of I[01])
K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)) is V22() set
K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk))) is set
K6( the carrier of (((TOP-REAL 2) | P) | pk)) is set
z is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Element of K6(K7( the carrier of I[01], the carrier of (((TOP-REAL 2) | P) | pk)))
G2 is Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
z " G2 is V143() V144() V145() Element of K6( the carrier of I[01])
p44 is Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | p44 is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p44) is set
[#] ((TOP-REAL 2) | p44) is non proper closed Element of K6( the carrier of ((TOP-REAL 2) | p44))
K6( the carrier of ((TOP-REAL 2) | p44)) is set
G4 is Element of K6( the carrier of (TOP-REAL 2))
G4 /\ ([#] ((TOP-REAL 2) | p44)) is Element of K6( the carrier of ((TOP-REAL 2) | p44))
G4 /\ ([#] ((TOP-REAL 2) | (Segment (p1,e,f,e,k)))) is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,e,k))))
G5 is Element of K6( the carrier of ((TOP-REAL 2) | (Segment (p1,e,f,e,k))))
rng z is non empty Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
p5 " G5 is V143() V144() V145() Element of K6( the carrier of I[01])
G4 /\ (Segment (p1,e,f,e,k)) is Element of K6( the carrier of (TOP-REAL 2))
z " (G4 /\ (Segment (p1,e,f,e,k))) is V143() V144() V145() Element of K6( the carrier of I[01])
z " G4 is V143() V144() V145() Element of K6( the carrier of I[01])
z " (Segment (p1,e,f,e,k)) is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " (Segment (p1,e,f,e,k))) is V143() V144() V145() Element of K6( the carrier of I[01])
z " ([#] ((TOP-REAL 2) | p44)) is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " ([#] ((TOP-REAL 2) | p44))) is V143() V144() V145() Element of K6( the carrier of I[01])
z " p44 is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " p44) is V143() V144() V145() Element of K6( the carrier of I[01])
(rng z) /\ p44 is Element of K6( the carrier of (TOP-REAL 2))
z " ((rng z) /\ p44) is V143() V144() V145() Element of K6( the carrier of I[01])
(z " G4) /\ (z " ((rng z) /\ p44)) is V143() V144() V145() Element of K6( the carrier of I[01])
[#] (((TOP-REAL 2) | P) | pk) is non empty non proper closed Element of K6( the carrier of (((TOP-REAL 2) | P) | pk))
G2 is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of k2,kk
G2 + kk is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of k2,z
(G2 + kk) . 1 is set
(G2 + kk) . 0 is set
k2 + (G2 + kk) is non empty V22() V25( the carrier of I[01]) V26( the carrier of (((TOP-REAL 2) | P) | pk)) Function-like total quasi_total Path of Y3,z
(k2 + (G2 + kk)) . 1 is set
(k2 + (G2 + kk)) . 0 is set
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e `1 is V11() real ext-real Element of REAL
LSeg (p,e) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * p) + (b₁ * e)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
f is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y is V11() real ext-real Element of REAL
p `1 is V11() real ext-real Element of REAL
i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
i `1 is V11() real ext-real Element of REAL
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
{p} is non empty set
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,e,P,p1,p2 ) } is set
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f `1 is V11() real ext-real Element of REAL
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{p} is non empty set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P,p1,p2 & LE b₁,p,P,p1,p2 ) } is set
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f `1 is V11() real ext-real Element of REAL
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e `1 is V11() real ext-real Element of REAL
LSeg (p,e) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * p) + (b₁ * e)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
f is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y is V11() real ext-real Element of REAL
p `1 is V11() real ext-real Element of REAL
i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
i `1 is V11() real ext-real Element of REAL
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
{p} is non empty set
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,e,P,p1,p2 ) } is set
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f `1 is V11() real ext-real Element of REAL
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{p} is non empty set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P,p1,p2 & LE b₁,p,P,p1,p2 ) } is set
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f `1 is V11() real ext-real Element of REAL
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e `1 is V11() real ext-real Element of REAL
LSeg (p,e) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * p) + (b₁ * e)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
f is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y is V11() real ext-real Element of REAL
p `1 is V11() real ext-real Element of REAL
i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
i `1 is V11() real ext-real Element of REAL
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
{p} is non empty set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P,p1,p2 & LE b₁,p,P,p1,p2 ) } is set
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f `1 is V11() real ext-real Element of REAL
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{p} is non empty set
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,e,P,p1,p2 ) } is set
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f `1 is V11() real ext-real Element of REAL
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
e `1 is V11() real ext-real Element of REAL
LSeg (p,e) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * p) + (b₁ * e)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
f is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y is V11() real ext-real Element of REAL
p `1 is V11() real ext-real Element of REAL
i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
i `1 is V11() real ext-real Element of REAL
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
{p} is non empty set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Segment (P,p1,p2,e,p) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P,p1,p2 & LE b₁,p,P,p1,p2 ) } is set
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f `1 is V11() real ext-real Element of REAL
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (e,p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * e) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{p} is non empty set
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
Segment (P,p1,p2,p,e) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,e,P,p1,p2 ) } is set
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f `1 is V11() real ext-real Element of REAL
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p1 `1 is V11() real ext-real Element of REAL
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p `1 is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
f is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
f /. (len f) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
{ (LSeg (f,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
union { (LSeg (f,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
Y is set
i is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
LSeg (f,i) is Element of K6( the carrier of (TOP-REAL 2))
i + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
i - 1 is V11() real ext-real Element of REAL
k is set
dom f is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
f . 1 is set
i -' 1 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
i -' (i -' 1) is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
f . (i -' (i -' 1)) is set
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k `1 is V11() real ext-real Element of REAL
k is ordinal natural V11() real ext-real non negative set
i -' k is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
f . (i -' k) is set
k is ordinal natural V11() real ext-real non negative set
i -' k is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
f . (i -' k) is set
k + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(i - 1) + 1 is V11() real ext-real Element of REAL
1 + k is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(1 + k) - k is V11() real ext-real Element of REAL
i - k is V11() real ext-real set
f /. (i -' k) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
pk `1 is V11() real ext-real Element of REAL
f /. i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f . i is set
mid (f,i,(len f)) is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
p5 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
Seg (len f) is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
1 + i is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + (1 + i) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + (len f) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(1 + 1) + i is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
((1 + 1) + i) - i is V11() real ext-real Element of REAL
(len f) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
((len f) + 1) - i is V11() real ext-real Element of REAL
(len f) - i is V11() real ext-real Element of REAL
(len f) -' i is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
((len f) -' i) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
0 + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
Y3 is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len Y3 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
Seg (len Y3) is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
dom Y3 is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
Y3 /. (1 + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y3 . (1 + 1) is set
(1 + 1) - 1 is V11() real ext-real Element of REAL
((1 + 1) - 1) + i is V11() real ext-real Element of REAL
f . (((1 + 1) - 1) + i) is set
f /. (i + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y3 /. 1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y3 . 1 is set
1 - 1 is V11() real ext-real Element of REAL
(1 - 1) + i is V11() real ext-real Element of REAL
f . ((1 - 1) + i) is set
LSeg ((f /. i),(f /. (i + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. i)) + (b₁ * (f /. (i + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (Y3,1) is Element of K6( the carrier of (TOP-REAL 2))
{ (LSeg (Y3,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len Y3 ) } is set
union { (LSeg (Y3,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len Y3 ) } is set
L~ (mid (f,i,(len f))) is Element of K6( the carrier of (TOP-REAL 2))
LSeg ((f /. i),p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. i)) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk `1 is V11() real ext-real Element of REAL
Segment (P,p1,p2,(f /. i),p) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f /. i,b₁,P,p1,p2 & LE b₁,p,P,p1,p2 ) } is set
mid (f,i,(len f)) is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
p44 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
Seg (len f) is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
1 + i is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + (1 + i) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + (len f) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(1 + 1) + i is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
((1 + 1) + i) - i is V11() real ext-real Element of REAL
(len f) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
((len f) + 1) - i is V11() real ext-real Element of REAL
(len f) - i is V11() real ext-real Element of REAL
(len f) -' i is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
((len f) -' i) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
0 + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
p5 is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len p5 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
Seg (len p5) is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
dom p5 is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
p5 /. (1 + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 . (1 + 1) is set
(1 + 1) - 1 is V11() real ext-real Element of REAL
((1 + 1) - 1) + i is V11() real ext-real Element of REAL
f . (((1 + 1) - 1) + i) is set
f /. (i + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 /. 1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 . 1 is set
1 - 1 is V11() real ext-real Element of REAL
(1 - 1) + i is V11() real ext-real Element of REAL
f . ((1 - 1) + i) is set
f /. i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg ((f /. i),(f /. (i + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. i)) + (b₁ * (f /. (i + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (p5,1) is Element of K6( the carrier of (TOP-REAL 2))
{ (LSeg (p5,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p5 ) } is set
union { (LSeg (p5,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p5 ) } is set
L~ (mid (f,i,(len f))) is Element of K6( the carrier of (TOP-REAL 2))
mid (f,1,i) is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
(i + 1) - 1 is V11() real ext-real Element of REAL
(f /. i) `1 is V11() real ext-real Element of REAL
f . i is set
i -' 0 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
f . (i -' 0) is set
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
z is set
kk is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
LSeg (f,kk) is Element of K6( the carrier of (TOP-REAL 2))
kk + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
f /. kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f /. (kk + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg ((f /. kk),(f /. (kk + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. kk)) + (b₁ * (f /. (kk + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(f /. kk) `1 is V11() real ext-real Element of REAL
k2 is set
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
(f /. kk) `2 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `2 is V11() real ext-real Element of REAL
f . kk is set
f . (kk + 1) is set
i -' kk is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
i - kk is V11() real ext-real set
(i - kk) + kk is V11() real ext-real set
0 + kk is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
i - (i -' kk) is V11() real ext-real set
i -' (i -' kk) is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
f . (i -' (i -' kk)) is set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
f /. (i -' (i -' kk)) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f /. kk,b₁, L~ f,f /. 1,f /. (len f) & LE b₁,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } is set
(f /. (i -' k)) `1 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
(f /. kk) `1 is V11() real ext-real Element of REAL
i -' kk is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
(i -' kk) -' 1 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
z is set
f . kk is set
f . (kk + 1) is set
Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f /. kk,b₁, L~ f,f /. 1,f /. (len f) & LE b₁,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } is set
i - kk is V11() real ext-real set
(i - kk) - 1 is V11() real ext-real Element of REAL
i - (kk + 1) is V11() real ext-real Element of REAL
(i - (kk + 1)) + (kk + 1) is V11() real ext-real Element of REAL
0 + (kk + 1) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(f /. kk) `2 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `2 is V11() real ext-real Element of REAL
((i - kk) - 1) + 1 is V11() real ext-real Element of REAL
i - ((i -' kk) -' 1) is V11() real ext-real set
i - ((i - kk) - 1) is V11() real ext-real Element of REAL
i -' ((i -' kk) -' 1) is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
f . (i -' ((i -' kk) -' 1)) is set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
(f /. kk) `1 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
(f /. kk) `1 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
Segment (P,p1,p2,(f /. i),p) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f /. i,b₁,P,p1,p2 & LE b₁,p,P,p1,p2 ) } is set
LSeg ((f /. i),p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. i)) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{(f /. i)} is non empty set
Y3 is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len Y3 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
(i -' 1) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(i -' k) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
LSeg (Y3,(i -' k)) is Element of K6( the carrier of (TOP-REAL 2))
Y3 /. (i -' k) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y3 /. ((i -' k) + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg ((Y3 /. (i -' k)),(Y3 /. ((i -' k) + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (Y3 /. (i -' k))) + (b₁ * (Y3 /. ((i -' k) + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Seg (len Y3) is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
dom Y3 is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
Y3 . (i -' k) is set
(i -' k) - 1 is V11() real ext-real Element of REAL
((i -' k) - 1) + 1 is V11() real ext-real Element of REAL
f . (((i -' k) - 1) + 1) is set
{ (LSeg (Y3,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len Y3 ) } is set
union { (LSeg (Y3,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len Y3 ) } is set
L~ (mid (f,1,i)) is Element of K6( the carrier of (TOP-REAL 2))
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
pk `1 is V11() real ext-real Element of REAL
f /. i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f . i is set
mid (f,i,(len f)) is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
p5 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
Seg (len f) is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
1 + i is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + (1 + i) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + (len f) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(1 + 1) + i is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
((1 + 1) + i) - i is V11() real ext-real Element of REAL
(len f) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
((len f) + 1) - i is V11() real ext-real Element of REAL
(len f) - i is V11() real ext-real Element of REAL
(len f) -' i is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
((len f) -' i) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
0 + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
Y3 is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len Y3 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
Seg (len Y3) is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
dom Y3 is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
Y3 /. (1 + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y3 . (1 + 1) is set
(1 + 1) - 1 is V11() real ext-real Element of REAL
((1 + 1) - 1) + i is V11() real ext-real Element of REAL
f . (((1 + 1) - 1) + i) is set
f /. (i + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y3 /. 1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y3 . 1 is set
1 - 1 is V11() real ext-real Element of REAL
(1 - 1) + i is V11() real ext-real Element of REAL
f . ((1 - 1) + i) is set
LSeg ((f /. i),(f /. (i + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. i)) + (b₁ * (f /. (i + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (Y3,1) is Element of K6( the carrier of (TOP-REAL 2))
{ (LSeg (Y3,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len Y3 ) } is set
union { (LSeg (Y3,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len Y3 ) } is set
L~ (mid (f,i,(len f))) is Element of K6( the carrier of (TOP-REAL 2))
LSeg ((f /. i),p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. i)) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk `1 is V11() real ext-real Element of REAL
Segment (P,p1,p2,(f /. i),p) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f /. i,b₁,P,p1,p2 & LE b₁,p,P,p1,p2 ) } is set
mid (f,i,(len f)) is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
p44 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
Seg (len f) is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
1 + i is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + (1 + i) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + (len f) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(1 + 1) + i is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
((1 + 1) + i) - i is V11() real ext-real Element of REAL
(len f) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
((len f) + 1) - i is V11() real ext-real Element of REAL
(len f) - i is V11() real ext-real Element of REAL
(len f) -' i is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
((len f) -' i) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
0 + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
p5 is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len p5 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
Seg (len p5) is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
dom p5 is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
p5 /. (1 + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 . (1 + 1) is set
(1 + 1) - 1 is V11() real ext-real Element of REAL
((1 + 1) - 1) + i is V11() real ext-real Element of REAL
f . (((1 + 1) - 1) + i) is set
f /. (i + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 /. 1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 . 1 is set
1 - 1 is V11() real ext-real Element of REAL
(1 - 1) + i is V11() real ext-real Element of REAL
f . ((1 - 1) + i) is set
f /. i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg ((f /. i),(f /. (i + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. i)) + (b₁ * (f /. (i + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (p5,1) is Element of K6( the carrier of (TOP-REAL 2))
{ (LSeg (p5,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p5 ) } is set
union { (LSeg (p5,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p5 ) } is set
L~ (mid (f,i,(len f))) is Element of K6( the carrier of (TOP-REAL 2))
mid (f,1,i) is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
(i + 1) - 1 is V11() real ext-real Element of REAL
(f /. i) `1 is V11() real ext-real Element of REAL
f . i is set
i -' 0 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
f . (i -' 0) is set
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
z is set
kk is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
LSeg (f,kk) is Element of K6( the carrier of (TOP-REAL 2))
kk + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
f /. kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f /. (kk + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg ((f /. kk),(f /. (kk + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. kk)) + (b₁ * (f /. (kk + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(f /. kk) `1 is V11() real ext-real Element of REAL
i -' kk is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
i - kk is V11() real ext-real set
(i - kk) + kk is V11() real ext-real set
0 + kk is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
i - (i -' kk) is V11() real ext-real set
i - (i - kk) is V11() real ext-real set
i -' (i -' kk) is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
f . (i -' (i -' kk)) is set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
f /. (i -' (i -' kk)) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z is set
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
(f /. kk) `2 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `2 is V11() real ext-real Element of REAL
f . kk is set
f . (kk + 1) is set
Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f /. kk,b₁, L~ f,f /. 1,f /. (len f) & LE b₁,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } is set
(f /. (i -' k)) `1 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
(f /. kk) `1 is V11() real ext-real Element of REAL
i -' kk is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
(i -' kk) -' 1 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
z is set
f . kk is set
f . (kk + 1) is set
Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f /. kk,b₁, L~ f,f /. 1,f /. (len f) & LE b₁,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } is set
i - kk is V11() real ext-real set
(i - kk) - 1 is V11() real ext-real Element of REAL
i - (kk + 1) is V11() real ext-real Element of REAL
(i - (kk + 1)) + (kk + 1) is V11() real ext-real Element of REAL
0 + (kk + 1) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(f /. kk) `2 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `2 is V11() real ext-real Element of REAL
((i - kk) - 1) + 1 is V11() real ext-real Element of REAL
i - ((i -' kk) -' 1) is V11() real ext-real set
i - ((i - kk) - 1) is V11() real ext-real Element of REAL
i -' ((i -' kk) -' 1) is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
f . (i -' ((i -' kk) -' 1)) is set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
(f /. kk) `1 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
(f /. kk) `1 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
Segment (P,p1,p2,(f /. i),p) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f /. i,b₁,P,p1,p2 & LE b₁,p,P,p1,p2 ) } is set
LSeg ((f /. i),p) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. i)) + (b₁ * p)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{(f /. i)} is non empty set
Y3 is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
len Y3 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
(i -' 1) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(i -' k) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
LSeg (Y3,(i -' k)) is Element of K6( the carrier of (TOP-REAL 2))
Y3 /. (i -' k) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Y3 /. ((i -' k) + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg ((Y3 /. (i -' k)),(Y3 /. ((i -' k) + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (Y3 /. (i -' k))) + (b₁ * (Y3 /. ((i -' k) + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Seg (len Y3) is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
dom Y3 is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
Y3 . (i -' k) is set
(i -' k) - 1 is V11() real ext-real Element of REAL
((i -' k) - 1) + 1 is V11() real ext-real Element of REAL
f . (((i -' k) - 1) + 1) is set
{ (LSeg (Y3,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len Y3 ) } is set
union { (LSeg (Y3,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len Y3 ) } is set
L~ (mid (f,1,i)) is Element of K6( the carrier of (TOP-REAL 2))
k2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k2 `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
pk `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
pk `1 is V11() real ext-real Element of REAL
P is non empty Element of K6( the carrier of (TOP-REAL 2))
p1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p2 `1 is V11() real ext-real Element of REAL
p is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p `1 is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
f is V22() V25( NAT ) V26( the carrier of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f is Element of K6( the carrier of (TOP-REAL 2))
f /. 1 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
f /. (len f) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
{ (LSeg (f,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
union { (LSeg (f,b₁)) where b₁ is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
Y is set
i is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
LSeg (f,i) is Element of K6( the carrier of (TOP-REAL 2))
i + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
Seg (len f) is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
dom f is V143() V144() V145() V146() V147() V148() bounded_below Element of K6(NAT)
k is set
(len f) - (i + 1) is V11() real ext-real Element of REAL
(len f) -' (i + 1) is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
(i + 1) + ((len f) -' (i + 1)) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(i + 1) + ((len f) - (i + 1)) is V11() real ext-real Element of REAL
f . ((i + 1) + ((len f) -' (i + 1))) is set
k is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k `1 is V11() real ext-real Element of REAL
k is ordinal natural V11() real ext-real non negative set
(i + 1) + k is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
f . ((i + 1) + k) is set
k is ordinal natural V11() real ext-real non negative set
(i + 1) + k is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
f . ((i + 1) + k) is set
k + (i + 1) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
((len f) - (i + 1)) + (i + 1) is V11() real ext-real Element of REAL
i + k is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
(i + k) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
f /. ((i + 1) + k) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
k + i is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
(k + i) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
pk `1 is V11() real ext-real Element of REAL
f /. (i + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg (p,(f /. (i + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * p) + (b₁ * (f /. (i + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
f /. i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg ((f /. i),(f /. (i + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. i)) + (b₁ * (f /. (i + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 `1 is V11() real ext-real Element of REAL
Segment (P,p1,p2,p,(f /. (i + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,f /. (i + 1),P,p1,p2 ) } is set
f /. (i + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
(f /. (i + 1)) `1 is V11() real ext-real Element of REAL
(i + 1) + 0 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
f . ((i + 1) + 0) is set
p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 `1 is V11() real ext-real Element of REAL
f /. i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg ((f /. i),(f /. (i + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. i)) + (b₁ * (f /. (i + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 `1 is V11() real ext-real Element of REAL
p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 `1 is V11() real ext-real Element of REAL
Y3 is set
kk is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
LSeg (f,kk) is Element of K6( the carrier of (TOP-REAL 2))
kk + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
f /. (kk + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f /. kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk - 1 is V11() real ext-real Element of REAL
LSeg ((f /. kk),(f /. (kk + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. kk)) + (b₁ * (f /. (kk + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
f . kk is set
f . (kk + 1) is set
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
kk -' i is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
kk - i is V11() real ext-real set
0 + i is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
(kk - i) + i is V11() real ext-real set
(i + 1) + (kk -' i) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + i is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(1 + i) + (kk - i) is V11() real ext-real Element of REAL
z is set
(f /. kk) `1 is V11() real ext-real Element of REAL
(f /. kk) `2 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `2 is V11() real ext-real Element of REAL
f . ((i + 1) + (kk -' i)) is set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
f /. ((i + 1) + (kk -' i)) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f /. kk,b₁, L~ f,f /. 1,f /. (len f) & LE b₁,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } is set
(f /. ((i + 1) + k)) `1 is V11() real ext-real Element of REAL
(f /. kk) `1 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
kk -' (i + 1) is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
z is set
Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f /. kk,b₁, L~ f,f /. 1,f /. (len f) & LE b₁,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } is set
kk - (i + 1) is V11() real ext-real Element of REAL
0 + (i + 1) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(kk - (i + 1)) + (i + 1) is V11() real ext-real Element of REAL
(LSeg ((f /. kk),(f /. (kk + 1)))) /\ (LSeg ((f /. i),(f /. (i + 1)))) is Element of K6( the carrier of (TOP-REAL 2))
kk -' 1 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
(kk -' 1) + 2 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
f . (i + 1) is set
(i + 1) - 1 is V11() real ext-real Element of REAL
(kk -' 1) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(f /. kk) `2 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `2 is V11() real ext-real Element of REAL
(i + 1) + (kk -' (i + 1)) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(i + 1) + (kk - (i + 1)) is V11() real ext-real Element of REAL
f . ((i + 1) + (kk -' (i + 1))) is set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
(f /. kk) `1 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
(f /. kk) `1 is V11() real ext-real Element of REAL
LSeg (p,(f /. (i + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * p) + (b₁ * (f /. (i + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 `1 is V11() real ext-real Element of REAL
Segment (P,p1,p2,p,(f /. (i + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,f /. (i + 1),P,p1,p2 ) } is set
{(f /. (i + 1))} is non empty set
p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
pk `1 is V11() real ext-real Element of REAL
f /. (i + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg (p,(f /. (i + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * p) + (b₁ * (f /. (i + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
f /. i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg ((f /. i),(f /. (i + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. i)) + (b₁ * (f /. (i + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 `1 is V11() real ext-real Element of REAL
Segment (P,p1,p2,p,(f /. (i + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,f /. (i + 1),P,p1,p2 ) } is set
f /. (i + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
(f /. (i + 1)) `1 is V11() real ext-real Element of REAL
(i + 1) + 0 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
f . ((i + 1) + 0) is set
p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 `1 is V11() real ext-real Element of REAL
f /. i is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
LSeg ((f /. i),(f /. (i + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. i)) + (b₁ * (f /. (i + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 `1 is V11() real ext-real Element of REAL
p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 `1 is V11() real ext-real Element of REAL
Y3 is set
kk is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
LSeg (f,kk) is Element of K6( the carrier of (TOP-REAL 2))
kk + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
f /. (kk + 1) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
f /. kk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
kk - 1 is V11() real ext-real Element of REAL
LSeg ((f /. kk),(f /. (kk + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (f /. kk)) + (b₁ * (f /. (kk + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
f . kk is set
f . (kk + 1) is set
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
kk -' i is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
kk - i is V11() real ext-real set
0 + i is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
(kk - i) + i is V11() real ext-real set
(i + 1) + (kk -' i) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
1 + i is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(1 + i) + (kk - i) is V11() real ext-real Element of REAL
z is set
(f /. kk) `1 is V11() real ext-real Element of REAL
(f /. kk) `2 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `2 is V11() real ext-real Element of REAL
f . ((i + 1) + (kk -' i)) is set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
f /. ((i + 1) + (kk -' i)) is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f /. kk,b₁, L~ f,f /. 1,f /. (len f) & LE b₁,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } is set
(f /. ((i + 1) + k)) `1 is V11() real ext-real Element of REAL
(f /. kk) `1 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
kk -' (i + 1) is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
z is set
Segment ((L~ f),(f /. 1),(f /. (len f)),(f /. kk),(f /. (kk + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE f /. kk,b₁, L~ f,f /. 1,f /. (len f) & LE b₁,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } is set
kk - (i + 1) is V11() real ext-real Element of REAL
0 + (i + 1) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(kk - (i + 1)) + (i + 1) is V11() real ext-real Element of REAL
(LSeg ((f /. kk),(f /. (kk + 1)))) /\ (LSeg ((f /. i),(f /. (i + 1)))) is Element of K6( the carrier of (TOP-REAL 2))
kk -' 1 is ordinal natural V11() real ext-real non negative V80() V81() V143() V144() V145() V146() V147() V148() bounded_below Element of NAT
(kk -' 1) + 2 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
f . (i + 1) is set
(i + 1) - 1 is V11() real ext-real Element of REAL
(kk -' 1) + 1 is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(f /. kk) `2 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `2 is V11() real ext-real Element of REAL
(i + 1) + (kk -' (i + 1)) is non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below Element of NAT
(i + 1) + (kk - (i + 1)) is V11() real ext-real Element of REAL
f . ((i + 1) + (kk -' (i + 1))) is set
z is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
z `1 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
(f /. kk) `1 is V11() real ext-real Element of REAL
(f /. (kk + 1)) `1 is V11() real ext-real Element of REAL
(f /. kk) `1 is V11() real ext-real Element of REAL
LSeg (p,(f /. (i + 1))) is non empty V226( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * p) + (b₁ * (f /. (i + 1)))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 `1 is V11() real ext-real Element of REAL
Segment (P,p1,p2,p,(f /. (i + 1))) is Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2) : ( LE p,b₁,P,p1,p2 & LE b₁,f /. (i + 1),P,p1,p2 ) } is set
{(f /. (i + 1))} is non empty set
p5 is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
p5 `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
pk `1 is V11() real ext-real Element of REAL
pk is V43(2) FinSequence-like V135() Element of the carrier of (TOP-REAL 2)
pk `1 is V11() real ext-real Element of REAL