:: EUCLID_9 semantic presentation

REAL is V126() V127() V128() V132() V304() V305() V307() set

NAT is non trivial ordinal non finite cardinal limit_cardinal V126() V127() V128() V129() V130() V131() V132() V304() Element of K19(REAL)

K19(REAL) is set

omega is non trivial ordinal non finite cardinal limit_cardinal V126() V127() V128() V129() V130() V131() V132() V304() set

K19(omega) is non trivial non finite set

K19(NAT) is non trivial non finite set

COMPLEX is V126() V132() set

RAT is V126() V127() V128() V129() V132() set

INT is V126() V127() V128() V129() V130() V132() set

K20(REAL,REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(REAL,REAL)) is set

K282() is non empty strict L8()

the carrier of K282() is non empty set

<REAL,+> is non empty strict V107() V108() V109() V111() left-invertible right-invertible V150() left-cancelable right-cancelable V153() L8()

K783() is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20(REAL,REAL),REAL))

K20(K20(REAL,REAL),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(K20(REAL,REAL),REAL)) is set

G8(REAL,K783()) is strict L8()

K288() is non empty strict V109() V111() left-cancelable right-cancelable V153() SubStr of <REAL,+>

<NAT,+> is non empty strict V107() V109() V111() left-cancelable right-cancelable V153() uniquely-decomposable SubStr of K288()

<REAL,*> is non empty strict V107() V109() V111() L8()

K785() is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20(REAL,REAL),REAL))

G8(REAL,K785()) is strict L8()

<NAT,*> is non empty strict V107() V109() V111() uniquely-decomposable SubStr of <REAL,*>

1 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT

K20(1,1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set

K19(K20(1,1)) is finite V49() set

K20(K20(1,1),1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set

K19(K20(K20(1,1),1)) is finite V49() set

K20(K20(1,1),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(K20(1,1),REAL)) is set

2 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT

K20(2,2) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set

K20(K20(2,2),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(K20(2,2),REAL)) is set

TOP-REAL 2 is non empty V83() constituted-Functions constituted-FinSeqs TopSpace-like V198() V199() V200() V201() V202() V203() V204() V210() L16()

the carrier of (TOP-REAL 2) is non empty set

K589() is V241() TopStruct

the carrier of K589() is V126() V127() V128() set

RealSpace is strict V241() MetrStruct

real_dist is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20(REAL,REAL),REAL))

MetrStruct(# REAL,real_dist #) is strict MetrStruct

R^1 is non empty strict TopSpace-like V241() TopStruct

TopSpaceMetr RealSpace is strict TopSpace-like TopStruct

the carrier of RealSpace is V126() V127() V128() set

Family_open_set RealSpace is Element of K19(K19( the carrier of RealSpace))

K19( the carrier of RealSpace) is set

K19(K19( the carrier of RealSpace)) is set

TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) is strict TopStruct

K596() is V241() SubSpace of R^1

K574(K596(),K596()) is strict TopSpace-like TopStruct

the carrier of K574(K596(),K596()) is set

K598() is non empty strict TopSpace-like V241() V243() SubSpace of R^1

the carrier of K598() is non empty V126() V127() V128() set

K19( the carrier of K598()) is set

K19(K19( the carrier of K598())) is set

K607(2) is non empty V244() SubSpace of TOP-REAL 2

K157((TOP-REAL 2)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite 2 -element FinSequence-like FinSubsequence-like zero Element of the carrier of (TOP-REAL 2)

K606(2,K157((TOP-REAL 2)),1) is non empty strict V244() SubSpace of TOP-REAL 2

Sphere (K157((TOP-REAL 2)),1) is non empty closed V214( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))

K19( the carrier of (TOP-REAL 2)) is set

(TOP-REAL 2) | (Sphere (K157((TOP-REAL 2)),1)) is strict SubSpace of TOP-REAL 2

the carrier of K607(2) is non empty set

K20( the carrier of K598(), the carrier of K607(2)) is Relation-like set

K19(K20( the carrier of K598(), the carrier of K607(2))) is set

K611() is Relation-like Function-like quasi_total quasi_total onto continuous Element of K19(K20( the carrier of K598(), the carrier of K607(2)))

K608() is Element of the carrier of K607(2)

0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real V43() V44() finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() Element of NAT

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() set

the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() set

|[1,0]| is Relation-like NAT -defined NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued finite 2 -element 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)

<*1*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing finite 1 -element FinSequence-like FinSubsequence-like set

[1,1] is set

{1,1} is non empty finite V49() V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() set

{1} is non empty trivial finite V49() 1 -element V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() set

{{1,1},{1}} is non empty finite V49() set

{[1,1]} is Relation-like Function-like constant non empty trivial finite 1 -element set

<*0*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing finite 1 -element FinSequence-like FinSubsequence-like Function-yielding V156() V157() set

[1,0] is set

{1,0} is non empty finite V49() V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() set

{{1,0},{1}} is non empty finite V49() set

{[1,0]} is Relation-like Function-like constant non empty trivial finite 1 -element set

K142(<*1*>,<*0*>) is Relation-like NAT -defined NAT -defined Function-like non empty complex-valued ext-real-valued real-valued finite K107(1,1) -element FinSequence-like FinSubsequence-like set

K107(1,1) is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT

K610(K608()) is non empty strict SubSpace of K607(2)

the carrier of K610(K608()) is non empty set

].0,1.[ is non empty V126() V127() V128() open V302() V303() V307() Element of K19(REAL)

R^1 ].0,1.[ is non empty V126() V127() V128() open Element of K19( the carrier of K598())

K598() | (R^1 ].0,1.[) is strict V241() SubSpace of K598()

the carrier of (K598() | (R^1 ].0,1.[)) is V126() V127() V128() set

K20( the carrier of K610(K608()), the carrier of (K598() | (R^1 ].0,1.[))) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20( the carrier of K610(K608()), the carrier of (K598() | (R^1 ].0,1.[)))) is set

K609() is Element of the carrier of K607(2)

- 1 is non empty ext-real non positive negative complex real Element of REAL

|[(- 1),0]| is Relation-like NAT -defined NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued finite 2 -element 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)

<*(- 1)*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing finite 1 -element FinSequence-like FinSubsequence-like set

[1,(- 1)] is set

{1,(- 1)} is non empty finite V126() V127() V128() V302() V303() V304() V305() V306() set

{{1,(- 1)},{1}} is non empty finite V49() set

{[1,(- 1)]} is Relation-like Function-like constant non empty trivial finite 1 -element set

K142(<*(- 1)*>,<*0*>) is Relation-like NAT -defined NAT -defined Function-like non empty complex-valued ext-real-valued real-valued finite K107(1,1) -element FinSequence-like FinSubsequence-like set

K610(K609()) is non empty strict SubSpace of K607(2)

the carrier of K610(K609()) is non empty set

1 / 2 is non empty ext-real positive non negative complex real Element of REAL

2 " is non empty ext-real positive non negative complex real set

1 * (2 ") is non empty ext-real positive non negative complex real set

3 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT

3 / 2 is non empty ext-real positive non negative complex real Element of REAL

3 * (2 ") is non empty ext-real positive non negative complex real set

].(1 / 2),(3 / 2).[ is non empty V126() V127() V128() open V302() V303() V307() Element of K19(REAL)

R^1 ].(1 / 2),(3 / 2).[ is non empty V126() V127() V128() open Element of K19( the carrier of K598())

K598() | (R^1 ].(1 / 2),(3 / 2).[) is strict V241() SubSpace of K598()

the carrier of (K598() | (R^1 ].(1 / 2),(3 / 2).[)) is V126() V127() V128() set

K20( the carrier of K610(K609()), the carrier of (K598() | (R^1 ].(1 / 2),(3 / 2).[))) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20( the carrier of K610(K609()), the carrier of (K598() | (R^1 ].(1 / 2),(3 / 2).[)))) is set

K687() is set

{{}} is functional non empty trivial finite V49() 1 -element V126() V127() V128() V129() V130() V131() complex-functions-membered V302() V303() V304() V305() V306() set

{{}} * is functional non empty FinSequence-membered FinSequenceSet of {{}}

K20(({{}} *),{{}}) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K19(K20(({{}} *),{{}})) is set

PFuncs (({{}} *),{{}}) is functional complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered set

K20(COMPLEX,COMPLEX) is Relation-like complex-valued set

K19(K20(COMPLEX,COMPLEX)) is set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like complex-valued set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set

K20(RAT,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set

K19(K20(RAT,RAT)) is set

K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set

K19(K20(K20(RAT,RAT),RAT)) is set

K20(INT,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set

K19(K20(INT,INT)) is set

K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set

K19(K20(K20(INT,INT),INT)) is set

K20(NAT,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K19(K20(K20(NAT,NAT),NAT)) is set

K20(COMPLEX,REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(COMPLEX,REAL)) is set

REAL 0 is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL

0 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL

{ b

TOP-REAL 0 is non empty V83() constituted-Functions constituted-FinSeqs TopSpace-like V198() V199() V200() V201() V202() V203() V204() V210() L16()

K157((TOP-REAL 0)) is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered zero V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() Element of the carrier of (TOP-REAL 0)

the carrier of (TOP-REAL 0) is non empty set

{K157((TOP-REAL 0))} is functional non empty trivial finite V49() 1 -element V126() V127() V128() V129() V130() V131() complex-functions-membered V302() V303() V304() V305() V306() set

the carrier of R^1 is non empty V126() V127() V128() set

K19( the carrier of R^1) is set

product {} is set

n is ext-real complex real set

J is ext-real non positive complex real set

n - J is ext-real complex real set

- J is ext-real non negative complex real set

n + (- J) is ext-real complex real set

n + J is ext-real complex real set

].(n - J),(n + J).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)

[.(n - J),(n + J).[ is V126() V127() V128() V303() V307() Element of K19(REAL)

].(n - J),(n + J).] is V126() V127() V128() V302() V307() Element of K19(REAL)

n is ext-real complex real set

J is non empty ext-real non positive negative complex real set

n - J is ext-real complex real set

- J is non empty ext-real positive non negative complex real set

n + (- J) is ext-real complex real set

n + J is ext-real complex real set

[.(n - J),(n + J).] is V126() V127() V128() closed V307() Element of K19(REAL)

n is ext-real non negative ordinal natural complex real finite cardinal set

J is Relation-like NAT -defined Function-like complex-valued finite n -element FinSequence-like FinSubsequence-like set

- J is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set

- 1 is non empty ext-real non positive negative complex real set

(- 1) (#) J is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set

dom (- J) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

len (- J) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

J " is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set

dom (J ") is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

len (J ") is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

J ^2 is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set

J (#) J is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set

dom (J ^2) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

len (J ^2) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

|.J.| is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like set

dom |.J.| is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

len |.J.| is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

PP is Relation-like NAT -defined Function-like complex-valued finite n -element FinSequence-like FinSubsequence-like set

J + PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set

dom (J + PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom PP is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

(dom J) /\ (dom PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

len PP is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

{ b

len (J + PP) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

J - PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set

- PP is Relation-like NAT -defined Function-like complex-valued finite n -element FinSequence-like FinSubsequence-like set

(- 1) (#) PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set

J + (- PP) is Relation-like NAT -defined Function-like complex-valued finite n -element FinSequence-like FinSubsequence-like set

J (#) PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set

dom (J (#) PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom PP is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

(dom J) /\ (dom PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

len PP is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

{ b

len (J (#) PP) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

J /" PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set

PP " is Relation-like NAT -defined Function-like complex-valued finite n -element FinSequence-like FinSubsequence-like set

J (#) (PP ") is Relation-like NAT -defined Function-like complex-valued finite n -element FinSequence-like FinSubsequence-like set

J is ext-real non negative ordinal natural complex real finite cardinal set

PP is Relation-like NAT -defined Function-like complex-valued finite J -element FinSequence-like FinSubsequence-like set

n is complex set

n + PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set

dom (n + PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom PP is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

len PP is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

len (n + PP) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

PP - n is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set

- n is complex set

(- n) + PP is Relation-like NAT -defined Function-like complex-valued finite J -element FinSequence-like FinSubsequence-like set

n (#) PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set

dom (n (#) PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom PP is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

len PP is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

len (n (#) PP) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

n is Relation-like Function-like complex-valued ext-real-valued real-valued set

{n} is functional non empty trivial finite 1 -element complex-functions-membered set

J is set

J is Relation-like Function-like complex-valued ext-real-valued real-valued set

{n,J} is functional non empty finite set

PP is set

n is ext-real non negative ordinal natural complex real finite cardinal set

C is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like set

J is set

PP is set

C +* (J,PP) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

dom (C +* (J,PP)) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom C is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

len (C +* (J,PP)) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

len C is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

n is ext-real non negative ordinal natural complex real finite cardinal set

J is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like set

dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

Seg 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal 0 -element {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() Element of K19(NAT)

{ b

len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

n is ext-real non negative ordinal natural complex real finite cardinal set

REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL

n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

J is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

rng J is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)

len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

n is Relation-like Function-like complex-valued set

J is Relation-like Function-like complex-valued set

n - J is Relation-like Function-like complex-valued set

- J is Relation-like Function-like complex-valued set

(- 1) (#) J is Relation-like Function-like complex-valued set

n + (- J) is Relation-like Function-like complex-valued set

|.(n - J).| is Relation-like Function-like complex-valued ext-real-valued real-valued set

J - n is Relation-like Function-like complex-valued set

- n is Relation-like Function-like complex-valued set

(- 1) (#) n is Relation-like Function-like complex-valued set

J + (- n) is Relation-like Function-like complex-valued set

|.(J - n).| is Relation-like Function-like complex-valued ext-real-valued real-valued set

- (J - n) is Relation-like Function-like complex-valued set

(- 1) (#) (J - n) is Relation-like Function-like complex-valued set

n is ext-real non negative ordinal natural complex real finite cardinal set

J is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

J - PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

- PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

(- 1) (#) PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

J + (- PP) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

abs (J - PP) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

absreal is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

(J - PP) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set

rng (abs (J - PP)) is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)

sup (rng (abs (J - PP))) is ext-real set

{(sup (rng (abs (J - PP))))} is non empty trivial finite 1 -element V127() V302() V303() set

(abs (J - PP)) " {(sup (rng (abs (J - PP))))} is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

the ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (J - PP)) " {(sup (rng (abs (J - PP))))} is ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (J - PP)) " {(sup (rng (abs (J - PP))))}

C is ext-real non negative ordinal natural complex real finite cardinal set

T is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

E is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

T - E is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

- E is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

(- 1) (#) E is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

T + (- E) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

abs (T - E) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

(T - E) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set

rng (abs (T - E)) is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)

sup (rng (abs (T - E))) is ext-real set

{(sup (rng (abs (T - E))))} is non empty trivial finite 1 -element V127() V302() V303() set

(abs (T - E)) " {(sup (rng (abs (T - E))))} is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

the ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (T - E)) " {(sup (rng (abs (T - E))))} is ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (T - E)) " {(sup (rng (abs (T - E))))}

E - T is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

- T is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

(- 1) (#) T is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

E + (- T) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

abs (E - T) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

(E - T) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set

rng (abs (E - T)) is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)

sup (rng (abs (E - T))) is ext-real set

{(sup (rng (abs (E - T))))} is non empty trivial finite 1 -element V127() V302() V303() set

(abs (E - T)) " {(sup (rng (abs (E - T))))} is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

the ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (E - T)) " {(sup (rng (abs (E - T))))} is ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (E - T)) " {(sup (rng (abs (E - T))))}

n is ext-real non negative ordinal natural complex real finite cardinal set

J is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

(n,J,PP) is ext-real non negative ordinal natural complex real finite cardinal set

J - PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

- PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

(- 1) (#) PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

J + (- PP) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

abs (J - PP) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

(J - PP) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set

rng (abs (J - PP)) is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)

sup (rng (abs (J - PP))) is ext-real set

{(sup (rng (abs (J - PP))))} is non empty trivial finite 1 -element V127() V302() V303() set

(abs (J - PP)) " {(sup (rng (abs (J - PP))))} is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

the ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (J - PP)) " {(sup (rng (abs (J - PP))))} is ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (J - PP)) " {(sup (rng (abs (J - PP))))}

Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

{ b

dom (abs (J - PP)) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

n is set

J is ext-real non negative ordinal natural complex real finite cardinal set

PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like set

C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like set

PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like FinSequence of REAL

- C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like set

(- 1) (#) C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like set

PP + (- C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like set

abs (PP - C) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like FinSequence of REAL

(PP - C) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set

(abs (PP - C)) . n is ext-real complex real set

(J,PP,C) is ext-real non negative ordinal natural complex real finite cardinal set

rng (abs (PP - C)) is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)

sup (rng (abs (PP - C))) is ext-real set

{(sup (rng (abs (PP - C))))} is non empty trivial finite 1 -element V127() V302() V303() set

(abs (PP - C)) " {(sup (rng (abs (PP - C))))} is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

the ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (PP - C)) " {(sup (rng (abs (PP - C))))} is ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (PP - C)) " {(sup (rng (abs (PP - C))))}

(abs (PP - C)) . (J,PP,C) is ext-real complex real set

dom (abs (PP - C)) is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom (PP - C) is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom PP is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom C is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

(dom PP) /\ (dom C) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

Seg J is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

{ b

(PP - C) . (J,PP,C) is ext-real complex real set

abs ((PP - C) . (J,PP,C)) is ext-real non negative complex real Element of REAL

Euclid 0 is non empty strict Reflexive discerning V192() triangle MetrStruct

Pitag_dist 0 is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL 0),(REAL 0)),REAL))

K20((REAL 0),(REAL 0)) is Relation-like set

K20(K20((REAL 0),(REAL 0)),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(K20((REAL 0),(REAL 0)),REAL)) is set

MetrStruct(# (REAL 0),(Pitag_dist 0) #) is strict MetrStruct

TopSpaceMetr (Euclid 0) is non empty strict TopSpace-like TopStruct

the carrier of (Euclid 0) is non empty set

Family_open_set (Euclid 0) is Element of K19(K19( the carrier of (Euclid 0)))

K19( the carrier of (Euclid 0)) is set

K19(K19( the carrier of (Euclid 0))) is set

TopStruct(# the carrier of (Euclid 0),(Family_open_set (Euclid 0)) #) is strict TopStruct

n is ext-real non negative ordinal natural complex real finite cardinal set

Euclid n is non empty strict Reflexive discerning V192() triangle MetrStruct

REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL

n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))

K20((REAL n),(REAL n)) is Relation-like set

K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(K20((REAL n),(REAL n)),REAL)) is set

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct

the carrier of (Euclid n) is non empty set

J is Element of the carrier of (Euclid n)

n is ext-real non negative ordinal natural complex real finite cardinal set

Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct

REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL

n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))

K20((REAL n),(REAL n)) is Relation-like set

K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(K20((REAL n),(REAL n)),REAL)) is set

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct

the carrier of (Euclid n) is non empty set

J is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)

PP is set

rng J is finite set

n is ext-real non negative ordinal natural complex real finite cardinal set

Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct

REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL

n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))

K20((REAL n),(REAL n)) is Relation-like set

K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(K20((REAL n),(REAL n)),REAL)) is set

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct

the carrier of (Euclid n) is non empty set

J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)

{{},{{}}} is non empty finite V49() set

the topology of (TOP-REAL 0) is Element of K19(K19( the carrier of (TOP-REAL 0)))

K19( the carrier of (TOP-REAL 0)) is set

K19(K19( the carrier of (TOP-REAL 0))) is set

TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #) is strict TopStruct

n is Element of K19( the carrier of (Euclid 0))

n is ext-real non negative ordinal natural complex real finite cardinal set

Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct

REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL

n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))

K20((REAL n),(REAL n)) is Relation-like set

K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(K20((REAL n),(REAL n)),REAL)) is set

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct

the carrier of (Euclid n) is non empty set

J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)

TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct

Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))

K19( the carrier of (Euclid n)) is set

K19(K19( the carrier of (Euclid n))) is set

TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct

the carrier of (TopSpaceMetr (Euclid n)) is non empty set

n is ext-real non negative ordinal natural complex real finite cardinal set

Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct

REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL

n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))

K20((REAL n),(REAL n)) is Relation-like set

K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(K20((REAL n),(REAL n)),REAL)) is set

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct

the carrier of (Euclid n) is non empty set

J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)

PP is ext-real non positive complex real set

Ball (J,PP) is Element of K19( the carrier of (Euclid n))

K19( the carrier of (Euclid n)) is set

C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)

dist (C,J) is ext-real complex real Element of REAL

the distance of (Euclid n) is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20( the carrier of (Euclid n), the carrier of (Euclid n)),REAL))

K20( the carrier of (Euclid n), the carrier of (Euclid n)) is Relation-like set

K20(K20( the carrier of (Euclid n), the carrier of (Euclid n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(K20( the carrier of (Euclid n), the carrier of (Euclid n)),REAL)) is set

the distance of (Euclid n) . (C,J) is ext-real complex real Element of REAL

n is ext-real non negative ordinal natural complex real finite cardinal set

Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct

REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL

n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))

K20((REAL n),(REAL n)) is Relation-like set

K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(K20((REAL n),(REAL n)),REAL)) is set

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct

the carrier of (Euclid n) is non empty set

J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)

PP is non empty ext-real positive non negative complex real set

Ball (J,PP) is Element of K19( the carrier of (Euclid n))

K19( the carrier of (Euclid n)) is set

n is ext-real non negative ordinal natural complex real finite cardinal set

TOP-REAL n is non empty V83() constituted-Functions constituted-FinSeqs TopSpace-like V198() V199() V200() V201() V202() V203() V204() V210() L16()

the carrier of (TOP-REAL n) is non empty set

J is ext-real non negative ordinal natural complex real finite cardinal set

PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)

dom PP is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

PP /. J is ext-real complex real Element of REAL

C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)

C /. J is ext-real complex real Element of REAL

(PP /. J) - (C /. J) is ext-real complex real Element of REAL

- (C /. J) is ext-real complex real set

(PP /. J) + (- (C /. J)) is ext-real complex real set

((PP /. J) - (C /. J)) ^2 is ext-real complex real Element of REAL

((PP /. J) - (C /. J)) * ((PP /. J) - (C /. J)) is ext-real non negative complex real set

PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)

PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

- C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

(- 1) (#) C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

PP + (- C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

sqr (PP - C) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

(PP - C) (#) (PP - C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

Sum (sqr (PP - C)) is ext-real complex real Element of REAL

E is ext-real non negative ordinal natural complex real finite cardinal set

dom (sqr (PP - C)) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

(sqr (PP - C)) . E is ext-real complex real set

(PP - C) . E is ext-real complex real set

((PP - C) . E) ^2 is ext-real complex real set

((PP - C) . E) * ((PP - C) . E) is ext-real non negative complex real set

dom (PP - C) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom C is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

(dom PP) /\ (dom C) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

{ b

PP . J is ext-real complex real set

C . J is ext-real complex real set

(sqr (PP - C)) . J is ext-real complex real set

(PP - C) . J is ext-real complex real set

((PP - C) . J) ^2 is ext-real complex real set

((PP - C) . J) * ((PP - C) . J) is ext-real non negative complex real set

n is ext-real non negative ordinal natural complex real finite cardinal set

TOP-REAL n is non empty V83() constituted-Functions constituted-FinSeqs TopSpace-like V198() V199() V200() V201() V202() V203() V204() V210() L16()

the carrier of (TOP-REAL n) is non empty set

J is ext-real complex real set

PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)

C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)

Ball (C,J) is open Element of K19( the carrier of (TOP-REAL n))

K19( the carrier of (TOP-REAL n)) is set

PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)

PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

- C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

(- 1) (#) C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

PP + (- C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

|.(PP - C).| is ext-real non negative complex real Element of REAL

sqr (PP - C) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

(PP - C) (#) (PP - C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

Sum (sqr (PP - C)) is ext-real complex real Element of REAL

sqrt (Sum (sqr (PP - C))) is ext-real complex real Element of REAL

(sqrt (Sum (sqr (PP - C)))) ^2 is ext-real complex real Element of REAL

(sqrt (Sum (sqr (PP - C)))) * (sqrt (Sum (sqr (PP - C)))) is ext-real non negative complex real set

J ^2 is ext-real complex real set

J * J is ext-real non negative complex real set

C - PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)

C - PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

- PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

(- 1) (#) PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

C + (- PP) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

sqr (C - PP) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

(C - PP) (#) (C - PP) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

E is set

(PP - C) . E is ext-real complex real set

abs ((PP - C) . E) is ext-real non negative complex real Element of REAL

PP . E is ext-real complex real set

C . E is ext-real complex real set

(PP . E) - (C . E) is ext-real complex real set

- (C . E) is ext-real complex real set

(PP . E) + (- (C . E)) is ext-real complex real set

abs ((PP . E) - (C . E)) is ext-real non negative complex real Element of REAL

dom (PP - C) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom PP is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

dom C is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

(dom PP) /\ (dom C) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

{ b

x is ext-real non negative ordinal natural complex real finite cardinal set

(PP - C) . x is ext-real complex real set

PP . x is ext-real complex real set

C . x is ext-real complex real set

(PP . x) - (C . x) is ext-real complex real set

- (C . x) is ext-real complex real set

(PP . x) + (- (C . x)) is ext-real complex real set

PP /. x is ext-real complex real Element of REAL

C /. x is ext-real complex real Element of REAL

(C . x) - (PP . x) is ext-real complex real set

- (PP . x) is ext-real complex real set

(C . x) + (- (PP . x)) is ext-real complex real set

((C . x) - (PP . x)) ^2 is ext-real complex real set

((C . x) - (PP . x)) * ((C . x) - (PP . x)) is ext-real non negative complex real set

(C /. x) - (PP /. x) is ext-real complex real Element of REAL

- (PP /. x) is ext-real complex real set

(C /. x) + (- (PP /. x)) is ext-real complex real set

((C /. x) - (PP /. x)) ^2 is ext-real complex real Element of REAL

((C /. x) - (PP /. x)) * ((C /. x) - (PP /. x)) is ext-real non negative complex real set

Sum (sqr (C - PP)) is ext-real complex real Element of REAL

(C . x) - J is ext-real complex real set

- J is ext-real complex real set

(C . x) + (- J) is ext-real complex real set

((PP . x) - (C . x)) ^2 is ext-real complex real set

((PP . x) - (C . x)) * ((PP . x) - (C . x)) is ext-real non negative complex real set

(PP /. x) - (C /. x) is ext-real complex real Element of REAL

- (C /. x) is ext-real complex real set

(PP /. x) + (- (C /. x)) is ext-real complex real set

((PP /. x) - (C /. x)) ^2 is ext-real complex real Element of REAL

((PP /. x) - (C /. x)) * ((PP /. x) - (C /. x)) is ext-real non negative complex real set

(C . x) + J is ext-real complex real set

abs (PP - C) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

(PP - C) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set

dom (abs (PP - C)) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

(abs (PP - C)) . E is ext-real complex real set

n is ext-real non negative ordinal natural complex real finite cardinal set

Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct

REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL

n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))

K20((REAL n),(REAL n)) is Relation-like set

K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(K20((REAL n),(REAL n)),REAL)) is set

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct

the carrier of (Euclid n) is non empty set

J is ext-real complex real set

PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)

C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)

Ball (C,J) is Element of K19( the carrier of (Euclid n))

K19( the carrier of (Euclid n)) is set

PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

- C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

(- 1) (#) C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

PP + (- C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

TOP-REAL n is non empty V83() constituted-Functions constituted-FinSeqs TopSpace-like V198() V199() V200() V201() V202() V203() V204() V210() L16()

the carrier of (TOP-REAL n) is non empty set

E is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)

Ball (E,J) is open Element of K19( the carrier of (TOP-REAL n))

K19( the carrier of (TOP-REAL n)) is set

T is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)

T - E is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)

T - E is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL

- E is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

(- 1) (#) E is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

T + (- E) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set

x is set

(PP - C) . x is ext-real complex real set

abs ((PP - C) . x) is ext-real non negative complex real Element of REAL

i is set

PP . i is ext-real complex real set

C . i is ext-real complex real set

(PP . i) - (C . i) is ext-real complex real set

- (C . i) is ext-real complex real set

(PP . i) + (- (C . i)) is ext-real complex real set

abs ((PP . i) - (C . i)) is ext-real non negative complex real Element of REAL

n is Relation-like Function-like complex-valued ext-real-valued real-valued set

dom n is set

J is ext-real complex real set

PP is Relation-like Function-like set

dom PP is set

PP is Relation-like Function-like set

dom PP is set

C is Relation-like Function-like set

dom C is set

T is set

PP . T is set

n . T is ext-real complex real set

(n . T) - J is ext-real complex real set

- J is ext-real complex real set

(n . T) + (- J) is ext-real complex real set

(n . T) + J is ext-real complex real set

].((n . T) - J),((n . T) + J).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)

C . T is set

n is ext-real complex real set

({},n) is Relation-like Function-like set

dom ({},n) is set

dom {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() Element of K19(NAT)

n is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like set

J is ext-real complex real set

(n,J) is Relation-like Function-like set

len n is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT

dom (n,J) is set

Seg (len n) is finite len n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

{ b

dom n is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)

n is ext-real non negative ordinal natural complex real finite cardinal set

Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct

REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL

n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

{ b

Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))

K20((REAL n),(REAL n)) is Relation-like set

K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K19(K20(