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
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() FinSequence-yielding finite-support V208() V209() V210() V211() set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() FinSequence-yielding finite-support V208() V209() V210() V211() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() FinSequence-yielding finite-support V208() V209() V210() V211() 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
K20(REAL,REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued 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
K20(NAT,NAT) is Relation-like RAT -valued INT -valued non empty V12() non finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20(NAT,NAT)) is non empty V12() non finite set
K20(NAT,REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is non empty V12() non finite set
1 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = 1 } 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
K20(K20(REAL,REAL),REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is non empty V12() non finite set
K20(RAT,RAT) is Relation-like RAT -valued non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is non empty V12() non finite set
K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is non empty V12() non finite set
K20(INT,INT) is Relation-like RAT -valued INT -valued non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is non empty V12() non finite set
K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is non empty V12() non finite set
K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued non empty V12() non finite complex-valued ext-real-valued real-valued natural-valued 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
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V57() complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() FinSequence-yielding finite-support V208() V209() V210() V211() Element of NAT
SetPrimes is non empty V12() non finite V80() V81() V82() V83() V84() V85() V206() V208() Element of K19(NAT)
multcomplex is Relation-like K20(COMPLEX,COMPLEX) -defined COMPLEX -valued Function-like non empty V14(K20(COMPLEX,COMPLEX)) quasi_total V21( COMPLEX ) V22( COMPLEX ) V28( COMPLEX ) complex-valued Element of K19(K20(K20(COMPLEX,COMPLEX),COMPLEX))
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() FinSequence-yielding finite-support V208() V209() V210() V211() FinSequence of REAL
Product (<*> REAL) is complex V37() ext-real Element of REAL
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
the Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V102() finite-support FinSequence of NAT is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V102() finite-support FinSequence of NAT
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n |^ S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n is ordinal natural complex V37() V38() prime finite cardinal ext-real non negative set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
x is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
m is ordinal natural complex V37() V38() finite cardinal ext-real non negative 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
e is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n |^ 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 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n |^ m is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
n |^ 0 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S |^ n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
x is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
S |^ 1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
x is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
x |^ S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
m 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
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n |^ S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
x is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
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 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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 is ordinal natural complex V37() V38() finite cardinal ext-real non negative Element of REAL
(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
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
S |^ n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
x is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V102() finite-support FinSequence 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
<*x*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V102() finite-support 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
{[1,x]} is Relation-like Function-like constant non empty V12() finite 1 -element finite-support set
S ^ <*x*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V102() finite-support FinSequence of NAT
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) \/ (rng <*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
e is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
{x} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() V102() FinSequence-yielding finite-support V208() V209() V210() V211() Element of NAT *
rng (<*> NAT) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V58() complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() FinSequence-yielding finite-support V208() V209() V210() V211() Element of K19(REAL)
Product (<*> NAT) 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 ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V102() finite-support FinSequence 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
n is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
S is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of SetPrimes
x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of SetPrimes
<*x*> is Relation-like NAT -defined SetPrimes -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of SetPrimes *
SetPrimes * is functional non empty FinSequence-membered FinSequenceSet of SetPrimes
[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
{[1,x]} is Relation-like Function-like constant non empty V12() finite 1 -element finite-support set
S ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of SetPrimes
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)
t is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
s is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V102() finite-support FinSequence 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
(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
e is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
{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
e is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
<*> SetPrimes is Relation-like non-empty empty-yielding NAT -defined SetPrimes -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() FinSequence-yielding finite-support V208() V209() V210() V211() Element of SetPrimes *
Product (<*> SetPrimes) 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 (<*> SetPrimes) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V58() complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() FinSequence-yielding finite-support V208() V209() V210() V211() Element of K19(REAL)
S is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
S is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of SetPrimes
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)
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support set
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
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
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
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
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 Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
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
e is ordinal natural complex V37() V38() finite cardinal ext-real non negative 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
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n,S) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
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
n is Relation-like NAT -defined RAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n,S) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support set
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 is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(n . x) |^ S is ordinal natural complex V37() V38() finite cardinal ext-real non negative Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n,S) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support set
rng (n,S) is finite V80() V81() V82() V208() V209() V210() Element of K19(REAL)
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V102() finite-support FinSequence of NAT
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n,S) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support set
(n,S) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
rng (n,S) is finite V80() V81() V82() V208() V209() V210() Element of K19(REAL)
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
(n,0) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence 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) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite len n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V102() finite-support Element of (len n) -tuples_on NAT
(len n) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = len n } 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
(Seg (len n)) --> 1 is Relation-like Seg (len n) -defined RAT -valued INT -valued {1} -valued Function-like V14( Seg (len n)) quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support Element of K19(K20((Seg (len n)),{1}))
{1} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
K20((Seg (len n)),{1}) is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued 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
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(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
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
(n,1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
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
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(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
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() FinSequence-yielding finite-support V208() V209() V210() V211() Element of REAL *
REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
((<*> REAL),n) is Relation-like NAT -defined REAL -valued RAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of REAL
len ((<*> REAL),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 (<*> REAL) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V57() complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() FinSequence-yielding finite-support V208() V209() V210() V211() Element of NAT
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is complex V37() ext-real Element of REAL
<*S*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V74() decreasing non-decreasing non-increasing finite-support 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
{[1,S]} is Relation-like Function-like constant non empty V12() finite 1 -element finite-support set
(<*S*>,n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
S |^ n is complex V37() ext-real Element of REAL
<*(S |^ n)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V74() decreasing non-decreasing non-increasing finite-support 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
{[1,(S |^ n)]} is Relation-like Function-like constant non empty V12() finite 1 -element finite-support 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
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is complex V37() ext-real Element of REAL
<*S*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V74() decreasing non-decreasing non-increasing finite-support 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
{[1,S]} is Relation-like Function-like constant non empty V12() finite 1 -element finite-support set
(<*S*>,n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
x is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
x ^ <*S*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
((x ^ <*S*>),n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
(x,n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
(x,n) ^ (<*S*>,n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
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) + (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) + 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
m is ordinal natural complex V37() V38() finite cardinal ext-real non negative 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
<*(S |^ n)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V74() decreasing non-decreasing non-increasing finite-support 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
{[1,(S |^ n)]} is Relation-like Function-like constant non empty V12() finite 1 -element finite-support set
(x,n) ^ <*(S |^ n)*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
((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
<*(S |^ n)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V74() decreasing non-decreasing non-increasing finite-support 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
{[1,(S |^ n)]} is Relation-like Function-like constant non empty V12() finite 1 -element finite-support 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 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
S is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
(S,(n + 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
Product (S,(n + 1)) is complex V37() ext-real Element of REAL
(S,n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
Product (S,n) is complex V37() ext-real Element of REAL
Product S is complex V37() ext-real Element of REAL
(Product (S,n)) * (Product S) is complex V37() ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
Product x is complex V37() ext-real Element of REAL
m is complex V37() ext-real Element of REAL
<*m*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V74() decreasing non-decreasing non-increasing finite-support 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
{[1,m]} is Relation-like Function-like constant non empty V12() finite 1 -element finite-support set
x ^ <*m*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
Product (x ^ <*m*>) is complex V37() ext-real Element of REAL
s is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
((x ^ <*m*>),(s + 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
Product ((x ^ <*m*>),(s + 1)) is complex V37() ext-real Element of REAL
((x ^ <*m*>),s) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence 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
(x,(s + 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
(<*m*>,(s + 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
(x,(s + 1)) ^ (<*m*>,(s + 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence 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
(x,s) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
Product (x,s) is complex V37() ext-real Element of REAL
(Product (x,s)) * (Product x) is complex V37() ext-real Element of REAL
((Product (x,s)) * (Product x)) * (Product (<*m*>,(s + 1))) is complex V37() ext-real Element of REAL
m |^ (s + 1) is complex V37() ext-real Element of REAL
<*(m |^ (s + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V74() decreasing non-decreasing non-increasing finite-support 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 x)) * (Product <*(m |^ (s + 1))*>) is complex V37() ext-real Element of REAL
((Product (x,s)) * (Product x)) * (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)) * (Product x)) * ((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) * (Product x) is complex V37() ext-real Element of REAL
<*(m |^ s)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V74() decreasing non-decreasing non-increasing finite-support 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
{[1,(m |^ s)]} is Relation-like Function-like constant non empty V12() finite 1 -element finite-support set
(x,s) ^ <*(m |^ s)*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence 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) * (Product x) is complex V37() ext-real Element of REAL
(<*m*>,s) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
(x,s) ^ (<*m*>,s) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence 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) * (Product x) 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) * (Product x) is complex V37() ext-real Element of REAL
(Product x) * m is complex V37() ext-real Element of REAL
(Product ((x ^ <*m*>),s)) * ((Product x) * m) is complex V37() ext-real Element of REAL
Product (<*> REAL) is complex V37() ext-real Element of REAL
m is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
((<*> REAL),(m + 1)) is Relation-like NAT -defined REAL -valued RAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of REAL
Product ((<*> REAL),(m + 1)) is complex V37() ext-real Element of REAL
((<*> REAL),m) is Relation-like NAT -defined REAL -valued RAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of REAL
Product ((<*> REAL),m) is complex V37() ext-real Element of REAL
(Product ((<*> REAL),m)) * (Product (<*> REAL)) is complex V37() ext-real Element of REAL
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
(S,n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
Product (S,n) is complex V37() ext-real Element of REAL
Product S is complex V37() ext-real Element of REAL
(Product S) |^ n is complex V37() ext-real Element of REAL
x is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(S,x) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
Product (S,x) is complex V37() ext-real Element of REAL
(Product S) |^ 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
(S,(x + 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
Product (S,(x + 1)) is complex V37() ext-real Element of REAL
(Product S) |^ (x + 1) is complex V37() ext-real Element of REAL
(Product (S,x)) * (Product S) is complex V37() ext-real Element of REAL
(S,0) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence 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
(len S) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite len S -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V102() finite-support Element of (len S) -tuples_on NAT
(len S) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = len S } 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
(Seg (len S)) --> 1 is Relation-like Seg (len S) -defined RAT -valued INT -valued {1} -valued Function-like V14( Seg (len S)) quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support Element of K19(K20((Seg (len S)),{1}))
{1} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
K20((Seg (len S)),{1}) is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued 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
(Product S) |^ 0 is complex V37() ext-real Element of REAL
n is set
the Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued finite-support set is Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued finite-support set
n is set
x is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
m is Relation-like n -defined Function-like V14(n) 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
m is Relation-like n -defined Function-like V14(n) set
e is Relation-like n -defined Function-like V14(n) set
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
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
x is ordinal natural complex V37() V38() finite cardinal ext-real non negative 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
S is Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued set
x is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n,S,x) is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued 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
S . m is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() 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
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
(n,S,0) is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued 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
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is set
x is Relation-like S -defined Function-like V14(S) complex-valued ext-real-valued real-valued set
support x is set
(S,x,n) is Relation-like S -defined Function-like V14(S) complex-valued ext-real-valued real-valued 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
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued finite-support set
x is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n,S,x) is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
support (n,S,x) is set
support (n,S,x) is set
support S is finite set
n is set
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
x is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
m is Relation-like n -defined Function-like V14(n) 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
m is Relation-like n -defined Function-like V14(n) set
e is Relation-like n -defined Function-like V14(n) 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
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
x is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued 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
S is Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued set
x is Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued set
(n,S,x) is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
m is set
dom (n,S,x) is set
(n,S,x) . m is complex V37() ext-real set
S . m is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
x . m is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
n is set
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued finite-support set
x is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued finite-support set
(n,S,x) is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
support (n,S,x) is set
support S is finite set
support x is finite set
(support S) \/ (support x) is finite set
e is set
(n,S,x) . e is complex V37() ext-real Element of REAL
S . e is complex V37() ext-real Element of REAL
x . e is complex V37() ext-real Element of REAL
n is set
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued finite-support set
x is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued finite-support set
(n,S,x) is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
support (n,S,x) is set
support S is finite set
support x is finite set
(support S) \/ (support x) is finite set
n is set
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
x is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
m is Relation-like n -defined Function-like V14(n) 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
m is Relation-like n -defined Function-like V14(n) set
e is Relation-like n -defined Function-like V14(n) 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
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
x is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued 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
S is Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued set
x is Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued set
(n,S,x) is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
m is set
dom (n,S,x) is set
(n,S,x) . m is complex V37() ext-real set
S . m is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
x . m is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
n is set
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued finite-support set
x is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued finite-support set
(n,S,x) is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
support (n,S,x) is set
support S is finite set
support x is finite set
(support S) \/ (support x) is finite set
e is set
(n,S,x) . e is complex V37() ext-real Element of REAL
S . e is complex V37() ext-real Element of REAL
x . e is complex V37() ext-real Element of REAL
n is set
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued finite-support set
x is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued finite-support set
(n,S,x) is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
support (n,S,x) is set
support S is finite set
support x is finite set
(support S) \/ (support x) is finite set
n is set
the Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued finite-support set is Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued finite-support set
n is set
S is Relation-like n -defined Function-like V14(n) complex-valued finite-support set
support S is finite set
canFS (support S) is Relation-like NAT -defined support S -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of support S
(canFS (support S)) * S is Relation-like NAT -defined Function-like finite complex-valued finite-support set
rng ((canFS (support S)) * S) is finite V80() set
dom S is set
rng (canFS (support S)) is finite set
dom ((canFS (support S)) * S) is finite set
dom (canFS (support S)) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
len (canFS (support 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
Seg (len (canFS (support S))) is finite len (canFS (support 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 (canFS (support S)) ) } is set
e is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support FinSequence of COMPLEX
Product e is complex Element of COMPLEX
x is complex set
e is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support FinSequence of COMPLEX
Product e is complex Element of COMPLEX
m is complex set
s is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support FinSequence of COMPLEX
Product s is complex Element of COMPLEX
n is set
S is Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued finite-support set
(n,S) is complex set
support S is finite Element of K19(n)
K19(n) is set
canFS (support S) is Relation-like NAT -defined support S -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of support S
(canFS (support S)) * S is Relation-like NAT -defined RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
x is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support FinSequence of COMPLEX
Product x is complex Element of COMPLEX
rng S is V80() V81() V82() V83() V84() V85() V208() Element of K19(REAL)
rng x is finite V80() set
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V102() finite-support FinSequence of NAT
Product 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
S is Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued finite-support set
support S is finite Element of K19(n)
K19(n) is set
x is Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued finite-support set
support x is finite Element of K19(n)
S + x is Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued finite-support set
(n,(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
(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
(n,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,S) * (n,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
support (S + x) is finite Element of K19(n)
canFS (support S) is Relation-like NAT -defined support S -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of support S
canFS (support x) is Relation-like NAT -defined support x -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of support x
(canFS (support S)) ^ (canFS (support x)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
canFS (support (S + x)) is Relation-like NAT -defined support (S + x) -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of support (S + x)
((canFS (support S)) ^ (canFS (support x))) " is Relation-like Function-like set
(canFS (support (S + x))) * (((canFS (support S)) ^ (canFS (support x))) ") is Relation-like NAT -defined Function-like finite finite-support set
rng (canFS (support (S + x))) is finite set
(support S) /\ (support x) is finite Element of K19(n)
rng (canFS (support S)) is finite set
(support S) \/ (support x) is finite Element of K19(n)
rng (canFS (support x)) is finite set
rng ((canFS (support S)) ^ (canFS (support x))) is finite set
len (canFS (support 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
card (support 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 omega
len (canFS (support 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
card (support 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 omega
len ((canFS (support S)) ^ (canFS (support 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
(card (support S)) + (card (support 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
card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V57() complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() FinSequence-yielding finite-support V208() V209() V210() V211() Element of omega
((card (support S)) + (card (support x))) - (card {}) is complex V37() V38() ext-real V57() Element of INT
card (support (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 omega
dom (((canFS (support S)) ^ (canFS (support x))) ") is set
rng ((canFS (support (S + x))) * (((canFS (support S)) ^ (canFS (support x))) ")) is finite set
rng (((canFS (support S)) ^ (canFS (support x))) ") is set
dom ((canFS (support S)) ^ (canFS (support x))) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
Seg (card (support (S + x))) is finite card (support (S + 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 <= card (support (S + x)) ) } is set
(canFS (support S)) * S is Relation-like NAT -defined RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
u is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support FinSequence of COMPLEX
Product u is complex Element of COMPLEX
(canFS (support x)) * x is Relation-like NAT -defined RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
w is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support FinSequence of COMPLEX
Product w is complex Element of COMPLEX
u ^ w is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support FinSequence of COMPLEX
(canFS (support (S + x))) * (S + x) is Relation-like NAT -defined RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
f is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support FinSequence of COMPLEX
Product f is complex Element of COMPLEX
dom S is set
dom (canFS (support S)) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
dom u is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
len u 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 (canFS (support (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
dom (canFS (support (S + x))) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
dom ((canFS (support (S + x))) * (((canFS (support S)) ^ (canFS (support x))) ")) is finite set
dom (S + x) is set
dom f is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
dom x is set
dom (canFS (support x)) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
dom w is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
len w 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 (u ^ w) 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 (u ^ w) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(NAT)
K20((dom (u ^ w)),(dom (u ^ w))) is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((dom (u ^ w)),(dom (u ^ w)))) is finite V46() set
p is Relation-like dom (u ^ w) -defined dom (u ^ w) -valued Function-like V14( dom (u ^ w)) quasi_total finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K19(K20((dom (u ^ w)),(dom (u ^ w))))
p is Relation-like dom (u ^ w) -defined dom (u ^ w) -valued Function-like one-to-one V14( dom (u ^ w)) quasi_total onto bijective finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K19(K20((dom (u ^ w)),(dom (u ^ w))))
p * (u ^ w) is Relation-like dom (u ^ w) -defined COMPLEX -valued Function-like finite complex-valued finite-support set
dom (p * (u ^ w)) is finite set
(len (canFS (support S))) + (len (canFS (support 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 set
(canFS (support (S + x))) . x is set
(((canFS (support S)) ^ (canFS (support x))) ") . ((canFS (support (S + x))) . x) is set
(p * (u ^ w)) . x is complex set
p . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative Element of REAL
(u ^ w) . (p . x) is complex set
(u ^ w) . ((((canFS (support S)) ^ (canFS (support x))) ") . ((canFS (support (S + x))) . x)) is complex set
d is set
((canFS (support S)) ^ (canFS (support x))) . d is set
cgx is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
cgxN is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(len u) + (len w) 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
cgx - (len (canFS (support S))) is complex V37() V38() ext-real V57() Element of INT
((len (canFS (support S))) + (len (canFS (support x)))) - (len (canFS (support S))) is complex V37() V38() ext-real V57() Element of INT
(len u) + 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
(len (canFS (support 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
((len (canFS (support S))) + 1) - (len (canFS (support S))) is complex V37() V38() ext-real V57() Element of INT
((canFS (support S)) ^ (canFS (support x))) . cgxN is set
(canFS (support x)) . (cgx - (len (canFS (support S)))) is set
((canFS (support S)) ^ (canFS (support x))) . cgx is set
(canFS (support S)) . cgx is set
(u ^ w) . cgx is complex set
u . cgxN is complex set
S . ((canFS (support (S + x))) . x) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
f . x is complex set
(S + x) . ((canFS (support (S + x))) . x) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
x . ((canFS (support (S + x))) . x) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(S . ((canFS (support (S + x))) . x)) + (x . ((canFS (support (S + x))) . 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
(S . ((canFS (support (S + x))) . 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
(len u) + 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
(canFS (support S)) . cgx is set
((canFS (support S)) ^ (canFS (support x))) . cgxN is set
((canFS (support S)) ^ (canFS (support x))) . cgx is set
cgx - (len (canFS (support S))) is complex V37() V38() ext-real V57() Element of INT
(canFS (support x)) . (cgx - (len (canFS (support S)))) is set
((len (canFS (support S))) + (len (canFS (support x)))) - (len (canFS (support S))) is complex V37() V38() ext-real V57() Element of INT
(len (canFS (support 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
((len (canFS (support S))) + 1) - (len (canFS (support S))) is complex V37() V38() ext-real V57() Element of INT
cgxN - (len (canFS (support S))) is complex V37() V38() ext-real V57() Element of INT
(u ^ w) . cgx is complex set
cgxN - (len u) is complex V37() V38() ext-real V57() Element of INT
w . (cgxN - (len u)) is complex set
x . ((canFS (support (S + x))) . x) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
f . x is complex set
(S + x) . ((canFS (support (S + x))) . x) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
S . ((canFS (support (S + x))) . x) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(S . ((canFS (support (S + x))) . x)) + (x . ((canFS (support (S + x))) . 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
0 + (x . ((canFS (support (S + x))) . 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
multcomplex $$ f is complex Element of COMPLEX
multcomplex $$ (u ^ w) is complex Element of COMPLEX
Product (u ^ w) is complex Element of COMPLEX
n is set
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued set
support S is set
x is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
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 set
s is Element of n
S . s is complex V37() ext-real Element of REAL
(S . s) |^ x is complex V37() ext-real Element of REAL
e is Relation-like Function-like set
dom e is set
s is Relation-like n -defined Function-like V14(n) set
support s is set
dom S is set
t is set
S . t is complex V37() ext-real Element of REAL
(S . t) |^ x is complex V37() ext-real Element of REAL
s . t is set
s is Element of n
S . s is complex V37() ext-real Element of REAL
(S . s) |^ x is complex V37() ext-real Element of REAL
(S . t) |^ m is complex V37() ext-real Element of REAL
s is Element of n
S . s is complex V37() ext-real Element of REAL
(S . s) |^ x is complex V37() ext-real Element of REAL
0 |^ m is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(S . t) |^ m is complex V37() ext-real Element of REAL
(S . t) |^ m is complex V37() ext-real Element of REAL
(S . t) |^ m is complex V37() ext-real Element of REAL
t is set
s . t is set
S . t is complex V37() ext-real Element of REAL
(S . t) |^ x is complex V37() ext-real Element of REAL
s is Element of n
S . s is complex V37() ext-real Element of REAL
(S . s) |^ x is complex V37() ext-real Element of REAL
0 |^ x is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
m is Relation-like n -defined Function-like V14(n) set
support m is set
e is Relation-like n -defined Function-like V14(n) set
support e is set
s is set
m . s is set
S . s is complex V37() ext-real Element of REAL
(S . s) |^ x is complex V37() ext-real Element of REAL
e . s is set
n is set
S is Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued set
x is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative 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 ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(S . m) |^ x is ordinal natural complex V37() V38() finite cardinal ext-real non negative Element of REAL
n is set
S is Relation-like n -defined Function-like V14(n) complex-valued ext-real-valued real-valued finite-support set
x is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n,S,x) is Relation-like n -defined Function-like V14(n) set
support (n,S,x) is set
support S is finite set
n is set
EmptyBag n is Relation-like n -defined RAT -valued Function-like V14(n) complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags n
Bags n is non empty set
Bags n is functional non empty Element of K19((Bags n))
K19((Bags n)) is set
n --> 0 is Relation-like n -defined NAT -valued RAT -valued INT -valued Function-like V14(n) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(n,NAT))
K20(n,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(n,NAT)) is set
(n,(EmptyBag 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
support (EmptyBag n) is finite Element of K19(n)
K19(n) is set
canFS (support (EmptyBag n)) is Relation-like NAT -defined support (EmptyBag n) -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of support (EmptyBag n)
(canFS (support (EmptyBag n))) * (EmptyBag n) is Relation-like NAT -defined RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
<*> COMPLEX is Relation-like non-empty empty-yielding NAT -defined COMPLEX -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() FinSequence-yielding finite-support V208() V209() V210() V211() Element of COMPLEX *
COMPLEX * is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S |^ 0 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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 |^ (0 + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
0 |^ 0 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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 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 set
S |^ m is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S |^ 0 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
m is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S |^ m is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
m + 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
m is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S |^ m is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
e is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S |^ e is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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 |^ (e + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
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
s is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
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
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
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
s + 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
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 |^ (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
x |^ (s + 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
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
s is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
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
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 + 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
t + 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
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 |^ (t + 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
x |^ (t + 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 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 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 ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n,S) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(1,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
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
n |^ (0 + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n |^ 1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n |^ 0 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n,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 + 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 |^ (1 + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n |^ 2 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n |^ 1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative 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
S |^ 0 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S |^ 1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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 |^ (0 + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
(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
n |^ 0 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n |^ 1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
n |^ (0 + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n |^ S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
((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
m 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
m |^ 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
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 |^ (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
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
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(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
n |^ (S,n) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(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
n |^ 0 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
n |^ (0 + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
n |^ (0 + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
x is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S * 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
((S * 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
(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
(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
(S,n) + (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
n |^ (x,n) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n |^ (S,n) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
((S,n) + (x,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
n |^ (((S,n) + (x,n)) + 1) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
s is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n |^ (((S,n) + (x,n)) + 1)) * 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,n) + (x,n)) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n |^ ((S,n) + (x,n))) * 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 * 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,n) + (x,n))) * (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
t is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n |^ (S,n)) * 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
(S,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
n |^ ((S,n) + 1) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(x,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
n |^ ((x,n) + 1) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
s is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n |^ (x,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
(n |^ (S,n)) * (n |^ (x,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 |^ (S,n)) * (n |^ (x,n))) * 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
(((n |^ (S,n)) * (n |^ (x,n))) * 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
(n |^ ((S,n) + (x,n))) * 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
((n |^ ((S,n) + (x,n))) * 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
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
(n |^ ((S,n) + (x,n))) * (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
t is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n * 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
(n |^ (S,n)) * 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 |^ (S,n)) * n) * 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
(n |^ ((S,n) + 1)) * 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 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n * 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
(n |^ (x,n)) * 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 |^ (x,n)) * n) * 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
(n |^ ((x,n) + 1)) * 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
n is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
x is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S * 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
((S * 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
n |^ ((S * x),n) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(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
n |^ (S,n) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(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
n |^ (x,n) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n |^ (S,n)) * (n |^ (x,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
(S,n) + (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
n |^ ((S,n) + (x,n)) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
x is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(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
(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 div 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
((S div 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
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
n |^ ((S div x),n) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n |^ (x,n) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
1 * (n |^ (x,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 |^ ((S div x),n)) * (n |^ (x,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
x * (S div 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 |^ (S,n) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
x is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S div 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
((S div 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
(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
(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
(S,n) -' (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
x * (S div 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 * (S div 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
(x,n) + ((S div 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
((S div x),n) + (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
(S,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
(x,n) - (x,n) is complex V37() V38() ext-real V57() Element of INT
(S,n) - (x,n) is complex V37() V38() ext-real V57() Element of INT
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
x is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
x |^ n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
((x |^ 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,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 * (x,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 set
x |^ m is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
((x |^ m),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 * (x,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 + 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 |^ (m + 1) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
((x |^ (m + 1)),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 + 1) * (x,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) * 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
(((x |^ m) * x),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,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 * (x,S)) + (1 * (x,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 |^ 0 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
((x |^ 0),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,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
0 * (x,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 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is set
x is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
(n,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
S is Relation-like SetPrimes -defined Function-like V14( SetPrimes ) set
x is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
S . x is set
(n,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
m is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n,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
S is Relation-like SetPrimes -defined Function-like V14( SetPrimes ) set
x is Relation-like SetPrimes -defined Function-like V14( SetPrimes ) set
m is set
S . m is set
e is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() 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
x . m is set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n) is Relation-like SetPrimes -defined Function-like V14( SetPrimes ) set
dom (n) is set
S is set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n) is Relation-like SetPrimes -defined Function-like V14( SetPrimes ) set
support (n) is set
S is set
dom (n) is set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(S) is Relation-like SetPrimes -defined Function-like V14( SetPrimes ) set
(S) . n is set
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 (S) is set
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
(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
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 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n) is Relation-like SetPrimes -defined Function-like V14( SetPrimes ) set
S is set
dom (n) is set
(n) . S is set
m is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
(n) . m is set
(n,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 ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued set
support (S) is set
m is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
(S) . m is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(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 ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued set
support (n) is set
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative 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
(n) . S is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued set
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
{ H1(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 : ( 0 <= b1 & b1 <= x & S1[b1] ) } is set
support (n) is set
e is set
s is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
(n) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
n is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(S) . n is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
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
n |^ (0 + 1) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(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
(1) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
EmptyBag SetPrimes is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags SetPrimes
Bags SetPrimes is non empty set
Bags SetPrimes is functional non empty Element of K19((Bags SetPrimes))
K19((Bags SetPrimes)) is set
SetPrimes --> 0 is Relation-like SetPrimes -defined NAT -valued RAT -valued INT -valued Function-like non empty V14( SetPrimes ) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(SetPrimes,NAT))
K20(SetPrimes,NAT) is Relation-like RAT -valued INT -valued non empty V12() non finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20(SetPrimes,NAT)) is non empty V12() non finite set
dom (1) is set
S is set
(1) . S is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
x is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
(1) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(1,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 (1)) --> 0 is Relation-like dom (1) -defined NAT -valued RAT -valued INT -valued Function-like V14( dom (1)) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((dom (1)),NAT))
K20((dom (1)),NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20((dom (1)),NAT)) is set
support (1) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
K19(SetPrimes) is non empty V12() non finite set
S is set
(1) . S is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
S |^ n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
((S |^ n)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
((S |^ n)) . S is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((S |^ 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
n is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(n) . n is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
n |^ 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
S |^ n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
((S |^ n)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support ((S |^ n)) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
{S} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
((S |^ n)) . S is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
m is set
e is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
((S |^ n)) . e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((S |^ 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
m is set
n is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
{n} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
n |^ 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n |^ S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
((n |^ S)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support ((n |^ S)) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
{n} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
n is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
{n} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (S) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
n gcd S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
e is set
s is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
(n) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(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
(S) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(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
s |^ (S,s) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
s |^ (n,s) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n * 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
((n * S)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support ((n * S)) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
e is set
s is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
(n) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(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
s |^ (n,s) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
s |^ 1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
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 |^ (0 + 1) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
((n * S)) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((n * 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
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n * 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
((n * S)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support ((n * S)) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (S) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
(support (n)) \/ (support (S)) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
s is set
t is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
((n * S)) . t is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((n * S),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 |^ ((n * S),t) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n,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 |^ (n,t) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(S,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 |^ (S,t) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(t |^ (n,t)) * (t |^ (S,t)) 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) . t is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(S) . t is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n * 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
((n * S)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support ((n * S)) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
card (support ((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 omega
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
card (support (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 omega
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (S) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
card (support (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 omega
(card (support (n))) + (card (support (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
(support (n)) \/ (support (S)) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n |^ S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
((n |^ S)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support ((n |^ S)) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
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
n |^ (S -' 1) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n |^ (S -' 1)) * 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
e is set
s is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
((n |^ S)) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((n |^ 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
(n) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n * 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
((n * S)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(n) + (S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
x is set
((n * S)) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((n) + (S)) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
m is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
((n * 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,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
(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,m) + (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) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((n) . 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
(S) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((n) . x) + ((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
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S div 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 div n)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued set
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(S) -' (n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
x is set
((S div n)) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((S) -' (n)) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
m is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
((S div n),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
(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,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
(S,m) -' (n,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
(S) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((S) . x) -' (n,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) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((S) . x) -' ((n) . 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 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S |^ n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
((S |^ n)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(SetPrimes,(S),n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
x is set
((S |^ n)) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(SetPrimes,(S),n) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
m is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
((S |^ n),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
(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 * (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
(S) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
n * ((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
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
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
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
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) 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 is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S gcd n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
((S gcd n)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued set
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(SetPrimes,(S),(n)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
e is set
s is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() 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
(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
((S gcd 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
((S gcd n)) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
s |^ (S,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
s |^ ((S gcd n),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
((S gcd n),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
s |^ (((S gcd n),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
(n,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
s |^ ((n,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
s |^ (n,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
(S) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(n) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(S,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
s |^ ((S,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
((S gcd n)) . e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(SetPrimes,(S),(n)) . e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(SetPrimes,(S),(n)) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(SetPrimes,(S),(n)) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S lcm n is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
((S lcm n)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued set
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(SetPrimes,(S),(n)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
e is set
s is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() 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
(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
((S lcm 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
((S lcm n)) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(S) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(S,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
s |^ ((S,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
s |^ ((S lcm n),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
((S lcm n),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
s |^ (((S lcm n),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
(n) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
s |^ (S,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
(n,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
s |^ ((n,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
s |^ (n,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
((S lcm n)) . e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(SetPrimes,(S),(n)) . e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
s1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(S,s) + s1 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
t1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(s |^ (S,s)) * t1 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
f is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
s * f 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,s)) * 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
((s |^ (S,s)) * s) * f 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,s) + 1)) * f 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
f is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S * f 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 set
(s |^ ((n,s) + 1)) * 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
(s |^ (n,s)) * 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
((s |^ (n,s)) * 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
x * 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
(s |^ (n,s)) * (x * 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
s |^ s1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative Element of REAL
(s |^ s1) * (x * 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
(s |^ (S,s)) * ((s |^ s1) * (x * 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
(s |^ (S,s)) * (s |^ s1) 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 |^ (S,s)) * (s |^ s1)) * (x * 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
t1 * f 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,s)) * (t1 * f) 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 |^ s1) * 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
((s |^ s1) * x) * 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 set
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
(s |^ (n,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
((s |^ (n,s)) * x) * 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
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
(S * m) * 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
g is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(s |^ (n,s)) * g 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
u is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
s * u 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,s)) * s) * u 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,s) + 1)) * u 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
u is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n * u 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
g * u 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,s)) * (g * u) 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
w is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
s * w 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 * w 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 * w) * 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
(s |^ (n,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
(SetPrimes,(S),(n)) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
s1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(n,s) + s1 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
t1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(s |^ (n,s)) * t1 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
f is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
s * f 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,s)) * 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
((s |^ (n,s)) * s) * f 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,s) + 1)) * f 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
f is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
n * f 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 set
(s |^ ((S,s) + 1)) * 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
(s |^ (S,s)) * 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
((s |^ (S,s)) * 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
x * 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
(s |^ (S,s)) * (x * 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
s |^ s1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative Element of REAL
(s |^ s1) * (x * 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
(s |^ (n,s)) * ((s |^ s1) * (x * 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
(s |^ (n,s)) * (s |^ s1) 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 |^ (n,s)) * (s |^ s1)) * (x * 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
t1 * f 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,s)) * (t1 * f) 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 |^ s1) * 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
((s |^ s1) * x) * 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 set
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
(s |^ (S,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
((s |^ (S,s)) * x) * 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 * 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 * m) * 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
g is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(s |^ (S,s)) * g 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
u is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
s * u 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,s)) * s) * u 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,s) + 1)) * u 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
u is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S * u 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
g * u 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,s)) * (g * u) 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
w is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
s * w 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 * w 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 * w) * 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
(s |^ (S,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
(SetPrimes,(S),(n)) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
S is set
x is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
(n,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 |^ (n,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
m is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
(n,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 |^ (n,m) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
x is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
m is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
(n,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 |^ (n,m) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
x is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
S is Relation-like Function-like set
dom S is set
support S is set
x is set
m is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
S . m is set
m is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
S . m is set
(n,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 |^ (n,m) 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 Relation-like SetPrimes -defined Function-like V14( SetPrimes ) set
support x is set
m is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
x . m is set
(n,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 |^ (n,m) is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
S is Relation-like SetPrimes -defined Function-like V14( SetPrimes ) set
support S is set
x is Relation-like SetPrimes -defined Function-like V14( SetPrimes ) set
support x is set
m is set
e is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
S . m is set
(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
e |^ (n,e) 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 . m is set
e is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
S . m is set
x . m is set
e is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined Function-like V14( SetPrimes ) set
rng (n) is set
S is set
dom (n) is set
x is set
(n) . x is set
m is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
(n) . m is set
(n,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 |^ (n,m) 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 non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
support (n) is set
(n) . m is set
m is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
support (n) is set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
n is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(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) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(S) . n is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(S) . n is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
support (S) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
support (S) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
n is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(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) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(S) . n is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
n |^ (S,n) is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(S) . n is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
support (S) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n * 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
((n * S)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(n) + (S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
n gcd S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
e is set
s is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
x is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
m is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
x * m 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 * m),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) 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
(n,s) + (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
((n * 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
((n * S)) . e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(S) . e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
0 + ((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
(n) . e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((n) . 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
((n) + (S)) . e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((n * 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
((n * S)) . e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((n) + (S)) . e is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
t is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
t + 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 |^ (n,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
s |^ t is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative Element of REAL
s * (s |^ t) 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 set
(s * (s |^ 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
(s |^ 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
s * ((s |^ 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
t is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
t + 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 |^ (S,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
s |^ t is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative Element of REAL
s * (s |^ t) 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
s1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(s * (s |^ t)) * s1 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 |^ t) * s1 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 |^ t) * s1) 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 is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((n) . s) + 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) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((n) . s) + ((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
t is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
t + 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 |^ (n,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
s |^ t is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative Element of REAL
s * (s |^ t) 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 set
(s * (s |^ 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
(s |^ 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
s * ((s |^ 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
t is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
t + 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 |^ (S,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
s |^ t is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative Element of REAL
s * (s |^ t) 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
s1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(s * (s |^ t)) * s1 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 |^ t) * s1 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 |^ t) * s1) 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() Element of REAL
0 + ((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
(n) . s is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((n) . s) + ((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
((n * 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
n is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n |^ S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
((n |^ S)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
((n |^ S)) . n is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((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
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
n |^ S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
((n |^ S)) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(SetPrimes,(n),S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
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 set
(SetPrimes,(n),S) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
(n) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
((n) . x) |^ S is ordinal natural complex V37() V38() finite cardinal ext-real non negative Element of REAL
m is non empty ordinal natural complex V37() V38() prime finite cardinal ext-real positive non negative V57() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of NAT
((n |^ 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,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
S * (n,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 |^ S)) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
0 |^ S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
((n |^ S)) . x is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
m |^ ((n |^ S),m) 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 |^ (n,m) 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 |^ (n,m)) |^ S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative Element of REAL
n is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(SetPrimes,(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
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (n) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
Seg 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() ordinal natural complex V37() V38() Function-yielding finite finite-yielding V46() cardinal 0 -element {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V80() V81() V82() V83() V84() V85() V86() FinSequence-yielding finite-support V208() V209() V210() V211() 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 <= 0 ) } is set
S is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (S) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
(SetPrimes,(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 set
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
(S) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (S) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
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
S is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
Seg S is finite 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 <= S ) } is set
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
Seg (S + 1) is non empty finite S + 1 -element K244(S,1) -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of K19(NAT)
K244(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
{ 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 <= S + 1 ) } is set
x is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(x) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (x) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
(SetPrimes,(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 Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (x) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
(x,(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) |^ (x,(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
t is set
s is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
t is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
((S + 1) |^ (x,(S + 1))) * 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
s is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(s) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
dom (s) is set
(x) . (S + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
t is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
(t) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (t) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
(t) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (t) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
(t,(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
x is set
m is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
(t) . (S + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
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
g is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
1 + g 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) |^ (t,(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
u is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
((S + 1) |^ (t,(S + 1))) * u 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) |^ g is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative Element of REAL
((S + 1) |^ g) * (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
(((S + 1) |^ g) * (S + 1)) * u 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 + 1) |^ g) * (S + 1)) * u) 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 + 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) |^ g) * u 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 + 1)) * (((S + 1) |^ g) * u) 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,(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
(S + 1) |^ ((x,(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
((S + 1) |^ ((x,(S + 1)) + 1)) * (((S + 1) |^ g) * u) 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
s1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
t1 is non empty ordinal natural complex V37() V38() finite cardinal ext-real positive non negative set
s1 gcd t1 is ordinal natural complex V37() V38() finite cardinal ext-real non negative set
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
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
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
(s) + (t) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(SetPrimes,(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
support (s) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
canFS (support (s)) is Relation-like NAT -defined support (s) -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of support (s)
(canFS (support (s))) * (s) is Relation-like NAT -defined RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
f is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support FinSequence of COMPLEX
Product f is complex Element of COMPLEX
(s) is Relation-like SetPrimes -defined RAT -valued Function-like V14( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (s) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
{(S + 1)} is non empty V12() finite V46() 1 -element V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
<*(S + 1)*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V74() decreasing non-decreasing non-increasing V102() finite-support Element of NAT *
[1,(S + 1)] is non empty set
{1,(S + 1)} 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,(S + 1)},{1}} is non empty finite V46() set
{[1,(S + 1)]} is Relation-like Function-like constant non empty V12() finite 1 -element finite-support set
<*(S + 1)*> * (s) is Relation-like NAT -defined RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
(s) . (S + 1) is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() Element of REAL
<*((s) . (S + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V74() decreasing non-decreasing non-increasing finite-support Element of REAL *
[1,((s) . (S + 1))] is non empty set
{1,((s) . (S + 1))} is non empty finite V46() V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() set
{{1,((s) . (S + 1))},{1}} is non empty finite V46() set
{[1,((s) . (S + 1))]} is Relation-like Function-like constant non empty V12() finite 1 -element finite-support set
(support (s)) /\ (support (t)) is finite V80() V81() V82() V83() V84() V85() V208() V209() V210() Element of K19(SetPrimes)
x is set
(SetPrimes,(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
S is non empty finite V80() V81() V82() V83() V84() V85() V206() V207() V208() V209() V210() Element of K19(NAT)
max S is ordinal natural complex V37() V38() finite cardinal ext-real non negative V57() set
Seg (max S) is finite max 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 <= max S ) } is set
x is set
m is ordinal natural complex V37() V38() finite cardinal ext-real non negative set