:: MOEBIUS1 semantic presentation

REAL is non empty non trivial non finite V73() V74() V75() V79() V210() V211() V213() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V73() V74() V75() V76() V77() V78() V79() V208() V210() Element of bool REAL
bool REAL is non trivial non finite set
bool NAT is non trivial non finite set
COMPLEX is non empty non trivial non finite V73() V79() set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V73() V74() V75() V76() V77() V78() V79() V208() V210() set
bool omega is non trivial non finite set
K148(NAT) is V35() set
RAT is non empty non trivial non finite V73() V74() V75() V76() V79() set
INT is non empty non trivial non finite V73() V74() V75() V76() V77() V79() set

bool is non trivial non finite set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
{{},1} is non empty finite V40() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() set
K375() is set
bool K375() is set
K376() is Element of bool K375()
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

bool is non trivial non finite set

bool is non trivial non finite set
K219(1,NAT) is M10( NAT )
SetPrimes is non empty non trivial non finite V73() V74() V75() V76() V77() V78() V208() V210() Element of bool NAT
is non trivial non finite complex-valued set
bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
K38(1) is non empty V11() real V13() ext-real non positive negative set
Seg 1 is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
{1} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() set
Seg 2 is non empty finite 2 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
{1,2} is non empty finite V40() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() set
n is set
x is set
k is set
k1 is set
n /\ k1 is set
x /\ k1 is set
F1() is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
F2() is set
[:NAT,F2():] is set
bool [:NAT,F2():] is set
n is set
F3(n) is set
n is Relation-like NAT -defined F2() -valued Function-like V29( NAT ,F2()) Element of bool [:NAT,F2():]
n is Relation-like NAT -defined F2() -valued Function-like V29( NAT ,F2()) Element of bool [:NAT,F2():]
n . 0 is Element of F2()
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n . x is Element of F2()
F3(x) is set

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

Seg x is finite x -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
n * k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT

Seg (n * x) is finite n * x -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
1 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() non prime finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
bool SetPrimes is non trivial non finite set

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
{n} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() set

support () is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool SetPrimes

(x |^ 2) * k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x * x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(x * x) * k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x * k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x * (x * k1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
x * k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

n * n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

n * n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

{n} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() set

x . n is V11() real ext-real Element of REAL

K218(REAL) is non empty functional FinSequence-membered M10( REAL )
dom x is set

Sum k1 is V11() real ext-real Element of REAL

K174(REAL,k1,K625()) is V11() real ext-real Element of REAL

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 <= 0 & b1 divides n & x divides b1 ) } is set

{ (x * b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 <= 0 & b1 divides n div x ) } is set
p is set

x * (e * s) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x * (n div x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p is set

(n div x) * x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(r * s) * x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT

s * (r * x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

x is non empty finite V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT

Seg (max x) is finite max x -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
k1 is set

n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Seg (n + 1) is non empty finite n + 1 -element n + 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Seg n is finite n -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
{(n + 1)} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
() \ {(n + 1)} is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(Seg (n + 1)) \ {(n + 1)} is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
k1 is set

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Seg (n + 1) is non empty finite n + 1 -element n + 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Seg n is finite n -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

(n + 1) |^ k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
x * ((n + 1) |^ k1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

k1 |^ (k1 |-count x) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r is set

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

(k1 |^ (k1 |-count x)) * r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

s is set

() . k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

1 + s1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
k1 |^ (k1 |-count s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

(k1 |^ (k1 |-count s)) * t1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

k1 |^ u is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(k1 |^ u) * k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
((k1 |^ u) * k1) * t1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e * (((k1 |^ u) * k1) * t1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e * k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(k1 |^ u) * t1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(e * k1) * ((k1 |^ u) * t1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(k1 |-count x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
k1 |^ ((k1 |-count x) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(k1 |^ ((k1 |-count x) + 1)) * ((k1 |^ u) * t1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
1 * s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(n + 1) |-count x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT

(n + 1) |^ s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t * ((n + 1) |^ s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
e is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
{k1} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
t is set

k1 |^ s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t |-count (k1 |^ s) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT

(t |-count (k1 |^ s)) + (t |-count s) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
Seg k1 is finite k1 -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT

Seg k is finite k -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Seg (k + 1) is non empty finite k + 1 -element k + 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
p is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
e is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

e |^ (e |-count r) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s is set

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

(e |^ (e |-count r)) * s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

u is set

() . e is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

1 + m is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
e |^ (e |-count s1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

(e |^ (e |-count s1)) * g is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

e |^ u is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(e |^ u) * e is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
((e |^ u) * e) * g is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t * (((e |^ u) * e) * g) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t * e is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(e |^ u) * g is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(t * e) * ((e |^ u) * g) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(e |-count r) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
e |^ ((e |-count r) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(e |^ ((e |-count r) + 1)) * ((e |^ u) * g) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
{e} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
t1 is set
() \/ () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

t1 |-count s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT

t1 |-count (e |^ (e |-count r)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(t1 |-count (e |^ (e |-count r))) + (t1 |-count s1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT

t1 |-count s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

(k + 1) |^ t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s * ((k + 1) |^ t) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

(k + 1) |^ t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s * ((k + 1) |^ t) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

e |-count (e |^ t) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT

(e |-count s) + t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT

e |-count (e |^ t) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT

(e |-count s) + t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT

k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
p is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

support () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes

support is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes