:: QC_LANG1 semantic presentation

REAL is set
NAT is non empty V27() V28() V29() V35() cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
NAT is non empty V27() V28() V29() V35() cardinal limit_cardinal set
bool NAT is non empty V35() set
bool NAT is non empty V35() set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V26() V27() V28() V29() V31() V32() V33() V34() V35() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V26() V27() V28() V29() V31() V32() V33() V34() V35() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V26() V27() V28() V29() V31() V32() V33() V34() V35() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty ext-real positive V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
2 is non empty ext-real positive V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
3 is non empty ext-real positive V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
Seg 1 is non empty trivial V35() 1 -element Element of bool NAT
{ b₁ where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V26() V27() V28() V29() V31() V32() V33() V34() V35() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
A is non empty set
Y is set
[:A,Y:] is Relation-like set
a is Element of A
{a} is non empty trivial 1 -element set
[:{a},Y:] is Relation-like set
bool A is non empty set
A is non empty set
Y is set
[:A,Y:] is Relation-like set
a is Element of A
k is Element of A
f is Element of A
{a,k,f} is non empty set
[:{a,k,f},Y:] is Relation-like set
bool A is non empty set
[:NAT,NAT:] is Relation-like non empty V35() Element of bool [:REAL,REAL:]
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is non empty set
A is ()
Y is set
[:NAT,Y:] is Relation-like set
A is Relation-like non empty ()
proj2 A is non empty set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is set
[:NAT,Y:] is Relation-like set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
6 is non empty ext-real positive V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
{6} is non empty trivial 1 -element set
[:{6},NAT:] is Relation-like non empty V35() set
4 is non empty ext-real positive V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
5 is non empty ext-real positive V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
{4,5} is non empty set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
A is Relation-like non empty ()
(A) is set
(A) is non empty set
proj2 A is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
{4} is non empty trivial 1 -element set
{5} is non empty trivial 1 -element set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
[:{4},(A):] is Relation-like non empty set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
[:{5},(A):] is Relation-like non empty set
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
[:NAT,(A):] is Relation-like non empty V35() set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
[:{4},(A):] is Relation-like non empty set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
bool (A) is non empty set
[:{5},(A):] is Relation-like non empty set
7 is non empty ext-real positive V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
{ [b₁,b₂] where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b₂ is Element of (A) : 7 <= b₁ } is set
A is Relation-like non empty ()
(A) is Element of bool (A)
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
bool (A) is non empty set
[:{4},(A):] is Relation-like non empty set
(A) is Element of bool (A)
[:{5},(A):] is Relation-like non empty set
(A) is Element of bool (A)
(A) is set
{ [b₁,b₂] where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b₂ is Element of (A) : 7 <= b₁ } is set
[7,0] is V15() set
{7,0} is non empty set
{7} is non empty trivial 1 -element set
{{7,0},{7}} is non empty set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
Y is set
[:NAT,Y:] is Relation-like set
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
{ [b₁,b₂] where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b₂ is Element of (A) : 7 <= b₁ } is set
[:NAT,(A):] is Relation-like non empty V35() set
Y is set
a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k is Element of (A)
[a,k] is V15() set
{a,k} is non empty set
{a} is non empty trivial 1 -element set
{{a,k},{a}} is non empty set
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
{ [b₁,b₂] where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b₂ is Element of (A) : 7 <= b₁ } is set
Y is Element of (A)
Y `1 is set
a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k is Element of (A)
[a,k] is V15() set
{a,k} is non empty set
{a} is non empty trivial 1 -element set
{{a,k},{a}} is non empty set
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal set
7 + f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
7 + a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
7 + k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b<sub>2</sub> is Element of (A) : 7 <= b<sub>1</sub> } is set
Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = Y } is set
bool (A) is non empty set
7 + Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
{(7 + Y)} is non empty trivial 1 -element set
[:{(7 + Y)},(A):] is Relation-like non empty set
k is set
k `1 is set
k `2 is set
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is Element of (A)
[f,f] is V15() set
{f,f} is non empty set
{f} is non empty trivial 1 -element set
{{f,f},{f}} is non empty set
k is Element of bool (A)
f is set
f `1 is set
f is Element of (A)
(A,f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is set
f is Element of (A)
(A,f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f `1 is set
[:NAT,(A):] is Relation-like non empty V35() set
f `2 is set
[(f `1),(f `2)] is V15() set
{(f `1),(f `2)} is non empty set
{(f `1)} is non empty trivial 1 -element set
{{(f `1),(f `2)},{(f `1)}} is non empty set
Y is Relation-like non empty ()
A is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(Y,A) is Element of bool (Y)
(Y) is non empty set
(Y) is non empty set
proj2 Y is non empty set
{ [b₁,b₂] where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b₂ is Element of (Y) : 7 <= b₁ } is set
bool (Y) is non empty set
{ b₁ where b₁ is Element of (Y) : (Y,b₁) = A } is set
7 + A is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
{(7 + A)} is non empty trivial 1 -element set
[:{(7 + A)},(Y):] is Relation-like non empty set
k is set
k `1 is set
k `2 is set
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is Element of (Y)
[f,f] is V15() set
{f,f} is non empty set
{f} is non empty trivial 1 -element set
{{f,f},{f}} is non empty set
k is non empty Element of bool (Y)
f is set
f `1 is set
f is Element of (Y)
(Y,f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is set
f is Element of (Y)
(Y,f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f `1 is set
[:NAT,(Y):] is Relation-like non empty V35() set
f `2 is set
[(f `1),(f `2)] is V15() set
{(f `1),(f `2)} is non empty set
{(f `1)} is non empty trivial 1 -element set
{{(f `1),(f `2)},{(f `1)}} is non empty set
Y is Relation-like non empty ()
(Y) is non empty set
(Y) is non empty set
proj2 Y is non empty set
[:{4,5},(Y):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(Y):] is Relation-like non empty set
A is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is Relation-like NAT -defined (Y) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (Y)
len a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
[0,0] is V15() set
{0,0} is functional non empty set
{0} is functional non empty trivial 1 -element set
{{0,0},{0}} is non empty set
<*[0,0]*> is Relation-like NAT -defined Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like set
[1,[0,0]] is V15() set
{1,[0,0]} is non empty set
{1} is non empty trivial 1 -element set
{{1,[0,0]},{1}} is non empty set
{[1,[0,0]]} is Relation-like Function-like constant non empty trivial 1 -element set
[1,0] is V15() set
{1,0} is non empty set
{{1,0},{1}} is non empty set
<*[1,0]*> is Relation-like NAT -defined Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like set
[1,[1,0]] is V15() set
{1,[1,0]} is non empty set
{{1,[1,0]},{1}} is non empty set
{[1,[1,0]]} is Relation-like Function-like constant non empty trivial 1 -element set
[2,0] is V15() set
{2,0} is non empty set
{2} is non empty trivial 1 -element set
{{2,0},{2}} is non empty set
<*[2,0]*> is Relation-like NAT -defined Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like set
[1,[2,0]] is V15() set
{1,[2,0]} is non empty set
{{1,[2,0]},{1}} is non empty set
{[1,[2,0]]} is Relation-like Function-like constant non empty trivial 1 -element set
[3,0] is V15() set
{3,0} is non empty set
{3} is non empty trivial 1 -element set
{{3,0},{3}} is non empty set
<*[3,0]*> is Relation-like NAT -defined Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like set
[1,[3,0]] is V15() set
{1,[3,0]} is non empty set
{{1,[3,0]},{1}} is non empty set
{[1,[3,0]]} is Relation-like Function-like constant non empty trivial 1 -element set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is Element of (A)
[Y,a] is V15() set
{Y,a} is non empty set
{Y} is non empty trivial 1 -element set
{{Y,a},{Y}} is non empty set
<*[Y,a]*> is Relation-like NAT -defined Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like set
[1,[Y,a]] is V15() set
{1,[Y,a]} is non empty set
{{1,[Y,a]},{1}} is non empty set
{[1,[Y,a]]} is Relation-like Function-like constant non empty trivial 1 -element set
proj2 <*[Y,a]*> is non empty trivial 1 -element set
{[Y,a]} is Relation-like Function-like constant non empty trivial 1 -element set
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b<sub>2</sub> is Element of (A) : 7 <= b<sub>1</sub> } is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
[:NAT,(A):] is Relation-like non empty V35() set
Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,Y) is non empty Element of bool (A)
bool (A) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = Y } is set
a is Element of (A,Y)
<*a*> is Relation-like NAT -defined (A,Y) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A,Y)
[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
k is Relation-like NAT -defined (A) -valued Function-like V35() Y -element FinSequence-like FinSubsequence-like FinSequence of (A)
<*a*> ^ k is Relation-like NAT -defined Function-like non empty V35() 1 + Y -element FinSequence-like FinSubsequence-like set
1 + Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
rng k is Element of bool (A)
bool (A) is non empty set
rng <*a*> is non empty trivial 1 -element Element of bool (A,Y)
bool (A,Y) is non empty set
(rng <*a*>) \/ (rng k) is non empty set
proj2 (<*a*> ^ k) is non empty set
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
(A) is non empty Element of bool (A)
bool (A) is non empty set
[:{4},(A):] is Relation-like non empty set
[:NAT,(A):] is Relation-like non empty V35() set
a is Element of (A)
<*a*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*a*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[3,0]*> ^ <*a*>) ^ k is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
rng <*a*> is non empty trivial 1 -element Element of bool (A)
bool (A) is non empty set
Y is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
f is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
Y ^ f is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(Y ^ f) ^ k is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
[:NAT,(A):] * is functional non empty FinSequence-membered set
Y is set
a is non empty set
a is non empty set
k is set
bool ([:NAT,(A):] *) is non empty set
(A) is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b<sub>2</sub> is Element of (A) : 7 <= b<sub>1</sub> } is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
(A) is non empty Element of bool (A)
bool (A) is non empty set
[:{4},(A):] is Relation-like non empty set
k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,k) is non empty Element of bool (A)
bool (A) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = k } is set
f is Element of (A,k)
<*f*> is Relation-like NAT -defined (A,k) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A,k)
[1,f] is V15() set
{1,f} is non empty set
{{1,f},{1}} is non empty set
{[1,f]} is Relation-like Function-like constant non empty trivial 1 -element set
f is Relation-like NAT -defined (A) -valued Function-like V35() k -element FinSequence-like FinSubsequence-like FinSequence of (A)
<*f*> ^ f is Relation-like NAT -defined Function-like non empty V35() 1 + k -element FinSequence-like FinSubsequence-like set
1 + k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
g is non empty set
f is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[1,0]*> ^ f is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
f is non empty set
k is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
k ^ f is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
f is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
f is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ f is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(<*[2,0]*> ^ f) ^ f is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
g is non empty set
k is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
k ^ f is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(k ^ f) ^ f is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
k is Element of (A)
<*k*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,k] is V15() set
{1,k} is non empty set
{{1,k},{1}} is non empty set
{[1,k]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*k*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[3,0]*> ^ <*k*>) ^ f is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
f is non empty set
k is non empty set
f is set
Y is non empty set
a is non empty set
A is Relation-like non empty ()
(A) is non empty set
A is Relation-like non empty ()
(A) is non empty set
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b<sub>2</sub> is Element of (A) : 7 <= b<sub>1</sub> } is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
Y is Element of (A)
(A,Y) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is Relation-like NAT -defined (A) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (A)
len a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
<*Y*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,Y] is V15() set
{1,Y} is non empty set
{{1,Y},{1}} is non empty set
{[1,Y]} is Relation-like Function-like constant non empty trivial 1 -element set
<*Y*> ^ a is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = len a } is set
(A,(len a)) is non empty Element of bool (A)
bool (A) is non empty set
f is Element of (A,(len a))
<*f*> is Relation-like NAT -defined (A,(len a)) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A,(len a))
[1,f] is V15() set
{1,f} is non empty set
{{1,f},{1}} is non empty set
{[1,f]} is Relation-like Function-like constant non empty trivial 1 -element set
g is Relation-like NAT -defined (A) -valued Function-like V35() len a -element FinSequence-like FinSubsequence-like FinSequence of (A)
<*f*> ^ g is Relation-like NAT -defined Function-like non empty V35() 1 + (len a) -element FinSequence-like FinSubsequence-like set
1 + (len a) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k is non empty (A) set
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b<sub>2</sub> is Element of (A) : 7 <= b<sub>1</sub> } is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,Y) is non empty Element of bool (A)
bool (A) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = Y } is set
a is Element of (A,Y)
<*a*> is Relation-like NAT -defined (A,Y) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A,Y)
[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
k is Relation-like NAT -defined (A) -valued Function-like V35() Y -element FinSequence-like FinSubsequence-like FinSequence of (A)
(A,a,k) is Element of (A)
(A) is non empty set
<*a*> ^ k is Relation-like NAT -defined Function-like non empty V35() 1 + Y -element FinSequence-like FinSubsequence-like set
1 + Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is Element of (A)
(A,f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
[:NAT,(A):] * is functional non empty FinSequence-membered set
bool ([:NAT,(A):] *) is non empty set
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
[:NAT,(A):] * is functional non empty FinSequence-membered set
bool ([:NAT,(A):] *) is non empty set
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
(A,Y) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
<*[1,0]*> ^ (A,Y) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*[2,0]*> ^ (A,Y) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
a is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,Y)) ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
(A) is non empty Element of bool (A)
bool (A) is non empty set
[:{4},(A):] is Relation-like non empty set
(A) is non empty set
Y is Element of (A)
<*Y*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,Y] is V15() set
{1,Y} is non empty set
{{1,Y},{1}} is non empty set
{[1,Y]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*Y*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
[:NAT,(A):] is Relation-like non empty V35() set
(<*[3,0]*> ^ <*Y*>) ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
F<sub>1</sub>() is Relation-like non empty ()
(F<sub>1</sub>()) is non empty set
(F<sub>1</sub>()) is non empty set
(F<sub>1</sub>()) is non empty set
proj2 F<sub>1</sub>() is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b<sub>2</sub> is Element of (F<sub>1</sub>()) : 7 <= b<sub>1</sub> } is set
(F<sub>1</sub>()) is non empty set
[:{4,5},(F<sub>1</sub>()):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(F<sub>1</sub>()):] is Relation-like non empty set
(F<sub>1</sub>()) is Element of (F<sub>1</sub>())
(F<sub>1</sub>()) is non empty Element of bool (F<sub>1</sub>())
bool (F<sub>1</sub>()) is non empty set
[:{4},(F<sub>1</sub>()):] is Relation-like non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of (F<sub>1</sub>()) : P<sub>1</sub>[b<sub>1</sub>] } is set
A is non empty set
Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(F<sub>1</sub>(),Y) is non empty Element of bool (F<sub>1</sub>())
bool (F<sub>1</sub>()) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of (F<sub>1</sub>()) : (F<sub>1</sub>(),b<sub>1</sub>) = Y } is set
a is Element of (F<sub>1</sub>(),Y)
<*a*> is Relation-like NAT -defined (F<sub>1</sub>(),Y) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (F<sub>1</sub>(),Y)
[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
k is Relation-like NAT -defined (F<sub>1</sub>()) -valued Function-like V35() Y -element FinSequence-like FinSubsequence-like FinSequence of (F<sub>1</sub>())
<*a*> ^ k is Relation-like NAT -defined Function-like non empty V35() 1 + Y -element FinSequence-like FinSubsequence-like set
1 + Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(F<sub>1</sub>(),a,k) is Element of (F<sub>1</sub>())
[:NAT,(F<sub>1</sub>()):] is Relation-like non empty V35() set
Y is Element of (F<sub>1</sub>())
<*Y*> is Relation-like NAT -defined (F<sub>1</sub>()) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (F<sub>1</sub>())
[1,Y] is V15() set
{1,Y} is non empty set
{{1,Y},{1}} is non empty set
{[1,Y]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*Y*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
a is Relation-like NAT -defined [:NAT,(F<sub>1</sub>()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F<sub>1</sub>()):]
(<*[3,0]*> ^ <*Y*>) ^ a is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
k is Element of (F<sub>1</sub>())
(F<sub>1</sub>(),Y,k) is Element of (F<sub>1</sub>())
(F<sub>1</sub>(),k) is Relation-like NAT -defined [:NAT,(F<sub>1</sub>()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F<sub>1</sub>()):]
(<*[3,0]*> ^ <*Y*>) ^ (F<sub>1</sub>(),k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
Y is Relation-like NAT -defined [:NAT,(F<sub>1</sub>()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F<sub>1</sub>()):]
a is Relation-like NAT -defined [:NAT,(F<sub>1</sub>()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F<sub>1</sub>()):]
<*[2,0]*> ^ Y is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(<*[2,0]*> ^ Y) ^ a is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
k is Element of (F<sub>1</sub>())
f is Element of (F<sub>1</sub>())
(F<sub>1</sub>(),k,f) is Element of (F<sub>1</sub>())
(F<sub>1</sub>(),k) is Relation-like NAT -defined [:NAT,(F<sub>1</sub>()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F<sub>1</sub>()):]
<*[2,0]*> ^ (F<sub>1</sub>(),k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(F<sub>1</sub>(),f) is Relation-like NAT -defined [:NAT,(F<sub>1</sub>()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F<sub>1</sub>()):]
(<*[2,0]*> ^ (F<sub>1</sub>(),k)) ^ (F<sub>1</sub>(),f) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
Y is Relation-like NAT -defined [:NAT,(F<sub>1</sub>()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F<sub>1</sub>()):]
<*[1,0]*> ^ Y is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
a is Element of (F<sub>1</sub>())
(F<sub>1</sub>(),a) is Element of (F<sub>1</sub>())
(F<sub>1</sub>(),a) is Relation-like NAT -defined [:NAT,(F<sub>1</sub>()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F<sub>1</sub>()):]
<*[1,0]*> ^ (F<sub>1</sub>(),a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
Y is Element of (F<sub>1</sub>())
[:NAT,(F<sub>1</sub>()):] * is functional non empty FinSequence-membered set
a is set
k is Element of (F<sub>1</sub>())
(F<sub>1</sub>(),k) is Relation-like NAT -defined [:NAT,(F<sub>1</sub>()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F<sub>1</sub>()):]
a is Element of (F<sub>1</sub>())
A is Relation-like non empty ()
(A) is non empty set
A is Relation-like non empty ()
(A) is non empty set
(A) is Element of (A)
Y is Element of (A)
(A,Y) is Element of (A)
(A,Y) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
<*[1,0]*> ^ (A,Y) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
(A) is non empty Element of bool (A)
bool (A) is non empty set
[:{4},(A):] is Relation-like non empty set
a is Element of (A)
Y is Element of (A)
(A,Y,a) is Element of (A)
<*Y*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,Y] is V15() set
{1,Y} is non empty set
{{1,Y},{1}} is non empty set
{[1,Y]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*Y*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
[:NAT,(A):] is Relation-like non empty V35() set
(<*[3,0]*> ^ <*Y*>) ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
Y is Element of (A)
a is Element of (A)
(A,Y,a) is Element of (A)
(A,Y) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
[:NAT,(A):] is Relation-like non empty V35() set
<*[2,0]*> ^ (A,Y) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,Y)) ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A) is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b<sub>2</sub> is Element of (A) : 7 <= b<sub>1</sub> } is set
Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,Y) is non empty Element of bool (A)
bool (A) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = Y } is set
a is Element of (A,Y)
k is Relation-like NAT -defined (A) -valued Function-like V35() Y -element FinSequence-like FinSubsequence-like FinSequence of (A)
(A,a,k) is Element of (A)
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
(A,Y) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
len (A,Y) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A) is Element of (A)
(A) is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b<sub>2</sub> is Element of (A) : 7 <= b<sub>1</sub> } is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,a) is non empty Element of bool (A)
bool (A) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = a } is set
k is Element of (A,a)
f is Relation-like NAT -defined (A) -valued Function-like V35() a -element FinSequence-like FinSubsequence-like FinSequence of (A)
(A,k,f) is Element of (A)
<*k*> is Relation-like NAT -defined (A,a) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A,a)
[1,k] is V15() set
{1,k} is non empty set
{{1,k},{1}} is non empty set
{[1,k]} is Relation-like Function-like constant non empty trivial 1 -element set
<*k*> ^ f is Relation-like NAT -defined Function-like non empty V35() 1 + a -element FinSequence-like FinSubsequence-like set
1 + a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len <*k*> is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len <*k*>) + (len f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
1 + (len f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is Element of (A)
(A,a) is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[1,0]*> ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len <*[1,0]*> is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len (A,a) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len <*[1,0]*>) + (len (A,a)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
1 + (len (A,a)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is Element of (A)
k is Element of (A)
(A,a,k) is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,a)) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,a) ^ (A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ ((A,a) ^ (A,k)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len <*[2,0]*> is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len ((A,a) ^ (A,k)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len <*[2,0]*>) + (len ((A,a) ^ (A,k))) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
1 + (len ((A,a) ^ (A,k))) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
(A) is non empty Element of bool (A)
bool (A) is non empty set
[:{4},(A):] is Relation-like non empty set
a is Element of (A)
k is Element of (A)
(A,a,k) is Element of (A)
<*a*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*a*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[3,0]*> ^ <*a*>) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*a*> ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ (<*a*> ^ (A,k)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len <*[3,0]*> is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len (<*a*> ^ (A,k)) is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len <*[3,0]*>) + (len (<*a*> ^ (A,k))) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
1 + (len (<*a*> ^ (A,k))) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A) is Element of (A)
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b<sub>2</sub> is Element of (A) : 7 <= b<sub>1</sub> } is set
Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,Y) is non empty Element of bool (A)
bool (A) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = Y } is set
a is Element of (A,Y)
(A,a) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k is Element of (A,Y)
f is Element of (A)
(A,f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
A is Relation-like non empty ()
(A) is non empty set
(A) is Element of (A)
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b<sub>2</sub> is Element of (A) : 7 <= b<sub>1</sub> } is set
Y is Element of (A)
(A,Y) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
[:NAT,(A):] is Relation-like non empty V35() set
(A,Y) . 1 is set
((A,Y) . 1) `1 is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,a) is non empty Element of bool (A)
bool (A) is non empty set
{ b₁ where b₁ is Element of (A) : (A,b₁) = a } is set
k is Element of (A,a)
f is Relation-like NAT -defined (A) -valued Function-like V35() a -element FinSequence-like FinSubsequence-like FinSequence of (A)
(A,k,f) is Element of (A)
<*k*> is Relation-like NAT -defined (A,a) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A,a)
[1,k] is V15() set
{1,k} is non empty set
{{1,k},{1}} is non empty set
{[1,k]} is Relation-like Function-like constant non empty trivial 1 -element set
<*k*> ^ f is Relation-like NAT -defined Function-like non empty V35() 1 + a -element FinSequence-like FinSubsequence-like set
1 + a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
[0,0] `1 is set
a is Element of (A)
(A,a) is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[1,0]*> ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
a is Element of (A)
k is Element of (A)
(A,a,k) is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,a)) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,a) ^ (A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ ((A,a) ^ (A,k)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
(A) is non empty Element of bool (A)
bool (A) is non empty set
[:{4},(A):] is Relation-like non empty set
a is Element of (A)
k is Element of (A)
(A,a,k) is Element of (A)
<*a*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*a*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[3,0]*> ^ <*a*>) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*a*> ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ (<*a*> ^ (A,k)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,a) is non empty Element of bool (A)
bool (A) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = a } is set
k is Element of (A,a)
f is Element of (A)
f `1 is set
(A,f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
7 + (A,f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k `1 is set
a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,a) is non empty Element of bool (A)
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = a } is set
k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,k) is non empty Element of bool (A)
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = k } is set
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
(A,Y) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
a is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
k is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
(A,a) ^ k is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal set
f is Element of (A)
(A,f) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
len (A,f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
g is Element of (A)
(A,g) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
k is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
(A,g) ^ k is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
dom (A,g) is Element of bool NAT
len (A,g) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
Seg (len (A,g)) is V35() len (A,g) -element Element of bool NAT
{ b<sub>1</sub> where b<sub>1</sub> is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= len (A,g) ) } is set
(A,f) . 1 is set
(A,g) . 1 is set
len ((A,g) ^ k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len (A,g)) + (len k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A) is Element of (A)
1 + 0 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
1 + (len k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A) is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b<sub>2</sub> is Element of (A) : 7 <= b<sub>1</sub> } is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
j is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,j) is non empty Element of bool (A)
bool (A) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = j } is set
k99 is Element of (A,j)
x9 is Relation-like NAT -defined (A) -valued Function-like V35() j -element FinSequence-like FinSubsequence-like FinSequence of (A)
(A,k99,x9) is Element of (A)
<*k99*> is Relation-like NAT -defined (A,j) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A,j)
[1,k99] is V15() set
{1,k99} is non empty set
{{1,k99},{1}} is non empty set
{[1,k99]} is Relation-like Function-like constant non empty trivial 1 -element set
<*k99*> ^ x9 is Relation-like NAT -defined Function-like non empty V35() 1 + j -element FinSequence-like FinSubsequence-like set
1 + j is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
p9 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,p9) is non empty Element of bool (A)
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = p9 } is set
a is Element of (A,p9)
b is Relation-like NAT -defined (A) -valued Function-like V35() p9 -element FinSequence-like FinSubsequence-like FinSequence of (A)
(A,a,b) is Element of (A)
<*a*> is Relation-like NAT -defined (A,p9) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A,p9)
[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*a*> ^ b is Relation-like NAT -defined Function-like non empty V35() 1 + p9 -element FinSequence-like FinSubsequence-like set
1 + p9 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
b ^ k is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
<*k99*> ^ (b ^ k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len x9 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len x9) + 0 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len b is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len b) + (len k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,k99) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
j is Element of (A)
(A,j) is Element of (A)
(A,j) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[1,0]*> ^ (A,j) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
((A,g) . 1) `1 is set
k99 is Element of (A)
(A,k99) is Element of (A)
(A,k99) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[1,0]*> ^ (A,k99) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,k99) ^ k is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
<*[1,0]*> ^ ((A,k99) ^ k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len (A,j) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len <*[1,0]*> is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len (A,j)) + (len <*[1,0]*>) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len (A,j)) + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,k99) ^ {} is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
j is Element of (A)
k99 is Element of (A)
(A,j,k99) is Element of (A)
(A,j) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ (A,j) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,k99) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,j)) ^ (A,k99) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,j) ^ (A,k99) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ ((A,j) ^ (A,k99)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len ((A,j) ^ (A,k99)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len <*[2,0]*> is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len ((A,j) ^ (A,k99))) + (len <*[2,0]*>) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len ((A,j) ^ (A,k99))) + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len (A,j) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len (A,k99) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len (A,j)) + (len (A,k99)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
((len (A,j)) + (len (A,k99))) + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
((A,g) . 1) `1 is set
x9 is Element of (A)
p9 is Element of (A)
(A,x9,p9) is Element of (A)
(A,x9) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ (A,x9) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,p9) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,x9)) ^ (A,p9) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len (A,x9) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,p9) ^ k is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
len ((A,p9) ^ k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len (A,x9)) + (len ((A,p9) ^ k)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,x9) ^ (A,p9) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ ((A,x9) ^ (A,p9)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
((A,x9) ^ (A,p9)) ^ k is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
<*[2,0]*> ^ (((A,x9) ^ (A,p9)) ^ k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,x9) ^ ((A,p9) ^ k) is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
((len (A,x9)) + (len ((A,p9) ^ k))) + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
b is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
len a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len b is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
c is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
a ^ c is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
d is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
b ^ d is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
c<sub>17</sub> is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
a ^ c<sub>17</sub> is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
(A) is non empty Element of bool (A)
bool (A) is non empty set
[:{4},(A):] is Relation-like non empty set
j is Element of (A)
k99 is Element of (A)
(A,j,k99) is Element of (A)
<*j*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,j] is V15() set
{1,j} is non empty set
{{1,j},{1}} is non empty set
{[1,j]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*j*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(A,k99) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[3,0]*> ^ <*j*>) ^ (A,k99) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*j*> ^ (A,k99) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ (<*j*> ^ (A,k99)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len (<*j*> ^ (A,k99)) is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len <*[3,0]*> is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len (<*j*> ^ (A,k99))) + (len <*[3,0]*>) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len (<*j*> ^ (A,k99))) + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len <*j*> is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len (A,k99) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len <*j*>) + (len (A,k99)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
((len <*j*>) + (len (A,k99))) + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
1 + (len (A,k99)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(1 + (len (A,k99))) + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len (A,k99)) + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
((A,g) . 1) `1 is set
x9 is Element of (A)
p9 is Element of (A)
(A,x9,p9) is Element of (A)
<*x9*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,x9] is V15() set
{1,x9} is non empty set
{{1,x9},{1}} is non empty set
{[1,x9]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*x9*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(A,p9) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[3,0]*> ^ <*x9*>) ^ (A,p9) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*x9*> ^ (A,p9) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ (<*x9*> ^ (A,p9)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(<*[3,0]*> ^ (<*x9*> ^ (A,p9))) ^ k is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(<*x9*> ^ (A,p9)) ^ k is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ ((<*x9*> ^ (A,p9)) ^ k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,p9) ^ k is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
<*x9*> ^ ((A,p9) ^ k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(<*x9*> ^ ((A,p9) ^ k)) . 1 is set
(A) is Element of (A)
len (A,Y) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
{ [b₁,b₂] where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b₂ is Element of (A) : 7 <= b₁ } is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,a) is non empty Element of bool (A)
bool (A) is non empty set
{ b₁ where b₁ is Element of (A) : (A,b₁) = a } is set
k is Element of (A,a)
f is Relation-like NAT -defined (A) -valued Function-like V35() a -element FinSequence-like FinSubsequence-like FinSequence of (A)
(A,k,f) is Element of (A)
a is Element of (A)
k is Element of (A)
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,f) is non empty Element of bool (A)
bool (A) is non empty set
{ b₁ where b₁ is Element of (A) : (A,b₁) = f } is set
g is Element of (A,f)
f is Relation-like NAT -defined (A) -valued Function-like V35() f -element FinSequence-like FinSubsequence-like FinSequence of (A)
(A,g,f) is Element of (A)
k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,k) is non empty Element of bool (A)
{ b₁ where b₁ is Element of (A) : (A,b₁) = k } is set
k99 is Element of (A,k)
j is Relation-like NAT -defined (A) -valued Function-like V35() k -element FinSequence-like FinSubsequence-like FinSequence of (A)
(A,k99,j) is Element of (A)
<*a*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*a*> ^ f is Relation-like NAT -defined Function-like non empty V35() 1 + f -element FinSequence-like FinSubsequence-like set
1 + f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
<*k*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,k] is V15() set
{1,k} is non empty set
{{1,k},{1}} is non empty set
{[1,k]} is Relation-like Function-like constant non empty trivial 1 -element set
<*k*> ^ j is Relation-like NAT -defined Function-like non empty V35() 1 + k -element FinSequence-like FinSubsequence-like set
1 + k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(<*a*> ^ f) . 1 is set
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
(A) is non empty set
{ [b₁,b₂] where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b₂ is Element of (A) : 7 <= b₁ } is set
a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,a) is non empty Element of bool (A)
bool (A) is non empty set
{ b₁ where b₁ is Element of (A) : (A,b₁) = a } is set
k is Element of (A,a)
f is Relation-like NAT -defined (A) -valued Function-like V35() a -element FinSequence-like FinSubsequence-like FinSequence of (A)
(A,k,f) is Element of (A)
f is Relation-like NAT -defined (A) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (A)
a is Relation-like NAT -defined (A) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (A)
k is Relation-like NAT -defined (A) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (A)
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,f) is non empty Element of bool (A)
bool (A) is non empty set
{ b₁ where b₁ is Element of (A) : (A,b₁) = f } is set
g is Relation-like NAT -defined (A) -valued Function-like V35() f -element FinSequence-like FinSubsequence-like FinSequence of (A)
f is Element of (A,f)
(A,f,g) is Element of (A)
<*f*> is Relation-like NAT -defined (A,f) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A,f)
[1,f] is V15() set
{1,f} is non empty set
{{1,f},{1}} is non empty set
{[1,f]} is Relation-like Function-like constant non empty trivial 1 -element set
<*f*> ^ g is Relation-like NAT -defined Function-like non empty V35() 1 + f -element FinSequence-like FinSubsequence-like set
1 + f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,k) is non empty Element of bool (A)
{ b₁ where b₁ is Element of (A) : (A,b₁) = k } is set
k99 is Relation-like NAT -defined (A) -valued Function-like V35() k -element FinSequence-like FinSubsequence-like FinSequence of (A)
j is Element of (A,k)
(A,j,k99) is Element of (A)
<*j*> is Relation-like NAT -defined (A,k) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A,k)
[1,j] is V15() set
{1,j} is non empty set
{{1,j},{1}} is non empty set
{[1,j]} is Relation-like Function-like constant non empty trivial 1 -element set
<*j*> ^ k99 is Relation-like NAT -defined Function-like non empty V35() 1 + k -element FinSequence-like FinSubsequence-like set
1 + k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,Y) is Element of (A)
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
a is Element of (A)
(A,a) is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
<*[1,0]*> ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
k is Element of (A)
(A,k) is Element of (A)
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[1,0]*> ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
a is Element of (A)
k is Element of (A)
f is Element of (A)
(A,a,f) is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
<*[2,0]*> ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,f) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,a)) ^ (A,f) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
f is Element of (A)
(A,k,f) is Element of (A)
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,f) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,k)) ^ (A,f) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,a) ^ (A,f) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ ((A,a) ^ (A,f)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,k) ^ (A,f) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ ((A,k) ^ (A,f)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len (A,a) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len (A,k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
g is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
len g is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
j is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
g ^ j is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
k99 is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
k ^ k99 is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
x9 is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
g ^ x9 is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
a is Element of (A)
k is Element of (A)
(A,a,k) is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
<*[2,0]*> ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,a)) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
a is Element of (A)
k is Element of (A)
f is Element of (A)
(A,f,a) is Element of (A)
(A,f) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
<*[2,0]*> ^ (A,f) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,f)) ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
f is Element of (A)
(A,f,k) is Element of (A)
(A,f) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ (A,f) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,f)) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,f) ^ (A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ ((A,f) ^ (A,a)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,f) ^ (A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ ((A,f) ^ (A,k)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,Y) is Element of (A)
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
(A) is non empty Element of bool (A)
bool (A) is non empty set
[:{4},(A):] is Relation-like non empty set
a is Element of (A)
k is Element of (A)
f is Element of (A)
(A,a,f) is Element of (A)
<*a*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*a*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(A,f) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
[:NAT,(A):] is Relation-like non empty V35() set
(<*[3,0]*> ^ <*a*>) ^ (A,f) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
f is Element of (A)
(A,k,f) is Element of (A)
<*k*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,k] is V15() set
{1,k} is non empty set
{{1,k},{1}} is non empty set
{[1,k]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*k*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(A,f) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[3,0]*> ^ <*k*>) ^ (A,f) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*a*> ^ (A,f) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ (<*a*> ^ (A,f)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*k*> ^ (A,f) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ (<*k*> ^ (A,f)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(<*a*> ^ (A,f)) . 1 is set
a is Element of (A)
k is Element of (A)
(A,a,k) is Element of (A)
<*a*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*a*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
[:NAT,(A):] is Relation-like non empty V35() set
(<*[3,0]*> ^ <*a*>) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
a is Element of (A)
k is Element of (A)
f is Element of (A)
(A,f,a) is Element of (A)
<*f*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,f] is V15() set
{1,f} is non empty set
{{1,f},{1}} is non empty set
{[1,f]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*f*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
[:NAT,(A):] is Relation-like non empty V35() set
(<*[3,0]*> ^ <*f*>) ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
f is Element of (A)
(A,f,k) is Element of (A)
<*f*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,f] is V15() set
{1,f} is non empty set
{{1,f},{1}} is non empty set
{[1,f]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*f*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[3,0]*> ^ <*f*>) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*f*> ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ (<*f*> ^ (A,a)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*f*> ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ (<*f*> ^ (A,k)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(<*f*> ^ (A,a)) . 1 is set
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
(A,Y) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
len (A,Y) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,Y) is Element of (A)
(A,(A,Y)) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
len (A,(A,Y)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is Element of (A)
(A,a) is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[1,0]*> ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len <*[1,0]*> is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len (A,a) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len <*[1,0]*>) + (len (A,a)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len (A,a)) + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
(A,Y) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
len (A,Y) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,Y) is Element of (A)
(A,(A,Y)) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
len (A,(A,Y)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,Y) is Element of (A)
(A,(A,Y)) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
len (A,(A,Y)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is Element of (A)
k is Element of (A)
(A,a,k) is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,a)) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,a) ^ (A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ ((A,a) ^ (A,k)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len <*[2,0]*> is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len ((A,a) ^ (A,k)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len <*[2,0]*>) + (len ((A,a) ^ (A,k))) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len ((A,a) ^ (A,k))) + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len (A,k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len (A,a) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len (A,k)) + (len (A,a)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
(A,Y) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
len (A,Y) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,Y) is Element of (A)
(A,(A,Y)) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
len (A,(A,Y)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
(A) is non empty Element of bool (A)
bool (A) is non empty set
[:{4},(A):] is Relation-like non empty set
a is Element of (A)
k is Element of (A)
(A,a,k) is Element of (A)
<*a*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*a*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[3,0]*> ^ <*a*>) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len (A,k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
len <*a*> is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len (A,k)) + (len <*a*>) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
<*a*> ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len (<*a*> ^ (A,k)) is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
<*[3,0]*> ^ (<*a*> ^ (A,k)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
len <*[3,0]*> is non empty ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len <*[3,0]*>) + (len (<*a*> ^ (A,k))) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(len (<*a*> ^ (A,k))) + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
F₁() is Relation-like non empty ()
(F₁()) is non empty set
(F₁()) is Element of (F₁())
(F₁()) is non empty set
(F₁()) is non empty set
proj2 F₁() is non empty set
[:{4,5},(F₁()):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(F₁()):] is Relation-like non empty set
(F₁()) is non empty Element of bool (F₁())
bool (F₁()) is non empty set
[:{4},(F₁()):] is Relation-like non empty set
Y is Element of (F₁())
A is Element of (F₁())
(F₁(),A,Y) is Element of (F₁())
<*A*> is Relation-like NAT -defined (F₁()) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (F₁())
[1,A] is V15() set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*A*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(F₁(),Y) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
[:NAT,(F₁()):] is Relation-like non empty V35() set
(<*[3,0]*> ^ <*A*>) ^ (F₁(),Y) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(F₁(),(F₁(),A,Y)) is Element of (F₁())
A is Element of (F₁())
(F₁(),A) is Element of (F₁())
(F₁(),A) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
<*[1,0]*> ^ (F₁(),A) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(F₁(),(F₁(),A)) is Element of (F₁())
A is Element of (F₁())
Y is Element of (F₁())
(F₁(),A,Y) is Element of (F₁())
(F₁(),A) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
<*[2,0]*> ^ (F₁(),A) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(F₁(),Y) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
(<*[2,0]*> ^ (F₁(),A)) ^ (F₁(),Y) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(F₁(),(F₁(),A,Y)) is Element of (F₁())
(F₁(),(F₁(),A,Y)) is Element of (F₁())
(F₁()) is non empty set
{ [b₁,b₂] where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b₂ is Element of (F₁()) : 7 <= b₁ } is set
A is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(F₁(),A) is non empty Element of bool (F₁())
bool (F₁()) is non empty set
{ b₁ where b₁ is Element of (F₁()) : (F₁(),b₁) = A } is set
Y is Element of (F₁(),A)
a is Relation-like NAT -defined (F₁()) -valued Function-like V35() A -element FinSequence-like FinSubsequence-like FinSequence of (F₁())
(F₁(),Y,a) is Element of (F₁())
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
{ [b₁,b₂] where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b₂ is Element of (A) : 7 <= b₁ } is set
Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,Y) is non empty Element of bool (A)
bool (A) is non empty set
{ b₁ where b₁ is Element of (A) : (A,b₁) = Y } is set
a is Element of (A,Y)
a `1 is set
k is Element of (A)
k `1 is set
(A,k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
7 + (A,k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
A is Relation-like non empty ()
(A) is non empty set
(A) is Element of (A)
(A,(A)) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
(A,(A)) . 1 is set
((A,(A)) . 1) `1 is set
(A) is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b<sub>2</sub> is Element of (A) : 7 <= b<sub>1</sub> } is set
Y is Element of (A)
(A,Y) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A,Y) . 1 is set
((A,Y) . 1) `1 is set
[0,0] `1 is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,a) is non empty Element of bool (A)
bool (A) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of (A) : (A,b<sub>1</sub>) = a } is set
k is Element of (A,a)
f is Relation-like NAT -defined (A) -valued Function-like V35() a -element FinSequence-like FinSubsequence-like FinSequence of (A)
(A,k,f) is Element of (A)
<*k*> is Relation-like NAT -defined (A,a) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A,a)
[1,k] is V15() set
{1,k} is non empty set
{{1,k},{1}} is non empty set
{[1,k]} is Relation-like Function-like constant non empty trivial 1 -element set
<*k*> ^ f is Relation-like NAT -defined Function-like non empty V35() 1 + a -element FinSequence-like FinSubsequence-like set
1 + a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is Element of (A)
(A,a) is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[1,0]*> ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
a is Element of (A)
k is Element of (A)
(A,a,k) is Element of (A)
(A,a) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ (A,a) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,a)) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,a) ^ (A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
<*[2,0]*> ^ ((A,a) ^ (A,k)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
(A) is non empty Element of bool (A)
bool (A) is non empty set
[:{4},(A):] is Relation-like non empty set
a is Element of (A)
k is Element of (A)
(A,a,k) is Element of (A)
<*a*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*a*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[3,0]*> ^ <*a*>) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*a*> ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
<*[3,0]*> ^ (<*a*> ^ (A,k)) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
A is Relation-like non empty ()
(A) is non empty set
Y is Element of (A)
(A,Y) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
(A,Y) . 1 is set
((A,Y) . 1) `1 is set
(A) is non empty set
{ [b₁,b₂] where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b₂ is Element of (A) : 7 <= b₁ } is set
a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,a) is non empty Element of bool (A)
bool (A) is non empty set
{ b₁ where b₁ is Element of (A) : (A,b₁) = a } is set
A is Relation-like non empty ()
(A) is Element of (A)
(A) is non empty set
(A,(A)) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
(A,(A)) . 1 is set
((A,(A)) . 1) `1 is set
Y is Element of (A)
(A,Y) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(A,Y) . 1 is set
((A,Y) . 1) `1 is set
F₂() is non empty set
F₁() is Relation-like non empty ()
(F₁()) is non empty set
[:(F₁()),F₂():] is Relation-like non empty set
bool [:(F₁()),F₂():] is non empty set
(F₁()) is Element of (F₁())
F₃() is Element of F₂()
A is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
A + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
Y is Relation-like Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
Y . (F₁()) is Element of F₂()
a is Element of (F₁())
(F₁(),a) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
(F₁()) is non empty set
proj2 F₁() is non empty set
[:NAT,(F₁()):] is Relation-like non empty V35() set
len (F₁(),a) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
Y . a is Element of F₂()
F₄(a) is Element of F₂()
(F₁(),a) is Element of (F₁())
Y . (F₁(),a) is Element of F₂()
F₅((Y . (F₁(),a))) is Element of F₂()
(F₁(),a) is Element of (F₁())
Y . (F₁(),a) is Element of F₂()
(F₁(),a) is Element of (F₁())
Y . (F₁(),a) is Element of F₂()
F₆((Y . (F₁(),a)),(Y . (F₁(),a))) is Element of F₂()
(F₁(),a) is Element of (F₁())
Y . (F₁(),a) is Element of F₂()
F₇(a,(Y . (F₁(),a))) is Element of F₂()
k is Element of F₂()
k is Element of F₂()
k is Element of F₂()
k is Element of F₂()
k is Element of F₂()
k is Element of F₂()
k is Element of F₂()
f is Element of F₂()
f is Element of F₂()
g is Element of F₂()
k is Element of F₂()
j is Element of F₂()
a is Relation-like Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
k is Relation-like Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
k . (F₁()) is Element of F₂()
(F₁(),(F₁())) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
(F₁()) is non empty set
proj2 F₁() is non empty set
[:NAT,(F₁()):] is Relation-like non empty V35() set
len (F₁(),(F₁())) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(F₁(),(F₁())) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
(F₁()) is non empty set
proj2 F₁() is non empty set
[:NAT,(F₁()):] is Relation-like non empty V35() set
len (F₁(),(F₁())) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(F₁(),(F₁())) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
(F₁()) is non empty set
proj2 F₁() is non empty set
[:NAT,(F₁()):] is Relation-like non empty V35() set
len (F₁(),(F₁())) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is Element of (F₁())
(F₁(),f) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
(F₁()) is non empty set
proj2 F₁() is non empty set
[:NAT,(F₁()):] is Relation-like non empty V35() set
len (F₁(),f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k . f is Element of F₂()
F₄(f) is Element of F₂()
(F₁(),f) is Element of (F₁())
k . (F₁(),f) is Element of F₂()
F₅((k . (F₁(),f))) is Element of F₂()
(F₁(),f) is Element of (F₁())
k . (F₁(),f) is Element of F₂()
(F₁(),f) is Element of (F₁())
k . (F₁(),f) is Element of F₂()
F₆((k . (F₁(),f)),(k . (F₁(),f))) is Element of F₂()
(F₁(),f) is Element of (F₁())
k . (F₁(),f) is Element of F₂()
F₇(f,(k . (F₁(),f))) is Element of F₂()
Y . f is Element of F₂()
(F₁(),(F₁(),f)) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),(F₁(),f)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
Y . (F₁(),f) is Element of F₂()
Y . f is Element of F₂()
(F₁(),(F₁(),f)) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),(F₁(),f)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
Y . (F₁(),f) is Element of F₂()
(F₁(),(F₁(),f)) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),(F₁(),f)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
Y . (F₁(),f) is Element of F₂()
Y . f is Element of F₂()
(F₁(),(F₁(),f)) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),(F₁(),f)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
Y . (F₁(),f) is Element of F₂()
Y . f is Element of F₂()
(F₁()) --> F₃() is Relation-like Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
A is Relation-like Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
A . (F₁()) is Element of F₂()
Y is Element of (F₁())
(F₁(),Y) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
(F₁()) is non empty set
proj2 F₁() is non empty set
[:NAT,(F₁()):] is Relation-like non empty V35() set
len (F₁(),Y) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
A . Y is Element of F₂()
F₄(Y) is Element of F₂()
(F₁(),Y) is Element of (F₁())
A . (F₁(),Y) is Element of F₂()
F₅((A . (F₁(),Y))) is Element of F₂()
(F₁(),Y) is Element of (F₁())
A . (F₁(),Y) is Element of F₂()
(F₁(),Y) is Element of (F₁())
A . (F₁(),Y) is Element of F₂()
F₆((A . (F₁(),Y)),(A . (F₁(),Y))) is Element of F₂()
(F₁(),Y) is Element of (F₁())
A . (F₁(),Y) is Element of F₂()
F₇(Y,(A . (F₁(),Y))) is Element of F₂()
(F₁(),(F₁())) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
(F₁()) is non empty set
proj2 F₁() is non empty set
[:NAT,(F₁()):] is Relation-like non empty V35() set
len (F₁(),(F₁())) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
A is set
Y is Element of (F₁())
(F₁(),Y) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),Y) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is Relation-like Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
a . (F₁()) is Element of F₂()
a . A is set
k is Relation-like Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
k . (F₁()) is Element of F₂()
k . Y is Element of F₂()
f is Element of (F₁())
(F₁(),f) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a . f is Element of F₂()
k . f is Element of F₂()
F₄(f) is Element of F₂()
(F₁(),f) is Element of (F₁())
(F₁(),(F₁(),f)) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),(F₁(),f)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a . (F₁(),f) is Element of F₂()
k . (F₁(),f) is Element of F₂()
F₅((k . (F₁(),f))) is Element of F₂()
(F₁(),f) is Element of (F₁())
(F₁(),(F₁(),f)) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),(F₁(),f)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a . (F₁(),f) is Element of F₂()
k . (F₁(),f) is Element of F₂()
(F₁(),f) is Element of (F₁())
(F₁(),(F₁(),f)) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),(F₁(),f)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a . (F₁(),f) is Element of F₂()
k . (F₁(),f) is Element of F₂()
F₆((k . (F₁(),f)),(k . (F₁(),f))) is Element of F₂()
(F₁(),f) is Element of (F₁())
(F₁(),(F₁(),f)) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),(F₁(),f)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a . (F₁(),f) is Element of F₂()
k . (F₁(),f) is Element of F₂()
F₇(f,(k . (F₁(),f))) is Element of F₂()
A is Relation-like Function-like set
proj1 A is set
proj2 A is set
Y is set
a is set
A . a is set
k is Element of (F₁())
(F₁(),k) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is Relation-like Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
f . (F₁()) is Element of F₂()
f . k is Element of F₂()
Y is Relation-like Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
Y . (F₁()) is Element of F₂()
a is Element of (F₁())
(F₁(),a) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),a) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k is Relation-like Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
k . (F₁()) is Element of F₂()
a is Element of (F₁())
Y . a is Element of F₂()
F₄(a) is Element of F₂()
(F₁(),a) is Element of (F₁())
Y . (F₁(),a) is Element of F₂()
F₅((Y . (F₁(),a))) is Element of F₂()
(F₁(),a) is Element of (F₁())
Y . (F₁(),a) is Element of F₂()
(F₁(),a) is Element of (F₁())
Y . (F₁(),a) is Element of F₂()
F₆((Y . (F₁(),a)),(Y . (F₁(),a))) is Element of F₂()
(F₁(),a) is Element of (F₁())
Y . (F₁(),a) is Element of F₂()
F₇(a,(Y . (F₁(),a))) is Element of F₂()
k is Element of (F₁())
(F₁(),k) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is Relation-like Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
f . (F₁()) is Element of F₂()
f . a is Element of F₂()
(F₁(),a) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),a) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
g is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k is Element of (F₁())
(F₁(),k) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f . k is Element of F₂()
F₄(k) is Element of F₂()
(F₁(),k) is Element of (F₁())
f . (F₁(),k) is Element of F₂()
F₅((f . (F₁(),k))) is Element of F₂()
(F₁(),k) is Element of (F₁())
f . (F₁(),k) is Element of F₂()
(F₁(),k) is Element of (F₁())
f . (F₁(),k) is Element of F₂()
F₆((f . (F₁(),k)),(f . (F₁(),k))) is Element of F₂()
(F₁(),k) is Element of (F₁())
f . (F₁(),k) is Element of F₂()
F₇(k,(f . (F₁(),k))) is Element of F₂()
(F₁(),(F₁(),a)) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),(F₁(),a)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
j is Element of (F₁())
(F₁(),j) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),j) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f . j is Element of F₂()
F₄(j) is Element of F₂()
(F₁(),j) is Element of (F₁())
f . (F₁(),j) is Element of F₂()
F₅((f . (F₁(),j))) is Element of F₂()
(F₁(),j) is Element of (F₁())
f . (F₁(),j) is Element of F₂()
(F₁(),j) is Element of (F₁())
f . (F₁(),j) is Element of F₂()
F₆((f . (F₁(),j)),(f . (F₁(),j))) is Element of F₂()
(F₁(),j) is Element of (F₁())
f . (F₁(),j) is Element of F₂()
F₇(j,(f . (F₁(),j))) is Element of F₂()
f . (F₁(),a) is Element of F₂()
j is Element of (F₁())
(F₁(),j) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),j) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(F₁(),(F₁(),a)) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),(F₁(),a)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(F₁(),(F₁(),a)) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),(F₁(),a)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
x9 is Element of (F₁())
(F₁(),x9) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),x9) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f . x9 is Element of F₂()
F₄(x9) is Element of F₂()
(F₁(),x9) is Element of (F₁())
f . (F₁(),x9) is Element of F₂()
F₅((f . (F₁(),x9))) is Element of F₂()
(F₁(),x9) is Element of (F₁())
f . (F₁(),x9) is Element of F₂()
(F₁(),x9) is Element of (F₁())
f . (F₁(),x9) is Element of F₂()
F₆((f . (F₁(),x9)),(f . (F₁(),x9))) is Element of F₂()
(F₁(),x9) is Element of (F₁())
f . (F₁(),x9) is Element of F₂()
F₇(x9,(f . (F₁(),x9))) is Element of F₂()
x9 is Element of (F₁())
(F₁(),x9) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),x9) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f . x9 is Element of F₂()
F₄(x9) is Element of F₂()
(F₁(),x9) is Element of (F₁())
f . (F₁(),x9) is Element of F₂()
F₅((f . (F₁(),x9))) is Element of F₂()
(F₁(),x9) is Element of (F₁())
f . (F₁(),x9) is Element of F₂()
(F₁(),x9) is Element of (F₁())
f . (F₁(),x9) is Element of F₂()
F₆((f . (F₁(),x9)),(f . (F₁(),x9))) is Element of F₂()
(F₁(),x9) is Element of (F₁())
f . (F₁(),x9) is Element of F₂()
F₇(x9,(f . (F₁(),x9))) is Element of F₂()
f . (F₁(),a) is Element of F₂()
x9 is Element of (F₁())
(F₁(),x9) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),x9) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f . (F₁(),a) is Element of F₂()
x9 is Element of (F₁())
(F₁(),x9) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),x9) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(F₁(),(F₁(),a)) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),(F₁(),a)) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k is Element of (F₁())
(F₁(),k) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f . k is Element of F₂()
F₄(k) is Element of F₂()
(F₁(),k) is Element of (F₁())
f . (F₁(),k) is Element of F₂()
F₅((f . (F₁(),k))) is Element of F₂()
(F₁(),k) is Element of (F₁())
f . (F₁(),k) is Element of F₂()
(F₁(),k) is Element of (F₁())
f . (F₁(),k) is Element of F₂()
F₆((f . (F₁(),k)),(f . (F₁(),k))) is Element of F₂()
(F₁(),k) is Element of (F₁())
f . (F₁(),k) is Element of F₂()
F₇(k,(f . (F₁(),k))) is Element of F₂()
f . (F₁(),a) is Element of F₂()
k is Element of (F₁())
(F₁(),k) is Relation-like NAT -defined [:NAT,(F₁()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F₁()):]
len (F₁(),k) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
Y is Relation-like NAT -defined (A) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (A)
len Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A) is non empty Element of bool (A)
bool (A) is non empty set
[:{4},(A):] is Relation-like non empty set
{ (Y . b₁) where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len Y & Y . b₁ in (A) ) } is set
bool (A) is non empty set
k is set
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
Y . f is set
A is Relation-like non empty ()
(A) is non empty set
(A) is non empty Element of bool (A)
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
[:{4,5},(A):] is Relation-like non empty set
[:{6},NAT:] \/ [:{4,5},(A):] is Relation-like non empty set
bool (A) is non empty set
[:{4},(A):] is Relation-like non empty set
bool (A) is non empty set
[:(A),(bool (A)):] is Relation-like non empty set
bool [:(A),(bool (A)):] is non empty set
Y is Element of (A)
(A) is Element of (A)
a is Element of bool (A)
k is Relation-like Function-like V18((A), bool (A)) Element of bool [:(A),(bool (A)):]
k . (A) is Element of bool (A)
k . Y is Element of bool (A)
f is Element of (A)
k . f is Element of bool (A)
(A,f) is Relation-like NAT -defined (A) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (A)
len (A,f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
{ ((A,f) . b₁) where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (A,f) & (A,f) . b₁ in (A) ) } is set
(A,f) is Element of (A)
k . (A,f) is Element of bool (A)
(A,f) is Element of (A)
k . (A,f) is Element of bool (A)
(A,f) is Element of (A)
k . (A,f) is Element of bool (A)
(k . (A,f)) \/ (k . (A,f)) is Element of bool (A)
(A,f) is Element of (A)
k . (A,f) is Element of bool (A)
(A,f) is Element of (A)
{(A,f)} is non empty trivial 1 -element set
(k . (A,f)) \ {(A,f)} is Element of bool (A)
(A,(A,f)) is Element of bool (A)
a is Element of bool (A)
k is Element of bool (A)
f is Relation-like Function-like V18((A), bool (A)) Element of bool [:(A),(bool (A)):]
f . Y is Element of bool (A)
f . (A) is Element of bool (A)
f is Relation-like Function-like V18((A), bool (A)) Element of bool [:(A),(bool (A)):]
f . Y is Element of bool (A)
f . (A) is Element of bool (A)
(A) is non empty set
{ [b₁,b₂] where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b₂ is Element of (A) : 7 <= b₁ } is set
g is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,g) is non empty Element of bool (A)
bool (A) is non empty set
{ b₁ where b₁ is Element of (A) : (A,b₁) = g } is set
k is Element of (A,g)
j is Relation-like NAT -defined (A) -valued Function-like V35() g -element FinSequence-like FinSubsequence-like FinSequence of (A)
(A,k,j) is Element of (A)
f . (A,k,j) is Element of bool (A)
f . (A,k,j) is Element of bool (A)
(A,(A,k,j)) is Relation-like NAT -defined (A) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of (A)
len j is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
{ (j . b₁) where b₁ is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len j & j . b₁ in (A) ) } is set
g is Element of (A)
f . g is Element of bool (A)
f . g is Element of bool (A)
(A,g) is Element of (A)
(A,g) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
[:NAT,(A):] is Relation-like non empty V35() set
<*[1,0]*> ^ (A,g) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
f . (A,g) is Element of bool (A)
f . (A,g) is Element of bool (A)
(A,(A,g)) is Element of (A)
g is Element of (A)
k is Element of (A)
f . k is Element of bool (A)
f . k is Element of bool (A)
(A,g,k) is Element of (A)
<*g*> is Relation-like NAT -defined (A) -valued Function-like constant non empty trivial V35() 1 -element FinSequence-like FinSubsequence-like FinSequence of (A)
[1,g] is V15() set
{1,g} is non empty set
{{1,g},{1}} is non empty set
{[1,g]} is Relation-like Function-like constant non empty trivial 1 -element set
<*[3,0]*> ^ <*g*> is Relation-like NAT -defined Function-like non empty V35() 1 + 1 -element FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
[:NAT,(A):] is Relation-like non empty V35() set
(<*[3,0]*> ^ <*g*>) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
f . (A,g,k) is Element of bool (A)
f . (A,g,k) is Element of bool (A)
(A,(A,g,k)) is Element of (A)
(A,(A,g,k)) is Element of (A)
{g} is non empty trivial 1 -element set
(f . k) \ {g} is Element of bool (A)
g is Element of (A)
f . g is Element of bool (A)
f . g is Element of bool (A)
k is Element of (A)
f . k is Element of bool (A)
f . k is Element of bool (A)
(A,g,k) is Element of (A)
(A,g) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
[:NAT,(A):] is Relation-like non empty V35() set
<*[2,0]*> ^ (A,g) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
(A,k) is Relation-like NAT -defined [:NAT,(A):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(A):]
(<*[2,0]*> ^ (A,g)) ^ (A,k) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set
f . (A,g,k) is Element of bool (A)
f . (A,g,k) is Element of bool (A)
(A,(A,g,k)) is Element of (A)
(A,(A,g,k)) is Element of (A)
(f . g) \/ (f . k) is Element of bool (A)
A is Relation-like non empty ()
(A) is non empty set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
(A) \ NAT is Element of bool (A)
bool (A) is non empty set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is Element of (A)
a is Element of (A)
[Y,a] is V15() set
{Y,a} is non empty set
{Y} is non empty trivial 1 -element set
{{Y,a},{Y}} is non empty set
the Relation-like (A) is Relation-like (A)
k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is Element of (A)
a is Element of (A)
k is Element of (A)
the Relation-like (A) is Relation-like (A)
(A) \ NAT is Element of bool (A)
bool (A) is non empty set
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
g is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
j is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
[Y,a] is V15() set
{Y,a} is non empty set
{Y} is non empty trivial 1 -element set
{{Y,a},{Y}} is non empty set
[a,k] is V15() set
{a,k} is non empty set
{a} is non empty trivial 1 -element set
{{a,k},{a}} is non empty set
[Y,k] is V15() set
{Y,k} is non empty set
{{Y,k},{Y}} is non empty set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is Element of (A)
the Relation-like (A) is Relation-like (A)
(A) \ NAT is Element of bool (A)
bool (A) is non empty set
[Y,Y] is V15() set
{Y,Y} is non empty set
{Y} is non empty trivial 1 -element set
{{Y,Y},{Y}} is non empty set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is Element of (A)
a is Element of (A)
the Relation-like (A) is Relation-like (A)
(A) \ NAT is Element of bool (A)
bool (A) is non empty set
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
g is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
[Y,a] is V15() set
{Y,a} is non empty set
{Y} is non empty trivial 1 -element set
{{Y,a},{Y}} is non empty set
[a,Y] is V15() set
{a,Y} is non empty set
{a} is non empty trivial 1 -element set
{{a,Y},{a}} is non empty set
[Y,a] is V15() set
{Y,a} is non empty set
{Y} is non empty trivial 1 -element set
{{Y,a},{Y}} is non empty set
[a,Y] is V15() set
{a,Y} is non empty set
{a} is non empty trivial 1 -element set
{{a,Y},{a}} is non empty set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is Element of (A)
a is Element of (A)
the Relation-like (A) is Relation-like (A)
(A) \ NAT is Element of bool (A)
bool (A) is non empty set
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
[Y,a] is V15() set
{Y,a} is non empty set
{Y} is non empty trivial 1 -element set
{{Y,a},{Y}} is non empty set
[a,Y] is V15() set
{a,Y} is non empty set
{a} is non empty trivial 1 -element set
{{a,Y},{a}} is non empty set
[a,Y] is V15() set
{a,Y} is non empty set
{a} is non empty trivial 1 -element set
{{a,Y},{a}} is non empty set
[Y,a] is V15() set
{Y,a} is non empty set
{Y} is non empty trivial 1 -element set
{{Y,a},{Y}} is non empty set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is Element of (A)
a is Element of (A)
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is Element of (A)
a is Element of (A)
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
bool (A) is non empty set
Y is non empty Element of bool (A)
a is non empty Element of bool NAT
min* a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is Element of (A)
f is Element of (A)
g is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal set
f is Element of (A)
a is set
the Relation-like (A) is Relation-like (A)
(A) \ NAT is Element of bool (A)
Y \ NAT is Element of bool (A)
f is set
f is Element of (A)
g is Element of (A)
[f,g] is V15() set
{f,g} is non empty set
{f} is non empty trivial 1 -element set
{{f,g},{f}} is non empty set
a is Element of (A)
k is Element of (A)
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
bool (A) is non empty set
Y is non empty Element of bool (A)
(A,Y) is Element of (A)
k is Element of (A)
Y is Element of (A)
a is Element of (A)
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is Element of (A)
{ b₁ where b₁ is Element of (A) : (A,Y,b₁) } is set
bool (A) is non empty set
k is set
f is Element of (A)
k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f is Element of (A)
k is Element of (A)
k is set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is Element of (A)
(A,Y) is non empty Element of bool (A)
bool (A) is non empty set
{ b₁ where b₁ is Element of (A) : (A,Y,b₁) } is set
(A,(A,Y)) is Element of (A)
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is Element of (A)
(A,Y) is Element of (A)
(A,Y) is non empty Element of bool (A)
bool (A) is non empty set
{ b₁ where b₁ is Element of (A) : (A,Y,b₁) } is set
(A,(A,Y)) is Element of (A)
a is Element of (A)
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
bool (A) is non empty set
Y is non empty Element of bool (A)
a is non empty Element of bool (A)
(A,a) is Element of (A)
(A,Y) is Element of (A)
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is Element of (A)
a is Element of (A)
k is Element of (A)
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is Element of (A)
a is Element of (A)
k is Element of (A)
Y is set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() set
bool [:NAT,(A):] is non empty V35() set
a is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
Y is Element of (A)
k is Relation-like Function-like V18( NAT ,(A)) Element of bool [:NAT,(A):]
k . 0 is Element of (A)
k . a is Element of (A)
f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
k . (f + 1) is Element of (A)
k . f is Element of (A)
(A,(k . f)) is Element of (A)
(A,(k . f)) is non empty Element of bool (A)
bool (A) is non empty set
{ b₁ where b₁ is Element of (A) : (A,k . f,b₁) } is set
(A,(A,(k . f))) is Element of (A)
(A,(k . f)) is Element of (A)
(A,(A,(k . f))) is Element of (A)
(A,(A,(k . f))) is non empty Element of bool (A)
{ b₁ where b₁ is Element of (A) : (A,(A,(k . f)),b₁) } is set
(A,(A,(A,(k . f)))) is Element of (A)
k is Element of (A)
f is Element of (A)
f is Relation-like Function-like V18( NAT ,(A)) Element of bool [:NAT,(A):]
f . a is Element of (A)
f . 0 is Element of (A)
g is Relation-like Function-like V18( NAT ,(A)) Element of bool [:NAT,(A):]
g . a is Element of (A)
g . 0 is Element of (A)
f is Relation-like Function-like V18( NAT ,(A)) Element of bool [:NAT,(A):]
f . a is Element of (A)
f . 0 is Element of (A)
g is Relation-like Function-like V18( NAT ,(A)) Element of bool [:NAT,(A):]
g . a is Element of (A)
g . 0 is Element of (A)
k is Relation-like Function-like V18( NAT ,(A)) Element of bool [:NAT,(A):]
k . a is Element of (A)
k . 0 is Element of (A)
g is Relation-like Function-like V18( NAT ,(A)) Element of bool [:NAT,(A):]
g . a is Element of (A)
g . 0 is Element of (A)
k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f . k is Element of (A)
g . k is Element of (A)
k + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
f . (k + 1) is Element of (A)
g . (k + 1) is Element of (A)
(A,(f . k)) is Element of (A)
(A,(f . k)) is non empty Element of bool (A)
bool (A) is non empty set
{ b₁ where b₁ is Element of (A) : (A,f . k,b₁) } is set
(A,(A,(f . k))) is Element of (A)
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is Element of (A)
(A,a,Y) is Element of (A)
(A,a,0) is Element of (A)
[:NAT,(A):] is Relation-like non empty V35() set
bool [:NAT,(A):] is non empty V35() set
k is Relation-like Function-like V18( NAT ,(A)) Element of bool [:NAT,(A):]
k . 0 is Element of (A)
k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,a,k) is Element of (A)
k + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(A,a,(k + 1)) is Element of (A)
[:NAT,(A):] is Relation-like non empty V35() set
bool [:NAT,(A):] is non empty V35() set
f is Relation-like Function-like V18( NAT ,(A)) Element of bool [:NAT,(A):]
f . (k + 1) is Element of (A)
f . 0 is Element of (A)
f . k is Element of (A)
(A,(A,a,k)) is Element of (A)
(A,(A,a,k)) is non empty Element of bool (A)
bool (A) is non empty set
{ b₁ where b₁ is Element of (A) : (A,(A,a,k),b₁) } is set
(A,(A,(A,a,k))) is Element of (A)
Y is set
A is Relation-like non empty ()
(A) is non empty set
proj2 A is non empty set
bool (A) is non empty set
the Element of Y is Element of Y
(A) is Element of (A)
a is set