:: RLAFFIN3 semantic presentation

REAL is non empty non trivial non finite V60() V61() V62() V66() set

NAT is non empty non trivial ordinal non finite cardinal limit_cardinal V60() V61() V62() V63() V64() V65() V66() Element of bool REAL

bool REAL is non empty non trivial non finite set

INT is non empty non trivial non finite V60() V61() V62() V63() V64() V66() set

COMPLEX is non empty non trivial non finite V60() V66() set

RAT is non empty non trivial non finite V60() V61() V62() V63() V66() set

[:COMPLEX,COMPLEX:] is non empty non trivial non finite complex-valued set

bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite complex-valued set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set

[:REAL,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:REAL,REAL:] is non empty non trivial non finite set

[:[:REAL,REAL:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set

[:RAT,RAT:] is RAT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:RAT,RAT:] is non empty non trivial non finite set

[:[:RAT,RAT:],RAT:] is RAT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set

[:INT,INT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:INT,INT:] is non empty non trivial non finite set

[:[:INT,INT:],INT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:INT,INT:],INT:] is non empty non trivial non finite set

[:NAT,NAT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued natural-valued set

[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued natural-valued set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

omega is non empty non trivial ordinal non finite cardinal limit_cardinal V60() V61() V62() V63() V64() V65() V66() set

bool omega is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

{} is Function-like functional empty trivial V21() ordinal natural real ext-real non positive non negative finite V39() cardinal {} -element FinSequence-membered V60() V61() V62() V63() V64() V65() V66() set

the Function-like functional empty trivial V21() ordinal natural real ext-real non positive non negative finite V39() cardinal {} -element FinSequence-membered V60() V61() V62() V63() V64() V65() V66() set is Function-like functional empty trivial V21() ordinal natural real ext-real non positive non negative finite V39() cardinal {} -element FinSequence-membered V60() V61() V62() V63() V64() V65() V66() set

2 is non empty V21() ordinal natural real V30() V31() ext-real positive non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

1 is non empty V21() ordinal natural real V30() V31() ext-real positive non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

[:1,1:] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set

bool [:1,1:] is non empty finite V39() set

[:[:1,1:],1:] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set

bool [:[:1,1:],1:] is non empty finite V39() set

[:[:1,1:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:1,1:],REAL:] is non empty non trivial non finite set

[:2,2:] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set

[:[:2,2:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:[:2,2:],REAL:] is non empty non trivial non finite set

TOP-REAL 2 is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like T_0 T_1 T_2 strict V231() V232() RLTopStruct

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

F_Real is non empty non degenerated non trivial right_complementable almost_left_invertible strict Abelian add-associative right_zeroed V199() V201() V203() right-distributive left-distributive right_unital well-unital V211() left_unital doubleLoopStr

the carrier of F_Real is non empty non trivial V60() V61() V62() set

K637() is non empty strict multMagma

the carrier of K637() is non empty set

K642() is non empty strict V199() V200() V201() V203() V241() V242() V243() V244() V245() V246() multMagma

K643() is non empty strict V201() V203() V244() V245() V246() M25(K642())

K644() is non empty strict V199() V201() V203() V244() V245() V246() V247() M28(K642(),K643())

K646() is non empty strict V199() V201() V203() multMagma

K647() is non empty strict V199() V201() V203() V247() M25(K646())

0 is Function-like functional empty trivial V21() ordinal natural real V30() V31() ext-real non positive non negative finite V39() cardinal {} -element FinSequence-membered V60() V61() V62() V63() V64() V65() V66() Element of NAT

K697(0,1,2) is non empty finite V60() V61() V62() V63() V64() V65() set

[:K697(0,1,2),K697(0,1,2):] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set

[:[:K697(0,1,2),K697(0,1,2):],K697(0,1,2):] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set

bool [:[:K697(0,1,2),K697(0,1,2):],K697(0,1,2):] is non empty finite V39() set

bool [:K697(0,1,2),K697(0,1,2):] is non empty finite V39() set

[:NAT,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set

bool [:NAT,REAL:] is non empty non trivial non finite set

K860() is V283() TopStruct

the carrier of K860() is V60() V61() V62() set

RealSpace is strict V283() MetrStruct

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

Euclid 0 is non empty strict Reflexive discerning V173() triangle V231() V232() MetrStruct

TopSpaceMetr (Euclid 0) is trivial finite TopStruct

3 is non empty V21() ordinal natural real V30() V31() ext-real positive non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

the carrier of R^1 is non empty V60() V61() V62() set

bool the carrier of R^1 is non empty set

-infty is non empty non real ext-real non positive negative set

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

TOP-REAL 0 is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like T_0 T_1 T_2 strict V231() V232() RLTopStruct

0. (TOP-REAL 0) is Relation-like NAT -defined REAL -valued Function-like one-to-one constant functional empty trivial V21() ordinal natural real ext-real non positive non negative finite finite-yielding V39() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V60() V61() V62() V63() V64() V65() V66() zero Element of the carrier of (TOP-REAL 0)

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

the ZeroF of (TOP-REAL 0) is Relation-like NAT -defined REAL -valued Function-like one-to-one constant functional empty trivial V21() ordinal natural real ext-real non positive non negative finite finite-yielding V39() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V60() V61() V62() V63() V64() V65() V66() Element of the carrier of (TOP-REAL 0)

{(0. (TOP-REAL 0))} is functional non empty trivial finite V39() 1 -element V60() V61() V62() V63() V64() V65() set

Seg 1 is non empty trivial finite 1 -element V60() V61() V62() V63() V64() V65() with_non-empty_elements Element of bool NAT

{ b

{1} is non empty trivial finite V39() 1 -element V60() V61() V62() V63() V64() V65() set

Seg 2 is non empty finite 2 -element V60() V61() V62() V63() V64() V65() with_non-empty_elements Element of bool NAT

{ b

{1,2} is non empty finite V39() V60() V61() V62() V63() V64() V65() set

TOP-REAL 1 is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like T_0 T_1 T_2 strict V231() V232() RLTopStruct

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

[: the carrier of (TOP-REAL 1), the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set

bool [: the carrier of (TOP-REAL 1), the carrier of R^1:] is non empty set

the carrier of F_Real * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real

0. F_Real is V21() real ext-real zero Element of the carrier of F_Real

the ZeroF of F_Real is V21() real ext-real Element of the carrier of F_Real

- 1 is V21() real V30() V31() ext-real non positive Element of INT

K143() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

K145() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

doubleLoopStr(# REAL,K143(),K145(),1,0 #) is strict doubleLoopStr

n is V21() ordinal natural real ext-real non negative finite cardinal set

TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like T_0 T_1 T_2 strict V231() V232() RLTopStruct

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

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

len Affn is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

@ Affn is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real

@ (@ Affn) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

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

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

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

L is V21() real ext-real set

Intervals (n,L) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Intervals (Affn,L) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(Intervals (n,L)) ^ (Intervals (Affn,L)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Intervals ((n ^ Affn),L) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

dom (Intervals ((n ^ Affn),L)) is finite V60() V61() V62() V63() V64() V65() Element of bool NAT

dom (n ^ Affn) is finite V60() V61() V62() V63() V64() V65() Element of bool NAT

len (n ^ Affn) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

len n is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

len Affn is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

(len n) + (len Affn) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

len ((Intervals (n,L)) ^ (Intervals (Affn,L))) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

len (Intervals (n,L)) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

len (Intervals (Affn,L)) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

(len (Intervals (n,L))) + (len (Intervals (Affn,L))) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

dom (Intervals (n,L)) is finite V60() V61() V62() V63() V64() V65() Element of bool NAT

dom n is finite V60() V61() V62() V63() V64() V65() Element of bool NAT

dom (Intervals (Affn,L)) is finite V60() V61() V62() V63() V64() V65() Element of bool NAT

dom Affn is finite V60() V61() V62() V63() V64() V65() Element of bool NAT

dom ((Intervals (n,L)) ^ (Intervals (Affn,L))) is finite V60() V61() V62() V63() V64() V65() Element of bool NAT

f is V21() ordinal natural real ext-real non negative finite cardinal set

(Intervals ((n ^ Affn),L)) . f is set

(n ^ Affn) . f is V21() real ext-real set

((n ^ Affn) . f) - L is V21() real ext-real Element of REAL

((n ^ Affn) . f) + L is V21() real ext-real Element of REAL

].(((n ^ Affn) . f) - L),(((n ^ Affn) . f) + L).[ is V60() V61() V62() Element of bool REAL

((Intervals (n,L)) ^ (Intervals (Affn,L))) . f is set

(Intervals (n,L)) . f is set

n . f is V21() real ext-real set

f is V21() ordinal natural real ext-real non negative finite cardinal set

(len (Intervals (n,L))) + f is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

f is V21() ordinal natural real ext-real non negative finite cardinal set

(len (Intervals (n,L))) + f is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

((Intervals (n,L)) ^ (Intervals (Affn,L))) . f is set

(Intervals (Affn,L)) . f is set

Affn . f is V21() real ext-real set

n is set

Affn is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

L is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Affn ^ L is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

product (Affn ^ L) is set

product Affn is set

product L is set

len (Affn ^ L) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

len Affn is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

len L is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

(len Affn) + (len L) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

dom Affn is finite V60() V61() V62() V63() V64() V65() Element of bool NAT

Seg (len Affn) is finite len Affn -element V60() V61() V62() V63() V64() V65() with_non-empty_elements Element of bool NAT

{ b

(Affn ^ L) | (Seg (len Affn)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set

dom (Affn ^ L) is finite V60() V61() V62() V63() V64() V65() Element of bool NAT

A is Relation-like Function-like set

dom A is set

Seg (len (Affn ^ L)) is finite len (Affn ^ L) -element V60() V61() V62() V63() V64() V65() with_non-empty_elements Element of bool NAT

{ b

L is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

L | (len Affn) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

L | (Seg (len Affn)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(L | (len Affn)) ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f ^ B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len L is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

len f is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

len B is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

(len f) + (len B) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

dom L is finite V60() V61() V62() V63() V64() V65() Element of bool NAT

dom B is finite V60() V61() V62() V63() V64() V65() Element of bool NAT

k is set

Y is V21() ordinal natural real ext-real non negative finite cardinal set

Y + (len Affn) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

L . (Y + (len Affn)) is set

(Affn ^ L) . (Y + (len Affn)) is set

L . Y is set

B . k is set

L . k is set

A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

L is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

A ^ L is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len A is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

E is Relation-like Function-like set

dom E is set

E is set

f is V21() ordinal natural real ext-real non negative finite cardinal set

(Affn ^ L) . E is set

Affn . f is set

(A ^ L) . E is set

A . f is set

f is Relation-like Function-like set

dom f is set

f is Relation-like Function-like set

dom f is set

f is V21() ordinal natural real ext-real non negative finite cardinal set

f is V21() ordinal natural real ext-real non negative finite cardinal set

(len Affn) + f is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

f is V21() ordinal natural real ext-real non negative finite cardinal set

(len Affn) + f is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

(Affn ^ L) . E is set

L . f is set

(A ^ L) . E is set

L . f is set

B is Relation-like Function-like set

dom B is set

B is Relation-like Function-like set

dom B is set

f is V21() ordinal natural real ext-real non negative finite cardinal set

len (A ^ L) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

len L is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

(len A) + (len L) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

E is Relation-like Function-like set

dom E is set

dom (A ^ L) is finite V60() V61() V62() V63() V64() V65() Element of bool NAT

n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of n is non empty set

bool the carrier of n is non empty set

0. n is zero Element of the carrier of n

the ZeroF of n is Element of the carrier of n

{(0. n)} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of n

Affn is Element of bool the carrier of n

Lin Affn is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n

Affn \ {(0. n)} is Element of bool the carrier of n

Lin (Affn \ {(0. n)}) is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n

(0). n is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n

the carrier of ((0). n) is non empty set

Lin {(0. n)} is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n

(Affn \ {(0. n)}) \/ {(0. n)} is non empty Element of bool the carrier of n

(Lin (Affn \ {(0. n)})) + ((0). n) is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n

n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

(Omega). n is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n

the carrier of ((Omega). n) is non empty set

bool the carrier of ((Omega). n) is non empty set

L is finite Element of bool the carrier of ((Omega). n)

the carrier of n is non empty set

the ZeroF of n is Element of the carrier of n

the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

[: the carrier of n, the carrier of n:] is non empty set

[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set

bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set

the Mult of n is Relation-like [:REAL, the carrier of n:] -defined the carrier of n -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of n:], the carrier of n:]

[:REAL, the carrier of n:] is non empty non trivial non finite set

[:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial non finite set

bool [:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial non finite set

RLSStruct(# the carrier of n, the ZeroF of n, the addF of n, the Mult of n #) is strict RLSStruct

bool the carrier of n is non empty set

Lin L is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of (Omega). n

TRn is finite Element of bool the carrier of n

Lin TRn is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n

n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional RLSStruct

the carrier of n is non empty set

bool the carrier of n is non empty set

Affn is affinely-independent Element of bool the carrier of n

0. n is zero Element of the carrier of n

the ZeroF of n is Element of the carrier of n

{(0. n)} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of n

L is Element of the carrier of n

- L is Element of the carrier of n

(- L) + Affn is affinely-independent Element of bool the carrier of n

((- L) + Affn) \ {(0. n)} is Element of bool the carrier of n

(((- L) + Affn) \ {(0. n)}) \/ {(0. n)} is non empty Element of bool the carrier of n

((- L) + Affn) \/ {(0. n)} is non empty Element of bool the carrier of n

card ((- L) + Affn) is ordinal cardinal set

card Affn is ordinal cardinal set

n is V21() ordinal natural real ext-real non negative finite cardinal set

TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like T_0 T_1 T_2 strict V231() V232() RLTopStruct

Euclid n is non empty strict Reflexive discerning V173() triangle V231() V232() MetrStruct

TopSpaceMetr (Euclid n) is TopStruct

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

the topology of (TOP-REAL n) is non empty Element of bool (bool the carrier of (TOP-REAL n))

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

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

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct

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

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

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

A + L is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

E is functional Element of bool the carrier of (TOP-REAL n)

the carrier of (Euclid n) is non empty set

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

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

k is Element of bool the carrier of (TopSpaceMetr (Euclid n))

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

Y is V21() real ext-real set

Ball (B,Y) is Element of bool the carrier of (Euclid n)

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

Y / 2 is V21() real ext-real Element of REAL

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

Ball (f,(Y / 2)) is Element of bool the carrier of (Euclid n)

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

Ball (f,(Y / 2)) is Element of bool the carrier of (Euclid n)

Ek is functional Element of bool the carrier of (TOP-REAL n)

Pro is functional Element of bool the carrier of (TOP-REAL n)

Ek + Pro is functional Element of bool the carrier of (TOP-REAL n)

P is set

Ek + Pro is functional Element of bool the carrier of (TOP-REAL n)

{ (b

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

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

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

B + y is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

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

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

dist (f,yP1) is V21() real ext-real Element of REAL

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

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

w - MT is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

|.(w - MT).| is V21() real ext-real non negative Element of REAL

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

dist (f,yP) is V21() real ext-real Element of REAL

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

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

x - MT1 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

|.(x - MT1).| is V21() real ext-real non negative Element of REAL

(Y / 2) + (Y / 2) is V21() real ext-real Element of REAL

|.(x - MT1).| + |.(w - MT).| is V21() real ext-real non negative Element of REAL

x + w is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

MT1 + MT is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(x + w) - (MT1 + MT) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

MT + MT1 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

- (MT + MT1) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(x + w) + (- (MT + MT1)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

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

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

(- MT) + (- MT1) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(x + w) + ((- MT) + (- MT1)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(x + w) + (- MT) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

((x + w) + (- MT)) + (- MT1) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

w + (- MT) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(w + (- MT)) + x is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

((w + (- MT)) + x) + (- MT1) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

x + (- MT1) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(w + (- MT)) + (x + (- MT1)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(w - MT) + (x + (- MT1)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(w - MT) + (x - MT1) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

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

dist (B,vP1) is V21() real ext-real Element of REAL

(x - MT1) + (w - MT) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

|.((x - MT1) + (w - MT)).| is V21() real ext-real non negative Element of REAL

A is V21() real ext-real Element of REAL

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

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

A * L is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

E is functional Element of bool the carrier of (TOP-REAL n)

the carrier of (Euclid n) is non empty set

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

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

B is Element of bool the carrier of (TopSpaceMetr (Euclid n))

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

k is V21() real ext-real set

Ball (f,k) is Element of bool the carrier of (Euclid n)

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

k / 2 is V21() real ext-real Element of REAL

(k / 2) / 2 is V21() real ext-real Element of REAL

abs A is V21() real ext-real Element of REAL

(abs A) * 1 is V21() real ext-real Element of REAL

((k / 2) / 2) / (abs A) is V21() real ext-real Element of REAL

k is non empty V21() real ext-real positive non negative Element of REAL

(abs A) * k is V21() real ext-real Element of REAL

k is non empty V21() real ext-real positive non negative Element of REAL

(abs A) * k is V21() real ext-real Element of REAL

k is non empty V21() real ext-real positive non negative Element of REAL

(abs A) * k is V21() real ext-real Element of REAL

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

Ball (f,k) is non empty Element of bool the carrier of (Euclid n)

|.L.| is V21() real ext-real non negative Element of REAL

|.L.| + k is non empty V21() real ext-real positive non negative Element of REAL

(k / 2) / (|.L.| + k) is V21() real ext-real Element of REAL

Pro is non empty V21() real ext-real positive non negative Element of REAL

Ek is functional Element of bool the carrier of (TOP-REAL n)

P is V21() real ext-real Element of REAL

P - A is V21() real ext-real Element of REAL

abs (P - A) is V21() real ext-real Element of REAL

P * Ek is functional Element of bool the carrier of (TOP-REAL n)

P - A is V21() real ext-real Element of REAL

abs (P - A) is V21() real ext-real Element of REAL

B is set

{ (P * b

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

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

P * y is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

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

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

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

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

MT1 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL

n |-> {} is Relation-like empty-yielding NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

MT1 - (n |-> {}) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

w is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL

w - w is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL

MT1 - (w - w) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL

MT1 - w is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL

(MT1 - w) + w is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL

|.x.| is V21() real ext-real non negative Element of REAL

x - vP1 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

|.(x - vP1).| is V21() real ext-real non negative Element of REAL

|.vP1.| is V21() real ext-real non negative Element of REAL

|.(x - vP1).| + |.vP1.| is V21() real ext-real non negative Element of REAL

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

dist (f,yP) is V21() real ext-real Element of REAL

k + |.L.| is non empty V21() real ext-real positive non negative Element of REAL

Pro * |.x.| is V21() real ext-real non negative Element of REAL

Pro * (k + |.L.|) is V21() real ext-real non negative Element of REAL

A * vP1 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

A * x is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

- (A * x) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(A * vP1) + (- (A * x)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(- 1) * (A * x) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(A * vP1) + ((- 1) * (A * x)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(- 1) * A is V21() real ext-real Element of REAL

((- 1) * A) * x is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(A * vP1) + (((- 1) * A) * x) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(- 1) * x is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

A * ((- 1) * x) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(A * vP1) + (A * ((- 1) * x)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

vP1 + ((- 1) * x) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

A * (vP1 + ((- 1) * x)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

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

vP1 + (- x) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

A * (vP1 + (- x)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

vP1 - x is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

A * (vP1 - x) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

|.((A * vP1) + (- (A * x))).| is V21() real ext-real non negative Element of REAL

|.(vP1 - x).| is V21() real ext-real non negative Element of REAL

(abs A) * |.(vP1 - x).| is V21() real ext-real Element of REAL

P * x is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

- (P * x) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(A * x) + (- (P * x)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(- 1) * (P * x) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(A * x) + ((- 1) * (P * x)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(- 1) * P is V21() real ext-real Element of REAL

((- 1) * P) * x is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

(A * x) + (((- 1) * P) * x) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

A + ((- 1) * P) is V21() real ext-real Element of REAL

(A + ((- 1) * P)) * x is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

|.((A * x) + (- (P * x))).| is V21() real ext-real non negative Element of REAL

A - P is V21() real ext-real Element of REAL

abs (A - P) is V21() real ext-real Element of REAL

(abs (A - P)) * |.x.| is V21() real ext-real Element of REAL

- (A - P) is V21() real ext-real Element of REAL

abs (- (A - P)) is V21() real ext-real Element of REAL

(abs (- (A - P))) * |.x.| is V21() real ext-real Element of REAL

Pro * (|.L.| + k) is V21() real ext-real non negative Element of REAL

((A * vP1) + (- (A * x))) + ((A * x) + (- (P * x))) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

|.(((A * vP1) + (- (A * x))) + ((A * x) + (- (P * x)))).| is V21() real ext-real non negative Element of REAL

|.((A * vP1) + (- (A * x))).| + |.((A * x) + (- (P * x))).| is V21() real ext-real non negative Element of REAL

(k / 2) + (k / 2) is V21() real ext-real Element of REAL

(A * vP1) - (P * x) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL n

A * w is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL

(A * w) - (n |-> {}) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

P * MT1 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL

((A * w) - (n |-> {})) - (P * MT1) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

A * MT1 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL

(A * MT1) - (A * MT1) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on REAL

(A * vP1) - ((A * MT1) - (A * MT1)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

((A * vP1) - ((A * MT1) - (A * MT1))) - (P * x) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(A * vP1) - (A * MT1) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

((A * vP1) - (A * MT1)) + (A * MT1) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(((A * vP1) - (A * MT1)) + (A * MT1)) - (P * x) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

(((A * vP1) - (A * MT1)) + (A * MT1)) + (- (P * x)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

((A * vP1) - (A * MT1)) + ((A * x) + (- (P * x))) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

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

dist (f,yP1) is V21() real ext-real Element of REAL

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

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

the addF of (TOP-REAL n) is Relation-like [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] -defined the carrier of (TOP-REAL n) -valued Function-like 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 non empty set

[:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is non empty set

bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is non empty set

the Mult of (TOP-REAL n) is Relation-like [:REAL, the carrier of (TOP-REAL n):] -defined the carrier of (TOP-REAL n) -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):]

[:REAL, the carrier of (TOP-REAL n):] is non empty non trivial non finite set

[:[:REAL, the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is non empty non trivial non finite set

bool [:[:REAL, the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is non empty non trivial non finite set

RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) is strict RLSStruct

Seg n is finite n -element V60() V61() V62() V63() V64() V65() with_non-empty_elements Element of bool NAT

{ b

RealVectSpace (Seg n) is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V231() V232() finite-dimensional RLSStruct

(Omega). (TOP-REAL n) is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of TOP-REAL n

n is V21() ordinal natural real ext-real non negative finite cardinal set

TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like T_0 T_1 T_2 strict add-continuous Mult-continuous V231() V232() finite-dimensional RLTopStruct

dim (TOP-REAL n) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

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

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

the addF of (TOP-REAL n) is Relation-like [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] -defined the carrier of (TOP-REAL n) -valued Function-like 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 non empty set

[:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is non empty set

bool [:[: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is non empty set

the Mult of (TOP-REAL n) is Relation-like [:REAL, the carrier of (TOP-REAL n):] -defined the carrier of (TOP-REAL n) -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):]

[:REAL, the carrier of (TOP-REAL n):] is non empty non trivial non finite set

[:[:REAL, the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is non empty non trivial non finite set

bool [:[:REAL, the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is non empty non trivial non finite set

RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) is strict RLSStruct

Seg n is finite n -element V60() V61() V62() V63() V64() V65() with_non-empty_elements Element of bool NAT

{ b

RealVectSpace (Seg n) is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V231() V232() finite-dimensional RLSStruct

(Omega). (TOP-REAL n) is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of TOP-REAL n

dim ((Omega). (TOP-REAL n)) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional RLSStruct

the carrier of n is non empty set

bool the carrier of n is non empty set

dim n is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

1 + (dim n) is non empty V21() ordinal natural real V30() V31() ext-real positive non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

Affn is finite affinely-independent Element of bool the carrier of n

card Affn is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of omega

0. n is zero Element of the carrier of n

the ZeroF of n is Element of the carrier of n

{(0. n)} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of n

L is Element of the carrier of n

- L is Element of the carrier of n

(- L) + Affn is finite affinely-independent Element of bool the carrier of n

((- L) + Affn) \ {(0. n)} is finite Element of bool the carrier of n

card {(0. n)} is non empty V21() ordinal natural real V30() V31() ext-real positive non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of omega

(((- L) + Affn) \ {(0. n)}) \/ {(0. n)} is non empty finite Element of bool the carrier of n

card ((((- L) + Affn) \ {(0. n)}) \/ {(0. n)}) is non empty V21() ordinal natural real V30() V31() ext-real positive non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of omega

card (((- L) + Affn) \ {(0. n)}) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of omega

(card (((- L) + Affn) \ {(0. n)})) + (card {(0. n)}) is non empty V21() ordinal natural real V30() V31() ext-real positive non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

card ((- L) + Affn) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of omega

A is finite set

A \ {(0. n)} is finite Element of bool A

bool A is non empty finite V39() set

card (A \ {(0. n)}) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of omega

Lin (((- L) + Affn) \ {(0. n)}) is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of n

dim (Lin (((- L) + Affn) \ {(0. n)})) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

(A \ {(0. n)}) \/ {(0. n)} is non empty finite set

card ((A \ {(0. n)}) \/ {(0. n)}) is non empty V21() ordinal natural real V30() V31() ext-real positive non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of omega

A \/ {(0. n)} is non empty finite set

n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional RLSStruct

the carrier of n is non empty set

bool the carrier of n is non empty set

dim n is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

(dim n) + 1 is non empty V21() ordinal natural real V30() V31() ext-real positive non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

[#] n is non empty non proper Element of bool the carrier of n

Affn is finite affinely-independent Element of bool the carrier of n

card Affn is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of omega

Affin Affn is Affine Element of bool the carrier of n

0. n is zero Element of the carrier of n

the ZeroF of n is Element of the carrier of n

{(0. n)} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of n

L is Element of the carrier of n

- L is Element of the carrier of n

(- L) + Affn is finite affinely-independent Element of bool the carrier of n

((- L) + Affn) \ {(0. n)} is finite Element of bool the carrier of n

(- L) + L is Element of the carrier of n

{ ((- L) + b

A is finite Element of bool the carrier of n

card A is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of omega

card {(0. n)} is non empty V21() ordinal natural real V30() V31() ext-real positive non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of omega

A \ {(0. n)} is finite Element of bool the carrier of n

(A \ {(0. n)}) \/ {(0. n)} is non empty finite Element of bool the carrier of n

card (A \ {(0. n)}) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of omega

(card (A \ {(0. n)})) + 1 is non empty V21() ordinal natural real V30() V31() ext-real positive non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

Lin (A \ {(0. n)}) is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of n

dim (Lin (A \ {(0. n)})) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

(Omega). n is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of n

(Omega). (Lin (A \ {(0. n)})) is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of Lin (A \ {(0. n)})

the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

[: the carrier of n, the carrier of n:] is non empty set

[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set

bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set

the Mult of n is Relation-like [:REAL, the carrier of n:] -defined the carrier of n -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of n:], the carrier of n:]

[:REAL, the carrier of n:] is non empty non trivial non finite set

[:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial non finite set

bool [:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial non finite set

RLSStruct(# the carrier of n, the ZeroF of n, the addF of n, the Mult of n #) is strict RLSStruct

Lin A is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of n

the carrier of (Lin A) is non empty set

L + (Lin A) is Element of bool the carrier of n

Up (Lin A) is non empty Element of bool the carrier of n

L + (Up (Lin A)) is Element of bool the carrier of n

L is Element of the carrier of n

- L is Element of the carrier of n

(- L) + Affn is finite affinely-independent Element of bool the carrier of n

((- L) + Affn) \ {(0. n)} is finite Element of bool the carrier of n

A is finite Element of bool the carrier of n

Lin A is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of n

Up (Lin A) is non empty Element of bool the carrier of n

L + (Up (Lin A)) is Element of bool the carrier of n

L + (Lin A) is Element of bool the carrier of n

[#] (Lin A) is non empty non proper Element of bool the carrier of (Lin A)

the carrier of (Lin A) is non empty set

bool the carrier of (Lin A) is non empty set

the carrier of RLSStruct(# the carrier of n, the ZeroF of n, the addF of n, the Mult of n #) is set

the carrier of ((Omega). n) is non empty set

A \ {(0. n)} is finite Element of bool the carrier of n

Lin (A \ {(0. n)}) is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of n

(- L) + L is Element of the carrier of n

{ ((- L) + b

(A \ {(0. n)}) \/ {(0. n)} is non empty finite Element of bool the carrier of n

card A is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of omega

card (A \ {(0. n)}) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of omega

(card (A \ {(0. n)})) + 1 is non empty V21() ordinal natural real V30() V31() ext-real positive non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

n is V21() ordinal natural real ext-real non negative finite cardinal set

TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like T_0 T_1 T_2 strict add-continuous Mult-continuous V231() V232() finite-dimensional RLTopStruct

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

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

Affn is V21() ordinal natural real ext-real non negative finite cardinal set

TOP-REAL Affn is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like T_0 T_1 T_2 strict add-continuous Mult-continuous V231() V232() finite-dimensional RLTopStruct

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

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

L is functional Element of bool the carrier of (TOP-REAL Affn)

TRn is functional Element of bool the carrier of (TOP-REAL n)

{ b

Affn - n is V21() real ext-real Element of REAL

the topology of (TOP-REAL Affn) is non empty Element of bool (bool the carrier of (TOP-REAL Affn))

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

TopStruct(# the carrier of (TOP-REAL Affn), the topology of (TOP-REAL Affn) #) is non empty strict TopSpace-like TopStruct

Euclid Affn is non empty strict Reflexive discerning V173() triangle V231() V232() MetrStruct

TopSpaceMetr (Euclid Affn) is TopStruct

the carrier of (TopSpaceMetr (Euclid Affn)) is set

bool the carrier of (TopSpaceMetr (Euclid Affn)) is non empty set

the topology of (TOP-REAL n) is non empty Element of bool (bool the carrier of (TOP-REAL n))

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

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct

Euclid n is non empty strict Reflexive discerning V173() triangle V231() V232() MetrStruct

TopSpaceMetr (Euclid n) is TopStruct

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

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

L is Element of bool the carrier of (TopSpaceMetr (Euclid Affn))

the carrier of (Euclid n) is non empty set

E is Element of bool the carrier of (TopSpaceMetr (Euclid n))

A is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

A |-> {} is Relation-like empty-yielding NAT -defined Function-like finite A -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

len (A |-> {}) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

@ (A |-> {}) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real

@ (@ (A |-> {})) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

Euclid A is non empty strict Reflexive discerning V173() triangle V231() V232() MetrStruct

the carrier of (Euclid A) is non empty set

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

f ^ (A |-> {}) is Relation-like NAT -defined Function-like finite K194(n,A) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set

K194(n,A) is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT

@ (f ^ (A |-> {})) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real

@ (@ (f ^ (A |-> {}))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued