:: RECDEF_1 semantic presentation

REAL is non empty non trivial V38() set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V38() V43() V44() Element of bool REAL

bool REAL is non empty non trivial V38() set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V38() V43() V44() set

bool NAT is non empty non trivial V38() set

bool NAT is non empty non trivial V38() set

RAT is non empty non trivial V38() set

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() V37() V38() V39() V42() V43() V45( {} ) FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued set

1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

INT is non empty non trivial V38() set

2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() V37() V38() V39() V42() V43() V45( {} ) FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued Element of NAT

Seg 1 is non empty trivial V38() V45(1) Element of bool NAT

00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f is non empty set

g is Relation-like NAT -defined f -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of f

len g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g . 00 is set

Seg (len g) is V38() V45( len g) Element of bool NAT

dom g is V38() Element of bool NAT

proj2 g is V38() set

00 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

f is set

00 . f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

F

00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f is set

the_rank_of f is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of f) is set

bool (Rank (the_rank_of f)) is non empty set

g is set

p is set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n is set

the_rank_of n is epsilon-transitive epsilon-connected ordinal set

k is epsilon-transitive epsilon-connected ordinal set

the_rank_of k is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of k) is set

the_rank_of (the_rank_of n) is epsilon-transitive epsilon-connected ordinal set

p is Relation-like Function-like set

proj1 p is set

proj2 p is set

sup (proj2 p) is epsilon-transitive epsilon-connected ordinal set

p is epsilon-transitive epsilon-connected ordinal set

the_rank_of p is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of p) is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . n is set

the_rank_of (p . n) is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of (p . n)) is set

k is set

n is epsilon-transitive epsilon-connected ordinal set

Rank n is set

Rank p is set

g is Relation-like Function-like set

proj1 g is set

proj2 g is set

sup (proj2 g) is epsilon-transitive epsilon-connected ordinal set

p is epsilon-transitive epsilon-connected ordinal set

Rank p is set

p is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g . p is set

the_rank_of (g . p) is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of (g . p)) is set

k is set

n is epsilon-transitive epsilon-connected ordinal set

Rank n is set

the_rank_of n is epsilon-transitive epsilon-connected ordinal set

p is epsilon-transitive epsilon-connected ordinal set

Rank p is set

00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f is set

g is set

the_rank_of f is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of f) is set

p is set

p is epsilon-transitive epsilon-connected ordinal set

Rank p is set

p is epsilon-transitive epsilon-connected ordinal set

Rank p is set

n is epsilon-transitive epsilon-connected ordinal set

Rank n is set

n is epsilon-transitive epsilon-connected ordinal set

Rank n is set

the_rank_of F

{ b

00 is Relation-like Function-like set

proj1 00 is set

f is Relation-like Function-like set

proj1 f is set

00 . 0 is set

f . 0 is set

g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

{ b

g + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

{ b

00 . g is set

f . g is set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . p is set

f . p is set

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . (p + 1) is set

f . (p + 1) is set

the_rank_of (00 . p) is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of (00 . p)) is set

p is epsilon-transitive epsilon-connected ordinal set

Rank p is set

n is epsilon-transitive epsilon-connected ordinal set

Rank n is set

00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

{ b

00 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

{ b

f is Relation-like Function-like set

proj1 f is set

f . 0 is set

f . 00 is set

the_rank_of (f . 00) is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of (f . 00)) is set

g is set

p is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f . p is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f . n is set

00 + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f . n is set

00 + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n is set

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n is set

p is Relation-like Function-like set

proj1 p is set

p . 0 is set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . p is set

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (p + 1) is set

the_rank_of (p . p) is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of (p . p)) is set

f . (p + 1) is set

f . p is set

n is epsilon-transitive epsilon-connected ordinal set

Rank n is set

n is epsilon-transitive epsilon-connected ordinal set

Rank n is set

k is epsilon-transitive epsilon-connected ordinal set

Rank k is set

{ b

H

{(the_rank_of F

[:H

bool [:H

proj1 (H

(H

f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

(H

(H

the_rank_of ((H

Rank (the_rank_of ((H

00 is set

f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

{ b

g is Relation-like Function-like set

proj1 g is set

g . 0 is set

g . f is set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

{ b

g . p is set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g . (p + 1) is set

g . p is set

the_rank_of (g . p) is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of (g . p)) is set

00 is Relation-like Function-like set

proj1 00 is set

f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

{ b

00 . f is set

g is Relation-like Function-like set

proj1 g is set

g . 0 is set

g . f is set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g . (p + 1) is set

g . p is set

the_rank_of (g . p) is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of (g . p)) is set

00 is Relation-like Function-like set

proj1 00 is set

00 is Relation-like Function-like set

proj1 00 is set

00 . 0 is set

{ b

f is Relation-like Function-like set

proj1 f is set

f . 0 is set

f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . f is set

f + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . (f + 1) is set

the_rank_of (00 . f) is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of (00 . f)) is set

{ b

g is Relation-like Function-like set

proj1 g is set

g . 0 is set

g . (f + 1) is set

{ b

p is Relation-like Function-like set

proj1 p is set

p . 0 is set

p . f is set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . p is set

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (p + 1) is set

the_rank_of (p . p) is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of (p . p)) is set

g . p is set

g . (p + 1) is set

the_rank_of (g . p) is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of (g . p)) is set

g . f is set

00 is Relation-like Function-like set

proj1 00 is set

00 . 0 is set

00 is Relation-like Function-like set

proj1 00 is set

00 . 0 is set

[F

{F

{F

{{F

[F

[F

proj2 00 is set

sup (proj2 00) is epsilon-transitive epsilon-connected ordinal set

Rank (sup (proj2 00)) is set

[:(Rank (sup (proj2 00))),NAT:] is Relation-like set

g is set

g `2 is set

g `1 is set

p is set

p is set

[p,p] is V15() set

{p,p} is non empty V38() set

{p} is non empty trivial V38() V45(1) set

{{p,p},{p}} is non empty V38() V42() set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

the_rank_of p is epsilon-transitive epsilon-connected ordinal set

k is epsilon-transitive epsilon-connected ordinal set

n is set

00 . n is set

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . (k + 1) is set

the_rank_of k is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of k) is set

n is epsilon-transitive epsilon-connected ordinal set

Rank n is set

Rank k is set

z is epsilon-transitive epsilon-connected ordinal set

Rank z is set

n is epsilon-transitive epsilon-connected ordinal set

Rank n is set

n is set

n is epsilon-transitive epsilon-connected ordinal set

Rank n is set

Y is set

Y is set

the_rank_of Y is epsilon-transitive epsilon-connected ordinal set

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

[Y,(n + 1)] is V15() set

{Y,(n + 1)} is non empty V38() set

{Y} is non empty trivial V38() V45(1) set

{{Y,(n + 1)},{Y}} is non empty V38() V42() set

u is V15() set

u `1 is set

u `2 is set

the_rank_of (u `1) is epsilon-transitive epsilon-connected ordinal set

i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

i + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

y is set

the_rank_of y is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of y) is set

g is Relation-like Function-like set

proj1 g is set

p is Relation-like Function-like set

proj1 p is set

p . 0 is set

the_rank_of (p . 0) is epsilon-transitive epsilon-connected ordinal set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . p is set

the_rank_of (p . p) is epsilon-transitive epsilon-connected ordinal set

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (p + 1) is set

the_rank_of (p . (p + 1)) is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

[(p . p),p] is V15() set

{(p . p),p} is non empty V38() set

{(p . p)} is non empty trivial V38() V45(1) set

{{(p . p),p},{(p . p)}} is non empty V38() V42() set

k is set

00 . k is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . (n + 1) is set

00 . n is set

the_rank_of (00 . n) is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of (00 . n)) is set

k is epsilon-transitive epsilon-connected ordinal set

Rank k is set

z is set

the_rank_of z is epsilon-transitive epsilon-connected ordinal set

[(p . p),p] `1 is set

[(p . p),p] `2 is set

g . [(p . p),p] is set

(g . [(p . p),p]) `1 is set

(g . [(p . p),p]) `2 is set

the_rank_of ((g . [(p . p),p]) `1) is epsilon-transitive epsilon-connected ordinal set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . p is set

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (p + 1) is set

(p + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . ((p + 1) + 1) is set

the_rank_of (p . (p + 1)) is epsilon-transitive epsilon-connected ordinal set

[(p . (p + 1)),(p + 1)] is V15() set

{(p . (p + 1)),(p + 1)} is non empty V38() set

{(p . (p + 1))} is non empty trivial V38() V45(1) set

{{(p . (p + 1)),(p + 1)},{(p . (p + 1))}} is non empty V38() V42() set

[(p . (p + 1)),(p + 1)] `1 is set

[(p . (p + 1)),(p + 1)] `2 is set

g . [(p . (p + 1)),(p + 1)] is set

(g . [(p . (p + 1)),(p + 1)]) `1 is set

(g . [(p . (p + 1)),(p + 1)]) `2 is set

the_rank_of ((g . [(p . (p + 1)),(p + 1)]) `1) is epsilon-transitive epsilon-connected ordinal set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g . [F

(g . [F

(g . [F

the_rank_of ((g . [F

0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (0 + 1) is set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

F

[:NAT,F

bool [:NAT,F

F

00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f is Element of F

[:[:NAT,F

bool [:[:NAT,F

00 is Relation-like [:NAT,F

F

f is set

union f is set

p is set

p is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

p . 1 is set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . n is set

p . n is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

p . n is set

p . n is set

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

k + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

k + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

k + (1 + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (k + (1 + 1)) is set

p . k is set

[k,(p . k)] is V15() set

{k,(p . k)} is non empty V38() set

{k} is non empty trivial V38() V42() V45(1) set

{{k,(p . k)},{k}} is non empty V38() V42() set

00 . [k,(p . k)] is set

k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (k + 1) is set

[k,(p . (k + 1))] is V15() set

{k,(p . (k + 1))} is non empty V38() set

{{k,(p . (k + 1))},{k}} is non empty V38() V42() set

00 . [k,(p . (k + 1))] is set

z is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

z . 1 is set

len z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

z is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

z . 1 is set

len z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

k is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

k . 1 is set

len k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

n . 1 is set

len n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n is set

dom p is V38() Element of bool NAT

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

p . k is set

[k,(p . k)] is V15() set

{k,(p . k)} is non empty V38() set

{k} is non empty trivial V38() V42() V45(1) set

{{k,(p . k)},{k}} is non empty V38() V42() set

Seg (len p) is V38() V45( len p) Element of bool NAT

Seg (len p) is V38() V45( len p) Element of bool NAT

dom p is V38() Element of bool NAT

p . k is set

[k,(p . k)] is V15() set

{k,(p . k)} is non empty V38() set

{{k,(p . k)},{k}} is non empty V38() V42() set

p is set

p is set

[p,p] is V15() set

{p,p} is non empty V38() set

{p} is non empty trivial V38() V45(1) set

{{p,p},{p}} is non empty V38() V42() set

n is set

[p,n] is V15() set

{p,n} is non empty V38() set

{{p,n},{p}} is non empty V38() V42() set

k is set

k is set

n is Relation-like NAT -defined F

len n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

z is Relation-like NAT -defined F

len z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p is Relation-like Function-like set

p is set

n is set

[p,n] is V15() set

{p,n} is non empty V38() set

{p} is non empty trivial V38() V45(1) set

{{p,n},{p}} is non empty V38() V42() set

k is set

n is Relation-like NAT -defined F

dom n is V38() Element of bool NAT

p is set

n is set

k is set

[n,k] is V15() set

{n,k} is non empty V38() set

{n} is non empty trivial V38() V45(1) set

{{n,k},{n}} is non empty V38() V42() set

n is set

k is Relation-like NAT -defined F

n is set

k is set

[n,k] is V15() set

{n,k} is non empty V38() set

{n} is non empty trivial V38() V45(1) set

{{n,k},{n}} is non empty V38() V42() set

p is Relation-like Function-like set

p is Relation-like Function-like set

proj2 p is set

p is set

proj1 p is set

n is set

p . n is set

[n,p] is V15() set

{n,p} is non empty V38() set

{n} is non empty trivial V38() V45(1) set

{{n,p},{n}} is non empty V38() V42() set

k is set

n is Relation-like NAT -defined F

dom n is V38() Element of bool NAT

n . n is set

proj2 n is V38() set

proj1 p is set

[:(proj1 p),F

bool [:(proj1 p),F

p is Relation-like proj1 p -defined F

proj1 p is set

<*F

len <*F

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

<*F

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

<*F

[n,(<*F

{n,(<*F

{n} is non empty trivial V38() V42() V45(1) set

{{n,(<*F

00 . [n,(<*F

1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n + (1 + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

<*F

[1,F

{1,F

{1} is non empty trivial V38() V42() V45(1) set

{{1,F

{[1,F

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

(n + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (n + 1) is set

[(n + 1),(p . (n + 1))] is V15() set

{(n + 1),(p . (n + 1))} is non empty V38() set

{(n + 1)} is non empty trivial V38() V42() V45(1) set

{{(n + 1),(p . (n + 1))},{(n + 1)}} is non empty V38() V42() set

k is set

n is Relation-like NAT -defined F

len n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n . (n + 1) is set

[n,(n . (n + 1))] is V15() set

{n,(n . (n + 1))} is non empty V38() set

{n} is non empty trivial V38() V42() V45(1) set

{{n,(n . (n + 1))},{n}} is non empty V38() V42() set

00 . [n,(n . (n + 1))] is set

<*(00 . [n,(n . (n + 1))])*> is Relation-like NAT -defined Function-like constant non empty trivial V38() V45(1) FinSequence-like FinSubsequence-like set

n ^ <*(00 . [n,(n . (n + 1))])*> is Relation-like NAT -defined Function-like non empty V38() FinSequence-like FinSubsequence-like set

Seg (len n) is V38() V45( len n) Element of bool NAT

dom n is V38() Element of bool NAT

len (n ^ <*(00 . [n,(n . (n + 1))])*>) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

z + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

(n ^ <*(00 . [n,(n . (n + 1))])*>) . (z + 2) is set

z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

(n ^ <*(00 . [n,(n . (n + 1))])*>) . (z + 1) is set

[z,((n ^ <*(00 . [n,(n . (n + 1))])*>) . (z + 1))] is V15() set

{z,((n ^ <*(00 . [n,(n . (n + 1))])*>) . (z + 1))} is non empty V38() set

{z} is non empty trivial V38() V42() V45(1) set

{{z,((n ^ <*(00 . [n,(n . (n + 1))])*>) . (z + 1))},{z}} is non empty V38() V42() set

00 . [z,((n ^ <*(00 . [n,(n . (n + 1))])*>) . (z + 1))] is set

len <*(00 . [n,(n . (n + 1))])*> is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

(len n) + (len <*(00 . [n,(n . (n + 1))])*>) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

(len n) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

(z + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

z + (1 + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n . (z + 2) is set

n . (z + 1) is set

[z,(n . (z + 1))] is V15() set

{z,(n . (z + 1))} is non empty V38() set

{{z,(n . (z + 1))},{z}} is non empty V38() V42() set

00 . [z,(n . (z + 1))] is set

n is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

n . 1 is set

len n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

(z + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

(z + 2) - 1 is ext-real V36() V37() Element of REAL

(z + 2) - ((z + 2) - 1) is ext-real V36() V37() Element of REAL

<*(00 . [n,(n . (n + 1))])*> . ((z + 2) - ((z + 2) - 1)) is set

n . (z + 1) is set

[z,(n . (z + 1))] is V15() set

{z,(n . (z + 1))} is non empty V38() set

{{z,(n . (z + 1))},{z}} is non empty V38() V42() set

00 . [z,(n . (z + 1))] is set

proj2 n is V38() set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

z is Element of F

[n,z] is V15() Element of [:NAT,F

{n,z} is non empty V38() set

{n} is non empty trivial V38() V42() V45(1) set

{{n,z},{n}} is non empty V38() V42() set

00 . [n,z] is Element of F

<*(00 . [n,z])*> is Relation-like NAT -defined F

n ^ <*(00 . [n,z])*> is Relation-like NAT -defined F

len <*(00 . [n,(n . (n + 1))])*> is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

(len n) + (len <*(00 . [n,(n . (n + 1))])*>) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

Seg (len (n ^ <*(00 . [n,(n . (n + 1))])*>)) is non empty V38() V45( len (n ^ <*(00 . [n,(n . (n + 1))])*>)) Element of bool NAT

dom (n ^ <*(00 . [n,(n . (n + 1))])*>) is non empty V38() Element of bool NAT

(n ^ <*(00 . [n,(n . (n + 1))])*>) . ((n + 1) + 1) is set

[((n + 1) + 1),((n ^ <*(00 . [n,(n . (n + 1))])*>) . ((n + 1) + 1))] is V15() set

{((n + 1) + 1),((n ^ <*(00 . [n,(n . (n + 1))])*>) . ((n + 1) + 1))} is non empty V38() set

{((n + 1) + 1)} is non empty trivial V38() V42() V45(1) set

{{((n + 1) + 1),((n ^ <*(00 . [n,(n . (n + 1))])*>) . ((n + 1) + 1))},{((n + 1) + 1)}} is non empty V38() V42() set

(n ^ <*(00 . [n,(n . (n + 1))])*>) . 1 is set

z is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

z . 1 is set

len z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

dom n is V38() Element of bool NAT

Seg (len n) is V38() V45( len n) Element of bool NAT

n . ((n + 1) + 1) is set

[((n + 1) + 1),(n . ((n + 1) + 1))] is V15() set

{((n + 1) + 1),(n . ((n + 1) + 1))} is non empty V38() set

{((n + 1) + 1)} is non empty trivial V38() V42() V45(1) set

{{((n + 1) + 1),(n . ((n + 1) + 1))},{((n + 1) + 1)}} is non empty V38() V42() set

0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (n + 2) is set

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (n + 1) is set

[n,(p . (n + 1))] is V15() set

{n,(p . (n + 1))} is non empty V38() set

{n} is non empty trivial V38() V42() V45(1) set

{{n,(p . (n + 1))},{n}} is non empty V38() V42() set

00 . [n,(p . (n + 1))] is set

(n + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

[(n + 2),(p . (n + 2))] is V15() set

{(n + 2),(p . (n + 2))} is non empty V38() set

{(n + 2)} is non empty trivial V38() V42() V45(1) set

{{(n + 2),(p . (n + 2))},{(n + 2)}} is non empty V38() V42() set

k is set

n is Relation-like NAT -defined F

dom n is V38() Element of bool NAT

len n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

Seg (len n) is V38() V45( len n) Element of bool NAT

n . (n + 1) is set

[(n + 1),(n . (n + 1))] is V15() set

{(n + 1),(n . (n + 1))} is non empty V38() set

{(n + 1)} is non empty trivial V38() V42() V45(1) set

{{(n + 1),(n . (n + 1))},{(n + 1)}} is non empty V38() V42() set

n . (n + 2) is set

[n,(n . (n + 1))] is V15() set

{n,(n . (n + 1))} is non empty V38() set

{{n,(n . (n + 1))},{n}} is non empty V38() V42() set

00 . [n,(n . (n + 1))] is set

k is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

k . 1 is set

len k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n is set

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (k + 1) is set

n is Relation-like Function-like set

proj1 n is set

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n . k is set

k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (k + 1) is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (n + 1) is set

n is Relation-like Function-like set

proj1 n is set

n is Relation-like Function-like set

proj1 n is set

proj2 n is set

k is set

n is set

n . n is set

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (k + 1) is set

proj2 p is set

k is Relation-like NAT -defined F

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

k . n is Element of F

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (n + 1) is set

n is Relation-like NAT -defined F

n is Relation-like NAT -defined F

<*F

len <*F

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

k + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

<*F

k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

<*F

[k,(<*F

{k,(<*F

{k} is non empty trivial V38() V42() V45(1) set

{{k,(<*F

00 . [k,(<*F

(k + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

0 + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

<*F

[1,F

{1,F

{1} is non empty trivial V38() V42() V45(1) set

{{1,F

{[1,F

n . 0 is Element of F

0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (0 + 1) is set

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n . k is Element of F

k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n . (k + 1) is Element of F

1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

k + (1 + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (k + (1 + 1)) is set

p . (k + 1) is set

00 . (k,(p . (k + 1))) is set

[k,(p . (k + 1))] is V15() set

{k,(p . (k + 1))} is non empty V38() set

{k} is non empty trivial V38() V42() V45(1) set

{{k,(p . (k + 1))},{k}} is non empty V38() V42() set

00 . [k,(p . (k + 1))] is set

00 . (k,(n . k)) is Element of F

[k,(n . k)] is V15() set

{k,(n . k)} is non empty V38() set

{{k,(n . k)},{k}} is non empty V38() V42() set

00 . [k,(n . k)] is set

(k + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . ((k + 1) + 1) is set

F

F

F

00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f is set

g is set

g is set

00 is Relation-like Function-like set

proj1 00 is set

00 . 0 is set

f is set

g is ext-real V36() V37() Element of REAL

g - 1 is ext-real V36() V37() Element of REAL

00 . (g - 1) is set

p is ext-real V36() V37() Element of REAL

p - 1 is ext-real V36() V37() Element of REAL

00 . (p - 1) is set

f is Relation-like Function-like set

proj1 f is set

Seg F

f | (Seg F

proj1 (f | (Seg F

g is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g . 1 is set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f . 1 is set

1 - 1 is ext-real V36() V37() Element of REAL

00 . (1 - 1) is set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g . p is set

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g . (p + 1) is set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g . (n + 1) is set

00 . n is set

f . (n + 1) is set

(n + 1) - 1 is ext-real V36() V37() Element of REAL

00 . ((n + 1) - 1) is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . n is set

00 . (n + 1) is set

(n + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g . ((n + 1) + 1) is set

F

F

F

the Element of F

F

f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g is Element of F

p is Element of F

p is Element of F

[:NAT,F

bool [:NAT,F

f is Relation-like NAT -defined F

f . 0 is Element of F

g is set

p is ext-real V36() V37() Element of REAL

p - 1 is ext-real V36() V37() Element of REAL

f . (p - 1) is set

p is ext-real V36() V37() Element of REAL

p - 1 is ext-real V36() V37() Element of REAL

f . (p - 1) is set

g is Relation-like Function-like set

proj1 g is set

Seg F

g | (Seg F

proj1 (g | (Seg F

p is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

proj2 p is V38() set

p is set

dom p is V38() Element of bool NAT

n is set

p . n is set

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

k - 1 is ext-real V36() V37() Element of REAL

f . (k - 1) is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f . k is Element of F

p . k is set

g . k is set

p is Relation-like NAT -defined F

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . 1 is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g . 1 is set

1 - 1 is ext-real V36() V37() Element of REAL

f . (1 - 1) is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . n is set

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (n + 1) is set

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (n + 1) is set

f . n is Element of F

g . (n + 1) is set

(n + 1) - 1 is ext-real V36() V37() Element of REAL

f . ((n + 1) - 1) is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f . n is Element of F

f . (n + 1) is Element of F

(n + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . ((n + 1) + 1) is set

F

len F

F

00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

F

f is set

00 is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len 00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . 1 is set

00 . (len 00) is set

f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

F

00 . f is set

00 . (f + 1) is set

F

F

f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

F

F

f is set

g is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g . (len g) is set

g . 1 is set

p is set

p is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (len p) is set

p . 1 is set

F

len F

F

00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

F

f is set

F

00 is set

f is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f . (len f) is set

f . 1 is set

f is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f . (len f) is set

f . 1 is set

g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f . (g + 1) is set

F

f . g is set

F

F

F

len F

F

F

F

len F

F

dom F

Seg (len F

dom F

00 is set

F

F

Seg (len F

f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

F

F

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

F

F

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

F

F

F

F

F

len F

F

F

F

len F

F

dom F

Seg (len F

dom F

00 is set

F

F

Seg (len F

f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

F

F

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

F

F

F

k is Element of F

n is Element of F

F

n is Element of F

F

len F

F

F

F

00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

F

f is set

g is set

p is set

00 is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len 00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . (len 00) is set

00 . 1 is set

00 is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len 00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . (len 00) is set

00 . 1 is set

f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

F

00 . f is set

00 . (f + 1) is set

f is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f . (len f) is set

f . 1 is set

f is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f . (len f) is set

f . 1 is set

g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

g + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

F

f . g is set

f . (g + 1) is set

F

F

len F

F

F

00 is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len 00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . (len 00) is set

00 . 1 is set

00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p is set

00 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

F

g is set

f is set

F

p is set

00 is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set

len 00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . (len 00) is set

00 . 1 is set

F

F

00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f is set

00 is Relation-like Function-like set

proj1 00 is set

00 . 0 is set

f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

g is set

p is set

p is set

00 . F

f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . f is set

f + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

00 . (f + 1) is set

f is set

g is set

p is Relation-like Function-like set

p . F

proj1 p is set

p . 0 is set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

p . p is set

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (p + 1) is set

p is Relation-like Function-like set

p . F

proj1 p is set

p . 0 is set

n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set

p . n is set

n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

p . (n + 1) is set

F

F

00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f is set

F

g is set

F

00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT

f is set

g is set

p is set

F

00 is set

f is Relation-like<