:: EULER_2 semantic presentation

REAL is non empty V2() non finite set
NAT is non empty V2() V4() V5() V6() non finite cardinal limit_cardinal Element of K6(REAL)
K6(REAL) is V2() non finite set
COMPLEX is non empty V2() non finite set
NAT is non empty V2() V4() V5() V6() non finite cardinal limit_cardinal set
K6(NAT) is V2() non finite set
K6(NAT) is V2() non finite set
RAT is non empty V2() non finite set
INT is non empty V2() non finite set
K7(REAL,REAL) is V2() non finite set
K6(K7(REAL,REAL)) is V2() non finite set

1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT
{{},1} is non empty finite V39() set
K393() is set
K6(K393()) is set
K394() is Element of K6(K393())
K7(COMPLEX,COMPLEX) is V2() non finite set
K6(K7(COMPLEX,COMPLEX)) is V2() non finite set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V2() non finite set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V2() non finite set
K7(K7(REAL,REAL),REAL) is V2() non finite set
K6(K7(K7(REAL,REAL),REAL)) is V2() non finite set
K7(RAT,RAT) is V2() non finite set
K6(K7(RAT,RAT)) is V2() non finite set
K7(K7(RAT,RAT),RAT) is V2() non finite set
K6(K7(K7(RAT,RAT),RAT)) is V2() non finite set
K7(INT,INT) is V2() non finite set
K6(K7(INT,INT)) is V2() non finite set
K7(K7(INT,INT),INT) is V2() non finite set
K6(K7(K7(INT,INT),INT)) is V2() non finite set
K7(NAT,NAT) is V2() non finite set
K7(K7(NAT,NAT),NAT) is V2() non finite set
K6(K7(K7(NAT,NAT),NAT)) is V2() non finite set
2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT
3 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT

K43(1) is V11() V12() ext-real non positive integer Element of REAL

Product () is V11() V12() ext-real Element of REAL
a is V11() V12() ext-real integer set
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
a - 1 is V11() V12() ext-real integer set
1 - 1 is V11() V12() ext-real integer set
a is V11() V12() ext-real integer set
1 gcd a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
abs 1 is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
abs a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(abs 1) gcd (abs a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
1 gcd (abs a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m is V11() V12() ext-real integer set
a * m is V11() V12() ext-real integer set
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
1 - a is V11() V12() ext-real integer set
a - 1 is V11() V12() ext-real integer set
m is V11() V12() ext-real integer set
mm is V11() V12() ext-real integer set
a * mm is V11() V12() ext-real integer set
Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * Y) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT
mm + 1 is V11() V12() ext-real integer set
a * 1 is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * mm) + (a * 1) is V11() V12() ext-real integer set
a * (mm + 1) is V11() V12() ext-real integer set
Y is V11() V12() ext-real integer set
1 - 1 is V11() V12() ext-real integer set
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
a * m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a * m) mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * m) gcd mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
mm * Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(mm * Y) + ((a * m) mod mm) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

- Y is V11() V12() ext-real non positive integer set
(- Y) * mm is V11() V12() ext-real non positive integer set
(a * m) + ((- Y) * mm) is V11() V12() ext-real integer set
((a * m) + ((- Y) * mm)) gcd mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
mm * Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(mm * Y) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a gcd Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a gcd Y) * FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a gcd Y) * X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
mm * ((a gcd Y) * X) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a gcd Y) * FY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(mm * ((a gcd Y) * X)) mod ((a gcd Y) * FY) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
((a gcd Y) * FY) * n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((a gcd Y) * FY) * n) + ((mm * ((a gcd Y) * X)) mod ((a gcd Y) * FY)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
mm * X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
FY * n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(mm * X) - (FY * n) is V11() V12() ext-real integer set
(a gcd Y) * ((mm * X) - (FY * n)) is V11() V12() ext-real integer set
- 1 is V11() V12() ext-real non positive integer set
a gcd m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FY gcd ((mm * X) - (FY * n)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a gcd Y) * (FY gcd ((mm * X) - (FY * n))) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
a mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a mod m) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m * mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(m * mm) + (a mod m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
a + m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a + m) mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
m mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a mod mm) + (m mod mm) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((a mod mm) + (m mod mm)) mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a mod mm) + m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((a mod mm) + m) mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
a * m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a * m) mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
m mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * (m mod mm) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * (m mod mm)) mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
mm * Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(mm * Y) + (m mod mm) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a * Y) * mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
((a * Y) * mm) + (a * (m mod mm)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((a * Y) * mm) + (a * (m mod mm))) mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
a * m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a * m) mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a mod mm) * m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((a mod mm) * m) mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
a * m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a * m) mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
m mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a mod mm) * (m mod mm) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((a mod mm) * (m mod mm)) mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * (m mod mm) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * (m mod mm)) mod mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

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

rng (m * a) is finite V69() V70() V71() Element of K6(REAL)
mm is set
dom (m * a) is finite Element of K6(NAT)
Y is set
(m * a) . Y is V11() V12() ext-real set
FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(m * a) . FX is V11() V12() ext-real set
a . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
m * (a . FX) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

Product a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
mm + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT

len Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Y . (mm + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
rng Y is finite V69() V70() V71() V74() Element of K6(REAL)
rng FX is finite V69() V70() V71() V74() Element of K6(REAL)

FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

{} + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT
dom Y is finite Element of K6(NAT)
dom FX is finite Element of K6(NAT)
X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
FX . X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

len FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
len (FX | n) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
n - 1 is V11() V12() ext-real integer set
max ({},(n - 1)) is V11() V12() ext-real set
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT
Seg a is finite a -element Element of K6(NAT)
Seg n is finite n -element Element of K6(NAT)
(FX | n) . n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

((FX | n) | a) ^ <*FYY*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT

(FX | (Seg n)) | (Seg a) is Relation-like NAT -defined RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() set
(Seg n) /\ (Seg a) is finite Element of K6(NAT)
FX | ((Seg n) /\ (Seg a)) is Relation-like NAT -defined RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() set

b is set
Coim (Y,b) is set
{b} is non empty V2() finite 1 -element set
Y " {b} is finite set
card (Coim (Y,b)) is V4() V5() V6() cardinal set
Coim (FX,b) is set
FX " {b} is finite set
card (Coim (FX,b)) is V4() V5() V6() cardinal set
(Y | mm) " {b} is finite set
card ((Y | mm) " {b}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
<*FYY*> " {b} is finite set
card (<*FYY*> " {b}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(card ((Y | mm) " {b})) + (card (<*FYY*> " {b})) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

((FX | a) ^ <*FYY*>) ^ (FX /^ n) is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(((FX | a) ^ <*FYY*>) ^ (FX /^ n)) " {b} is finite set
card ((((FX | a) ^ <*FYY*>) ^ (FX /^ n)) " {b}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((FX | a) ^ <*FYY*>) " {b} is finite set
card (((FX | a) ^ <*FYY*>) " {b}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FX /^ n) " {b} is finite set
card ((FX /^ n) " {b}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(card (((FX | a) ^ <*FYY*>) " {b})) + (card ((FX /^ n) " {b})) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FX | a) " {b} is finite set
card ((FX | a) " {b}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(card ((FX | a) " {b})) + (card (<*FYY*> " {b})) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((card ((FX | a) " {b})) + (card (<*FYY*> " {b}))) + (card ((FX /^ n) " {b})) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(card ((FX | a) " {b})) + (card ((FX /^ n) " {b})) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((card ((FX | a) " {b})) + (card ((FX /^ n) " {b}))) + (card (<*FYY*> " {b})) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

((FX | a) ^ (FX /^ n)) " {b} is finite set
card (((FX | a) ^ (FX /^ n)) " {b}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(card (((FX | a) ^ (FX /^ n)) " {b})) + (card (<*FYY*> " {b})) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Coim ((Y | mm),b) is set
card (Coim ((Y | mm),b)) is V4() V5() V6() cardinal set
Coim (((FX | a) ^ (FX /^ n)),b) is set
card (Coim (((FX | a) ^ (FX /^ n)),b)) is V4() V5() V6() cardinal set
len (Y | mm) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product (Y | mm) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product ((FX | a) ^ (FX /^ n)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product <*FYY*> is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product ((FX | a) ^ (FX /^ n))) * (Product <*FYY*>) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product (FX | a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product (FX /^ n) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product (FX | a)) * (Product (FX /^ n)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((Product (FX | a)) * (Product (FX /^ n))) * (Product <*FYY*>) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product (FX | a)) * (Product <*FYY*>) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((Product (FX | a)) * (Product <*FYY*>)) * (Product (FX /^ n)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product (FX | n) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product (FX | n)) * (Product (FX /^ n)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
len a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

len mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
len Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

len a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
dom a is finite Element of K6(NAT)
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set

len mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
dom mm is finite Element of K6(NAT)
rng mm is finite set
Y is set
FX is set
mm . FX is set
FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
mm . FYY is set
a . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a . FYY) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

len Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
Y . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a . FX) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
dom Y is finite Element of K6(NAT)

len mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

len Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX is set
FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
mm . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Y . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a . FYY) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len a) is finite len a -element Element of K6(NAT)
dom Y is finite Element of K6(NAT)
dom mm is finite Element of K6(NAT)
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set

Product (m,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product (m,a)) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
() mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
len m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
mm + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT

len Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

Product (Y,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product (Y,a)) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
() mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

len FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
len (Y,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

len ((Y,a) | mm) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
((Y,a) | mm) . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FX,a) . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Y | mm) . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg mm is finite mm -element Element of K6(NAT)

(Y | (Seg mm)) . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal V46() Element of NAT

((Y,a) | (Seg mm)) . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal V46() Element of NAT
(Y,a) . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
dom Y is finite Element of K6(NAT)
dom FX is finite Element of K6(NAT)
FX . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FX . FYY) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Y . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Y . FYY) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
{} + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT
dom Y is finite Element of K6(NAT)
(Y,a) . (mm + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Y . (mm + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Y . (mm + 1)) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
len (FX,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
<*((Y . (mm + 1)) mod a)*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() V63() V64() V65() V66() FinSequence of NAT
(FX,a) ^ <*((Y . (mm + 1)) mod a)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Product (FX,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product (FX,a)) * ((Y . (mm + 1)) mod a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((Product (FX,a)) * ((Y . (mm + 1)) mod a)) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product (FX,a)) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((Y . (mm + 1)) mod a) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((Product (FX,a)) mod a) * (((Y . (mm + 1)) mod a) mod a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((Product (FX,a)) mod a) * (((Y . (mm + 1)) mod a) mod a)) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product FX) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((Product FX) mod a) * (((Y . (mm + 1)) mod a) mod a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((Product FX) mod a) * (((Y . (mm + 1)) mod a) mod a)) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((Product FX) mod a) * ((Y . (mm + 1)) mod a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((Product FX) mod a) * ((Y . (mm + 1)) mod a)) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

FX ^ <*(Y . (mm + 1))*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Product (FX ^ <*(Y . (mm + 1))*>) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product (FX ^ <*(Y . (mm + 1))*>)) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product FX) * (Y . (mm + 1)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((Product FX) * (Y . (mm + 1))) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

len mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

Product (mm,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product (mm,a)) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Product mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product mm) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

len (mm,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
a mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
a * mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a * mm) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
mm mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m * Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(m * Y) + (mm mod m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m * FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(m * FX) + ((a * mm) mod m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a - 1 is V11() V12() ext-real integer set
(a - 1) * mm is V11() V12() ext-real integer set
FX - Y is V11() V12() ext-real integer set
m * (FX - Y) is V11() V12() ext-real integer set
FY is V11() V12() ext-real integer set
FYY is V11() V12() ext-real integer set
X is V11() V12() ext-real integer set
FY * X is V11() V12() ext-real integer set
(FY * X) + 1 is V11() V12() ext-real integer set
FF is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a mod FF is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FF * n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FF * n) mod FF is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((FF * n) mod FF) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT
(((FF * n) mod FF) + 1) mod FF is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
{} + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT
({} + 1) mod FF is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set

dom (m,a) is finite Element of K6(NAT)
len (m,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len (m,a)) is finite len (m,a) -element Element of K6(NAT)
len m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len m) is finite len m -element Element of K6(NAT)
dom m is finite Element of K6(NAT)
mm is set
((m,a),a) . mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(m,a) . mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m,a),a) . Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(m,a) . Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m,a) . Y) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
m . Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(m . Y) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m . Y) mod a) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
dom ((m,a),a) is finite Element of K6(NAT)
len ((m,a),a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len ((m,a),a)) is finite len ((m,a),a) -element Element of K6(NAT)
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set

dom (mm,a) is finite Element of K6(NAT)
len (mm,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len (mm,a)) is finite len (mm,a) -element Element of K6(NAT)
len mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len mm) is finite len mm -element Element of K6(NAT)
dom mm is finite Element of K6(NAT)
dom ((mm,m),a) is finite Element of K6(NAT)
len ((mm,m),a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len ((mm,m),a)) is finite len ((mm,m),a) -element Element of K6(NAT)
len (mm,m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len (mm,m)) is finite len (mm,m) -element Element of K6(NAT)
Y is set
(((mm,m),a),m) . Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((mm,a),m) . Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((mm,m),a),m) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((mm,m),a) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((mm,m),a) . FX) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(mm,m) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * ((mm,m) . FX) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * ((mm,m) . FX)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
mm . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(mm . FX) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * ((mm . FX) mod m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * ((mm . FX) mod m)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * (mm . FX) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * (mm . FX)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(mm,a) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((mm,a) . FX) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((mm,a),m) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
dom ((mm,a),m) is finite Element of K6(NAT)
len ((mm,a),m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len ((mm,a),m)) is finite len ((mm,a),m) -element Element of K6(NAT)
dom (((mm,m),a),m) is finite Element of K6(NAT)
len (((mm,m),a),m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len (((mm,m),a),m)) is finite len (((mm,m),a),m) -element Element of K6(NAT)
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set

dom ((m ^ mm),a) is finite Element of K6(NAT)
len ((m ^ mm),a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len ((m ^ mm),a)) is finite len ((m ^ mm),a) -element Element of K6(NAT)
len (m ^ mm) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len (m ^ mm)) is finite len (m ^ mm) -element Element of K6(NAT)
dom (m ^ mm) is finite Element of K6(NAT)
dom (mm,a) is finite Element of K6(NAT)
len (mm,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len (mm,a)) is finite len (mm,a) -element Element of K6(NAT)
len mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len mm) is finite len mm -element Element of K6(NAT)
dom mm is finite Element of K6(NAT)
dom (m,a) is finite Element of K6(NAT)
len (m,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len (m,a)) is finite len (m,a) -element Element of K6(NAT)
len m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len m) is finite len m -element Element of K6(NAT)
dom m is finite Element of K6(NAT)
Y is set
((m ^ mm),a) . Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m,a) ^ (mm,a)) . Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m ^ mm),a) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(m ^ mm) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m ^ mm) . FX) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
m . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(m . FX) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m,a) ^ (mm,a)) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(m,a) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(len m) + FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(len m) + FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m ^ mm),a) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(m ^ mm) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m ^ mm) . FX) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
mm . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(mm . FYY) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m,a) ^ (mm,a)) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(mm,a) . FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m ^ mm),a) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m,a) ^ (mm,a)) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m ^ mm),a) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((m,a) ^ (mm,a)) . FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
dom ((m,a) ^ (mm,a)) is finite Element of K6(NAT)
len ((m,a) ^ (mm,a)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len ((m,a) ^ (mm,a))) is finite len ((m,a) ^ (mm,a)) -element Element of K6(NAT)
(len (m,a)) + (len (mm,a)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg ((len (m,a)) + (len (mm,a))) is finite (len (m,a)) + (len (mm,a)) -element Element of K6(NAT)
(len m) + (len (mm,a)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg ((len m) + (len (mm,a))) is finite (len m) + (len (mm,a)) -element Element of K6(NAT)
(len m) + (len mm) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg ((len m) + (len mm)) is finite (len m) + (len mm) -element Element of K6(NAT)
a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set

((mm,a),m) ^ ((Y,a),m) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
dom ((mm ^ Y),a) is finite Element of K6(NAT)

len (FX,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len (FX,a)) is finite len (FX,a) -element Element of K6(NAT)
len FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len FX) is finite len FX -element Element of K6(NAT)
dom (mm ^ Y) is finite Element of K6(NAT)
dom (Y,a) is finite Element of K6(NAT)
len (Y,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len (Y,a)) is finite len (Y,a) -element Element of K6(NAT)
len Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len Y) is finite len Y -element Element of K6(NAT)
dom Y is finite Element of K6(NAT)
dom ((Y,a),m) is finite Element of K6(NAT)
len ((Y,a),m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len ((Y,a),m)) is finite len ((Y,a),m) -element Element of K6(NAT)
dom (mm,a) is finite Element of K6(NAT)
len (mm,a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len (mm,a)) is finite len (mm,a) -element Element of K6(NAT)
len mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len mm) is finite len mm -element Element of K6(NAT)
dom mm is finite Element of K6(NAT)
dom ((mm,a),m) is finite Element of K6(NAT)
len ((mm,a),m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len ((mm,a),m)) is finite len ((mm,a),m) -element Element of K6(NAT)
FY is set
(((mm ^ Y),a),m) . FY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((mm,a),m) ^ ((Y,a),m)) . FY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((mm ^ Y),a),m) . X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((mm ^ Y),a) . X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((mm ^ Y),a) . X) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT

FYY . X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT