:: MFOLD_2 semantic presentation

REAL is non empty non trivial non finite set

bool REAL is non empty 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

bool 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,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

bool is non empty set

[: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

the carrier of () is functional non empty set
K463() is V226() TopStruct
the carrier of K463() is V128() set

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 () is non empty set
[: the carrier of K472(), the carrier of ():] is Relation-like non empty set
bool [: the carrier of K472(), the carrier of ():] is non empty set
CircleMap is Relation-like the carrier of K472() -defined the carrier of K472() -defined the carrier of () -valued the carrier of () -valued Function-like non empty total total quasi_total quasi_total onto continuous Element of bool [: the carrier of K472(), the carrier of ():]
c[10] is Element of the carrier of ()

the carrier of is non empty set

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 , the carrier of (K472() | (R^1 K386(0,1))):] is Relation-like non empty complex-yielding V117() V118() set
bool [: the carrier of , the carrier of (K472() | (R^1 K386(0,1))):] is non empty set
c[-10] is Element of the carrier of ()

the carrier of is non empty set
1 / 2 is non empty V21() real ext-real positive non negative Element of REAL

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 , 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 , the carrier of (K472() | (R^1 K386((1 / 2),(3 / 2)))):] is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

the carrier of F_Real is non empty non trivial V128() 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

- 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

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

M is 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

p is set
M is 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

bool is non empty finite V36() set

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:]

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

the carrier of n is set

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

the carrier of n is set

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):]

the carrier of n is set
bool the carrier of n is non empty set

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 is set
bool the carrier of n is non empty set

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

the carrier of n is set
bool the carrier of n is non empty set

the carrier of M is set
bool the carrier of M is non empty set

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

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)

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 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

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

the carrier of () is functional non empty set
bool the carrier of () 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 ()
m is open Element of bool the carrier of M
S is functional open Element of bool the carrier of ()
n1 " m is Element of bool the carrier of p
U11 is a_neighborhood of p1

M is non empty TopSpace-like TopStruct
p is non empty TopSpace-like TopStruct

dom (mlt (n,M)) is finite Element of bool 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

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) /\ (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

multreal .: ((n ^ p),(M ^ n1)) is set

bool is non empty set
dom (n ^ p) is finite Element of bool 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

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

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

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 n1 is finite Element of bool NAT
(dom p) /\ (dom n1) is finite 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

multreal .: (n,M) is set

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 () is finite Element of bool NAT

(dom n) /\ (dom M) is finite 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

(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() 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

(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))) + (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 ^ 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

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

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

{ 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

the carrier of (RealVectSpace (Seg n)) is non empty set

the carrier of () is functional non empty set
M is non empty set
Funcs ((Seg n),M) is functional non empty FUNCTION_DOMAIN of Seg n,M

Funcs ((Seg n),REAL) is functional non empty FUNCTION_DOMAIN of 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)),() #) is strict RLSStruct

{ 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

the carrier of (RealVectSpace (Seg n)) is non empty set

the carrier of () is functional non empty set

Funcs ((Seg n),REAL) is functional non empty FUNCTION_DOMAIN of 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)),() #) is strict RLSStruct

bool [:(Seg n),:] is non empty finite V36() set

the carrier of () is functional non empty set

{ 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 . n is V21() real ext-real Element 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

{ 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

the carrier of (RealVectSpace (Seg n)) is non empty set

the carrier of () is functional non empty set
M is set
bool the carrier of (RealVectSpace (Seg n)) is non empty set

A is finite Element of bool the carrier of (RealVectSpace (Seg n))

p1 . U1 is V21() real ext-real Element of REAL
Funcs ( the carrier of (),REAL) is functional non empty FUNCTION_DOMAIN of the carrier of (), REAL
bool the carrier of () is non empty set

A is functional finite closed compact Element of bool the carrier of ()

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

the carrier of () is functional non empty set
[: the carrier of (),REAL:] is Relation-like non empty set
bool [: the carrier of (),REAL:] is non empty set

{ 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

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

p is Relation-like the carrier of () -defined REAL -valued Function-like non empty total quasi_total complex-yielding V117() V118() Element of bool [: the carrier of (),REAL:]

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:]

the carrier of () is set

the carrier of A is non empty set
dom (p1 (#) n1) is finite Element of bool NAT

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

the carrier of () is functional non empty set

{ 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

the carrier of (RealVectSpace (Seg n)) is non empty set

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

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

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 . {} is set

U1 . m is set
U . m is set

U1 . (m + 1) is set
U . (m + 1) is set

the carrier of () is set

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

(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

{ 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

the carrier of (RealVectSpace (Seg n)) is non empty set

the carrier of () is functional non empty set

Carrier p1 is functional Element of bool the carrier of ()
bool the carrier of () is non empty set

{ 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

the carrier of (RealVectSpace (Seg n)) is non empty set
bool the carrier of (RealVectSpace (Seg n)) is non empty set

the carrier of () is functional non empty set
bool the carrier of () is non empty set
p is Element of bool the carrier of (RealVectSpace (Seg n))
p1 is functional Element of bool the carrier of ()

Carrier A is functional Element of bool the carrier of ()

Carrier A is Element of bool the carrier of (RealVectSpace (Seg n))

the carrier of () is functional non empty set
bool the carrier of () is non empty set

bool (REAL n) is non empty set

p is functional Element of bool the carrier of ()

{ 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

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))

Carrier A is Element of bool the carrier of (RealVectSpace (Seg n))