:: MFOLD_2 semantic presentation

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

{ b

{1} is non empty finite set

Seg 2 is non empty finite 2 -element Element of bool NAT

{ b

{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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

(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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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