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
F1() is non empty set
{ b1 where b1 is Element of F1() : ( P1[b1] or P2[b1] ) } is set
{ b1 where b1 is Element of F1() : P1[b1] } is set
{ b1 where b1 is Element of F1() : P2[b1] } is set
{ b1 where b1 is Element of F1() : P1[b1] } \/ { b1 where b1 is Element of F1() : P2[b1] } is set
r is set
q is Element of F1()
q is Element of F1()
{ b2 where b1 is Element of F1() : ( P1[b2] or P2[b2] ) } is set
q is Element of F1()
{ b2 where b1 is Element of F1() : ( P1[b2] or P2[b2] ) } is set
{ b2 where b1 is Element of F1() : ( P1[b2] or P2[b2] ) } 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
c9 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))))
c9 . 0 is set
c9 . 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 - b1) * |[0,0]|) + (b1 * |[0,1]|)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * |[0,1]|) + (b1 * |[1,1]|)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * |[1,1]|) + (b1 * |[1,0]|)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * |[1,0]|) + (b1 * |[0,0]|)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * x) + (b1 * r)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (x,A) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b1) * x) + (b1 * A)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * p) + (b1 * A)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * p) + (b1 * A)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * x) + (b1 * r)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (x,A) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b1) * x) + (b1 * A)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (A,r) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b1) * A) + (b1 * r)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * r) + (b1 * A)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * A) + (b1 * x)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * r) + (b1 * q)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (A,r) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b1) * A) + (b1 * r)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (r,x) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b1) * r) + (b1 * x)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * q) + (b1 * r)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * r) + (b1 * q)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * r) + (b1 * A)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (A,x) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b1) * A) + (b1 * x)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * x) + (b1 * q)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * r) + (b1 * x)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * x) + (b1 * A)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (A,q) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b1) * A) + (b1 * q)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 - b1) * x) + (b1 * r)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (x,A) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b1) * x) + (b1 * A)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (A,r) is non empty V216( TOP-REAL p) Element of K10( the carrier of (TOP-REAL p))
{ (((1 - b1) * A) + (b1 * r)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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)
c9 is V14() real ext-real Element of REAL
1 - c9 is V14() real ext-real Element of REAL
(1 - c9) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
c9 * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - c9) * x) + (c9 * 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) * c9 is V14() real ext-real Element of REAL
(1 - f) * c9 is V14() real ext-real Element of REAL
((1 - f) * c9) + f is V14() real ext-real Element of REAL
(1 - f) * ((1 - c9) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - f) * (c9 * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * ((1 - c9) * x)) + ((1 - f) * (c9 * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * ((1 - c9) * x)) + ((1 - f) * (c9 * r))) + (f * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - f) * (1 - c9) is V14() real ext-real Element of REAL
((1 - f) * (1 - c9)) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * (1 - c9)) * x) + ((1 - f) * (c9 * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - f) * (1 - c9)) * x) + ((1 - f) * (c9 * r))) + (f * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * c9) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * (1 - c9)) * x) + (((1 - f) * c9) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - f) * (1 - c9)) * x) + (((1 - f) * c9) * r)) + (f * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * c9) * r) + (f * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * (1 - c9)) * x) + ((((1 - f) * c9) * r) + (f * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * c9) + f) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * (1 - c9)) * x) + ((((1 - f) * c9) + 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) * c9) + f) is V14() real ext-real Element of REAL
(1 - (((1 - f) * c9) + f)) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - c9) * x) + (c9 * r)) - ((1 - (((1 - f) * c9) + f)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - c9) * x) + (c9 * r)) - ((1 - (((1 - f) * c9) + f)) * x)) - ((((1 - f) * c9) + f) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - c9) * x) - ((1 - (((1 - f) * c9) + f)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - c9) * x) - ((1 - (((1 - f) * c9) + f)) * x)) + (c9 * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - c9) * x) - ((1 - (((1 - f) * c9) + f)) * x)) + (c9 * r)) - ((((1 - f) * c9) + f) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - c9) - (1 - (((1 - f) * c9) + f)) is V14() real ext-real Element of REAL
((1 - c9) - (1 - (((1 - f) * c9) + f))) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - c9) - (1 - (((1 - f) * c9) + f))) * x) + (c9 * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - c9) - (1 - (((1 - f) * c9) + f))) * x) + (c9 * r)) - ((((1 - f) * c9) + f) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * c9) + f) - c9 is V14() real ext-real Element of REAL
((((1 - f) * c9) + f) - c9) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((((1 - f) * c9) + f) - c9) * x) - ((((1 - f) * c9) + f) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((((1 - f) * c9) + f) - c9) * x) - ((((1 - f) * c9) + f) * r)) + (c9 * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - f) * c9) + f) * r) - (c9 * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((((1 - f) * c9) + f) - c9) * x) - (((((1 - f) * c9) + f) * r) - (c9 * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - f) * c9) + f) - c9) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((((1 - f) * c9) + f) - c9) * x) - (((((1 - f) * c9) + f) - c9) * 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) * c9) + f) - c9) * (x - r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * ((1 - c9) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * (c9 * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(f * ((1 - c9) * x)) + (f * (c9 * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * x) + ((f * ((1 - c9) * x)) + (f * (c9 * r))) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * x) + (f * ((1 - c9) * x)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * x) + (f * ((1 - c9) * x))) + (f * (c9 * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * (1 - c9) is V14() real ext-real Element of REAL
(f * (1 - c9)) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - f) * x) + ((f * (1 - c9)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * x) + ((f * (1 - c9)) * x)) + (f * (c9 * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - f) + (f * (1 - c9)) is V14() real ext-real Element of REAL
((1 - f) + (f * (1 - c9))) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) + (f * (1 - c9))) * x) + (f * (c9 * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
f * c9 is V14() real ext-real Element of REAL
1 - (f * c9) is V14() real ext-real Element of REAL
(1 - (f * c9)) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(f * c9) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - (f * c9)) * x) + ((f * c9) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - c9) * x) + (c9 * r)) - ((1 - (f * c9)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - c9) * x) + (c9 * r)) - ((1 - (f * c9)) * x)) - ((f * c9) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((1 - c9) * x) - ((1 - (f * c9)) * x) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - c9) * x) - ((1 - (f * c9)) * x)) + (c9 * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - c9) * x) - ((1 - (f * c9)) * x)) + (c9 * r)) - ((f * c9) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(1 - c9) - (1 - (f * c9)) is V14() real ext-real Element of REAL
((1 - c9) - (1 - (f * c9))) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - c9) - (1 - (f * c9))) * x) + (c9 * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - c9) - (1 - (f * c9))) * x) + (c9 * r)) - ((f * c9) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(f * c9) - c9 is V14() real ext-real Element of REAL
((f * c9) - c9) * x is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((f * c9) - c9) * x) - ((f * c9) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((f * c9) - c9) * x) - ((f * c9) * r)) + (c9 * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((f * c9) * r) - (c9 * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((f * c9) - c9) * x) - (((f * c9) * r) - (c9 * r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((f * c9) - c9) * r is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((f * c9) - c9) * x) - (((f * c9) - c9) * r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((f * c9) - c9) * (x - r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((((1 - f) * c9) + f) - c9) * (x - r)) - (((f * c9) - c9) * (x - r)) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
((((1 - f) * c9) + f) - c9) - ((f * c9) - c9) is V14() real ext-real Element of REAL
(((((1 - f) * c9) + f) - c9) - ((f * c9) - c9)) * (x - r) is V45(p) FinSequence-like V146() Element of the carrier of (TOP-REAL p)
(((1 - f) * c9) + f) - (f * c9) is V14() real ext-real Element of REAL
f * (1 - c9) is V14() real ext-real Element of REAL
((1 - f) * c9) + (f * (1 - c9)) 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 #))
c9 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)
c9 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 - b1) * A) + (b1 * x)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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
c9 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)
c9 is Relation-like Function-like set
dom c9 is set
rng c9 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
c9 . f is set
{ b1 where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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
{ b1 where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
c13 is V14() real ext-real Element of REAL
1 - c13 is V14() real ext-real Element of REAL
(1 - c13) * 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)
c13 * 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 - c13) * A) + (c13 * 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)
(c13 * 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 - c13) * A) + ((c13 * 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)
c13 + (- p29) is V14() real ext-real Element of REAL
(c13 + (- 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 - c13) * A) + ((c13 + (- 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)
c13 - p29 is V14() real ext-real Element of REAL
(c13 - 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 - c13) * A) + ((c13 - 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 - c13) is V14() real ext-real Element of REAL
(- (1 - c13)) * 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 - c13)) * 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 - c13)) * A) + (((1 - c13) * A) + ((c13 - 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 - c13)) * A) + ((1 - c13) * 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 - c13)) * A) + ((1 - c13) * A)) + ((c13 - 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 - c13)) + (1 - c13) is V14() real ext-real Element of REAL
((- (1 - c13)) + (1 - c13)) * 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 - c13)) + (1 - c13)) * A) + ((c13 - 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)) + ((c13 - 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)
c13 - 1 is V14() real ext-real Element of REAL
(c13 - 1) + (1 - p29) is V14() real ext-real Element of REAL
((c13 - 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
c13 is V14() real ext-real Element of the carrier of I[01]
f1 . c13 is Element of the carrier of ((TOP-REAL p) | (LSeg (A,x)))
p29 is a_neighborhood of f1 . c13
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 c13
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