:: FIB_NUM2 semantic presentation

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

{ b

{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

{ b

{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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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 + b

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

{ b

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

{ b

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

{ b

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()