:: 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
{} is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional integer finite V39() cardinal {} -element FinSequence-membered set
the empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional integer finite V39() cardinal {} -element FinSequence-membered set is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional integer finite V39() cardinal {} -element FinSequence-membered 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
0 is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional integer finite V39() cardinal {} -element FinSequence-membered Element of NAT
K43(1) is V11() V12() ext-real non positive integer Element of REAL
<*> REAL is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Relation-like NAT -defined REAL -valued Function-like one-to-one constant functional integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() V65() V66() FinSequence of REAL
Product (<*> REAL) 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
a * {} is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional integer finite V39() cardinal {} -element FinSequence-membered set
- 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
a is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m * a is Relation-like Function-like set
m * a is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() FinSequence of REAL
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
a is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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
Y is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
FX is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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)
Y | mm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
<*FYY*> 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
(Y | mm) ^ <*FYY*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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
FX /^ n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
FX | n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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 | n) ^ (FX /^ n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(FX | n) | (Seg a) is Relation-like NAT -defined RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() set
FX | (Seg n) is Relation-like NAT -defined RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() set
(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
FX | (Seg a) is Relation-like NAT -defined RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() set
FX | a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
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*> 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) 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) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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
mm is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Y is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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
<*> NAT is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Relation-like NAT -defined NAT -valued Function-like one-to-one constant functional integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() FinSequence of NAT
a is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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
mm is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
Y is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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)
mm is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
len mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Y is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(m,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
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
(Product m) 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
Y is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
len Y is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Y,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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
(Product Y) mod a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Y | mm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
FX is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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
(Y,a) | mm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
len ((Y,a) | mm) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FX,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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) is Relation-like NAT -defined RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() set
(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) is Relation-like NAT -defined RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() set
((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
<*(Y . (mm + 1))*> 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 ^ <*(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
mm is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
len mm is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(mm,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence 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
<*> NAT is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Relation-like NAT -defined NAT -valued Function-like one-to-one constant functional integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() FinSequence 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
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(m,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
((m,a),a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of 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)
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
mm is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(mm,m) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
((mm,m),a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(((mm,m),a),m) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(mm,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
((mm,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,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
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
mm is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
m ^ mm is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
((m ^ mm),a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(m,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(mm,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(m,a) ^ (mm,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
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 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Y is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
mm ^ Y is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
((mm ^ Y),a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(((mm ^ Y),a),m) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(mm,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
((mm,a),m) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Y,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
((Y,a),m) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
((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)
FX is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(FX,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of 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 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
FYY . X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * (FYY . X) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * (FYY . X)) mod m 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 Element of NAT
a * (mm . X) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * (mm . X)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((mm,a),m) ^ ((Y,a),m)) . X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((mm,a),m) . X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(mm,a) . X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((mm,a) . X) mod m 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
n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(len mm) + n 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 mm) + n 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 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
FYY . X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * (FYY . X) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * (FYY . X)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Y . n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * (Y . n) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * (Y . n)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((mm,a),m) ^ ((Y,a),m)) . X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((Y,a),m) . n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Y,a) . n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((Y,a) . n) mod m 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,a),m) ^ ((Y,a),m)) . X 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,a),m) ^ ((Y,a),m)) . X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
dom (((mm ^ Y),a),m) is finite Element of K6(NAT)
((FX,a),m) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
len ((FX,a),m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len ((FX,a),m)) is finite len ((FX,a),m) -element Element of K6(NAT)
dom (((mm,a),m) ^ ((Y,a),m)) is finite Element of K6(NAT)
len (((mm,a),m) ^ ((Y,a),m)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len (((mm,a),m) ^ ((Y,a),m))) is finite len (((mm,a),m) ^ ((Y,a),m)) -element Element of K6(NAT)
(len ((mm,a),m)) + (len ((Y,a),m)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg ((len ((mm,a),m)) + (len ((Y,a),m))) is finite (len ((mm,a),m)) + (len ((Y,a),m)) -element Element of K6(NAT)
(len (mm,a)) + (len ((Y,a),m)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg ((len (mm,a)) + (len ((Y,a),m))) is finite (len (mm,a)) + (len ((Y,a),m)) -element Element of K6(NAT)
(len (mm,a)) + (len (Y,a)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg ((len (mm,a)) + (len (Y,a))) is finite (len (mm,a)) + (len (Y,a)) -element Element of K6(NAT)
(len mm) + (len (Y,a)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg ((len mm) + (len (Y,a))) is finite (len mm) + (len (Y,a)) -element Element of K6(NAT)
(len mm) + (len Y) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg ((len mm) + (len Y)) is finite (len mm) + (len Y) -element Element of K6(NAT)
len (mm ^ Y) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len (mm ^ Y)) is finite len (mm ^ Y) -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 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
mm + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT
a |^ (mm + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
a |^ 1 is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a |^ mm) * (a |^ 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a |^ mm) * a 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
(a |^ {}) gcd m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
1 gcd m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
m gcd 1 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 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
Euler m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a |^ (Euler m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a |^ (Euler m)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT : ( m,b₁ are_relative_prime & 1 <= b₁ & b₁ <= m ) } is set
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT : ex b₂ being V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT st
( b₁ = (a * b₂) mod m & b₂ in { b₁ where b₃ is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT : ( m,b₁ are_relative_prime & 1 <= b₁ & b₁ <= m ) } ) } is set
FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
a * FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a * FX) mod m 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
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
FY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m * FY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(m * FY) + {} is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
FY gcd 1 is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
m * 1 is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(m * FY) gcd (m * 1) 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 Element of NAT
FY is V11() V12() ext-real integer set
FY * a is V11() V12() ext-real integer set
X is V11() V12() ext-real integer set
X * m is V11() V12() ext-real integer set
(FY * a) + (X * m) is V11() V12() ext-real integer set
FYY mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FY mod m is V11() V12() ext-real integer set
FY div m is V11() V12() ext-real integer set
(FY div m) * m is V11() V12() ext-real integer set
FY - ((FY div m) * m) is V11() V12() ext-real integer set
m gcd FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
m * 1 is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FY div m) * a is V11() V12() ext-real integer set
((FY div m) * a) + X is V11() V12() ext-real integer set
m * (((FY div m) * a) + X) is V11() V12() ext-real integer set
(m * 1) gcd (m * (((FY div m) * a) + X)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
1 gcd (((FY div m) * a) + X) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
m * (1 gcd (((FY div m) * a) + X)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FY div m is V11() V12() ext-real integer set
(FY div m) * m is V11() V12() ext-real integer set
((FY div m) * m) + (FY mod m) is V11() V12() ext-real integer set
(FY mod m) * a is V11() V12() ext-real integer set
(FY div m) * a is V11() V12() ext-real integer set
((FY div m) * a) + X is V11() V12() ext-real integer set
(((FY div m) * a) + X) * m is V11() V12() ext-real integer set
((FY mod m) * a) + ((((FY div m) * a) + X) * m) 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
FF mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
n * a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(n * a) mod m 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 Element of NAT
FY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * FY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * FY) 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
a * FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a * FX) mod m 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 * FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a * FYY) mod m 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
a * n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * n) div m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
m * ((a * n) div m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * n) - (m * ((a * n) div m)) 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 * FF is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * FF) div m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
m * ((a * FF) div m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * FF) - (m * ((a * FF) div m)) is V11() V12() ext-real integer set
FF - n is V11() V12() ext-real integer set
a * (FF - n) is V11() V12() ext-real integer set
((a * FF) div m) - ((a * n) div m) is V11() V12() ext-real integer set
m * (((a * FF) div m) - ((a * n) div m)) is V11() V12() ext-real integer set
(a * (FF - n)) - (m * (((a * FF) div m) - ((a * n) div m))) is V11() V12() ext-real integer set
ff is V11() V12() ext-real integer set
1 - ff is V11() V12() ext-real integer set
a is V11() V12() ext-real integer set
ff - 1 is V11() V12() ext-real integer set
Sgm { b₁ where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT : ( m,b₁ are_relative_prime & 1 <= b₁ & b₁ <= m ) } is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
FX is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(FX,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
FYY is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(FYY,m) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Seg m is finite m -element Element of K6(NAT)
X is set
n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
dom FYY is finite Element of K6(NAT)
len FYY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len FYY) is finite len FYY -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 FX is finite Element of K6(NAT)
FY is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
dom FY is finite Element of K6(NAT)
len FY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
Seg (len FY) is finite len FY -element Element of K6(NAT)
rng FY is finite V69() V70() V71() V74() Element of K6(REAL)
n is set
FF is set
FY . FF is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
ff is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX . ff is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
rng FX is finite V69() V70() V71() V74() Element of K6(REAL)
X is finite set
FY . ff is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FYY . ff is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FYY . ff) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * (FX . ff) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * (FX . ff)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
n is set
X is finite set
FF is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
ff is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * ff is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * ff) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
ff is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * ff is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * ff) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
rng FX is finite V69() V70() V71() V74() Element of K6(REAL)
a is set
FX . a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
b is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FY . b is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FYY . b is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FYY . b) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
n is set
dom FY is finite set
FF is set
FY . n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
FY . FF 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
FY . 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 Element of NAT
FX . a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
rng FX is finite V69() V70() V71() V74() Element of K6(REAL)
ff is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX . ff is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FY . ff is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FYY . ff is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FYY . ff) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * (FX . ff) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * (FX . ff)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FY . a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FYY . a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FYY . a) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * (FX . a) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a * (FX . a)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
X is finite set
n is set
Coim (FX,n) is set
{n} is non empty V2() finite 1 -element set
FX " {n} is finite set
card (Coim (FX,n)) is V4() V5() V6() cardinal set
Coim (FY,n) is set
FY " {n} is finite set
card (Coim (FY,n)) is V4() V5() V6() cardinal set
X is finite set
rng FX is finite V69() V70() V71() V74() Element of K6(REAL)
FX - {n} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (FX - {n}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(len FX) - 1 is V11() V12() ext-real integer set
(len (FX - {n})) - (len (FX - {n})) is V11() V12() ext-real integer set
card (FX " {n}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(len FX) - (card (FX " {n})) is V11() V12() ext-real integer set
((len FX) - (card (FX " {n}))) - (len (FX - {n})) is V11() V12() ext-real integer set
FY - {n} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (FY - {n}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
card (FY " {n}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(len FY) - (card (FY " {n})) is V11() V12() ext-real integer set
(len FY) - 1 is V11() V12() ext-real integer set
X is finite set
rng FX is finite V69() V70() V71() V74() Element of K6(REAL)
X is finite set
Product FY is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product FY) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a |^ (len FY) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
Product FX is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a |^ (len FY)) * (Product FX) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((a |^ (len FY)) * (Product FX)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FY | (len FY) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
FY | (Seg (len FY)) is Relation-like NAT -defined RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() set
n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
FY | n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Product (FY | n) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product (FY | n)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
len (FY | n) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a |^ (len (FY | n)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
FX | n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Product (FX | n) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a |^ (len (FY | n))) * (Product (FX | n)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((a |^ (len (FY | n))) * (Product (FX | n))) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
n + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT
FY | (n + 1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Product (FY | (n + 1)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product (FY | (n + 1))) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
len (FY | (n + 1)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a |^ (len (FY | (n + 1))) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
FX | (n + 1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Product (FX | (n + 1)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a |^ (len (FY | (n + 1)))) * (Product (FX | (n + 1))) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((a |^ (len (FY | (n + 1)))) * (Product (FX | (n + 1)))) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
len (FX | (n + 1)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FX | (n + 1)) | n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(FX | (n + 1)) . (n + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
<*((FX | (n + 1)) . (n + 1))*> 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 | (n + 1)) | n) ^ <*((FX | (n + 1)) . (n + 1))*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
{} + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT
(FY | (n + 1)) . (n + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FY . (n + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX . (n + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FY | (n + 1)) | n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
<*((FY | (n + 1)) . (n + 1))*> 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
((FY | (n + 1)) | n) ^ <*((FY | (n + 1)) . (n + 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 (FY | n)) * (FY . (n + 1)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((Product (FY | n)) * (FY . (n + 1))) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FY . (n + 1)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * ((FY . (n + 1)) mod m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * ((FY . (n + 1)) mod m)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FYY . (n + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FYY . (n + 1)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((FYY . (n + 1)) mod m) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * (((FYY . (n + 1)) mod m) mod m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * (((FYY . (n + 1)) mod m) mod m)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(FX,a) . (n + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((FX,a) . (n + 1)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * (((FX,a) . (n + 1)) mod m) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * (((FX,a) . (n + 1)) mod m)) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((a |^ (len (FY | n))) * (Product (FX | n))) * ((FX,a) . (n + 1)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((a |^ (len (FY | n))) * (Product (FX | n))) * ((FX,a) . (n + 1))) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a |^ n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(a |^ n) * (Product (FX | n)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a * (FX . (n + 1)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((a |^ n) * (Product (FX | n))) * (a * (FX . (n + 1))) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((a |^ n) * (Product (FX | n))) * (a * (FX . (n + 1)))) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a |^ n) * a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
(Product (FX | n)) * (FX . (n + 1)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((a |^ n) * a) * ((Product (FX | n)) * (FX . (n + 1))) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(((a |^ n) * a) * ((Product (FX | n)) * (FX . (n + 1)))) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a |^ (len (FY | (n + 1)))) * ((Product (FX | n)) * (FX . (n + 1))) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((a |^ (len (FY | (n + 1)))) * ((Product (FX | n)) * (FX . (n + 1)))) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX | (len FX) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
FX | (Seg (len FX)) is Relation-like NAT -defined RAT -valued Function-like finite FinSubsequence-like V59() V60() V61() V62() set
FX | (len FY) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
FY | {} is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Relation-like NAT -defined NAT -valued RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() FinSequence of NAT
Product (FY | {}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product (FY | {})) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
len (FY | {}) is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional integer finite V39() cardinal {} -element FinSequence-membered Element of NAT
a |^ (len (FY | {})) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
FX | {} is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Relation-like NAT -defined NAT -valued RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() FinSequence of NAT
Product (FX | {}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(a |^ (len (FY | {}))) * (Product (FX | {})) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
((a |^ (len (FY | {}))) * (Product (FX | {}))) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX | (len FX) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
n is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
FX | n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Product (FX | n) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
n + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT
FX | (n + 1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Product (FX | (n + 1)) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FF is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
FF . (n + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
len FF is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FF | n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
ff is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
<*ff*> 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
(FF | n) ^ <*ff*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
Product (FF | n) 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
(FX | (n + 1)) . (n + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX . (n + 1) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
rng FX is finite V69() V70() V71() V74() Element of K6(REAL)
X is finite set
a is V11() V12() ext-real integer set
m9 is V11() V12() ext-real integer set
b is V11() V12() ext-real integer set
a * b is V11() V12() ext-real integer set
c₁₅ is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
FX | {} is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Relation-like NAT -defined NAT -valued RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() FinSequence of NAT
Product (FX | {}) is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product (FX | {})) gcd m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
X is finite set
card X is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
(Product FX) 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
(a |^ m) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
a mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
m - 1 is V11() V12() ext-real integer set
1 - 1 is V11() V12() ext-real integer set
Euler 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 Element of NAT
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
((a |^ mm) mod m) * a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
1 * a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT
mm + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative integer finite cardinal Element of NAT
(a |^ mm) * a is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal set
((a |^ mm) * a) mod m is V4() V5() V6() V10() V11() V12() ext-real non negative integer finite cardinal Element of NAT