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
F1() is set
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 F1() is epsilon-transitive epsilon-connected ordinal set
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT : b1 <= a1 } is set
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
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT : b1 <= g } is set
g + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT : b1 <= g + 1 } is set
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
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT : b1 <= 00 } 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
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT : b1 <= 00 + 1 } is set
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
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT : b1 <= 0 } is set
H1( 0 ) --> (the_rank_of F1()) is Relation-like H1( 0 ) -defined {(the_rank_of F1())} -valued Function-like V18(H1( 0 ),{(the_rank_of F1())}) Element of bool [:H1( 0 ),{(the_rank_of F1())}:]
{(the_rank_of F1())} is non empty trivial V38() V45(1) set
[:H1( 0 ),{(the_rank_of F1())}:] is Relation-like set
bool [:H1( 0 ),{(the_rank_of F1())}:] is non empty set
proj1 (H1( 0 ) --> (the_rank_of F1())) is set
(H1( 0 ) --> (the_rank_of F1())) . 0 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
(H1( 0 ) --> (the_rank_of F1())) . (f + 1) is set
(H1( 0 ) --> (the_rank_of F1())) . f is set
the_rank_of ((H1( 0 ) --> (the_rank_of F1())) . f) is epsilon-transitive epsilon-connected ordinal set
Rank (the_rank_of ((H1( 0 ) --> (the_rank_of F1())) . f)) is set
00 is set
f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT : b1 <= 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
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT : b1 <= p } is set
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
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT : b1 <= f } is set
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
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT : b1 <= 0 } is set
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
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT : b1 <= f + 1 } is set
g is Relation-like Function-like set
proj1 g is set
g . 0 is set
g . (f + 1) is set
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT : b1 <= f } is set
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
[F1(),0] is V15() set
{F1(),0} is non empty V38() set
{F1()} is non empty trivial V38() V45(1) set
{{F1(),0},{F1()}} is non empty V38() V42() set
[F1(),0] `1 is set
[F1(),0] `2 is set
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 . [F1(),0] is set
(g . [F1(),0]) `1 is set
(g . [F1(),0]) `2 is set
the_rank_of ((g . [F1(),0]) `1) is epsilon-transitive epsilon-connected ordinal set
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
F1() is non empty set
[:NAT,F1():] is Relation-like non empty non trivial V38() set
bool [:NAT,F1():] is non empty non trivial V38() set
F2() is Element of F1()
00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
f is Element of F1()
[:[:NAT,F1():],F1():] is Relation-like non empty non trivial V38() set
bool [:[:NAT,F1():],F1():] is non empty non trivial V38() set
00 is Relation-like [:NAT,F1():] -defined F1() -valued Function-like V18([:NAT,F1():],F1()) Element of bool [:[:NAT,F1():],F1():]
F1() * is functional non empty FinSequence-membered set
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 F1() -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of F1()
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 F1() -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of F1()
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 F1() -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of F1()
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 F1() -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of F1()
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 F1() -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of F1()
dom n is V38() Element of bool NAT
n . n is set
proj2 n is V38() set
proj1 p is set
[:(proj1 p),F1():] is Relation-like set
bool [:(proj1 p),F1():] is non empty set
p is Relation-like proj1 p -defined F1() -valued Function-like V18( proj1 p,F1()) Element of bool [:(proj1 p),F1():]
proj1 p is set
<*F2()*> is Relation-like NAT -defined F1() -valued Function-like constant non empty trivial V38() V45(1) FinSequence-like FinSubsequence-like FinSequence of F1()
len <*F2()*> 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
<*F2()*> . (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
<*F2()*> . (n + 1) is set
[n,(<*F2()*> . (n + 1))] is V15() set
{n,(<*F2()*> . (n + 1))} is non empty V38() set
{n} is non empty trivial V38() V42() V45(1) set
{{n,(<*F2()*> . (n + 1))},{n}} is non empty V38() V42() set
00 . [n,(<*F2()*> . (n + 1))] is set
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
<*F2()*> . 1 is set
[1,F2()] is V15() Element of [:NAT,F1():]
{1,F2()} is non empty V38() set
{1} is non empty trivial V38() V42() V45(1) set
{{1,F2()},{1}} is non empty V38() V42() set
{[1,F2()]} is Relation-like NAT -defined F1() -valued Function-like constant non empty trivial V38() V45(1) Element of bool [:NAT,F1():]
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 F1() -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of F1()
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 F1()
[n,z] is V15() Element of [:NAT,F1():]
{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 F1()
<*(00 . [n,z])*> is Relation-like NAT -defined F1() -valued Function-like constant non empty trivial V38() V45(1) FinSequence-like FinSubsequence-like FinSequence of F1()
n ^ <*(00 . [n,z])*> is Relation-like NAT -defined F1() -valued Function-like non empty V38() FinSequence-like FinSubsequence-like FinSequence of F1()
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 F1() -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of F1()
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 F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
k . n is Element of F1()
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 F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
n is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
<*F2()*> is Relation-like NAT -defined F1() -valued Function-like constant non empty trivial V38() V45(1) FinSequence-like FinSubsequence-like FinSequence of F1()
len <*F2()*> 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
<*F2()*> . (k + 2) 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
<*F2()*> . (k + 1) is set
[k,(<*F2()*> . (k + 1))] is V15() set
{k,(<*F2()*> . (k + 1))} is non empty V38() set
{k} is non empty trivial V38() V42() V45(1) set
{{k,(<*F2()*> . (k + 1))},{k}} is non empty V38() V42() set
00 . [k,(<*F2()*> . (k + 1))] 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
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
<*F2()*> . 1 is set
[1,F2()] is V15() Element of [:NAT,F1():]
{1,F2()} is non empty V38() set
{1} is non empty trivial V38() V42() V45(1) set
{{1,F2()},{1}} is non empty V38() V42() set
{[1,F2()]} is Relation-like NAT -defined F1() -valued Function-like constant non empty trivial V38() V45(1) Element of bool [:NAT,F1():]
n . 0 is Element of F1()
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 F1()
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 F1()
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 F1()
[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
F2() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set
F1() is set
F2() - 1 is ext-real V36() V37() Element of REAL
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 F2() is V38() V45(F2()) Element of bool NAT
f | (Seg F2()) is Relation-like Function-like V38() set
proj1 (f | (Seg F2())) is V38() 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 . 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
F1() is non empty set
F3() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set
F2() is Element of F1()
the Element of F1() is Element of F1()
F3() - 1 is ext-real V36() V37() Element of REAL
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 F1()
p is Element of F1()
p is Element of F1()
[:NAT,F1():] is Relation-like non empty non trivial V38() set
bool [:NAT,F1():] is non empty non trivial V38() set
f is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
f . 0 is Element of F1()
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 F3() is V38() V45(F3()) Element of bool NAT
g | (Seg F3()) is Relation-like Function-like V38() set
proj1 (g | (Seg F3())) is V38() set
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 F1()
p . k is set
g . k is set
p is Relation-like NAT -defined F1() -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of F1()
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 F1()
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 F1()
f . (n + 1) is Element of F1()
(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
F1() is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set
len F1() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
F1() . 1 is set
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
F1() . (00 + 1) is set
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
F1() . (f + 1) is set
00 . f is set
00 . (f + 1) is set
F1() . 0 is set
F1() . (len F1()) 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
F1() . (f + 1) is set
F1() . f is set
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
F1() is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set
len F1() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
F1() . 1 is set
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
F1() . (00 + 1) is set
f is set
F2((F1() . (00 + 1)),f) is set
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
F1() . (g + 1) is set
f . g is set
F2((F1() . (g + 1)),(f . g)) is set
F2() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set
F3() is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set
len F3() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
F3() . 1 is set
F1() is set
F4() is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set
len F4() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
F4() . 1 is set
dom F3() is V38() Element of bool NAT
Seg (len F4()) is V38() V45( len F4()) Element of bool NAT
dom F4() is V38() Element of bool NAT
00 is set
F3() . 00 is set
F4() . 00 is set
Seg (len F3()) is V38() V45( len F3()) Element of bool NAT
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
F3() . g is set
F4() . g 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
p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
F3() . p is set
F4() . 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
F4() . (p + 1) is set
F3() . (p + 1) is set
F1() is non empty set
F3() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set
F4() is Relation-like NAT -defined F1() -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of F1()
len F4() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
F4() . 1 is set
F2() is Element of F1()
F5() is Relation-like NAT -defined F1() -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of F1()
len F5() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
F5() . 1 is set
dom F4() is V38() Element of bool NAT
Seg (len F5()) is V38() V45( len F5()) Element of bool NAT
dom F5() is V38() Element of bool NAT
00 is set
F4() . 00 is set
F5() . 00 is set
Seg (len F4()) is V38() V45( len F4()) Element of bool NAT
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
F4() . g is set
F5() . g 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
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
F5() . (p + 1) is set
F4() . p is set
F5() . p is set
k is Element of F1()
n is Element of F1()
F4() . (p + 1) is set
n is Element of F1()
F1() is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set
len F1() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
F2() is set
F1() . 1 is set
F3() is set
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
F1() . (00 + 1) is set
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
F1() . (f + 1) is set
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
F1() . (g + 1) is set
f . g is set
f . (g + 1) is set
F3() is set
F1() is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set
len F1() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
F1() . 1 is set
F4() 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 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
F1() . (00 + 1) is set
g is set
f is set
F2(p,f) 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
F2() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set
F1() is set
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 . F2() 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
f is set
g is set
p is Relation-like Function-like set
p . F2() is 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() 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 . F2() is set
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
F2() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set
F1() is set
00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
f is set
F3(00,f) is set
g is set
F3(00,g) 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
p is set
F3(00,f) is set
00 is set
f is Relation-like Function-like set
f . F2() is set
proj1 f is set
f . 0 is set
00 is set
f is Relation-like Function-like set
f . F2() is set
proj1 f 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
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 . g is set
F3(g,(f . g)) is set
g is set
p is set
p is Relation-like Function-like set
p . F2() is set
proj1 p is set
p . 0 is set
k 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
F3(n,k) is set
n is Relation-like Function-like set
n . F2() is set
proj1 n is set
n . 0 is set
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
n . (k + 1) is set
F3(k,n) is set
k is set
n is Relation-like Function-like set
n . F2() is set
proj1 n is set
n . 0 is set
F1() is non empty set
[:NAT,F1():] is Relation-like non empty non trivial V38() set
bool [:NAT,F1():] is non empty non trivial V38() set
F3() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set
F2() is Element of F1()
00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
f is Element of F1()
00 is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
00 . 0 is Element of F1()
f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set
g is Element of F1()
p is Element of F1()
p is Element of F1()
f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
00 . f is Element of F1()
00 . F3() is set
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
00 . g is Element of F1()
g + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
00 . (g + 1) is Element of F1()
f is Element of F1()
g is Element of F1()
p is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
p . F3() is set
p . 0 is Element of F1()
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 Element of F1()
p is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
p . F3() is set
p . 0 is Element of F1()
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 Element of F1()
F1() is non empty set
[:NAT,F1():] is Relation-like non empty non trivial V38() set
bool [:NAT,F1():] is non empty non trivial V38() set
F3() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set
F2() is Element of F1()
00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
f is Element of F1()
F4(00,f) is Element of F1()
g is Element of F1()
F4(00,g) is Element of F1()
00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
f is Element of F1()
g is Element of F1()
p is Element of F1()
F4(00,f) is Element of F1()
00 is Element of F1()
f is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
f . F3() is set
f . 0 is Element of F1()
00 is Element of F1()
f is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
f . F3() is set
f . 0 is Element of F1()
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() set
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 Element of F1()
f . g is set
F4(g,(f . g)) is Element of F1()
p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
f . p is Element of F1()
p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
f . (p + 1) is Element of F1()
p is Element of F1()
F4(p,p) is Element of F1()
g is Element of F1()
p is Element of F1()
p is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
p . F3() is set
p . 0 is Element of F1()
k is Element of F1()
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
p . n is Element of F1()
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 Element of F1()
F4(n,k) is Element of F1()
n is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
n . F3() is set
n . 0 is Element of F1()
n is Element of F1()
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
n . k is Element of F1()
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 F1()
F4(k,n) is Element of F1()
k is Element of F1()
n is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
n . F3() is set
n . 0 is Element of F1()
F1() is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set
len F1() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
F1() . 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
F1() . (00 + 1) is set
f is set
g is set
p is set
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
F1() . (00 + 1) is set
f is set
00 is set
f is set
F1() is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set
len F1() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
F1() . 1 is set
00 is set
f is set
F2() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
Seg F2() is V38() V45(F2()) Element of bool NAT
F1() is non empty set
<*> F1() is Relation-like non-empty empty-yielding NAT -defined F1() -valued Function-like one-to-one constant functional empty proper 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 FinSequence of F1()
[:NAT,F1():] is Relation-like non empty non trivial V38() set
dom (<*> F1()) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty proper 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 bool NAT
00 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
(<*> F1()) /. 00 is Element of F1()
00 is non empty set
f is Element of 00
[:00,F1():] is Relation-like non empty set
bool [:00,F1():] is non empty set
f is Relation-like 00 -defined F1() -valued Function-like V18(00,F1()) Element of bool [:00,F1():]
proj1 f is set
g is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set
proj2 g is V38() set
p is set
p is Relation-like NAT -defined F1() -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of F1()
dom p is V38() Element of bool 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 /. p is Element of F1()
p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
p /. p is Element of F1()
F1() is non empty set
F3() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
F3() - 1 is ext-real V36() V37() Element of REAL
F2() is Element of F1()
the Element of F1() is Element of F1()
F3() - 2 is ext-real V36() V37() Element of REAL
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 F1()
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
(F3() - 2) + 1 is ext-real V36() V37() Element of REAL
p is Element of F1()
p is Element of F1()
[:NAT,F1():] is Relation-like non empty non trivial V38() set
bool [:NAT,F1():] is non empty non trivial V38() set
f is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
f . 0 is Element of F1()
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 F3() is V38() V45(F3()) Element of bool NAT
g | (Seg F3()) is Relation-like Function-like V38() set
proj1 (g | (Seg F3())) is V38() set
p is set
p is Relation-like NAT -defined Function-like V38() FinSequence-like FinSubsequence-like set
proj2 p is V38() 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 F1()
p . k is set
g . k is set
p is Relation-like NAT -defined F1() -valued Function-like V38() FinSequence-like FinSubsequence-like FinSequence of F1()
len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() V38() V43() Element of NAT
p /. 1 is Element of F1()
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
p . 1 is set
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 Element of F1()
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 Element of F1()
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 Element of F1()
f . n is Element of F1()
(F3() - 1) + 1 is ext-real V36() V37() Element of REAL
g . (n + 1) is set
(n + 1) - 1 is ext-real V36() V37() Element of REAL
f . ((n + 1) - 1) is set
p . (n + 1) is set
(F3() - 1) - 1 is ext-real V36() V37() Element of REAL
f . k is set
f . (k + 1) is Element of F1()
(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 Element of F1()