:: INT_7 semantic presentation

REAL is V71() V72() V73() V77() set
NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal V71() V72() V73() V74() V75() V76() V77() Element of bool REAL
bool REAL is non empty set

the carrier of K703() is set
COMPLEX is V71() V77() set
NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal V71() V72() V73() V74() V75() V76() V77() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
RAT is V71() V72() V73() V74() V77() set
INT is V71() V72() V73() V74() V75() V77() set

1 is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
{{},1} is non empty finite V42() V71() V72() V73() V74() V75() V76() set
K340() is set
bool K340() is non empty set
K341() is Element of bool K340()
2 is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
SetPrimes is non empty non trivial non finite V71() V72() V73() V74() V75() V76() Element of bool NAT

bool [:1,1:] is non empty finite V42() set

bool [:[:1,1:],1:] is non empty finite V42() set

bool [:[:1,1:],REAL:] is non empty set

bool is non empty set

bool [:[:2,2:],REAL:] is non empty set
bool is non empty set
K491(2) is V193() L15()
the carrier of K491(2) is set

the carrier of K632() is non empty V71() V72() V73() V74() V75() set

bool is non empty set

In (1,INT) is V11() V12() integer ext-real V52() Element of INT

In (0,INT) is V11() V12() integer ext-real V52() Element of INT
doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #) is strict doubleLoopStr
the carrier of INT.Ring is non empty non trivial non finite V71() V72() V73() V74() V75() set

bool [: the carrier of INT.Ring,NAT:] is non empty non trivial non finite set

bool is non empty non trivial non finite set

bool is non empty set
K228(1,NAT) is M8( NAT )
[:NAT, the carrier of K703():] is Relation-like set
bool [:NAT, the carrier of K703():] is non empty set

bool is non empty set

bool is non empty set

bool is non empty set
bool is non empty set

bool is non empty non trivial non finite set
3 is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

Product () is V11() V12() ext-real Element of REAL
- 1 is V11() V12() integer ext-real non positive set
p is set
a is set

bool [:a,NAT:] is non empty set
ZP is set
(a --> 0) +* (p,ZP) is Relation-like a -defined Function-like total set
f is set
((a --> 0) +* (p,ZP)) . f is set
dom (a --> 0) is Element of bool a
bool a is non empty set
(a --> 0) . f is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(a --> 0) . f is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
p is set

bool [:p,NAT:] is non empty set
a is set
{a} is non empty trivial finite 1 -element set

support ZP is set
ZP . a is set
(p --> 0) +* (a,(ZP . a)) is Relation-like p -defined Function-like total set
dom ZP is Element of bool p
bool p is non empty set
f is set
ZP . f is set
((p --> 0) +* (a,(ZP . a))) . f is set
dom (p --> 0) is Element of bool p
dom ((p --> 0) +* (a,(ZP . a))) is Element of bool p
dom (p --> 0) is Element of bool p
p is set

support a is set

support ZP is set
() /\ (support ZP) is set
() \/ (support ZP) is set

support f is set

g is set
f . g is V11() V12() ext-real set
a . g is V11() V12() ext-real set
ZP . g is V11() V12() ext-real set
(a . g) + (ZP . g) is V11() V12() ext-real set
(f | ()) . g is V11() V12() ext-real set
(a . g) + 0 is V11() V12() ext-real set
(f | (support ZP)) . g is V11() V12() ext-real set
0 + (ZP . g) is V11() V12() ext-real set
0 + (ZP . g) is V11() V12() ext-real set
p is set

support a is set

support ZP is set

dom (a | ()) is Element of bool ()
bool () is non empty set
dom a is Element of bool p
bool p is non empty set
(dom a) /\ () is Element of bool p
dom (ZP | (support ZP)) is Element of bool (support ZP)
bool (support ZP) is non empty set
dom ZP is Element of bool p
(dom ZP) /\ (support ZP) is Element of bool p
f is set
a . f is set
ZP . f is set
(a | ()) . f is set
p is set

support a is finite Element of bool p
bool p is non empty set

support ZP is finite Element of bool p
dom ZP is Element of bool p
(dom ZP) /\ {} is Relation-like finite V71() V72() V73() V74() V75() V76() Element of bool p

dom (ZP | (support ZP)) is finite Element of bool (support ZP)
bool (support ZP) is non empty finite V42() set

dom (a | ()) is finite Element of bool ()
bool () is non empty finite V42() set
dom a is Element of bool p
(dom a) /\ () is finite Element of bool p
f is set
(a | ()) . f is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(ZP | (support ZP)) . f is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

support p is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
bool SetPrimes is non empty non trivial non finite set

support a is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes

() \ () is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
ZP is set
a . ZP is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

bool is non empty non trivial non finite set

f is set
ZP . f is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
a . f is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
f is set
ZP . f is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom ZP is non empty V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
f is set
ZP . f is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
support ZP is set

support f is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
() \/ () is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
() \/ (() \ ()) is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
() \/ () is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes

dom (ZP | (support ZP)) is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
dom ZP is non empty V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
(dom ZP) /\ (support ZP) is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes

g is set
(ZP | (support ZP)) . g is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(a | (support ZP)) . g is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
a . g is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
ZP . g is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom (a | (support ZP)) is Element of bool (support ZP)
bool (support ZP) is non empty set
dom a is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
(dom a) /\ (support ZP) is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
(dom a) /\ (() \ ()) is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
(dom a) /\ () is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
((dom a) /\ ()) \ () is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
g is set
() /\ (support ZP) is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes

support p is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
bool SetPrimes is non empty non trivial non finite set
a is set
() \ a is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes

bool [:a,NAT:] is non empty set

rng (p +* (a --> 0)) is V71() V72() V73() V74() V75() V76() Element of bool RAT
bool RAT is non empty set
rng p is V71() V72() V73() V74() V75() V76() Element of bool RAT
rng (a --> 0) is V71() V72() V73() V74() V75() V76() Element of bool RAT
(rng p) \/ (rng (a --> 0)) is V71() V72() V73() V74() V75() V76() Element of bool RAT
SetPrimes \ a is V71() V72() V73() V74() V75() V76() Element of bool NAT

bool [:(),NAT:] is non empty set

dom (p +* (() --> 0)) is set
dom p is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
dom (() --> 0) is V71() V72() V73() V74() V75() V76() Element of bool ()
bool () is non empty set
(dom p) \/ (dom (() --> 0)) is V71() V72() V73() V74() V75() V76() set
(dom p) \/ () is V71() V72() V73() V74() V75() V76() set
SetPrimes \/ () is non empty V71() V72() V73() V74() V75() V76() Element of bool NAT
rng (p +* (() --> 0)) is V71() V72() V73() V74() V75() V76() Element of bool RAT
rng (() --> 0) is V71() V72() V73() V74() V75() V76() Element of bool RAT
(rng p) \/ (rng (() --> 0)) is V71() V72() V73() V74() V75() V76() Element of bool RAT

bool is non empty non trivial non finite set

y is set
g . y is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(() --> 0) . y is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom (a --> 0) is Element of bool a
bool a is non empty set
dom (p +* (a --> 0)) is set
(dom p) \/ a is set
SetPrimes \/ a is non empty set

support y is set

dom (y | ()) is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
dom y is non empty V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
(dom y) /\ () is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
x is set
g . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
y . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom g is non empty V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
x is set
g . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
p . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
x is set
g . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
p . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
x is set
g . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
support g is set

dom (g | ()) is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
dom g is non empty V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
(dom g) /\ () is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes

x is set
(g | ()) . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(p | ()) . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
p . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
g . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom (p | ()) is Element of bool ()
bool () is non empty set
(dom p) /\ () is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
(dom p) /\ a is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
x is set
y . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(a --> 0) . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
x is set
y . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
p . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

dom (p | ()) is Element of bool ()
bool () is non empty set
(dom p) /\ () is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
(dom p) /\ (() \ a) is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
(dom p) /\ () is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
((dom p) /\ ()) \ a is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
() /\ () is set
gg is set
p . gg is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
y . gg is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
gg is set
(y | ()) . gg is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(p | ()) . gg is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
p . gg is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
y . gg is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
() \/ () is set
() \ () is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
() \/ (() \ ()) is set
() \/ () is set

p is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative set

a is non empty V4() V5() V6() V10() V11() V12() integer prime finite cardinal ext-real positive non negative set
support is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
bool SetPrimes is non empty non trivial non finite set
. a is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
a |-count p is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
a |^ (a |-count p) is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative set

support () is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
p is non empty V4() V5() V6() V10() V11() V12() integer prime finite cardinal ext-real positive non negative set
a is non empty V4() V5() V6() V10() V11() V12() integer prime finite cardinal ext-real positive non negative set
f is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative set
ZP is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative set
a |^ ZP is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative set
f * (a |^ ZP) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative set
p is non empty V4() V5() V6() V10() V11() V12() integer prime finite cardinal ext-real positive non negative set

support a is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
bool SetPrimes is non empty non trivial non finite set
Product a is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
a . p is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
ZP is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative set
p |^ ZP is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative set
rng a is V71() V72() V73() V74() V75() V76() Element of bool RAT
bool RAT is non empty set

rng (canFS ()) is finite V71() V72() V73() V74() V75() V76() Element of bool ()
bool () is non empty finite V42() set
dom (canFS ()) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
f is set
(canFS ()) . f is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

Product g is V11() Element of COMPLEX

bool COMPLEX is non empty set
dom a is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes

dom y is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
((canFS ()) * a) . f is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
rng y is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Product y is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

len p is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Product p is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
a is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

K227(NAT) is non empty functional FinSequence-membered M8( NAT )
[1,a] is set
{1,a} is non empty finite V42() V71() V72() V73() V74() V75() V76() set
{1} is non empty trivial finite V42() 1 -element V71() V72() V73() V74() V75() V76() set
{{1,a},{1}} is non empty finite V42() set

support ZP is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
bool SetPrimes is non empty non trivial non finite set

rng (canFS (support ZP)) is finite V71() V72() V73() V74() V75() V76() Element of bool (support ZP)
bool (support ZP) is non empty finite V42() set
dom ZP is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
dom ((canFS (support ZP)) * ZP) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
dom (canFS (support ZP)) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
dom p is finite V71() V72() V73() V74() V75() V76() Element of bool NAT

(dom ((canFS (support ZP)) * ZP)) /\ (dom p) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT

bool [:NAT,(support ZP):] is non empty set
dom ((canFS (support ZP)) | (dom p)) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
card (support ZP) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
len (canFS (support ZP)) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(len p) + 1 is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Seg ((len p) + 1) is non empty finite (len p) + 1 -element (len p) + 1 -element V71() V72() V73() V74() V75() V76() Element of bool NAT
(len p) + 1 is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= (len p) + 1 ) } is set
len <*a*> is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
len (p ^ <*a*>) is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(p ^ <*a*>) . ((len p) + 1) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(canFS (support ZP)) . ((len p) + 1) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
ZP . ((canFS (support ZP)) . ((len p) + 1)) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
f is non empty V4() V5() V6() V10() V11() V12() integer prime finite cardinal ext-real positive non negative set
{f} is non empty trivial finite V42() 1 -element V71() V72() V73() V74() V75() V76() set
(support ZP) \ {f} is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes

rng g is set
y is set
dom g is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
x is set
g . x is set
x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() Element of SetPrimes
g . x is set
ZP . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
y is set
support g is set
dom g is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
g . y is set
x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() Element of SetPrimes
g . x is set
y is set
x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() Element of SetPrimes
g . x is set
ZP . x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
ZP . f is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative set
f |^ x is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative set
card (dom ((canFS (support ZP)) * ZP)) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
card (dom (canFS (support ZP))) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Seg (len (canFS (support ZP))) is finite len (canFS (support ZP)) -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len (canFS (support ZP)) ) } is set
card (Seg (len (canFS (support ZP)))) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
card (len (canFS (support ZP))) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Seg (len (p ^ <*a*>)) is non empty finite len (p ^ <*a*>) -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len (p ^ <*a*>) ) } is set
card (Seg (len (p ^ <*a*>))) is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
card (len (p ^ <*a*>)) is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
card ((support ZP) \ {f}) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
card {f} is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(card (support ZP)) - () is V11() V12() integer ext-real set
(card (support ZP)) - 1 is V11() V12() integer ext-real set

support y is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes

len (canFS ()) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom (canFS ()) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Seg (len p) is finite len p -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len p ) } is set
gg is non empty V4() V5() V6() V10() V11() V12() integer prime finite cardinal ext-real positive non negative set
ZP . gg is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
n is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative set
gg |^ n is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative set
m0 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative set
y . gg is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
gg |^ m0 is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative set

Seg (len (canFS ())) is finite len (canFS ()) -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len (canFS ()) ) } is set

{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set

len n is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Product n is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
f |^ x is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative set
gg is set
n is set
(canFS (support ZP)) . n is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
m0 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(dom (canFS (support ZP))) /\ (dom p) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
((canFS (support ZP)) | (dom p)) . n is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
rng ((canFS (support ZP)) | (dom p)) is finite V71() V72() V73() V74() V75() V76() Element of bool RAT
bool RAT is non empty set
gg is set
n is set
((canFS (support ZP)) | (dom p)) . n is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(canFS (support ZP)) . n is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
1 + (len p) is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(len p) + 0 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

bool [:(dom p),((support ZP) \ {f}):] is non empty finite V42() set

dom (gg ") is set
dom gg is finite V71() V72() V73() V74() V75() V76() Element of bool (dom p)
bool (dom p) is non empty finite V42() set
rng (gg ") is set

bool [:((support ZP) \ {f}),(dom p):] is non empty finite V42() set
rng (canFS ()) is finite V71() V72() V73() V74() V75() V76() Element of bool ()
bool () is non empty finite V42() set

bool [:(dom p),(dom p):] is non empty finite V42() set

bool [:NAT,(dom p):] is non empty set

rng m0 is finite V71() V72() V73() V74() V75() V76() Element of bool (dom p)

bool [:(dom p),(support ZP):] is non empty finite V42() set

bool [:((support ZP) \ {f}),(support ZP):] is non empty finite V42() set

bool [:(),():] is non empty finite V42() set

bool [:(dom p),():] is non empty finite V42() set

rng u is finite V71() V72() V73() V74() V75() V76() Element of bool (dom p)

dom j is finite V71() V72() V73() V74() V75() V76() Element of bool NAT

dom (u * j) is finite V71() V72() V73() V74() V75() V76() Element of bool (dom p)
dom u is finite V71() V72() V73() V74() V75() V76() Element of bool (dom p)

dom y is V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
dom (j * y) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
rng (u * j) is finite set
rng j is finite set

dom ((u * j) * y) is finite V71() V72() V73() V74() V75() V76() Element of bool (dom p)
rng n0 is finite V71() V72() V73() V74() V75() V76() Element of bool (dom p)

dom (p ^ <*a*>) is non empty finite V71() V72() V73() V74() V75() V76() Element of bool NAT
d1 is set
(u * j) . d1 is set
p . d1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(p ^ <*a*>) . d1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
(canFS (support ZP)) . d1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
ZP . ((canFS (support ZP)) . d1) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
((canFS (support ZP)) | (dom p)) . d1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
ZP . (((canFS (support ZP)) | (dom p)) . d1) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
ZP . ((u * j) . d1) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
y . ((u * j) . d1) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
((u * j) * y) . d1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

rng (j * y) is finite V71() V72() V73() V74() V75() V76() Element of bool RAT

len d1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Product d1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
x is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
f |^ x is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative set

Seg (len d1) is finite len d1 -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len d1 ) } is set
p is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
p + 1 is non empty V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

len a is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Product a is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

Product ZP is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
support ZP is finite V71() V72() V73() V74() V75() V76() Element of bool SetPrimes
bool SetPrimes is non empty non trivial non finite set

f is non empty V4() V5() V6() V10() V11() V12() integer prime finite cardinal ext-real positive non negative set

Seg p is finite p -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= p ) } is set

a . (p + 1) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

len g is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
a /. (len a) is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

K227(NAT) is non empty functional FinSequence-membered M8( NAT )
[1,(a /. (len a))] is set
{1,(a /. (len a))} is non empty finite V42() V71() V72() V73() V74() V75() V76() set
{1} is non empty trivial finite V42() 1 -element V71() V72() V73() V74() V75() V76() set
{{1,(a /. (len a))},{1}} is non empty finite V42() set

y is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT

[1,y] is set
{1,y} is non empty finite V42() V71() V72() V73() V74() V75() V76() set
{{1,y},{1}} is non empty finite V42() set

Product g is V4() V5() V6() V10() V11() V12() integer finite cardinal ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
gg is V4() V5() V6() V10() V11()