:: 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