:: TOPREAL1 semantic presentation

REAL is V154() V155() V156() V160() set
NAT is V154() V155() V156() V157() V158() V159() V160() Element of K10(REAL)
K10(REAL) is non empty set
COMPLEX is V154() V160() set
omega is V154() V155() V156() V157() V158() V159() V160() set
K10(omega) is non empty set
K10(NAT) is non empty set
1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
INT is V154() V155() V156() V157() V158() V160() set
K11(1,1) is non empty RAT -valued INT -valued V144() V145() V146() V147() set
RAT is V154() V155() V156() V157() V160() set
K10(K11(1,1)) is non empty set
K11(K11(1,1),1) is non empty RAT -valued INT -valued V144() V145() V146() V147() set
K10(K11(K11(1,1),1)) is non empty set
K11(K11(1,1),REAL) is V144() V145() V146() set
K10(K11(K11(1,1),REAL)) is non empty set
K11(REAL,REAL) is V144() V145() V146() set
K11(K11(REAL,REAL),REAL) is V144() V145() V146() set
K10(K11(K11(REAL,REAL),REAL)) is non empty set
2 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
K11(2,2) is non empty RAT -valued INT -valued V144() V145() V146() V147() set
K11(K11(2,2),REAL) is V144() V145() V146() set
K10(K11(K11(2,2),REAL)) is non empty set
K10(K11(REAL,REAL)) is non empty set
TOP-REAL 2 is non empty TopSpace-like V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K457() is non empty strict TopSpace-like V199() TopStruct
the carrier of K457() is non empty V154() V155() V156() set
RealSpace is non empty strict Reflexive discerning V103() triangle Discerning V199() MetrStruct
R^1 is non empty strict TopSpace-like V199() TopStruct
K11(COMPLEX,COMPLEX) is V144() set
K10(K11(COMPLEX,COMPLEX)) is non empty set
K11(K11(COMPLEX,COMPLEX),COMPLEX) is V144() set
K10(K11(K11(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K11(RAT,RAT) is RAT -valued V144() V145() V146() set
K10(K11(RAT,RAT)) is non empty set
K11(K11(RAT,RAT),RAT) is RAT -valued V144() V145() V146() set
K10(K11(K11(RAT,RAT),RAT)) is non empty set
K11(INT,INT) is RAT -valued INT -valued V144() V145() V146() set
K10(K11(INT,INT)) is non empty set
K11(K11(INT,INT),INT) is RAT -valued INT -valued V144() V145() V146() set
K10(K11(K11(INT,INT),INT)) is non empty set
K11(NAT,NAT) is RAT -valued INT -valued V144() V145() V146() V147() set
K11(K11(NAT,NAT),NAT) is RAT -valued INT -valued V144() V145() V146() V147() set
K10(K11(K11(NAT,NAT),NAT)) is non empty set
{} is empty Function-like functional FinSequence-membered V154() V155() V156() V157() V158() V159() V160() set
the empty Function-like functional FinSequence-membered V154() V155() V156() V157() V158() V159() V160() set is empty Function-like functional FinSequence-membered V154() V155() V156() V157() V158() V159() V160() set
3 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
0 is empty ordinal natural V14() real ext-real non positive non negative Function-like functional FinSequence-membered V91() V92() V154() V155() V156() V157() V158() V159() V160() Element of NAT
[.0,1.] is V154() V155() V156() Element of K10(REAL)
0. (TOP-REAL 2) is V45(2) FinSequence-like V61( TOP-REAL 2) V146() Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
|[0,0]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
the carrier of RealSpace is non empty V154() V155() V156() set
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V199() SubSpace of R^1
I[01] is non empty strict TopSpace-like V199() SubSpace of R^1
the carrier of I[01] is non empty V154() V155() V156() set
union {} is set
F₁() is non empty set
{ b₁ where b₁ is Element of F₁() : ( P₁[b₁] or P₂[b₁] ) } is set
{ b₁ where b₁ is Element of F₁() : P₁[b₁] } is set
{ b₁ where b₁ is Element of F₁() : P₂[b₁] } is set
{ b₁ where b₁ is Element of F₁() : P₁[b₁] } \/ { b₁ where b₁ is Element of F₁() : P₂[b₁] } is set
r is set
q is Element of F₁()
q is Element of F₁()
{ b₂ where b₁ is Element of F₁() : ( P₁[b₂] or P₂[b₂] ) } is set
q is Element of F₁()
{ b₂ where b₁ is Element of F₁() : ( P₁[b₂] or P₂[b₂] ) } is set
{ b₂ where b₁ is Element of F₁() : ( P₁[b₂] or P₂[b₂] ) } is set
K10( the carrier of (TOP-REAL 2)) is non empty set
p is TopSpace-like TopStruct
the carrier of p is set
K10( the carrier of p) is non empty set
p is TopSpace-like TopStruct
the carrier of p is set
K10( the carrier of p) is non empty set
A is Element of K10( the carrier of p)
x is Element of the carrier of p
r is Element of the carrier of p
p | A is strict TopSpace-like SubSpace of p
the carrier of (p | A) is set
K11( the carrier of I[01], the carrier of (p | A)) is set
K10(K11( the carrier of I[01], the carrier of (p | A))) is non empty set
q is Relation-like the carrier of I[01] -defined the carrier of (p | A) -valued Function-like V33( the carrier of I[01], the carrier of (p | A)) Element of K10(K11( the carrier of I[01], the carrier of (p | A)))
q . 0 is set
q . 1 is set
dom q is set
[#] I[01] is non empty non proper closed V154() V155() V156() Element of K10( the carrier of I[01])
K10( the carrier of I[01]) is non empty set
rng q is set
[#] (p | A) is non proper closed Element of K10( the carrier of (p | A))
K10( the carrier of (p | A)) is non empty set
p is TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of p is set
K10( the carrier of p) is non empty set
A is Element of K10( the carrier of p)
x is Element of K10( the carrier of p)
A /\ x is Element of K10( the carrier of p)
A \/ x is Element of K10( the carrier of p)
r is Element of the carrier of p
q is Element of the carrier of p
NE is Element of the carrier of p
{q} is non empty set
p | x is strict TopSpace-like SubSpace of p
the carrier of (p | x) is set
K11( the carrier of I[01], the carrier of (p | x)) is set
K10(K11( the carrier of I[01], the carrier of (p | x))) is non empty set
f is Relation-like the carrier of I[01] -defined the carrier of (p | x) -valued Function-like V33( the carrier of I[01], the carrier of (p | x)) Element of K10(K11( the carrier of I[01], the carrier of (p | x)))
f . 0 is set
f . 1 is set
p | A is strict TopSpace-like SubSpace of p
the carrier of (p | A) is set
K11( the carrier of I[01], the carrier of (p | A)) is set
K10(K11( the carrier of I[01], the carrier of (p | A))) is non empty set
f is Relation-like the carrier of I[01] -defined the carrier of (p | A) -valued Function-like V33( the carrier of I[01], the carrier of (p | A)) Element of K10(K11( the carrier of I[01], the carrier of (p | A)))
f . 0 is set
f . 1 is set
p | (A \/ x) is strict TopSpace-like SubSpace of p
the carrier of (p | (A \/ x)) is set
K11( the carrier of I[01], the carrier of (p | (A \/ x))) is set
K10(K11( the carrier of I[01], the carrier of (p | (A \/ x)))) is non empty set
c₉ is Relation-like the carrier of I[01] -defined the carrier of (p | (A \/ x)) -valued Function-like V33( the carrier of I[01], the carrier of (p | (A \/ x))) Element of K10(K11( the carrier of I[01], the carrier of (p | (A \/ x))))
c₉ . 0 is set
c₉ . 1 is set
|[0,1]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
LSeg (|[0,0]|,|[0,1]|) is non empty V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[0,0]|) + (b₁ * |[0,1]|)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
|[1,1]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
LSeg (|[0,1]|,|[1,1]|) is non empty V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[0,1]|) + (b₁ * |[1,1]|)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) is non empty Element of K10( the carrier of (TOP-REAL 2))
|[1,0]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
LSeg (|[1,1]|,|[1,0]|) is non empty V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[1,1]|) + (b₁ * |[1,0]|)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (|[1,0]|,|[0,0]|) is non empty V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[1,0]|) + (b₁ * |[0,0]|)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)) is non empty Element of K10( the carrier of (TOP-REAL 2))
((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))) is non empty Element of K10( the carrier of (TOP-REAL 2))
() is Element of K10( the carrier of (TOP-REAL 2))
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty set
A is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
LSeg (x,r) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
K10( the carrier of (TOP-REAL p)) is non empty set
{ (((1 - b₁) * x) + (b₁ * r)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (x,A) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * x) + (b₁ * A)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
q is V14() real ext-real Element of REAL
1 - q is V14() real ext-real Element of REAL
(1 - q) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
q * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - q) * x) + (q * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
NE is set
f is V14() real ext-real Element of REAL
1 - f is V14() real ext-real Element of REAL
(1 - f) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * A is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * x) + (f * A) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * ((1 - q) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * (q * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(f * ((1 - q) * x)) + (f * (q * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * x) + ((f * ((1 - q) * x)) + (f * (q * r))) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * x) + (f * ((1 - q) * x)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * x) + (f * ((1 - q) * x))) + (f * (q * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * (1 - q) is V14() real ext-real Element of REAL
(f * (1 - q)) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * x) + ((f * (1 - q)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * x) + ((f * (1 - q)) * x)) + (f * (q * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - f) + (f * (1 - q)) is V14() real ext-real Element of REAL
((1 - f) + (f * (1 - q))) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) + (f * (1 - q))) * x) + (f * (q * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * q is V14() real ext-real Element of REAL
1 - (f * q) is V14() real ext-real Element of REAL
(1 - (f * q)) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(f * q) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - (f * q)) * x) + ((f * q) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
p is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
p `1 is V14() real ext-real Element of REAL
A is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
A `1 is V14() real ext-real Element of REAL
LSeg (p,A) is non empty V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * p) + (b₁ * A)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
x is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
x `1 is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
1 - r is V14() real ext-real Element of REAL
(1 - r) * p is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
r * A is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
((1 - r) * p) + (r * A) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
((1 - r) * p) `1 is V14() real ext-real Element of REAL
(1 - r) * (p `1) is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
(1 - r) * (p `2) is V14() real ext-real Element of REAL
|[((1 - r) * (p `1)),((1 - r) * (p `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[((1 - r) * (p `1)),((1 - r) * (p `2))]| `1 is V14() real ext-real Element of REAL
(r * A) `1 is V14() real ext-real Element of REAL
r * (A `1) is V14() real ext-real Element of REAL
A `2 is V14() real ext-real Element of REAL
r * (A `2) is V14() real ext-real Element of REAL
|[(r * (A `1)),(r * (A `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[(r * (A `1)),(r * (A `2))]| `1 is V14() real ext-real Element of REAL
(((1 - r) * p) `1) + ((r * A) `1) is V14() real ext-real Element of REAL
((1 - r) * p) `2 is V14() real ext-real Element of REAL
(r * A) `2 is V14() real ext-real Element of REAL
(((1 - r) * p) `2) + ((r * A) `2) is V14() real ext-real Element of REAL
|[((((1 - r) * p) `1) + ((r * A) `1)),((((1 - r) * p) `2) + ((r * A) `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[((((1 - r) * p) `1) + ((r * A) `1)),((((1 - r) * p) `2) + ((r * A) `2))]| `1 is V14() real ext-real Element of REAL
((1 - r) * (p `1)) + (r * (A `1)) is V14() real ext-real Element of REAL
r * (p `1) is V14() real ext-real Element of REAL
((1 - r) * (p `1)) + (r * (p `1)) is V14() real ext-real Element of REAL
(1 - r) * (A `1) is V14() real ext-real Element of REAL
((1 - r) * (A `1)) + (r * (A `1)) is V14() real ext-real Element of REAL
p is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
p `2 is V14() real ext-real Element of REAL
A is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
A `2 is V14() real ext-real Element of REAL
LSeg (p,A) is non empty V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * p) + (b₁ * A)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
x is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
x `2 is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
1 - r is V14() real ext-real Element of REAL
(1 - r) * p is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
r * A is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
((1 - r) * p) + (r * A) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
((1 - r) * p) `2 is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
(1 - r) * (p `1) is V14() real ext-real Element of REAL
(1 - r) * (p `2) is V14() real ext-real Element of REAL
|[((1 - r) * (p `1)),((1 - r) * (p `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[((1 - r) * (p `1)),((1 - r) * (p `2))]| `2 is V14() real ext-real Element of REAL
(r * A) `2 is V14() real ext-real Element of REAL
A `1 is V14() real ext-real Element of REAL
r * (A `1) is V14() real ext-real Element of REAL
r * (A `2) is V14() real ext-real Element of REAL
|[(r * (A `1)),(r * (A `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[(r * (A `1)),(r * (A `2))]| `2 is V14() real ext-real Element of REAL
((1 - r) * p) `1 is V14() real ext-real Element of REAL
(r * A) `1 is V14() real ext-real Element of REAL
(((1 - r) * p) `1) + ((r * A) `1) is V14() real ext-real Element of REAL
(((1 - r) * p) `2) + ((r * A) `2) is V14() real ext-real Element of REAL
|[((((1 - r) * p) `1) + ((r * A) `1)),((((1 - r) * p) `2) + ((r * A) `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[((((1 - r) * p) `1) + ((r * A) `1)),((((1 - r) * p) `2) + ((r * A) `2))]| `2 is V14() real ext-real Element of REAL
((1 - r) * (p `2)) + (r * (A `2)) is V14() real ext-real Element of REAL
r * (p `2) is V14() real ext-real Element of REAL
((1 - r) * (p `2)) + (r * (p `2)) is V14() real ext-real Element of REAL
(1 - r) * (A `2) is V14() real ext-real Element of REAL
((1 - r) * (A `2)) + (r * (A `2)) is V14() real ext-real Element of REAL
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty set
A is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
LSeg (x,r) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
K10( the carrier of (TOP-REAL p)) is non empty set
{ (((1 - b₁) * x) + (b₁ * r)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (x,A) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * x) + (b₁ * A)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (A,r) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * A) + (b₁ * r)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (x,A)) \/ (LSeg (A,r)) is non empty Element of K10( the carrier of (TOP-REAL p))
q is V14() real ext-real Element of REAL
1 - q is V14() real ext-real Element of REAL
(1 - q) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
q * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - q) * x) + (q * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
NE is set
f is V14() real ext-real Element of REAL
1 - f is V14() real ext-real Element of REAL
(1 - f) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * x) + (f * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
1 / q is V14() real ext-real Element of REAL
f * (1 / q) is V14() real ext-real Element of REAL
q * (1 / q) is V14() real ext-real Element of REAL
1 - (f * (1 / q)) is V14() real ext-real Element of REAL
(1 - (f * (1 / q))) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(f * (1 / q)) * A is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - (f * (1 / q))) * x) + ((f * (1 / q)) * A) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(f * (1 / q)) * ((1 - q) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(f * (1 / q)) * (q * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((f * (1 / q)) * ((1 - q) * x)) + ((f * (1 / q)) * (q * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - (f * (1 / q))) * x) + (((f * (1 / q)) * ((1 - q) * x)) + ((f * (1 / q)) * (q * r))) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - (f * (1 / q))) * x) + ((f * (1 / q)) * ((1 - q) * x)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - (f * (1 / q))) * x) + ((f * (1 / q)) * ((1 - q) * x))) + ((f * (1 / q)) * (q * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(f * (1 / q)) * (1 - q) is V14() real ext-real Element of REAL
((f * (1 / q)) * (1 - q)) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - (f * (1 / q))) * x) + (((f * (1 / q)) * (1 - q)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - (f * (1 / q))) * x) + (((f * (1 / q)) * (1 - q)) * x)) + ((f * (1 / q)) * (q * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(f * (1 / q)) * q is V14() real ext-real Element of REAL
((f * (1 / q)) * q) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - (f * (1 / q))) * x) + (((f * (1 / q)) * (1 - q)) * x)) + (((f * (1 / q)) * q) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - (f * (1 / q))) + ((f * (1 / q)) * (1 - q)) is V14() real ext-real Element of REAL
((1 - (f * (1 / q))) + ((f * (1 / q)) * (1 - q))) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - (f * (1 / q))) + ((f * (1 / q)) * (1 - q))) * x) + (((f * (1 / q)) * q) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
1 - ((f * (1 / q)) * q) is V14() real ext-real Element of REAL
(1 - ((f * (1 / q)) * q)) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - ((f * (1 / q)) * q)) * x) + (f * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
1 / (1 - q) is V14() real ext-real Element of REAL
(1 - f) * (1 / (1 - q)) is V14() real ext-real Element of REAL
q - q is V14() real ext-real Element of REAL
(1 - q) * (1 / (1 - q)) is V14() real ext-real Element of REAL
1 - 0 is non empty V14() real ext-real positive non negative Element of REAL
1 - ((1 - f) * (1 / (1 - q))) is V14() real ext-real Element of REAL
(1 - ((1 - f) * (1 / (1 - q)))) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * (1 / (1 - q))) * A is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - ((1 - f) * (1 / (1 - q)))) * r) + (((1 - f) * (1 / (1 - q))) * A) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
1 - (1 - q) is V14() real ext-real Element of REAL
(1 - (1 - q)) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * (1 / (1 - q))) * ((1 - (1 - q)) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * (1 / (1 - q))) * ((1 - q) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * (1 / (1 - q))) * ((1 - (1 - q)) * r)) + (((1 - f) * (1 / (1 - q))) * ((1 - q) * x)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - ((1 - f) * (1 / (1 - q)))) * r) + ((((1 - f) * (1 / (1 - q))) * ((1 - (1 - q)) * r)) + (((1 - f) * (1 / (1 - q))) * ((1 - q) * x))) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - ((1 - f) * (1 / (1 - q)))) * r) + (((1 - f) * (1 / (1 - q))) * ((1 - (1 - q)) * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - ((1 - f) * (1 / (1 - q)))) * r) + (((1 - f) * (1 / (1 - q))) * ((1 - (1 - q)) * r))) + (((1 - f) * (1 / (1 - q))) * ((1 - q) * x)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * (1 / (1 - q))) * (1 - (1 - q)) is V14() real ext-real Element of REAL
(((1 - f) * (1 / (1 - q))) * (1 - (1 - q))) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - ((1 - f) * (1 / (1 - q)))) * r) + ((((1 - f) * (1 / (1 - q))) * (1 - (1 - q))) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - ((1 - f) * (1 / (1 - q)))) * r) + ((((1 - f) * (1 / (1 - q))) * (1 - (1 - q))) * r)) + (((1 - f) * (1 / (1 - q))) * ((1 - q) * x)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * (1 / (1 - q))) * (1 - q) is V14() real ext-real Element of REAL
(((1 - f) * (1 / (1 - q))) * (1 - q)) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - ((1 - f) * (1 / (1 - q)))) * r) + ((((1 - f) * (1 / (1 - q))) * (1 - (1 - q))) * r)) + ((((1 - f) * (1 / (1 - q))) * (1 - q)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - ((1 - f) * (1 / (1 - q)))) + (((1 - f) * (1 / (1 - q))) * (1 - (1 - q))) is V14() real ext-real Element of REAL
((1 - ((1 - f) * (1 / (1 - q)))) + (((1 - f) * (1 / (1 - q))) * (1 - (1 - q)))) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - ((1 - f) * (1 / (1 - q)))) + (((1 - f) * (1 / (1 - q))) * (1 - (1 - q)))) * r) + ((((1 - f) * (1 / (1 - q))) * (1 - q)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
1 - (((1 - f) * (1 / (1 - q))) * (1 - q)) is V14() real ext-real Element of REAL
(1 - (((1 - f) * (1 / (1 - q))) * (1 - q))) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - (((1 - f) * (1 / (1 - q))) * (1 - q))) * r) + ((1 - f) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
1 - (1 - f) is V14() real ext-real Element of REAL
(1 - (1 - f)) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - (1 - f)) * r) + ((1 - f) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
{ (((1 - b₁) * r) + (b₁ * A)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
1 * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
0. (TOP-REAL p) is V45(p) FinSequence-like V61( TOP-REAL p) V146() Element of the carrier of (TOP-REAL p)
the ZeroF of (TOP-REAL p) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 * x) + (0. (TOP-REAL p)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
x + (0. (TOP-REAL p)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
{A} is non empty set
0. (TOP-REAL p) is V45(p) FinSequence-like V61( TOP-REAL p) V146() Element of the carrier of (TOP-REAL p)
the ZeroF of (TOP-REAL p) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
1 * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(0. (TOP-REAL p)) + (1 * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(0. (TOP-REAL p)) + r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
{A} is non empty set
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty set
r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
A is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
LSeg (A,x) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
K10( the carrier of (TOP-REAL p)) is non empty set
{ (((1 - b₁) * A) + (b₁ * x)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
q is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
LSeg (r,q) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * r) + (b₁ * q)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (A,r) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * A) + (b₁ * r)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (r,x) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * r) + (b₁ * x)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (A,r)) \/ (LSeg (r,x)) is non empty Element of K10( the carrier of (TOP-REAL p))
LSeg (q,r) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * q) + (b₁ * r)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty set
A is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
q is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
LSeg (r,q) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
K10( the carrier of (TOP-REAL p)) is non empty set
{ (((1 - b₁) * r) + (b₁ * q)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
LSeg (r,A) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * r) + (b₁ * A)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (A,x) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * A) + (b₁ * x)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (r,A)) \/ (LSeg (A,x)) is non empty Element of K10( the carrier of (TOP-REAL p))
LSeg (x,q) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * x) + (b₁ * q)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
((LSeg (r,A)) \/ (LSeg (A,x))) \/ (LSeg (x,q)) is non empty Element of K10( the carrier of (TOP-REAL p))
LSeg (r,x) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * r) + (b₁ * x)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (r,x)) \/ (LSeg (x,q)) is non empty Element of K10( the carrier of (TOP-REAL p))
LSeg (x,A) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * x) + (b₁ * A)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (A,q) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * A) + (b₁ * q)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (x,A)) \/ (LSeg (A,q)) is non empty Element of K10( the carrier of (TOP-REAL p))
(LSeg (r,A)) \/ (LSeg (A,q)) is non empty Element of K10( the carrier of (TOP-REAL p))
(LSeg (r,A)) \/ (LSeg (x,q)) is non empty Element of K10( the carrier of (TOP-REAL p))
((LSeg (r,A)) \/ (LSeg (x,q))) \/ (LSeg (A,x)) is non empty Element of K10( the carrier of (TOP-REAL p))
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty set
A is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
LSeg (x,r) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
K10( the carrier of (TOP-REAL p)) is non empty set
{ (((1 - b₁) * x) + (b₁ * r)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (x,A) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * x) + (b₁ * A)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (A,r) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * A) + (b₁ * r)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (x,A)) /\ (LSeg (A,r)) is Element of K10( the carrier of (TOP-REAL p))
{A} is non empty set
q is set
NE is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f is V14() real ext-real Element of REAL
1 - f is V14() real ext-real Element of REAL
(1 - f) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * A is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * x) + (f * A) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f is V14() real ext-real Element of REAL
1 - f is V14() real ext-real Element of REAL
(1 - f) * A is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * A) + (f * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
c₉ is V14() real ext-real Element of REAL
1 - c₉ is V14() real ext-real Element of REAL
(1 - c₉) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
c₉ * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - c₉) * x) + (c₉ * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
1 - 1 is V14() real ext-real Element of REAL
(1 - 1) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - 1) * x) + A is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
0. (TOP-REAL p) is V45(p) FinSequence-like V61( TOP-REAL p) V146() Element of the carrier of (TOP-REAL p)
the ZeroF of (TOP-REAL p) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(0. (TOP-REAL p)) + A is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
1 - 0 is non empty V14() real ext-real positive non negative Element of REAL
(1 - 0) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - 0) * x) + (0. (TOP-REAL p)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - f) * c₉ is V14() real ext-real Element of REAL
(1 - f) * c₉ is V14() real ext-real Element of REAL
((1 - f) * c₉) + f is V14() real ext-real Element of REAL
(1 - f) * ((1 - c₉) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - f) * (c₉ * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * ((1 - c₉) * x)) + ((1 - f) * (c₉ * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * ((1 - c₉) * x)) + ((1 - f) * (c₉ * r))) + (f * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - f) * (1 - c₉) is V14() real ext-real Element of REAL
((1 - f) * (1 - c₉)) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * (1 - c₉)) * x) + ((1 - f) * (c₉ * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - f) * (1 - c₉)) * x) + ((1 - f) * (c₉ * r))) + (f * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * c₉) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * (1 - c₉)) * x) + (((1 - f) * c₉) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - f) * (1 - c₉)) * x) + (((1 - f) * c₉) * r)) + (f * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * c₉) * r) + (f * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * (1 - c₉)) * x) + ((((1 - f) * c₉) * r) + (f * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * c₉) + f) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * (1 - c₉)) * x) + ((((1 - f) * c₉) + f) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
A - NE is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
1 - (((1 - f) * c₉) + f) is V14() real ext-real Element of REAL
(1 - (((1 - f) * c₉) + f)) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - c₉) * x) + (c₉ * r)) - ((1 - (((1 - f) * c₉) + f)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - c₉) * x) + (c₉ * r)) - ((1 - (((1 - f) * c₉) + f)) * x)) - ((((1 - f) * c₉) + f) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - c₉) * x) - ((1 - (((1 - f) * c₉) + f)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - c₉) * x) - ((1 - (((1 - f) * c₉) + f)) * x)) + (c₉ * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - c₉) * x) - ((1 - (((1 - f) * c₉) + f)) * x)) + (c₉ * r)) - ((((1 - f) * c₉) + f) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - c₉) - (1 - (((1 - f) * c₉) + f)) is V14() real ext-real Element of REAL
((1 - c₉) - (1 - (((1 - f) * c₉) + f))) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - c₉) - (1 - (((1 - f) * c₉) + f))) * x) + (c₉ * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - c₉) - (1 - (((1 - f) * c₉) + f))) * x) + (c₉ * r)) - ((((1 - f) * c₉) + f) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * c₉) + f) - c₉ is V14() real ext-real Element of REAL
((((1 - f) * c₉) + f) - c₉) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((((1 - f) * c₉) + f) - c₉) * x) - ((((1 - f) * c₉) + f) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((((1 - f) * c₉) + f) - c₉) * x) - ((((1 - f) * c₉) + f) * r)) + (c₉ * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - f) * c₉) + f) * r) - (c₉ * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((((1 - f) * c₉) + f) - c₉) * x) - (((((1 - f) * c₉) + f) * r) - (c₉ * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - f) * c₉) + f) - c₉) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((((1 - f) * c₉) + f) - c₉) * x) - (((((1 - f) * c₉) + f) - c₉) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
x - r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - f) * c₉) + f) - c₉) * (x - r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * ((1 - c₉) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * (c₉ * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(f * ((1 - c₉) * x)) + (f * (c₉ * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * x) + ((f * ((1 - c₉) * x)) + (f * (c₉ * r))) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * x) + (f * ((1 - c₉) * x)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * x) + (f * ((1 - c₉) * x))) + (f * (c₉ * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * (1 - c₉) is V14() real ext-real Element of REAL
(f * (1 - c₉)) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * x) + ((f * (1 - c₉)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * x) + ((f * (1 - c₉)) * x)) + (f * (c₉ * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - f) + (f * (1 - c₉)) is V14() real ext-real Element of REAL
((1 - f) + (f * (1 - c₉))) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) + (f * (1 - c₉))) * x) + (f * (c₉ * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * c₉ is V14() real ext-real Element of REAL
1 - (f * c₉) is V14() real ext-real Element of REAL
(1 - (f * c₉)) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(f * c₉) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - (f * c₉)) * x) + ((f * c₉) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - c₉) * x) + (c₉ * r)) - ((1 - (f * c₉)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - c₉) * x) + (c₉ * r)) - ((1 - (f * c₉)) * x)) - ((f * c₉) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - c₉) * x) - ((1 - (f * c₉)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - c₉) * x) - ((1 - (f * c₉)) * x)) + (c₉ * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - c₉) * x) - ((1 - (f * c₉)) * x)) + (c₉ * r)) - ((f * c₉) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - c₉) - (1 - (f * c₉)) is V14() real ext-real Element of REAL
((1 - c₉) - (1 - (f * c₉))) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - c₉) - (1 - (f * c₉))) * x) + (c₉ * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - c₉) - (1 - (f * c₉))) * x) + (c₉ * r)) - ((f * c₉) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(f * c₉) - c₉ is V14() real ext-real Element of REAL
((f * c₉) - c₉) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((f * c₉) - c₉) * x) - ((f * c₉) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((f * c₉) - c₉) * x) - ((f * c₉) * r)) + (c₉ * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((f * c₉) * r) - (c₉ * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((f * c₉) - c₉) * x) - (((f * c₉) * r) - (c₉ * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((f * c₉) - c₉) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((f * c₉) - c₉) * x) - (((f * c₉) - c₉) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((f * c₉) - c₉) * (x - r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((((1 - f) * c₉) + f) - c₉) * (x - r)) - (((f * c₉) - c₉) * (x - r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - f) * c₉) + f) - c₉) - ((f * c₉) - c₉) is V14() real ext-real Element of REAL
(((((1 - f) * c₉) + f) - c₉) - ((f * c₉) - c₉)) * (x - r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * c₉) + f) - (f * c₉) is V14() real ext-real Element of REAL
f * (1 - c₉) is V14() real ext-real Element of REAL
((1 - f) * c₉) + (f * (1 - c₉)) is V14() real ext-real Element of REAL
{x} is non empty set
p is TopSpace-like TopStruct
the carrier of p is set
the topology of p is non empty Element of K10(K10( the carrier of p))
K10( the carrier of p) is non empty set
K10(K10( the carrier of p)) is non empty set
TopStruct(# the carrier of p, the topology of p #) is strict TopSpace-like TopStruct
the carrier of TopStruct(# the carrier of p, the topology of p #) is set
A is Element of the carrier of TopStruct(# the carrier of p, the topology of p #)
x is Element of the carrier of TopStruct(# the carrier of p, the topology of p #)
K10( the carrier of TopStruct(# the carrier of p, the topology of p #)) is non empty set
r is Element of the carrier of p
q is Element of the carrier of p
NE is Element of K10( the carrier of p)
f is Element of K10( the carrier of p)
f is Element of K10( the carrier of TopStruct(# the carrier of p, the topology of p #))
c₉ is Element of K10( the carrier of TopStruct(# the carrier of p, the topology of p #))
A is Element of the carrier of p
x is Element of the carrier of p
the carrier of TopStruct(# the carrier of p, the topology of p #) is set
K10( the carrier of TopStruct(# the carrier of p, the topology of p #)) is non empty set
r is Element of the carrier of TopStruct(# the carrier of p, the topology of p #)
q is Element of the carrier of TopStruct(# the carrier of p, the topology of p #)
NE is Element of K10( the carrier of TopStruct(# the carrier of p, the topology of p #))
f is Element of K10( the carrier of TopStruct(# the carrier of p, the topology of p #))
f is Element of K10( the carrier of p)
c₉ is Element of K10( the carrier of p)
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty set
A is set
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty functional set
A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
LSeg (A,x) is non empty functional V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
K10( the carrier of (TOP-REAL p)) is non empty set
{ (((1 - b₁) * A) + (b₁ * x)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
Euclid p is non empty strict Reflexive discerning V103() triangle Discerning MetrStruct
REAL p is non empty functional FinSequence-membered M13( REAL )
K360(p,REAL) is functional FinSequence-membered M13( REAL )
Pitag_dist p is Relation-like K11((REAL p),(REAL p)) -defined REAL -valued Function-like V33(K11((REAL p),(REAL p)), REAL ) V144() V145() V146() Element of K10(K11(K11((REAL p),(REAL p)),REAL))
K11((REAL p),(REAL p)) is non empty set
K11(K11((REAL p),(REAL p)),REAL) is V144() V145() V146() set
K10(K11(K11((REAL p),(REAL p)),REAL)) is non empty set
MetrStruct(# (REAL p),(Pitag_dist p) #) is strict MetrStruct
the carrier of (Euclid p) is non empty set
K10( the carrier of (Euclid p)) is non empty set
q is Element of K10( the carrier of (Euclid p))
[#] I[01] is non empty non proper closed V154() V155() V156() Element of K10( the carrier of I[01])
K10( the carrier of I[01]) is non empty set
c₉ is set
f1 is V14() real ext-real Element of REAL
1 - f1 is V14() real ext-real Element of REAL
(1 - f1) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
f1 * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - f1) * A) + (f1 * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
f is V14() real ext-real Element of REAL
1 - f is V14() real ext-real Element of REAL
(1 - f) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
f * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - f) * A) + (f * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
c₉ is Relation-like Function-like set
dom c₉ is set
rng c₉ is set
(TOP-REAL p) | (LSeg (A,x)) is non empty strict TopSpace-like SubSpace of TOP-REAL p
the carrier of ((TOP-REAL p) | (LSeg (A,x))) is non empty set
f1 is set
f is set
c₉ . f is set
{ b₁ where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
hh is V14() real ext-real Element of REAL
1 - hh is V14() real ext-real Element of REAL
(1 - hh) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
hh * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - hh) * A) + (hh * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
[#] ((TOP-REAL p) | (LSeg (A,x))) is non empty non proper closed Element of K10( the carrier of ((TOP-REAL p) | (LSeg (A,x))))
K10( the carrier of ((TOP-REAL p) | (LSeg (A,x)))) is non empty set
K11( the carrier of I[01], the carrier of ((TOP-REAL p) | (LSeg (A,x)))) is non empty set
K10(K11( the carrier of I[01], the carrier of ((TOP-REAL p) | (LSeg (A,x))))) is non empty set
f is set
f1 is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL p) | (LSeg (A,x))) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL p) | (LSeg (A,x)))) Element of K10(K11( the carrier of I[01], the carrier of ((TOP-REAL p) | (LSeg (A,x)))))
dom f1 is set
hh is set
f1 . f is set
f1 . hh is set
{ b₁ where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
c₁₃ is V14() real ext-real Element of REAL
1 - c₁₃ is V14() real ext-real Element of REAL
(1 - c₁₃) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
c₁₃ * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - c₁₃) * A) + (c₁₃ * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
p29 is V14() real ext-real Element of REAL
1 - p29 is V14() real ext-real Element of REAL
(1 - p29) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
p29 * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - p29) * A) + (p29 * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
- p29 is V14() real ext-real Element of REAL
(- p29) * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(((1 - p29) * A) + (p29 * x)) + ((- p29) * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(c₁₃ * x) + ((- p29) * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - c₁₃) * A) + ((c₁₃ * x) + ((- p29) * x)) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
c₁₃ + (- p29) is V14() real ext-real Element of REAL
(c₁₃ + (- p29)) * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - c₁₃) * A) + ((c₁₃ + (- p29)) * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(p29 * x) + ((- p29) * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - p29) * A) + ((p29 * x) + ((- p29) * x)) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
c₁₃ - p29 is V14() real ext-real Element of REAL
(c₁₃ - p29) * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - c₁₃) * A) + ((c₁₃ - p29) * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
p29 + (- p29) is V14() real ext-real Element of REAL
(p29 + (- p29)) * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - p29) * A) + ((p29 + (- p29)) * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
0. (TOP-REAL p) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V61( TOP-REAL p) V144() V145() V146() Element of the carrier of (TOP-REAL p)
the ZeroF of (TOP-REAL p) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - p29) * A) + (0. (TOP-REAL p)) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
- (1 - c₁₃) is V14() real ext-real Element of REAL
(- (1 - c₁₃)) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((- (1 - c₁₃)) * A) + ((1 - p29) * A) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((- (1 - c₁₃)) * A) + (((1 - c₁₃) * A) + ((c₁₃ - p29) * x)) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((- (1 - c₁₃)) * A) + ((1 - c₁₃) * A) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(((- (1 - c₁₃)) * A) + ((1 - c₁₃) * A)) + ((c₁₃ - p29) * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(- (1 - c₁₃)) + (1 - c₁₃) is V14() real ext-real Element of REAL
((- (1 - c₁₃)) + (1 - c₁₃)) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(((- (1 - c₁₃)) + (1 - c₁₃)) * A) + ((c₁₃ - p29) * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(0. (TOP-REAL p)) + ((c₁₃ - p29) * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
c₁₃ - 1 is V14() real ext-real Element of REAL
(c₁₃ - 1) + (1 - p29) is V14() real ext-real Element of REAL
((c₁₃ - 1) + (1 - p29)) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
[#] ((TOP-REAL p) | (LSeg (A,x))) is non empty non proper closed Element of K10( the carrier of ((TOP-REAL p) | (LSeg (A,x))))
K10( the carrier of ((TOP-REAL p) | (LSeg (A,x)))) is non empty set
rng f1 is set
f is set
hh is V14() real ext-real Element of REAL
1 - hh is V14() real ext-real Element of REAL
(1 - hh) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
hh * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - hh) * A) + (hh * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
f1 . hh is set
TopSpaceMetr (Euclid p) is non empty strict TopSpace-like TopStruct
NE is non empty Element of K10( the carrier of (Euclid p))
(Euclid p) | NE is non empty strict Reflexive discerning V103() triangle Discerning SubSpace of Euclid p
TopSpaceMetr ((Euclid p) | NE) is non empty strict TopSpace-like TopStruct
c₁₃ is V14() real ext-real Element of the carrier of I[01]
f1 . c₁₃ is Element of the carrier of ((TOP-REAL p) | (LSeg (A,x)))
p29 is a_neighborhood of f1 . c₁₃
Closed-Interval-MSpace (0,1) is non empty strict Reflexive discerning V103() triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (0,1)) is non empty set
f is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like Element of REAL p
f is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like Element of REAL p
(Pitag_dist p) . (f,f) is V14() real ext-real Element of REAL
f is Element of the carrier of (Euclid p)
hh is Element of the carrier of (Euclid p)
dist (f,hh) is V14() real ext-real Element of REAL
the carrier of ((Euclid p) | NE) is non empty set
i is Element of the carrier of ((Euclid p) | NE)
Int p29 is Element of K10( the carrier of ((TOP-REAL p) | (LSeg (A,x))))
Q is Element of K10( the carrier of ((TOP-REAL p) | (LSeg (A,x))))
r is V14() real ext-real set
Ball (i,r) is Element of K10( the carrier of ((Euclid p) | NE))
K10( the carrier of ((Euclid p) | NE)) is non empty set
r is V14() real ext-real Element of REAL
r / ((Pitag_dist p) . (f,f)) is V14() real ext-real Element of REAL
X is Element of the carrier of (Closed-Interval-MSpace (0,1))
Ball (X,(r / ((Pitag_dist p) . (f,f)))) is Element of K10( the carrier of (Closed-Interval-MSpace (0,1)))
K10( the carrier of (Closed-Interval-MSpace (0,1))) is non empty set
TopSpaceMetr (Closed-Interval-MSpace (0,1)) is non empty strict TopSpace-like TopStruct
H is V154() V155() V156() Element of K10( the carrier of I[01])
Int H is V154() V155() V156() Element of K10( the carrier of I[01])
H is V154() V155() V156() a_neighborhood of c₁₃
f1 .: H is set
Ball (i,r) is Element of K10( the carrier of ((Euclid p) | NE))
p29 is Element of the carrier of (Euclid p)
a is set
u is set
f1 . u is set
u9 is Element of the carrier of (Closed-Interval-MSpace (0,1))
dist (X,u9) is V14() real ext-real Element of REAL
the distance of (Closed-Interval-MSpace (0,1)) is Relation-like K11( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Closed-Interval-MSpace (0,1))) -defined REAL -valued Function-like V33(K11( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Closed-Interval-MSpace (0,1))), REAL ) V144() V145() V146() Element of K10(K11(K11( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Closed-Interval-MSpace (0,1))),REAL))
K11( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Closed-Interval-MSpace (0,1))) is non empty set
K11(K11( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Closed-Interval-MSpace (0,1))),REAL) is V144() V145() V146() set
K10(K11(K11( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Closed-Interval-MSpace (0,1))),REAL)) is non empty set
the distance of (Closed-Interval-MSpace (0,1)) . (X,u9) is V14() real ext-real Element of REAL
the distance of RealSpace is Relation-like K11( the carrier of RealSpace, the carrier of RealSpace) -defined REAL -valued Function-like V33(K11( the carrier of RealSpace, the carrier of RealSpace), REAL ) V144() V145() V146() Element of K10(K11(K11( the carrier of RealSpace, the carrier of RealSpace),REAL))
K11( the carrier of RealSpace, the carrier of RealSpace) is non empty V144() V145() V146() set
K11(K11( the carrier of RealSpace, the carrier of RealSpace),REAL) is V144() V145() V146() set
K10(K11(K11( the carrier of RealSpace, the carrier of RealSpace),REAL)) is non empty set
W99 is V14() real ext-real Element of the carrier of RealSpace
u99 is V14() real ext-real Element of the carrier of RealSpace
the distance of RealSpace . (W99,u99) is V14() real ext-real Element of REAL
dist (W99,u99) is V14() real ext-real Element of REAL
p19 is V14() real ext-real Element of REAL
u1 is V14() real ext-real Element of REAL
p19 - u1 is V14() real ext-real Element of REAL
abs (p19 - u1) is V14() real ext-real Element of REAL
u1 - p19 is V14() real ext-real Element of REAL
- (u1 - p19) is V14() real ext-real Element of REAL
abs (- (u1 - p19)) is V14() real ext-real Element of REAL
abs (u1 - p19) is V14() real ext-real Element of REAL
r / (r / ((Pitag_dist p) . (f,f))) is V14() real ext-real Element of REAL
f - f is Relation-like NAT -defined REAL -valued Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() M14( REAL , REAL p)
|.(f - f).| is V14() real ext-real non negative Element of REAL
aa is Element of the carrier of ((Euclid p) | NE)
aa9 is Element of the carrier of (Euclid p)
A - x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
WW1 is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like Element of REAL p
1 - p19 is V14() real ext-real Element of REAL
(1 - p19) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
p19 * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - p19) * A) + (p19 * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
aa1 is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like Element of REAL p
1 - u1 is V14() real ext-real Element of REAL
(1 - u1) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
u1 * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - u1) * A) + (u1 * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
WW1 - aa1 is Relation-like NAT -defined REAL -valued Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() M14( REAL , REAL p)
(((1 - p19) * A) + (p19 * x)) - (((1 - u1) * A) + (u1 * x)) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(p19 * x) + ((1 - p19) * A) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((p19 * x) + ((1 - p19) * A)) - ((1 - u1) * A) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(((p19 * x) + ((1 - p19) * A)) - ((1 - u1) * A)) - (u1 * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - p19) * A) - ((1 - u1) * A) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(p19 * x) + (((1 - p19) * A) - ((1 - u1) * A)) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((p19 * x) + (((1 - p19) * A) - ((1 - u1) * A))) - (u1 * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(1 - p19) - (1 - u1) is V14() real ext-real Element of REAL
((1 - p19) - (1 - u1)) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(p19 * x) + (((1 - p19) - (1 - u1)) * A) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((p19 * x) + (((1 - p19) - (1 - u1)) * A)) - (u1 * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(u1 - p19) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(p19 * x) - (u1 * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((u1 - p19) * A) + ((p19 * x) - (u1 * x)) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(p19 - u1) * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((u1 - p19) * A) + ((p19 - u1) * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(- (u1 - p19)) * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((u1 - p19) * A) + ((- (u1 - p19)) * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(u1 - p19) * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
- ((u1 - p19) * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((u1 - p19) * A) + (- ((u1 - p19) * x)) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((u1 - p19) * A) - ((u1 - p19) * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(u1 - p19) * (A - x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(u1 - p19) * (f - f) is Relation-like NAT -defined REAL -valued Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() M14( REAL , REAL p)
|.(WW1 - aa1).| is V14() real ext-real non negative Element of REAL
(abs (u1 - p19)) * |.(f - f).| is V14() real ext-real Element of REAL
(r / ((Pitag_dist p) . (f,f))) * (r / (r / ((Pitag_dist p) . (f,f)))) is V14() real ext-real Element of REAL
the distance of (Euclid p) is Relation-like K11( the carrier of (Euclid p), the carrier of (Euclid p)) -defined REAL -valued Function-like V33(K11( the carrier of (Euclid p), the carrier of (Euclid p)), REAL ) V144() V145() V146() Element of K10(K11(K11( the carrier of (Euclid p), the carrier of (Euclid p)),REAL))
K11( the carrier of (Euclid p), the carrier of (Euclid p)) is non empty set
K11(K11( the carrier of (Euclid p), the carrier of (Euclid p)),REAL) is V144() V145() V146() set
K10(K11(K11( the carrier of (Euclid p), the carrier of (Euclid p)),REAL)) is non empty set
the distance of (Euclid p) . (p29,aa9) is V14() real ext-real Element of REAL
the distance of ((Euclid p) | NE) is Relation-like K11( the carrier of ((Euclid p) | NE), the carrier of ((Euclid p) | NE)) -defined REAL -valued Function-like V33(K11( the carrier of ((Euclid p) | NE), the carrier of ((Euclid p) | NE)), REAL ) V144() V145() V146() Element of K10(K11(K11( the carrier of ((Euclid p) | NE), the carrier of ((Euclid p) | NE)),REAL))
K11( the carrier of ((Euclid p) | NE), the carrier of ((Euclid p) | NE)) is non empty set
K11(K11( the carrier of ((Euclid p) | NE), the carrier of ((Euclid p) | NE)),REAL) is V144() V145() V146() set
K10(K11(K11( the carrier of ((Euclid p) | NE), the carrier of ((Euclid p) | NE)),REAL)) is non empty set
the distance of ((Euclid p) | NE) . (i,aa) is V14() real ext-real Element of REAL
dist (i,aa) is V14() real ext-real Element of REAL
f1 . 0 is set
f1 . 1 is set
the topology of (TOP-REAL p) is non empty Element of K10(K10( the carrier of (TOP-REAL p)))
K10(K10( the carrier of (TOP-REAL p))) is non empty set
TopStruct(# the carrier of (TOP-REAL p), the topology of (TOP-REAL p) #) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid p)) is non empty set
K10( the carrier of (TopSpaceMetr (Euclid p))) is non empty set
f is Element of K10( the carrier of (TopSpaceMetr (Euclid p)))
(TopSpaceMetr (Euclid p)) | f is strict TopSpace-like SubSpace of TopSpaceMetr (Euclid p)
1 - 0 is non empty V14() real ext-real positive non negative Element of REAL
(1 - 0) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
0 * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - 0) * A) + (0 * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
A + (0 * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
A + (0. (TOP-REAL p)) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
1 - 1 is V14() real ext-real Element of REAL
(1 - 1) * A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
1 * x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
((1 - 1) * A) + (1 * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(0. (TOP-REAL p)) + (1 * x) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty functional set
the topology of (TOP-REAL p) is non empty Element of K10(K10( the carrier of (TOP-REAL p)))
K10( the carrier of (TOP-REAL p)) is non empty set
K10(K10( the carrier of (TOP-REAL p))) is non empty set
TopStruct(# the carrier of (TOP-REAL p), the topology of (TOP-REAL p) #) is non empty strict TopSpace-like TopStruct
Euclid p is non empty strict Reflexive discerning V103() triangle Discerning MetrStruct
REAL p is non empty functional FinSequence-membered M13( REAL )
K360(p,REAL) is functional FinSequence-membered M13( REAL )
Pitag_dist p is Relation-like K11((REAL p),(REAL p)) -defined REAL -valued Function-like V33(K11((REAL p),(REAL p)), REAL ) V144() V145() V146() Element of K10(K11(K11((REAL p),(REAL p)),REAL))
K11((REAL p),(REAL p)) is non empty set
K11(K11((REAL p),(REAL p)),REAL) is V144() V145() V146() set
K10(K11(K11((REAL p),(REAL p)),REAL)) is non empty set
MetrStruct(# (REAL p),(Pitag_dist p) #) is strict MetrStruct
TopSpaceMetr (Euclid p) is non empty strict TopSpace-like TopStruct
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like T_0 T_1 T_2 V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty functional set
K10( the carrier of (TOP-REAL p)) is non empty set
A is functional Element of K10( the carrier of (TOP-REAL p))
x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
r is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
q is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
LSeg (r,q) is non empty functional V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * r) + (b₁ * q)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
A /\ (LSeg (r,q)) is functional Element of K10( the carrier of (TOP-REAL p))
{r} is non empty functional set
A \/ (LSeg (r,q)) is non empty functional Element of K10( the carrier of (TOP-REAL p))
{q} is non empty functional set
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like T_0 T_1 T_2 V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty functional set
K10( the carrier of (TOP-REAL p)) is non empty set
A is functional Element of K10( the carrier of (TOP-REAL p))
r is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
q is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
LSeg (q,r) is non empty functional V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * q) + (b₁ * r)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (q,r)) /\ A is functional Element of K10( the carrier of (TOP-REAL p))
{r} is non empty functional set
(LSeg (q,r)) \/ A is non empty functional Element of K10( the carrier of (TOP-REAL p))
{q} is non empty functional set
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like T_0 T_1 T_2 V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty functional set
A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
r is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
LSeg (A,x) is non empty functional V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
K10( the carrier of (TOP-REAL p)) is non empty set
{ (((1 - b₁) * A) + (b₁ * x)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (x,r) is non empty functional V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * x) + (b₁ * r)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(LSeg (A,x)) /\ (LSeg (x,r)) is functional Element of K10( the carrier of (TOP-REAL p))
{x} is non empty functional set
(LSeg (A,x)) \/ (LSeg (x,r)) is non empty functional Element of K10( the carrier of (TOP-REAL p))
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = 0 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) } is set
{ b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 1 ) } is set
LSeg (|[0,0]|,|[1,0]|) is non empty V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * |[0,0]|) + (b₁ * |[1,0]|)) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 0 ) } is set
LSeg (|[1,0]|,|[1,1]|) is non empty V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b<sub>1</sub>) * |[1,0]|) + (b<sub>1</sub> * |[1,1]|)) where b<sub>1</sub> is V14() real ext-real Element of REAL : ( 0 <= b<sub>1</sub> & b<sub>1</sub> <= 1 ) } is set
{ b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 1 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } is set
|[0,1]| `2 is V14() real ext-real Element of REAL
|[0,1]| `1 is V14() real ext-real Element of REAL
c₉ is set
f1 is V14() real ext-real Element of REAL
1 - f1 is V14() real ext-real Element of REAL
(1 - f1) * |[0,0]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
f1 * |[0,1]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
((1 - f1) * |[0,0]|) + (f1 * |[0,1]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(0. (TOP-REAL 2)) + (f1 * |[0,1]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
f1 * (|[0,1]| `1) is V14() real ext-real Element of REAL
f1 * (|[0,1]| `2) is V14() real ext-real Element of REAL
|[(f1 * (|[0,1]| `1)),(f1 * (|[0,1]| `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[0,f1]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(((1 - f1) * |[0,0]|) + (f1 * |[0,1]|)) `2 is V14() real ext-real Element of REAL
(((1 - f1) * |[0,0]|) + (f1 * |[0,1]|)) `1 is V14() real ext-real Element of REAL
c₉ is set
f1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
f1 `1 is V14() real ext-real Element of REAL
f1 `2 is V14() real ext-real Element of REAL
1 - (f1 `2) is V14() real ext-real Element of REAL
(1 - (f1 `2)) * |[0,0]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(f1 `2) * |[0,1]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
((1 - (f1 `2)) * |[0,0]|) + ((f1 `2) * |[0,1]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(0. (TOP-REAL 2)) + ((f1 `2) * |[0,1]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(f1 `2) * (|[0,1]| `1) is V14() real ext-real Element of REAL
(f1 `2) * (|[0,1]| `2) is V14() real ext-real Element of REAL
|[((f1 `2) * (|[0,1]| `1)),((f1 `2) * (|[0,1]| `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[1,1]| `2 is V14() real ext-real Element of REAL
|[1,1]| `1 is V14() real ext-real Element of REAL
c₉ is set
f1 is V14() real ext-real Element of REAL
1 - f1 is V14() real ext-real Element of REAL
(1 - f1) * |[0,1]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
f1 * |[1,1]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
((1 - f1) * |[0,1]|) + (f1 * |[1,1]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(1 - f1) * 0 is V14() real ext-real Element of REAL
(1 - f1) * (|[0,1]| `2) is V14() real ext-real Element of REAL
|[((1 - f1) * 0),((1 - f1) * (|[0,1]| `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[((1 - f1) * 0),((1 - f1) * (|[0,1]| `2))]| + (f1 * |[1,1]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
|[0,(1 - f1)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
f1 * 1 is V14() real ext-real Element of REAL
|[f1,(f1 * 1)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[0,(1 - f1)]| + |[f1,(f1 * 1)]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
0 + f1 is V14() real ext-real Element of REAL
(1 - f1) + f1 is V14() real ext-real Element of REAL
|[(0 + f1),((1 - f1) + f1)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[f1,1]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(((1 - f1) * |[0,1]|) + (f1 * |[1,1]|)) `1 is V14() real ext-real Element of REAL
(((1 - f1) * |[0,1]|) + (f1 * |[1,1]|)) `2 is V14() real ext-real Element of REAL
c<sub>9</sub> is set
f1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
f1 `1 is V14() real ext-real Element of REAL
f1 `2 is V14() real ext-real Element of REAL
1 - (f1 `1) is V14() real ext-real Element of REAL
(1 - (f1 `1)) * |[0,1]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(f1 `1) * |[1,1]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
((1 - (f1 `1)) * |[0,1]|) + ((f1 `1) * |[1,1]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(1 - (f1 `1)) * 0 is V14() real ext-real Element of REAL
(1 - (f1 `1)) * (|[0,1]| `2) is V14() real ext-real Element of REAL
|[((1 - (f1 `1)) * 0),((1 - (f1 `1)) * (|[0,1]| `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[((1 - (f1 `1)) * 0),((1 - (f1 `1)) * (|[0,1]| `2))]| + ((f1 `1) * |[1,1]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
|[0,(1 - (f1 `1))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(f1 `1) * 1 is V14() real ext-real Element of REAL
|[((f1 `1) * 1),(f1 `1)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[0,(1 - (f1 `1))]| + |[((f1 `1) * 1),(f1 `1)]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
0 + (f1 `1) is V14() real ext-real Element of REAL
(1 - (f1 `1)) + (f1 `1) is V14() real ext-real Element of REAL
|[(0 + (f1 `1)),((1 - (f1 `1)) + (f1 `1))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[1,0]| `2 is V14() real ext-real Element of REAL
|[1,0]| `1 is V14() real ext-real Element of REAL
c<sub>9</sub> is set
f1 is V14() real ext-real Element of REAL
1 - f1 is V14() real ext-real Element of REAL
(1 - f1) * |[0,0]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
f1 * |[1,0]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
((1 - f1) * |[0,0]|) + (f1 * |[1,0]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(0. (TOP-REAL 2)) + (f1 * |[1,0]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
f1 * (|[1,0]| `1) is V14() real ext-real Element of REAL
f1 * (|[1,0]| `2) is V14() real ext-real Element of REAL
|[(f1 * (|[1,0]| `1)),(f1 * (|[1,0]| `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[f1,0]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(((1 - f1) * |[0,0]|) + (f1 * |[1,0]|)) `1 is V14() real ext-real Element of REAL
(((1 - f1) * |[0,0]|) + (f1 * |[1,0]|)) `2 is V14() real ext-real Element of REAL
c<sub>9</sub> is set
f1 is V14() real ext-real Element of REAL
1 - f1 is V14() real ext-real Element of REAL
(1 - f1) * |[1,0]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
f1 * |[1,1]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
((1 - f1) * |[1,0]|) + (f1 * |[1,1]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(1 - f1) * 1 is V14() real ext-real Element of REAL
(1 - f1) * (|[1,0]| `2) is V14() real ext-real Element of REAL
|[((1 - f1) * 1),((1 - f1) * (|[1,0]| `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[((1 - f1) * 1),((1 - f1) * (|[1,0]| `2))]| + (f1 * |[1,1]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
|[(1 - f1),0]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
f1 * 1 is V14() real ext-real Element of REAL
|[f1,(f1 * 1)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[(1 - f1),0]| + |[f1,(f1 * 1)]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(1 - f1) + f1 is V14() real ext-real Element of REAL
0 + f1 is V14() real ext-real Element of REAL
|[((1 - f1) + f1),(0 + f1)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[1,f1]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(((1 - f1) * |[1,0]|) + (f1 * |[1,1]|)) `2 is V14() real ext-real Element of REAL
(((1 - f1) * |[1,0]|) + (f1 * |[1,1]|)) `1 is V14() real ext-real Element of REAL
c₉ is set
f1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
f1 `1 is V14() real ext-real Element of REAL
f1 `2 is V14() real ext-real Element of REAL
1 - (f1 `1) is V14() real ext-real Element of REAL
(1 - (f1 `1)) * |[0,0]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(f1 `1) * |[1,0]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
((1 - (f1 `1)) * |[0,0]|) + ((f1 `1) * |[1,0]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(0. (TOP-REAL 2)) + ((f1 `1) * |[1,0]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(f1 `1) * (|[1,0]| `1) is V14() real ext-real Element of REAL
(f1 `1) * (|[1,0]| `2) is V14() real ext-real Element of REAL
|[((f1 `1) * (|[1,0]| `1)),((f1 `1) * (|[1,0]| `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
c₉ is set
f1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
f1 `1 is V14() real ext-real Element of REAL
f1 `2 is V14() real ext-real Element of REAL
1 - (f1 `2) is V14() real ext-real Element of REAL
(1 - (f1 `2)) * |[1,0]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(f1 `2) * |[1,1]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
((1 - (f1 `2)) * |[1,0]|) + ((f1 `2) * |[1,1]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(1 - (f1 `2)) * 1 is V14() real ext-real Element of REAL
(1 - (f1 `2)) * (|[1,0]| `2) is V14() real ext-real Element of REAL
|[((1 - (f1 `2)) * 1),((1 - (f1 `2)) * (|[1,0]| `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[((1 - (f1 `2)) * 1),((1 - (f1 `2)) * (|[1,0]| `2))]| + ((f1 `2) * |[1,1]|) is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
|[(1 - (f1 `2)),0]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(f1 `2) * 1 is V14() real ext-real Element of REAL
|[((f1 `2) * 1),(f1 `2)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[(1 - (f1 `2)),0]| + |[((f1 `2) * 1),(f1 `2)]| is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2)
(1 - (f1 `2)) + (f1 `2) is V14() real ext-real Element of REAL
0 + (f1 `2) is V14() real ext-real Element of REAL
|[((1 - (f1 `2)) + (f1 `2)),(0 + (f1 `2))]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( ( b₁ `1 = 0 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) or ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 1 ) or ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 0 ) or ( b<sub>1</sub> `1 = 1 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) ) } is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : S₄[b₁] } is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : S₃[b₁] } is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : S₂[b₁] } is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : S₁[b₁] } is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( S₆[b₁] or S₅[b₁] ) } is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : S₆[b₁] } is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : S₅[b₁] } is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : S₆[b₁] } \/ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : S₅[b₁] } is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( S₂[b₁] or S₁[b₁] ) } is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : S₂[b₁] } \/ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : S₁[b₁] } is set
(LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) is non empty functional Element of K10( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( S₄[b₁] or S₃[b₁] ) } is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : S₄[b₁] } \/ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : S₃[b₁] } is set
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) is functional Element of K10( the carrier of (TOP-REAL 2))
{|[0,1]|} is non empty functional set
r is set
q is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
q `1 is V14() real ext-real Element of REAL
q `2 is V14() real ext-real Element of REAL
NE is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
NE `1 is V14() real ext-real Element of REAL
NE `2 is V14() real ext-real Element of REAL
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is functional Element of K10( the carrier of (TOP-REAL 2))
{|[1,0]|} is non empty functional set
r is set
q is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
q `1 is V14() real ext-real Element of REAL
q `2 is V14() real ext-real Element of REAL
NE is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
NE `1 is V14() real ext-real Element of REAL
NE `2 is V14() real ext-real Element of REAL
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) is functional Element of K10( the carrier of (TOP-REAL 2))
{|[0,0]|} is non empty functional set
p is set
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
A `1 is V14() real ext-real Element of REAL
A `2 is V14() real ext-real Element of REAL
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
x `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is functional Element of K10( the carrier of (TOP-REAL 2))
{|[1,1]|} is non empty functional set
p is set
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
A `1 is V14() real ext-real Element of REAL
A `2 is V14() real ext-real Element of REAL
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
x `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) is functional Element of K10( the carrier of (TOP-REAL 2))
the Relation-like Function-like Element of (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) is Relation-like Function-like Element of (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
A `1 is V14() real ext-real Element of REAL
A `2 is V14() real ext-real Element of REAL
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
x `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is functional Element of K10( the carrier of (TOP-REAL 2))
the Relation-like Function-like Element of (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is Relation-like Function-like Element of (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
A `1 is V14() real ext-real Element of REAL
A `2 is V14() real ext-real Element of REAL
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
x `1 is V14() real ext-real Element of REAL
x `2 is V14() real ext-real Element of REAL
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like T_0 T_1 T_2 V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty functional set
x is ordinal natural V14() real ext-real non negative set
x + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
A is Relation-like NAT -defined the carrier of (TOP-REAL p) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL p)
len A is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
A /. x is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
A /. (x + 1) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
LSeg ((A /. x),(A /. (x + 1))) is non empty functional V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
K10( the carrier of (TOP-REAL p)) is non empty set
{ (((1 - b₁) * (A /. x)) + (b₁ * (A /. (x + 1)))) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{} (TOP-REAL p) is empty proper Function-like functional FinSequence-membered closed V154() V155() V156() V157() V158() V159() V160() V175( TOP-REAL p) circled Element of K10( the carrier of (TOP-REAL p))
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like T_0 T_1 T_2 V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty functional set
A is ordinal natural V14() real ext-real non negative set
A + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
x is Relation-like NAT -defined the carrier of (TOP-REAL p) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL p)
len x is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
x /. A is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
(p,x,A) is functional Element of K10( the carrier of (TOP-REAL p))
K10( the carrier of (TOP-REAL p)) is non empty set
x /. (A + 1) is Relation-like NAT -defined Function-like V38() V45(p) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL p)
LSeg ((x /. A),(x /. (A + 1))) is non empty functional V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b₁) * (x /. A)) + (b₁ * (x /. (A + 1)))) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like T_0 T_1 T_2 V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty functional set
A is Relation-like NAT -defined the carrier of (TOP-REAL p) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL p)
len A is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
{ (p,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
union { (p,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
K10( the carrier of (TOP-REAL p)) is non empty set
bool the carrier of (TOP-REAL p) is non empty Element of K10(K10( the carrier of (TOP-REAL p)))
K10(K10( the carrier of (TOP-REAL p))) is non empty set
r is set
q is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(p,A,q) is functional Element of K10( the carrier of (TOP-REAL p))
q + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
r is Element of K10(K10( the carrier of (TOP-REAL p)))
union r is functional Element of K10( the carrier of (TOP-REAL p))
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like T_0 T_1 T_2 V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty functional set
A is Relation-like NAT -defined the carrier of (TOP-REAL p) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL p)
len A is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(p,A) is functional Element of K10( the carrier of (TOP-REAL p))
K10( the carrier of (TOP-REAL p)) is non empty set
{ (p,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
union { (p,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
the Element of { (p,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is Element of { (p,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) }
q is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(p,A,q) is functional Element of K10( the carrier of (TOP-REAL p))
q + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
0 + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
q is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(p,A,q) is functional Element of K10( the carrier of (TOP-REAL p))
q + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
0 + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
0 + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
1 + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(p,A,1) is functional Element of K10( the carrier of (TOP-REAL p))
p is ordinal natural V14() real ext-real non negative set
TOP-REAL p is non empty TopSpace-like T_0 T_1 T_2 V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL p) is non empty functional set
A is Relation-like NAT -defined the carrier of (TOP-REAL p) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL p)
len A is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(p,A) is functional Element of K10( the carrier of (TOP-REAL p))
K10( the carrier of (TOP-REAL p)) is non empty set
{ (p,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
union { (p,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
{|[0,0]|,|[1,1]|} is non empty functional set
|[1,1]| `1 is V14() real ext-real Element of REAL
<*|[0,0]|,|[1,0]|,|[1,1]|*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() V45(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
<*|[0,0]|,|[0,1]|,|[1,1]|*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() V45(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
|[0,0]| `1 is V14() real ext-real Element of REAL
f1 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(2,f1) is functional Element of K10( the carrier of (TOP-REAL 2))
len f1 is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
{ (2,f1,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f1 ) } is set
union { (2,f1,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f1 ) } is set
f1 /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
f1 /. (len f1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
c₉ is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(2,c₉) is functional Element of K10( the carrier of (TOP-REAL 2))
len c₉ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
{ (2,c₉,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len c₉ ) } is set
union { (2,c₉,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len c₉ ) } is set
(2,f1) \/ (2,c₉) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,f1) /\ (2,c₉) is functional Element of K10( the carrier of (TOP-REAL 2))
c₉ /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
c₉ /. (len c₉) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
f1 /. 2 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
f is set
hh is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
hh `1 is V14() real ext-real Element of REAL
hh `2 is V14() real ext-real Element of REAL
c₁₃ is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
c₁₃ `1 is V14() real ext-real Element of REAL
c<sub>13</sub> `2 is V14() real ext-real Element of REAL
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 1 ) } /\ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 0 ) } is set
|[1,0]| `2 is V14() real ext-real Element of REAL
|[1,0]| `1 is V14() real ext-real Element of REAL
1 + 2 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
1 + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
f1 /. 3 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
{(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))} is non empty set
f is set
hh is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,f1,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
hh + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
2 + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
Seg (len f1) is V38() V45( len f1) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
(2,f1,1) is functional Element of K10( the carrier of (TOP-REAL 2))
c₉ /. 3 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
|[0,0]| `2 is V14() real ext-real Element of REAL
f is set
hh is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
hh `1 is V14() real ext-real Element of REAL
hh `2 is V14() real ext-real Element of REAL
c<sub>13</sub> is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
c<sub>13</sub> `1 is V14() real ext-real Element of REAL
c₁₃ `2 is V14() real ext-real Element of REAL
f is ordinal natural V14() real ext-real non negative set
f + 2 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,f1,f) is functional Element of K10( the carrier of (TOP-REAL 2))
f + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,f1,(f + 1)) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,f1,f) /\ (2,f1,(f + 1)) is functional Element of K10( the carrier of (TOP-REAL 2))
f1 /. (f + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
{(f1 /. (f + 1))} is non empty functional set
(2,f1,(1 + 1)) is functional Element of K10( the carrier of (TOP-REAL 2))
f is ordinal natural V14() real ext-real non negative set
f + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,f1,f) is functional Element of K10( the carrier of (TOP-REAL 2))
hh is ordinal natural V14() real ext-real non negative set
(2,f1,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
hh + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
hh + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,f1,f) /\ (2,f1,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
hh + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,f1,f) /\ (2,f1,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
hh + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,f1,f) /\ (2,f1,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,f1,f) /\ (2,f1,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,f1,f) /\ (2,f1,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,f1,f) /\ (2,f1,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
f is ordinal natural V14() real ext-real non negative set
f + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
f1 /. f is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(f1 /. f) `1 is V14() real ext-real Element of REAL
f1 /. (f + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(f1 /. (f + 1)) `1 is V14() real ext-real Element of REAL
(f1 /. f) `2 is V14() real ext-real Element of REAL
(f1 /. (f + 1)) `2 is V14() real ext-real Element of REAL
|[0,1]| `2 is V14() real ext-real Element of REAL
c₉ /. 2 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
{(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))} is non empty set
f is set
hh is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,c₉,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
hh + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
2 + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
Seg (len c₉) is V38() V45( len c₉) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
(2,c₉,1) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,c₉,2) is functional Element of K10( the carrier of (TOP-REAL 2))
union {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))} is set
|[1,1]| `2 is V14() real ext-real Element of REAL
f is set
hh is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
hh `1 is V14() real ext-real Element of REAL
hh `2 is V14() real ext-real Element of REAL
c<sub>13</sub> is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
c<sub>13</sub> `1 is V14() real ext-real Element of REAL
c₁₃ `2 is V14() real ext-real Element of REAL
f is ordinal natural V14() real ext-real non negative set
f + 2 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,c<sub>9</sub>,f) is functional Element of K10( the carrier of (TOP-REAL 2))
f + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,c<sub>9</sub>,(f + 1)) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,c<sub>9</sub>,f) /\ (2,c<sub>9</sub>,(f + 1)) is functional Element of K10( the carrier of (TOP-REAL 2))
c<sub>9</sub> /. (f + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
{(c<sub>9</sub> /. (f + 1))} is non empty functional set
(2,c<sub>9</sub>,(1 + 1)) is functional Element of K10( the carrier of (TOP-REAL 2))
f is ordinal natural V14() real ext-real non negative set
f + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,c<sub>9</sub>,f) is functional Element of K10( the carrier of (TOP-REAL 2))
hh is ordinal natural V14() real ext-real non negative set
(2,c<sub>9</sub>,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
hh + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
hh + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,c<sub>9</sub>,f) /\ (2,c<sub>9</sub>,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
hh + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,c<sub>9</sub>,f) /\ (2,c<sub>9</sub>,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
hh + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,c<sub>9</sub>,f) /\ (2,c<sub>9</sub>,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,c<sub>9</sub>,f) /\ (2,c<sub>9</sub>,hh) is functional Element of K10( the carrier of (TOP-REAL 2))
f is ordinal natural V14() real ext-real non negative set
f + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
c<sub>9</sub> /. f is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(c<sub>9</sub> /. f) `1 is V14() real ext-real Element of REAL
c₉ /. (f + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(c₉ /. (f + 1)) `1 is V14() real ext-real Element of REAL
(c<sub>9</sub> /. f) `2 is V14() real ext-real Element of REAL
(c₉ /. (f + 1)) `2 is V14() real ext-real Element of REAL
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,f1,2) is functional Element of K10( the carrier of (TOP-REAL 2))
union {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))} is set
(LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) is non empty functional Element of K10( the carrier of (TOP-REAL 2))
{ b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 0 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } \/ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 1 ) } is set
{ b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 0 ) } \/ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = 1 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) } is set
( { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 0 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } \/ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 1 ) } ) /\ ( { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 0 ) } \/ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = 1 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) } ) is set
( { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 0 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } \/ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 1 ) } ) /\ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 0 ) } is set
( { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = 0 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) } \/ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 1 ) } ) /\ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = 1 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) } is set
(( { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 0 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } \/ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 1 ) } ) /\ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 0 ) } ) \/ (( { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = 0 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) } \/ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 1 ) } ) /\ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = 1 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) } ) is set
{ b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 0 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } /\ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 0 ) } is set
( { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 0 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } /\ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 0 ) } ) \/ ( { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 1 ) } /\ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 0 ) } ) is set
(( { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 0 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } /\ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 0 ) } ) \/ ( { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 1 ) } /\ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 0 ) } )) \/ (( { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 0 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } \/ { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 1 ) } ) /\ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 1 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } ) is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = 0 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) } /\ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 1 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } is set
{ b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 1 ) } /\ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 1 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } is set
( { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = 0 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) } /\ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 1 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } ) \/ ( { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 1 ) } /\ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 1 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } ) is set
(( { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = 0 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) } /\ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 0 ) } ) \/ ( { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 1 ) } /\ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 0 ) } )) \/ (( { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = 0 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) } /\ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 1 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } ) \/ ( { b₁ where b₁ is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 1 ) } /\ { b<sub>1</sub> where b<sub>1</sub> is V45(2) FinSequence-like V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 1 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } )) is set
p is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
len p is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
p /. (len p) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(2,p) is functional Element of K10( the carrier of (TOP-REAL 2))
{ (2,p,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p ) } is set
union { (2,p,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p ) } is set
1 + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
p /. (1 + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
Seg (len p) is V38() V45( len p) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
q is ordinal natural V14() real ext-real non negative set
q + 2 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
p | (q + 2) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(2,(p | (q + 2))) is functional Element of K10( the carrier of (TOP-REAL 2))
len (p | (q + 2)) is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
{ (2,(p | (q + 2)),b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | (q + 2)) ) } is set
union { (2,(p | (q + 2)),b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | (q + 2)) ) } is set
p /. (q + 2) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
q + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(q + 1) + 2 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
p | ((q + 1) + 2) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(2,(p | ((q + 1) + 2))) is functional Element of K10( the carrier of (TOP-REAL 2))
len (p | ((q + 1) + 2)) is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
{ (2,(p | ((q + 1) + 2)),b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | ((q + 1) + 2)) ) } is set
union { (2,(p | ((q + 1) + 2)),b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | ((q + 1) + 2)) ) } is set
p /. ((q + 1) + 2) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(q + 2) + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
p /. ((q + 2) + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(q + 1) + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
LSeg ((p /. (q + 2)),(p /. ((q + 2) + 1))) is non empty V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (p /. (q + 2))) + (b₁ * (p /. ((q + 2) + 1)))) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
H₁(q) \/ (LSeg ((p /. (q + 2)),(p /. ((q + 2) + 1)))) is non empty functional Element of K10( the carrier of (TOP-REAL 2))
(q + 1) + 2 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
dom p is V154() V155() V156() V157() V158() V159() Element of K10(NAT)
c₉ is non empty functional Element of K10( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | c₉ is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | c₉) is non empty set
K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₉)) is non empty set
K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₉))) is non empty set
f1 is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | c₉) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₉)) Element of K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₉)))
f1 . 0 is set
f1 . 1 is set
c₉ is non empty functional Element of K10( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | c₉ is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | c₉) is non empty set
K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₉)) is non empty set
K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₉))) is non empty set
q + (1 + 1) is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
f1 is set
(2,p,(q + 2)) is functional Element of K10( the carrier of (TOP-REAL 2))
H₁(q) \/ (2,p,(q + 2)) is functional Element of K10( the carrier of (TOP-REAL 2))
f is set
hh is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,(p | (q + 2)),hh) is functional Element of K10( the carrier of (TOP-REAL 2))
hh + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
Seg (len (p | (q + 2))) is V38() V45( len (p | (q + 2))) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
dom (p | (q + 2)) is V154() V155() V156() V157() V158() V159() Element of K10(NAT)
(p | (q + 2)) /. hh is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p | (q + 2)) /. (hh + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
Seg ((q + 1) + 2) is non empty V38() V45((q + 1) + 2) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
p | ((q + 1) + 2) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (p | ((q + 1) + 2)) is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
Seg (len (p | ((q + 1) + 2))) is V38() V45( len (p | ((q + 1) + 2))) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
dom (p | ((q + 1) + 2)) is V154() V155() V156() V157() V158() V159() Element of K10(NAT)
(p | ((q + 1) + 2)) /. hh is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
p /. hh is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
1 + 2 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
q + (1 + 2) is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
q + 3 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
1 + hh is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(p | ((q + 1) + 2)) /. (hh + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
p /. (hh + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
LSeg (((p | (q + 2)) /. hh),((p | (q + 2)) /. (hh + 1))) is non empty V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * ((p | (q + 2)) /. hh)) + (b₁ * ((p | (q + 2)) /. (hh + 1)))) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(2,(p | ((q + 1) + 2)),hh) is functional Element of K10( the carrier of (TOP-REAL 2))
{ (2,(p | ((q + 1) + 2)),b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | ((q + 1) + 2)) ) } is set
p | ((q + 1) + 2) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (p | ((q + 1) + 2)) is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
Seg (len (p | ((q + 1) + 2))) is V38() V45( len (p | ((q + 1) + 2))) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
dom (p | ((q + 1) + 2)) is V154() V155() V156() V157() V158() V159() Element of K10(NAT)
(p | ((q + 1) + 2)) /. ((q + 2) + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p | ((q + 1) + 2)) /. (q + 2) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(2,(p | ((q + 1) + 2)),(q + 2)) is functional Element of K10( the carrier of (TOP-REAL 2))
{ (2,(p | ((q + 1) + 2)),b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | ((q + 1) + 2)) ) } is set
f is non empty functional Element of K10( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | f is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | f) is non empty set
K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)) is non empty set
K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | f))) is non empty set
p | ((q + 1) + 2) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (p | ((q + 1) + 2)) is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(len (p | ((q + 1) + 2))) - 1 is V14() real ext-real Element of REAL
((q + 1) + 2) - 1 is V14() real ext-real Element of REAL
f1 is set
{ (2,(p | ((q + 1) + 2)),b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | ((q + 1) + 2)) ) } is set
f is set
hh is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,(p | ((q + 1) + 2)),hh) is functional Element of K10( the carrier of (TOP-REAL 2))
hh + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(hh + 1) - 1 is V14() real ext-real Element of REAL
Seg (len (p | ((q + 1) + 2))) is V38() V45( len (p | ((q + 1) + 2))) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
dom (p | ((q + 1) + 2)) is V154() V155() V156() V157() V158() V159() Element of K10(NAT)
(p | ((q + 1) + 2)) /. ((q + 2) + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
2 + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
q + (2 + 1) is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
p /. (q + (2 + 1)) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p | ((q + 1) + 2)) /. (q + 2) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(2,(p | ((q + 1) + 2)),(q + 2)) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,(p | (q + 2)),hh) is functional Element of K10( the carrier of (TOP-REAL 2))
(p | (q + 2)) /. hh is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p | (q + 2)) /. (hh + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
1 + hh is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
Seg (len (p | (q + 2))) is V38() V45( len (p | (q + 2))) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
dom (p | (q + 2)) is V154() V155() V156() V157() V158() V159() Element of K10(NAT)
Seg ((q + 1) + 2) is non empty V38() V45((q + 1) + 2) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
Seg (len (p | ((q + 1) + 2))) is V38() V45( len (p | ((q + 1) + 2))) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
dom (p | ((q + 1) + 2)) is V154() V155() V156() V157() V158() V159() Element of K10(NAT)
(p | ((q + 1) + 2)) /. hh is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
p /. hh is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p | ((q + 1) + 2)) /. (hh + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
p /. (hh + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
LSeg (((p | (q + 2)) /. hh),((p | (q + 2)) /. (hh + 1))) is non empty V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * ((p | (q + 2)) /. hh)) + (b₁ * ((p | (q + 2)) /. (hh + 1)))) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(TOP-REAL 2) | (LSeg ((p /. (q + 2)),(p /. ((q + 2) + 1)))) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (LSeg ((p /. (q + 2)),(p /. ((q + 2) + 1))))) is non empty set
K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((p /. (q + 2)),(p /. ((q + 2) + 1)))))) is non empty set
K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((p /. (q + 2)),(p /. ((q + 2) + 1))))))) is non empty set
f1 is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (LSeg ((p /. (q + 2)),(p /. ((q + 2) + 1))))) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((p /. (q + 2)),(p /. ((q + 2) + 1)))))) Element of K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((p /. (q + 2)),(p /. ((q + 2) + 1)))))))
f1 . 0 is set
f1 . 1 is set
f is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | c₉) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₉)) Element of K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₉)))
f . 0 is set
f . 1 is set
f is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | c₉) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₉)) Element of K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₉)))
f . 0 is set
f . 1 is set
H₁(q) /\ (LSeg ((p /. (q + 2)),(p /. ((q + 2) + 1)))) is functional Element of K10( the carrier of (TOP-REAL 2))
hh is set
(2,p,(q + 1)) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,p,((q + 1) + 1)) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,p,(q + 1)) /\ (2,p,((q + 1) + 1)) is functional Element of K10( the carrier of (TOP-REAL 2))
p /. ((q + 1) + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
{(p /. ((q + 1) + 1))} is non empty functional set
p /. (q + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
1 + q is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
X is set
i is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,(p | (q + 2)),i) is functional Element of K10( the carrier of (TOP-REAL 2))
i + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
Seg (len (p | (q + 2))) is V38() V45( len (p | (q + 2))) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
dom (p | (q + 2)) is V154() V155() V156() V157() V158() V159() Element of K10(NAT)
(p | (q + 2)) /. (q + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
1 + (q + 1) is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(p | (q + 2)) /. ((q + 1) + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
LSeg ((p /. (q + 1)),(p /. ((q + 1) + 1))) is non empty functional V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (p /. (q + 1))) + (b₁ * (p /. ((q + 1) + 1)))) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(2,(p | (q + 2)),(q + 1)) is functional Element of K10( the carrier of (TOP-REAL 2))
p /. i is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
p /. (i + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p | (q + 2)) /. i is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
1 + i is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(p | (q + 2)) /. (i + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(2,p,i) is functional Element of K10( the carrier of (TOP-REAL 2))
LSeg ((p /. i),(p /. (i + 1))) is non empty functional V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (p /. i)) + (b₁ * (p /. (i + 1)))) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(2,(p | (q + 2)),(q + 1)) is functional Element of K10( the carrier of (TOP-REAL 2))
Seg (q + 2) is non empty V38() V45(q + 2) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
dom (p | (q + 2)) is V154() V155() V156() V157() V158() V159() Element of K10(NAT)
(p | (q + 2)) /. ((q + 1) + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
{(p /. (q + 2))} is non empty functional set
hh is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | c₉) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₉)) Element of K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | c₉)))
hh . 0 is set
hh . 1 is set
hh is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | f) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)) Element of K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | f)))
hh . 0 is set
hh . 1 is set
p /. ((q + 1) + 2) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
p | 2 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
Seg 2 is non empty V38() V45(2) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
p | (Seg 2) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K10(K11(NAT, the carrier of (TOP-REAL 2)))
K11(NAT, the carrier of (TOP-REAL 2)) is set
K10(K11(NAT, the carrier of (TOP-REAL 2))) is non empty set
dom (p | 2) is V154() V155() V156() V157() V158() V159() Element of K10(NAT)
dom p is V154() V155() V156() V157() V158() V159() Element of K10(NAT)
(dom p) /\ (Seg 2) is V154() V155() V156() V157() V158() V159() Element of K10(NAT)
(Seg (len p)) /\ (Seg 2) is V154() V155() V156() V157() V158() V159() Element of K10(NAT)
len (p | 2) is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
Seg (len (p | 2)) is V38() V45( len (p | 2)) V154() V155() V156() V157() V158() V159() Element of K10(NAT)
(p | 2) /. 2 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
q is set
{ (2,(p | 2),b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | 2) ) } is set
(2,p,1) is functional Element of K10( the carrier of (TOP-REAL 2))
NE is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(2,(p | 2),NE) is functional Element of K10( the carrier of (TOP-REAL 2))
NE + 1 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(p | 2) /. (1 + 1) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p | 2) /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
LSeg ((p /. 1),(p /. (1 + 1))) is non empty V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (p /. 1)) + (b₁ * (p /. (1 + 1)))) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg ((p /. 1),(p /. (1 + 1))) is non empty V216( TOP-REAL 2) Element of K10( the carrier of (TOP-REAL 2))
{ (((1 - b₁) * (p /. 1)) + (b₁ * (p /. (1 + 1)))) where b₁ is V14() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(p | 2) /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(2,(p | 2),1) is functional Element of K10( the carrier of (TOP-REAL 2))
{(2,p,1)} is non empty set
0 + 2 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
p | (0 + 2) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(2,(p | (0 + 2))) is functional Element of K10( the carrier of (TOP-REAL 2))
len (p | (0 + 2)) is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
{ (2,(p | (0 + 2)),b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | (0 + 2)) ) } is set
union { (2,(p | (0 + 2)),b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | (0 + 2)) ) } is set
0 + 2 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
(TOP-REAL 2) | (LSeg ((p /. 1),(p /. (1 + 1)))) is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (LSeg ((p /. 1),(p /. (1 + 1))))) is non empty set
K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((p /. 1),(p /. (1 + 1)))))) is non empty set
K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((p /. 1),(p /. (1 + 1))))))) is non empty set
p /. (0 + 2) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
p /. (0 + 2) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
q is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (LSeg ((p /. 1),(p /. (1 + 1))))) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((p /. 1),(p /. (1 + 1)))))) Element of K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | (LSeg ((p /. 1),(p /. (1 + 1)))))))
q . 0 is set
q . 1 is set
(len p) - 2 is V14() real ext-real Element of REAL
q is ordinal natural V14() real ext-real non negative set
q + 2 is non empty ordinal natural V14() real ext-real positive non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
p | (q + 2) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(2,(p | (q + 2))) is functional Element of K10( the carrier of (TOP-REAL 2))
len (p | (q + 2)) is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
{ (2,(p | (q + 2)),b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | (q + 2)) ) } is set
union { (2,(p | (q + 2)),b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | (q + 2)) ) } is set
p /. (q + 2) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
NE is non empty functional Element of K10( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | NE is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | NE) is non empty set
K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | NE)) is non empty set
K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | NE))) is non empty set
f is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | NE) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | NE)) Element of K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | NE)))
f . 0 is set
f . 1 is set
f is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | NE) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | NE)) Element of K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | NE)))
f . 0 is set
f . 1 is set
p | (len p) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p | (Seg (len p)) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K10(K11(NAT, the carrier of (TOP-REAL 2)))
p | (dom p) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K10(K11(NAT, the carrier of (TOP-REAL 2)))
(TOP-REAL 2) | (2,p) is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | (2,p)) is set
K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | (2,p))) is set
K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | (2,p)))) is non empty set
f is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | (2,p)) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | (2,p))) Element of K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | (2,p))))
f . 0 is set
f . 1 is set
p is functional Element of K10( the carrier of (TOP-REAL 2))
A is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(2,A) is functional Element of K10( the carrier of (TOP-REAL 2))
len A is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
{ (2,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
union { (2,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
p is functional Element of K10( the carrier of (TOP-REAL 2))
p is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
A is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(2,p) is functional Element of K10( the carrier of (TOP-REAL 2))
len p is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
{ (2,p,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p ) } is set
union { (2,p,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p ) } is set
(2,A) is functional Element of K10( the carrier of (TOP-REAL 2))
len A is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
{ (2,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
union { (2,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
(2,p) \/ (2,A) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,p) /\ (2,A) is functional Element of K10( the carrier of (TOP-REAL 2))
p /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
p /. (len p) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
A /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
A /. (len A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
p is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
A is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(2,p) is functional Element of K10( the carrier of (TOP-REAL 2))
len p is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
{ (2,p,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p ) } is set
union { (2,p,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p ) } is set
(2,A) is functional Element of K10( the carrier of (TOP-REAL 2))
len A is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
{ (2,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
union { (2,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
(2,p) \/ (2,A) is functional Element of K10( the carrier of (TOP-REAL 2))
(2,p) /\ (2,A) is functional Element of K10( the carrier of (TOP-REAL 2))
p /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
p /. (len p) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
A /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
A /. (len A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
x is non empty functional Element of K10( the carrier of (TOP-REAL 2))
r is non empty functional Element of K10( the carrier of (TOP-REAL 2))
x \/ r is non empty functional Element of K10( the carrier of (TOP-REAL 2))
x /\ r is functional Element of K10( the carrier of (TOP-REAL 2))
p is functional Element of K10( the carrier of (TOP-REAL 2))
A is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(2,A) is functional Element of K10( the carrier of (TOP-REAL 2))
len A is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT
{ (2,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
union { (2,A,b₁) where b₁ is ordinal natural V14() real ext-real non negative V91() V92() V154() V155() V156() V157() V158() V159() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len A ) } is set
A /. 1 is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
A /. (len A) is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
p is functional Element of K10( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | p is strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | p) is set
K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | p)) is set
K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | p))) is non empty set
A is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
x is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
r is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | p) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | p)) Element of K10(K11( the carrier of I[01], the carrier of ((TOP-REAL 2) | p)))
r . 0 is set
r . 1 is set
F₁() is ordinal natural V14() real ext-real non negative set
TOP-REAL F₁() is non empty TopSpace-like T_0 T_1 T_2 V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL F₁()) is non empty functional set
K10( the carrier of (TOP-REAL F₁())) is non empty set
p is set
A is set
A is functional Element of K10( the carrier of (TOP-REAL F₁()))
x is Relation-like NAT -defined Function-like V38() V45(F₁()) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL F₁())
r is Relation-like NAT -defined Function-like V38() V45(F₁()) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL F₁())
F₁() is ordinal natural V14() real ext-real non negative set
TOP-REAL F₁() is non empty TopSpace-like T_0 T_1 T_2 V120() V166() V167() V168() V169() V170() V171() V172() strict RLTopStruct
the carrier of (TOP-REAL F₁()) is non empty functional set
K10( the carrier of (TOP-REAL F₁())) is non empty set
p is functional Element of K10( the carrier of (TOP-REAL F₁()))
A is functional Element of K10( the carrier of (TOP-REAL F₁()))
x is set
x is set
p is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
p is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p) is functional Element of K10( the carrier of (TOP-REAL 2))
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
{ b₁ where b₁ is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = p `1 & p `2 <= b<sub>1</sub> `2 ) } is set
x is set
r is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
r `2 is V14() real ext-real Element of REAL
r `1 is V14() real ext-real Element of REAL
x is set
r is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
r `1 is V14() real ext-real Element of REAL
r `2 is V14() real ext-real Element of REAL
p is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p) is functional Element of K10( the carrier of (TOP-REAL 2))
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
{ |[(p `1),b<sub>1</sub>]| where b<sub>1</sub> is V14() real ext-real Element of REAL : p `2 <= b₁ } is set
x is set
r is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
r `2 is V14() real ext-real Element of REAL
r `1 is V14() real ext-real Element of REAL
|[(r `1),(r `2)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
x is set
r is V14() real ext-real Element of REAL
|[(p `1),r]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
q is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
q `2 is V14() real ext-real Element of REAL
q `1 is V14() real ext-real Element of REAL
p is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p) is functional Element of K10( the carrier of (TOP-REAL 2))
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2) : ( p `1 <= b₁ `1 & b<sub>1</sub> `2 = p `2 ) } is set
x is set
r is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
r `2 is V14() real ext-real Element of REAL
r `1 is V14() real ext-real Element of REAL
x is set
r is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
r `1 is V14() real ext-real Element of REAL
r `2 is V14() real ext-real Element of REAL
p is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p) is functional Element of K10( the carrier of (TOP-REAL 2))
p `2 is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,(p `2)]| where b₁ is V14() real ext-real Element of REAL : p `1 <= b<sub>1</sub> } is set
x is set
r is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
r `2 is V14() real ext-real Element of REAL
r `1 is V14() real ext-real Element of REAL
|[(r `1),(r `2)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
x is set
r is V14() real ext-real Element of REAL
|[r,(p `2)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
q is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
q `2 is V14() real ext-real Element of REAL
q `1 is V14() real ext-real Element of REAL
p is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p) is functional Element of K10( the carrier of (TOP-REAL 2))
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
{ b₁ where b₁ is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = p `1 & b₁ `2 <= p `2 ) } is set
x is set
r is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
r `2 is V14() real ext-real Element of REAL
r `1 is V14() real ext-real Element of REAL
x is set
r is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
r `1 is V14() real ext-real Element of REAL
r `2 is V14() real ext-real Element of REAL
p is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p) is functional Element of K10( the carrier of (TOP-REAL 2))
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
{ |[(p `1),b<sub>1</sub>]| where b<sub>1</sub> is V14() real ext-real Element of REAL : b<sub>1</sub> <= p `2 } is set
x is set
r is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
r `2 is V14() real ext-real Element of REAL
r `1 is V14() real ext-real Element of REAL
|[(r `1),(r `2)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
x is set
r is V14() real ext-real Element of REAL
|[(p `1),r]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
q is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
q `2 is V14() real ext-real Element of REAL
q `1 is V14() real ext-real Element of REAL
p is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p) is functional Element of K10( the carrier of (TOP-REAL 2))
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= p `1 & b<sub>1</sub> `2 = p `2 ) } is set
x is set
r is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
r `2 is V14() real ext-real Element of REAL
r `1 is V14() real ext-real Element of REAL
x is set
r is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
r `1 is V14() real ext-real Element of REAL
r `2 is V14() real ext-real Element of REAL
p is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p) is functional Element of K10( the carrier of (TOP-REAL 2))
p `2 is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
{ |[b<sub>1</sub>,(p `2)]| where b₁ is V14() real ext-real Element of REAL : b₁ <= p `1 } is set
x is set
r is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
r `2 is V14() real ext-real Element of REAL
r `1 is V14() real ext-real Element of REAL
|[(r `1),(r `2)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
x is set
r is V14() real ext-real Element of REAL
|[r,(p `2)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
q is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
q `2 is V14() real ext-real Element of REAL
q `1 is V14() real ext-real Element of REAL
p is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p) is functional Element of K10( the carrier of (TOP-REAL 2))
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
{ |[(p `1),b<sub>1</sub>]| where b<sub>1</sub> is V14() real ext-real Element of REAL : p `2 <= b₁ } is set
|[(p `1),(p `2)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p) is functional Element of K10( the carrier of (TOP-REAL 2))
p `2 is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
{ |[b₁,(p `2)]| where b<sub>1</sub> is V14() real ext-real Element of REAL : p `1 <= b₁ } is set
|[(p `1),(p `2)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p) is functional Element of K10( the carrier of (TOP-REAL 2))
p `1 is V14() real ext-real Element of REAL
p `2 is V14() real ext-real Element of REAL
{ |[(p `1),b<sub>1</sub>]| where b<sub>1</sub> is V14() real ext-real Element of REAL : b<sub>1</sub> <= p `2 } is set
|[(p `1),(p `2)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p) is functional Element of K10( the carrier of (TOP-REAL 2))
p `2 is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL
{ |[b₁,(p `2)]| where b<sub>1</sub> is V14() real ext-real Element of REAL : b<sub>1</sub> <= p `1 } is set
|[(p `1),(p `2)]| is non empty Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
p is Relation-like NAT -defined Function-like V38() V45(2) FinSequence-like FinSubsequence-like V144() V145() V146() Element of the carrier of (TOP-REAL 2)
(p) is non empty functional Element of K10( the carrier of (TOP-REAL 2))
(p) is non empty functional Element of K10( the carrier of (TOP-REAL 2))
(p) is non empty functional Element of K10( the carrier of (TOP-REAL 2))
(p) is non empty functional Element of K10( the carrier of (TOP-REAL 2))
p `2 is V14() real ext-real Element of REAL
p `1 is V14() real ext-real Element of REAL