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

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

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

[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

[: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

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

Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT

{ b

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

bool (Y) is non empty set

{ b

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

(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

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

(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

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

(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

(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

(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

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

(F

(F

(F

proj2 F

{ [b

(F

[:{4,5},(F

[:{6},NAT:] \/ [:{4,5},(F

(F

(F

bool (F

[:{4},(F

{ b

A is non empty set

Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT

(F

bool (F

{ b

a is Element of (F

<*a*> is Relation-like NAT -defined (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

k is Relation-like NAT -defined (F

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

[:NAT,(F

Y is Element of (F

<*Y*> is Relation-like NAT -defined (F

[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

(<*[3,0]*> ^ <*Y*>) ^ a is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set

k is Element of (F

(F

(F

(<*[3,0]*> ^ <*Y*>) ^ (F

Y is Relation-like NAT -defined [:NAT,(F

a is Relation-like NAT -defined [:NAT,(F

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

f is Element of (F

(F

(F

<*[2,0]*> ^ (F

(F

(<*[2,0]*> ^ (F

Y is Relation-like NAT -defined [:NAT,(F

<*[1,0]*> ^ Y is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set

a is Element of (F

(F

(F

<*[1,0]*> ^ (F

Y is Element of (F

[:NAT,(F

a is set

k is Element of (F

(F

a is Element of (F

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

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

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

(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

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

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

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

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

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

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

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

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

(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

(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

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

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

a ^ c

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