REAL is non empty non trivial non finite set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL
bool REAL is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal set
bool omega is non empty set
bool NAT is non empty set
COMPLEX is non empty non trivial non finite set
RAT is non empty non trivial non finite set
INT is non empty non trivial non finite set
[:REAL,REAL:] is Relation-like non empty set
bool [:REAL,REAL:] is non empty set
K281() is non empty V72() L8()
the carrier of K281() is non empty set
K286() is non empty V72() V94() V95() V96() V98() V148() V149() V150() V151() V152() V153() L8()
K287() is non empty V72() V96() V98() V151() V152() V153() M13(K286())
K288() is non empty V72() V94() V96() V98() V151() V152() V153() V154() M16(K286(),K287())
K290() is non empty V72() V94() V96() V98() L8()
K291() is non empty V72() V94() V96() V98() V154() M13(K290())
1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative Element of NAT
[:1,1:] is Relation-like non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is Relation-like non empty set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is Relation-like non empty set
bool [:[:1,1:],REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is Relation-like non empty set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative Element of NAT
[:2,2:] is Relation-like non empty set
[:[:2,2:],REAL:] is Relation-like non empty set
bool [:[:2,2:],REAL:] is non empty set
TOP-REAL 2 is non empty V70() V138() V139() TopSpace-like T_0 T_1 T_2 Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous V234() second-countable finite-dimensional 2 -locally_euclidean 2 -manifold manifold-like RLTopStruct
the carrier of (TOP-REAL 2) is functional non empty set
K463() is V226() TopStruct
the carrier of K463() is V128() set
RealSpace is non empty strict Reflexive discerning V177() triangle Discerning V226() MetrStruct
R^1 is non empty strict TopSpace-like V226() TopStruct
K470() is TopSpace-like V226() SubSpace of R^1
K448(K470(),K470()) is strict TopSpace-like TopStruct
the carrier of K448(K470(),K470()) is set
K472() is non empty strict TopSpace-like V226() V228() SubSpace of R^1
the carrier of K472() is non empty V128() set
bool the carrier of K472() is non empty set
bool (bool the carrier of K472()) is non empty set
Tunit_circle 2 is non empty TopSpace-like T_0 T_1 T_2 V229() SubSpace of TOP-REAL 2
the carrier of (Tunit_circle 2) is non empty set
[: the carrier of K472(), the carrier of (Tunit_circle 2):] is Relation-like non empty set
bool [: the carrier of K472(), the carrier of (Tunit_circle 2):] is non empty set
CircleMap is Relation-like the carrier of K472() -defined the carrier of K472() -defined the carrier of (Tunit_circle 2) -valued the carrier of (Tunit_circle 2) -valued Function-like non empty total total quasi_total quasi_total onto continuous Element of bool [: the carrier of K472(), the carrier of (Tunit_circle 2):]
c[10] is Element of the carrier of (Tunit_circle 2)
Topen_unit_circle c[10] is non empty strict TopSpace-like T_0 T_1 T_2 V240( Tunit_circle 2) SubSpace of Tunit_circle 2
the carrier of (Topen_unit_circle c[10]) is non empty set
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real finite finite-yielding V36() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-yielding V117() V118() V119() R-orthogonal R-normal R-orthonormal Element of NAT
K386(0,1) is non empty Element of bool REAL
R^1 K386(0,1) is non empty Element of bool the carrier of K472()
K472() | (R^1 K386(0,1)) is non empty strict TopSpace-like V226() SubSpace of K472()
the carrier of (K472() | (R^1 K386(0,1))) is non empty V128() set
[: the carrier of (Topen_unit_circle c[10]), the carrier of (K472() | (R^1 K386(0,1))):] is Relation-like non empty complex-yielding V117() V118() set
bool [: the carrier of (Topen_unit_circle c[10]), the carrier of (K472() | (R^1 K386(0,1))):] is non empty set
c[-10] is Element of the carrier of (Tunit_circle 2)
Topen_unit_circle c[-10] is non empty strict TopSpace-like T_0 T_1 T_2 V240( Tunit_circle 2) SubSpace of Tunit_circle 2
the carrier of (Topen_unit_circle c[-10]) is non empty set
1 / 2 is non empty V21() real ext-real positive non negative Element of REAL
3 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative Element of NAT
3 / 2 is non empty V21() real ext-real positive non negative Element of REAL
K386((1 / 2),(3 / 2)) is non empty Element of bool REAL
R^1 K386((1 / 2),(3 / 2)) is non empty Element of bool the carrier of K472()
K472() | (R^1 K386((1 / 2),(3 / 2))) is non empty strict TopSpace-like V226() SubSpace of K472()
the carrier of (K472() | (R^1 K386((1 / 2),(3 / 2)))) is non empty V128() set
[: the carrier of (Topen_unit_circle c[-10]), the carrier of (K472() | (R^1 K386((1 / 2),(3 / 2)))):] is Relation-like non empty complex-yielding V117() V118() set
bool [: the carrier of (Topen_unit_circle c[-10]), the carrier of (K472() | (R^1 K386((1 / 2),(3 / 2)))):] is non empty set
[:COMPLEX,COMPLEX:] is Relation-like non empty set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:RAT,RAT:] is Relation-like non empty set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is Relation-like non empty set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is Relation-like non empty set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is Relation-like non empty set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is Relation-like non empty set
[:[:NAT,NAT:],NAT:] is Relation-like non empty set
bool [:[:NAT,NAT:],NAT:] is non empty set
F_Real is non empty non degenerated non trivial V70() almost_left_invertible V93() V94() V96() V98() right-distributive left-distributive right_unital well-unital V104() left_unital Abelian add-associative right_zeroed L11()
addreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total quasi_total complex-yielding V117() V118() Element of bool [:[:REAL,REAL:],REAL:]
multreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total quasi_total complex-yielding V117() V118() Element of bool [:[:REAL,REAL:],REAL:]
G11(REAL,addreal,multreal,1,0) is V93() L11()
the carrier of F_Real is non empty non trivial V128() set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real finite finite-yielding V36() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-yielding V117() V118() V119() R-orthogonal R-normal R-orthonormal set
{{},1} is non empty finite set
the carrier of F_Real * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL
REAL 0 is functional non empty FinSequence-membered FinSequenceSet of REAL
0 -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
- 1 is non empty V21() real ext-real non positive negative Element of REAL
Seg 1 is non empty finite 1 -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty finite set
Seg 2 is non empty finite 2 -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite set
sqrt 1 is V21() real ext-real Element of REAL
real_dist is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total quasi_total complex-yielding V117() V118() Element of bool [:[:REAL,REAL:],REAL:]
MetrStruct(# REAL,real_dist #) is strict MetrStruct
TopSpaceMetr RealSpace is metrizable TopStruct
the carrier of R^1 is non empty V128() set
rng {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty trivial proper V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real finite finite-yielding V36() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-yielding V117() V118() V119() increasing V121() V122() V123() V126() V127() V128() V129() V131() with_non-empty_elements R-orthogonal R-normal R-orthonormal Element of bool REAL
n is Relation-like Function-like set
M is set
M |` n is Relation-like Function-like set
dom (M |` n) is set
n " M is set
p is set
n1 is set
[p,n1] is set
{p,n1} is non empty finite set
{p} is non empty finite set
{{p,n1},{p}} is non empty finite V36() set
n1 is set
[p,n1] is set
{p,n1} is non empty finite set
{{p,n1},{p}} is non empty finite V36() set
n is Relation-like Function-like set
p is set
M is set
M |` n is Relation-like Function-like set
(M |` n) " p is set
n " p is set
n1 is set
p1 is set
[n1,p1] is set
{n1,p1} is non empty finite set
{n1} is non empty finite set
{{n1,p1},{n1}} is non empty finite V36() set
p1 is set
[n1,p1] is set
{n1,p1} is non empty finite set
{{n1,p1},{n1}} is non empty finite V36() set
n is TopStruct
the carrier of n is set
M is TopStruct
the carrier of M is set
[: the carrier of n, the carrier of M:] is Relation-like set
bool [: the carrier of n, the carrier of M:] is non empty set
p is Relation-like the carrier of n -defined the carrier of M -valued Function-like quasi_total Element of bool [: the carrier of n, the carrier of M:]
p /" is Relation-like the carrier of M -defined the carrier of n -valued Function-like quasi_total Element of bool [: the carrier of M, the carrier of n:]
[: the carrier of M, the carrier of n:] is Relation-like set
bool [: the carrier of M, the carrier of n:] is non empty set
dom p is Element of bool the carrier of n
bool the carrier of n is non empty set
[#] n is non proper Element of bool the carrier of n
rng p is Element of bool the carrier of M
bool the carrier of M is non empty set
[#] M is non proper Element of bool the carrier of M
[:{},{}:] is Relation-like finite set
bool [:{},{}:] is non empty finite V36() set
n1 is Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional empty onto bijective V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real finite finite-yielding V36() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-yielding V117() V118() V119() R-orthogonal R-normal R-orthonormal Element of bool [:{},{}:]
n1 " is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real finite finite-yielding V36() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-yielding V117() V118() V119() R-orthogonal R-normal R-orthonormal Element of REAL
dom (p /") is Element of bool the carrier of M
rng (p /") is Element of bool the carrier of n
(p /") /" is Relation-like the carrier of n -defined the carrier of M -valued Function-like quasi_total Element of bool [: the carrier of n, the carrier of M:]
p1 is Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional empty onto bijective V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real finite finite-yielding V36() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-yielding V117() V118() V119() R-orthogonal R-normal R-orthonormal Element of bool [:{},{}:]
p1 " is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real finite finite-yielding V36() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-yielding V117() V118() V119() R-orthogonal R-normal R-orthonormal Element of REAL
p is TopStruct
n1 is TopStruct
the carrier of p is set
the carrier of n1 is set
[: the carrier of p, the carrier of n1:] is Relation-like set
bool [: the carrier of p, the carrier of n1:] is non empty set
p1 is Relation-like the carrier of p -defined the carrier of n1 -valued Function-like quasi_total Element of bool [: the carrier of p, the carrier of n1:]
p1 /" is Relation-like the carrier of n1 -defined the carrier of p -valued Function-like quasi_total Element of bool [: the carrier of n1, the carrier of p:]
[: the carrier of n1, the carrier of p:] is Relation-like set
bool [: the carrier of n1, the carrier of p:] is non empty set
n is TopSpace-like TopStruct
the carrier of n is set
M is TopSpace-like TopStruct
the carrier of M is set
bool the carrier of M is non empty set
[: the carrier of n, the carrier of M:] is Relation-like set
bool [: the carrier of n, the carrier of M:] is non empty set
p is Element of bool the carrier of M
M | p is strict TopSpace-like SubSpace of M
the carrier of (M | p) is set
n1 is Relation-like the carrier of n -defined the carrier of M -valued Function-like quasi_total Element of bool [: the carrier of n, the carrier of M:]
n1 " p is Element of bool the carrier of n
bool the carrier of n is non empty set
n | (n1 " p) is strict TopSpace-like SubSpace of n
the carrier of (n | (n1 " p)) is set
[: the carrier of (n | (n1 " p)), the carrier of (M | p):] is Relation-like set
bool [: the carrier of (n | (n1 " p)), the carrier of (M | p):] is non empty set
p |` n1 is Relation-like the carrier of n -defined the carrier of M -valued p -valued the carrier of M -valued Function-like Element of bool [: the carrier of n, the carrier of M:]
dom n1 is Element of bool the carrier of n
[#] n is non proper open closed Element of bool the carrier of n
rng n1 is Element of bool the carrier of M
[#] M is non proper open closed Element of bool the carrier of M
A is Relation-like the carrier of (n | (n1 " p)) -defined the carrier of (M | p) -valued Function-like quasi_total Element of bool [: the carrier of (n | (n1 " p)), the carrier of (M | p):]
rng A is Element of bool the carrier of (M | p)
bool the carrier of (M | p) is non empty set
dom A is Element of bool the carrier of (n | (n1 " p))
bool the carrier of (n | (n1 " p)) is non empty set
[#] (n | (n1 " p)) is non proper open closed Element of bool the carrier of (n | (n1 " p))
[#] (M | p) is non proper open closed Element of bool the carrier of (M | p)
m is Element of bool the carrier of (M | p)
A " m is Element of bool the carrier of (n | (n1 " p))
S is Element of bool the carrier of M
S /\ p is Element of bool the carrier of M
n1 " S is Element of bool the carrier of n
n1 " m is Element of bool the carrier of n
(n1 " S) /\ the carrier of (n | (n1 " p)) is Element of bool the carrier of n
n1 /" is Relation-like the carrier of M -defined the carrier of n -valued Function-like quasi_total Element of bool [: the carrier of M, the carrier of n:]
[: the carrier of M, the carrier of n:] is Relation-like set
bool [: the carrier of M, the carrier of n:] is non empty set
A /" is Relation-like the carrier of (M | p) -defined the carrier of (n | (n1 " p)) -valued Function-like quasi_total Element of bool [: the carrier of (M | p), the carrier of (n | (n1 " p)):]
[: the carrier of (M | p), the carrier of (n | (n1 " p)):] is Relation-like set
bool [: the carrier of (M | p), the carrier of (n | (n1 " p)):] is non empty set
m is Element of bool the carrier of (n | (n1 " p))
(A /") " m is Element of bool the carrier of (M | p)
S is Element of bool the carrier of n
S /\ (n1 " p) is Element of bool the carrier of n
(n1 /") " S is Element of bool the carrier of M
n1 .: (n1 " p) is Element of bool the carrier of M
(n1 /") " (n1 " p) is Element of bool the carrier of M
(p |` n1) .: m is Element of bool the carrier of M
n1 .: m is Element of bool the carrier of M
(n1 .: m) /\ the carrier of (M | p) is Element of bool the carrier of M
(n1 /") " (S /\ (n1 " p)) is Element of bool the carrier of M
((n1 /") " (S /\ (n1 " p))) /\ the carrier of (M | p) is Element of bool the carrier of M
((n1 /") " S) /\ ((n1 /") " (n1 " p)) is Element of bool the carrier of M
(((n1 /") " S) /\ ((n1 /") " (n1 " p))) /\ the carrier of (M | p) is Element of bool the carrier of M
((n1 /") " (n1 " p)) /\ the carrier of (M | p) is Element of bool the carrier of M
((n1 /") " S) /\ (((n1 /") " (n1 " p)) /\ the carrier of (M | p)) is Element of bool the carrier of M
((n1 /") " S) /\ the carrier of (M | p) is Element of bool the carrier of M
n is TopSpace-like TopStruct
the carrier of n is set
M is TopSpace-like TopStruct
the carrier of M is set
bool the carrier of M is non empty set
[: the carrier of n, the carrier of M:] is Relation-like set
bool [: the carrier of n, the carrier of M:] is non empty set
p is Element of bool the carrier of M
n1 is Relation-like the carrier of n -defined the carrier of M -valued Function-like quasi_total Element of bool [: the carrier of n, the carrier of M:]
n1 " p is Element of bool the carrier of n
bool the carrier of n is non empty set
p |` n1 is Relation-like the carrier of n -defined the carrier of M -valued p -valued the carrier of M -valued Function-like Element of bool [: the carrier of n, the carrier of M:]
dom (p |` n1) is Element of bool the carrier of n
n | (n1 " p) is strict TopSpace-like SubSpace of n
[#] (n | (n1 " p)) is non proper open closed Element of bool the carrier of (n | (n1 " p))
the carrier of (n | (n1 " p)) is set
bool the carrier of (n | (n1 " p)) is non empty set
rng n1 is Element of bool the carrier of M
[#] M is non proper open closed Element of bool the carrier of M
rng (p |` n1) is Element of bool p
bool p is non empty set
M | p is strict TopSpace-like SubSpace of M
[#] (M | p) is non proper open closed Element of bool the carrier of (M | p)
the carrier of (M | p) is set
bool the carrier of (M | p) is non empty set
[: the carrier of (n | (n1 " p)), the carrier of (M | p):] is Relation-like set
bool [: the carrier of (n | (n1 " p)), the carrier of (M | p):] is non empty set
p1 is Relation-like the carrier of (n | (n1 " p)) -defined the carrier of (M | p) -valued Function-like quasi_total Element of bool [: the carrier of (n | (n1 " p)), the carrier of (M | p):]
n is TopSpace-like TopStruct
the carrier of n is set
bool the carrier of n is non empty set
M is TopSpace-like TopStruct
the carrier of M is set
bool the carrier of M is non empty set
p is Element of bool the carrier of n
n1 is Element of bool the carrier of M
n | p is strict TopSpace-like SubSpace of n
M | n1 is strict TopSpace-like SubSpace of M
n is TopSpace-like TopStruct
the carrier of n is set
bool the carrier of n is non empty set
M is TopSpace-like TopStruct
the carrier of M is set
bool the carrier of M is non empty set
p is Element of bool the carrier of n
n1 is Element of bool the carrier of M
n | p is strict TopSpace-like SubSpace of n
M | n1 is strict TopSpace-like SubSpace of M
the carrier of (n | p) is set
the carrier of (M | n1) is set
[: the carrier of (n | p), the carrier of (M | n1):] is Relation-like set
bool [: the carrier of (n | p), the carrier of (M | n1):] is non empty set
p1 is Relation-like the carrier of (n | p) -defined the carrier of (M | n1) -valued Function-like quasi_total Element of bool [: the carrier of (n | p), the carrier of (M | n1):]
dom p1 is Element of bool the carrier of (n | p)
bool the carrier of (n | p) is non empty set
[#] (n | p) is non proper open closed Element of bool the carrier of (n | p)
rng p1 is Element of bool the carrier of (M | n1)
bool the carrier of (M | n1) is non empty set
[#] (M | n1) is non proper open closed Element of bool the carrier of (M | n1)
p1 /" is Relation-like the carrier of (M | n1) -defined the carrier of (n | p) -valued Function-like quasi_total Element of bool [: the carrier of (M | n1), the carrier of (n | p):]
[: the carrier of (M | n1), the carrier of (n | p):] is Relation-like set
bool [: the carrier of (M | n1), the carrier of (n | p):] is non empty set
n is TopSpace-like TopStruct
the carrier of n is set
bool the carrier of n is non empty set
M is TopSpace-like TopStruct
the carrier of M is set
bool the carrier of M is non empty set
p is TopSpace-like TopStruct
the carrier of p is set
bool the carrier of p is non empty set
n1 is Element of bool the carrier of n
p1 is Element of bool the carrier of M
A is Element of bool the carrier of p
n | n1 is strict TopSpace-like SubSpace of n
M | p1 is strict TopSpace-like SubSpace of M
p | A is strict TopSpace-like SubSpace of p
the carrier of (n | n1) is set
the carrier of (p | A) is set
U1 is Relation-like Function-like set
dom U1 is set
rng U1 is set
[: the carrier of (n | n1), the carrier of (p | A):] is Relation-like set
bool [: the carrier of (n | n1), the carrier of (p | A):] is non empty set
U is Relation-like the carrier of (n | n1) -defined the carrier of (p | A) -valued Function-like quasi_total Element of bool [: the carrier of (n | n1), the carrier of (p | A):]
dom U is Element of bool the carrier of (n | n1)
bool the carrier of (n | n1) is non empty set
[#] (n | n1) is non proper open closed Element of bool the carrier of (n | n1)
rng U is Element of bool the carrier of (p | A)
bool the carrier of (p | A) is non empty set
[#] (p | A) is non proper open closed Element of bool the carrier of (p | A)
m is Element of bool the carrier of (p | A)
U " m is Element of bool the carrier of (n | n1)
[:{},{}:] is Relation-like finite set
bool [:{},{}:] is non empty finite V36() set
U /" is Relation-like the carrier of (p | A) -defined the carrier of (n | n1) -valued Function-like quasi_total Element of bool [: the carrier of (p | A), the carrier of (n | n1):]
[: the carrier of (p | A), the carrier of (n | n1):] is Relation-like set
bool [: the carrier of (p | A), the carrier of (n | n1):] is non empty set
S is Element of bool the carrier of (n | n1)
(U /") " S is Element of bool the carrier of (p | A)
n is TopSpace-like TopStruct
M is TopSpace-like TopStruct
weight n is cardinal set
weight M is cardinal set
n is non empty TopSpace-like TopStruct
M is non empty TopSpace-like TopStruct
the carrier of M is non empty set
the carrier of n is non empty set
[: the carrier of M, the carrier of n:] is Relation-like non empty set
bool [: the carrier of M, the carrier of n:] is non empty set
p is Relation-like the carrier of M -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [: the carrier of M, the carrier of n:]
dom p is non empty Element of bool the carrier of M
bool the carrier of M is non empty set
[#] M is non empty non proper open closed Element of bool the carrier of M
rng p is non empty Element of bool the carrier of n
bool the carrier of n is non empty set
[#] n is non empty non proper open closed Element of bool the carrier of n
p /" is Relation-like the carrier of n -defined the carrier of M -valued Function-like non empty total quasi_total Element of bool [: the carrier of n, the carrier of M:]
[: the carrier of n, the carrier of M:] is Relation-like non empty set
bool [: the carrier of n, the carrier of M:] is non empty set
n1 is Element of the carrier of M
p1 is Element of the carrier of M
p . n1 is Element of the carrier of n
p . p1 is Element of the carrier of n
A is Element of bool the carrier of n
U1 is Element of bool the carrier of n
p " A is Element of bool the carrier of M
p " U1 is Element of bool the carrier of M
U is Element of bool the carrier of M
m is Element of bool the carrier of M
n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
M is non empty TopSpace-like TopStruct
p is non empty TopSpace-like TopStruct
the carrier of p is non empty set
the carrier of M is non empty set
[: the carrier of p, the carrier of M:] is Relation-like non empty set
bool [: the carrier of p, the carrier of M:] is non empty set
n1 is Relation-like the carrier of p -defined the carrier of M -valued Function-like non empty total quasi_total Element of bool [: the carrier of p, the carrier of M:]
dom n1 is non empty Element of bool the carrier of p
bool the carrier of p is non empty set
[#] p is non empty non proper open closed Element of bool the carrier of p
rng n1 is non empty Element of bool the carrier of M
bool the carrier of M is non empty set
[#] M is non empty non proper open closed Element of bool the carrier of M
n1 /" is Relation-like the carrier of M -defined the carrier of p -valued Function-like non empty total quasi_total Element of bool [: the carrier of M, the carrier of p:]
[: the carrier of M, the carrier of p:] is Relation-like non empty set
bool [: the carrier of M, the carrier of p:] is non empty set
TOP-REAL n is non empty V70() V138() V139() TopSpace-like T_0 T_1 T_2 Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous V234() second-countable finite-dimensional n -locally_euclidean n -manifold manifold-like RLTopStruct
the carrier of (TOP-REAL n) is functional non empty set
bool the carrier of (TOP-REAL n) is non empty set
p1 is Element of the carrier of p
n1 . p1 is Element of the carrier of M
U1 is a_neighborhood of n1 . p1
U is functional open Element of bool the carrier of (TOP-REAL n)
m is open Element of bool the carrier of M
S is functional open Element of bool the carrier of (TOP-REAL n)
n1 " m is Element of bool the carrier of p
U11 is a_neighborhood of p1
n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
M is non empty TopSpace-like TopStruct
p is non empty TopSpace-like TopStruct
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
M is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
mlt (n,M) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
dom (mlt (n,M)) is finite Element of bool NAT
p is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
(mlt (n,M)) . p is V21() real ext-real Element of REAL
n /. p is V21() real ext-real Element of REAL
M /. p is V21() real ext-real Element of REAL
(n /. p) * (M /. p) is V21() real ext-real Element of REAL
(mlt (n,M)) /. p is V21() real ext-real Element of REAL
multreal .: (n,M) is set
dom multreal is Relation-like REAL -defined REAL -valued non empty complex-yielding V117() V118() Element of bool [:REAL,REAL:]
rng n is finite V126() V127() V128() Element of bool REAL
rng M is finite V126() V127() V128() Element of bool REAL
[:(rng n),(rng M):] is Relation-like finite complex-yielding V117() V118() set
dom n is finite Element of bool NAT
dom M is finite Element of bool NAT
(dom n) /\ (dom M) is finite Element of bool NAT
M . p is V21() real ext-real Element of REAL
n . p is V21() real ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
len n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
M is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
len M is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
p is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
len p is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
n1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
len n1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
n ^ p is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
M ^ n1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
mlt ((n ^ p),(M ^ n1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
mlt (n,M) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
mlt (p,n1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
(mlt (n,M)) ^ (mlt (p,n1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
multreal .: ((n ^ p),(M ^ n1)) is set
<:(n ^ p),(M ^ n1):> is Relation-like NAT -defined [:REAL,REAL:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:REAL,REAL:]
multreal * <:(n ^ p),(M ^ n1):> is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding V117() V118() Element of bool [:NAT,REAL:]
[:NAT,REAL:] is Relation-like non empty set
bool [:NAT,REAL:] is non empty set
dom (n ^ p) is finite Element of bool NAT
len (n ^ p) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
Seg (len (n ^ p)) is finite len (n ^ p) -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (n ^ p) ) } is set
dom multreal is Relation-like REAL -defined REAL -valued non empty complex-yielding V117() V118() Element of bool [:REAL,REAL:]
rng (n ^ p) is finite V126() V127() V128() Element of bool REAL
rng (M ^ n1) is finite V126() V127() V128() Element of bool REAL
[:(rng (n ^ p)),(rng (M ^ n1)):] is Relation-like finite complex-yielding V117() V118() set
dom (multreal * <:(n ^ p),(M ^ n1):>) is finite Element of bool NAT
dom (M ^ n1) is finite Element of bool NAT
(dom (n ^ p)) /\ (dom (M ^ n1)) is finite Element of bool NAT
len (M ^ n1) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
(len M) + (len n1) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
Seg (len (M ^ n1)) is finite len (M ^ n1) -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (M ^ n1) ) } is set
dom (mlt ((n ^ p),(M ^ n1))) is finite Element of bool NAT
multreal .: (p,n1) is set
<:p,n1:> is Relation-like NAT -defined [:REAL,REAL:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:REAL,REAL:]
multreal * <:p,n1:> is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding V117() V118() Element of bool [:NAT,REAL:]
rng p is finite V126() V127() V128() Element of bool REAL
rng n1 is finite V126() V127() V128() Element of bool REAL
[:(rng p),(rng n1):] is Relation-like finite complex-yielding V117() V118() set
dom (multreal * <:p,n1:>) is finite Element of bool NAT
dom p is finite Element of bool NAT
dom n1 is finite Element of bool NAT
(dom p) /\ (dom n1) is finite Element of bool NAT
Seg (len p) is finite len p -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len p ) } is set
dom (mlt (p,n1)) is finite Element of bool NAT
len (mlt (p,n1)) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
multreal .: (n,M) is set
<:n,M:> is Relation-like NAT -defined [:REAL,REAL:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:REAL,REAL:]
multreal * <:n,M:> is Relation-like NAT -defined REAL -valued Function-like finite complex-yielding V117() V118() Element of bool [:NAT,REAL:]
rng n is finite V126() V127() V128() Element of bool REAL
rng M is finite V126() V127() V128() Element of bool REAL
[:(rng n),(rng M):] is Relation-like finite complex-yielding V117() V118() set
dom (multreal * <:n,M:>) is finite Element of bool NAT
dom n is finite Element of bool NAT
dom M is finite Element of bool NAT
(dom n) /\ (dom M) is finite Element of bool NAT
(len n) + (len p) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
Seg (len n) is finite len n -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len n ) } is set
dom (mlt (n,M)) is finite Element of bool NAT
len (mlt ((n ^ p),(M ^ n1))) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
p1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
(mlt ((n ^ p),(M ^ n1))) . p1 is V21() real ext-real Element of REAL
((mlt (n,M)) ^ (mlt (p,n1))) . p1 is V21() real ext-real Element of REAL
Seg (len (mlt ((n ^ p),(M ^ n1)))) is finite len (mlt ((n ^ p),(M ^ n1))) -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (mlt ((n ^ p),(M ^ n1))) ) } is set
(n ^ p) /. p1 is V21() real ext-real Element of REAL
(n ^ p) . p1 is V21() real ext-real Element of REAL
(M ^ n1) /. p1 is V21() real ext-real Element of REAL
(M ^ n1) . p1 is V21() real ext-real Element of REAL
M . p1 is V21() real ext-real Element of REAL
(mlt (n,M)) . p1 is V21() real ext-real Element of REAL
n /. p1 is V21() real ext-real Element of REAL
M /. p1 is V21() real ext-real Element of REAL
(n /. p1) * (M /. p1) is V21() real ext-real Element of REAL
n . p1 is V21() real ext-real Element of REAL
((n ^ p) /. p1) * ((M ^ n1) /. p1) is V21() real ext-real Element of REAL
p1 -' (len n) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
p1 - (len n) is V21() real ext-real Element of REAL
(len n) + (p1 -' (len n)) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
((len n) + (len p)) - (len n) is V21() real ext-real Element of REAL
(p1 -' (len n)) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative Element of NAT
{} + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative Element of NAT
len (mlt (n,M)) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
(len (mlt (n,M))) + (p1 -' (len n)) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
(mlt (p,n1)) . (p1 -' (len n)) is V21() real ext-real Element of REAL
p /. (p1 -' (len n)) is V21() real ext-real Element of REAL
n1 /. (p1 -' (len n)) is V21() real ext-real Element of REAL
(p /. (p1 -' (len n))) * (n1 /. (p1 -' (len n))) is V21() real ext-real Element of REAL
p . (p1 -' (len n)) is V21() real ext-real Element of REAL
n1 . (p1 -' (len n)) is V21() real ext-real Element of REAL
((n ^ p) /. p1) * ((M ^ n1) /. p1) is V21() real ext-real Element of REAL
((n ^ p) /. p1) * ((M ^ n1) /. p1) is V21() real ext-real Element of REAL
((n ^ p) /. p1) * ((M ^ n1) /. p1) is V21() real ext-real Element of REAL
len (mlt (n,M)) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
(len (mlt (n,M))) + (len (mlt (p,n1))) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
len ((mlt (n,M)) ^ (mlt (p,n1))) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
len n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
M is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
len M is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
p is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
len p is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
n1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
len n1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
n ^ p is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
M ^ n1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
|((n ^ p),(M ^ n1))| is V21() real ext-real Element of REAL
|(n,M)| is V21() real ext-real Element of REAL
|(p,n1)| is V21() real ext-real Element of REAL
|(n,M)| + |(p,n1)| is V21() real ext-real Element of REAL
mlt (n,M) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
mlt (p,n1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
(mlt (n,M)) ^ (mlt (p,n1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
Sum ((mlt (n,M)) ^ (mlt (p,n1))) is V21() real ext-real Element of REAL
Sum (mlt (n,M)) is V21() real ext-real Element of REAL
Sum (mlt (p,n1)) is V21() real ext-real Element of REAL
(Sum (mlt (n,M))) + (Sum (mlt (p,n1))) is V21() real ext-real Element of REAL
mlt ((n ^ p),(M ^ n1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
Sum (mlt ((n ^ p),(M ^ n1))) is V21() real ext-real Element of REAL
(Sum (mlt (n,M))) + |(p,n1)| is V21() real ext-real Element of REAL
n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
Seg n is finite n -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
RealVectSpace (Seg n) is non empty V70() V138() V139() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional RLSStruct
the carrier of (RealVectSpace (Seg n)) is non empty set
TOP-REAL n is non empty V70() V138() V139() TopSpace-like T_0 T_1 T_2 Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous V234() second-countable finite-dimensional n -locally_euclidean n -manifold manifold-like RLTopStruct
the carrier of (TOP-REAL n) is functional non empty set
M is non empty set
Funcs ((Seg n),M) is functional non empty FUNCTION_DOMAIN of Seg n,M
REAL n is functional non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
Funcs ((Seg n),REAL) is functional non empty FUNCTION_DOMAIN of Seg n, REAL
RealFuncZero (Seg n) is Relation-like Seg n -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Element of Funcs ((Seg n),REAL)
RealFuncAdd (Seg n) is Relation-like [:(Funcs ((Seg n),REAL)),(Funcs ((Seg n),REAL)):] -defined Funcs ((Seg n),REAL) -valued Function-like non empty total quasi_total Element of bool [:[:(Funcs ((Seg n),REAL)),(Funcs ((Seg n),REAL)):],(Funcs ((Seg n),REAL)):]
[:(Funcs ((Seg n),REAL)),(Funcs ((Seg n),REAL)):] is Relation-like non empty set
[:[:(Funcs ((Seg n),REAL)),(Funcs ((Seg n),REAL)):],(Funcs ((Seg n),REAL)):] is Relation-like non empty set
bool [:[:(Funcs ((Seg n),REAL)),(Funcs ((Seg n),REAL)):],(Funcs ((Seg n),REAL)):] is non empty set
RealFuncExtMult (Seg n) is Relation-like [:REAL,(Funcs ((Seg n),REAL)):] -defined Funcs ((Seg n),REAL) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(Funcs ((Seg n),REAL)):],(Funcs ((Seg n),REAL)):]
[:REAL,(Funcs ((Seg n),REAL)):] is Relation-like non empty set
[:[:REAL,(Funcs ((Seg n),REAL)):],(Funcs ((Seg n),REAL)):] is Relation-like non empty set
bool [:[:REAL,(Funcs ((Seg n),REAL)):],(Funcs ((Seg n),REAL)):] is non empty set
RLSStruct(# (Funcs ((Seg n),REAL)),(RealFuncZero (Seg n)),(RealFuncAdd (Seg n)),(RealFuncExtMult (Seg n)) #) is strict RLSStruct
n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
Seg n is finite n -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
RealVectSpace (Seg n) is non empty V70() V138() V139() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional RLSStruct
0. (RealVectSpace (Seg n)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V51( RealVectSpace (Seg n)) complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
the carrier of (RealVectSpace (Seg n)) is non empty set
the ZeroF of (RealVectSpace (Seg n)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
TOP-REAL n is non empty V70() V138() V139() TopSpace-like T_0 T_1 T_2 Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous V234() second-countable finite-dimensional n -locally_euclidean n -manifold manifold-like RLTopStruct
0. (TOP-REAL n) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like V51( TOP-REAL n) complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
the carrier of (TOP-REAL n) is functional non empty set
the ZeroF of (TOP-REAL n) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
Funcs ((Seg n),REAL) is functional non empty FUNCTION_DOMAIN of Seg n, REAL
RealFuncZero (Seg n) is Relation-like Seg n -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Element of Funcs ((Seg n),REAL)
RealFuncAdd (Seg n) is Relation-like [:(Funcs ((Seg n),REAL)),(Funcs ((Seg n),REAL)):] -defined Funcs ((Seg n),REAL) -valued Function-like non empty total quasi_total Element of bool [:[:(Funcs ((Seg n),REAL)),(Funcs ((Seg n),REAL)):],(Funcs ((Seg n),REAL)):]
[:(Funcs ((Seg n),REAL)),(Funcs ((Seg n),REAL)):] is Relation-like non empty set
[:[:(Funcs ((Seg n),REAL)),(Funcs ((Seg n),REAL)):],(Funcs ((Seg n),REAL)):] is Relation-like non empty set
bool [:[:(Funcs ((Seg n),REAL)),(Funcs ((Seg n),REAL)):],(Funcs ((Seg n),REAL)):] is non empty set
RealFuncExtMult (Seg n) is Relation-like [:REAL,(Funcs ((Seg n),REAL)):] -defined Funcs ((Seg n),REAL) -valued Function-like non empty total quasi_total Element of bool [:[:REAL,(Funcs ((Seg n),REAL)):],(Funcs ((Seg n),REAL)):]
[:REAL,(Funcs ((Seg n),REAL)):] is Relation-like non empty set
[:[:REAL,(Funcs ((Seg n),REAL)):],(Funcs ((Seg n),REAL)):] is Relation-like non empty set
bool [:[:REAL,(Funcs ((Seg n),REAL)):],(Funcs ((Seg n),REAL)):] is non empty set
RLSStruct(# (Funcs ((Seg n),REAL)),(RealFuncZero (Seg n)),(RealFuncAdd (Seg n)),(RealFuncExtMult (Seg n)) #) is strict RLSStruct
(Seg n) --> {} is Relation-like Seg n -defined {{}} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() V119() Element of bool [:(Seg n),{{}}:]
{{}} is functional non empty finite V36() set
[:(Seg n),{{}}:] is Relation-like finite set
bool [:(Seg n),{{}}:] is non empty finite V36() set
0* n is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of REAL n
REAL n is functional non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
n |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of n -tuples_on REAL
n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
M is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
TOP-REAL M is non empty V70() V138() V139() TopSpace-like T_0 T_1 T_2 Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous V234() second-countable finite-dimensional M -locally_euclidean M -manifold manifold-like RLTopStruct
the carrier of (TOP-REAL M) is functional non empty set
Seg M is finite M -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= M ) } is set
p is Relation-like NAT -defined Function-like finite M -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL M)
p . n is V21() real ext-real Element of REAL
n1 is Relation-like NAT -defined Function-like finite M -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL M)
p + n1 is Relation-like NAT -defined Function-like finite M -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL M)
p + n1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() FinSequence of REAL
(p + n1) . n is V21() real ext-real Element of REAL
n1 . n is V21() real ext-real Element of REAL
(p . n) + (n1 . n) is V21() real ext-real Element of REAL
dom (p + n1) is finite Element of bool NAT
n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
Seg n is finite n -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
RealVectSpace (Seg n) is non empty V70() V138() V139() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional RLSStruct
the carrier of (RealVectSpace (Seg n)) is non empty set
TOP-REAL n is non empty V70() V138() V139() TopSpace-like T_0 T_1 T_2 Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous V234() second-countable finite-dimensional n -locally_euclidean n -manifold manifold-like RLTopStruct
the carrier of (TOP-REAL n) is functional non empty set
M is set
bool the carrier of (RealVectSpace (Seg n)) is non empty set
p1 is Relation-like the carrier of (RealVectSpace (Seg n)) -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Linear_Combination of RealVectSpace (Seg n)
A is finite Element of bool the carrier of (RealVectSpace (Seg n))
U1 is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
p1 . U1 is V21() real ext-real Element of REAL
Funcs ( the carrier of (TOP-REAL n),REAL) is functional non empty FUNCTION_DOMAIN of the carrier of (TOP-REAL n), REAL
bool the carrier of (TOP-REAL n) is non empty set
p1 is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Linear_Combination of TOP-REAL n
A is functional finite closed compact Element of bool the carrier of (TOP-REAL n)
U1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
p1 . U1 is V21() real ext-real Element of REAL
Funcs ( the carrier of (RealVectSpace (Seg n)),REAL) is functional non empty FUNCTION_DOMAIN of the carrier of (RealVectSpace (Seg n)), REAL
n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
TOP-REAL n is non empty V70() V138() V139() TopSpace-like T_0 T_1 T_2 Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous V234() second-countable finite-dimensional n -locally_euclidean n -manifold manifold-like RLTopStruct
the carrier of (TOP-REAL n) is functional non empty set
[: the carrier of (TOP-REAL n),REAL:] is Relation-like non empty set
bool [: the carrier of (TOP-REAL n),REAL:] is non empty set
Seg n is finite n -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
RealVectSpace (Seg n) is non empty V70() V138() V139() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional RLSStruct
the carrier of (RealVectSpace (Seg n)) is non empty set
[: the carrier of (RealVectSpace (Seg n)),REAL:] is Relation-like non empty set
bool [: the carrier of (RealVectSpace (Seg n)),REAL:] is non empty set
M is Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL n)
p is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like non empty total quasi_total complex-yielding V117() V118() Element of bool [: the carrier of (TOP-REAL n),REAL:]
p (#) M is Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL n)
n1 is Relation-like NAT -defined the carrier of (RealVectSpace (Seg n)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (RealVectSpace (Seg n))
p1 is Relation-like the carrier of (RealVectSpace (Seg n)) -defined REAL -valued Function-like non empty total quasi_total complex-yielding V117() V118() Element of bool [: the carrier of (RealVectSpace (Seg n)),REAL:]
p1 (#) n1 is Relation-like NAT -defined the carrier of (RealVectSpace (Seg n)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (RealVectSpace (Seg n))
len (p1 (#) n1) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
len n1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
len (p (#) M) is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
len M is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
U1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
M /. U1 is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
n -VectSp_over F_Real is strict VectSpStr over F_Real
the carrier of (n -VectSp_over F_Real) is set
REAL n is functional non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
n1 /. U1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
A is non empty V70() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of A is non empty set
dom (p1 (#) n1) is finite Element of bool NAT
dom M is finite Element of bool NAT
M . U1 is Relation-like Function-like set
dom n1 is finite Element of bool NAT
n1 . U1 is set
dom (p (#) M) is finite Element of bool NAT
(p (#) M) . U1 is Relation-like Function-like set
S is Element of the carrier of A
p . S is V21() real ext-real Element of REAL
(p . S) * S is Element of the carrier of A
p1 . (n1 /. U1) is V21() real ext-real Element of REAL
(p1 . (n1 /. U1)) * (n1 /. U1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
(p1 . (n1 /. U1)) * (n1 /. U1) is Relation-like Function-like set
(p1 (#) n1) . U1 is set
n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
TOP-REAL n is non empty V70() V138() V139() TopSpace-like T_0 T_1 T_2 Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous V234() second-countable finite-dimensional n -locally_euclidean n -manifold manifold-like RLTopStruct
the carrier of (TOP-REAL n) is functional non empty set
Seg n is finite n -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
RealVectSpace (Seg n) is non empty V70() V138() V139() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional RLSStruct
the carrier of (RealVectSpace (Seg n)) is non empty set
n1 is Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL n)
Sum n1 is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
p1 is Relation-like NAT -defined the carrier of (RealVectSpace (Seg n)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (RealVectSpace (Seg n))
Sum p1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
A is non empty V70() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of A is non empty set
[:NAT, the carrier of A:] is Relation-like non empty set
bool [:NAT, the carrier of A:] is non empty set
len n1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
0. A is V51(A) Element of the carrier of A
the ZeroF of A is Element of the carrier of A
U1 is Relation-like NAT -defined the carrier of A -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of A:]
U1 . (len n1) is Element of the carrier of A
U1 . {} is set
[:NAT, the carrier of (RealVectSpace (Seg n)):] is Relation-like non empty set
bool [:NAT, the carrier of (RealVectSpace (Seg n)):] is non empty set
len p1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
0. (RealVectSpace (Seg n)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V51( RealVectSpace (Seg n)) complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
the ZeroF of (RealVectSpace (Seg n)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
U is Relation-like NAT -defined the carrier of (RealVectSpace (Seg n)) -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of (RealVectSpace (Seg n)):]
U . (len p1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
U . {} is set
m is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT
U1 . m is set
U . m is set
m + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative Element of NAT
U1 . (m + 1) is set
U . (m + 1) is set
n -VectSp_over F_Real is strict VectSpStr over F_Real
the carrier of (n -VectSp_over F_Real) is set
REAL n is functional non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
p1 /. (m + 1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
U . m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
n1 /. (m + 1) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
dom n1 is finite Element of bool NAT
n1 . (m + 1) is Relation-like Function-like set
U1 . (m + 1) is Element of the carrier of A
U1 . m is Element of the carrier of A
U2 is Element of the carrier of A
(U1 . m) + U2 is Element of the carrier of A
p1 . (m + 1) is set
U11 is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of F_Real
(U . m) + (p1 /. (m + 1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
K186((U . m),(p1 /. (m + 1))) is Relation-like Function-like set
U . (m + 1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
Seg n is finite n -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
RealVectSpace (Seg n) is non empty V70() V138() V139() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional RLSStruct
the carrier of (RealVectSpace (Seg n)) is non empty set
TOP-REAL n is non empty V70() V138() V139() TopSpace-like T_0 T_1 T_2 Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous V234() second-countable finite-dimensional n -locally_euclidean n -manifold manifold-like RLTopStruct
the carrier of (TOP-REAL n) is functional non empty set
n1 is Relation-like the carrier of (RealVectSpace (Seg n)) -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Linear_Combination of RealVectSpace (Seg n)
Sum n1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
p1 is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Linear_Combination of TOP-REAL n
Sum p1 is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
Carrier p1 is functional Element of bool the carrier of (TOP-REAL n)
bool the carrier of (TOP-REAL n) is non empty set
A is Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL n)
rng A is functional finite closed compact Element of bool the carrier of (TOP-REAL n)
p1 (#) A is Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL n)
Sum (p1 (#) A) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
U1 is Relation-like NAT -defined the carrier of (RealVectSpace (Seg n)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (RealVectSpace (Seg n))
n1 (#) U1 is Relation-like NAT -defined the carrier of (RealVectSpace (Seg n)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (RealVectSpace (Seg n))
Sum (n1 (#) U1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
Seg n is finite n -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
RealVectSpace (Seg n) is non empty V70() V138() V139() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional RLSStruct
the carrier of (RealVectSpace (Seg n)) is non empty set
bool the carrier of (RealVectSpace (Seg n)) is non empty set
TOP-REAL n is non empty V70() V138() V139() TopSpace-like T_0 T_1 T_2 Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous V234() second-countable finite-dimensional n -locally_euclidean n -manifold manifold-like RLTopStruct
the carrier of (TOP-REAL n) is functional non empty set
bool the carrier of (TOP-REAL n) is non empty set
p is Element of bool the carrier of (RealVectSpace (Seg n))
p1 is functional Element of bool the carrier of (TOP-REAL n)
A is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Linear_Combination of p1
Sum A is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
0. (TOP-REAL n) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like V51( TOP-REAL n) complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
0. (RealVectSpace (Seg n)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V51( RealVectSpace (Seg n)) complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
the ZeroF of (RealVectSpace (Seg n)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
U1 is Relation-like the carrier of (RealVectSpace (Seg n)) -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Linear_Combination of RealVectSpace (Seg n)
Sum U1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
Carrier A is functional Element of bool the carrier of (TOP-REAL n)
A is Relation-like the carrier of (RealVectSpace (Seg n)) -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Linear_Combination of p
Carrier A is Element of bool the carrier of (RealVectSpace (Seg n))
U1 is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Linear_Combination of TOP-REAL n
Sum A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
U is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Linear_Combination of p1
Sum U is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative set
TOP-REAL n is non empty V70() V138() V139() TopSpace-like T_0 T_1 T_2 Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous V234() second-countable finite-dimensional n -locally_euclidean n -manifold manifold-like RLTopStruct
the carrier of (TOP-REAL n) is functional non empty set
bool the carrier of (TOP-REAL n) is non empty set
RN_Base n is functional finite FinSequence-membered R-orthogonal R-normal R-orthonormal V353(n) orthogonal_basis Element of bool (REAL n)
REAL n is functional non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
bool (REAL n) is non empty set
M is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
p is functional Element of bool the carrier of (TOP-REAL n)
Seg n is finite n -element Element of bool NAT
{ b1 where b1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
RealVectSpace (Seg n) is non empty V70() V138() V139() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional RLSStruct
the carrier of (RealVectSpace (Seg n)) is non empty set
bool the carrier of (RealVectSpace (Seg n)) is non empty set
p1 is Element of bool the carrier of (RealVectSpace (Seg n))
n1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
A is Relation-like the carrier of (RealVectSpace (Seg n)) -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Linear_Combination of p1
Sum A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (RealVectSpace (Seg n))
Carrier A is Element of bool the carrier of (RealVectSpace (Seg n))
U1 is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Linear_Combination of TOP-REAL n
U is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total complex-yielding V117() V118() Linear_Combination of p
Sum U is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-yielding V117() V118() Element of the carrier of (TOP-REAL n)
n is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non