REAL is non empty non trivial non finite set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty non trivial non finite set
RAT is non empty non trivial non finite set
INT is non empty non trivial non finite set
[:COMPLEX,COMPLEX:] is non empty set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is non empty set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty set
[:[:NAT,NAT:],NAT:] is non empty set
bool [:[:NAT,NAT:],NAT:] is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal set
bool omega is non empty set
bool NAT is non empty set
K240(NAT) is V46() set
K384() is V72() V100() L8()
K189() is Relation-like [:INT,INT:] -defined INT -valued Function-like quasi_total Element of bool [:[:INT,INT:],INT:]
G8(INT,K189()) is V100() L8()
the U1 of K384() is set
{} is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() integer finite V36() FinSequence-membered ext-real set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive Element of NAT
{{},1} is non empty finite set
K503() is set
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
K518(NAT) is non empty functional M13(NAT * , NAT )
K453((NAT *),NAT) is M13(NAT * , NAT )
{ b1 where b1 is Relation-like NAT * -defined NAT -valued Function-like M14(NAT * , NAT ,K453((NAT *),NAT)) : b1 is homogeneous } is set
bool K518(NAT) is non empty set
K396(K518(NAT)) is non empty Element of bool (bool K518(NAT))
bool (bool K518(NAT)) is non empty set
[:NAT,K396(K518(NAT)):] is non empty set
bool [:NAT,K396(K518(NAT)):] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive Element of NAT
0 is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() integer finite V36() FinSequence-membered ext-real Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive Element of NAT
Seg 1 is non empty finite V39(1) Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
Seg 2 is non empty finite V39(2) Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
[+] is non empty Relation-like NAT * -defined Function-like V53() homogeneous V147() V152() V153(2) set
1 proj 1 is non empty Relation-like NAT * -defined Function-like V53() homogeneous V147() V152() V153(1) set
1 |-> NAT is Relation-like NAT -defined bool REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of 1 -tuples_on (bool REAL)
1 -tuples_on (bool REAL) is FinSequenceSet of bool REAL
K408((1 |-> NAT),1) is Relation-like Function-like set
3 succ 3 is non empty Relation-like NAT * -defined Function-like V53() homogeneous V147() V152() V153(3) set
K523((1 proj 1),(3 succ 3),2) is non empty Relation-like NAT * -defined NAT -valued Function-like V53() homogeneous quasi_total V147() V152() V153(2) M14(NAT * , NAT ,K518(NAT))
4 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive Element of NAT
s is non empty set
t is non empty set
[:s,t:] is non empty set
bool [:s,t:] is non empty set
h is Relation-like s -defined t -valued Function-like quasi_total Element of bool [:s,t:]
n is Relation-like s -defined t -valued Function-like Element of bool [:s,t:]
h +* n is Relation-like Function-like set
h1 is set
proj1 n is set
h +* n is Relation-like s -defined t -valued Function-like Element of bool [:s,t:]
(h +* n) . h1 is set
n . h1 is set
proj1 n is set
h +* n is Relation-like s -defined t -valued Function-like Element of bool [:s,t:]
(h +* n) . h1 is set
h . h1 is set
proj1 n is set
h +* n is Relation-like s -defined t -valued Function-like Element of bool [:s,t:]
h +* n is Relation-like s -defined t -valued Function-like Element of bool [:s,t:]
proj1 h is set
proj1 n is set
proj1 (h +* n) is set
(proj1 h) \/ (proj1 n) is set
s is non empty set
t is non empty set
h is Element of s
n is Element of t
h .--> n is Relation-like s -defined {h} -defined t -valued Function-like one-to-one finite set
{h} is non empty finite set
{h} --> n is non empty Relation-like {h} -defined t -valued {n} -valued Function-like constant total quasi_total finite Element of bool [:{h},{n}:]
{n} is non empty finite set
[:{h},{n}:] is non empty finite set
bool [:{h},{n}:] is non empty finite V36() set
[:s,t:] is non empty set
bool [:s,t:] is non empty set
proj1 (h .--> n) is finite set
{h} is non empty finite Element of bool s
bool s is non empty set
proj2 (h .--> n) is finite set
{n} is non empty finite Element of bool t
bool t is non empty set
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
succ s is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : b1 <= s } is set
t is Element of bool NAT
h is Element of bool NAT
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(s) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : b1 <= s } is set
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(t) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer finite ext-real Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : b1 <= t } is set
h is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
s is Relation-like Function-like set
h1 is set
t is set
h is set
[t,h] is V1() set
n is set
[t,h] .--> n is Relation-like {[t,h]} -defined Function-like one-to-one finite set
{[t,h]} is non empty finite set
{[t,h]} --> n is non empty Relation-like {[t,h]} -defined {n} -valued Function-like constant total quasi_total finite Element of bool [:{[t,h]},{n}:]
{n} is non empty finite set
[:{[t,h]},{n}:] is non empty finite set
bool [:{[t,h]},{n}:] is non empty finite V36() set
s +* ([t,h] .--> n) is Relation-like Function-like set
s1 is set
[h1,s1] is V1() set
(s +* ([t,h] .--> n)) . [h1,s1] is set
s . [h1,s1] is set
proj1 ([t,h] .--> n) is finite set
s is Relation-like Function-like set
s1 is set
h is set
t is set
[t,h] is V1() set
n is set
[t,h] .--> n is Relation-like {[t,h]} -defined Function-like one-to-one finite set
{[t,h]} is non empty finite set
{[t,h]} --> n is non empty Relation-like {[t,h]} -defined {n} -valued Function-like constant total quasi_total finite Element of bool [:{[t,h]},{n}:]
{n} is non empty finite set
[:{[t,h]},{n}:] is non empty finite set
bool [:{[t,h]},{n}:] is non empty finite V36() set
s +* ([t,h] .--> n) is Relation-like Function-like set
h1 is set
[h1,s1] is V1() set
(s +* ([t,h] .--> n)) . [h1,s1] is set
s . [h1,s1] is set
proj1 ([t,h] .--> n) is finite set
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
t | s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seg s is finite V39(s) Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= s ) } is set
t | (Seg s) is Relation-like finite FinSubsequence-like set
t | (Seg s) is Relation-like NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
proj1 (t | (Seg s)) is finite set
dom t is finite Element of bool NAT
t . n is set
(t | (Seg s)) . n is set
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
<*s,t*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V39(2) FinSequence-like FinSubsequence-like FinSequence of NAT
<*s*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set
[1,s] is V1() set
{[1,s]} is non empty finite set
<*t*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set
[1,t] is V1() set
{[1,t]} is non empty finite set
<*s*> ^ <*t*> is non empty Relation-like NAT -defined Function-like finite V39(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(1,<*s,t*>) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
<*s,t*> | (Seg 1) is Relation-like finite FinSubsequence-like set
Sum (1,<*s,t*>) is V24() V25() integer ext-real Element of INT
K241(INT,(1,<*s,t*>),K189()) is V24() V25() integer ext-real Element of INT
(2,<*s,t*>) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
<*s,t*> | (Seg 2) is Relation-like finite FinSubsequence-like set
Sum (2,<*s,t*>) is V24() V25() integer ext-real Element of INT
K241(INT,(2,<*s,t*>),K189()) is V24() V25() integer ext-real Element of INT
s + t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
h is V24() V25() integer ext-real Element of INT
<*h*> is non empty Relation-like NAT -defined INT -valued Function-like finite V39(1) FinSequence-like FinSubsequence-like FinSequence of INT
[1,h] is V1() set
{[1,h]} is non empty finite set
Sum <*h*> is V24() V25() integer ext-real Element of INT
K241(INT,<*h*>,K189()) is V24() V25() integer ext-real Element of INT
len <*s,t*> is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
n is V24() V25() integer ext-real Element of INT
<*h,n*> is non empty Relation-like NAT -defined INT -valued Function-like finite V39(2) FinSequence-like FinSubsequence-like FinSequence of INT
<*h*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set
<*n*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set
[1,n] is V1() set
{[1,n]} is non empty finite set
<*h*> ^ <*n*> is non empty Relation-like NAT -defined Function-like finite V39(1 + 1) FinSequence-like FinSubsequence-like set
Sum <*h,n*> is V24() V25() integer ext-real Element of INT
K241(INT,<*h,n*>,K189()) is V24() V25() integer ext-real Element of INT
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
h is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
<*s,t,h*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V39(3) FinSequence-like FinSubsequence-like FinSequence of NAT
<*s*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set
[1,s] is V1() set
{[1,s]} is non empty finite set
<*t*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set
[1,t] is V1() set
{[1,t]} is non empty finite set
<*s*> ^ <*t*> is non empty Relation-like NAT -defined Function-like finite V39(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
<*h*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set
[1,h] is V1() set
{[1,h]} is non empty finite set
(<*s*> ^ <*t*>) ^ <*h*> is non empty Relation-like NAT -defined Function-like finite V39((1 + 1) + 1) FinSequence-like FinSubsequence-like set
(1 + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(1,<*s,t,h*>) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
<*s,t,h*> | (Seg 1) is Relation-like finite FinSubsequence-like set
Sum (1,<*s,t,h*>) is V24() V25() integer ext-real Element of INT
K241(INT,(1,<*s,t,h*>),K189()) is V24() V25() integer ext-real Element of INT
(2,<*s,t,h*>) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
<*s,t,h*> | (Seg 2) is Relation-like finite FinSubsequence-like set
Sum (2,<*s,t,h*>) is V24() V25() integer ext-real Element of INT
K241(INT,(2,<*s,t,h*>),K189()) is V24() V25() integer ext-real Element of INT
s + t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(3,<*s,t,h*>) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Seg 3 is non empty finite V39(3) Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 3 ) } is set
<*s,t,h*> | (Seg 3) is Relation-like finite FinSubsequence-like set
Sum (3,<*s,t,h*>) is V24() V25() integer ext-real Element of INT
K241(INT,(3,<*s,t,h*>),K189()) is V24() V25() integer ext-real Element of INT
(s + t) + h is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
n is V24() V25() integer ext-real Element of INT
<*n*> is non empty Relation-like NAT -defined INT -valued Function-like finite V39(1) FinSequence-like FinSubsequence-like FinSequence of INT
[1,n] is V1() set
{[1,n]} is non empty finite set
Sum <*n*> is V24() V25() integer ext-real Element of INT
K241(INT,<*n*>,K189()) is V24() V25() integer ext-real Element of INT
h1 is V24() V25() integer ext-real Element of INT
<*n,h1*> is non empty Relation-like NAT -defined INT -valued Function-like finite V39(2) FinSequence-like FinSubsequence-like FinSequence of INT
<*n*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set
<*h1*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set
[1,h1] is V1() set
{[1,h1]} is non empty finite set
<*n*> ^ <*h1*> is non empty Relation-like NAT -defined Function-like finite V39(1 + 1) FinSequence-like FinSubsequence-like set
Sum <*n,h1*> is V24() V25() integer ext-real Element of INT
K241(INT,<*n,h1*>,K189()) is V24() V25() integer ext-real Element of INT
len <*s,t,h*> is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
s1 is V24() V25() integer ext-real Element of INT
<*n,h1,s1*> is non empty Relation-like NAT -defined INT -valued Function-like finite V39(3) FinSequence-like FinSubsequence-like FinSequence of INT
<*s1*> is non empty Relation-like NAT -defined Function-like finite V39(1) FinSequence-like FinSubsequence-like set
[1,s1] is V1() set
{[1,s1]} is non empty finite set
(<*n*> ^ <*h1*>) ^ <*s1*> is non empty Relation-like NAT -defined Function-like finite V39((1 + 1) + 1) FinSequence-like FinSubsequence-like set
Sum <*n,h1,s1*> is V24() V25() integer ext-real Element of INT
K241(INT,<*n,h1,s1*>,K189()) is V24() V25() integer ext-real Element of INT
- 1 is V24() V25() integer ext-real Element of REAL
{(- 1),0,1} is non empty finite Element of bool REAL
s is ()
the of s is non empty finite set
Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s
t is Relation-like INT -defined the of s -valued Function-like quasi_total Element of Funcs (INT, the of s)
h is V24() V25() integer ext-real set
n is Element of the of s
h .--> n is Relation-like {h} -defined the of s -valued Function-like one-to-one finite set
{h} is non empty finite set
{h} --> n is non empty Relation-like {h} -defined the of s -valued {n} -valued Function-like constant total quasi_total finite Element of bool [:{h},{n}:]
{n} is non empty finite set
[:{h},{n}:] is non empty finite set
bool [:{h},{n}:] is non empty finite V36() set
t +* (h .--> n) is Relation-like Function-like set
proj2 (h .--> n) is finite set
{n} is non empty finite Element of bool the of s
bool the of s is non empty finite V36() set
proj2 (t +* (h .--> n)) is set
proj2 t is set
(proj2 t) \/ (proj2 (h .--> n)) is set
t2 is Relation-like Function-like set
proj1 t2 is set
proj2 t2 is set
proj1 (t +* (h .--> n)) is set
proj1 t is set
proj1 (h .--> n) is finite set
(proj1 t) \/ (proj1 (h .--> n)) is set
(proj1 t) \/ {h} is non empty set
t2 is Relation-like Function-like set
proj1 t2 is set
proj2 t2 is set
s is ()
the of s is non empty finite set
the of s is non empty finite set
[: the of s, the of s,{(- 1),0,1}:] is non empty finite set
t is Element of [: the of s, the of s,{(- 1),0,1}:]
t `3_3 is Element of {(- 1),0,1}
s is ()
the of s is non empty finite set
the of s is non empty finite set
Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s
[: the of s,INT,(Funcs (INT, the of s)):] is non empty set
t is Element of [: the of s,INT,(Funcs (INT, the of s)):]
t `2_3 is V24() V25() integer ext-real Element of INT
t `1 is set
(t `1) `2 is set
s is ()
the of s is non empty finite set
the of s is non empty finite set
Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s
[: the of s,INT,(Funcs (INT, the of s)):] is non empty set
the of s is Relation-like [: the of s, the of s:] -defined [: the of s, the of s,{(- 1),0,1}:] -valued Function-like quasi_total finite Element of bool [:[: the of s, the of s:],[: the of s, the of s,{(- 1),0,1}:]:]
[: the of s, the of s:] is non empty finite set
[: the of s, the of s,{(- 1),0,1}:] is non empty finite set
[:[: the of s, the of s:],[: the of s, the of s,{(- 1),0,1}:]:] is non empty finite set
bool [:[: the of s, the of s:],[: the of s, the of s,{(- 1),0,1}:]:] is non empty finite V36() set
t is Element of [: the of s,INT,(Funcs (INT, the of s)):]
t `1_3 is Element of the of s
t `1 is set
(t `1) `1 is set
t `3_3 is Element of Funcs (INT, the of s)
(s,t) is V24() V25() integer ext-real set
t `2_3 is V24() V25() integer ext-real Element of INT
(t `1) `2 is set
(t `3_3) . (s,t) is set
[(t `1_3),((t `3_3) . (s,t))] is V1() set
the of s . [(t `1_3),((t `3_3) . (s,t))] is set
h is V24() V25() integer ext-real Element of INT
(t `3_3) . h is Element of the of s
[(t `1_3),((t `3_3) . h)] is V1() Element of [: the of s, the of s:]
the of s . [(t `1_3),((t `3_3) . h)] is Element of [: the of s, the of s,{(- 1),0,1}:]
s is ()
the of s is non empty finite set
the of s is non empty finite set
Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s
[: the of s,INT,(Funcs (INT, the of s)):] is non empty set
t is Element of [: the of s,INT,(Funcs (INT, the of s)):]
t `1_3 is Element of the of s
t `1 is set
(t `1) `1 is set
the of s is Element of the of s
(s,t) is Element of [: the of s, the of s,{(- 1),0,1}:]
[: the of s, the of s,{(- 1),0,1}:] is non empty finite set
the of s is Relation-like [: the of s, the of s:] -defined [: the of s, the of s,{(- 1),0,1}:] -valued Function-like quasi_total finite Element of bool [:[: the of s, the of s:],[: the of s, the of s,{(- 1),0,1}:]:]
[: the of s, the of s:] is non empty finite set
[:[: the of s, the of s:],[: the of s, the of s,{(- 1),0,1}:]:] is non empty finite set
bool [:[: the of s, the of s:],[: the of s, the of s,{(- 1),0,1}:]:] is non empty finite V36() set
t `3_3 is Element of Funcs (INT, the of s)
(s,t) is V24() V25() integer ext-real set
t `2_3 is V24() V25() integer ext-real Element of INT
(t `1) `2 is set
(t `3_3) . (s,t) is set
[(t `1_3),((t `3_3) . (s,t))] is V1() set
the of s . [(t `1_3),((t `3_3) . (s,t))] is set
(s,t) `1_3 is Element of the of s
(s,t) `1 is set
((s,t) `1) `1 is set
(s,(s,t)) is V24() V25() integer ext-real set
(s,t) `3_3 is Element of {(- 1),0,1}
(s,t) + (s,(s,t)) is V24() V25() integer ext-real set
(s,t) `2_3 is Element of the of s
((s,t) `1) `2 is set
(s,(t `3_3),(s,t),((s,t) `2_3)) is Relation-like INT -defined the of s -valued Function-like quasi_total Element of Funcs (INT, the of s)
(s,t) .--> ((s,t) `2_3) is Relation-like {(s,t)} -defined the of s -valued Function-like one-to-one finite set
{(s,t)} is non empty finite set
{(s,t)} --> ((s,t) `2_3) is non empty Relation-like {(s,t)} -defined the of s -valued {((s,t) `2_3)} -valued Function-like constant total quasi_total finite Element of bool [:{(s,t)},{((s,t) `2_3)}:]
{((s,t) `2_3)} is non empty finite set
[:{(s,t)},{((s,t) `2_3)}:] is non empty finite set
bool [:{(s,t)},{((s,t) `2_3)}:] is non empty finite V36() set
(t `3_3) +* ((s,t) .--> ((s,t) `2_3)) is Relation-like Function-like set
[((s,t) `1_3),((s,t) + (s,(s,t))),(s,(t `3_3),(s,t),((s,t) `2_3))] is V1() V2() set
[((s,t) `1_3),((s,t) + (s,(s,t)))] is V1() set
[[((s,t) `1_3),((s,t) + (s,(s,t)))],(s,(t `3_3),(s,t),((s,t) `2_3))] is V1() set
s is ()
the of s is non empty finite set
the of s is non empty finite set
Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s
[: the of s,INT,(Funcs (INT, the of s)):] is non empty set
[:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set
bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set
t is Element of [: the of s,INT,(Funcs (INT, the of s)):]
h is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]
h . 0 is Element of [: the of s,INT,(Funcs (INT, the of s)):]
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
n + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
h . (n + 1) is Element of [: the of s,INT,(Funcs (INT, the of s)):]
h . n is Element of [: the of s,INT,(Funcs (INT, the of s)):]
(s,(h . n)) is Element of [: the of s,INT,(Funcs (INT, the of s)):]
h is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]
h . 0 is Element of [: the of s,INT,(Funcs (INT, the of s)):]
n is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]
n . 0 is Element of [: the of s,INT,(Funcs (INT, the of s)):]
h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
h1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
h . (h1 + 1) is Element of [: the of s,INT,(Funcs (INT, the of s)):]
h . h1 is Element of [: the of s,INT,(Funcs (INT, the of s)):]
(s,(h . h1)) is Element of [: the of s,INT,(Funcs (INT, the of s)):]
h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
h1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
n . (h1 + 1) is Element of [: the of s,INT,(Funcs (INT, the of s)):]
n . h1 is Element of [: the of s,INT,(Funcs (INT, the of s)):]
(s,(n . h1)) is Element of [: the of s,INT,(Funcs (INT, the of s)):]
s is ()
the of s is non empty finite set
the of s is non empty finite set
Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s
[: the of s,INT,(Funcs (INT, the of s)):] is non empty set
t is Element of [: the of s,INT,(Funcs (INT, the of s)):]
t `1_3 is Element of the of s
t `1 is set
(t `1) `1 is set
the of s is Element of the of s
(s,t) is Element of [: the of s,INT,(Funcs (INT, the of s)):]
s is ()
the of s is non empty finite set
the of s is non empty finite set
Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s
[: the of s,INT,(Funcs (INT, the of s)):] is non empty set
t is Element of [: the of s,INT,(Funcs (INT, the of s)):]
(s,t) is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]
[:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set
bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set
(s,t) . 0 is Element of [: the of s,INT,(Funcs (INT, the of s)):]
t is ()
the of t is non empty finite set
the of t is non empty finite set
Funcs (INT, the of t) is non empty FUNCTION_DOMAIN of INT , the of t
[: the of t,INT,(Funcs (INT, the of t)):] is non empty set
h is Element of [: the of t,INT,(Funcs (INT, the of t)):]
(t,h) is Relation-like NAT -defined [: the of t,INT,(Funcs (INT, the of t)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of t,INT,(Funcs (INT, the of t)):]:]
[:NAT,[: the of t,INT,(Funcs (INT, the of t)):]:] is non empty set
bool [:NAT,[: the of t,INT,(Funcs (INT, the of t)):]:] is non empty set
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
s + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(t,h) . (s + 1) is Element of [: the of t,INT,(Funcs (INT, the of t)):]
(t,h) . s is Element of [: the of t,INT,(Funcs (INT, the of t)):]
(t,((t,h) . s)) is Element of [: the of t,INT,(Funcs (INT, the of t)):]
s is ()
the of s is non empty finite set
the of s is non empty finite set
Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s
[: the of s,INT,(Funcs (INT, the of s)):] is non empty set
t is Element of [: the of s,INT,(Funcs (INT, the of s)):]
(s,t) is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]
[:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set
bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set
(s,t) . 1 is Element of [: the of s,INT,(Funcs (INT, the of s)):]
(s,t) is Element of [: the of s,INT,(Funcs (INT, the of s)):]
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(s,t) . (0 + 1) is Element of [: the of s,INT,(Funcs (INT, the of s)):]
(s,t) . 0 is Element of [: the of s,INT,(Funcs (INT, the of s)):]
(s,((s,t) . 0)) is Element of [: the of s,INT,(Funcs (INT, the of s)):]
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
s + t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
h is ()
the of h is non empty finite set
the of h is non empty finite set
Funcs (INT, the of h) is non empty FUNCTION_DOMAIN of INT , the of h
[: the of h,INT,(Funcs (INT, the of h)):] is non empty set
n is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(h,n) is Relation-like NAT -defined [: the of h,INT,(Funcs (INT, the of h)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:]
[:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:] is non empty set
bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:] is non empty set
(h,n) . (s + t) is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(h,n) . s is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(h,((h,n) . s)) is Relation-like NAT -defined [: the of h,INT,(Funcs (INT, the of h)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:]
(h,((h,n) . s)) . t is Element of [: the of h,INT,(Funcs (INT, the of h)):]
h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
s + h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(h,n) . (s + h1) is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(h,((h,n) . s)) . h1 is Element of [: the of h,INT,(Funcs (INT, the of h)):]
h1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
s + (h1 + 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(h,n) . (s + (h1 + 1)) is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(h,((h,n) . s)) . (h1 + 1) is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(s + h1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(h,n) . ((s + h1) + 1) is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(h,((h,n) . (s + h1))) is Element of [: the of h,INT,(Funcs (INT, the of h)):]
s + 0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(h,n) . (s + 0) is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(h,((h,n) . s)) . 0 is Element of [: the of h,INT,(Funcs (INT, the of h)):]
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
h is ()
the of h is non empty finite set
the of h is non empty finite set
Funcs (INT, the of h) is non empty FUNCTION_DOMAIN of INT , the of h
[: the of h,INT,(Funcs (INT, the of h)):] is non empty set
n is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(h,n) is Relation-like NAT -defined [: the of h,INT,(Funcs (INT, the of h)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:]
[:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:] is non empty set
bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:] is non empty set
(h,n) . s is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(h,((h,n) . s)) is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(h,n) . t is Element of [: the of h,INT,(Funcs (INT, the of h)):]
h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
s + h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
s1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
s + s1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(h,n) . (s + s1) is Element of [: the of h,INT,(Funcs (INT, the of h)):]
s1 + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
s + (s1 + 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(h,n) . (s + (s1 + 1)) is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(s + s1) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(h,n) . ((s + s1) + 1) is Element of [: the of h,INT,(Funcs (INT, the of h)):]
s + 0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(h,n) . (s + 0) is Element of [: the of h,INT,(Funcs (INT, the of h)):]
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
h is ()
the of h is non empty finite set
the of h is non empty finite set
Funcs (INT, the of h) is non empty FUNCTION_DOMAIN of INT , the of h
[: the of h,INT,(Funcs (INT, the of h)):] is non empty set
the of h is Element of the of h
n is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(h,n) is Relation-like NAT -defined [: the of h,INT,(Funcs (INT, the of h)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:]
[:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:] is non empty set
bool [:NAT,[: the of h,INT,(Funcs (INT, the of h)):]:] is non empty set
(h,n) . s is Element of [: the of h,INT,(Funcs (INT, the of h)):]
((h,n) . s) `1_3 is Element of the of h
((h,n) . s) `1 is set
(((h,n) . s) `1) `1 is set
(h,n) . t is Element of [: the of h,INT,(Funcs (INT, the of h)):]
(h,((h,n) . s)) is Element of [: the of h,INT,(Funcs (INT, the of h)):]
s is ()
the of s is non empty finite set
the of s is non empty finite set
Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s
[: the of s,INT,(Funcs (INT, the of s)):] is non empty set
s is ()
the of s is non empty finite set
the of s is non empty finite set
Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s
[: the of s,INT,(Funcs (INT, the of s)):] is non empty set
t is Element of [: the of s,INT,(Funcs (INT, the of s)):]
(s,t) is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]
[:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set
bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set
the of s is Element of the of s
h is Element of [: the of s,INT,(Funcs (INT, the of s)):]
n is Element of [: the of s,INT,(Funcs (INT, the of s)):]
h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(s,t) . h1 is Element of [: the of s,INT,(Funcs (INT, the of s)):]
((s,t) . h1) `1_3 is Element of the of s
((s,t) . h1) `1 is set
(((s,t) . h1) `1) `1 is set
s1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(s,t) . s1 is Element of [: the of s,INT,(Funcs (INT, the of s)):]
((s,t) . s1) `1_3 is Element of the of s
((s,t) . s1) `1 is set
(((s,t) . s1) `1) `1 is set
h is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(s,t) . h is Element of [: the of s,INT,(Funcs (INT, the of s)):]
((s,t) . h) `1_3 is Element of the of s
((s,t) . h) `1 is set
(((s,t) . h) `1) `1 is set
s is ()
the of s is non empty finite set
the of s is non empty finite set
Funcs (INT, the of s) is non empty FUNCTION_DOMAIN of INT , the of s
[: the of s,INT,(Funcs (INT, the of s)):] is non empty set
the of s is Element of the of s
t is Element of [: the of s,INT,(Funcs (INT, the of s)):]
(s,t) is Relation-like NAT -defined [: the of s,INT,(Funcs (INT, the of s)):] -valued Function-like quasi_total Element of bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:]
[:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set
bool [:NAT,[: the of s,INT,(Funcs (INT, the of s)):]:] is non empty set
(s,t) is Element of [: the of s,INT,(Funcs (INT, the of s)):]
h is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(s,t) . h is Element of [: the of s,INT,(Funcs (INT, the of s)):]
((s,t) . h) `1_3 is Element of the of s
((s,t) . h) `1 is set
(((s,t) . h) `1) `1 is set
h is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real set
(s,t) . h is Element of [: the of s,INT,(Funcs (INT, the of s)):]
((s,t) . h) `1_3 is Element of the of s
((s,t) . h) `1 is set
(((s,t) . h) `1) `1 is set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(s,t) . n is Element of [: the of s,INT,(Funcs (INT, the of s)):]
((s,t) . n) `1_3 is Element of the of s
((s,t) . n) `1 is set
(((s,t) . n) `1) `1 is set
h1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(s,t) . h1 is Element of [: the of s,INT,(Funcs (INT, the of s)):]
((s,t) . h1) `1_3 is Element of the of s
((s,t) . h1) `1 is set
(((s,t) . h1) `1) `1 is set
h is set
t is non empty set
s is non empty set
[:s,t:] is non empty set
[:s,[:s,t:]:] is non empty set
bool [:s,[:s,t:]:] is non empty set
n is Element of t
h1 is Relation-like s -defined [:s,t:] -valued Function-like quasi_total Element of bool [:s,[:s,t:]:]
s1 is Element of s
h1 . s1 is Element of [:s,t:]
[s1,h] is V1() set
5 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real positive Element of NAT
(5) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer finite ext-real Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT : b1 <= 5 } is set
{0,1} is non empty finite Element of bool NAT
[:(5),{0,1}:] is non empty Relation-like NAT -defined NAT -valued finite Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty set
([:(5),{0,1}:],{(- 1),0,1},0) is Relation-like [:(5),{0,1}:] -defined [:[:(5),{0,1}:],{(- 1),0,1}:] -valued Function-like quasi_total finite Element of bool [:[:(5),{0,1}:],[:[:(5),{0,1}:],{(- 1),0,1}:]:]
[:[:(5),{0,1}:],{(- 1),0,1}:] is non empty finite set
[:[:(5),{0,1}:],[:[:(5),{0,1}:],{(- 1),0,1}:]:] is non empty finite set
bool [:[:(5),{0,1}:],[:[:(5),{0,1}:],{(- 1),0,1}:]:] is non empty finite V36() set
[:NAT,NAT,NAT:] is non empty set
[0,0] is V1() Element of [:NAT,NAT:]
[0,0,1] is V1() V2() Element of [:NAT,NAT,NAT:]
[0,0] is V1() set
[[0,0],1] is V1() set
([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1]) is Relation-like [:NAT,NAT:] -defined {[0,0]} -defined [:NAT,NAT,NAT:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:]
{[0,0]} is non empty finite set
[:[:NAT,NAT:],[:NAT,NAT,NAT:]:] is non empty set
bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:] is non empty set
{[0,0]} --> [0,0,1] is non empty Relation-like {[0,0]} -defined [:NAT,NAT,NAT:] -valued {[0,0,1]} -valued Function-like constant total quasi_total finite Element of bool [:{[0,0]},{[0,0,1]}:]
{[0,0,1]} is non empty finite set
[:{[0,0]},{[0,0,1]}:] is non empty finite set
bool [:{[0,0]},{[0,0,1]}:] is non empty finite V36() set
([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1]) is Relation-like Function-like finite set
[0,1] is V1() Element of [:NAT,NAT:]
[1,0,1] is V1() V2() Element of [:NAT,NAT,NAT:]
[1,0] is V1() set
[[1,0],1] is V1() set
([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1]) is Relation-like [:NAT,NAT:] -defined {[0,1]} -defined [:NAT,NAT,NAT:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:]
{[0,1]} is non empty finite set
{[0,1]} --> [1,0,1] is non empty Relation-like {[0,1]} -defined [:NAT,NAT,NAT:] -valued {[1,0,1]} -valued Function-like constant total quasi_total finite Element of bool [:{[0,1]},{[1,0,1]}:]
{[1,0,1]} is non empty finite set
[:{[0,1]},{[1,0,1]}:] is non empty finite set
bool [:{[0,1]},{[1,0,1]}:] is non empty finite V36() set
(([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1]) is Relation-like Function-like finite set
[1,1] is V1() Element of [:NAT,NAT:]
[1,1,1] is V1() V2() Element of [:NAT,NAT,NAT:]
[1,1] is V1() set
[[1,1],1] is V1() set
([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1]) is Relation-like [:NAT,NAT:] -defined {[1,1]} -defined [:NAT,NAT,NAT:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:]
{[1,1]} is non empty finite set
{[1,1]} --> [1,1,1] is non empty Relation-like {[1,1]} -defined [:NAT,NAT,NAT:] -valued {[1,1,1]} -valued Function-like constant total quasi_total finite Element of bool [:{[1,1]},{[1,1,1]}:]
{[1,1,1]} is non empty finite set
[:{[1,1]},{[1,1,1]}:] is non empty finite set
bool [:{[1,1]},{[1,1,1]}:] is non empty finite V36() set
((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1]) is Relation-like Function-like finite set
[1,0] is V1() Element of [:NAT,NAT:]
[2,1,1] is V1() V2() Element of [:NAT,NAT,NAT:]
[2,1] is V1() set
[[2,1],1] is V1() set
([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1]) is Relation-like [:NAT,NAT:] -defined {[1,0]} -defined [:NAT,NAT,NAT:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:]
{[1,0]} is non empty finite set
{[1,0]} --> [2,1,1] is non empty Relation-like {[1,0]} -defined [:NAT,NAT,NAT:] -valued {[2,1,1]} -valued Function-like constant total quasi_total finite Element of bool [:{[1,0]},{[2,1,1]}:]
{[2,1,1]} is non empty finite set
[:{[1,0]},{[2,1,1]}:] is non empty finite set
bool [:{[1,0]},{[2,1,1]}:] is non empty finite V36() set
(((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1]) is Relation-like Function-like finite set
[2,1] is V1() Element of [:NAT,NAT:]
([:NAT,NAT:],[:NAT,NAT,NAT:],[2,1],[2,1,1]) is Relation-like [:NAT,NAT:] -defined {[2,1]} -defined [:NAT,NAT,NAT:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:]
{[2,1]} is non empty finite set
{[2,1]} --> [2,1,1] is non empty Relation-like {[2,1]} -defined [:NAT,NAT,NAT:] -valued {[2,1,1]} -valued Function-like constant total quasi_total finite Element of bool [:{[2,1]},{[2,1,1]}:]
[:{[2,1]},{[2,1,1]}:] is non empty finite set
bool [:{[2,1]},{[2,1,1]}:] is non empty finite V36() set
((((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[2,1],[2,1,1]) is Relation-like Function-like finite set
[:NAT,NAT,REAL:] is non empty set
[2,0] is V1() Element of [:NAT,NAT:]
[3,0,(- 1)] is V1() V2() Element of [:NAT,NAT,REAL:]
[3,0] is V1() set
[[3,0],(- 1)] is V1() set
([:NAT,NAT:],[:NAT,NAT,REAL:],[2,0],[3,0,(- 1)]) is Relation-like [:NAT,NAT:] -defined {[2,0]} -defined [:NAT,NAT,REAL:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,REAL:]:]
{[2,0]} is non empty finite set
[:[:NAT,NAT:],[:NAT,NAT,REAL:]:] is non empty set
bool [:[:NAT,NAT:],[:NAT,NAT,REAL:]:] is non empty set
{[2,0]} --> [3,0,(- 1)] is non empty Relation-like {[2,0]} -defined [:NAT,NAT,REAL:] -valued {[3,0,(- 1)]} -valued Function-like constant total quasi_total finite Element of bool [:{[2,0]},{[3,0,(- 1)]}:]
{[3,0,(- 1)]} is non empty finite set
[:{[2,0]},{[3,0,(- 1)]}:] is non empty finite set
bool [:{[2,0]},{[3,0,(- 1)]}:] is non empty finite V36() set
(((((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[2,1],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[2,0],[3,0,(- 1)]) is Relation-like Function-like finite set
[3,1] is V1() Element of [:NAT,NAT:]
[4,0,(- 1)] is V1() V2() Element of [:NAT,NAT,REAL:]
[4,0] is V1() set
[[4,0],(- 1)] is V1() set
([:NAT,NAT:],[:NAT,NAT,REAL:],[3,1],[4,0,(- 1)]) is Relation-like [:NAT,NAT:] -defined {[3,1]} -defined [:NAT,NAT,REAL:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,REAL:]:]
{[3,1]} is non empty finite set
{[3,1]} --> [4,0,(- 1)] is non empty Relation-like {[3,1]} -defined [:NAT,NAT,REAL:] -valued {[4,0,(- 1)]} -valued Function-like constant total quasi_total finite Element of bool [:{[3,1]},{[4,0,(- 1)]}:]
{[4,0,(- 1)]} is non empty finite set
[:{[3,1]},{[4,0,(- 1)]}:] is non empty finite set
bool [:{[3,1]},{[4,0,(- 1)]}:] is non empty finite V36() set
((((((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[2,1],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[2,0],[3,0,(- 1)])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[3,1],[4,0,(- 1)]) is Relation-like Function-like finite set
[4,1] is V1() Element of [:NAT,NAT:]
[4,1,(- 1)] is V1() V2() Element of [:NAT,NAT,REAL:]
[4,1] is V1() set
[[4,1],(- 1)] is V1() set
([:NAT,NAT:],[:NAT,NAT,REAL:],[4,1],[4,1,(- 1)]) is Relation-like [:NAT,NAT:] -defined {[4,1]} -defined [:NAT,NAT,REAL:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,REAL:]:]
{[4,1]} is non empty finite set
{[4,1]} --> [4,1,(- 1)] is non empty Relation-like {[4,1]} -defined [:NAT,NAT,REAL:] -valued {[4,1,(- 1)]} -valued Function-like constant total quasi_total finite Element of bool [:{[4,1]},{[4,1,(- 1)]}:]
{[4,1,(- 1)]} is non empty finite set
[:{[4,1]},{[4,1,(- 1)]}:] is non empty finite set
bool [:{[4,1]},{[4,1,(- 1)]}:] is non empty finite V36() set
(((((((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[2,1],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[2,0],[3,0,(- 1)])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[3,1],[4,0,(- 1)])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[4,1],[4,1,(- 1)]) is Relation-like Function-like finite set
[4,0] is V1() Element of [:NAT,NAT:]
[5,0,0] is V1() V2() Element of [:NAT,NAT,NAT:]
[5,0] is V1() set
[[5,0],0] is V1() set
([:NAT,NAT:],[:NAT,NAT,NAT:],[4,0],[5,0,0]) is Relation-like [:NAT,NAT:] -defined {[4,0]} -defined [:NAT,NAT,NAT:] -valued Function-like one-to-one finite Element of bool [:[:NAT,NAT:],[:NAT,NAT,NAT:]:]
{[4,0]} is non empty finite set
{[4,0]} --> [5,0,0] is non empty Relation-like {[4,0]} -defined [:NAT,NAT,NAT:] -valued {[5,0,0]} -valued Function-like constant total quasi_total finite Element of bool [:{[4,0]},{[5,0,0]}:]
{[5,0,0]} is non empty finite set
[:{[4,0]},{[5,0,0]}:] is non empty finite set
bool [:{[4,0]},{[5,0,0]}:] is non empty finite V36() set
((((((((([:(5),{0,1}:],{(- 1),0,1},0) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,0],[0,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[0,1],[1,0,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,1],[1,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[1,0],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[2,1],[2,1,1])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[2,0],[3,0,(- 1)])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[3,1],[4,0,(- 1)])) +* ([:NAT,NAT:],[:NAT,NAT,REAL:],[4,1],[4,1,(- 1)])) +* ([:NAT,NAT:],[:NAT,NAT,NAT:],[4,0],[5,0,0]) is Relation-like Function-like finite set
[:(5),{0,1},{(- 1),0,1}:] is non empty finite Element of bool [:NAT,NAT,REAL:]
bool [:NAT,NAT,REAL:] is non empty set
[:[:(5),{0,1}:],[:(5),{0,1},{(- 1),0,1}:]:] is non empty finite set
bool [:[:(5),{0,1}:],[:(5),{0,1},{(- 1),0,1}:]:] is non empty finite V36() set
[:[:(5),{0,1}:],{(- 1),0,1}:] is non empty Relation-like [:NAT,NAT:] -defined REAL -valued finite Element of bool [:[:NAT,NAT:],REAL:]
[:[:NAT,NAT:],REAL:] is non empty set
bool [:[:NAT,NAT:],REAL:] is non empty set
s1k is Element of {(- 1),0,1}
([:(5),{0,1}:],{(- 1),0,1},s1k) is Relation-like [:(5),{0,1}:] -defined [:[:(5),{0,1}:],{(- 1),0,1}:] -valued Function-like quasi_total finite Element of bool [:[:(5),{0,1}:],[:[:(5),{0,1}:],{(- 1),0,1}:]:]
[:(5),{0,1}:] is non empty finite set
[:(5),{0,1},{(- 1),0,1}:] is non