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)
{ b1 where b1 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 <= b1 & b1 <= 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)
{ b1 where b1 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 <= b1 & b1 <= 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)
{ b1 where b1 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 <= b1 & b1 <= 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)
{ b1 where b1 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 <= b1 & b1 <= (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)
{ b1 where b1 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 <= b1 & b1 <= 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