:: NAT_3 semantic presentation

REAL is non empty V12() non finite V80() V81() V82() V86() V208() V209() V211() set
NAT is non empty V12() ordinal non finite cardinal limit_cardinal V80() V81() V82() V83() V84() V85() V86() V206() V208() Element of K19(REAL)
K19(REAL) is non empty V12() non finite set
RAT is non empty V12() non finite V80() V81() V82() V83() V86() set

COMPLEX is non empty V12() non finite V80() V86() set
omega is non empty V12() ordinal non finite cardinal limit_cardinal V80() V81() V82() V83() V84() V85() V86() V206() V208() set
K19(omega) is non empty V12() non finite set
K19(NAT) is non empty V12() non finite set
K101(NAT) is V27() set
INT is non empty V12() non finite V80() V81() V82() V83() V84() V86() set

K19(K20(REAL,REAL)) is non empty V12() non finite set
1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
{{},1} is non empty finite V46() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
K419() is set
K19(K419()) is set
K420() is Element of K19(K419())
2 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT

K19(K20(NAT,NAT)) is non empty V12() non finite set

K19(K20(NAT,REAL)) is non empty V12() non finite set

{ } is set
K20(COMPLEX,COMPLEX) is Relation-like non empty V12() non finite complex-valued set
K19(K20(COMPLEX,COMPLEX)) is non empty V12() non finite set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like non empty V12() non finite complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is non empty V12() non finite set

K19(K20(K20(REAL,REAL),REAL)) is non empty V12() non finite set

K19(K20(RAT,RAT)) is non empty V12() non finite set

K19(K20(K20(RAT,RAT),RAT)) is non empty V12() non finite set

K19(K20(INT,INT)) is non empty V12() non finite set

K19(K20(K20(INT,INT),INT)) is non empty V12() non finite set

K19(K20(K20(NAT,NAT),NAT)) is non empty V12() non finite set
3 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT

SetPrimes is non empty V12() non finite V80() V81() V82() V83() V84() V85() V206() V208() Element of K19(NAT)

Seg 1 is non empty V12() finite 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of K19(NAT)
{ b1 where b1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set

n * S is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
x * m is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

n * e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

S * s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
e * s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
(n * S) * (e * s) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set

n - 1 is complex V37() V38() ext-real V57() Element of INT

m + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
n |^ (m + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n |^ m) + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
(n |^ m) * n is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
((n |^ m) + 1) - ((n |^ m) + 1) is complex V37() V38() ext-real V57() Element of INT
((n |^ m) * n) - ((n |^ m) + 1) is complex V37() V38() ext-real V57() Element of INT
0 + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
(n |^ m) * x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
((n |^ m) * x) - 1 is complex V37() V38() ext-real V57() Element of INT
(((n |^ m) * x) - 1) + 1 is complex V37() V38() ext-real V57() Element of INT

x + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT

m is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
m + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
S |^ (m + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set

n + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
x |^ (n + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
e + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
t is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
t |^ (e + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
t |^ s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

m is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

s + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
e |^ (s + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

(e |^ s) * e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
s -' 1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
(s -' 1) + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
e |^ ((s -' 1) + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
0 + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
(0 + 1) - 1 is complex V37() V38() ext-real V57() Element of INT
s - 1 is complex V37() V38() ext-real V57() Element of INT
s - 0 is complex V37() V38() ext-real V57() Element of INT
0 + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
S -' 1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
(S -' 1) + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
e |^ (0 + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

rng S is finite V80() V81() V82() V208() V209() V210() Element of K19(REAL)
Product S is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

[1,x] is non empty set
{1,x} is non empty finite V46() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
{1} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
{{1,x},{1}} is non empty finite V46() set

rng (S ^ <*x*>) is non empty finite V80() V81() V82() V206() V207() V208() V209() V210() Element of K19(REAL)
Product (S ^ <*x*>) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
rng <*x*> is non empty V12() finite 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of K19(REAL)
(rng S) \/ () is non empty finite V80() V81() V82() V206() V207() V208() V209() V210() Element of K19(REAL)
() * x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

{x} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set

Product () is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

rng S is finite V80() V81() V82() V208() V209() V210() Element of K19(REAL)
Product S is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

[1,x] is non empty set
{1,x} is non empty finite V46() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
{1} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
{{1,x},{1}} is non empty finite V46() set

Product S is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
rng S is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(REAL)
Product (S ^ <*x*>) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
rng (S ^ <*x*>) is non empty finite V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of K19(REAL)

Product s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
() * x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

{x} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
rng <*x*> is non empty V12() finite 1 -element set

Product () is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

Product S is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
rng S is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(REAL)

len n is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

len x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
dom x is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
m is set
x . m is set
n . m is complex V37() ext-real Element of REAL
(n . m) |^ S is complex V37() ext-real Element of REAL

len x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
dom x is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)

len m is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
dom m is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
Seg (len x) is finite len x -element V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
{ b1 where b1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT : ( 1 <= b1 & b1 <= len x ) } is set
Seg (len m) is finite len m -element V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
{ b1 where b1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT : ( 1 <= b1 & b1 <= len m ) } is set

x . e is set
m . e is set
n . e is complex V37() ext-real Element of REAL
(n . e) |^ S is complex V37() ext-real Element of REAL

x is set
dom (n,S) is finite set
(n,S) . x is set
dom (n,S) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
n . x is complex V37() ext-real Element of REAL
(n . x) |^ S is complex V37() ext-real Element of REAL

x is set
dom (n,S) is finite set
(n,S) . x is complex V37() ext-real set
dom (n,S) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
(n,S) . x is complex V37() ext-real Element of REAL

(n . x) |^ S is ordinal natural complex V37() V38() finite cardinal ext-real non negative Element of REAL

rng (n,S) is finite V80() V81() V82() V208() V209() V210() Element of K19(REAL)

rng (n,S) is finite V80() V81() V82() V208() V209() V210() Element of K19(REAL)

len n is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

{ } is set
Seg (len n) is finite len n -element V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
{ b1 where b1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT : ( 1 <= b1 & b1 <= len n ) } is set

{1} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set

K19(K20((Seg (len n)),{1})) is finite V46() set
len (n,0) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

(n,0) . S is complex V37() ext-real Element of REAL
((len n) |-> 1) . S is ordinal natural complex V37() V38() finite cardinal ext-real non negative Element of REAL
dom (n,0) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
n . S is complex V37() ext-real Element of REAL
(n . S) |^ 0 is complex V37() ext-real Element of REAL
len ((len n) |-> 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

len (n,1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

(n,1) . S is complex V37() ext-real Element of REAL
n . S is complex V37() ext-real Element of REAL
dom (n,1) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
(n . S) |^ 1 is complex V37() ext-real Element of REAL
len n is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

len ((),n) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

[1,S] is non empty set
{1,S} is non empty finite V80() V81() V82() V206() V207() V208() V209() V210() set
{1} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
{{1,S},{1}} is non empty finite V46() set

S |^ n is complex V37() ext-real Element of REAL

[1,(S |^ n)] is non empty set
{1,(S |^ n)} is non empty finite V80() V81() V82() V206() V207() V208() V209() V210() set
{{1,(S |^ n)},{1}} is non empty finite V46() set

len (<*S*>,n) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
len <*S*> is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
0 + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
Seg (0 + 1) is non empty finite 0 + 1 -element K244(0,1) -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of K19(NAT)
K244(0,1) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
{ b1 where b1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT : ( 1 <= b1 & b1 <= 0 + 1 ) } is set
dom (<*S*>,n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
(<*S*>,n) . 1 is complex V37() ext-real Element of REAL
<*S*> . 1 is complex V37() ext-real Element of REAL
(<*S*> . 1) |^ n is complex V37() ext-real Element of REAL

[1,S] is non empty set
{1,S} is non empty finite V80() V81() V82() V206() V207() V208() V209() V210() set
{1} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
{{1,S},{1}} is non empty finite V46() set

len (x,n) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
len x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
len ((x ^ <*S*>),n) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
len (x ^ <*S*>) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
len <*S*> is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
(len x) + () is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
(len x) + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
dom ((x ^ <*S*>),n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
Seg ((len x) + 1) is non empty finite (len x) + 1 -element K244((len x),1) -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of K19(NAT)
K244((len x),1) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
{ b1 where b1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT : ( 1 <= b1 & b1 <= (len x) + 1 ) } is set

dom x is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
dom (x,n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
((x ^ <*S*>),n) . m is complex V37() ext-real Element of REAL
(x ^ <*S*>) . m is complex V37() ext-real Element of REAL
((x ^ <*S*>) . m) |^ n is complex V37() ext-real Element of REAL
x . m is complex V37() ext-real Element of REAL
(x . m) |^ n is complex V37() ext-real Element of REAL
(x,n) . m is complex V37() ext-real Element of REAL
((x,n) ^ (<*S*>,n)) . m is complex V37() ext-real Element of REAL
((x ^ <*S*>),n) . m is complex V37() ext-real Element of REAL
(x ^ <*S*>) . m is complex V37() ext-real Element of REAL
((x ^ <*S*>) . m) |^ n is complex V37() ext-real Element of REAL
S |^ n is complex V37() ext-real Element of REAL

[1,(S |^ n)] is non empty set
{1,(S |^ n)} is non empty finite V80() V81() V82() V206() V207() V208() V209() V210() set
{{1,(S |^ n)},{1}} is non empty finite V46() set

((x,n) ^ <*(S |^ n)*>) . m is complex V37() ext-real Element of REAL
((x,n) ^ (<*S*>,n)) . m is complex V37() ext-real Element of REAL
len ((x,n) ^ (<*S*>,n)) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
len (<*S*>,n) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
(len (x,n)) + (len (<*S*>,n)) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
(len x) + (len (<*S*>,n)) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
S |^ n is complex V37() ext-real Element of REAL

[1,(S |^ n)] is non empty set
{1,(S |^ n)} is non empty finite V80() V81() V82() V206() V207() V208() V209() V210() set
{{1,(S |^ n)},{1}} is non empty finite V46() set

len <*(S |^ n)*> is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
(len x) + (len <*(S |^ n)*>) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT

n + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT

Product (S,(n + 1)) is complex V37() ext-real Element of REAL

Product (S,n) is complex V37() ext-real Element of REAL

(Product (S,n)) * () is complex V37() ext-real Element of REAL

[1,m] is non empty set
{1,m} is non empty finite V80() V81() V82() V206() V207() V208() V209() V210() set
{1} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
{{1,m},{1}} is non empty finite V46() set

Product (x ^ <*m*>) is complex V37() ext-real Element of REAL

s + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT

Product ((x ^ <*m*>),(s + 1)) is complex V37() ext-real Element of REAL

Product ((x ^ <*m*>),s) is complex V37() ext-real Element of REAL
(Product ((x ^ <*m*>),s)) * (Product (x ^ <*m*>)) is complex V37() ext-real Element of REAL

Product (x,(s + 1)) is complex V37() ext-real Element of REAL
Product (<*m*>,(s + 1)) is complex V37() ext-real Element of REAL
(Product (x,(s + 1))) * (Product (<*m*>,(s + 1))) is complex V37() ext-real Element of REAL

Product (x,s) is complex V37() ext-real Element of REAL
(Product (x,s)) * () is complex V37() ext-real Element of REAL
((Product (x,s)) * ()) * (Product (<*m*>,(s + 1))) is complex V37() ext-real Element of REAL
m |^ (s + 1) is complex V37() ext-real Element of REAL

[1,(m |^ (s + 1))] is non empty set
{1,(m |^ (s + 1))} is non empty finite V80() V81() V82() V206() V207() V208() V209() V210() set
{{1,(m |^ (s + 1))},{1}} is non empty finite V46() set
{[1,(m |^ (s + 1))]} is Relation-like Function-like constant non empty V12() finite 1 -element finite-support set
Product <*(m |^ (s + 1))*> is complex V37() ext-real Element of REAL
((Product (x,s)) * ()) * (Product <*(m |^ (s + 1))*>) is complex V37() ext-real Element of REAL
((Product (x,s)) * ()) * (m |^ (s + 1)) is complex V37() ext-real Element of REAL
m |^ s is complex V37() ext-real Element of REAL
(m |^ s) * m is complex V37() ext-real Element of REAL
((Product (x,s)) * ()) * ((m |^ s) * m) is complex V37() ext-real Element of REAL
(Product (x,s)) * (m |^ s) is complex V37() ext-real Element of REAL
((Product (x,s)) * (m |^ s)) * m is complex V37() ext-real Element of REAL
(((Product (x,s)) * (m |^ s)) * m) * () is complex V37() ext-real Element of REAL

[1,(m |^ s)] is non empty set
{1,(m |^ s)} is non empty finite V80() V81() V82() V206() V207() V208() V209() V210() set
{{1,(m |^ s)},{1}} is non empty finite V46() set

Product ((x,s) ^ <*(m |^ s)*>) is complex V37() ext-real Element of REAL
(Product ((x,s) ^ <*(m |^ s)*>)) * m is complex V37() ext-real Element of REAL
((Product ((x,s) ^ <*(m |^ s)*>)) * m) * () is complex V37() ext-real Element of REAL

Product ((x,s) ^ (<*m*>,s)) is complex V37() ext-real Element of REAL
(Product ((x,s) ^ (<*m*>,s))) * m is complex V37() ext-real Element of REAL
((Product ((x,s) ^ (<*m*>,s))) * m) * () is complex V37() ext-real Element of REAL
(Product ((x ^ <*m*>),s)) * m is complex V37() ext-real Element of REAL
((Product ((x ^ <*m*>),s)) * m) * () is complex V37() ext-real Element of REAL
() * m is complex V37() ext-real Element of REAL
(Product ((x ^ <*m*>),s)) * (() * m) is complex V37() ext-real Element of REAL

m + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT

Product ((),(m + 1)) is complex V37() ext-real Element of REAL

Product ((),m) is complex V37() ext-real Element of REAL
(Product ((),m)) * () is complex V37() ext-real Element of REAL

Product (S,n) is complex V37() ext-real Element of REAL

() |^ n is complex V37() ext-real Element of REAL

Product (S,x) is complex V37() ext-real Element of REAL
() |^ x is complex V37() ext-real Element of REAL
x + 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT

Product (S,(x + 1)) is complex V37() ext-real Element of REAL
() |^ (x + 1) is complex V37() ext-real Element of REAL
(Product (S,x)) * () is complex V37() ext-real Element of REAL

Product (S,0) is complex V37() ext-real Element of REAL
len S is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

{ } is set
Seg (len S) is finite len S -element V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
{ b1 where b1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT : ( 1 <= b1 & b1 <= len S ) } is set

{1} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set

K19(K20((Seg (len S)),{1})) is finite V46() set
Product ((len S) |-> 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
() |^ 0 is complex V37() ext-real Element of REAL
n is set

n is set

e is set
m . e is set
S . e is complex V37() ext-real Element of REAL
x * (S . e) is complex V37() ext-real Element of REAL
dom S is set
dom m is set
x * 0 is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT

s is set
m . s is set
e . s is set
S . s is complex V37() ext-real Element of REAL
x * (S . s) is complex V37() ext-real Element of REAL
n is set

(n,S,x) is Relation-like n -defined Function-like V14(n) set
m is set
dom (n,S,x) is set
(n,S,x) . m is set
S . m is complex V37() ext-real Element of REAL
x * (S . m) is complex V37() ext-real Element of REAL
n is set

m is set
dom (n,S,x) is set
(n,S,x) . m is complex V37() ext-real set
(n,S,x) . m is complex V37() ext-real Element of REAL

x * (S . m) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of NAT
n is set

support (n,S,0) is set
x is set
(n,S,0) . x is complex V37() ext-real Element of REAL
S . x is complex V37() ext-real Element of REAL
0 * (S . x) is complex V37() ext-real Element of REAL

S is set

support x is set

support (S,x,n) is set
m is set
x . m is complex V37() ext-real Element of REAL
n * (x . m) is complex V37() ext-real Element of REAL
(S,x,n) . m is complex V37() ext-real Element of REAL
m is set
(S,x,n) . m is complex V37() ext-real Element of REAL
x . m is complex V37() ext-real Element of REAL
n * (x . m) is complex V37() ext-real Element of REAL
n is set

support (n,S,x) is set
support (n,S,x) is set

n is set

e is set
S . e is complex V37() ext-real Element of REAL
x . e is complex V37() ext-real Element of REAL
m . e is set
dom m is set
dom S is set
dom x is set

s is set
S . s is complex V37() ext-real Element of REAL
x . s is complex V37() ext-real Element of REAL
m . s is set
e . s is set
S . s is complex V37() ext-real Element of REAL
x . s is complex V37() ext-real Element of REAL
m . s is set
e . s is set
S . s is complex V37() ext-real Element of REAL
x . s is complex V37() ext-real Element of REAL
n is set

(n,S,x) is Relation-like n -defined Function-like V14(n) set
m is set
dom (n,S,x) is set
(n,S,x) . m is set
S . m is complex V37() ext-real Element of REAL
x . m is complex V37() ext-real Element of REAL
n is set

m is set
dom (n,S,x) is set
(n,S,x) . m is complex V37() ext-real set