:: 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

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