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

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
{ b1 where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set

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

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

bool is non empty set
A is ()
Y is 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

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
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
\/ [:{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
\/ [:{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
\/ [:{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
\/ [:{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
\/ [:{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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } 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
\/ [:{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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } 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

A is Relation-like non empty ()
(A) is non empty set
(A) is non empty set
proj2 A is non empty set
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } 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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } 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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } is set
Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
{ b1 where b1 is Element of (A) : (A,b1) = 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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (Y) : 7 <= b1 } is set
bool (Y) is non empty set
{ b1 where b1 is Element of (Y) : (Y,b1) = 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
\/ [:{4,5},(Y):] is Relation-like non empty set
A is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT

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

is non empty 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] is V15() set
{1,0} is non empty set
{{1,0},{1}} is non empty set

[1,[1,0]] is V15() set
{1,[1,0]} is non empty set
{{1,[1,0]},{1}} is non empty 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

[1,[2,0]] is V15() set
{1,[2,0]} is non empty set
{{1,[2,0]},{1}} is non empty 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

[1,[3,0]] is V15() set
{1,[3,0]} is non empty set
{{1,[3,0]},{1}} 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 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

[1,[Y,a]] is V15() set
{1,[Y,a]} is non empty set
{{1,[Y,a]},{1}} is non empty set

proj2 <*[Y,a]*> is 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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
\/ [:{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
{ b1 where b1 is Element of (A) : (A,b1) = Y } is set
a is Element of (A,Y)

[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty 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 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
\/ [:{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)

[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set

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

rng <*a*> is non empty trivial 1 -element 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
[:NAT,(A):] is Relation-like non empty V35() 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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
\/ [:{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
{ b1 where b1 is Element of (A) : (A,b1) = k } is set
f is Element of (A,k)

[1,f] is V15() set
{1,f} is non empty set
{{1,f},{1}} is non empty set

1 + k is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
g is non empty set

f is non empty set

g is non empty set

k is Element of (A)

[1,k] is V15() set
{1,k} is non empty set
{{1,k},{1}} is non empty set

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

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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
\/ [:{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

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

[1,Y] is V15() set
{1,Y} is non empty set
{{1,Y},{1}} is non empty set

(A) is non empty set
{ b1 where b1 is Element of (A) : (A,b1) = 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))

[1,f] is V15() set
{1,f} is non empty set
{{1,f},{1}} is non empty 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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
\/ [:{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
{ b1 where b1 is Element of (A) : (A,b1) = Y } is set
a is Element of (A,Y)

[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set

(A,a,k) is Element of (A)
(A) is non empty 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

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

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

a is Element of (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
\/ [:{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)

[1,Y] is V15() set
{1,Y} is non empty set
{{1,Y},{1}} is non empty set

1 + 1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
a is Element of (A)

[:NAT,(A):] is Relation-like non empty V35() set

F1() is Relation-like non empty ()
(F1()) is non empty set
(F1()) is non empty set
(F1()) is non empty set
proj2 F1() is non empty set
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (F1()) : 7 <= b1 } is set
(F1()) is non empty set
[:{4,5},(F1()):] is Relation-like non empty set
\/ [:{4,5},(F1()):] is Relation-like non empty set
(F1()) is Element of (F1())
(F1()) is non empty Element of bool (F1())
bool (F1()) is non empty set
[:{4},(F1()):] is Relation-like non empty set
{ b1 where b1 is Element of (F1()) : P1[b1] } is set
A is non empty set
Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(F1(),Y) is non empty Element of bool (F1())
bool (F1()) is non empty set
{ b1 where b1 is Element of (F1()) : (F1(),b1) = Y } is set
a is Element of (F1(),Y)

[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set

1 + Y is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
(F1(),a,k) is Element of (F1())
[:NAT,(F1()):] is Relation-like non empty V35() set
Y is Element of (F1())

[1,Y] is V15() set
{1,Y} is non empty set
{{1,Y},{1}} is non empty set

k is Element of (F1())
(F1(),Y,k) is Element of (F1())
(F1(),k) is Relation-like NAT -defined [:NAT,(F1()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F1()):]

k is Element of (F1())
f is Element of (F1())
(F1(),k,f) is Element of (F1())
(F1(),k) is Relation-like NAT -defined [:NAT,(F1()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F1()):]

(F1(),f) is Relation-like NAT -defined [:NAT,(F1()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F1()):]
(<*[2,0]*> ^ (F1(),k)) ^ (F1(),f) is Relation-like NAT -defined Function-like non empty V35() FinSequence-like FinSubsequence-like set

a is Element of (F1())
(F1(),a) is Element of (F1())
(F1(),a) is Relation-like NAT -defined [:NAT,(F1()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F1()):]

Y is Element of (F1())
[:NAT,(F1()):] * is functional non empty FinSequence-membered set
a is set
k is Element of (F1())
(F1(),k) is Relation-like NAT -defined [:NAT,(F1()):] -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:NAT,(F1()):]
a is Element of (F1())
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) is non empty set
proj2 A is non empty set
[:NAT,(A):] is Relation-like non empty V35() 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
\/ [:{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)

[1,Y] is V15() set
{1,Y} is non empty set
{{1,Y},{1}} is non empty set

[:NAT,(A):] is Relation-like non empty V35() set

Y is Element of (A)
a is Element of (A)
(A,Y,a) is Element of (A)

[:NAT,(A):] is Relation-like non empty V35() set

(<*[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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } 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
{ b1 where b1 is Element of (A) : (A,b1) = Y } is set
a is Element of (A,Y)

(A,a,k) 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
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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
\/ [:{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
{ b1 where b1 is Element of (A) : (A,b1) = a } is set
k is Element of (A,a)

(A,k,f) is Element of (A)

[1,k] is V15() set
{1,k} is non empty set
{{1,k},{1}} is non empty 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 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)

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

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

<*[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 ((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
\/ [:{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)

[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty 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 (<*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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } 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
{ b1 where b1 is Element of (A) : (A,b1) = 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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } is set
Y is Element of (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
\/ [:{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
{ b1 where b1 is Element of (A) : (A,b1) = a } is set
k is Element of (A,a)

(A,k,f) is Element of (A)

[1,k] is V15() set
{1,k} is non empty set
{{1,k},{1}} is non empty 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 is Element of (A)
k is Element of (A)
(A,a,k) is Element of (A)

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

<*[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
\/ [:{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)

[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is 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
{ b1 where b1 is Element of (A) : (A,b1) = 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)
{ b1 where b1 is Element of (A) : (A,b1) = 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)
{ b1 where b1 is Element of (A) : (A,b1) = k } is 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
a is Element of (A)

f is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal set
f is Element of (A)

len (A,f) is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT
g is Element of (A)

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
{ b1 where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT : ( 1 <= b1 & b1 <= 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
{ [b1,b2] where b1 is ext-real V26() V27() V28() V29() V33() V34() V35() cardinal Element of NAT , b2 is Element of (A) : 7 <= b1 } is set
(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
\/ [:{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
{ b1 where b1 is Element of (A) : (A,b1) = j } is set
k99 is Element of (A,j)

(A,k99,x9) is Element of (A)

[1,k99] is V15() set
{1,k99} is non empty set
{{1,k99},{1}} is non empty 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)
{ b1 where b1 is Element of (A) : (A,b1) = p9 } is set
a is Element of (A,p9)

(A,a,b) is Element of (A)

[1,a] is V15() set
{1,a} is non empty set
{{1,a},{1}} is non empty set

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

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,g) . 1) `1 is set
k99 is Element of (A)
(A,k99) is Element of (A)

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

j is Element of (A)
k99 is Element of (A)
(A,j,k99) is Element of (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))) + () 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)

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

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

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

(A) is non empty set
[:{4,5},(A):] is Relation-like non empty set
\/ [:{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)

[1,j] is V15() set
{1,j} is non empty set
{{1,j},{1}} is non empty 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))) + () 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 (A,k99)) 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
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)

[1,x9] is V15() set
{1,x9} is non empty set
{{1,x9},{1}} is non empty set
{[1,x9]