REAL is non empty non trivial non finite non empty-membered complex-membered ext-real-membered real-membered V92() non bounded_below non bounded_above V120() set
NAT is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V92() left_end bounded_below Element of bool REAL
bool REAL is non empty non empty-membered set
bool NAT is non empty non empty-membered set
COMPLEX is non empty non trivial non finite non empty-membered complex-membered V92() set
omega is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V92() left_end bounded_below set
bool omega is non empty non empty-membered set
K158(NAT) is V35() set
[:NAT,REAL:] is Relation-like V76() V77() V78() set
bool [:NAT,REAL:] is set
RAT is non empty non trivial non finite non empty-membered complex-membered ext-real-membered real-membered rational-membered V92() set
INT is non empty non trivial non finite non empty-membered complex-membered ext-real-membered real-membered rational-membered integer-membered V92() set
[:COMPLEX,COMPLEX:] is Relation-like V76() set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like V76() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is Relation-like V76() V77() V78() set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is Relation-like V76() V77() V78() set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is Relation-like RAT -valued V76() V77() V78() set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued V76() V77() V78() set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is Relation-like RAT -valued INT -valued V76() V77() V78() set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued V76() V77() V78() set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued V76() V77() V78() V79() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued V76() V77() V78() V79() set
bool [:[:NAT,NAT:],NAT:] is set
K325() is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V40() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V76() V77() V78() V79() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V92() bounded_below bounded_above real-bounded V120() set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V40() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V76() V77() V78() V79() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V92() bounded_below bounded_above real-bounded V120() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V40() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V76() V77() V78() V79() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V92() bounded_below bounded_above real-bounded V120() set
{{},1} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
K520() is set
bool K520() is set
K521() is Element of bool K520()
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V40() FinSequence-like FinSubsequence-like FinSequence-membered V47() ext-real non positive non negative V76() V77() V78() V79() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V92() bounded_below bounded_above real-bounded V120() Element of NAT
Fib 0 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
Fib 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
sqrt 4 is V11() real ext-real Element of REAL
Seg 1 is non empty finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty finite with_non-empty_elements non empty-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
Seg 2 is non empty finite 2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite with_non-empty_elements non empty-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
Seg 3 is non empty finite 3 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= 3 ) } is set
K602(1,2,3) is finite with_non-empty_elements complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded set
Seg 4 is non empty finite 4 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= 4 ) } is set
K603(1,2,3,4) is finite with_non-empty_elements set
tau is V11() real ext-real set
5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
sqrt 5 is V11() real ext-real Element of REAL
1 + (sqrt 5) is V11() real ext-real set
K65((1 + (sqrt 5)),2) is V11() real ext-real Element of COMPLEX
tau_bar is V11() real ext-real set
1 - (sqrt 5) is V11() real ext-real set
K65((1 - (sqrt 5)),2) is V11() real ext-real Element of COMPLEX
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n -' 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
(n + 2) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n + 2) - 1 is V11() real integer ext-real set
- 1 is V11() real integer ext-real non positive set
n is non empty V11() real integer ext-real non even set
(- 1) to_power n is V11() real ext-real set
1 to_power n is V11() real ext-real set
- (1 to_power n) is V11() real ext-real set
n is V11() real integer ext-real even set
(- 1) to_power n is V11() real ext-real set
1 to_power n is V11() real ext-real set
n is non empty V11() real ext-real set
(- 1) * n is V11() real ext-real set
n is V11() real integer ext-real set
((- 1) * n) to_power n is V11() real ext-real set
(- 1) to_power n is V11() real ext-real set
n to_power n is V11() real ext-real set
((- 1) to_power n) * (n to_power n) is V11() real ext-real set
- n is V11() real ext-real set
(- n) to_power n is V11() real ext-real set
- (n to_power n) is V11() real ext-real set
(- 1) * (n to_power n) is V11() real ext-real set
- n is V11() real ext-real set
(- n) to_power n is V11() real ext-real set
1 * (n to_power n) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n + n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
C is V11() real ext-real set
C to_power (n + n) is V11() real ext-real set
C to_power n is V11() real ext-real set
C to_power n is V11() real ext-real set
(C to_power n) * (C to_power n) is V11() real ext-real set
C |^ (n + n) is V11() real ext-real set
C |^ n is V11() real ext-real set
C |^ n is V11() real ext-real set
(C |^ n) * (C |^ n) is V11() real ext-real set
(C to_power n) * (C |^ n) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n is non empty V11() real ext-real set
C is non empty V11() real integer ext-real non even set
n to_power C is V11() real ext-real set
(n to_power C) to_power n is V11() real ext-real set
C * n is V11() real integer ext-real set
n to_power (C * n) is V11() real ext-real set
n #Z (C * n) is V11() real ext-real set
n #Z C is V11() real ext-real set
(n #Z C) #Z n is V11() real ext-real set
(n to_power C) #Z n is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
- n is V11() real integer ext-real non positive set
(- 1) to_power (- n) is V11() real ext-real set
((- 1) to_power (- n)) ^2 is V11() real ext-real set
((- 1) to_power (- n)) * ((- 1) to_power (- n)) is V11() real ext-real set
(- 1) #Z (- n) is V11() real ext-real set
((- 1) #Z (- n)) ^2 is V11() real ext-real set
((- 1) #Z (- n)) * ((- 1) #Z (- n)) is V11() real ext-real set
(- 1) #Z n is V11() real ext-real set
1 / ((- 1) #Z n) is V11() real ext-real set
(1 / ((- 1) #Z n)) ^2 is V11() real ext-real set
(1 / ((- 1) #Z n)) * (1 / ((- 1) #Z n)) is V11() real ext-real set
(1 / ((- 1) #Z n)) to_power 2 is V11() real ext-real set
(1 / ((- 1) #Z n)) |^ 2 is V11() real ext-real set
((- 1) #Z n) |^ 2 is V11() real ext-real set
1 / (((- 1) #Z n) |^ 2) is V11() real ext-real set
((- 1) #Z n) #Z 2 is V11() real ext-real set
1 / (((- 1) #Z n) #Z 2) is V11() real ext-real set
n * 2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered even bounded_below Element of NAT
(- 1) #Z (n * 2) is V11() real ext-real set
1 / ((- 1) #Z (n * 2)) is V11() real ext-real set
2 * n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered even bounded_below Element of NAT
(- 1) |^ (2 * n) is V11() real ext-real set
1 / ((- 1) |^ (2 * n)) is V11() real ext-real set
1 |^ (2 * n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
1 / (1 |^ (2 * n)) is V11() real ext-real non negative set
1 |^ 2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(1 |^ 2) |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of REAL
1 / ((1 |^ 2) |^ n) is V11() real ext-real non negative set
1 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of REAL
1 / (1 |^ n) is V11() real ext-real non negative set
1 / 1 is V11() real ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
- n is V11() real integer ext-real non positive set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
- n is V11() real integer ext-real non positive set
(- n) - n is V11() real integer ext-real non positive set
r is non empty V11() real ext-real set
r to_power (- n) is V11() real ext-real set
r to_power (- n) is V11() real ext-real set
(r to_power (- n)) * (r to_power (- n)) is V11() real ext-real set
r to_power ((- n) - n) is V11() real ext-real set
r #Z (- n) is V11() real ext-real set
(r #Z (- n)) * (r to_power (- n)) is V11() real ext-real set
r #Z (- n) is V11() real ext-real set
(r #Z (- n)) * (r #Z (- n)) is V11() real ext-real set
(- n) + (- n) is V11() real integer ext-real non positive set
r #Z ((- n) + (- n)) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
2 * n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered even bounded_below Element of NAT
- (2 * n) is V11() real integer ext-real non positive set
(- 1) to_power (- (2 * n)) is V11() real ext-real set
(- 1) * (2 * n) is V11() real integer ext-real non positive even set
(- 1) #Z ((- 1) * (2 * n)) is V11() real ext-real set
(- 1) #Z (- 1) is V11() real ext-real set
((- 1) #Z (- 1)) #Z (2 * n) is V11() real ext-real set
(- 1) #Z 1 is V11() real ext-real set
1 / ((- 1) #Z 1) is V11() real ext-real set
(1 / ((- 1) #Z 1)) #Z (2 * n) is V11() real ext-real set
1 / (- 1) is V11() real ext-real non positive set
(1 / (- 1)) #Z (2 * n) is V11() real ext-real set
(- 1) |^ (2 * n) is V11() real ext-real set
1 |^ (2 * n) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
1 |^ 2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(1 |^ 2) |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of REAL
1 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
- n is V11() real integer ext-real non positive set
n is non empty V11() real ext-real set
n to_power n is V11() real ext-real set
n to_power (- n) is V11() real ext-real set
(n to_power n) * (n to_power (- n)) is V11() real ext-real set
n #Z n is V11() real ext-real set
(n #Z n) * (n to_power (- n)) is V11() real ext-real set
n #Z (- n) is V11() real ext-real set
(n #Z n) * (n #Z (- n)) is V11() real ext-real set
n + (- n) is V11() real integer ext-real set
n #Z (n + (- n)) is V11() real ext-real set
n is non empty V11() real integer ext-real non even set
- n is V11() real integer ext-real set
2 * (- 1) is V11() real integer ext-real non positive even set
(2 * (- 1)) + 1 is non empty V11() real integer ext-real non even set
n is non empty V11() real integer ext-real non even set
n * n is non empty V11() real integer ext-real non even set
n is V11() real integer ext-real even set
- n is V11() real integer ext-real set
n is V11() real integer ext-real set
n * n is V11() real integer ext-real even set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
- n is V11() real integer ext-real non positive set
(- 1) to_power (- n) is V11() real ext-real set
(- 1) to_power n is V11() real ext-real set
n is non empty V11() real integer ext-real non even set
- n is non empty V11() real integer ext-real non even set
(- 1) to_power (- n) is V11() real ext-real set
(- 1) to_power n is V11() real ext-real set
n is V11() real integer ext-real even set
- n is V11() real integer ext-real even set
(- 1) to_power (- n) is V11() real ext-real set
(- 1) to_power n is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
C * C is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n * r is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(C * C) + (n * r) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
{1} is non empty finite with_non-empty_elements non empty-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
n is non empty finite with_non-empty_elements non empty-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
bool [:NAT,NAT:] is set
n is Relation-like NAT -defined NAT -valued Function-like V29( NAT , NAT ) V76() V77() V78() V79() Element of bool [:NAT,NAT:]
n is finite with_non-empty_elements complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded set
n | n is Relation-like n -defined NAT -defined NAT -valued RAT -valued Function-like finite V76() V77() V78() V79() set
C is non empty finite with_non-empty_elements non empty-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
max C is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative set
dom (n | n) is finite set
C is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
Seg C is finite C -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= C ) } is set
r is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
RR is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n is Relation-like NAT -defined Function-like FinSubsequence-like set
Seq n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom n is set
Sgm (dom n) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V76() V77() V78() V79() FinSequence of NAT
(Sgm (dom n)) (#) n is Relation-like NAT -defined Function-like finite set
rng (Seq n) is finite set
rng n is set
n is Relation-like NAT -defined NAT -valued Function-like V29( NAT , NAT ) V76() V77() V78() V79() Element of bool [:NAT,NAT:]
n is finite with_non-empty_elements complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded set
n | n is Relation-like n -defined NAT -defined NAT -valued RAT -valued Function-like finite FinSubsequence-like V76() V77() V78() V79() set
Seq (n | n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (n | n) is finite set
Sgm (dom (n | n)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V76() V77() V78() V79() FinSequence of NAT
(Sgm (dom (n | n))) (#) (n | n) is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite V76() V77() V78() V79() set
rng (Seq (n | n)) is finite set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
C is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
C + n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n + C is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n + C is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n + C) - n is V11() real integer ext-real set
n - n is V11() real integer ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
C is set
[n,C] is set
{n,C} is non empty finite set
{n} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
{{n,C},{n}} is non empty finite V40() with_non-empty_elements non empty-membered set
C is set
[n,C] is set
{n,C} is non empty finite set
{n} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
{{n,C},{n}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[n,C],[n,C]} is non empty Relation-like finite set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
k is set
{n,n} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
Seg n is finite n -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
r is Relation-like Function-like set
dom r is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
C is set
[n,C] is set
{n,C} is non empty finite set
{n} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
{{n,C},{n}} is non empty finite V40() with_non-empty_elements non empty-membered set
C is set
[n,C] is set
{n,C} is non empty finite set
{n} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
{{n,C},{n}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[n,C],[n,C]} is non empty Relation-like finite set
<*C,C*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*C*> is non empty Relation-like NAT -defined Function-like finite 1 -element FinSequence-like FinSubsequence-like set
[1,C] is set
{1,C} is non empty finite set
{{1,C},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,C]} is non empty Relation-like Function-like finite set
<*C*> is non empty Relation-like NAT -defined Function-like finite 1 -element FinSequence-like FinSubsequence-like set
[1,C] is set
{1,C} is non empty finite set
{{1,C},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,C]} is non empty Relation-like Function-like finite set
<*C*> ^ <*C*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
r is Relation-like NAT -defined Function-like FinSubsequence-like set
Seq r is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom r is set
Sgm (dom r) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V76() V77() V78() V79() FinSequence of NAT
(Sgm (dom r)) (#) r is Relation-like NAT -defined Function-like finite set
(n,n) --> (C,C) is finite set
{n,n} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
Seg k is finite k -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= k ) } is set
<*n,n*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*n*> is non empty Relation-like NAT -defined Function-like finite 1 -element FinSequence-like FinSubsequence-like set
[1,n] is set
{1,n} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
{{1,n},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,n]} is non empty Relation-like Function-like finite set
<*n*> is non empty Relation-like NAT -defined Function-like finite 1 -element FinSequence-like FinSubsequence-like set
[1,n] is set
{1,n} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
{{1,n},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,n]} is non empty Relation-like Function-like finite set
<*n*> ^ <*n*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<*n,n*> (#) r is Relation-like NAT -defined Function-like finite set
r . n is set
r . n is set
<*(r . n),(r . n)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*(r . n)*> is non empty Relation-like NAT -defined Function-like finite 1 -element FinSequence-like FinSubsequence-like set
[1,(r . n)] is set
{1,(r . n)} is non empty finite set
{{1,(r . n)},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,(r . n)]} is non empty Relation-like Function-like finite set
<*(r . n)*> is non empty Relation-like NAT -defined Function-like finite 1 -element FinSequence-like FinSubsequence-like set
[1,(r . n)] is set
{1,(r . n)} is non empty finite set
{{1,(r . n)},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,(r . n)]} is non empty Relation-like Function-like finite set
<*(r . n)*> ^ <*(r . n)*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
<*C,(r . n)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*C*> ^ <*(r . n)*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
Seg n is finite n -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
n is with_non-empty_elements set
bool n is set
n is Element of bool n
n is with_non-empty_elements set
n is set
n /\ n is set
bool n is set
C is with_non-empty_elements Element of bool n
n /\ n is with_non-empty_elements set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n is set
[n,n] is set
{n,n} is non empty finite set
{n} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
{{n,n},{n}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[n,n]} is non empty Relation-like Function-like finite set
C is Relation-like Function-like set
dom C is set
{n} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
Seg n is finite n -element with_non-empty_elements complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
C is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
1 + n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
n is set
[1,n] is set
{1,n} is non empty finite set
{{1,n},{1}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[1,n]} is non empty Relation-like Function-like finite set
[(1 + n),n] is set
{(1 + n),n} is non empty finite set
{(1 + n)} is non empty finite with_non-empty_elements non empty-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
{{(1 + n),n},{(1 + n)}} is non empty finite V40() with_non-empty_elements non empty-membered set
{[(1 + n),n]} is non empty Relation-like Function-like finite set
C is Relation-like NAT -defined Function-like FinSubsequence-like set
n Shift C is Relation-like NAT -defined Function-like FinSubsequence-like set
card C is cardinal set
card (n Shift C) is cardinal set
dom C is set
{1} is non empty finite with_non-empty_elements non empty-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
dom (n Shift C) is set
{(1 + n)} is non empty finite with_non-empty_elements non empty-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
r is set
{ (n + b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : b1 in dom C } is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
r is set
(n Shift C) . (1 + n) is set
C . 1 is set
r is set
{r} is non empty finite set
n is Relation-like NAT -defined Function-like FinSubsequence-like set
dom n is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
Seg n is finite n -element with_non-empty_elements complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
C is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
Seg C is finite C -element with_non-empty_elements complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= C ) } is set
id (Seg C) is Relation-like Seg C -defined Seg C -valued RAT -valued INT -valued Function-like one-to-one V76() V77() V78() V79() set
C is Relation-like Function-like set
C +* n is Relation-like Function-like set
dom (C +* n) is set
dom C is set
(dom C) \/ (dom n) is set
(Seg C) \/ (dom n) is set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined Function-like FinSubsequence-like set
dom n is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
Seg n is finite n -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
id (Seg n) is Relation-like Seg n -defined Seg n -valued RAT -valued INT -valued Function-like one-to-one V76() V77() V78() V79() set
C is Relation-like Function-like set
C +* n is Relation-like Function-like set
dom (C +* n) is set
dom C is set
(dom C) \/ (dom n) is set
(Seg n) \/ (dom n) is set
r is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
(n + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
n is non empty non trivial epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative non empty-membered set
n - 1 is V11() real integer ext-real set
1 - 1 is V11() real integer ext-real set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib 2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
(0 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib ((0 + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
Fib 3 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
(1 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib ((1 + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
Fib 4 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
(2 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib ((2 + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
Fib n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib n) + (Fib (n + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
Fib n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib n) + (Fib (n + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib ((n + 1) + 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib ((n + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib (n + 1)) + (Fib ((n + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n + 2) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib ((n + 2) + 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib ((n + 2) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib (n + 2)) + (Fib ((n + 2) + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n + 2) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib ((n + 2) + 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
((n + 2) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (((n + 2) + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
Fib ((n + 2) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib (n + 2)) + (Fib ((n + 2) + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (0 + 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
(0 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib ((0 + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib 0) + (Fib 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (0 + 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib 0) + (Fib (0 + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (1 + 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib 1) + (Fib (1 + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 3) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib (n + 2)) + (Fib (n + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib ((n + 1) + 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib ((n + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib ((n + 1) + 1)) + (Fib (n + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 4) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 3) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib (n + 2)) + (Fib (n + 3)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
((n + 2) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (((n + 2) + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
Fib ((n + 2) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib (n + 2)) + (Fib ((n + 2) + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n + 5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 5) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 3) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 4) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib (n + 3)) + (Fib (n + 4)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(n + 3) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
((n + 3) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (((n + 3) + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
Fib ((n + 3) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib (n + 3)) + (Fib ((n + 3) + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
2 * (n + 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered even bounded_below Element of NAT
(2 * (n + 2)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non even left_end bounded_below Element of NAT
Fib ((2 * (n + 2)) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
2 * n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered even bounded_below Element of NAT
(2 * n) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib ((2 * n) + 3) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(2 * n) + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib ((2 * n) + 4) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib ((2 * n) + 3)) + (Fib ((2 * n) + 4)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(2 * n) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered even left_end bounded_below Element of NAT
((2 * n) + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non even left_end bounded_below Element of NAT
Fib (((2 * n) + 2) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(((2 * n) + 2) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered even left_end bounded_below Element of NAT
Fib ((((2 * n) + 2) + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib (((2 * n) + 2) + 1)) + (Fib ((((2 * n) + 2) + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 2) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 3) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (n + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib (n + 3)) - (Fib (n + 1)) is V11() real integer ext-real set
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
((n + 1) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
Fib (((n + 1) + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(Fib (n + 1)) + (Fib (n + 2)) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V47() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11()