:: WSIERP_1 semantic presentation

REAL is non empty V36() V73() V74() V75() V79() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V36() V41() V42() V73() V74() V75() V76() V77() V78() V79() Element of K6(REAL)
K6(REAL) is non empty V36() set
INT is non empty V36() V73() V74() V75() V76() V77() V79() set
COMPLEX is non empty V36() V73() V79() set
RAT is non empty V36() V73() V74() V75() V76() V79() set
K7(COMPLEX,COMPLEX) is non empty Relation-like V36() V63() set
K6(K7(COMPLEX,COMPLEX)) is non empty V36() set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty Relation-like V36() V63() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty V36() set
K7(REAL,REAL) is non empty Relation-like V36() V63() V64() V65() set
K6(K7(REAL,REAL)) is non empty V36() set
K7(K7(REAL,REAL),REAL) is non empty Relation-like V36() V63() V64() V65() set
K6(K7(K7(REAL,REAL),REAL)) is non empty V36() set
K7(RAT,RAT) is non empty Relation-like RAT -valued V36() V63() V64() V65() set
K6(K7(RAT,RAT)) is non empty V36() set
K7(K7(RAT,RAT),RAT) is non empty Relation-like RAT -valued V36() V63() V64() V65() set
K6(K7(K7(RAT,RAT),RAT)) is non empty V36() set
K7(INT,INT) is non empty Relation-like RAT -valued INT -valued V36() V63() V64() V65() set
K6(K7(INT,INT)) is non empty V36() set
K7(K7(INT,INT),INT) is non empty Relation-like RAT -valued INT -valued V36() V63() V64() V65() set
K6(K7(K7(INT,INT),INT)) is non empty V36() set
K7(NAT,NAT) is non empty Relation-like RAT -valued INT -valued V36() V63() V64() V65() V66() set
K7(K7(NAT,NAT),NAT) is non empty Relation-like RAT -valued INT -valued V36() V63() V64() V65() V66() set
K6(K7(K7(NAT,NAT),NAT)) is non empty V36() set
omega is non empty epsilon-transitive epsilon-connected ordinal V36() V41() V42() V73() V74() V75() V76() V77() V78() V79() set
K6(omega) is non empty V36() set
K6(NAT) is non empty V36() set
K297(NAT) is V62() set
K7(NAT,REAL) is non empty Relation-like V36() V63() V64() V65() set
K6(K7(NAT,REAL)) is non empty V36() set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
{{},1} is non empty V73() V74() V75() V76() V77() V78() set
K473() is set
K6(K473()) is non empty set
K474() is Element of K6(K473())
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() Element of NAT
- 1 is V11() real ext-real non positive integer rational set
sqrt 0 is V11() real ext-real Element of REAL
sqrt 1 is V11() real ext-real Element of REAL
Seg 1 is non empty V2() V36() V43(1) V73() V74() V75() V76() V77() V78() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty V2() V43(1) V73() V74() V75() V76() V77() V78() set
Seg 2 is non empty V36() V43(2) V73() V74() V75() V76() V77() V78() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is non empty V73() V74() V75() V76() V77() V78() set
<*> REAL is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V69() V70() V73() V74() V75() V76() V77() V78() V79() FinSequence of REAL
Sum (<*> REAL) is V11() real ext-real Element of REAL
K203() is Relation-like Function-like V30(K7(REAL,REAL), REAL ) V63() V64() V65() Element of K6(K7(K7(REAL,REAL),REAL))
K298(REAL,(<*> REAL),K203()) is V11() real ext-real Element of REAL
Product (<*> REAL) is V11() real ext-real Element of REAL
K205() is Relation-like Function-like V30(K7(REAL,REAL), REAL ) V63() V64() V65() Element of K6(K7(K7(REAL,REAL),REAL))
K298(REAL,(<*> REAL),K205()) is V11() real ext-real Element of REAL
len {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() set
k is V11() real ext-real set
k |^ 2 is V11() real ext-real set
k * k is V11() real ext-real set
- k is V11() real ext-real set
(- k) |^ 2 is V11() real ext-real set
(- k) |^ 1 is V11() real ext-real set
k |^ 1 is V11() real ext-real set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k |^ (1 + 1) is V11() real ext-real set
(- k) * (- k) is V11() real ext-real set
(- k) |^ (1 + 1) is V11() real ext-real set
k is V11() real ext-real set
- k is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
2 * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(- k) |^ (2 * n) is V11() real ext-real set
k |^ (2 * n) is V11() real ext-real set
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(- k) |^ ((2 * n) + 1) is V11() real ext-real set
k |^ ((2 * n) + 1) is V11() real ext-real set
- (k |^ ((2 * n) + 1)) is V11() real ext-real set
(- k) |^ 2 is V11() real ext-real set
((- k) |^ 2) |^ n is V11() real ext-real set
k |^ 2 is V11() real ext-real set
(k |^ 2) |^ n is V11() real ext-real set
((- k) |^ (2 * n)) * (- k) is V11() real ext-real set
(k |^ (2 * n)) * k is V11() real ext-real set
- ((k |^ (2 * n)) * k) is V11() real ext-real set
k is V11() real ext-real set
n is V11() real ext-real set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k |^ d is V11() real ext-real set
n |^ d is V11() real ext-real set
d -Root (k |^ d) is V11() real ext-real set
k is V11() real ext-real set
n is V11() real ext-real set
k + n is V11() real ext-real set
n - k is V11() real ext-real set
0 + n is V11() real ext-real set
k is V11() real ext-real set
n is V11() real ext-real set
k + n is V11() real ext-real set
d is V11() real ext-real set
d - k is V11() real ext-real set
d + 0 is V11() real ext-real set
k is V11() real ext-real set
n is V11() real ext-real set
k + n is V11() real ext-real set
d is V11() real ext-real set
d - k is V11() real ext-real set
d + 0 is V11() real ext-real set
k is V11() real ext-real integer rational set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k |^ n is V11() real ext-real set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k |^ d is V11() real ext-real set
d + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k |^ (d + 1) is V11() real ext-real set
d1 is V11() real ext-real integer rational set
k * d1 is V11() real ext-real integer rational set
k |^ 0 is V11() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k div 2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
2 * (k div 2) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(2 * (k div 2)) + (k mod 2) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(2 * (k div 2)) + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(2 * (k div 2)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
n + d is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
k * d1 is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
k * d is V11() real ext-real integer rational set
d1 + d is V11() real ext-real integer rational set
k * (d1 + d) is V11() real ext-real integer rational set
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
n * d1 is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
d * d is V11() real ext-real integer rational set
(n * d1) + (d * d) is V11() real ext-real integer rational set
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
k gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is V11() real ext-real integer rational set
d gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k * d is V11() real ext-real integer rational set
(k * d) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k * d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(k * d) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is V11() real ext-real integer rational set
0 gcd k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
abs k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
1 gcd k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k gcd 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
abs 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(abs k) gcd (abs 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(abs k) gcd 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k gcd 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
abs 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(abs k) gcd (abs 0) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(abs k) gcd 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is V11() real ext-real integer rational set
1 gcd k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is V11() real ext-real integer rational set
n |^ k is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n |^ d1 is V11() real ext-real integer rational set
d1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n |^ (d1 + 1) is V11() real ext-real integer rational set
n * (n |^ d1) is V11() real ext-real integer rational set
n |^ 0 is V11() real ext-real integer rational set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is V11() real ext-real integer rational set
d |^ k is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
d1 |^ n is V11() real ext-real integer rational set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is V11() real ext-real integer rational set
d |^ n is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
d gcd d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 |^ k is V11() real ext-real integer rational set
d gcd (d1 |^ k) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(d |^ n) gcd (d1 |^ k) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is V11() real ext-real integer rational set
abs k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
k * d is V11() real ext-real integer rational set
(abs k) * d is V11() real ext-real integer rational set
- d is V11() real ext-real integer rational set
(abs k) * (- d) is V11() real ext-real integer rational set
- k is V11() real ext-real integer rational set
(- k) * (- d) is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
(abs k) * d is V11() real ext-real integer rational set
k * d is V11() real ext-real integer rational set
- k is V11() real ext-real integer rational set
(- k) * d is V11() real ext-real integer rational set
- d is V11() real ext-real integer rational set
k * (- d) is V11() real ext-real integer rational set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k |^ d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n |^ d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k * d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 |^ d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(k |^ d) * (d1 |^ d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n gcd d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k gcd d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n / k is V11() real ext-real non negative rational set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k * d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k * d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k * d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
n / k is V11() real ext-real rational set
d is V11() real ext-real integer rational set
k * d is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
k * d is V11() real ext-real integer rational set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is V11() real ext-real integer rational set
n * d is V11() real ext-real integer rational set
k / n is V11() real ext-real non negative rational set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n - d is V11() real ext-real integer rational set
k + d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
n - 1 is V11() real ext-real integer rational Element of REAL
k + 1 is V11() real ext-real integer rational Element of REAL
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
n + 1 is V11() real ext-real integer rational Element of REAL
k - 1 is V11() real ext-real integer rational Element of REAL
k is non empty set
K6(k) is non empty set
n is non empty Element of K6(k)
d is Relation-like NAT -defined k -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n
d1 is Relation-like NAT -defined k -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n
d ^ d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d ^ d1 is Relation-like NAT -defined n -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n
rng (d ^ d1) is set
k is Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
Product k is V11() set
d is V11() real ext-real integer rational Element of INT
n is Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
Product n is V11() set
<*d*> is non empty V2() Relation-like NAT -defined INT -valued Function-like one-to-one constant V36() V43(1) FinSequence-like FinSubsequence-like V63() V64() V65() V67() V68() V69() V70() FinSequence of INT
[1,d] is set
{1,d} is non empty V73() V74() V75() V76() V77() set
{{1,d},{1}} is non empty set
{[1,d]} is non empty V2() Relation-like Function-like constant V43(1) set
n ^ <*d*> is non empty Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
Product (n ^ <*d*>) is V11() set
d is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
d * d1 is V11() real ext-real integer rational set
<*> INT is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined INT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() FinSequence of INT
K7(NAT,INT) is non empty Relation-like INT -valued RAT -valued V36() V63() V64() V65() set
Product (<*> INT) is V11() set
k is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
Sum k is V11() set
K298(REAL,k,K203()) is V11() real ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
Sum n is V11() real ext-real Element of REAL
K298(REAL,n,K203()) is V11() real ext-real Element of REAL
d is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
Sum d is V11() real ext-real Element of REAL
K298(REAL,d,K203()) is V11() real ext-real Element of REAL
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
<*d*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V36() V43(1) FinSequence-like FinSubsequence-like V63() V64() V65() V66() V67() V68() V69() V70() FinSequence of NAT
[1,d] is set
{1,d} is non empty V73() V74() V75() V76() V77() V78() set
{{1,d},{1}} is non empty set
{[1,d]} is non empty V2() Relation-like Function-like constant V43(1) set
(REAL,NAT,n,<*d*>) is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
Sum (REAL,NAT,n,<*d*>) is V11() real ext-real Element of REAL
K298(REAL,(REAL,NAT,n,<*d*>),K203()) is V11() real ext-real Element of REAL
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 + d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
<*> NAT is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() FinSequence of NAT
n is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
Sum n is V11() real ext-real Element of REAL
K298(REAL,n,K203()) is V11() real ext-real Element of REAL
k is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
Product k is V11() set
K298(REAL,k,K205()) is V11() real ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
Product n is V11() real ext-real Element of REAL
K298(REAL,n,K205()) is V11() real ext-real Element of REAL
d is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
Product d is V11() real ext-real Element of REAL
K298(REAL,d,K205()) is V11() real ext-real Element of REAL
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
<*d*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V36() V43(1) FinSequence-like FinSubsequence-like V63() V64() V65() V66() V67() V68() V69() V70() FinSequence of NAT
[1,d] is set
{1,d} is non empty V73() V74() V75() V76() V77() V78() set
{{1,d},{1}} is non empty set
{[1,d]} is non empty V2() Relation-like Function-like constant V43(1) set
(REAL,NAT,n,<*d*>) is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
Product (REAL,NAT,n,<*d*>) is V11() real ext-real Element of REAL
K298(REAL,(REAL,NAT,n,<*d*>),K205()) is V11() real ext-real Element of REAL
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 * d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
<*> NAT is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() FinSequence of NAT
n is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
Product n is V11() real ext-real Element of REAL
K298(REAL,n,K205()) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k - 1 is V11() real ext-real integer rational Element of REAL
n is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
dom n is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
n . k is set
<*(n . k)*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,(n . k)] is set
{1,(n . k)} is non empty set
{{1,(n . k)},{1}} is non empty set
{[1,(n . k)]} is non empty V2() Relation-like Function-like constant V43(1) set
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len n) - k is V11() real ext-real integer rational Element of REAL
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k + d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d ^ d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
e1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
e1 is set
<*e1*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,e1] is set
{1,e1} is non empty set
{{1,e1},{1}} is non empty set
{[1,e1]} is non empty V2() Relation-like Function-like constant V43(1) set
e1 ^ <*e1*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len e1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
dom d is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
d . k is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
dom n is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
Del (n,k) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len d) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d . d1 is set
n . d1 is set
d1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n . (d1 + 1) is set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
dom d is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
d1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n . (d1 + 1) is set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d . d1 is set
(Del (n,k)) . d1 is set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d . d is set
n . d is set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d . d is set
d + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n . (d + 1) is set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len (Del (n,k)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k - 1 is V11() real ext-real integer rational Element of REAL
n is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
dom n is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
Del (n,k) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d ^ d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d is set
<*d*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,d] is set
{1,d} is non empty set
{{1,d},{1}} is non empty set
{[1,d]} is non empty V2() Relation-like Function-like constant V43(1) set
d ^ <*d*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(d ^ <*d*>) ^ d1 is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len (Del (n,k)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len (Del (n,k))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len (d ^ <*d*>) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len (d ^ <*d*>)) + (len d1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len d) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
((len d) + 1) + (len d1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k + (len d1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len d1) + (len d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len (d ^ d1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len <*d*> is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
<*d*> ^ d1 is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d ^ (<*d*> ^ d1) is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len (<*d*> ^ d1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(k - 1) + (len (<*d*> ^ d1)) is V11() real ext-real integer rational Element of REAL
(len n) - (k - 1) is V11() real ext-real integer rational Element of REAL
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
dom d is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
(d ^ d1) . d1 is set
d . d1 is set
n . d1 is set
(Del (n,k)) . d1 is set
d1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(d1 + 1) - k is V11() real ext-real integer rational Element of REAL
((d1 + 1) - k) + 1 is V11() real ext-real integer rational Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(d1 + 1) - (k - 1) is V11() real ext-real integer rational Element of REAL
(d ^ d1) . d1 is set
d1 - (len d) is V11() real ext-real integer rational Element of REAL
d1 . (d1 - (len d)) is set
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
e1 - 1 is V11() real ext-real integer rational Element of REAL
d1 . (e1 - 1) is set
(<*d*> ^ d1) . e1 is set
(d ^ (<*d*> ^ d1)) . (d1 + 1) is set
(Del (n,k)) . d1 is set
(d ^ d1) . d1 is set
(Del (n,k)) . d1 is set
(d ^ d1) . d1 is set
(Del (n,k)) . d1 is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
Del (n,k) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
dom (Del (n,k)) is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
dom n is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
Seg (len n) is V36() V43( len n) V73() V74() V75() V76() V77() V78() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
len (Del (n,k)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len (Del (n,k))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
Seg ((len (Del (n,k))) + 1) is non empty V36() V43((len (Del (n,k))) + 1) V73() V74() V75() V76() V77() V78() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT : ( 1 <= b₁ & b₁ <= (len (Del (n,k))) + 1 ) } is set
Seg (len (Del (n,k))) is V36() V43( len (Del (n,k))) V73() V74() V75() V76() V77() V78() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT : ( 1 <= b₁ & b₁ <= len (Del (n,k)) ) } is set
{((len (Del (n,k))) + 1)} is non empty V2() V43(1) V73() V74() V75() V76() V77() V78() set
(Seg (len (Del (n,k)))) \/ {((len (Del (n,k))) + 1)} is non empty V73() V74() V75() V76() V77() V78() set
(dom (Del (n,k))) \/ {((len (Del (n,k))) + 1)} is non empty V73() V74() V75() V76() V77() V78() set
k is non empty set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is Relation-like NAT -defined k -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of k
Del (d,n) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
rng d is set
rng (Del (d,n)) is set
k is non empty set
K6(k) is non empty set
n is non empty Element of K6(k)
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 is Relation-like NAT -defined k -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n
Del (d1,d) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(n,d,d1) is Relation-like NAT -defined n -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of n
rng (n,d,d1) is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
Del (n,k) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(len n) + k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
n ^ d is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
Del ((n ^ d),k) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(Del (n,k)) ^ d is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
Del ((n ^ d),((len n) + k)) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
Del (d,k) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
n ^ (Del (d,k)) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len (n ^ d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len n) + (len d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
dom d is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
dom (n ^ d) is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
dom d is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
k - 1 is V11() real ext-real integer rational Element of REAL
(len n) + (k - 1) is V11() real ext-real integer rational Element of REAL
dom (n ^ d) is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
(n ^ d) . ((len n) + k) is set
<*((n ^ d) . ((len n) + k))*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,((n ^ d) . ((len n) + k))] is set
{1,((n ^ d) . ((len n) + k))} is non empty set
{{1,((n ^ d) . ((len n) + k))},{1}} is non empty set
{[1,((n ^ d) . ((len n) + k))]} is non empty V2() Relation-like Function-like constant V43(1) set
((len n) + k) - 1 is V11() real ext-real integer rational Element of REAL
(len (n ^ d)) - ((len n) + k) is V11() real ext-real integer rational Element of REAL
e1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
e1 ^ <*((n ^ d) . ((len n) + k))*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
e1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(e1 ^ <*((n ^ d) . ((len n) + k))*>) ^ e1 is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
e1 ^ e1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
<*((n ^ d) . ((len n) + k))*> ^ e1 is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
e1 ^ (<*((n ^ d) . ((len n) + k))*> ^ e1) is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
fs is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
n ^ fs is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
fs ^ <*((n ^ d) . ((len n) + k))*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(fs ^ <*((n ^ d) . ((len n) + k))*>) ^ e1 is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
n ^ ((fs ^ <*((n ^ d) . ((len n) + k))*>) ^ e1) is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
n ^ (fs ^ <*((n ^ d) . ((len n) + k))*>) is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(n ^ (fs ^ <*((n ^ d) . ((len n) + k))*>)) ^ e1 is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len fs is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len n) + (len fs) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
fs ^ e1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(n ^ d) . k is set
<*((n ^ d) . k)*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,((n ^ d) . k)] is set
{1,((n ^ d) . k)} is non empty set
{{1,((n ^ d) . k)},{1}} is non empty set
{[1,((n ^ d) . k)]} is non empty V2() Relation-like Function-like constant V43(1) set
dom n is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
dom (n ^ d) is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
dom (n ^ d) is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
k - 1 is V11() real ext-real integer rational Element of REAL
(len (n ^ d)) - k is V11() real ext-real integer rational Element of REAL
e1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
e1 ^ <*((n ^ d) . k)*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
fs is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(e1 ^ <*((n ^ d) . k)*>) ^ fs is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len fs is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len (e1 ^ <*((n ^ d) . k)*>) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(k - 1) + 1 is V11() real ext-real integer rational Element of REAL
v1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(e1 ^ <*((n ^ d) . k)*>) ^ v1 is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
v1 ^ d is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(e1 ^ <*((n ^ d) . k)*>) ^ (v1 ^ d) is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
dom n is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
e1 ^ v1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
e1 ^ fs is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len k) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n is set
<*n*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty V2() Relation-like Function-like constant V43(1) set
<*n*> ^ k is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
Del ((<*n*> ^ k),1) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
k ^ <*n*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
Del ((k ^ <*n*>),((len k) + 1)) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len <*n*> is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
dom <*n*> is non empty V2() V43(1) V73() V74() V75() V76() V77() V78() Element of K6(NAT)
Del (<*n*>,1) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len (Del (<*n*>,1)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len (Del (<*n*>,1))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
{} ^ k is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
k ^ {} is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
k is set
<*k*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,k] is set
{1,k} is non empty set
{{1,k},{1}} is non empty set
{[1,k]} is non empty V2() Relation-like Function-like constant V43(1) set
Del (<*k*>,1) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
n is set
<*k,n*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like set
<*n*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty V2() Relation-like Function-like constant V43(1) set
<*k*> ^ <*n*> is non empty Relation-like NAT -defined Function-like V36() V43(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
Del (<*k,n*>,1) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
Del (<*k,n*>,2) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d is set
<*k,n,d*> is non empty Relation-like NAT -defined Function-like V36() V43(3) FinSequence-like FinSubsequence-like set
<*d*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,d] is set
{1,d} is non empty set
{{1,d},{1}} is non empty set
{[1,d]} is non empty V2() Relation-like Function-like constant V43(1) set
(<*k*> ^ <*n*>) ^ <*d*> is non empty Relation-like NAT -defined Function-like V36() V43((1 + 1) + 1) FinSequence-like FinSubsequence-like set
(1 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
Del (<*k,n,d*>,1) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
<*n,d*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like set
<*n*> ^ <*d*> is non empty Relation-like NAT -defined Function-like V36() V43(1 + 1) FinSequence-like FinSubsequence-like set
Del (<*k,n,d*>,2) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
<*k,d*> is non empty Relation-like NAT -defined Function-like V36() V43(2) FinSequence-like FinSubsequence-like set
<*k*> ^ <*d*> is non empty Relation-like NAT -defined Function-like V36() V43(1 + 1) FinSequence-like FinSubsequence-like set
Del (<*k,n,d*>,3) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
<*k*> ^ {} is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
Del ((<*k*> ^ {}),1) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len <*k*> is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len <*k*>) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
Del ((<*k*> ^ <*n*>),((len <*k*>) + 1)) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
<*k*> ^ <*n,d*> is non empty Relation-like NAT -defined Function-like V36() V43(1 + 2) FinSequence-like FinSubsequence-like set
1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
Del ((<*k*> ^ <*n,d*>),1) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len <*k,n*> is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len <*k,n*>) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k . 1 is set
<*(k . 1)*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,(k . 1)] is set
{1,(k . 1)} is non empty set
{{1,(k . 1)},{1}} is non empty set
{[1,(k . 1)]} is non empty V2() Relation-like Function-like constant V43(1) set
Del (k,1) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
<*(k . 1)*> ^ (Del (k,1)) is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
Del (k,(len k)) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
k . (len k) is set
<*(k . (len k))*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,(k . (len k))] is set
{1,(k . (len k))} is non empty set
{{1,(k . (len k))},{1}} is non empty set
{[1,(k . (len k))]} is non empty V2() Relation-like Function-like constant V43(1) set
(Del (k,(len k))) ^ <*(k . (len k))*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len <*(k . 1)*> is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
dom k is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
len (Del (k,1)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len <*(k . 1)*>) + (len (Del (k,1))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len (<*(k . 1)*> ^ (Del (k,1))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k . d1 is set
(<*(k . 1)*> ^ (Del (k,1))) . d1 is set
dom <*(k . 1)*> is non empty V2() V43(1) V73() V74() V75() V76() V77() V78() Element of K6(NAT)
<*(k . 1)*> . 1 is set
d1 - 1 is V11() real ext-real integer rational Element of REAL
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(Del (k,1)) . d is set
d + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k . (d + 1) is set
len <*(k . (len k))*> is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len (Del (k,(len k))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len <*(k . (len k))*>) + (len (Del (k,(len k)))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len ((Del (k,(len k))) ^ <*(k . (len k))*>) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len (Del (k,(len k)))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len k) - 1 is V11() real ext-real integer rational Element of REAL
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k . d1 is set
((Del (k,(len k))) ^ <*(k . (len k))*>) . d1 is set
d1 - 1 is V11() real ext-real integer rational Element of REAL
d1 - (d1 - 1) is V11() real ext-real integer rational Element of REAL
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
<*(k . (len k))*> . d is set
d1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
dom (Del (k,(len k))) is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
(Del (k,(len k))) . d1 is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
dom n is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
(REAL,k,n) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Product (REAL,k,n) is V11() real ext-real Element of REAL
K298(REAL,(REAL,k,n),K205()) is V11() real ext-real Element of REAL
n . k is V11() real ext-real Element of REAL
(Product (REAL,k,n)) * (n . k) is V11() real ext-real Element of REAL
Product n is V11() real ext-real Element of REAL
K298(REAL,n,K205()) is V11() real ext-real Element of REAL
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n . d is V11() real ext-real Element of REAL
(REAL,d,n) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Product (REAL,d,n) is V11() real ext-real Element of REAL
K298(REAL,(REAL,d,n),K205()) is V11() real ext-real Element of REAL
(n . d) * (Product (REAL,d,n)) is V11() real ext-real Element of REAL
d + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n . (d + 1) is V11() real ext-real Element of REAL
(REAL,(d + 1),n) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Product (REAL,(d + 1),n) is V11() real ext-real Element of REAL
K298(REAL,(REAL,(d + 1),n),K205()) is V11() real ext-real Element of REAL
(n . (d + 1)) * (Product (REAL,(d + 1),n)) is V11() real ext-real Element of REAL
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n . 1 is V11() real ext-real Element of REAL
<*(n . 1)*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() V43(1) FinSequence-like FinSubsequence-like V63() V64() V65() V67() V68() V69() V70() FinSequence of REAL
[1,(n . 1)] is set
{1,(n . 1)} is non empty V73() V74() V75() set
{{1,(n . 1)},{1}} is non empty set
{[1,(n . 1)]} is non empty V2() Relation-like Function-like constant V43(1) set
(REAL,1,n) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
<*(n . 1)*> ^ (REAL,1,n) is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Product <*(n . 1)*> is V11() real ext-real Element of REAL
K298(REAL,<*(n . 1)*>,K205()) is V11() real ext-real Element of REAL
Product (REAL,1,n) is V11() real ext-real Element of REAL
K298(REAL,(REAL,1,n),K205()) is V11() real ext-real Element of REAL
(Product <*(n . 1)*>) * (Product (REAL,1,n)) is V11() real ext-real Element of REAL
(n . 1) * (Product (REAL,1,n)) is V11() real ext-real Element of REAL
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
<*(n . (d + 1))*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() V43(1) FinSequence-like FinSubsequence-like V63() V64() V65() V67() V68() V69() V70() FinSequence of REAL
[1,(n . (d + 1))] is set
{1,(n . (d + 1))} is non empty V73() V74() V75() set
{{1,(n . (d + 1))},{1}} is non empty set
{[1,(n . (d + 1))]} is non empty V2() Relation-like Function-like constant V43(1) set
(d + 1) - 1 is V11() real ext-real integer rational Element of REAL
(len n) - (d + 1) is V11() real ext-real integer rational Element of REAL
d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d1 ^ <*(n . (d + 1))*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(d1 ^ <*(n . (d + 1))*>) ^ d is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 ^ d is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
e1 is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
e1 ^ <*(n . (d + 1))*> is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Product (e1 ^ <*(n . (d + 1))*>) is V11() real ext-real Element of REAL
K298(REAL,(e1 ^ <*(n . (d + 1))*>),K205()) is V11() real ext-real Element of REAL
d1 is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Product d1 is V11() real ext-real Element of REAL
K298(REAL,d1,K205()) is V11() real ext-real Element of REAL
(Product (e1 ^ <*(n . (d + 1))*>)) * (Product d1) is V11() real ext-real Element of REAL
Product e1 is V11() real ext-real Element of REAL
K298(REAL,e1,K205()) is V11() real ext-real Element of REAL
Product <*(n . (d + 1))*> is V11() real ext-real Element of REAL
K298(REAL,<*(n . (d + 1))*>,K205()) is V11() real ext-real Element of REAL
(Product e1) * (Product <*(n . (d + 1))*>) is V11() real ext-real Element of REAL
((Product e1) * (Product <*(n . (d + 1))*>)) * (Product d1) is V11() real ext-real Element of REAL
(n . (d + 1)) * (Product e1) is V11() real ext-real Element of REAL
((n . (d + 1)) * (Product e1)) * (Product d1) is V11() real ext-real Element of REAL
(Product e1) * (Product d1) is V11() real ext-real Element of REAL
(n . (d + 1)) * ((Product e1) * (Product d1)) is V11() real ext-real Element of REAL
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n . 0 is V11() real ext-real Element of REAL
(REAL,0,n) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Product (REAL,0,n) is V11() real ext-real Element of REAL
K298(REAL,(REAL,0,n),K205()) is V11() real ext-real Element of REAL
(n . 0) * (Product (REAL,0,n)) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
dom n is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
(REAL,k,n) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Sum (REAL,k,n) is V11() real ext-real Element of REAL
K298(REAL,(REAL,k,n),K203()) is V11() real ext-real Element of REAL
n . k is V11() real ext-real Element of REAL
(Sum (REAL,k,n)) + (n . k) is V11() real ext-real Element of REAL
Sum n is V11() real ext-real Element of REAL
K298(REAL,n,K203()) is V11() real ext-real Element of REAL
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n . d is V11() real ext-real Element of REAL
(REAL,d,n) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Sum (REAL,d,n) is V11() real ext-real Element of REAL
K298(REAL,(REAL,d,n),K203()) is V11() real ext-real Element of REAL
(n . d) + (Sum (REAL,d,n)) is V11() real ext-real Element of REAL
d + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n . (d + 1) is V11() real ext-real Element of REAL
(REAL,(d + 1),n) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Sum (REAL,(d + 1),n) is V11() real ext-real Element of REAL
K298(REAL,(REAL,(d + 1),n),K203()) is V11() real ext-real Element of REAL
(n . (d + 1)) + (Sum (REAL,(d + 1),n)) is V11() real ext-real Element of REAL
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n . 1 is V11() real ext-real Element of REAL
<*(n . 1)*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() V43(1) FinSequence-like FinSubsequence-like V63() V64() V65() V67() V68() V69() V70() FinSequence of REAL
[1,(n . 1)] is set
{1,(n . 1)} is non empty V73() V74() V75() set
{{1,(n . 1)},{1}} is non empty set
{[1,(n . 1)]} is non empty V2() Relation-like Function-like constant V43(1) set
(REAL,1,n) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
<*(n . 1)*> ^ (REAL,1,n) is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Sum <*(n . 1)*> is V11() real ext-real Element of REAL
K298(REAL,<*(n . 1)*>,K203()) is V11() real ext-real Element of REAL
Sum (REAL,1,n) is V11() real ext-real Element of REAL
K298(REAL,(REAL,1,n),K203()) is V11() real ext-real Element of REAL
(Sum <*(n . 1)*>) + (Sum (REAL,1,n)) is V11() real ext-real Element of REAL
(n . 1) + (Sum (REAL,1,n)) is V11() real ext-real Element of REAL
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
<*(n . (d + 1))*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() V43(1) FinSequence-like FinSubsequence-like V63() V64() V65() V67() V68() V69() V70() FinSequence of REAL
[1,(n . (d + 1))] is set
{1,(n . (d + 1))} is non empty V73() V74() V75() set
{{1,(n . (d + 1))},{1}} is non empty set
{[1,(n . (d + 1))]} is non empty V2() Relation-like Function-like constant V43(1) set
(d + 1) - 1 is V11() real ext-real integer rational Element of REAL
(len n) - (d + 1) is V11() real ext-real integer rational Element of REAL
d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d1 ^ <*(n . (d + 1))*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(d1 ^ <*(n . (d + 1))*>) ^ d is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 ^ d is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
e1 is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
e1 ^ <*(n . (d + 1))*> is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Sum (e1 ^ <*(n . (d + 1))*>) is V11() real ext-real Element of REAL
K298(REAL,(e1 ^ <*(n . (d + 1))*>),K203()) is V11() real ext-real Element of REAL
d1 is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Sum d1 is V11() real ext-real Element of REAL
K298(REAL,d1,K203()) is V11() real ext-real Element of REAL
(Sum (e1 ^ <*(n . (d + 1))*>)) + (Sum d1) is V11() real ext-real Element of REAL
Sum e1 is V11() real ext-real Element of REAL
K298(REAL,e1,K203()) is V11() real ext-real Element of REAL
Sum <*(n . (d + 1))*> is V11() real ext-real Element of REAL
K298(REAL,<*(n . (d + 1))*>,K203()) is V11() real ext-real Element of REAL
(Sum e1) + (Sum <*(n . (d + 1))*>) is V11() real ext-real Element of REAL
((Sum e1) + (Sum <*(n . (d + 1))*>)) + (Sum d1) is V11() real ext-real Element of REAL
(n . (d + 1)) + (Sum e1) is V11() real ext-real Element of REAL
((n . (d + 1)) + (Sum e1)) + (Sum d1) is V11() real ext-real Element of REAL
(Sum e1) + (Sum d1) is V11() real ext-real Element of REAL
(n . (d + 1)) + ((Sum e1) + (Sum d1)) is V11() real ext-real Element of REAL
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n . 0 is V11() real ext-real Element of REAL
(REAL,0,n) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Sum (REAL,0,n) is V11() real ext-real Element of REAL
K298(REAL,(REAL,0,n),K203()) is V11() real ext-real Element of REAL
(n . 0) + (Sum (REAL,0,n)) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
dom n is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
K298(REAL,n,K205()) is V11() real ext-real Element of REAL
n . k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(n) / (n . k) is V11() real ext-real non negative rational Element of REAL
<*(n . k)*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant V36() V43(1) FinSequence-like FinSubsequence-like V63() V64() V65() V67() V68() V69() V70() FinSequence of REAL
[1,(n . k)] is set
{1,(n . k)} is non empty V73() V74() V75() V76() V77() V78() set
{{1,(n . k)},{1}} is non empty set
{[1,(n . k)]} is non empty V2() Relation-like Function-like constant V43(1) set
k - 1 is V11() real ext-real integer rational Element of REAL
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len n) - k is V11() real ext-real integer rational Element of REAL
d is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d ^ <*(n . k)*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d1 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
(d ^ <*(n . k)*>) ^ d1 is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
d1 ^ <*(n . k)*> is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of REAL
Product (d1 ^ <*(n . k)*>) is V11() real ext-real Element of REAL
K298(REAL,(d1 ^ <*(n . k)*>),K205()) is V11() real ext-real Element of REAL
d is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
(d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
K298(REAL,d,K205()) is V11() real ext-real Element of REAL
(Product (d1 ^ <*(n . k)*>)) * (d) is V11() real ext-real Element of REAL
(d1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
K298(REAL,d1,K205()) is V11() real ext-real Element of REAL
(n . k) * (d1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
((n . k) * (d1)) * (d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(d1) * (d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(n . k) * ((d1) * (d)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(n . k) " is V11() real ext-real non negative rational Element of REAL
(n) * ((n . k) ") is V11() real ext-real non negative rational Element of REAL
(n) * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() Element of NAT
k is V11() real ext-real rational set
numerator k is V11() real ext-real integer rational set
denominator k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(numerator k) gcd (denominator k) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 * d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 * d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
e1 is V11() real ext-real integer rational set
d1 * e1 is V11() real ext-real integer rational Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is V11() real ext-real integer rational set
n / k is V11() real ext-real rational set
d is V11() real ext-real rational set
numerator d is V11() real ext-real integer rational set
denominator d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(numerator d) * d1 is V11() real ext-real integer rational Element of REAL
(denominator d) * d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n gcd k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
abs d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is V11() real ext-real rational set
d |^ n is V11() real ext-real set
denominator d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
numerator d is V11() real ext-real integer rational set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(denominator d) |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(numerator d) |^ n is V11() real ext-real integer rational set
((numerator d) |^ n) gcd (denominator d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(numerator d) / (denominator d) is V11() real ext-real rational Element of REAL
((numerator d) |^ n) / ((denominator d) |^ n) is V11() real ext-real rational Element of REAL
k * ((denominator d) |^ n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(denominator d) |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
((denominator d) |^ d1) * (denominator d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k * (((denominator d) |^ d1) * (denominator d)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k * ((denominator d) |^ d1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(k * ((denominator d) |^ d1)) * (denominator d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
- 1 is V11() real ext-real non positive integer rational Element of REAL
1 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is V11() real ext-real integer rational set
d1 |^ n is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
d |^ n is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
d1 |^ n is V11() real ext-real integer rational set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is V11() real ext-real rational set
d |^ n is V11() real ext-real set
d is V11() real ext-real integer rational set
d |^ n is V11() real ext-real integer rational set
0 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
2 * d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(2 * d1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
- d is V11() real ext-real non positive integer rational Element of REAL
d |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
- (d |^ n) is V11() real ext-real non positive integer rational Element of REAL
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
e1 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
1 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n |^ k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d |^ k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(n |^ k) * d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(d |^ k) / (n |^ k) is V11() real ext-real non negative rational set
d / n is V11() real ext-real non negative rational set
(d / n) |^ k is V11() real ext-real set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d |^ k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n * d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(n * d) |^ k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
0 * d is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() Element of NAT
n * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
0 gcd d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
0 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() Element of REAL
d * 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(0 * 0) + (d * 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
d is V11() real ext-real integer rational set
0 * d is V11() real ext-real integer rational Element of REAL
d1 is V11() real ext-real integer rational set
k * d1 is V11() real ext-real integer rational set
(0 * d) + (k * d1) is V11() real ext-real integer rational Element of REAL
k + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k * 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n * 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(k * 1) + (n * 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 is V11() real ext-real integer rational set
k * d1 is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
n * d is V11() real ext-real integer rational set
(k * d1) + (n * d) is V11() real ext-real integer rational set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d * d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(d * d1) + d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 is V11() real ext-real integer rational set
k * d1 is V11() real ext-real integer rational set
e1 is V11() real ext-real integer rational set
n * e1 is V11() real ext-real integer rational set
(k * d1) + (n * e1) is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
k * d1 is V11() real ext-real integer rational set
e1 is V11() real ext-real integer rational set
n * e1 is V11() real ext-real integer rational set
(k * d1) + (n * e1) is V11() real ext-real integer rational set
k - (d * d1) is V11() real ext-real integer rational set
d1 * d1 is V11() real ext-real integer rational set
1 - (d1 * d1) is V11() real ext-real integer rational Element of REAL
k * (1 - (d1 * d1)) is V11() real ext-real integer rational Element of REAL
e1 * d1 is V11() real ext-real integer rational set
- (e1 * d1) is V11() real ext-real integer rational set
n * (- (e1 * d1)) is V11() real ext-real integer rational set
(k * (1 - (d1 * d1))) + (n * (- (e1 * d1))) is V11() real ext-real integer rational Element of REAL
e1 is V11() real ext-real integer rational set
k * e1 is V11() real ext-real integer rational set
fs is V11() real ext-real integer rational set
n * fs is V11() real ext-real integer rational set
(k * e1) + (n * fs) is V11() real ext-real integer rational set
e1 is V11() real ext-real integer rational set
k * e1 is V11() real ext-real integer rational set
fs is V11() real ext-real integer rational set
n * fs is V11() real ext-real integer rational set
(k * e1) + (n * fs) is V11() real ext-real integer rational set
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d * e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
fs is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(d * e1) + fs is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n - (d * e1) is V11() real ext-real integer rational set
e1 * e1 is V11() real ext-real integer rational set
1 - (e1 * e1) is V11() real ext-real integer rational Element of REAL
n * (1 - (e1 * e1)) is V11() real ext-real integer rational Element of REAL
d1 * e1 is V11() real ext-real integer rational set
- (d1 * e1) is V11() real ext-real integer rational set
k * (- (d1 * e1)) is V11() real ext-real integer rational set
(n * (1 - (e1 * e1))) + (k * (- (d1 * e1))) is V11() real ext-real integer rational Element of REAL
v1 is V11() real ext-real integer rational set
k * v1 is V11() real ext-real integer rational set
v2 is V11() real ext-real integer rational set
n * v2 is V11() real ext-real integer rational set
(k * v1) + (n * v2) is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
k * d is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
n * d1 is V11() real ext-real integer rational set
(k * d) + (n * d1) is V11() real ext-real integer rational set
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
k gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
abs k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
abs n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(abs k) gcd (abs n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is V11() real ext-real integer rational set
(abs k) * d is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
(abs n) * d1 is V11() real ext-real integer rational set
((abs k) * d) + ((abs n) * d1) is V11() real ext-real integer rational set
- n is V11() real ext-real integer rational set
k * d is V11() real ext-real integer rational set
- d1 is V11() real ext-real integer rational set
n * (- d1) is V11() real ext-real integer rational set
(k * d) + (n * (- d1)) is V11() real ext-real integer rational set
- k is V11() real ext-real integer rational set
- d is V11() real ext-real integer rational set
k * (- d) is V11() real ext-real integer rational set
n * d1 is V11() real ext-real integer rational set
(k * (- d)) + (n * d1) is V11() real ext-real integer rational set
- k is V11() real ext-real integer rational set
- n is V11() real ext-real integer rational set
- d is V11() real ext-real integer rational set
k * (- d) is V11() real ext-real integer rational set
- d1 is V11() real ext-real integer rational set
n * (- d1) is V11() real ext-real integer rational set
(k * (- d)) + (n * (- d1)) is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
k * d is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
n * d1 is V11() real ext-real integer rational set
(k * d) + (n * d1) is V11() real ext-real integer rational set
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
k gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is V11() real ext-real integer rational set
n * d is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
k * d1 is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
n * d is V11() real ext-real integer rational set
(k * d1) + (n * d) is V11() real ext-real integer rational set
((k * d1) + (n * d)) * d is V11() real ext-real integer rational set
d1 * d is V11() real ext-real integer rational set
k * (d1 * d) is V11() real ext-real integer rational set
(n * d) * d is V11() real ext-real integer rational set
(k * (d1 * d)) + ((n * d) * d) is V11() real ext-real integer rational set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n * d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is V11() real ext-real integer rational set
k * d is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
n * d1 is V11() real ext-real integer rational set
(k * d) + (n * d1) is V11() real ext-real integer rational set
d / n is V11() real ext-real rational set
- (d / n) is V11() real ext-real rational set
d1 / k is V11() real ext-real rational set
max ((- (d / n)),(d1 / k)) is V11() real ext-real set
[/(max ((- (d / n)),(d1 / k)))\] is V11() real ext-real integer rational set
[/(max ((- (d / n)),(d1 / k)))\] + 1 is V11() real ext-real integer rational Element of REAL
([/(max ((- (d / n)),(d1 / k)))\] + 1) * k is V11() real ext-real integer rational Element of REAL
(([/(max ((- (d / n)),(d1 / k)))\] + 1) * k) - d1 is V11() real ext-real integer rational Element of REAL
- d is V11() real ext-real integer rational set
(- d) / n is V11() real ext-real rational set
([/(max ((- (d / n)),(d1 / k)))\] + 1) * n is V11() real ext-real integer rational Element of REAL
(([/(max ((- (d / n)),(d1 / k)))\] + 1) * n) - (- d) is V11() real ext-real integer rational Element of REAL
(([/(max ((- (d / n)),(d1 / k)))\] + 1) * n) + d is V11() real ext-real integer rational Element of REAL
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
k * d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n * e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(k * d1) - (n * e1) is V11() real ext-real integer rational Element of REAL
(k * d) + 0 is V11() real ext-real integer rational set
((k * d) + 0) + (n * d1) is V11() real ext-real integer rational set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d |^ k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
0 |^ k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
0 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
0 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
0 |^ k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k * d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n * d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(k * d) - (n * d1) is V11() real ext-real integer rational set
d1 |^ d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(d1 |^ d) / (d |^ d1) is V11() real ext-real non negative rational set
d #Z 1 is set
d |^ (k * d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d |^ (d1 * n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(d |^ (k * d)) / (d |^ (d1 * n)) is V11() real ext-real non negative rational set
(d |^ k) |^ d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
((d |^ k) |^ d) / (d |^ (d1 * n)) is V11() real ext-real non negative rational set
(d1 |^ n) |^ d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(d |^ d1) |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
((d1 |^ n) |^ d) / ((d |^ d1) |^ n) is V11() real ext-real non negative rational set
n * d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 |^ (n * d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(d1 |^ (n * d)) / ((d |^ d1) |^ n) is V11() real ext-real non negative rational set
(d1 |^ d) |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
((d1 |^ d) |^ n) / ((d |^ d1) |^ n) is V11() real ext-real non negative rational set
e1 is V11() real ext-real rational set
e1 |^ n is V11() real ext-real set
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
e1 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
e1 |^ (k * n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
e1 |^ k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(e1 |^ k) |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d |^ k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
k gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
k * d1 is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
n * d is V11() real ext-real integer rational set
(k * d1) + (n * d) is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
(k gcd n) * d1 is V11() real ext-real integer rational set
d1 * d1 is V11() real ext-real integer rational set
k * (d1 * d1) is V11() real ext-real integer rational set
d * d1 is V11() real ext-real integer rational set
n * (d * d1) is V11() real ext-real integer rational set
(k * (d1 * d1)) + (n * (d * d1)) is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
k * d1 is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
n * d is V11() real ext-real integer rational set
(k * d1) + (n * d) is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
k * d1 is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
n * d is V11() real ext-real integer rational set
(k * d1) + (n * d) is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
k * d1 is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
n * d is V11() real ext-real integer rational set
(k * d1) + (n * d) is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
k * d1 is V11() real ext-real integer rational set
e1 is V11() real ext-real integer rational set
n * e1 is V11() real ext-real integer rational set
(k * d1) + (n * e1) is V11() real ext-real integer rational set
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
k gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n / (k gcd n) is V11() real ext-real rational set
k / (k gcd n) is V11() real ext-real rational set
d is V11() real ext-real integer rational set
k * d is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
n * d1 is V11() real ext-real integer rational set
(k * d) + (n * d1) is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
d1 is V11() real ext-real integer rational set
(k gcd n) * d1 is V11() real ext-real integer rational set
e1 is V11() real ext-real integer rational set
(k gcd n) * e1 is V11() real ext-real integer rational set
e1 gcd d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
e1 is V11() real ext-real integer rational set
k * e1 is V11() real ext-real integer rational set
fs is V11() real ext-real integer rational set
n * fs is V11() real ext-real integer rational set
(k * e1) + (n * fs) is V11() real ext-real integer rational set
e1 - d is V11() real ext-real integer rational set
k * (e1 - d) is V11() real ext-real integer rational set
d1 - fs is V11() real ext-real integer rational set
n * (d1 - fs) is V11() real ext-real integer rational set
d1 * (e1 - d) is V11() real ext-real integer rational set
(n * (d1 - fs)) / (k gcd n) is V11() real ext-real rational set
e1 * (d1 - fs) is V11() real ext-real integer rational set
v1 is V11() real ext-real integer rational set
e1 * v1 is V11() real ext-real integer rational set
(e1 - d) / e1 is V11() real ext-real rational set
(d1 - fs) / d1 is V11() real ext-real rational set
v1 * d1 is V11() real ext-real integer rational set
d1 - (v1 * d1) is V11() real ext-real integer rational set
v1 * e1 is V11() real ext-real integer rational set
d + (v1 * e1) is V11() real ext-real integer rational set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k gcd d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(k gcd d) |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(k gcd d) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
((k gcd d) |^ d1) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
((k gcd d) |^ d1) * d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
1 + e1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
v2 is V11() real ext-real integer rational set
(k gcd d) * v2 is V11() real ext-real integer rational set
v1 is V11() real ext-real integer rational set
(k gcd d) * v1 is V11() real ext-real integer rational set
v2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
fs is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
fs + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(k gcd d) |^ (fs + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
((k gcd d) |^ (fs + 1)) * e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(((k gcd d) |^ (fs + 1)) * e1) / (k gcd d) is V11() real ext-real non negative rational Element of REAL
(k gcd d) |^ fs is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(k gcd d) * ((k gcd d) |^ fs) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
((k gcd d) * ((k gcd d) |^ fs)) * e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(((k gcd d) * ((k gcd d) |^ fs)) * e1) / (k gcd d) is V11() real ext-real non negative rational Element of REAL
((k gcd d) |^ fs) * e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(k gcd d) * (((k gcd d) |^ fs) * e1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
((k gcd d) * (((k gcd d) |^ fs) * e1)) / (k gcd d) is V11() real ext-real non negative rational Element of REAL
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
v2 gcd x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
e1 gcd x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
x1 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
e1 gcd (x1 |^ d1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v1 is V11() real ext-real Element of REAL
v1 |^ d1 is V11() real ext-real Element of REAL
d / (k gcd d) is V11() real ext-real non negative rational set
e1 * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
((k gcd d) |^ d1) * (e1 * n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(((k gcd d) |^ d1) * (e1 * n)) / ((k gcd d) |^ d1) is V11() real ext-real non negative rational Element of REAL
1 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
0 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v1 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v2 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v1 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v2 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v1 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v2 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v1 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v2 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
1 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
e1 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
fs is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
fs |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v1 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v2 |^ d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
dom k is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
(k) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
K298(REAL,k,K205()) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(k) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
<*d1*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V36() V43(1) FinSequence-like FinSubsequence-like V63() V64() V65() V66() V67() V68() V69() V70() FinSequence of NAT
[1,d1] is set
{1,d1} is non empty V73() V74() V75() V76() V77() V78() set
{{1,d1},{1}} is non empty set
{[1,d1]} is non empty V2() Relation-like Function-like constant V43(1) set
(REAL,NAT,d,<*d1*>) is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
dom (REAL,NAT,d,<*d1*>) is non empty V73() V74() V75() V76() V77() V78() Element of K6(NAT)
((REAL,NAT,d,<*d1*>)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
K298(REAL,(REAL,NAT,d,<*d1*>),K205()) is V11() real ext-real Element of REAL
((REAL,NAT,d,<*d1*>)) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
dom d is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d . d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(d . d1) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(REAL,NAT,d,<*d1*>) . d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
((REAL,NAT,d,<*d1*>) . d1) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
len (REAL,NAT,d,<*d1*>) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
len d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len d) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(REAL,NAT,d,<*d1*>) . (len (REAL,NAT,d,<*d1*>)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
((REAL,NAT,d,<*d1*>) . (len (REAL,NAT,d,<*d1*>))) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
K298(REAL,d,K205()) is V11() real ext-real Element of REAL
(d) * d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
dom d1 is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
d1 . e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(d1 . e1) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(d1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
K298(REAL,d1,K205()) is V11() real ext-real Element of REAL
(d1) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
<*> NAT is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() FinSequence of NAT
dom (<*> NAT) is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() Element of K6(NAT)
((<*> NAT)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
((<*> NAT)) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
dom d is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
d . d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(d . d1) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
K298(REAL,d,K205()) is V11() real ext-real Element of REAL
(d) gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
len k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
dom k is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
k . 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
<*d*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V36() V43(1) FinSequence-like FinSubsequence-like V63() V64() V65() V66() V67() V68() V69() V70() FinSequence of NAT
[1,d] is set
{1,d} is non empty V73() V74() V75() V76() V77() V78() set
{{1,d},{1}} is non empty set
{[1,d]} is non empty V2() Relation-like Function-like constant V43(1) set
(REAL,NAT,n,<*d*>) is non empty Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
len (REAL,NAT,n,<*d*>) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
dom (REAL,NAT,n,<*d*>) is non empty V73() V74() V75() V76() V77() V78() Element of K6(NAT)
(len n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
len d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(REAL,NAT,n,<*d*>) . 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(REAL,NAT,n,<*d*>) . 2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
((REAL,NAT,n,<*d*>) . 1) gcd ((REAL,NAT,n,<*d*>) . 2) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 . 1 is V11() real ext-real integer rational Element of REAL
d1 . 2 is V11() real ext-real integer rational Element of REAL
(d1 . 1) - (d1 . 2) is V11() real ext-real integer rational Element of REAL
e1 is V11() real ext-real integer rational set
((REAL,NAT,n,<*d*>) . 1) * e1 is V11() real ext-real integer rational Element of REAL
e1 is V11() real ext-real integer rational set
((REAL,NAT,n,<*d*>) . 2) * e1 is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,n,<*d*>) . 1) * e1) + (((REAL,NAT,n,<*d*>) . 2) * e1) is V11() real ext-real integer rational Element of REAL
- e1 is V11() real ext-real integer rational set
fs is V11() real ext-real integer rational Element of INT
v1 is V11() real ext-real integer rational Element of INT
<*fs,v1*> is non empty Relation-like NAT -defined INT -valued Function-like V36() V43(2) FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
<*fs*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,fs] is set
{1,fs} is non empty V73() V74() V75() V76() V77() set
{{1,fs},{1}} is non empty set
{[1,fs]} is non empty V2() Relation-like Function-like constant V43(1) set
<*v1*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,v1] is set
{1,v1} is non empty V73() V74() V75() V76() V77() set
{{1,v1},{1}} is non empty set
{[1,v1]} is non empty V2() Relation-like Function-like constant V43(1) set
<*fs*> ^ <*v1*> is non empty Relation-like NAT -defined Function-like V36() V43(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
v2 is non empty Relation-like NAT -defined INT -valued Function-like V36() V43(2) FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
len v2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
Seg (len (REAL,NAT,n,<*d*>)) is non empty V36() V43( len (REAL,NAT,n,<*d*>)) V73() V74() V75() V76() V77() V78() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT : ( 1 <= b₁ & b₁ <= len (REAL,NAT,n,<*d*>) ) } is set
(REAL,NAT,n,<*d*>) . v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
v2 . v1 is V11() real ext-real integer rational Element of REAL
((REAL,NAT,n,<*d*>) . v1) * (v2 . v1) is V11() real ext-real integer rational Element of REAL
d1 . v1 is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,n,<*d*>) . v1) * (v2 . v1)) + (d1 . v1) is V11() real ext-real integer rational Element of REAL
v2 . 1 is V11() real ext-real integer rational Element of REAL
((REAL,NAT,n,<*d*>) . 1) * (v2 . 1) is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,n,<*d*>) . 1) * (v2 . 1)) + (d1 . 1) is V11() real ext-real integer rational Element of REAL
v2 . 1 is V11() real ext-real integer rational Element of REAL
v2 . 2 is V11() real ext-real integer rational Element of REAL
((REAL,NAT,n,<*d*>) . 1) * (- e1) is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,n,<*d*>) . 2) * e1) - (((REAL,NAT,n,<*d*>) . 1) * (- e1)) is V11() real ext-real integer rational Element of REAL
(REAL,NAT,n,<*d*>) . v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
v2 . v1 is V11() real ext-real integer rational Element of REAL
((REAL,NAT,n,<*d*>) . v1) * (v2 . v1) is V11() real ext-real integer rational Element of REAL
d1 . v1 is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,n,<*d*>) . v1) * (v2 . v1)) + (d1 . v1) is V11() real ext-real integer rational Element of REAL
((REAL,NAT,n,<*d*>) . 1) * (v2 . 1) is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,n,<*d*>) . 1) * (v2 . 1)) + (d1 . 1) is V11() real ext-real integer rational Element of REAL
(REAL,NAT,n,<*d*>) . v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
v2 . v1 is V11() real ext-real integer rational Element of REAL
((REAL,NAT,n,<*d*>) . v1) * (v2 . v1) is V11() real ext-real integer rational Element of REAL
d1 . v1 is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,n,<*d*>) . v1) * (v2 . v1)) + (d1 . v1) is V11() real ext-real integer rational Element of REAL
v2 . 1 is V11() real ext-real integer rational Element of REAL
((REAL,NAT,n,<*d*>) . 1) * (v2 . 1) is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,n,<*d*>) . 1) * (v2 . 1)) + (d1 . 1) is V11() real ext-real integer rational Element of REAL
(REAL,NAT,n,<*d*>) . v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
v2 . v1 is V11() real ext-real integer rational Element of REAL
((REAL,NAT,n,<*d*>) . v1) * (v2 . v1) is V11() real ext-real integer rational Element of REAL
d1 . v1 is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,n,<*d*>) . v1) * (v2 . v1)) + (d1 . v1) is V11() real ext-real integer rational Element of REAL
v2 . 1 is V11() real ext-real integer rational Element of REAL
((REAL,NAT,n,<*d*>) . 1) * (v2 . 1) is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,n,<*d*>) . 1) * (v2 . 1)) + (d1 . 1) is V11() real ext-real integer rational Element of REAL
d1 is Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
len d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 . 1 is V11() real ext-real integer rational Element of REAL
dom n is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n . d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n . e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(n . d1) gcd (n . e1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(REAL,NAT,n,<*d*>) . d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(REAL,NAT,n,<*d*>) . e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
len d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
e1 is Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
e1 is V11() real ext-real integer rational Element of INT
<*e1*> is non empty V2() Relation-like NAT -defined INT -valued Function-like one-to-one constant V36() V43(1) FinSequence-like FinSubsequence-like V63() V64() V65() V67() V68() V69() V70() FinSequence of INT
[1,e1] is set
{1,e1} is non empty V73() V74() V75() V76() V77() set
{{1,e1},{1}} is non empty set
{[1,e1]} is non empty V2() Relation-like Function-like constant V43(1) set
e1 ^ <*e1*> is non empty Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
len e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len e1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n . 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
e1 . 1 is V11() real ext-real integer rational Element of REAL
fs is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
len fs is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
dom fs is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
v2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
fs . v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
fs . v2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(fs . v1) gcd (fs . v2) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
fs . 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
fs is Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
len fs is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
fs . 1 is V11() real ext-real integer rational Element of REAL
(n . 1) * (fs . 1) is V11() real ext-real integer rational Element of REAL
((n . 1) * (fs . 1)) + (e1 . 1) is V11() real ext-real integer rational Element of REAL
v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n . v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(n . v1) gcd d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(REAL,NAT,n,<*d*>) . ((len n) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(REAL,NAT,n,<*d*>) . v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
K298(REAL,n,K205()) is V11() real ext-real Element of REAL
(n) gcd d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 . ((len n) + 1) is V11() real ext-real integer rational Element of REAL
(d1 . ((len n) + 1)) - ((n . 1) * (fs . 1)) is V11() real ext-real integer rational Element of REAL
d1 . 1 is V11() real ext-real integer rational Element of REAL
((d1 . ((len n) + 1)) - ((n . 1) * (fs . 1))) - (d1 . 1) is V11() real ext-real integer rational Element of REAL
v1 is V11() real ext-real integer rational set
(n) * v1 is V11() real ext-real integer rational Element of REAL
v2 is V11() real ext-real integer rational set
d * v2 is V11() real ext-real integer rational Element of REAL
((n) * v1) + (d * v2) is V11() real ext-real integer rational Element of REAL
- v2 is V11() real ext-real integer rational set
v2 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len v2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
dom v2 is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
v2 . x1 is set
x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
v2 . x2 is set
(REAL,NAT,x2,n) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
((REAL,NAT,x2,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
K298(REAL,(REAL,NAT,x2,n),K205()) is V11() real ext-real Element of REAL
((REAL,NAT,x2,n)) * v1 is V11() real ext-real integer rational Element of REAL
fs . x2 is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,x2,n)) * v1) + (fs . x2) is V11() real ext-real integer rational Element of REAL
Seg (len n) is V36() V43( len n) V73() V74() V75() V76() V77() V78() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
x1 is Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
v1 is V11() real ext-real integer rational Element of INT
<*v1*> is non empty V2() Relation-like NAT -defined INT -valued Function-like one-to-one constant V36() V43(1) FinSequence-like FinSubsequence-like V63() V64() V65() V67() V68() V69() V70() FinSequence of INT
[1,v1] is set
{1,v1} is non empty V73() V74() V75() V76() V77() set
{{1,v1},{1}} is non empty set
{[1,v1]} is non empty V2() Relation-like Function-like constant V43(1) set
x1 ^ <*v1*> is non empty Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
x2 is non empty Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
len x2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(REAL,NAT,n,<*d*>) . x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
x2 . x is V11() real ext-real integer rational Element of REAL
((REAL,NAT,n,<*d*>) . x) * (x2 . x) is V11() real ext-real integer rational Element of REAL
d1 . x is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,n,<*d*>) . x) * (x2 . x)) + (d1 . x) is V11() real ext-real integer rational Element of REAL
(REAL,NAT,n,<*d*>) . 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
x2 . 1 is V11() real ext-real integer rational Element of REAL
((REAL,NAT,n,<*d*>) . 1) * (x2 . 1) is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,n,<*d*>) . 1) * (x2 . 1)) + (d1 . 1) is V11() real ext-real integer rational Element of REAL
y1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(REAL,NAT,n,<*d*>) . y1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
x2 . y1 is V11() real ext-real integer rational Element of REAL
((REAL,NAT,n,<*d*>) . y1) * (x2 . y1) is V11() real ext-real integer rational Element of REAL
n . y1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
fs . y1 is V11() real ext-real integer rational Element of REAL
(n . y1) * (fs . y1) is V11() real ext-real integer rational Element of REAL
((n) * v1) + ((n . y1) * (fs . y1)) is V11() real ext-real integer rational Element of REAL
dom x1 is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
x1 . y1 is V11() real ext-real integer rational Element of REAL
(REAL,NAT,y1,n) is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
((REAL,NAT,y1,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
K298(REAL,(REAL,NAT,y1,n),K205()) is V11() real ext-real Element of REAL
((REAL,NAT,y1,n)) * v1 is V11() real ext-real integer rational Element of REAL
(((REAL,NAT,y1,n)) * v1) + (fs . y1) is V11() real ext-real integer rational Element of REAL
(n . y1) * ((REAL,NAT,y1,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
((n . y1) * ((REAL,NAT,y1,n))) * v1 is V11() real ext-real integer rational Element of REAL
(((n . y1) * ((REAL,NAT,y1,n))) * v1) + ((n . y1) * (fs . y1)) is V11() real ext-real integer rational Element of REAL
dom e1 is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
e1 . x is V11() real ext-real integer rational Element of REAL
n . x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
fs . x is V11() real ext-real integer rational Element of REAL
(n . x) * (fs . x) is V11() real ext-real integer rational Element of REAL
((n) * v1) + ((n . x) * (fs . x)) is V11() real ext-real integer rational Element of REAL
(((n) * v1) + ((n . x) * (fs . x))) + (d1 . x) is V11() real ext-real integer rational Element of REAL
((n . x) * (fs . x)) + (e1 . x) is V11() real ext-real integer rational Element of REAL
((n) * v1) + (((n . x) * (fs . x)) + (e1 . x)) is V11() real ext-real integer rational Element of REAL
((n) * v1) + (((n . 1) * (fs . 1)) + (e1 . 1)) is V11() real ext-real integer rational Element of REAL
((n) * v1) + ((n . 1) * (fs . 1)) is V11() real ext-real integer rational Element of REAL
(((n) * v1) + ((n . 1) * (fs . 1))) + (e1 . 1) is V11() real ext-real integer rational Element of REAL
((n . 1) * (fs . 1)) + (d1 . 1) is V11() real ext-real integer rational Element of REAL
(d1 . x) - (((n . 1) * (fs . 1)) + (d1 . 1)) is V11() real ext-real integer rational Element of REAL
(d * v2) + ((n) * v1) is V11() real ext-real integer rational Element of REAL
((n) * v1) + ((n . 1) * (fs . 1)) is V11() real ext-real integer rational Element of REAL
(((n) * v1) + ((n . 1) * (fs . 1))) + (d1 . 1) is V11() real ext-real integer rational Element of REAL
d * (- v2) is V11() real ext-real integer rational Element of REAL
(d1 . x) + (d * (- v2)) is V11() real ext-real integer rational Element of REAL
d1 is Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
len d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 . 1 is V11() real ext-real integer rational Element of REAL
(REAL,NAT,n,<*d*>) . 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(REAL,NAT,n,<*d*>) . 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
d1 is Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
len d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 . 1 is V11() real ext-real integer rational Element of REAL
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
(REAL,NAT,n,<*d*>) . d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(REAL,NAT,n,<*d*>) . e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
((REAL,NAT,n,<*d*>) . d1) gcd ((REAL,NAT,n,<*d*>) . e1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
<*> NAT is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() FinSequence of NAT
len (<*> NAT) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() Element of NAT
dom (<*> NAT) is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() Element of K6(NAT)
(<*> NAT) . 1 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer rational V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V63() V64() V65() V66() V73() V74() V75() V76() V77() V78() V79() Element of REAL
n is Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n . 1 is V11() real ext-real integer rational Element of REAL
n is Relation-like NAT -defined INT -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() FinSequence of INT
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n . 1 is V11() real ext-real integer rational Element of REAL
d is Relation-like NAT -defined REAL -valued Function-like V36() FinSequence-like FinSubsequence-like V63() V64() V65() V66() FinSequence of NAT
len d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
dom d is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d . d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
d . d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
(d . d1) gcd (d . d) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d . 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() Element of REAL
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
abs n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
- n is V11() real ext-real integer rational set
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
k * n is V11() real ext-real integer rational set
(k * n) mod n is V11() real ext-real integer rational set
(k * n) div n is V11() real ext-real integer rational set
((k * n) div n) * n is V11() real ext-real integer rational set
(k * n) - (((k * n) div n) * n) is V11() real ext-real integer rational set
(k * n) / n is V11() real ext-real rational set
[\((k * n) / n)/] is V11() real ext-real integer rational set
[\((k * n) / n)/] * n is V11() real ext-real integer rational set
(k * n) - ([\((k * n) / n)/] * n) is V11() real ext-real integer rational set
[\k/] is V11() real ext-real integer rational set
[\k/] * n is V11() real ext-real integer rational set
(k * n) - ([\k/] * n) is V11() real ext-real integer rational set
(k * n) - (k * n) is V11() real ext-real integer rational set
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
k mod n is V11() real ext-real integer rational set
d is V11() real ext-real integer rational set
d mod n is V11() real ext-real integer rational set
k - d is V11() real ext-real integer rational set
(k - d) mod n is V11() real ext-real integer rational set
k div n is V11() real ext-real integer rational set
(k div n) * n is V11() real ext-real integer rational set
k - ((k div n) * n) is V11() real ext-real integer rational set
d div n is V11() real ext-real integer rational set
(d div n) * n is V11() real ext-real integer rational set
d - ((d div n) * n) is V11() real ext-real integer rational set
(k div n) - (d div n) is V11() real ext-real integer rational set
n * ((k div n) - (d div n)) is V11() real ext-real integer rational set
k is V11() real ext-real integer rational set
n is V11() real ext-real integer rational set
n mod k is V11() real ext-real integer rational set
n div k is V11() real ext-real integer rational set
(n div k) * k is V11() real ext-real integer rational set
((n div k) * k) + 0 is V11() real ext-real integer rational set
k is V11() real ext-real integer rational set
sqrt k is V11() real ext-real set
(sqrt k) ^2 is V11() real ext-real set
(sqrt k) * (sqrt k) is V11() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
sqrt k is V11() real ext-real set
n is V11() real ext-real integer rational set
k gcd n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n * d is V11() real ext-real integer rational set
d1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(n * d) + d1 is V11() real ext-real integer rational set
(n * d) - d1 is V11() real ext-real integer rational set
n * d is V11() real ext-real integer rational Element of REAL
(n * d) + d1 is V11() real ext-real integer rational Element of REAL
(n * d) - d1 is V11() real ext-real integer rational Element of REAL
[\(sqrt k)/] is V11() real ext-real integer rational set
[\(sqrt k)/] + 1 is V11() real ext-real integer rational Element of REAL
(sqrt k) - 1 is V11() real ext-real Element of REAL
d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 ^2 is V11() real ext-real Element of REAL
d1 * d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
d1 * d1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
e1 - 1 is V11() real ext-real integer rational Element of REAL
(e1 - 1) / d1 is V11() real ext-real rational Element of REAL
1 / d1 is V11() real ext-real non negative rational Element of REAL
d1 - (1 / d1) is V11() real ext-real rational Element of REAL
fs is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len fs is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
dom fs is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
rng fs is set
Seg k is V36() V43(k) V73() V74() V75() V76() V77() V78() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT : ( 1 <= b₁ & b₁ <= k ) } is set
v1 is set
v2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
fs . v2 is set
v2 - 1 is V11() real ext-real integer rational Element of REAL
(v2 - 1) div d1 is V11() real ext-real integer rational set
n * ((v2 - 1) div d1) is V11() real ext-real integer rational set
(v2 - 1) mod d1 is V11() real ext-real integer rational set
(n * ((v2 - 1) div d1)) + ((v2 - 1) mod d1) is V11() real ext-real integer rational set
((n * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) mod k is V11() real ext-real integer rational set
1 + (((n * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) mod k) is V11() real ext-real integer rational Element of REAL
v1 is V11() real ext-real integer rational set
v2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(sqrt k) ^2 is V11() real ext-real set
(sqrt k) * (sqrt k) is V11() real ext-real set
Seg e1 is V36() V43(e1) V73() V74() V75() V76() V77() V78() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT : ( 1 <= b₁ & b₁ <= e1 ) } is set
v1 is set
v2 is set
fs . v1 is set
fs . v2 is set
v1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
v1 - 1 is V11() real ext-real integer rational Element of REAL
(v1 - 1) div d1 is V11() real ext-real integer rational set
v2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
v2 - 1 is V11() real ext-real integer rational Element of REAL
(v2 - 1) div d1 is V11() real ext-real integer rational set
((v1 - 1) div d1) - ((v2 - 1) div d1) is V11() real ext-real integer rational set
(v1 - 1) mod d1 is V11() real ext-real integer rational set
(v2 - 1) mod d1 is V11() real ext-real integer rational set
((v1 - 1) mod d1) - ((v2 - 1) mod d1) is V11() real ext-real integer rational set
fs . v1 is set
n * ((v1 - 1) div d1) is V11() real ext-real integer rational set
(n * ((v1 - 1) div d1)) + ((v1 - 1) mod d1) is V11() real ext-real integer rational set
((n * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) mod k is V11() real ext-real integer rational set
1 + (((n * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) mod k) is V11() real ext-real integer rational Element of REAL
fs . v2 is set
n * ((v2 - 1) div d1) is V11() real ext-real integer rational set
(n * ((v2 - 1) div d1)) + ((v2 - 1) mod d1) is V11() real ext-real integer rational set
((n * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) mod k is V11() real ext-real integer rational set
1 + (((n * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) mod k) is V11() real ext-real integer rational Element of REAL
((n * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((n * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) is V11() real ext-real integer rational set
(((n * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((n * ((v2 - 1) div d1)) + ((v2 - 1) mod d1))) mod k is V11() real ext-real integer rational set
(v2 - 1) / d1 is V11() real ext-real rational Element of REAL
[\((v2 - 1) / d1)/] is V11() real ext-real integer rational set
n * (((v1 - 1) div d1) - ((v2 - 1) div d1)) is V11() real ext-real integer rational set
(n * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) is V11() real ext-real integer rational set
[\0/] is V11() real ext-real integer rational set
(v1 - 1) / d1 is V11() real ext-real rational Element of REAL
[\((v1 - 1) / d1)/] is V11() real ext-real integer rational set
((v2 - 1) div d1) - ((v1 - 1) div d1) is V11() real ext-real integer rational set
- d is V11() real ext-real non positive integer rational Element of REAL
- (((v2 - 1) div d1) - ((v1 - 1) div d1)) is V11() real ext-real integer rational set
((v2 - 1) div d1) * d1 is V11() real ext-real integer rational Element of REAL
(((v2 - 1) div d1) * d1) + ((v2 - 1) mod d1) is V11() real ext-real integer rational Element of REAL
((v2 - 1) mod d1) - ((v1 - 1) mod d1) is V11() real ext-real integer rational set
- (((v2 - 1) mod d1) - ((v1 - 1) mod d1)) is V11() real ext-real integer rational set
abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
n * b is V11() real ext-real integer rational set
abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(n * b) + e is V11() real ext-real integer rational set
(n * b) - e is V11() real ext-real integer rational set
- (((v1 - 1) div d1) - ((v2 - 1) div d1)) is V11() real ext-real integer rational set
- (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) is V11() real ext-real integer rational set
- ((n * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1))) is V11() real ext-real integer rational set
n * (- (((v1 - 1) div d1) - ((v2 - 1) div d1))) is V11() real ext-real integer rational set
(n * (- (((v1 - 1) div d1) - ((v2 - 1) div d1)))) + (- (((v1 - 1) mod d1) - ((v2 - 1) mod d1))) is V11() real ext-real integer rational set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
n is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
Del (n,k) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
dom (Del (n,k)) is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
dom n is V73() V74() V75() V76() V77() V78() Element of K6(NAT)
n is set
<*n*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty V2() Relation-like Function-like constant V43(1) set
k is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
<*n*> ^ k is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
Del ((<*n*> ^ k),1) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
d is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
len d is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
(len d) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V36() V41() V73() V74() V75() V76() V77() V78() Element of NAT
d1 is set
<*d1*> is non empty V2() Relation-like NAT -defined Function-like constant V36() V43(1) FinSequence-like FinSubsequence-like set
[1,d1] is set
{1,d1} is non empty set
{{1,d1},{1}} is non empty set
{[1,d1]} is non empty V2() Relation-like Function-like constant V43(1) set
d ^ <*d1*> is non empty Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
Del ((d ^ <*d1*>),((len d) + 1)) is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
k is V11() real ext-real integer rational set
- k is V11() real ext-real integer rational set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k mod n is V11() real ext-real integer rational set
k div n is V11() real ext-real integer rational set
- (k div n) is V11() real ext-real integer rational set
(- k) div n is V11() real ext-real integer rational set
((- k) div n) + 1 is V11() real ext-real integer rational Element of REAL
k / n is V11() real ext-real rational set
[\(k / n)/] is V11() real ext-real integer rational set
- [\(k / n)/] is V11() real ext-real integer rational set
(- k) / n is V11() real ext-real rational set
[\((- k) / n)/] is V11() real ext-real integer rational set
[\((- k) / n)/] + 1 is V11() real ext-real integer rational Element of REAL
k is V11() real ext-real integer rational set
- k is V11() real ext-real integer rational set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V36() V41() set
k mod n is V11() real ext-real integer rational set
k div n is V11() real ext-real integer rational set
- (k div n) is V11() real ext-real integer rational set
(- k) div n is V11() real ext-real integer rational set
k / n is V11() real ext-real rational set
[\(k / n)/] is V11() real ext-real integer rational set
- [\(k / n)/] is V11() real ext-real integer rational set
(- k) / n is V11() real ext-real rational set
[\((- k) / n)/] is V11() real ext-real integer rational set