:: TOPALG_1 semantic presentation

REAL is V167() V168() V169() V173() set
NAT is V167() V168() V169() V170() V171() V172() V173() Element of bool REAL
bool REAL is set
K543() is non empty strict TopSpace-like V203() pathwise_connected SubSpace of K541()
K541() is non empty strict TopSpace-like V203() TopStruct
the carrier of K543() is non empty V167() V168() V169() set
[:K543(),K543():] is non empty strict TopSpace-like TopStruct
the carrier of [:K543(),K543():] is non empty set
COMPLEX is V167() V173() set
RAT is V167() V168() V169() V170() V173() set
INT is V167() V168() V169() V170() V171() V173() set
[:COMPLEX,COMPLEX:] is complex-valued set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is complex-valued set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is V5( RAT ) complex-valued ext-real-valued real-valued set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is V5( RAT ) complex-valued ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is set
NAT is V167() V168() V169() V170() V171() V172() V173() set
bool NAT is set
bool NAT is set
1 is non empty V21() natural real V30() V31() ext-real positive non negative V167() V168() V169() V170() V171() V172() Element of NAT
[:1,1:] is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
bool [:1,1:] is set
[:[:1,1:],1:] is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is complex-valued ext-real-valued real-valued set
bool [:[:1,1:],REAL:] is set
2 is non empty V21() natural real V30() V31() ext-real positive non negative V167() V168() V169() V170() V171() V172() Element of NAT
[:2,2:] is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
[:[:2,2:],REAL:] is complex-valued ext-real-valued real-valued set
bool [:[:2,2:],REAL:] is set
TOP-REAL 2 is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() pathwise_connected V219() V220() L15()
the carrier of (TOP-REAL 2) is non empty set
{} is empty trivial V167() V168() V169() V170() V171() V172() V173() set
the empty trivial V167() V168() V169() V170() V171() V172() V173() set is empty trivial V167() V168() V169() V170() V171() V172() V173() set
{{},1} is non empty set
I[01] is non empty strict TopSpace-like V203() pathwise_connected TopStruct
the carrier of I[01] is non empty V167() V168() V169() set
RealSpace is strict V203() MetrStruct
[: the carrier of K543(), the carrier of K543():] is complex-valued ext-real-valued real-valued set
bool [: the carrier of K543(), the carrier of K543():] is set
bool the carrier of [:K543(),K543():] is set
K584() is non empty strict multMagma
the carrier of K584() is non empty set
K589() is non empty strict unital Group-like associative commutative V229() V230() V231() V232() V233() V234() multMagma
K590() is non empty strict associative commutative V232() V233() V234() M25(K589())
K591() is non empty strict unital associative commutative V232() V233() V234() V235() M28(K589(),K590())
K593() is non empty strict unital associative commutative multMagma
K594() is non empty strict unital associative commutative V235() M25(K593())
0 is empty trivial V21() natural real V30() V31() ext-real non positive non negative V167() V168() V169() V170() V171() V172() V173() Element of NAT
K1({}) is set
[.0,1.] is compact V167() V168() V169() Element of bool REAL
0[01] is V21() real ext-real Element of the carrier of I[01]
1[01] is V21() real ext-real Element of the carrier of I[01]
bool the carrier of K543() is set
n is set
a is set
[:n,a:] is set
bool [:n,a:] is set
[:a,n:] is set
bool [:a,n:] is set
id n is V1() V4(n) V5(n) total quasi_total Element of bool [:n,n:]
[:n,n:] is set
bool [:n,n:] is set
id a is V1() V4(a) V5(a) total quasi_total Element of bool [:a,a:]
[:a,a:] is set
bool [:a,a:] is set
b is V1() V4(n) V5(a) Function-like quasi_total Element of bool [:n,a:]
P is V1() V4(a) V5(n) Function-like quasi_total Element of bool [:a,n:]
P * b is V1() V4(n) V5(n) Function-like Element of bool [:n,n:]
b * P is V1() V4(a) V5(a) Function-like Element of bool [:a,a:]
bool the carrier of I[01] is set
a is V167() V168() V169() Element of bool the carrier of I[01]
a ` is V167() V168() V169() Element of bool the carrier of I[01]
b is V21() real ext-real Element of the carrier of I[01]
].b,1.] is V167() V168() V169() Element of bool REAL
[.0,b.] is compact V167() V168() V169() Element of bool REAL
the carrier of I[01] \ a is V167() V168() V169() Element of bool the carrier of I[01]
Q is set
y is V21() real ext-real Element of the carrier of I[01]
Q is set
y is V21() real ext-real Element of REAL
a is V167() V168() V169() Element of bool the carrier of I[01]
a ` is V167() V168() V169() Element of bool the carrier of I[01]
b is V21() real ext-real Element of the carrier of I[01]
[.0,b.[ is V167() V168() V169() Element of bool REAL
[.b,1.] is compact V167() V168() V169() Element of bool REAL
the carrier of I[01] \ a is V167() V168() V169() Element of bool the carrier of I[01]
Q is set
y is V21() real ext-real Element of the carrier of I[01]
Q is set
y is V21() real ext-real Element of REAL
n is V167() V168() V169() Element of bool the carrier of I[01]
a is V21() real ext-real Element of the carrier of I[01]
].a,1.] is V167() V168() V169() Element of bool REAL
[.0,a.] is compact V167() V168() V169() Element of bool REAL
P is set
Q is V21() real ext-real Element of REAL
P is V167() V168() V169() Element of bool the carrier of I[01]
n ` is V167() V168() V169() Element of bool the carrier of I[01]
n is V167() V168() V169() Element of bool the carrier of I[01]
a is V21() real ext-real Element of the carrier of I[01]
[.0,a.[ is V167() V168() V169() Element of bool REAL
[.a,1.] is compact V167() V168() V169() Element of bool REAL
P is set
Q is V21() real ext-real Element of REAL
P is V167() V168() V169() Element of bool the carrier of I[01]
n ` is V167() V168() V169() Element of bool the carrier of I[01]
n is V21() real ext-real set
a is V1() Function-like FinSequence-like complex-valued ext-real-valued real-valued set
- a is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
- 1 is V21() real ext-real non positive set
(- 1) * a is V1() Function-like set
n * (- a) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n * a is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
- (n * a) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(- 1) * (n * a) is V1() Function-like set
- 1 is V21() real ext-real non positive Element of REAL
(- 1) * a is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n * ((- 1) * a) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(- 1) * n is V21() real ext-real Element of REAL
((- 1) * n) * a is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
a is V1() Function-like FinSequence-like complex-valued ext-real-valued real-valued set
b is V1() Function-like FinSequence-like complex-valued ext-real-valued real-valued set
a - b is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K398(b) is V1() Function-like complex-valued set
- 1 is V21() real ext-real non positive set
(- 1) * b is V1() Function-like set
K369(a,K398(b)) is V1() Function-like set
n is V21() real ext-real set
n * (a - b) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n * a is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n * b is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(n * a) - (n * b) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K398((n * b)) is V1() Function-like complex-valued set
(- 1) * (n * b) is V1() Function-like set
K369((n * a),K398((n * b))) is V1() Function-like set
n is V21() real ext-real set
a is V21() real ext-real set
n - a is V21() real ext-real set
b is V1() Function-like FinSequence-like complex-valued ext-real-valued real-valued set
(n - a) * b is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n * b is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
a * b is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(n * b) - (a * b) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K398((a * b)) is V1() Function-like complex-valued set
- 1 is V21() real ext-real non positive set
(- 1) * (a * b) is V1() Function-like set
K369((n * b),K398((a * b))) is V1() Function-like set
dom ((n - a) * b) is V167() V168() V169() V170() V171() V172() Element of bool NAT
dom b is V167() V168() V169() V170() V171() V172() Element of bool NAT
dom ((n * b) - (a * b)) is V167() V168() V169() V170() V171() V172() Element of bool NAT
dom (n * b) is V167() V168() V169() V170() V171() V172() Element of bool NAT
dom (a * b) is V167() V168() V169() V170() V171() V172() Element of bool NAT
(dom (n * b)) /\ (dom (a * b)) is V167() V168() V169() V170() V171() V172() Element of bool NAT
P is V21() natural real ext-real set
((n - a) * b) . P is V21() real ext-real set
b . P is V21() real ext-real set
(n - a) * (b . P) is V21() real ext-real set
n * (b . P) is V21() real ext-real set
a * (b . P) is V21() real ext-real set
(n * (b . P)) - (a * (b . P)) is V21() real ext-real set
(a * b) . P is V21() real ext-real set
(n * (b . P)) - ((a * b) . P) is V21() real ext-real set
(n * b) . P is V21() real ext-real set
((n * b) . P) - ((a * b) . P) is V21() real ext-real set
((n * b) - (a * b)) . P is V21() real ext-real set
n is V1() Function-like FinSequence-like complex-valued ext-real-valued real-valued set
a is V1() Function-like FinSequence-like complex-valued ext-real-valued real-valued set
n + a is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
b is V1() Function-like FinSequence-like complex-valued ext-real-valued real-valued set
P is V1() Function-like FinSequence-like complex-valued ext-real-valued real-valued set
b + P is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(n + a) - (b + P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K398((b + P)) is V1() Function-like complex-valued set
- 1 is V21() real ext-real non positive set
(- 1) * (b + P) is V1() Function-like set
K369((n + a),K398((b + P))) is V1() Function-like set
n - b is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K398(b) is V1() Function-like complex-valued set
(- 1) * b is V1() Function-like set
K369(n,K398(b)) is V1() Function-like set
a - P is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K398(P) is V1() Function-like complex-valued set
(- 1) * P is V1() Function-like set
K369(a,K398(P)) is V1() Function-like set
(n - b) + (a - P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
- (b + P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
a + (- (b + P)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n + (a + (- (b + P))) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
- b is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
- P is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(- b) + (- P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
a + ((- b) + (- P)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n + (a + ((- b) + (- P))) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
a + (- P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(- b) + (a + (- P)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n + ((- b) + (a + (- P))) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n + (- b) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(n + (- b)) + (a + (- P)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(n - b) + (a + (- P)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n is V21() real ext-real set
a is V21() natural real ext-real set
REAL a is non empty FinSequence-membered FinSequenceSet of REAL
b is V1() V4( NAT ) V5( REAL ) Function-like V45(a) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL a
n * b is V1() V4( NAT ) V5( REAL ) Function-like V45(a) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL a
|.(n * b).| is V21() real ext-real non negative Element of REAL
|.b.| is V21() real ext-real non negative Element of REAL
abs n is V21() real ext-real Element of REAL
(abs n) * |.b.| is V21() real ext-real Element of REAL
1 * |.b.| is V21() real ext-real non negative Element of REAL
n is V21() natural real ext-real set
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
a is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
|.a.| is V21() real ext-real non negative Element of REAL
b is V21() real ext-real Element of the carrier of I[01]
b * a is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
|.(b * a).| is V21() real ext-real non negative Element of REAL
{ b₁ where b₁ is V21() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
P is V21() real ext-real Element of REAL
n is V21() real ext-real set
a is V21() real ext-real set
n + a is V21() real ext-real set
b is V21() natural real ext-real set
Euclid b is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid b) is non empty set
TOP-REAL b is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL b) is non empty set
P is Element of the carrier of (Euclid b)
Q is Element of the carrier of (Euclid b)
y is Element of the carrier of (Euclid b)
P is Element of the carrier of (Euclid b)
C is Element of the carrier of (Euclid b)
Pa is Element of the carrier of (Euclid b)
dist (P,Q) is V21() real ext-real Element of REAL
dist (y,P) is V21() real ext-real Element of REAL
dist (C,Pa) is V21() real ext-real Element of REAL
Pb is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
Pa is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
Pb is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
p is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
Pb + Pb is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
the addF of (TOP-REAL b) is V1() V4([: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):]) V5( the carrier of (TOP-REAL b)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):], the carrier of (TOP-REAL b):]
[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):] is set
[:[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):], the carrier of (TOP-REAL b):] is set
bool [:[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):], the carrier of (TOP-REAL b):] is set
the addF of (TOP-REAL b) . (Pb,Pb) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
[Pb,Pb] is non empty set
{Pb,Pb} is non empty set
{Pb} is non empty trivial set
{{Pb,Pb},{Pb}} is non empty set
the addF of (TOP-REAL b) . [Pb,Pb] is set
Pb + Pb is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Pa + p is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
the addF of (TOP-REAL b) . (Pa,p) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
[Pa,p] is non empty set
{Pa,p} is non empty set
{Pa} is non empty trivial set
{{Pa,p},{Pa}} is non empty set
the addF of (TOP-REAL b) . [Pa,p] is set
Pa + p is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
REAL b is non empty FinSequence-membered FinSequenceSet of REAL
s is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
t is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
s - t is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
K398(t) is V1() Function-like complex-valued set
- 1 is V21() real ext-real non positive set
(- 1) * t is V1() Function-like set
K369(s,K398(t)) is V1() Function-like set
X1 is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
W is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
X1 - W is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
K398(W) is V1() Function-like complex-valued set
(- 1) * W is V1() Function-like set
K369(X1,K398(W)) is V1() Function-like set
(s - t) + (X1 - W) is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
|.((s - t) + (X1 - W)).| is V21() real ext-real non negative Element of REAL
|.(s - t).| is V21() real ext-real non negative Element of REAL
|.(X1 - W).| is V21() real ext-real non negative Element of REAL
|.(s - t).| + |.(X1 - W).| is V21() real ext-real non negative Element of REAL
(dist (P,Q)) + (dist (y,P)) is V21() real ext-real Element of REAL
b -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
z is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
y is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of b -tuples_on REAL
ez is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of b -tuples_on REAL
y + ez is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of b -tuples_on REAL
ey is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of b -tuples_on REAL
s + X1 is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
(s + X1) - z is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
K398(z) is V1() Function-like complex-valued set
(- 1) * z is V1() Function-like set
K369((s + X1),K398(z)) is V1() Function-like set
z is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of b -tuples_on REAL
z - y is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of b -tuples_on REAL
K398(y) is V1() Function-like complex-valued set
(- 1) * y is V1() Function-like set
K369(z,K398(y)) is V1() Function-like set
j is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of b -tuples_on REAL
j - ez is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of b -tuples_on REAL
K398(ez) is V1() Function-like complex-valued set
(- 1) * ez is V1() Function-like set
K369(j,K398(ez)) is V1() Function-like set
(z - y) + (j - ez) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of b -tuples_on REAL
m is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
m - z is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
K369(m,K398(z)) is V1() Function-like set
|.(m - z).| is V21() real ext-real non negative Element of REAL
n is V21() real ext-real set
abs n is V21() real ext-real Element of REAL
a is V21() real ext-real set
(abs n) * a is V21() real ext-real Element of REAL
b is V21() natural real ext-real set
Euclid b is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid b) is non empty set
TOP-REAL b is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL b) is non empty set
P is Element of the carrier of (Euclid b)
Q is Element of the carrier of (Euclid b)
y is Element of the carrier of (Euclid b)
P is Element of the carrier of (Euclid b)
dist (P,Q) is V21() real ext-real Element of REAL
dist (y,P) is V21() real ext-real Element of REAL
C is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
Pa is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
n * C is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
n * C is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n * Pa is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
n * Pa is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
REAL b is non empty FinSequence-membered FinSequenceSet of REAL
Pb is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
Pa is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
Pb - Pa is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
K398(Pa) is V1() Function-like complex-valued set
- 1 is V21() real ext-real non positive set
(- 1) * Pa is V1() Function-like set
K369(Pb,K398(Pa)) is V1() Function-like set
|.(Pb - Pa).| is V21() real ext-real non negative Element of REAL
Pb is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
p is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
Pb - p is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
K398(p) is V1() Function-like complex-valued set
(- 1) * p is V1() Function-like set
K369(Pb,K398(p)) is V1() Function-like set
|.(Pb - p).| is V21() real ext-real non negative Element of REAL
n * Pb is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
(n * Pb) - p is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
K369((n * Pb),K398(p)) is V1() Function-like set
|.((n * Pb) - p).| is V21() real ext-real non negative Element of REAL
n * Pa is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
(n * Pb) - (n * Pa) is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
K398((n * Pa)) is V1() Function-like complex-valued set
(- 1) * (n * Pa) is V1() Function-like set
K369((n * Pb),K398((n * Pa))) is V1() Function-like set
|.((n * Pb) - (n * Pa)).| is V21() real ext-real non negative Element of REAL
n * (Pb - Pa) is V1() V4( NAT ) V5( REAL ) Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL b
|.(n * (Pb - Pa)).| is V21() real ext-real non negative Element of REAL
(abs n) * |.(Pb - Pa).| is V21() real ext-real Element of REAL
n is V21() real ext-real set
abs n is V21() real ext-real Element of REAL
a is V21() real ext-real set
abs a is V21() real ext-real Element of REAL
b is V21() real ext-real set
(abs n) * b is V21() real ext-real Element of REAL
P is V21() real ext-real set
(abs a) * P is V21() real ext-real Element of REAL
((abs n) * b) + ((abs a) * P) is V21() real ext-real Element of REAL
Q is V21() natural real ext-real set
Euclid Q is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid Q) is non empty set
TOP-REAL Q is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL Q) is non empty set
y is Element of the carrier of (Euclid Q)
P is Element of the carrier of (Euclid Q)
C is Element of the carrier of (Euclid Q)
Pa is Element of the carrier of (Euclid Q)
Pb is Element of the carrier of (Euclid Q)
Pa is Element of the carrier of (Euclid Q)
dist (y,P) is V21() real ext-real Element of REAL
dist (C,Pa) is V21() real ext-real Element of REAL
dist (Pb,Pa) is V21() real ext-real Element of REAL
Pb is V1() Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL Q)
p is V1() Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL Q)
s is V1() Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL Q)
t is V1() Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL Q)
n * Pb is V1() Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL Q)
n * Pb is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
a * s is V1() Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL Q)
a * s is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(n * Pb) + (a * s) is V1() Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL Q)
the addF of (TOP-REAL Q) is V1() V4([: the carrier of (TOP-REAL Q), the carrier of (TOP-REAL Q):]) V5( the carrier of (TOP-REAL Q)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL Q), the carrier of (TOP-REAL Q):], the carrier of (TOP-REAL Q):]
[: the carrier of (TOP-REAL Q), the carrier of (TOP-REAL Q):] is set
[:[: the carrier of (TOP-REAL Q), the carrier of (TOP-REAL Q):], the carrier of (TOP-REAL Q):] is set
bool [:[: the carrier of (TOP-REAL Q), the carrier of (TOP-REAL Q):], the carrier of (TOP-REAL Q):] is set
the addF of (TOP-REAL Q) . ((n * Pb),(a * s)) is V1() Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL Q)
[(n * Pb),(a * s)] is non empty set
{(n * Pb),(a * s)} is non empty set
{(n * Pb)} is non empty trivial set
{{(n * Pb),(a * s)},{(n * Pb)}} is non empty set
the addF of (TOP-REAL Q) . [(n * Pb),(a * s)] is set
(n * Pb) + (a * s) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n * p is V1() Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL Q)
n * p is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
a * t is V1() Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL Q)
a * t is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(n * p) + (a * t) is V1() Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL Q)
the addF of (TOP-REAL Q) . ((n * p),(a * t)) is V1() Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL Q)
[(n * p),(a * t)] is non empty set
{(n * p),(a * t)} is non empty set
{(n * p)} is non empty trivial set
{{(n * p),(a * t)},{(n * p)}} is non empty set
the addF of (TOP-REAL Q) . [(n * p),(a * t)] is set
(n * p) + (a * t) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
REAL Q is non empty FinSequence-membered FinSequenceSet of REAL
W is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
n * W is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
z is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
a * z is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
X1 is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
n * X1 is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
m is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
a * m is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
z is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
(n * X1) + (a * m) is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
m - z is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
K398(z) is V1() Function-like complex-valued set
- 1 is V21() real ext-real non positive set
(- 1) * z is V1() Function-like set
K369(m,K398(z)) is V1() Function-like set
|.(m - z).| is V21() real ext-real non negative Element of REAL
(abs a) * |.(m - z).| is V21() real ext-real Element of REAL
X1 - W is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
K398(W) is V1() Function-like complex-valued set
(- 1) * W is V1() Function-like set
K369(X1,K398(W)) is V1() Function-like set
|.(X1 - W).| is V21() real ext-real non negative Element of REAL
(abs n) * |.(X1 - W).| is V21() real ext-real Element of REAL
((abs n) * |.(X1 - W).|) + ((abs a) * |.(m - z).|) is V21() real ext-real Element of REAL
n * (X1 - W) is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
a * (m - z) is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
(n * (X1 - W)) + (a * (m - z)) is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
|.((n * (X1 - W)) + (a * (m - z))).| is V21() real ext-real non negative Element of REAL
|.(n * (X1 - W)).| is V21() real ext-real non negative Element of REAL
|.(a * (m - z)).| is V21() real ext-real non negative Element of REAL
|.(n * (X1 - W)).| + |.(a * (m - z)).| is V21() real ext-real non negative Element of REAL
|.(n * (X1 - W)).| + ((abs a) * |.(m - z).|) is V21() real ext-real Element of REAL
y is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
z - y is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
K398(y) is V1() Function-like complex-valued set
(- 1) * y is V1() Function-like set
K369(z,K398(y)) is V1() Function-like set
|.(z - y).| is V21() real ext-real non negative Element of REAL
(n * W) + (a * z) is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
((n * X1) + (a * m)) - ((n * W) + (a * z)) is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
K398(((n * W) + (a * z))) is V1() Function-like complex-valued set
(- 1) * ((n * W) + (a * z)) is V1() Function-like set
K369(((n * X1) + (a * m)),K398(((n * W) + (a * z)))) is V1() Function-like set
|.(((n * X1) + (a * m)) - ((n * W) + (a * z))).| is V21() real ext-real non negative Element of REAL
(n * X1) - (n * W) is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
K398((n * W)) is V1() Function-like complex-valued set
(- 1) * (n * W) is V1() Function-like set
K369((n * X1),K398((n * W))) is V1() Function-like set
(a * m) - (a * z) is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
K398((a * z)) is V1() Function-like complex-valued set
(- 1) * (a * z) is V1() Function-like set
K369((a * m),K398((a * z))) is V1() Function-like set
((n * X1) - (n * W)) + ((a * m) - (a * z)) is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
|.(((n * X1) - (n * W)) + ((a * m) - (a * z))).| is V21() real ext-real non negative Element of REAL
(n * (X1 - W)) + ((a * m) - (a * z)) is V1() V4( NAT ) V5( REAL ) Function-like V45(Q) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL Q
|.((n * (X1 - W)) + ((a * m) - (a * z))).| is V21() real ext-real non negative Element of REAL
n is V21() natural real ext-real set
TOP-REAL n is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL n) is non empty set
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
[: the carrier of a, the carrier of (TOP-REAL n):] is set
bool [: the carrier of a, the carrier of (TOP-REAL n):] is set
b is V1() V4( the carrier of a) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of (TOP-REAL n):]
P is V1() V4( the carrier of a) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of (TOP-REAL n):]
Q is V1() V4( the carrier of a) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of (TOP-REAL n):]
y is V1() V4( the carrier of a) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of (TOP-REAL n):]
P is Element of the carrier of a
Q . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
y . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
b . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
P . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(b . P) + (P . P) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) is V1() V4([: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]) V5( the carrier of (TOP-REAL n)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):]
[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is set
[:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
the addF of (TOP-REAL n) . ((b . P),(P . P)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[(b . P),(P . P)] is non empty set
{(b . P),(P . P)} is non empty set
{(b . P)} is non empty trivial set
{{(b . P),(P . P)},{(b . P)}} is non empty set
the addF of (TOP-REAL n) . [(b . P),(P . P)] is set
(b . P) + (P . P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n is V21() real ext-real set
a is V21() natural real ext-real set
TOP-REAL a is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL a) is non empty set
b is non empty TopSpace-like TopStruct
the carrier of b is non empty set
[: the carrier of b, the carrier of (TOP-REAL a):] is set
bool [: the carrier of b, the carrier of (TOP-REAL a):] is set
P is V1() V4( the carrier of b) V5( the carrier of (TOP-REAL a)) Function-like non empty total quasi_total Element of bool [: the carrier of b, the carrier of (TOP-REAL a):]
Q is V1() V4( the carrier of b) V5( the carrier of (TOP-REAL a)) Function-like non empty total quasi_total Element of bool [: the carrier of b, the carrier of (TOP-REAL a):]
bool the carrier of (TOP-REAL a) is set
bool the carrier of b is set
y is Element of the carrier of b
Q . y is V1() Function-like V45(a) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
P is Element of bool the carrier of (TOP-REAL a)
Euclid a is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid a) is non empty set
P . y is V1() Function-like V45(a) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
Int P is open Element of bool the carrier of (TOP-REAL a)
C is Element of the carrier of (Euclid a)
Pb is V21() real ext-real set
Ball (C,Pb) is Element of bool the carrier of (Euclid a)
bool the carrier of (Euclid a) is set
Pa is Element of the carrier of (Euclid a)
abs n is V21() real ext-real Element of REAL
Pb / (abs n) is V21() real ext-real Element of REAL
Ball (Pa,(Pb / (abs n))) is Element of bool the carrier of (Euclid a)
Pa is Element of bool the carrier of (TOP-REAL a)
Pb is Element of bool the carrier of b
P .: Pb is Element of bool the carrier of (TOP-REAL a)
Q .: Pb is Element of bool the carrier of (TOP-REAL a)
p is set
dom Q is Element of bool the carrier of b
s is set
Q . s is set
t is Element of the carrier of b
P . t is V1() Function-like V45(a) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
n * (P . t) is V1() Function-like V45(a) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
n * (P . t) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom P is Element of bool the carrier of b
W is Element of the carrier of (Euclid a)
dist (Pa,W) is V21() real ext-real Element of REAL
n * (P . y) is V1() Function-like V45(a) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
n * (P . y) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(abs n) * (Pb / (abs n)) is V21() real ext-real Element of REAL
X1 is Element of the carrier of (Euclid a)
dist (C,X1) is V21() real ext-real Element of REAL
n * (P . y) is V1() Function-like V45(a) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
n * (P . y) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
0. (TOP-REAL a) is V1() Function-like V45(a) V54( TOP-REAL a) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
the ZeroF of (TOP-REAL a) is V1() Function-like V45(a) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
[#] b is non empty non proper open closed dense non boundary Element of bool the carrier of b
Pb is non empty non proper open closed dense non boundary Element of bool the carrier of b
Q .: Pb is Element of bool the carrier of (TOP-REAL a)
p is set
dom Q is Element of bool the carrier of b
s is set
Q . s is set
t is Element of the carrier of b
P . t is V1() Function-like V45(a) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
n * (P . t) is V1() Function-like V45(a) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL a)
n * (P . t) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n is V21() real ext-real set
a is V21() real ext-real set
b is V21() natural real ext-real set
TOP-REAL b is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL b) is non empty set
P is non empty TopSpace-like TopStruct
the carrier of P is non empty set
[: the carrier of P, the carrier of (TOP-REAL b):] is set
bool [: the carrier of P, the carrier of (TOP-REAL b):] is set
Q is V1() V4( the carrier of P) V5( the carrier of (TOP-REAL b)) Function-like non empty total quasi_total Element of bool [: the carrier of P, the carrier of (TOP-REAL b):]
y is V1() V4( the carrier of P) V5( the carrier of (TOP-REAL b)) Function-like non empty total quasi_total Element of bool [: the carrier of P, the carrier of (TOP-REAL b):]
P is V1() V4( the carrier of P) V5( the carrier of (TOP-REAL b)) Function-like non empty total quasi_total Element of bool [: the carrier of P, the carrier of (TOP-REAL b):]
bool the carrier of (TOP-REAL b) is set
bool the carrier of P is set
C is Element of the carrier of P
P . C is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
Pa is Element of bool the carrier of (TOP-REAL b)
Euclid b is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid b) is non empty set
Int Pa is open Element of bool the carrier of (TOP-REAL b)
Pb is Element of the carrier of (Euclid b)
Pa is V21() real ext-real set
Ball (Pb,Pa) is Element of bool the carrier of (Euclid b)
bool the carrier of (Euclid b) is set
Pa / 2 is V21() real ext-real Element of REAL
y . C is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
Pb is Element of the carrier of (Euclid b)
abs a is V21() real ext-real Element of REAL
(Pa / 2) / (abs a) is V21() real ext-real Element of REAL
Ball (Pb,((Pa / 2) / (abs a))) is Element of bool the carrier of (Euclid b)
p is Element of bool the carrier of (TOP-REAL b)
Q . C is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
s is Element of the carrier of (Euclid b)
abs n is V21() real ext-real Element of REAL
(Pa / 2) / (abs n) is V21() real ext-real Element of REAL
Ball (s,((Pa / 2) / (abs n))) is Element of bool the carrier of (Euclid b)
t is Element of bool the carrier of (TOP-REAL b)
X1 is Element of bool the carrier of P
y .: X1 is Element of bool the carrier of (TOP-REAL b)
W is Element of bool the carrier of P
Q .: W is Element of bool the carrier of (TOP-REAL b)
W /\ X1 is Element of bool the carrier of P
m is Element of bool the carrier of P
P .: m is Element of bool the carrier of (TOP-REAL b)
z is set
dom P is Element of bool the carrier of P
z is set
P . z is set
y is Element of the carrier of P
y . y is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
Q . y is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
dom y is Element of bool the carrier of P
j is Element of the carrier of (Euclid b)
dist (Pb,j) is V21() real ext-real Element of REAL
dom Q is Element of bool the carrier of P
ez is Element of the carrier of (Euclid b)
dist (s,ez) is V21() real ext-real Element of REAL
n * (Q . y) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
n * (Q . y) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
a * (y . y) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
a * (y . y) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(n * (Q . y)) + (a * (y . y)) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
the addF of (TOP-REAL b) is V1() V4([: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):]) V5( the carrier of (TOP-REAL b)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):], the carrier of (TOP-REAL b):]
[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):] is set
[:[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):], the carrier of (TOP-REAL b):] is set
bool [:[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):], the carrier of (TOP-REAL b):] is set
the addF of (TOP-REAL b) . ((n * (Q . y)),(a * (y . y))) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
[(n * (Q . y)),(a * (y . y))] is non empty set
{(n * (Q . y)),(a * (y . y))} is non empty set
{(n * (Q . y))} is non empty trivial set
{{(n * (Q . y)),(a * (y . y))},{(n * (Q . y))}} is non empty set
the addF of (TOP-REAL b) . [(n * (Q . y)),(a * (y . y))] is set
(n * (Q . y)) + (a * (y . y)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n * (Q . C) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
n * (Q . C) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
a * (y . C) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
a * (y . C) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(n * (Q . C)) + (a * (y . C)) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
the addF of (TOP-REAL b) . ((n * (Q . C)),(a * (y . C))) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
[(n * (Q . C)),(a * (y . C))] is non empty set
{(n * (Q . C)),(a * (y . C))} is non empty set
{(n * (Q . C))} is non empty trivial set
{{(n * (Q . C)),(a * (y . C))},{(n * (Q . C))}} is non empty set
the addF of (TOP-REAL b) . [(n * (Q . C)),(a * (y . C))] is set
(n * (Q . C)) + (a * (y . C)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(abs n) * ((Pa / 2) / (abs n)) is V21() real ext-real Element of REAL
(abs a) * ((Pa / 2) / (abs a)) is V21() real ext-real Element of REAL
((abs n) * ((Pa / 2) / (abs n))) + ((abs a) * ((Pa / 2) / (abs a))) is V21() real ext-real Element of REAL
ey is Element of the carrier of (Euclid b)
dist (Pb,ey) is V21() real ext-real Element of REAL
Pa / (abs n) is V21() real ext-real Element of REAL
(Pa / (abs n)) / 2 is V21() real ext-real Element of REAL
(abs n) * ((Pa / (abs n)) / 2) is V21() real ext-real Element of REAL
((abs n) * ((Pa / (abs n)) / 2)) + ((abs a) * ((Pa / 2) / (abs a))) is V21() real ext-real Element of REAL
Pa / (abs a) is V21() real ext-real Element of REAL
(Pa / (abs a)) / 2 is V21() real ext-real Element of REAL
(abs a) * ((Pa / (abs a)) / 2) is V21() real ext-real Element of REAL
((abs n) * ((Pa / (abs n)) / 2)) + ((abs a) * ((Pa / (abs a)) / 2)) is V21() real ext-real Element of REAL
(Pa / 2) + ((abs a) * ((Pa / (abs a)) / 2)) is V21() real ext-real Element of REAL
(Pa / 2) + (Pa / 2) is V21() real ext-real Element of REAL
C is Element of the carrier of P
P . C is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
y . C is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
a * (y . C) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
a * (y . C) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Q . C is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
n * (Q . C) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
n * (Q . C) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(n * (Q . C)) + (a * (y . C)) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
the addF of (TOP-REAL b) is V1() V4([: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):]) V5( the carrier of (TOP-REAL b)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):], the carrier of (TOP-REAL b):]
[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):] is set
[:[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):], the carrier of (TOP-REAL b):] is set
bool [:[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):], the carrier of (TOP-REAL b):] is set
the addF of (TOP-REAL b) . ((n * (Q . C)),(a * (y . C))) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
[(n * (Q . C)),(a * (y . C))] is non empty set
{(n * (Q . C)),(a * (y . C))} is non empty set
{(n * (Q . C))} is non empty trivial set
{{(n * (Q . C)),(a * (y . C))},{(n * (Q . C))}} is non empty set
the addF of (TOP-REAL b) . [(n * (Q . C)),(a * (y . C))] is set
(n * (Q . C)) + (a * (y . C)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
0. (TOP-REAL b) is V1() Function-like V45(b) V54( TOP-REAL b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
the ZeroF of (TOP-REAL b) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
(0. (TOP-REAL b)) + (a * (y . C)) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
the addF of (TOP-REAL b) . ((0. (TOP-REAL b)),(a * (y . C))) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
[(0. (TOP-REAL b)),(a * (y . C))] is non empty set
{(0. (TOP-REAL b)),(a * (y . C))} is non empty set
{(0. (TOP-REAL b))} is non empty trivial set
{{(0. (TOP-REAL b)),(a * (y . C))},{(0. (TOP-REAL b))}} is non empty set
the addF of (TOP-REAL b) . [(0. (TOP-REAL b)),(a * (y . C))] is set
(0. (TOP-REAL b)) + (a * (y . C)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
C is Element of the carrier of P
P . C is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
Q . C is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
n * (Q . C) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
n * (Q . C) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
y . C is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
a * (y . C) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
a * (y . C) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(n * (Q . C)) + (a * (y . C)) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
the addF of (TOP-REAL b) is V1() V4([: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):]) V5( the carrier of (TOP-REAL b)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):], the carrier of (TOP-REAL b):]
[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):] is set
[:[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):], the carrier of (TOP-REAL b):] is set
bool [:[: the carrier of (TOP-REAL b), the carrier of (TOP-REAL b):], the carrier of (TOP-REAL b):] is set
the addF of (TOP-REAL b) . ((n * (Q . C)),(a * (y . C))) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
[(n * (Q . C)),(a * (y . C))] is non empty set
{(n * (Q . C)),(a * (y . C))} is non empty set
{(n * (Q . C))} is non empty trivial set
{{(n * (Q . C)),(a * (y . C))},{(n * (Q . C))}} is non empty set
the addF of (TOP-REAL b) . [(n * (Q . C)),(a * (y . C))] is set
(n * (Q . C)) + (a * (y . C)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
0. (TOP-REAL b) is V1() Function-like V45(b) V54( TOP-REAL b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
the ZeroF of (TOP-REAL b) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
(n * (Q . C)) + (0. (TOP-REAL b)) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
the addF of (TOP-REAL b) . ((n * (Q . C)),(0. (TOP-REAL b))) is V1() Function-like V45(b) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL b)
[(n * (Q . C)),(0. (TOP-REAL b))] is non empty set
{(n * (Q . C)),(0. (TOP-REAL b))} is non empty set
{{(n * (Q . C)),(0. (TOP-REAL b))},{(n * (Q . C))}} is non empty set
the addF of (TOP-REAL b) . [(n * (Q . C)),(0. (TOP-REAL b))] is set
(n * (Q . C)) + (0. (TOP-REAL b)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n is V21() natural real ext-real set
TOP-REAL n is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
[:(TOP-REAL n),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(TOP-REAL n),I[01]:] is non empty set
the carrier of (TOP-REAL n) is non empty set
[: the carrier of [:(TOP-REAL n),I[01]:], the carrier of (TOP-REAL n):] is set
bool [: the carrier of [:(TOP-REAL n),I[01]:], the carrier of (TOP-REAL n):] is set
b is V1() V4( the carrier of [:(TOP-REAL n),I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:(TOP-REAL n),I[01]:], the carrier of (TOP-REAL n):]
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
[#] I[01] is non empty non proper open closed dense non boundary V167() V168() V169() Element of bool the carrier of I[01]
bool the carrier of (TOP-REAL n) is set
bool the carrier of [:(TOP-REAL n),I[01]:] is set
P is Element of the carrier of [:(TOP-REAL n),I[01]:]
b . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
Q is Element of bool the carrier of (TOP-REAL n)
Euclid n is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid n) is non empty set
P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C is V21() real ext-real Element of the carrier of I[01]
[P,C] is non empty Element of the carrier of [:(TOP-REAL n),I[01]:]
{P,C} is non empty set
{P} is non empty trivial set
{{P,C},{P}} is non empty set
y is Element of the carrier of (Euclid n)
b . (P,C) is set
[P,C] is non empty set
b . [P,C] is set
1 - C is V21() real ext-real Element of REAL
(1 - C) * P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(1 - C) * P is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Int Q is open Element of bool the carrier of (TOP-REAL n)
Pa is V21() real ext-real set
Ball (y,Pa) is Element of bool the carrier of (Euclid n)
bool the carrier of (Euclid n) is set
Pa / 2 is V21() real ext-real Element of REAL
- (1 - C) is V21() real ext-real Element of REAL
- (- (1 - C)) is V21() real ext-real Element of REAL
- 0 is empty trivial V21() real ext-real non positive non negative V167() V168() V169() V170() V171() V172() V173() Element of REAL
C - 1 is V21() real ext-real Element of REAL
2 * (1 - C) is V21() real ext-real Element of REAL
Pa is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
|.Pa.| is V21() real ext-real non negative Element of REAL
(2 * (1 - C)) * |.Pa.| is V21() real ext-real Element of REAL
(C - 1) * ((2 * (1 - C)) * |.Pa.|) is V21() real ext-real Element of REAL
((2 * (1 - C)) * |.Pa.|) + Pa is V21() real ext-real Element of REAL
(1 - C) * Pa is V21() real ext-real Element of REAL
((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
C + (((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa)) is V21() real ext-real Element of REAL
C * (((2 * (1 - C)) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
(C * (((2 * (1 - C)) * |.Pa.|) + Pa)) / (((2 * (1 - C)) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
((C * (((2 * (1 - C)) * |.Pa.|) + Pa)) / (((2 * (1 - C)) * |.Pa.|) + Pa)) + (((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa)) is V21() real ext-real Element of REAL
(C * (((2 * (1 - C)) * |.Pa.|) + Pa)) + ((1 - C) * Pa) is V21() real ext-real Element of REAL
((C * (((2 * (1 - C)) * |.Pa.|) + Pa)) + ((1 - C) * Pa)) / (((2 * (1 - C)) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
C * 2 is V21() real ext-real Element of REAL
(C * 2) * (1 - C) is V21() real ext-real Element of REAL
((C * 2) * (1 - C)) * |.Pa.| is V21() real ext-real Element of REAL
(((C * 2) * (1 - C)) * |.Pa.|) + Pa is V21() real ext-real Element of REAL
((((C * 2) * (1 - C)) * |.Pa.|) + Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
(C + (((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa))) - 1 is V21() real ext-real Element of REAL
(((2 * (1 - C)) * |.Pa.|) + Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
(((((C * 2) * (1 - C)) * |.Pa.|) + Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa)) - ((((2 * (1 - C)) * |.Pa.|) + Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa)) is V21() real ext-real Element of REAL
((((C * 2) * (1 - C)) * |.Pa.|) + Pa) - (((2 * (1 - C)) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
(((((C * 2) * (1 - C)) * |.Pa.|) + Pa) - (((2 * (1 - C)) * |.Pa.|) + Pa)) / (((2 * (1 - C)) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
((C + (((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa))) - 1) + 1 is V21() real ext-real Element of REAL
0 + 1 is non empty V21() real ext-real positive non negative Element of REAL
C - (((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa)) is V21() real ext-real Element of REAL
].(C - (((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa))),(C + (((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa))).[ is V167() V168() V169() Element of bool REAL
].(C - (((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa))),(C + (((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa))).[ /\ the carrier of I[01] is V167() V168() V169() Element of bool REAL
Pb is Element of the carrier of (Euclid n)
(Pa / 2) / (1 - C) is V21() real ext-real Element of REAL
Ball (Pb,((Pa / 2) / (1 - C))) is Element of bool the carrier of (Euclid n)
W is Element of bool the carrier of (TOP-REAL n)
X1 is V167() V168() V169() Element of bool the carrier of I[01]
[:W,X1:] is complex-valued ext-real-valued real-valued Element of bool the carrier of [:(TOP-REAL n),I[01]:]
m is complex-valued ext-real-valued real-valued Element of bool the carrier of [:(TOP-REAL n),I[01]:]
b .: m is Element of bool the carrier of (TOP-REAL n)
C - C is V21() real ext-real set
abs (C - C) is V21() real ext-real Element of REAL
z is set
z is V21() real ext-real Element of REAL
z is V167() V168() V169() Element of bool the carrier of I[01]
z is V167() V168() V169() Element of bool the carrier of I[01]
{} I[01] is empty trivial open closed boundary nowhere_dense V167() V168() V169() V170() V171() V172() V173() Element of bool the carrier of I[01]
z is V167() V168() V169() Element of bool the carrier of I[01]
z is V167() V168() V169() Element of bool the carrier of I[01]
[.0,(C + (((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa))).[ is V167() V168() V169() Element of bool REAL
z is set
z is V21() real ext-real Element of REAL
z is set
z is V21() real ext-real Element of REAL
z is set
dom b is Element of bool the carrier of [:(TOP-REAL n),I[01]:]
z is set
b . z is set
y is Element of the carrier of [:(TOP-REAL n),I[01]:]
j is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
ez is V21() real ext-real Element of the carrier of I[01]
[j,ez] is non empty Element of the carrier of [:(TOP-REAL n),I[01]:]
{j,ez} is non empty set
{j} is non empty trivial set
{{j,ez},{j}} is non empty set
b . y is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
ey is Element of the carrier of (Euclid n)
(1 - C) * j is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(1 - C) * j is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Pa / (1 - C) is V21() real ext-real Element of REAL
(Pa / (1 - C)) / 2 is V21() real ext-real Element of REAL
(1 - C) * ((Pa / (1 - C)) / 2) is V21() real ext-real Element of REAL
fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
fp is Element of the carrier of (Euclid n)
dist (Pb,fp) is V21() real ext-real Element of REAL
ez - C is V21() real ext-real set
abs (ez - C) is V21() real ext-real Element of REAL
C - ez is V21() real ext-real set
abs (C - ez) is V21() real ext-real Element of REAL
|.fy.| is V21() real ext-real non negative Element of REAL
(abs (C - ez)) * |.fy.| is V21() real ext-real Element of REAL
(((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa)) * |.fy.| is V21() real ext-real Element of REAL
b . (j,ez) is set
[j,ez] is non empty set
b . [j,ez] is set
1 - ez is V21() real ext-real Element of REAL
(1 - ez) * j is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(1 - ez) * j is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
fe is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
fe - fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(fy) is V1() Function-like complex-valued set
- 1 is V21() real ext-real non positive set
(- 1) * fy is V1() Function-like set
K369(fe,K398(fy)) is V1() Function-like set
yy is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
(1 - C) * yy is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
(1 - ez) * yy is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
((1 - C) * yy) - ((1 - ez) * yy) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K398(((1 - ez) * yy)) is V1() Function-like complex-valued set
(- 1) * ((1 - ez) * yy) is V1() Function-like set
K369(((1 - C) * yy),K398(((1 - ez) * yy))) is V1() Function-like set
|.(fe - fy).| is V21() real ext-real non negative Element of REAL
(1 - C) - (1 - ez) is V21() real ext-real Element of REAL
((1 - C) - (1 - ez)) * fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
|.(((1 - C) - (1 - ez)) * fy).| is V21() real ext-real non negative Element of REAL
(abs (ez - C)) * |.fy.| is V21() real ext-real Element of REAL
dist (y,ey) is V21() real ext-real Element of REAL
fz is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
fz - fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K369(fz,K398(fy)) is V1() Function-like set
|.(fz - fy).| is V21() real ext-real non negative Element of REAL
fz - fe is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(fe) is V1() Function-like complex-valued set
(- 1) * fe is V1() Function-like set
K369(fz,K398(fe)) is V1() Function-like set
|.(fz - fe).| is V21() real ext-real non negative Element of REAL
|.(fz - fe).| + |.(fe - fy).| is V21() real ext-real non negative Element of REAL
Pa - fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(fy) is V1() Function-like complex-valued set
(- 1) * fy is V1() Function-like set
K369(Pa,K398(fy)) is V1() Function-like set
(1 - C) * (Pa - fy) is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
yy is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
gy is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
yy - gy is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K398(gy) is V1() Function-like complex-valued set
(- 1) * gy is V1() Function-like set
K369(yy,K398(gy)) is V1() Function-like set
(1 - C) * (yy - gy) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
(1 - C) * yy is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
(1 - C) * gy is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
((1 - C) * yy) - ((1 - C) * gy) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K398(((1 - C) * gy)) is V1() Function-like complex-valued set
(- 1) * ((1 - C) * gy) is V1() Function-like set
K369(((1 - C) * yy),K398(((1 - C) * gy))) is V1() Function-like set
(1 - C) * Pa is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
(1 - C) * fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
((1 - C) * Pa) - ((1 - C) * fy) is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(((1 - C) * fy)) is V1() Function-like complex-valued set
(- 1) * ((1 - C) * fy) is V1() Function-like set
K369(((1 - C) * Pa),K398(((1 - C) * fy))) is V1() Function-like set
((1 - C) * Pa) - fe is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K369(((1 - C) * Pa),K398(fe)) is V1() Function-like set
|.(Pa - fy).| is V21() real ext-real non negative Element of REAL
(1 - C) * ((Pa / 2) / (1 - C)) is V21() real ext-real Element of REAL
(1 - C) * |.(Pa - fy).| is V21() real ext-real Element of REAL
abs (1 - C) is V21() real ext-real Element of REAL
(abs (1 - C)) * |.(Pa - fy).| is V21() real ext-real Element of REAL
|.(((1 - C) * Pa) - fe).| is V21() real ext-real non negative Element of REAL
fy - Pa is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(Pa) is V1() Function-like complex-valued set
(- 1) * Pa is V1() Function-like set
K369(fy,K398(Pa)) is V1() Function-like set
|.(fy - Pa).| is V21() real ext-real non negative Element of REAL
|.fy.| - |.Pa.| is V21() real ext-real Element of REAL
|.Pa.| + ((Pa / 2) / (1 - C)) is V21() real ext-real Element of REAL
(((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa)) * (|.Pa.| + ((Pa / 2) / (1 - C))) is V21() real ext-real Element of REAL
Pa / (2 * (1 - C)) is V21() real ext-real Element of REAL
|.Pa.| + (Pa / (2 * (1 - C))) is V21() real ext-real Element of REAL
(((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa)) * (|.Pa.| + (Pa / (2 * (1 - C)))) is V21() real ext-real Element of REAL
|.Pa.| * (2 * (1 - C)) is V21() real ext-real Element of REAL
(|.Pa.| * (2 * (1 - C))) / (2 * (1 - C)) is V21() real ext-real Element of REAL
((|.Pa.| * (2 * (1 - C))) / (2 * (1 - C))) + (Pa / (2 * (1 - C))) is V21() real ext-real Element of REAL
(((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa)) * (((|.Pa.| * (2 * (1 - C))) / (2 * (1 - C))) + (Pa / (2 * (1 - C)))) is V21() real ext-real Element of REAL
(|.Pa.| * (2 * (1 - C))) + Pa is V21() real ext-real Element of REAL
((|.Pa.| * (2 * (1 - C))) + Pa) / (2 * (1 - C)) is V21() real ext-real Element of REAL
(((1 - C) * Pa) / (((2 * (1 - C)) * |.Pa.|) + Pa)) * (((|.Pa.| * (2 * (1 - C))) + Pa) / (2 * (1 - C))) is V21() real ext-real Element of REAL
((1 - C) * Pa) / (2 * (1 - C)) is V21() real ext-real Element of REAL
(Pa / 2) + (Pa / 2) is V21() real ext-real Element of REAL
(1 - C) + C is V21() real ext-real Element of REAL
0 + C is V21() real ext-real Element of REAL
Pa is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
|.Pa.| is V21() real ext-real non negative Element of REAL
|.Pa.| + Pa is V21() real ext-real Element of REAL
Pb is Element of the carrier of (Euclid n)
Ball (Pb,Pa) is Element of bool the carrier of (Euclid n)
Pa / (|.Pa.| + Pa) is V21() real ext-real Element of REAL
1 - (Pa / (|.Pa.| + Pa)) is V21() real ext-real Element of REAL
].(1 - (Pa / (|.Pa.| + Pa))),1.] is V167() V168() V169() Element of bool REAL
p is Element of bool the carrier of (TOP-REAL n)
0 + Pa is V21() real ext-real Element of REAL
(Pa / (|.Pa.| + Pa)) - (Pa / (|.Pa.| + Pa)) is V21() real ext-real Element of REAL
X1 is set
W is V21() real ext-real Element of REAL
X1 is V167() V168() V169() Element of bool the carrier of I[01]
[:p,X1:] is complex-valued ext-real-valued real-valued Element of bool the carrier of [:(TOP-REAL n),I[01]:]
W is complex-valued ext-real-valued real-valued Element of bool the carrier of [:(TOP-REAL n),I[01]:]
b .: W is Element of bool the carrier of (TOP-REAL n)
1 - 0 is non empty V21() real ext-real positive non negative Element of REAL
m is set
dom b is Element of bool the carrier of [:(TOP-REAL n),I[01]:]
z is set
b . z is set
z is Element of the carrier of [:(TOP-REAL n),I[01]:]
y is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
j is V21() real ext-real Element of the carrier of I[01]
[y,j] is non empty Element of the carrier of [:(TOP-REAL n),I[01]:]
{y,j} is non empty set
{y} is non empty trivial set
{{y,j},{y}} is non empty set
b . z is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
ez is Element of the carrier of (Euclid n)
fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
ey is Element of the carrier of (Euclid n)
dist (Pb,ey) is V21() real ext-real Element of REAL
b . (y,j) is set
[y,j] is non empty set
b . [y,j] is set
1 - j is V21() real ext-real Element of REAL
(1 - j) * y is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(1 - j) * y is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
fp is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
0. (TOP-REAL n) is V1() Function-like V45(n) V54( TOP-REAL n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
fz is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
fz - fp is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(fp) is V1() Function-like complex-valued set
- 1 is V21() real ext-real non positive set
(- 1) * fp is V1() Function-like set
K369(fz,K398(fp)) is V1() Function-like set
(b . z) - (0. (TOP-REAL n)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
- (0. (TOP-REAL n)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
- (0. (TOP-REAL n)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(- 1) * (0. (TOP-REAL n)) is V1() Function-like set
(b . z) + (- (0. (TOP-REAL n))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) is V1() V4([: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]) V5( the carrier of (TOP-REAL n)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):]
[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is set
[:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
the addF of (TOP-REAL n) . ((b . z),(- (0. (TOP-REAL n)))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[(b . z),(- (0. (TOP-REAL n)))] is non empty set
{(b . z),(- (0. (TOP-REAL n)))} is non empty set
{(b . z)} is non empty trivial set
{{(b . z),(- (0. (TOP-REAL n)))},{(b . z)}} is non empty set
the addF of (TOP-REAL n) . [(b . z),(- (0. (TOP-REAL n)))] is set
(b . z) + (- (0. (TOP-REAL n))) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(b . z) - (0. (TOP-REAL n)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K398((0. (TOP-REAL n))) is V1() Function-like complex-valued set
K369((b . z),K398((0. (TOP-REAL n)))) is V1() Function-like set
|.fy.| is V21() real ext-real non negative Element of REAL
|.fy.| - |.Pa.| is V21() real ext-real Element of REAL
fy - Pa is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(Pa) is V1() Function-like complex-valued set
(- 1) * Pa is V1() Function-like set
K369(fy,K398(Pa)) is V1() Function-like set
|.(fy - Pa).| is V21() real ext-real non negative Element of REAL
Pa - fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(fy) is V1() Function-like complex-valued set
(- 1) * fy is V1() Function-like set
K369(Pa,K398(fy)) is V1() Function-like set
|.(Pa - fy).| is V21() real ext-real non negative Element of REAL
j - j is V21() real ext-real set
j + (Pa / (|.Pa.| + Pa)) is V21() real ext-real Element of REAL
(1 - (Pa / (|.Pa.| + Pa))) + (Pa / (|.Pa.| + Pa)) is V21() real ext-real Element of REAL
(j + (Pa / (|.Pa.| + Pa))) - j is V21() real ext-real Element of REAL
Pa / (1 - j) is V21() real ext-real Element of REAL
Pa / (Pa / (|.Pa.| + Pa)) is V21() real ext-real Element of REAL
(1 - j) * (Pa / (1 - j)) is V21() real ext-real Element of REAL
(1 - j) * |.fy.| is V21() real ext-real Element of REAL
(1 - j) * |.fy.| is V21() real ext-real Element of REAL
(1 - j) * |.fy.| is V21() real ext-real Element of REAL
(1 - j) * |.fy.| is V21() real ext-real Element of REAL
dist (y,ez) is V21() real ext-real Element of REAL
|.(fz - fp).| is V21() real ext-real non negative Element of REAL
|.fz.| is V21() real ext-real non negative Element of REAL
(1 - j) * fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
|.((1 - j) * fy).| is V21() real ext-real non negative Element of REAL
abs (1 - j) is V21() real ext-real Element of REAL
(abs (1 - j)) * |.fy.| is V21() real ext-real Element of REAL
n is V21() natural real ext-real set
TOP-REAL n is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
[:(TOP-REAL n),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(TOP-REAL n),I[01]:] is non empty set
the carrier of (TOP-REAL n) is non empty set
[: the carrier of [:(TOP-REAL n),I[01]:], the carrier of (TOP-REAL n):] is set
bool [: the carrier of [:(TOP-REAL n),I[01]:], the carrier of (TOP-REAL n):] is set
b is V1() V4( the carrier of [:(TOP-REAL n),I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:(TOP-REAL n),I[01]:], the carrier of (TOP-REAL n):]
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
[#] I[01] is non empty non proper open closed dense non boundary V167() V168() V169() Element of bool the carrier of I[01]
bool the carrier of (TOP-REAL n) is set
bool the carrier of [:(TOP-REAL n),I[01]:] is set
P is Element of the carrier of [:(TOP-REAL n),I[01]:]
b . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
Q is Element of bool the carrier of (TOP-REAL n)
Euclid n is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid n) is non empty set
P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C is V21() real ext-real Element of the carrier of I[01]
[P,C] is non empty Element of the carrier of [:(TOP-REAL n),I[01]:]
{P,C} is non empty set
{P} is non empty trivial set
{{P,C},{P}} is non empty set
y is Element of the carrier of (Euclid n)
b . (P,C) is set
[P,C] is non empty set
b . [P,C] is set
C * P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C * P is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Int Q is open Element of bool the carrier of (TOP-REAL n)
Pa is V21() real ext-real set
Ball (y,Pa) is Element of bool the carrier of (Euclid n)
bool the carrier of (Euclid n) is set
Pa / 2 is V21() real ext-real Element of REAL
2 * C is V21() real ext-real Element of REAL
Pa is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
|.Pa.| is V21() real ext-real non negative Element of REAL
(2 * C) * |.Pa.| is V21() real ext-real Element of REAL
((2 * C) * |.Pa.|) + Pa is V21() real ext-real Element of REAL
C * Pa is V21() real ext-real set
(C * Pa) / (((2 * C) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
C - 1 is V21() real ext-real Element of REAL
1 - 1 is V21() real ext-real Element of REAL
((2 * C) * |.Pa.|) * (C - 1) is V21() real ext-real Element of REAL
Pa - Pa is V21() real ext-real set
C * ((2 * C) * |.Pa.|) is V21() real ext-real Element of REAL
(C * ((2 * C) * |.Pa.|)) - ((2 * C) * |.Pa.|) is V21() real ext-real Element of REAL
((C * ((2 * C) * |.Pa.|)) - ((2 * C) * |.Pa.|)) - Pa is V21() real ext-real Element of REAL
C - ((C * Pa) / (((2 * C) * |.Pa.|) + Pa)) is V21() real ext-real Element of REAL
C * (((2 * C) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
(C * (((2 * C) * |.Pa.|) + Pa)) / (((2 * C) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
((C * (((2 * C) * |.Pa.|) + Pa)) / (((2 * C) * |.Pa.|) + Pa)) - ((C * Pa) / (((2 * C) * |.Pa.|) + Pa)) is V21() real ext-real Element of REAL
(C * (((2 * C) * |.Pa.|) + Pa)) - (C * Pa) is V21() real ext-real Element of REAL
((C * (((2 * C) * |.Pa.|) + Pa)) - (C * Pa)) / (((2 * C) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
(C * ((2 * C) * |.Pa.|)) / (((2 * C) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
(C - ((C * Pa) / (((2 * C) * |.Pa.|) + Pa))) - 1 is V21() real ext-real Element of REAL
(((2 * C) * |.Pa.|) + Pa) / (((2 * C) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
((C * ((2 * C) * |.Pa.|)) / (((2 * C) * |.Pa.|) + Pa)) - ((((2 * C) * |.Pa.|) + Pa) / (((2 * C) * |.Pa.|) + Pa)) is V21() real ext-real Element of REAL
(C * ((2 * C) * |.Pa.|)) - (((2 * C) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
((C * ((2 * C) * |.Pa.|)) - (((2 * C) * |.Pa.|) + Pa)) / (((2 * C) * |.Pa.|) + Pa) is V21() real ext-real Element of REAL
0 + 1 is non empty V21() real ext-real positive non negative Element of REAL
((C - ((C * Pa) / (((2 * C) * |.Pa.|) + Pa))) - 1) + 1 is V21() real ext-real Element of REAL
C + ((C * Pa) / (((2 * C) * |.Pa.|) + Pa)) is V21() real ext-real Element of REAL
].(C - ((C * Pa) / (((2 * C) * |.Pa.|) + Pa))),(C + ((C * Pa) / (((2 * C) * |.Pa.|) + Pa))).[ is V167() V168() V169() Element of bool REAL
].(C - ((C * Pa) / (((2 * C) * |.Pa.|) + Pa))),(C + ((C * Pa) / (((2 * C) * |.Pa.|) + Pa))).[ /\ the carrier of I[01] is V167() V168() V169() Element of bool REAL
Pb is Element of the carrier of (Euclid n)
(Pa / 2) / C is V21() real ext-real Element of REAL
Ball (Pb,((Pa / 2) / C)) is Element of bool the carrier of (Euclid n)
W is Element of bool the carrier of (TOP-REAL n)
X1 is V167() V168() V169() Element of bool the carrier of I[01]
[:W,X1:] is complex-valued ext-real-valued real-valued Element of bool the carrier of [:(TOP-REAL n),I[01]:]
m is complex-valued ext-real-valued real-valued Element of bool the carrier of [:(TOP-REAL n),I[01]:]
b .: m is Element of bool the carrier of (TOP-REAL n)
C - C is V21() real ext-real set
abs (C - C) is V21() real ext-real Element of REAL
z is set
z is V21() real ext-real Element of REAL
z is V167() V168() V169() Element of bool the carrier of I[01]
].(C - ((C * Pa) / (((2 * C) * |.Pa.|) + Pa))),1.] is V167() V168() V169() Element of bool REAL
z is set
z is V21() real ext-real Element of REAL
z is set
z is V21() real ext-real Element of REAL
z is set
dom b is Element of bool the carrier of [:(TOP-REAL n),I[01]:]
z is set
b . z is set
y is Element of the carrier of [:(TOP-REAL n),I[01]:]
j is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
ez is V21() real ext-real Element of the carrier of I[01]
[j,ez] is non empty Element of the carrier of [:(TOP-REAL n),I[01]:]
{j,ez} is non empty set
{j} is non empty trivial set
{{j,ez},{j}} is non empty set
b . y is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
ey is Element of the carrier of (Euclid n)
C * j is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C * j is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Pa / C is V21() real ext-real Element of COMPLEX
(Pa / C) / 2 is V21() real ext-real Element of REAL
C * ((Pa / C) / 2) is V21() real ext-real Element of REAL
fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
fp is Element of the carrier of (Euclid n)
dist (Pb,fp) is V21() real ext-real Element of REAL
ez - C is V21() real ext-real set
abs (ez - C) is V21() real ext-real Element of REAL
C - ez is V21() real ext-real set
abs (C - ez) is V21() real ext-real Element of REAL
|.fy.| is V21() real ext-real non negative Element of REAL
(abs (C - ez)) * |.fy.| is V21() real ext-real Element of REAL
((C * Pa) / (((2 * C) * |.Pa.|) + Pa)) * |.fy.| is V21() real ext-real Element of REAL
b . (j,ez) is set
[j,ez] is non empty set
b . [j,ez] is set
ez * j is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
ez * j is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
fe is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
fe - fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(fy) is V1() Function-like complex-valued set
- 1 is V21() real ext-real non positive set
(- 1) * fy is V1() Function-like set
K369(fe,K398(fy)) is V1() Function-like set
yy is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
C * yy is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
ez * yy is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
(C * yy) - (ez * yy) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
K398((ez * yy)) is V1() Function-like complex-valued set
(- 1) * (ez * yy) is V1() Function-like set
K369((C * yy),K398((ez * yy))) is V1() Function-like set
|.(fe - fy).| is V21() real ext-real non negative Element of REAL
(C - ez) * fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
|.((C - ez) * fy).| is V21() real ext-real non negative Element of REAL
dist (y,ey) is V21() real ext-real Element of REAL
fz is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
fz - fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K369(fz,K398(fy)) is V1() Function-like set
|.(fz - fy).| is V21() real ext-real non negative Element of REAL
fz - fe is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(fe) is V1() Function-like complex-valued set
(- 1) * fe is V1() Function-like set
K369(fz,K398(fe)) is V1() Function-like set
|.(fz - fe).| is V21() real ext-real non negative Element of REAL
|.(fz - fe).| + |.(fe - fy).| is V21() real ext-real non negative Element of REAL
Pa - fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(fy) is V1() Function-like complex-valued set
(- 1) * fy is V1() Function-like set
K369(Pa,K398(fy)) is V1() Function-like set
|.(Pa - fy).| is V21() real ext-real non negative Element of REAL
C * ((Pa / 2) / C) is V21() real ext-real Element of REAL
C * |.(Pa - fy).| is V21() real ext-real Element of REAL
abs C is V21() real ext-real Element of REAL
(abs C) * |.(Pa - fy).| is V21() real ext-real Element of REAL
fy - Pa is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(Pa) is V1() Function-like complex-valued set
(- 1) * Pa is V1() Function-like set
K369(fy,K398(Pa)) is V1() Function-like set
|.(fy - Pa).| is V21() real ext-real non negative Element of REAL
|.fy.| - |.Pa.| is V21() real ext-real Element of REAL
|.Pa.| + ((Pa / 2) / C) is V21() real ext-real Element of REAL
((C * Pa) / (((2 * C) * |.Pa.|) + Pa)) * (|.Pa.| + ((Pa / 2) / C)) is V21() real ext-real Element of REAL
Pa / (2 * C) is V21() real ext-real Element of REAL
|.Pa.| + (Pa / (2 * C)) is V21() real ext-real Element of REAL
((C * Pa) / (((2 * C) * |.Pa.|) + Pa)) * (|.Pa.| + (Pa / (2 * C))) is V21() real ext-real Element of REAL
|.Pa.| * (2 * C) is V21() real ext-real Element of REAL
(|.Pa.| * (2 * C)) / (2 * C) is V21() real ext-real Element of REAL
((|.Pa.| * (2 * C)) / (2 * C)) + (Pa / (2 * C)) is V21() real ext-real Element of REAL
((C * Pa) / (((2 * C) * |.Pa.|) + Pa)) * (((|.Pa.| * (2 * C)) / (2 * C)) + (Pa / (2 * C))) is V21() real ext-real Element of REAL
(|.Pa.| * (2 * C)) + Pa is V21() real ext-real Element of REAL
((|.Pa.| * (2 * C)) + Pa) / (2 * C) is V21() real ext-real Element of REAL
((C * Pa) / (((2 * C) * |.Pa.|) + Pa)) * (((|.Pa.| * (2 * C)) + Pa) / (2 * C)) is V21() real ext-real Element of REAL
(C * Pa) / (2 * C) is V21() real ext-real Element of REAL
C * Pa is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
(C * Pa) - fe is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K369((C * Pa),K398(fe)) is V1() Function-like set
yy is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
C * yy is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL
(C * Pa) - (C * yy) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K398((C * yy)) is V1() Function-like complex-valued set
(- 1) * (C * yy) is V1() Function-like set
K369((C * Pa),K398((C * yy))) is V1() Function-like set
C * (Pa - fy) is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
|.((C * Pa) - fe).| is V21() real ext-real non negative Element of REAL
(Pa / 2) + (Pa / 2) is V21() real ext-real Element of REAL
Pa is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
|.Pa.| is V21() real ext-real non negative Element of REAL
|.Pa.| + Pa is V21() real ext-real Element of REAL
Pb is Element of the carrier of (Euclid n)
Ball (Pb,Pa) is Element of bool the carrier of (Euclid n)
Pa / (|.Pa.| + Pa) is V21() real ext-real Element of REAL
[.0,(Pa / (|.Pa.| + Pa)).[ is V167() V168() V169() Element of bool REAL
0 + Pa is V21() real ext-real Element of REAL
X1 is set
W is V21() real ext-real Element of REAL
p is Element of bool the carrier of (TOP-REAL n)
X1 is V167() V168() V169() Element of bool the carrier of I[01]
[:p,X1:] is complex-valued ext-real-valued real-valued Element of bool the carrier of [:(TOP-REAL n),I[01]:]
W is complex-valued ext-real-valued real-valued Element of bool the carrier of [:(TOP-REAL n),I[01]:]
b .: W is Element of bool the carrier of (TOP-REAL n)
m is set
dom b is Element of bool the carrier of [:(TOP-REAL n),I[01]:]
z is set
b . z is set
z is Element of the carrier of [:(TOP-REAL n),I[01]:]
y is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
j is V21() real ext-real Element of the carrier of I[01]
[y,j] is non empty Element of the carrier of [:(TOP-REAL n),I[01]:]
{y,j} is non empty set
{y} is non empty trivial set
{{y,j},{y}} is non empty set
b . z is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
ez is Element of the carrier of (Euclid n)
fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
ey is Element of the carrier of (Euclid n)
dist (Pb,ey) is V21() real ext-real Element of REAL
b . (y,j) is set
[y,j] is non empty set
b . [y,j] is set
j * y is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
j * y is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
fp is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
0. (TOP-REAL n) is V1() Function-like V45(n) V54( TOP-REAL n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
fz is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
fz - fp is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(fp) is V1() Function-like complex-valued set
- 1 is V21() real ext-real non positive set
(- 1) * fp is V1() Function-like set
K369(fz,K398(fp)) is V1() Function-like set
(b . z) - (0. (TOP-REAL n)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
- (0. (TOP-REAL n)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
- (0. (TOP-REAL n)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(- 1) * (0. (TOP-REAL n)) is V1() Function-like set
(b . z) + (- (0. (TOP-REAL n))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) is V1() V4([: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]) V5( the carrier of (TOP-REAL n)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):]
[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is set
[:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
the addF of (TOP-REAL n) . ((b . z),(- (0. (TOP-REAL n)))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[(b . z),(- (0. (TOP-REAL n)))] is non empty set
{(b . z),(- (0. (TOP-REAL n)))} is non empty set
{(b . z)} is non empty trivial set
{{(b . z),(- (0. (TOP-REAL n)))},{(b . z)}} is non empty set
the addF of (TOP-REAL n) . [(b . z),(- (0. (TOP-REAL n)))] is set
(b . z) + (- (0. (TOP-REAL n))) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(b . z) - (0. (TOP-REAL n)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K398((0. (TOP-REAL n))) is V1() Function-like complex-valued set
K369((b . z),K398((0. (TOP-REAL n)))) is V1() Function-like set
|.fy.| is V21() real ext-real non negative Element of REAL
|.fy.| - |.Pa.| is V21() real ext-real Element of REAL
fy - Pa is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(Pa) is V1() Function-like complex-valued set
(- 1) * Pa is V1() Function-like set
K369(fy,K398(Pa)) is V1() Function-like set
|.(fy - Pa).| is V21() real ext-real non negative Element of REAL
Pa - fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
K398(fy) is V1() Function-like complex-valued set
(- 1) * fy is V1() Function-like set
K369(Pa,K398(fy)) is V1() Function-like set
|.(Pa - fy).| is V21() real ext-real non negative Element of REAL
Pa / j is V21() real ext-real Element of COMPLEX
Pa / (Pa / (|.Pa.| + Pa)) is V21() real ext-real Element of REAL
j * (Pa / j) is V21() real ext-real set
j * |.fy.| is V21() real ext-real Element of REAL
j * |.fy.| is V21() real ext-real Element of REAL
j * |.fy.| is V21() real ext-real Element of REAL
j * |.fy.| is V21() real ext-real Element of REAL
dist (y,ez) is V21() real ext-real Element of REAL
|.(fz - fp).| is V21() real ext-real non negative Element of REAL
|.fz.| is V21() real ext-real non negative Element of REAL
j * fy is V1() V4( NAT ) V5( REAL ) Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL n
|.(j * fy).| is V21() real ext-real non negative Element of REAL
abs j is V21() real ext-real Element of REAL
(abs j) * |.fy.| is V21() real ext-real Element of REAL
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of b,b is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of b,b
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,P
P + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
- C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,b
(P + C) + (- C) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
y + the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of b,b is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
C + (- C) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
P + (C + (- C)) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,P
y + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,b
(y + P) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of b,b is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of b,b
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,b
- C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,P
P + (- C) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
(P + (- C)) + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
y + the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of b,b is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(- C) + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
P + ((- C) + C) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,b
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,P
y + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
(y + (- P)) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,a
- C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
(- C) + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
((- C) + C) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a + y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,a
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
(- P) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,a
((- P) + P) + y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
- C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,a
C + (- C) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
(C + (- C)) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a + y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,a
P + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,a
(P + (- P)) + y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,P
Q + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
y + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,b
(Q + P) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(y + P) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,P
Q + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
y + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,a
P + Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,b
P + y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,b
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
(- P) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
((- P) + P) + Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(- P) + (P + Q) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(- P) + (P + y) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
((- P) + P) + y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,a
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
P + Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,b
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
P + y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,b
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is Element of the carrier of n
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,P
P + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,Q
(P + C) + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,Q
C + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,Q
P + (C + Pa) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,Q
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of Q,y
((P + C) + Pa) + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,y
(P + (C + Pa)) + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,y
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is Element of the carrier of n
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,P
P + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,Q
(P + C) + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,Q
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of Q,y
((P + C) + Pa) + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,y
C + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,Q
P + (C + Pa) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,Q
(P + (C + Pa)) + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,y
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is Element of the carrier of n
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,P
P + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,Q
(P + C) + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,Q
C + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,Q
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of Q,y
((P + C) + Pa) + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,y
(C + Pa) + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,y
P + ((C + Pa) + Pb) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,y
P + (C + Pa) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,Q
(P + (C + Pa)) + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,y
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is Element of the carrier of n
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,P
P + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,Q
(P + C) + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,Q
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of Q,y
((P + C) + Pa) + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,y
C + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,Q
(C + Pa) + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,y
P + ((C + Pa) + Pb) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,y
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is Element of the carrier of n
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,P
P + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,Q
C + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,Q
P + (C + Pa) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,Q
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of Q,y
(P + (C + Pa)) + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,y
Pa + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,y
(P + C) + (Pa + Pb) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,y
(P + C) + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,Q
((P + C) + Pa) + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,y
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is Element of the carrier of n
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,P
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,Q
C + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,Q
P + (C + Pa) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,Q
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of Q,y
(P + (C + Pa)) + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,y
P + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
Pa + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,y
(P + C) + (Pa + Pb) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,y
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of Q,b
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,Q
y + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,Q
(y + (- P)) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,P
((y + (- P)) + P) + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
y + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
(- P) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
((- P) + P) + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,P
y + (((- P) + P) + C) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of b,b is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of b,b
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of b,b + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,P
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,b
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,P
y + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
(y + (- P)) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,Q
((y + (- P)) + P) + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,Q
y + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,Q
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
- y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a
y + (- y) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,Q
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of Q,P
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
(y + (- y)) + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
((y + (- y)) + C) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,Q
(((y + (- y)) + C) + P) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
P + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,P
((y + (- y)) + C) + (P + (- P)) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
C + (P + (- P)) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
C + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,Q
(C + P) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
- y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,a
y + (- y) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,a
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
(y + (- y)) + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,Q
((y + (- y)) + C) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,Q
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of Q,P
(((y + (- y)) + C) + P) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
- y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,Q
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of Q,P
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
(- y) + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,P
((- y) + C) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,Q
y + (((- y) + C) + P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,Q
(y + (((- y) + C) + P)) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
y + (- y) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
(y + (- y)) + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
((y + (- y)) + C) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,Q
(((y + (- y)) + C) + P) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
- y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,a
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
(- y) + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,P
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,Q
((- y) + C) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,Q
y + (((- y) + C) + P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,Q
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of Q,P
(y + (((- y) + C) + P)) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is Element of the carrier of n
P is Element of the carrier of n
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,P
C + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,Q
Pa + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,Q
C + (Pa + Pb) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,Q
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of Q,y
(C + (Pa + Pb)) + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,y
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,P
- Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,P
(C + Pa) + (- Pb) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
Pb + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,Q
(Pb + Pb) + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,y
((C + Pa) + (- Pb)) + ((Pb + Pb) + Pa) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,y
Pb + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,y
Pb + (Pb + Pa) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of P,y
((C + Pa) + (- Pb)) + (Pb + (Pb + Pa)) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,y
((C + Pa) + (- Pb)) + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,P
(((C + Pa) + (- Pb)) + Pb) + (Pb + Pa) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,y
(C + Pa) + (Pb + Pa) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,y
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is Element of the carrier of n
Q is Element of the carrier of n
y is Element of the carrier of n
P is Element of the carrier of n
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,P
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,Q
Pa + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,Q
C + (Pa + Pb) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,Q
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of Q,y
(C + (Pa + Pb)) + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,y
C + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,P
- Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,P
(C + Pa) + (- Pb) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,P
Pb + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,Q
(Pb + Pb) + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of P,y
((C + Pa) + (- Pb)) + ((Pb + Pb) + Pa) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,y
n is TopStruct
the carrier of n is set
n is non empty TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
Funcs ( the carrier of I[01], the carrier of n) is functional non empty FUNCTION_DOMAIN of the carrier of I[01], the carrier of n
P is set
Q is set
n is non empty TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
(n,a,b) is set
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
n is non empty TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a,a) is non empty set
n is non empty TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is set
(n,a,a) is non empty set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
(n,a,b) is non empty set
[:(n,a,b),(n,a,b):] is set
bool [:(n,a,b),(n,a,b):] is set
P is set
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
P is set
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Q is set
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
y is set
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
P is set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Q is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
(n,a,b) is non empty set
[:(n,a,b),(n,a,b):] is set
bool [:(n,a,b),(n,a,b):] is set
P is V1() V4((n,a,b)) V5((n,a,b)) total quasi_total symmetric transitive Element of bool [:(n,a,b),(n,a,b):]
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
[Q,y] is non empty set
{Q,y} is non empty set
{Q} is non empty trivial set
{{Q,y},{Q}} is non empty set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
P is V1() V4((n,a,b)) V5((n,a,b)) Element of bool [:(n,a,b),(n,a,b):]
Q is V1() V4((n,a,b)) V5((n,a,b)) Element of bool [:(n,a,b),(n,a,b):]
y is set
P is set
[y,P] is non empty set
{y,P} is non empty set
{y} is non empty trivial set
{{y,P},{y}} is non empty set
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
(n,a,b) is V1() V4((n,a,b)) V5((n,a,b)) Element of bool [:(n,a,b),(n,a,b):]
(n,a,b) is non empty set
[:(n,a,b),(n,a,b):] is set
bool [:(n,a,b),(n,a,b):] is set
y is V1() V4((n,a,b)) V5((n,a,b)) total quasi_total symmetric transitive Element of bool [:(n,a,b),(n,a,b):]
P is set
C is set
[P,C] is non empty set
{P,C} is non empty set
{P} is non empty trivial set
{{P,C},{P}} is non empty set
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
(n,a,b) is non empty set
(n,a,b) is V1() V4((n,a,b)) V5((n,a,b)) Element of bool [:(n,a,b),(n,a,b):]
[:(n,a,b),(n,a,b):] is set
bool [:(n,a,b),(n,a,b):] is set
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Class ((n,a,b),Q) is Element of bool (n,a,b)
bool (n,a,b) is set
{Q} is non empty trivial set
(n,a,b) .: {Q} is set
[y,Q] is non empty set
{y,Q} is non empty set
{y} is non empty trivial set
{{y,Q},{y}} is non empty set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
(n,a,b) is non empty set
(n,a,b) is V1() V4((n,a,b)) V5((n,a,b)) Element of bool [:(n,a,b),(n,a,b):]
[:(n,a,b),(n,a,b):] is set
bool [:(n,a,b),(n,a,b):] is set
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Class ((n,a,b),Q) is Element of bool (n,a,b)
bool (n,a,b) is set
{Q} is non empty trivial set
(n,a,b) .: {Q} is set
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Class ((n,a,b),y) is Element of bool (n,a,b)
{y} is non empty trivial set
(n,a,b) .: {y} is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
(n,a,a) is non empty set
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
(n,a) is non empty set
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is V1() V4((n,a)) V5((n,a)) Element of bool [:(n,a),(n,a):]
(n,a) is non empty set
(n,a,a) is non empty set
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
(n,a) is non empty set
(n,a,a) is non empty set
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
Class (n,a) is non empty V126() a_partition of (n,a)
y is Element of Class (n,a)
P is Element of Class (n,a)
C is set
Class ((n,a),C) is Element of bool (n,a)
bool (n,a) is set
{C} is non empty trivial set
(n,a) .: {C} is set
Pa is set
Class ((n,a),Pa) is Element of bool (n,a)
{Pa} is non empty trivial set
(n,a) .: {Pa} is set
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Pb + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),(Pb + Pa)) is Element of bool (n,a)
{(Pb + Pa)} is non empty trivial set
(n,a) .: {(Pb + Pa)} is set
Pb is Element of Class (n,a)
[:(Class (n,a)),(Class (n,a)):] is set
[:[:(Class (n,a)),(Class (n,a)):],(Class (n,a)):] is set
bool [:[:(Class (n,a)),(Class (n,a)):],(Class (n,a)):] is set
y is V1() V4([:(Class (n,a)),(Class (n,a)):]) V5( Class (n,a)) Function-like total quasi_total Element of bool [:[:(Class (n,a)),(Class (n,a)):],(Class (n,a)):]
multMagma(# (Class (n,a)),y #) is strict multMagma
the carrier of multMagma(# (Class (n,a)),y #) is set
the multF of multMagma(# (Class (n,a)),y #) is V1() V4([: the carrier of multMagma(# (Class (n,a)),y #), the carrier of multMagma(# (Class (n,a)),y #):]) V5( the carrier of multMagma(# (Class (n,a)),y #)) Function-like quasi_total Element of bool [:[: the carrier of multMagma(# (Class (n,a)),y #), the carrier of multMagma(# (Class (n,a)),y #):], the carrier of multMagma(# (Class (n,a)),y #):]
[: the carrier of multMagma(# (Class (n,a)),y #), the carrier of multMagma(# (Class (n,a)),y #):] is set
[:[: the carrier of multMagma(# (Class (n,a)),y #), the carrier of multMagma(# (Class (n,a)),y #):], the carrier of multMagma(# (Class (n,a)),y #):] is set
bool [:[: the carrier of multMagma(# (Class (n,a)),y #), the carrier of multMagma(# (Class (n,a)),y #):], the carrier of multMagma(# (Class (n,a)),y #):] is set
P is Element of the carrier of multMagma(# (Class (n,a)),y #)
C is Element of the carrier of multMagma(# (Class (n,a)),y #)
the multF of multMagma(# (Class (n,a)),y #) . (P,C) is Element of the carrier of multMagma(# (Class (n,a)),y #)
[P,C] is non empty set
{P,C} is non empty set
{P} is non empty trivial set
{{P,C},{P}} is non empty set
the multF of multMagma(# (Class (n,a)),y #) . [P,C] is set
y is strict multMagma
the carrier of y is set
the multF of y is V1() V4([: the carrier of y, the carrier of y:]) V5( the carrier of y) Function-like quasi_total Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is set
P is strict multMagma
the carrier of P is set
the multF of P is V1() V4([: the carrier of P, the carrier of P:]) V5( the carrier of P) Function-like quasi_total Element of bool [:[: the carrier of P, the carrier of P:], the carrier of P:]
[: the carrier of P, the carrier of P:] is set
[:[: the carrier of P, the carrier of P:], the carrier of P:] is set
bool [:[: the carrier of P, the carrier of P:], the carrier of P:] is set
Pb is Element of the carrier of y
Pa is Element of the carrier of y
the multF of y . (Pb,Pa) is Element of the carrier of y
[Pb,Pa] is non empty set
{Pb,Pa} is non empty set
{Pb} is non empty trivial set
{{Pb,Pa},{Pb}} is non empty set
the multF of y . [Pb,Pa] is set
the multF of P . (Pb,Pa) is set
the multF of P . [Pb,Pa] is set
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),Pb) is Element of bool (n,a)
bool (n,a) is set
{Pb} is non empty trivial set
(n,a) .: {Pb} is set
p is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),p) is Element of bool (n,a)
{p} is non empty trivial set
(n,a) .: {p} is set
Pb + p is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),(Pb + p)) is Element of bool (n,a)
{(Pb + p)} is non empty trivial set
(n,a) .: {(Pb + p)} is set
s is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),s) is Element of bool (n,a)
{s} is non empty trivial set
(n,a) .: {s} is set
t is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),t) is Element of bool (n,a)
{t} is non empty trivial set
(n,a) .: {t} is set
s + t is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),(s + t)) is Element of bool (n,a)
{(s + t)} is non empty trivial set
(n,a) .: {(s + t)} is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is strict multMagma
the carrier of (n,a) is set
(n,a) is non empty set
(n,a,a) is non empty set
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
Class (n,a) is non empty V126() a_partition of (n,a)
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict multMagma
the carrier of (n,a) is non empty set
(n,a) is non empty set
(n,a,a) is non empty set
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
b is set
Class (n,a) is non empty V126() a_partition of (n,a)
P is Element of (n,a)
Class ((n,a),P) is Element of bool (n,a)
bool (n,a) is set
{P} is non empty trivial set
(n,a) .: {P} is set
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),y) is Element of bool (n,a)
{y} is non empty trivial set
(n,a) .: {y} is set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),P) is Element of bool (n,a)
{P} is non empty trivial set
(n,a) .: {P} is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict multMagma
the carrier of (n,a) is non empty set
(n,a) is non empty set
(n,a,a) is non empty set
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
P is Element of the carrier of (n,a)
Q is Element of the carrier of (n,a)
P * Q is Element of the carrier of (n,a)
the multF of (n,a) is V1() V4([: the carrier of (n,a), the carrier of (n,a):]) V5( the carrier of (n,a)) Function-like total quasi_total Element of bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):]
[: the carrier of (n,a), the carrier of (n,a):] is set
[:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
the multF of (n,a) . (P,Q) is Element of the carrier of (n,a)
[P,Q] is non empty set
{P,Q} is non empty set
{P} is non empty trivial set
{{P,Q},{P}} is non empty set
the multF of (n,a) . [P,Q] is set
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),y) is Element of bool (n,a)
bool (n,a) is set
{y} is non empty trivial set
(n,a) .: {y} is set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),P) is Element of bool (n,a)
{P} is non empty trivial set
(n,a) .: {P} is set
y + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),(y + P)) is Element of bool (n,a)
{(y + P)} is non empty trivial set
(n,a) .: {(y + P)} is set
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),C) is Element of bool (n,a)
{C} is non empty trivial set
(n,a) .: {C} is set
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),Pa) is Element of bool (n,a)
{Pa} is non empty trivial set
(n,a) .: {Pa} is set
C + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),(C + Pa)) is Element of bool (n,a)
{(C + Pa)} is non empty trivial set
(n,a) .: {(C + Pa)} is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict multMagma
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
(n,a) is non empty set
(n,a,a) is non empty set
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
Class ((n,a), the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a) is Element of bool (n,a)
bool (n,a) is set
{ the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a} is non empty trivial set
(n,a) .: { the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a} is set
Class (n,a) is non empty V126() a_partition of (n,a)
the carrier of (n,a) is non empty set
P is Element of the carrier of (n,a)
C is Element of the carrier of (n,a)
P * C is Element of the carrier of (n,a)
the multF of (n,a) is V1() V4([: the carrier of (n,a), the carrier of (n,a):]) V5( the carrier of (n,a)) Function-like total quasi_total Element of bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):]
[: the carrier of (n,a), the carrier of (n,a):] is set
[:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
the multF of (n,a) . (P,C) is Element of the carrier of (n,a)
[P,C] is non empty set
{P,C} is non empty set
{P} is non empty trivial set
{{P,C},{P}} is non empty set
the multF of (n,a) . [P,C] is set
Pa is Element of the carrier of (n,a)
(P * C) * Pa is Element of the carrier of (n,a)
the multF of (n,a) . ((P * C),Pa) is Element of the carrier of (n,a)
[(P * C),Pa] is non empty set
{(P * C),Pa} is non empty set
{(P * C)} is non empty trivial set
{{(P * C),Pa},{(P * C)}} is non empty set
the multF of (n,a) . [(P * C),Pa] is set
C * Pa is Element of the carrier of (n,a)
the multF of (n,a) . (C,Pa) is Element of the carrier of (n,a)
[C,Pa] is non empty set
{C,Pa} is non empty set
{C} is non empty trivial set
{{C,Pa},{C}} is non empty set
the multF of (n,a) . [C,Pa] is set
P * (C * Pa) is Element of the carrier of (n,a)
the multF of (n,a) . (P,(C * Pa)) is Element of the carrier of (n,a)
[P,(C * Pa)] is non empty set
{P,(C * Pa)} is non empty set
{{P,(C * Pa)},{P}} is non empty set
the multF of (n,a) . [P,(C * Pa)] is set
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),Pb) is Element of bool (n,a)
{Pb} is non empty trivial set
(n,a) .: {Pb} is set
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),Pa) is Element of bool (n,a)
{Pa} is non empty trivial set
(n,a) .: {Pa} is set
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),Pb) is Element of bool (n,a)
{Pb} is non empty trivial set
(n,a) .: {Pb} is set
p is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),p) is Element of bool (n,a)
{p} is non empty trivial set
(n,a) .: {p} is set
Pa + p is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),(Pa + p)) is Element of bool (n,a)
{(Pa + p)} is non empty trivial set
(n,a) .: {(Pa + p)} is set
Pb + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Pb + (Pa + p) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
s is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),s) is Element of bool (n,a)
{s} is non empty trivial set
(n,a) .: {s} is set
Pb + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),(Pb + Pa)) is Element of bool (n,a)
{(Pb + Pa)} is non empty trivial set
(n,a) .: {(Pb + Pa)} is set
s + p is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
(Pb + Pa) + p is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),(s + p)) is Element of bool (n,a)
{(s + p)} is non empty trivial set
(n,a) .: {(s + p)} is set
Class ((n,a),((Pb + Pa) + p)) is Element of bool (n,a)
{((Pb + Pa) + p)} is non empty trivial set
(n,a) .: {((Pb + Pa) + p)} is set
Class ((n,a),(Pb + (Pa + p))) is Element of bool (n,a)
{(Pb + (Pa + p))} is non empty trivial set
(n,a) .: {(Pb + (Pa + p))} is set
Class ((n,a),(Pb + Pb)) is Element of bool (n,a)
{(Pb + Pb)} is non empty trivial set
(n,a) .: {(Pb + Pb)} is set
the carrier of (n,a) is non empty set
P is Element of the carrier of (n,a)
C is Element of the carrier of (n,a)
C * P is Element of the carrier of (n,a)
the multF of (n,a) is V1() V4([: the carrier of (n,a), the carrier of (n,a):]) V5( the carrier of (n,a)) Function-like total quasi_total Element of bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):]
[: the carrier of (n,a), the carrier of (n,a):] is set
[:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
the multF of (n,a) . (C,P) is Element of the carrier of (n,a)
[C,P] is non empty set
{C,P} is non empty set
{C} is non empty trivial set
{{C,P},{C}} is non empty set
the multF of (n,a) . [C,P] is set
P * C is Element of the carrier of (n,a)
the multF of (n,a) . (P,C) is Element of the carrier of (n,a)
[P,C] is non empty set
{P,C} is non empty set
{P} is non empty trivial set
{{P,C},{P}} is non empty set
the multF of (n,a) . [P,C] is set
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),Pa) is Element of bool (n,a)
{Pa} is non empty trivial set
(n,a) .: {Pa} is set
Pa + the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),(Pa + the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a)) is Element of bool (n,a)
{(Pa + the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a)} is non empty trivial set
(n,a) .: {(Pa + the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a)} is set
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),( the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a + Pa)) is Element of bool (n,a)
{( the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a + Pa)} is non empty trivial set
(n,a) .: {( the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a + Pa)} is set
- Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),(- Pa)) is Element of bool (n,a)
{(- Pa)} is non empty trivial set
(n,a) .: {(- Pa)} is set
Pa is Element of the carrier of (n,a)
C * Pa is Element of the carrier of (n,a)
the multF of (n,a) . (C,Pa) is Element of the carrier of (n,a)
[C,Pa] is non empty set
{C,Pa} is non empty set
{{C,Pa},{C}} is non empty set
the multF of (n,a) . [C,Pa] is set
Pa * C is Element of the carrier of (n,a)
the multF of (n,a) . (Pa,C) is Element of the carrier of (n,a)
[Pa,C] is non empty set
{Pa,C} is non empty set
{Pa} is non empty trivial set
{{Pa,C},{Pa}} is non empty set
the multF of (n,a) . [Pa,C] is set
Pa + (- Pa) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),(Pa + (- Pa))) is Element of bool (n,a)
{(Pa + (- Pa))} is non empty trivial set
(n,a) .: {(Pa + (- Pa))} is set
(- Pa) + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),((- Pa) + Pa)) is Element of bool (n,a)
{((- Pa) + Pa)} is non empty trivial set
(n,a) .: {((- Pa) + Pa)} is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,b) is non empty set
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,a) is non empty set
[: the carrier of (n,b), the carrier of (n,a):] is set
bool [: the carrier of (n,b), the carrier of (n,a):] is set
(n,b) is non empty set
(n,b,b) is non empty set
(n,b) is V1() V4((n,b)) V5((n,b)) non empty total quasi_total symmetric transitive Element of bool [:(n,b),(n,b):]
[:(n,b),(n,b):] is set
bool [:(n,b),(n,b):] is set
(n,b,b) is V1() V4((n,b,b)) V5((n,b,b)) Element of bool [:(n,b,b),(n,b,b):]
[:(n,b,b),(n,b,b):] is set
bool [:(n,b,b),(n,b,b):] is set
(n,a) is non empty set
(n,a,a) is non empty set
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a
Q is Element of the carrier of (n,b)
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
Class ((n,b),y) is Element of bool (n,b)
bool (n,b) is set
{y} is non empty trivial set
(n,b) .: {y} is set
P + y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(P + y) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),((P + y) + (- P))) is Element of bool (n,a)
bool (n,a) is set
{((P + y) + (- P))} is non empty trivial set
(n,a) .: {((P + y) + (- P))} is set
P is Element of the carrier of (n,a)
Q is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
y is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
Class ((n,b),P) is Element of bool (n,b)
bool (n,b) is set
{P} is non empty trivial set
(n,b) .: {P} is set
y . (Class ((n,b),P)) is set
P + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(P + P) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),((P + P) + (- P))) is Element of bool (n,a)
bool (n,a) is set
{((P + P) + (- P))} is non empty trivial set
(n,a) .: {((P + P) + (- P))} is set
Class (n,b) is non empty V126() a_partition of (n,b)
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
Class ((n,b),C) is Element of bool (n,b)
{C} is non empty trivial set
(n,b) .: {C} is set
P + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(P + C) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),((P + C) + (- P))) is Element of bool (n,a)
{((P + C) + (- P))} is non empty trivial set
(n,a) .: {((P + C) + (- P))} is set
Q is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
y is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
P is Element of the carrier of (n,b)
Q . P is Element of the carrier of (n,a)
y . P is Element of the carrier of (n,a)
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
Class ((n,b),C) is Element of bool (n,b)
bool (n,b) is set
{C} is non empty trivial set
(n,b) .: {C} is set
P + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(P + C) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),((P + C) + (- P))) is Element of bool (n,a)
bool (n,a) is set
{((P + C) + (- P))} is non empty trivial set
(n,a) .: {((P + C) + (- P))} is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,a) is non empty set
b is Element of the carrier of n
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,b) is non empty set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(n,a,b,P) is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
[: the carrier of (n,b), the carrier of (n,a):] is set
bool [: the carrier of (n,b), the carrier of (n,a):] is set
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(n,a,b,Q) is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a
- Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a
y is Element of the carrier of (n,b)
(n,a,b,P) . y is Element of the carrier of (n,a)
(n,a,b,Q) . y is Element of the carrier of (n,a)
(n,b) is non empty set
(n,b,b) is non empty set
(n,b) is V1() V4((n,b)) V5((n,b)) non empty total quasi_total symmetric transitive Element of bool [:(n,b),(n,b):]
[:(n,b),(n,b):] is set
bool [:(n,b),(n,b):] is set
(n,b,b) is V1() V4((n,b,b)) V5((n,b,b)) Element of bool [:(n,b,b),(n,b,b):]
[:(n,b,b),(n,b,b):] is set
bool [:(n,b,b),(n,b,b):] is set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
Class ((n,b),P) is Element of bool (n,b)
bool (n,b) is set
{P} is non empty trivial set
(n,b) .: {P} is set
P + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
Q + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(P + P) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
(Q + P) + (- Q) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
(n,a) is non empty set
(n,a,a) is non empty set
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
Class ((n,a),((P + P) + (- P))) is Element of bool (n,a)
bool (n,a) is set
{((P + P) + (- P))} is non empty trivial set
(n,a) .: {((P + P) + (- P))} is set
Class ((n,a),((Q + P) + (- Q))) is Element of bool (n,a)
{((Q + P) + (- Q))} is non empty trivial set
(n,a) .: {((Q + P) + (- Q))} is set
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,a) is non empty set
b is Element of the carrier of n
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,b) is non empty set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
(n,a,b,P) is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
[: the carrier of (n,b), the carrier of (n,a):] is set
bool [: the carrier of (n,b), the carrier of (n,a):] is set
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
(n,a,b,Q) is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,a) is non empty set
b is Element of the carrier of n
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,b) is non empty set
[: the carrier of (n,b), the carrier of (n,a):] is set
bool [: the carrier of (n,b), the carrier of (n,a):] is set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(n,a,b,P) is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
y is Element of the carrier of (n,b)
(n,b) is non empty set
(n,b,b) is non empty set
(n,b) is V1() V4((n,b)) V5((n,b)) non empty total quasi_total symmetric transitive Element of bool [:(n,b),(n,b):]
[:(n,b),(n,b):] is set
bool [:(n,b),(n,b):] is set
(n,b,b) is V1() V4((n,b,b)) V5((n,b,b)) Element of bool [:(n,b,b),(n,b,b):]
[:(n,b,b),(n,b,b):] is set
bool [:(n,b,b),(n,b,b):] is set
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
Class ((n,b),C) is Element of bool (n,b)
bool (n,b) is set
{C} is non empty trivial set
(n,b) .: {C} is set
P is Element of the carrier of (n,b)
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
Class ((n,b),Pa) is Element of bool (n,b)
{Pa} is non empty trivial set
(n,b) .: {Pa} is set
(n,a,b,P) . P is Element of the carrier of (n,a)
(n,a) is non empty set
(n,a,a) is non empty set
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),Pb) is Element of bool (n,a)
bool (n,a) is set
{Pb} is non empty trivial set
(n,a) .: {Pb} is set
P + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a
(P + Pa) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),((P + Pa) + (- P))) is Element of bool (n,a)
{((P + Pa) + (- P))} is non empty trivial set
(n,a) .: {((P + Pa) + (- P))} is set
C + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
P + (C + Pa) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(P + (C + Pa)) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
P + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(P + C) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
((P + C) + (- P)) + ((P + Pa) + (- P)) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
(n,a,b,P) . y is Element of the carrier of (n,a)
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),Pa) is Element of bool (n,a)
{Pa} is non empty trivial set
(n,a) .: {Pa} is set
Class ((n,a),((P + C) + (- P))) is Element of bool (n,a)
{((P + C) + (- P))} is non empty trivial set
(n,a) .: {((P + C) + (- P))} is set
Pa + Pb is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
y * P is Element of the carrier of (n,b)
the multF of (n,b) is V1() V4([: the carrier of (n,b), the carrier of (n,b):]) V5( the carrier of (n,b)) Function-like total quasi_total Element of bool [:[: the carrier of (n,b), the carrier of (n,b):], the carrier of (n,b):]
[: the carrier of (n,b), the carrier of (n,b):] is set
[:[: the carrier of (n,b), the carrier of (n,b):], the carrier of (n,b):] is set
bool [:[: the carrier of (n,b), the carrier of (n,b):], the carrier of (n,b):] is set
the multF of (n,b) . (y,P) is Element of the carrier of (n,b)
[y,P] is non empty set
{y,P} is non empty set
{y} is non empty trivial set
{{y,P},{y}} is non empty set
the multF of (n,b) . [y,P] is set
(n,a,b,P) . (y * P) is Element of the carrier of (n,a)
Class ((n,b),(C + Pa)) is Element of bool (n,b)
{(C + Pa)} is non empty trivial set
(n,b) .: {(C + Pa)} is set
(n,a,b,P) . (Class ((n,b),(C + Pa))) is set
Class ((n,a),((P + (C + Pa)) + (- P))) is Element of bool (n,a)
{((P + (C + Pa)) + (- P))} is non empty trivial set
(n,a) .: {((P + (C + Pa)) + (- P))} is set
Class ((n,a),(Pa + Pb)) is Element of bool (n,a)
{(Pa + Pb)} is non empty trivial set
(n,a) .: {(Pa + Pb)} is set
((n,a,b,P) . y) * ((n,a,b,P) . P) is Element of the carrier of (n,a)
the multF of (n,a) is V1() V4([: the carrier of (n,a), the carrier of (n,a):]) V5( the carrier of (n,a)) Function-like total quasi_total Element of bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):]
[: the carrier of (n,a), the carrier of (n,a):] is set
[:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
the multF of (n,a) . (((n,a,b,P) . y),((n,a,b,P) . P)) is Element of the carrier of (n,a)
[((n,a,b,P) . y),((n,a,b,P) . P)] is non empty set
{((n,a,b,P) . y),((n,a,b,P) . P)} is non empty set
{((n,a,b,P) . y)} is non empty trivial set
{{((n,a,b,P) . y),((n,a,b,P) . P)},{((n,a,b,P) . y)}} is non empty set
the multF of (n,a) . [((n,a,b,P) . y),((n,a,b,P) . P)] is set
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
(n,a,b,P) is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
the carrier of (n,b) is non empty set
the carrier of (n,a) is non empty set
[: the carrier of (n,b), the carrier of (n,a):] is set
bool [: the carrier of (n,b), the carrier of (n,a):] is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(n,a,b,P) is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,b) is non empty set
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,a) is non empty set
[: the carrier of (n,b), the carrier of (n,a):] is set
bool [: the carrier of (n,b), the carrier of (n,a):] is set
y is set
K48((n,a,b,P)) is set
P is set
(n,a,b,P) . y is set
(n,a,b,P) . P is set
dom (n,a,b,P) is Element of bool the carrier of (n,b)
bool the carrier of (n,b) is set
(n,b) is non empty set
(n,b,b) is non empty set
(n,b) is V1() V4((n,b)) V5((n,b)) non empty total quasi_total symmetric transitive Element of bool [:(n,b),(n,b):]
[:(n,b),(n,b):] is set
bool [:(n,b),(n,b):] is set
(n,b,b) is V1() V4((n,b,b)) V5((n,b,b)) Element of bool [:(n,b,b),(n,b,b):]
[:(n,b,b),(n,b,b):] is set
bool [:(n,b,b),(n,b,b):] is set
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
Class ((n,b),C) is Element of bool (n,b)
bool (n,b) is set
{C} is non empty trivial set
(n,b) .: {C} is set
(n,a) is non empty set
(n,a,a) is non empty set
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
P + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a
(P + C) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),((P + C) + (- P))) is Element of bool (n,a)
bool (n,a) is set
{((P + C) + (- P))} is non empty trivial set
(n,a) .: {((P + C) + (- P))} is set
Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
Class ((n,b),Pa) is Element of bool (n,b)
{Pa} is non empty trivial set
(n,b) .: {Pa} is set
P + Pa is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(P + Pa) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),((P + Pa) + (- P))) is Element of bool (n,a)
{((P + Pa) + (- P))} is non empty trivial set
(n,a) .: {((P + Pa) + (- P))} is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,a) is non empty set
b is Element of the carrier of n
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(n,a,b,P) is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,b) is non empty set
[: the carrier of (n,b), the carrier of (n,a):] is set
bool [: the carrier of (n,b), the carrier of (n,a):] is set
rng (n,a,b,P) is Element of bool the carrier of (n,a)
bool the carrier of (n,a) is set
y is set
(n,a) is non empty set
(n,a,a) is non empty set
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),P) is Element of bool (n,a)
bool (n,a) is set
{P} is non empty trivial set
(n,a) .: {P} is set
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a
(- P) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a
((- P) + P) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
P + (((- P) + P) + P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(P + (((- P) + P) + P)) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
(n,b) is non empty set
(n,b,b) is non empty set
(n,b) is V1() V4((n,b)) V5((n,b)) non empty total quasi_total symmetric transitive Element of bool [:(n,b),(n,b):]
[:(n,b),(n,b):] is set
bool [:(n,b),(n,b):] is set
(n,b,b) is V1() V4((n,b,b)) V5((n,b,b)) Element of bool [:(n,b,b),(n,b,b):]
[:(n,b,b),(n,b,b):] is set
bool [:(n,b,b),(n,b,b):] is set
Class ((n,b),(((- P) + P) + P)) is Element of bool (n,b)
bool (n,b) is set
{(((- P) + P) + P)} is non empty trivial set
(n,b) .: {(((- P) + P) + P)} is set
dom (n,a,b,P) is Element of bool the carrier of (n,b)
bool the carrier of (n,b) is set
(n,a,b,P) . (Class ((n,b),(((- P) + P) + P))) is set
Class ((n,a),((P + (((- P) + P) + P)) + (- P))) is Element of bool (n,a)
{((P + (((- P) + P) + P)) + (- P))} is non empty trivial set
(n,a) .: {((P + (((- P) + P) + P)) + (- P))} is set
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
(n,a,b,P) is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total multiplicative Element of bool [: the carrier of (n,b), the carrier of (n,a):]
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,b) is non empty set
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,a) is non empty set
[: the carrier of (n,b), the carrier of (n,a):] is set
bool [: the carrier of (n,b), the carrier of (n,a):] is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,a) is non empty set
b is Element of the carrier of n
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,b) is non empty set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(n,a,b,P) is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
[: the carrier of (n,b), the carrier of (n,a):] is set
bool [: the carrier of (n,b), the carrier of (n,a):] is set
(n,a,b,P) " is V1() V4( the carrier of (n,a)) V5( the carrier of (n,b)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,a), the carrier of (n,b):]
[: the carrier of (n,a), the carrier of (n,b):] is set
bool [: the carrier of (n,a), the carrier of (n,b):] is set
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a
(n,b,a,(- P)) is V1() V4( the carrier of (n,a)) V5( the carrier of (n,b)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,a), the carrier of (n,b):]
(n,a,b,P) " is V1() Function-like set
P is Element of the carrier of (n,a)
((n,a,b,P) ") . P is Element of the carrier of (n,b)
(n,b,a,(- P)) . P is Element of the carrier of (n,b)
(n,a) is non empty set
(n,a,a) is non empty set
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),C) is Element of bool (n,a)
bool (n,a) is set
{C} is non empty trivial set
(n,a) .: {C} is set
- (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(- P) + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a
((- P) + C) + (- (- P)) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,b
P + (((- P) + C) + (- (- P))) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(P + (((- P) + C) + (- (- P)))) + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
dom (n,a,b,P) is Element of bool the carrier of (n,b)
bool the carrier of (n,b) is set
(n,b) is non empty set
(n,b,b) is non empty set
(n,b) is V1() V4((n,b)) V5((n,b)) non empty total quasi_total symmetric transitive Element of bool [:(n,b),(n,b):]
[:(n,b),(n,b):] is set
bool [:(n,b),(n,b):] is set
(n,b,b) is V1() V4((n,b,b)) V5((n,b,b)) Element of bool [:(n,b,b),(n,b,b):]
[:(n,b,b),(n,b,b):] is set
bool [:(n,b,b),(n,b,b):] is set
Class ((n,b),(((- P) + C) + (- (- P)))) is Element of bool (n,b)
bool (n,b) is set
{(((- P) + C) + (- (- P)))} is non empty trivial set
(n,b) .: {(((- P) + C) + (- (- P)))} is set
(n,a,b,P) . (Class ((n,b),(((- P) + C) + (- (- P))))) is set
Class ((n,a),((P + (((- P) + C) + (- (- P)))) + (- P))) is Element of bool (n,a)
{((P + (((- P) + C) + (- (- P)))) + (- P))} is non empty trivial set
(n,a) .: {((P + (((- P) + C) + (- (- P)))) + (- P))} is set
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,a) is non empty set
b is Element of the carrier of n
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,b) is non empty set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
(n,a,b,P) is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like one-to-one non empty total quasi_total onto bijective multiplicative Element of bool [: the carrier of (n,b), the carrier of (n,a):]
[: the carrier of (n,b), the carrier of (n,a):] is set
bool [: the carrier of (n,b), the carrier of (n,a):] is set
(n,a,b,P) " is V1() V4( the carrier of (n,a)) V5( the carrier of (n,b)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,a), the carrier of (n,b):]
[: the carrier of (n,a), the carrier of (n,b):] is set
bool [: the carrier of (n,a), the carrier of (n,b):] is set
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,a
(n,b,a,(- P)) is V1() V4( the carrier of (n,a)) V5( the carrier of (n,b)) Function-like one-to-one non empty total quasi_total onto bijective multiplicative Element of bool [: the carrier of (n,a), the carrier of (n,b):]
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,a) is non empty set
b is Element of the carrier of n
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,b) is non empty set
[: the carrier of (n,b), the carrier of (n,a):] is set
bool [: the carrier of (n,b), the carrier of (n,a):] is set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,b
(n,a,b,P) is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,b), the carrier of (n,a):]
Q is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like non empty total quasi_total multiplicative Element of bool [: the carrier of (n,b), the carrier of (n,a):]
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,b) is non empty set
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,a) is non empty set
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of a,b
(n,a,b,P) is V1() V4( the carrier of (n,b)) V5( the carrier of (n,a)) Function-like one-to-one non empty total quasi_total onto bijective multiplicative Element of bool [: the carrier of (n,b), the carrier of (n,a):]
[: the carrier of (n,b), the carrier of (n,a):] is set
bool [: the carrier of (n,b), the carrier of (n,a):] is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
b is Element of the carrier of n
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a
the carrier of (n,a) is non empty set
the carrier of (n,b) is non empty set
[: the carrier of (n,a), the carrier of (n,b):] is set
bool [: the carrier of (n,a), the carrier of (n,b):] is set
(n,b,a, the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of b,a) is V1() V4( the carrier of (n,a)) V5( the carrier of (n,b)) Function-like non empty total quasi_total Element of bool [: the carrier of (n,a), the carrier of (n,b):]
Q is V1() V4( the carrier of (n,a)) V5( the carrier of (n,b)) Function-like non empty total quasi_total multiplicative Element of bool [: the carrier of (n,a), the carrier of (n,b):]
n is non empty TopSpace-like pathwise_connected TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
b is Element of the carrier of n
(n,b) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,a is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,a
(n,b,a, the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total continuous Path of b,a) is V1() V4( the carrier of (n,a)) V5( the carrier of (n,b)) Function-like one-to-one non empty total quasi_total onto bijective multiplicative Element of bool [: the carrier of (n,a), the carrier of (n,b):]
the carrier of (n,a) is non empty set
the carrier of (n,b) is non empty set
[: the carrier of (n,a), the carrier of (n,b):] is set
bool [: the carrier of (n,a), the carrier of (n,b):] is set
n is V21() natural real ext-real set
TOP-REAL n is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL n) is non empty set
[: the carrier of I[01], the carrier of (TOP-REAL n):] is set
bool [: the carrier of I[01], the carrier of (TOP-REAL n):] is set
[:I[01],I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:I[01],I[01]:] is non empty set
[: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):] is set
a is V1() V4( the carrier of I[01]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of I[01], the carrier of (TOP-REAL n):]
b is V1() V4( the carrier of I[01]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of I[01], the carrier of (TOP-REAL n):]
[: the carrier of I[01], the carrier of I[01]:] is complex-valued ext-real-valued real-valued set
[:[: the carrier of I[01], the carrier of I[01]:], the carrier of (TOP-REAL n):] is set
bool [:[: the carrier of I[01], the carrier of I[01]:], the carrier of (TOP-REAL n):] is set
Q is V1() V4([: the carrier of I[01], the carrier of I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like total quasi_total Element of bool [:[: the carrier of I[01], the carrier of I[01]:], the carrier of (TOP-REAL n):]
y is V1() V4( the carrier of [:I[01],I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):]
P is V21() real ext-real Element of the carrier of I[01]
C is V21() real ext-real Element of the carrier of I[01]
y . (P,C) is set
[P,C] is non empty set
{P,C} is non empty V167() V168() V169() set
{P} is non empty trivial V167() V168() V169() set
{{P,C},{P}} is non empty set
y . [P,C] is set
a . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
1 - C is V21() real ext-real Element of REAL
(1 - C) * (a . P) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(1 - C) * (a . P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
b . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C * (b . P) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C * (b . P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
((1 - C) * (a . P)) + (C * (b . P)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) is V1() V4([: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]) V5( the carrier of (TOP-REAL n)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):]
[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is set
[:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
the addF of (TOP-REAL n) . (((1 - C) * (a . P)),(C * (b . P))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[((1 - C) * (a . P)),(C * (b . P))] is non empty set
{((1 - C) * (a . P)),(C * (b . P))} is non empty set
{((1 - C) * (a . P))} is non empty trivial set
{{((1 - C) * (a . P)),(C * (b . P))},{((1 - C) * (a . P))}} is non empty set
the addF of (TOP-REAL n) . [((1 - C) * (a . P)),(C * (b . P))] is set
((1 - C) * (a . P)) + (C * (b . P)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Q is V1() V4( the carrier of [:I[01],I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):]
y is V1() V4( the carrier of [:I[01],I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):]
P is V21() real ext-real Element of the carrier of I[01]
C is V21() real ext-real Element of the carrier of I[01]
Q . (P,C) is set
[P,C] is non empty set
{P,C} is non empty V167() V168() V169() set
{P} is non empty trivial V167() V168() V169() set
{{P,C},{P}} is non empty set
Q . [P,C] is set
y . (P,C) is set
y . [P,C] is set
a . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
1 - C is V21() real ext-real Element of REAL
(1 - C) * (a . P) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(1 - C) * (a . P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
b . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C * (b . P) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C * (b . P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
((1 - C) * (a . P)) + (C * (b . P)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) is V1() V4([: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]) V5( the carrier of (TOP-REAL n)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):]
[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is set
[:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
the addF of (TOP-REAL n) . (((1 - C) * (a . P)),(C * (b . P))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[((1 - C) * (a . P)),(C * (b . P))] is non empty set
{((1 - C) * (a . P)),(C * (b . P))} is non empty set
{((1 - C) * (a . P))} is non empty trivial set
{{((1 - C) * (a . P)),(C * (b . P))},{((1 - C) * (a . P))}} is non empty set
the addF of (TOP-REAL n) . [((1 - C) * (a . P)),(C * (b . P))] is set
((1 - C) * (a . P)) + (C * (b . P)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
[: the carrier of I[01], the carrier of I[01]:] is complex-valued ext-real-valued real-valued set
n is V21() natural real ext-real set
TOP-REAL n is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL n) is non empty set
[: the carrier of I[01], the carrier of (TOP-REAL n):] is set
bool [: the carrier of I[01], the carrier of (TOP-REAL n):] is set
b is V1() V4( the carrier of I[01]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of (TOP-REAL n):]
P is V1() V4( the carrier of I[01]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of (TOP-REAL n):]
(n,b,P) is V1() V4( the carrier of [:I[01],I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):]
[: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):] is set
id I[01] is V1() V4( the carrier of I[01]) V5( the carrier of I[01]) Function-like non empty total quasi_total continuous V138( I[01] , I[01] ) complex-valued ext-real-valued real-valued Element of bool [: the carrier of I[01], the carrier of I[01]:]
[: the carrier of I[01], the carrier of I[01]:] is complex-valued ext-real-valued real-valued set
bool [: the carrier of I[01], the carrier of I[01]:] is set
id the carrier of I[01] is V1() V4( the carrier of I[01]) V5( the carrier of I[01]) non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of I[01], the carrier of I[01]:]
[:b,(id I[01]):] is V1() V4( the carrier of [:I[01],I[01]:]) V5( the carrier of [:(TOP-REAL n),I[01]:]) Function-like non empty total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of [:(TOP-REAL n),I[01]:]:]
[:(TOP-REAL n),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(TOP-REAL n),I[01]:] is non empty set
[: the carrier of [:I[01],I[01]:], the carrier of [:(TOP-REAL n),I[01]:]:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of [:(TOP-REAL n),I[01]:]:] is set
[:P,(id I[01]):] is V1() V4( the carrier of [:I[01],I[01]:]) V5( the carrier of [:(TOP-REAL n),I[01]:]) Function-like non empty total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of [:(TOP-REAL n),I[01]:]:]
[: the carrier of (TOP-REAL n), the carrier of I[01]:] is complex-valued ext-real-valued real-valued set
[:[: the carrier of (TOP-REAL n), the carrier of I[01]:], the carrier of (TOP-REAL n):] is set
bool [:[: the carrier of (TOP-REAL n), the carrier of I[01]:], the carrier of (TOP-REAL n):] is set
Pa is V1() V4([: the carrier of (TOP-REAL n), the carrier of I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL n), the carrier of I[01]:], the carrier of (TOP-REAL n):]
Pb is V1() V4([: the carrier of (TOP-REAL n), the carrier of I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL n), the carrier of I[01]:], the carrier of (TOP-REAL n):]
[: the carrier of [:(TOP-REAL n),I[01]:], the carrier of (TOP-REAL n):] is set
bool [: the carrier of [:(TOP-REAL n),I[01]:], the carrier of (TOP-REAL n):] is set
Pb is V1() V4( the carrier of [:(TOP-REAL n),I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:(TOP-REAL n),I[01]:], the carrier of (TOP-REAL n):]
Pa is V1() V4( the carrier of [:(TOP-REAL n),I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:(TOP-REAL n),I[01]:], the carrier of (TOP-REAL n):]
Pa * [:b,(id I[01]):] is V1() V4( the carrier of [:I[01],I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):]
Pb * [:P,(id I[01]):] is V1() V4( the carrier of [:I[01],I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):]
dom P is V167() V168() V169() Element of bool the carrier of I[01]
dom b is V167() V168() V169() Element of bool the carrier of I[01]
p is Element of the carrier of [:I[01],I[01]:]
(n,b,P) . p is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(Pa * [:b,(id I[01]):]) . p is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(Pb * [:P,(id I[01]):]) . p is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
((Pa * [:b,(id I[01]):]) . p) + ((Pb * [:P,(id I[01]):]) . p) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) is V1() V4([: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]) V5( the carrier of (TOP-REAL n)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):]
[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is set
[:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
the addF of (TOP-REAL n) . (((Pa * [:b,(id I[01]):]) . p),((Pb * [:P,(id I[01]):]) . p)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[((Pa * [:b,(id I[01]):]) . p),((Pb * [:P,(id I[01]):]) . p)] is non empty set
{((Pa * [:b,(id I[01]):]) . p),((Pb * [:P,(id I[01]):]) . p)} is non empty set
{((Pa * [:b,(id I[01]):]) . p)} is non empty trivial set
{{((Pa * [:b,(id I[01]):]) . p),((Pb * [:P,(id I[01]):]) . p)},{((Pa * [:b,(id I[01]):]) . p)}} is non empty set
the addF of (TOP-REAL n) . [((Pa * [:b,(id I[01]):]) . p),((Pb * [:P,(id I[01]):]) . p)] is set
((Pa * [:b,(id I[01]):]) . p) + ((Pb * [:P,(id I[01]):]) . p) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
s is V21() real ext-real Element of the carrier of I[01]
t is V21() real ext-real Element of the carrier of I[01]
[s,t] is non empty Element of the carrier of [:I[01],I[01]:]
{s,t} is non empty V167() V168() V169() set
{s} is non empty trivial V167() V168() V169() set
{{s,t},{s}} is non empty set
dom (id I[01]) is V167() V168() V169() Element of bool the carrier of I[01]
(id I[01]) . t is V21() real ext-real Element of the carrier of I[01]
[:P,(id I[01]):] . (s,t) is set
[s,t] is non empty set
[:P,(id I[01]):] . [s,t] is set
Pb . ([:P,(id I[01]):] . (s,t)) is set
P . s is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
Pb . ((P . s),t) is set
[(P . s),t] is non empty set
{(P . s),t} is non empty set
{(P . s)} is non empty trivial set
{{(P . s),t},{(P . s)}} is non empty set
Pb . [(P . s),t] is set
t * (P . s) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
t * (P . s) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
[:b,(id I[01]):] . (s,t) is set
[:b,(id I[01]):] . [s,t] is set
Pa . ([:b,(id I[01]):] . (s,t)) is set
b . s is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
Pa . ((b . s),t) is set
[(b . s),t] is non empty set
{(b . s),t} is non empty set
{(b . s)} is non empty trivial set
{{(b . s),t},{(b . s)}} is non empty set
Pa . [(b . s),t] is set
1 - t is V21() real ext-real Element of REAL
(1 - t) * (b . s) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(1 - t) * (b . s) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(n,b,P) . (s,t) is set
(n,b,P) . [s,t] is set
n is V21() natural real ext-real set
TOP-REAL n is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL n) is non empty set
a is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
b is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
P is V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Path of a,b
Q is V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Path of a,b
(n,P,Q) is V1() V4( the carrier of [:I[01],I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):]
[: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):] is set
P is V21() real ext-real Element of the carrier of I[01]
(n,P,Q) . (P,0) is set
[P,0] is non empty set
{P,0} is non empty V167() V168() V169() set
{P} is non empty trivial V167() V168() V169() set
{{P,0},{P}} is non empty set
(n,P,Q) . [P,0] is set
P . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(n,P,Q) . (P,1) is set
[P,1] is non empty set
{P,1} is non empty V167() V168() V169() set
{{P,1},{P}} is non empty set
(n,P,Q) . [P,1] is set
Q . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
1 - 0 is non empty V21() real ext-real positive non negative Element of REAL
(1 - 0) * (P . P) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(1 - 0) * (P . P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
0 * (Q . P) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
0 * (Q . P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
((1 - 0) * (P . P)) + (0 * (Q . P)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) is V1() V4([: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]) V5( the carrier of (TOP-REAL n)) Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):]
[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] is set
[:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is set
the addF of (TOP-REAL n) . (((1 - 0) * (P . P)),(0 * (Q . P))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[((1 - 0) * (P . P)),(0 * (Q . P))] is non empty set
{((1 - 0) * (P . P)),(0 * (Q . P))} is non empty set
{((1 - 0) * (P . P))} is non empty trivial set
{{((1 - 0) * (P . P)),(0 * (Q . P))},{((1 - 0) * (P . P))}} is non empty set
the addF of (TOP-REAL n) . [((1 - 0) * (P . P)),(0 * (Q . P))] is set
((1 - 0) * (P . P)) + (0 * (Q . P)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(P . P) + (0 * (Q . P)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) . ((P . P),(0 * (Q . P))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[(P . P),(0 * (Q . P))] is non empty set
{(P . P),(0 * (Q . P))} is non empty set
{(P . P)} is non empty trivial set
{{(P . P),(0 * (Q . P))},{(P . P)}} is non empty set
the addF of (TOP-REAL n) . [(P . P),(0 * (Q . P))] is set
(P . P) + (0 * (Q . P)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
0. (TOP-REAL n) is V1() Function-like V45(n) V54( TOP-REAL n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(P . P) + (0. (TOP-REAL n)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) . ((P . P),(0. (TOP-REAL n))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[(P . P),(0. (TOP-REAL n))] is non empty set
{(P . P),(0. (TOP-REAL n))} is non empty set
{{(P . P),(0. (TOP-REAL n))},{(P . P)}} is non empty set
the addF of (TOP-REAL n) . [(P . P),(0. (TOP-REAL n))] is set
(P . P) + (0. (TOP-REAL n)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
1 - 1 is V21() real ext-real Element of REAL
(1 - 1) * (P . P) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(1 - 1) * (P . P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
1 * (Q . P) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
1 * (Q . P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
((1 - 1) * (P . P)) + (1 * (Q . P)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) . (((1 - 1) * (P . P)),(1 * (Q . P))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[((1 - 1) * (P . P)),(1 * (Q . P))] is non empty set
{((1 - 1) * (P . P)),(1 * (Q . P))} is non empty set
{((1 - 1) * (P . P))} is non empty trivial set
{{((1 - 1) * (P . P)),(1 * (Q . P))},{((1 - 1) * (P . P))}} is non empty set
the addF of (TOP-REAL n) . [((1 - 1) * (P . P)),(1 * (Q . P))] is set
((1 - 1) * (P . P)) + (1 * (Q . P)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(0. (TOP-REAL n)) + (1 * (Q . P)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) . ((0. (TOP-REAL n)),(1 * (Q . P))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[(0. (TOP-REAL n)),(1 * (Q . P))] is non empty set
{(0. (TOP-REAL n)),(1 * (Q . P))} is non empty set
{(0. (TOP-REAL n))} is non empty trivial set
{{(0. (TOP-REAL n)),(1 * (Q . P))},{(0. (TOP-REAL n))}} is non empty set
the addF of (TOP-REAL n) . [(0. (TOP-REAL n)),(1 * (Q . P))] is set
(0. (TOP-REAL n)) + (1 * (Q . P)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(0. (TOP-REAL n)) + (Q . P) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) . ((0. (TOP-REAL n)),(Q . P)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[(0. (TOP-REAL n)),(Q . P)] is non empty set
{(0. (TOP-REAL n)),(Q . P)} is non empty set
{{(0. (TOP-REAL n)),(Q . P)},{(0. (TOP-REAL n))}} is non empty set
the addF of (TOP-REAL n) . [(0. (TOP-REAL n)),(Q . P)] is set
(0. (TOP-REAL n)) + (Q . P) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
C is V21() real ext-real Element of the carrier of I[01]
(n,P,Q) . (0,C) is set
[0,C] is non empty set
{0,C} is non empty V167() V168() V169() set
{0} is non empty trivial V167() V168() V169() V170() V171() V172() set
{{0,C},{0}} is non empty set
(n,P,Q) . [0,C] is set
(n,P,Q) . (1,C) is set
[1,C] is non empty set
{1,C} is non empty V167() V168() V169() set
{1} is non empty trivial V167() V168() V169() V170() V171() V172() set
{{1,C},{1}} is non empty set
(n,P,Q) . [1,C] is set
P . 0[01] is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
Q . 0[01] is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
1 - C is V21() real ext-real Element of REAL
(1 - C) * (P . 0[01]) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(1 - C) * (P . 0[01]) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
C * (Q . 0[01]) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C * (Q . 0[01]) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
((1 - C) * (P . 0[01])) + (C * (Q . 0[01])) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) . (((1 - C) * (P . 0[01])),(C * (Q . 0[01]))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[((1 - C) * (P . 0[01])),(C * (Q . 0[01]))] is non empty set
{((1 - C) * (P . 0[01])),(C * (Q . 0[01]))} is non empty set
{((1 - C) * (P . 0[01]))} is non empty trivial set
{{((1 - C) * (P . 0[01])),(C * (Q . 0[01]))},{((1 - C) * (P . 0[01]))}} is non empty set
the addF of (TOP-REAL n) . [((1 - C) * (P . 0[01])),(C * (Q . 0[01]))] is set
((1 - C) * (P . 0[01])) + (C * (Q . 0[01])) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
1 * a is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
1 * a is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
C * a is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C * a is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(1 * a) - (C * a) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
- (C * a) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
- (C * a) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
- 1 is V21() real ext-real non positive set
(- 1) * (C * a) is V1() Function-like set
(1 * a) + (- (C * a)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) . ((1 * a),(- (C * a))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[(1 * a),(- (C * a))] is non empty set
{(1 * a),(- (C * a))} is non empty set
{(1 * a)} is non empty trivial set
{{(1 * a),(- (C * a))},{(1 * a)}} is non empty set
the addF of (TOP-REAL n) . [(1 * a),(- (C * a))] is set
(1 * a) + (- (C * a)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(1 * a) - (C * a) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K398((C * a)) is V1() Function-like complex-valued set
K369((1 * a),K398((C * a))) is V1() Function-like set
((1 * a) - (C * a)) + (C * a) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) . (((1 * a) - (C * a)),(C * a)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[((1 * a) - (C * a)),(C * a)] is non empty set
{((1 * a) - (C * a)),(C * a)} is non empty set
{((1 * a) - (C * a))} is non empty trivial set
{{((1 * a) - (C * a)),(C * a)},{((1 * a) - (C * a))}} is non empty set
the addF of (TOP-REAL n) . [((1 * a) - (C * a)),(C * a)] is set
((1 * a) - (C * a)) + (C * a) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
P . 1[01] is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
Q . 1[01] is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(1 - C) * (P . 1[01]) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(1 - C) * (P . 1[01]) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
C * (Q . 1[01]) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C * (Q . 1[01]) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
((1 - C) * (P . 1[01])) + (C * (Q . 1[01])) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) . (((1 - C) * (P . 1[01])),(C * (Q . 1[01]))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[((1 - C) * (P . 1[01])),(C * (Q . 1[01]))] is non empty set
{((1 - C) * (P . 1[01])),(C * (Q . 1[01]))} is non empty set
{((1 - C) * (P . 1[01]))} is non empty trivial set
{{((1 - C) * (P . 1[01])),(C * (Q . 1[01]))},{((1 - C) * (P . 1[01]))}} is non empty set
the addF of (TOP-REAL n) . [((1 - C) * (P . 1[01])),(C * (Q . 1[01]))] is set
((1 - C) * (P . 1[01])) + (C * (Q . 1[01])) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
1 * b is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
1 * b is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
C * b is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C * b is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(1 * b) - (C * b) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
- (C * b) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
- (C * b) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(- 1) * (C * b) is V1() Function-like set
(1 * b) + (- (C * b)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) . ((1 * b),(- (C * b))) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[(1 * b),(- (C * b))] is non empty set
{(1 * b),(- (C * b))} is non empty set
{(1 * b)} is non empty trivial set
{{(1 * b),(- (C * b))},{(1 * b)}} is non empty set
the addF of (TOP-REAL n) . [(1 * b),(- (C * b))] is set
(1 * b) + (- (C * b)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(1 * b) - (C * b) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K398((C * b)) is V1() Function-like complex-valued set
K369((1 * b),K398((C * b))) is V1() Function-like set
((1 * b) - (C * b)) + (C * b) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) . (((1 * b) - (C * b)),(C * b)) is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
[((1 * b) - (C * b)),(C * b)] is non empty set
{((1 * b) - (C * b)),(C * b)} is non empty set
{((1 * b) - (C * b))} is non empty trivial set
{{((1 * b) - (C * b)),(C * b)},{((1 * b) - (C * b))}} is non empty set
the addF of (TOP-REAL n) . [((1 * b) - (C * b)),(C * b)] is set
((1 * b) - (C * b)) + (C * b) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
n is V21() natural real ext-real set
TOP-REAL n is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL n) is non empty set
a is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
b is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
P is V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Path of a,b
Q is V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Path of a,b
[: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):] is set
(n,P,Q) is V1() V4( the carrier of [:I[01],I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):]
y is V1() V4( the carrier of [:I[01],I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):]
P is V21() real ext-real Element of the carrier of K543()
y . (P,0) is set
[P,0] is non empty set
{P,0} is non empty V167() V168() V169() set
{P} is non empty trivial V167() V168() V169() set
{{P,0},{P}} is non empty set
y . [P,0] is set
P . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C is V21() real ext-real Element of the carrier of K543()
y . (C,1) is set
[C,1] is non empty set
{C,1} is non empty V167() V168() V169() set
{C} is non empty trivial V167() V168() V169() set
{{C,1},{C}} is non empty set
y . [C,1] is set
Q . C is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
Pa is V21() real ext-real Element of the carrier of K543()
y . (0,Pa) is set
[0,Pa] is non empty set
{0,Pa} is non empty V167() V168() V169() set
{0} is non empty trivial V167() V168() V169() V170() V171() V172() set
{{0,Pa},{0}} is non empty set
y . [0,Pa] is set
Pb is V21() real ext-real Element of the carrier of K543()
y . (1,Pb) is set
[1,Pb] is non empty set
{1,Pb} is non empty V167() V168() V169() set
{1} is non empty trivial V167() V168() V169() V170() V171() V172() set
{{1,Pb},{1}} is non empty set
y . [1,Pb] is set
n is V21() natural real ext-real set
TOP-REAL n is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL n) is non empty set
a is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
b is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
P is V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Path of a,b
Q is V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Path of a,b
y is V1() V4( the carrier of [:K543(),K543():]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Homotopy of P,Q
n is V21() natural real ext-real set
TOP-REAL n is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL n) is non empty set
a is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
((TOP-REAL n),a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of ((TOP-REAL n),a) is non empty set
((TOP-REAL n),a) is non empty set
((TOP-REAL n),a,a) is non empty set
((TOP-REAL n),a) is V1() V4(((TOP-REAL n),a)) V5(((TOP-REAL n),a)) non empty total quasi_total symmetric transitive Element of bool [:((TOP-REAL n),a),((TOP-REAL n),a):]
[:((TOP-REAL n),a),((TOP-REAL n),a):] is set
bool [:((TOP-REAL n),a),((TOP-REAL n),a):] is set
((TOP-REAL n),a,a) is V1() V4(((TOP-REAL n),a,a)) V5(((TOP-REAL n),a,a)) Element of bool [:((TOP-REAL n),a,a),((TOP-REAL n),a,a):]
[:((TOP-REAL n),a,a),((TOP-REAL n),a,a):] is set
bool [:((TOP-REAL n),a,a),((TOP-REAL n),a,a):] is set
b is V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Path of a,a
Class (((TOP-REAL n),a),b) is Element of bool ((TOP-REAL n),a)
bool ((TOP-REAL n),a) is set
{b} is non empty trivial set
((TOP-REAL n),a) .: {b} is set
{(Class (((TOP-REAL n),a),b))} is non empty trivial set
y is set
P is V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Path of a,a
Class (((TOP-REAL n),a),P) is Element of bool ((TOP-REAL n),a)
{P} is non empty trivial set
((TOP-REAL n),a) .: {P} is set
y is set
Class ((TOP-REAL n),a) is non empty V126() a_partition of ((TOP-REAL n),a)
n is V21() natural real ext-real set
TOP-REAL n is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL n) is non empty set
a is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
((TOP-REAL n),a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like constant non empty total quasi_total Path of a,a is V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like constant non empty total quasi_total Path of a,a
((TOP-REAL n),a) is V1() V4(((TOP-REAL n),a)) V5(((TOP-REAL n),a)) non empty total quasi_total symmetric transitive Element of bool [:((TOP-REAL n),a),((TOP-REAL n),a):]
((TOP-REAL n),a) is non empty set
((TOP-REAL n),a,a) is non empty set
[:((TOP-REAL n),a),((TOP-REAL n),a):] is set
bool [:((TOP-REAL n),a),((TOP-REAL n),a):] is set
((TOP-REAL n),a,a) is V1() V4(((TOP-REAL n),a,a)) V5(((TOP-REAL n),a,a)) Element of bool [:((TOP-REAL n),a,a),((TOP-REAL n),a,a):]
[:((TOP-REAL n),a,a),((TOP-REAL n),a,a):] is set
bool [:((TOP-REAL n),a,a),((TOP-REAL n),a,a):] is set
the carrier of ((TOP-REAL n),a) is non empty set
Class ((TOP-REAL n),a) is non empty V126() a_partition of ((TOP-REAL n),a)
Class (((TOP-REAL n),a), the V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like constant non empty total quasi_total Path of a,a) is Element of bool ((TOP-REAL n),a)
bool ((TOP-REAL n),a) is set
{ the V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like constant non empty total quasi_total Path of a,a} is non empty trivial set
((TOP-REAL n),a) .: { the V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like constant non empty total quasi_total Path of a,a} is set
{(Class (((TOP-REAL n),a), the V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like constant non empty total quasi_total Path of a,a))} is non empty trivial set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,a) is non empty set
b is Element of the carrier of (n,a)
(n,a) is non empty set
(n,a,a) is non empty set
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
Q is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),Q) is Element of bool (n,a)
bool (n,a) is set
{Q} is non empty trivial set
(n,a) .: {Q} is set
P is Element of the carrier of (n,a)
y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),y) is Element of bool (n,a)
{y} is non empty trivial set
(n,a) .: {y} is set
b * P is Element of the carrier of (n,a)
the multF of (n,a) is V1() V4([: the carrier of (n,a), the carrier of (n,a):]) V5( the carrier of (n,a)) Function-like total quasi_total Element of bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):]
[: the carrier of (n,a), the carrier of (n,a):] is set
[:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
the multF of (n,a) . (b,P) is Element of the carrier of (n,a)
[b,P] is non empty set
{b,P} is non empty set
{b} is non empty trivial set
{{b,P},{b}} is non empty set
the multF of (n,a) . [b,P] is set
Q + y is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),(Q + y)) is Element of bool (n,a)
{(Q + y)} is non empty trivial set
(n,a) .: {(Q + y)} is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
1_ (n,a) is Element of the carrier of (n,a)
the carrier of (n,a) is non empty set
(n,a) is non empty set
(n,a,a) is non empty set
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
b is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a
Class ((n,a),b) is Element of bool (n,a)
bool (n,a) is set
{b} is non empty trivial set
(n,a) .: {b} is set
P is Element of the carrier of (n,a)
C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),C) is Element of bool (n,a)
{C} is non empty trivial set
(n,a) .: {C} is set
C + b is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Q is Element of the carrier of (n,a)
P * Q is Element of the carrier of (n,a)
the multF of (n,a) is V1() V4([: the carrier of (n,a), the carrier of (n,a):]) V5( the carrier of (n,a)) Function-like total quasi_total Element of bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):]
[: the carrier of (n,a), the carrier of (n,a):] is set
[:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
the multF of (n,a) . (P,Q) is Element of the carrier of (n,a)
[P,Q] is non empty set
{P,Q} is non empty set
{P} is non empty trivial set
{{P,Q},{P}} is non empty set
the multF of (n,a) . [P,Q] is set
Class ((n,a),(C + b)) is Element of bool (n,a)
{(C + b)} is non empty trivial set
(n,a) .: {(C + b)} is set
b + C is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Q * P is Element of the carrier of (n,a)
the multF of (n,a) . (Q,P) is Element of the carrier of (n,a)
[Q,P] is non empty set
{Q,P} is non empty set
{Q} is non empty trivial set
{{Q,P},{Q}} is non empty set
the multF of (n,a) . [Q,P] is set
Class ((n,a),(b + C)) is Element of bool (n,a)
{(b + C)} is non empty trivial set
(n,a) .: {(b + C)} is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
(n,a) is non empty strict unital Group-like associative V229() V230() V231() V232() V233() V234() multMagma
the carrier of (n,a) is non empty set
(n,a) is non empty set
(n,a,a) is non empty set
(n,a) is V1() V4((n,a)) V5((n,a)) non empty total quasi_total symmetric transitive Element of bool [:(n,a),(n,a):]
[:(n,a),(n,a):] is set
bool [:(n,a),(n,a):] is set
(n,a,a) is V1() V4((n,a,a)) V5((n,a,a)) Element of bool [:(n,a,a),(n,a,a):]
[:(n,a,a),(n,a,a):] is set
bool [:(n,a,a),(n,a,a):] is set
Q is Element of the carrier of (n,a)
y is Element of the carrier of (n,a)
Q " is Element of the carrier of (n,a)
P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),P) is Element of bool (n,a)
bool (n,a) is set
{P} is non empty trivial set
(n,a) .: {P} is set
- P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Class ((n,a),(- P)) is Element of bool (n,a)
{(- P)} is non empty trivial set
(n,a) .: {(- P)} is set
the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a
(- P) + P is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
y * Q is Element of the carrier of (n,a)
the multF of (n,a) is V1() V4([: the carrier of (n,a), the carrier of (n,a):]) V5( the carrier of (n,a)) Function-like total quasi_total Element of bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):]
[: the carrier of (n,a), the carrier of (n,a):] is set
[:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
bool [:[: the carrier of (n,a), the carrier of (n,a):], the carrier of (n,a):] is set
the multF of (n,a) . (y,Q) is Element of the carrier of (n,a)
[y,Q] is non empty set
{y,Q} is non empty set
{y} is non empty trivial set
{{y,Q},{y}} is non empty set
the multF of (n,a) . [y,Q] is set
Class ((n,a),((- P) + P)) is Element of bool (n,a)
{((- P) + P)} is non empty trivial set
(n,a) .: {((- P) + P)} is set
Class ((n,a), the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a) is Element of bool (n,a)
{ the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a} is non empty trivial set
(n,a) .: { the V1() V4( the carrier of K543()) V5( the carrier of n) Function-like constant non empty total quasi_total Path of a,a} is set
1_ (n,a) is Element of the carrier of (n,a)
P + (- P) is V1() V4( the carrier of K543()) V5( the carrier of n) Function-like non empty total quasi_total Path of a,a
Q * y is Element of the carrier of (n,a)
the multF of (n,a) . (Q,y) is Element of the carrier of (n,a)
[Q,y] is non empty set
{Q,y} is non empty set
{Q} is non empty trivial set
{{Q,y},{Q}} is non empty set
the multF of (n,a) . [Q,y] is set
Class ((n,a),(P + (- P))) is Element of bool (n,a)
{(P + (- P))} is non empty trivial set
(n,a) .: {(P + (- P))} is set
n is V21() natural real ext-real set
TOP-REAL n is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL n) is non empty set
[: the carrier of I[01], the carrier of (TOP-REAL n):] is set
bool [: the carrier of I[01], the carrier of (TOP-REAL n):] is set
a is V1() V4( the carrier of I[01]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of (TOP-REAL n):]
b is V1() V4( the carrier of I[01]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of (TOP-REAL n):]
(n,a,b) is V1() V4( the carrier of [:I[01],I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):]
[: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):] is set
n is V21() natural real ext-real set
TOP-REAL n is non empty TopSpace-like right_complementable V179() V180() V181() V182() V183() V184() V185() V191() V219() V220() L15()
the carrier of (TOP-REAL n) is non empty set
a is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
b is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
P is V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Path of a,b
Q is V1() V4( the carrier of K543()) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Path of a,b
(n,P,Q) is V1() V4( the carrier of [:I[01],I[01]:]) V5( the carrier of (TOP-REAL n)) Function-like non empty total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):]
[: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL n):] is set
y is V21() real ext-real Element of the carrier of K543()
(n,P,Q) . (y,0) is set
[y,0] is non empty set
{y,0} is non empty V167() V168() V169() set
{y} is non empty trivial V167() V168() V169() set
{{y,0},{y}} is non empty set
(n,P,Q) . [y,0] is set
P . y is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
P is V21() real ext-real Element of the carrier of K543()
(n,P,Q) . (P,1) is set
[P,1] is non empty set
{P,1} is non empty V167() V168() V169() set
{P} is non empty trivial V167() V168() V169() set
{{P,1},{P}} is non empty set
(n,P,Q) . [P,1] is set
Q . P is V1() Function-like V45(n) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
C is V21() real ext-real Element of the carrier of K543()
(n,P,Q) . (0,C) is set
[0,C] is non empty set
{0,C} is non empty V167() V168() V169() set
{0} is non empty trivial V167() V168() V169() V170() V171() V172() set
{{0,C},{0}} is non empty set
(n,P,Q) . [0,C] is set
Pa is V21() real ext-real Element of the carrier of K543()
(n,P,Q) . (1,Pa) is set
[1,Pa] is non empty set
{1,Pa} is non empty V167() V168() V169() set
{1} is non empty trivial V167() V168() V169() V170() V171() V172() set
{{1,Pa},{1}} is non empty set
(n,P,Q) . [1,Pa] is set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
(n,a,b) is V1() V4((n,a,b)) V5((n,a,b)) Element of bool [:(n,a,b),(n,a,b):]
(n,a,b) is non empty set
[:(n,a,b),(n,a,b):] is set
bool [:(n,a,b),(n,a,b):] is set