:: 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₁ where b₁ is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{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₁ where b₁ is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{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₁ where b₁ is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT : ( 1 <= b₁ & b₁ <= len Affn ) } is set
(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₁ where b₁ is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT : ( 1 <= b₁ & b₁ <= len (Affn ^ L) ) } is set
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₂) where 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) : ( b₁ in Ek & b₂ in Pro ) } is set
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₁) where 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) : b₁ in Ek } is set
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₁ where b₁ is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
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₁ where b₁ is V21() ordinal natural real V30() V31() ext-real non negative finite cardinal V60() V61() V62() V63() V64() V65() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
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₁) where b₁ is Element of the carrier of n : b₁ in Affn } is set
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₁) where b₁ is Element of the carrier of n : b₁ in Affn } is set
(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₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite Affn -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL Affn) : b₁ | n in TRn } is set
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