REAL is non empty non trivial V48() V49() V50() V54() non finite set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty non trivial non finite set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
RAT is non empty non trivial V48() V49() V50() V51() V54() non finite set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
{{},1} is non empty V48() V49() V50() V51() V52() V53() finite V59() set
COMPLEX is non empty non trivial V48() V54() non finite set
INT is non empty non trivial V48() V49() V50() V51() V52() V54() non finite set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() non finite cardinal limit_cardinal set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
[:REAL,REAL:] is Relation-like non empty non trivial V38() V39() V40() non finite set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:1,1:] is Relation-like RAT -valued INT -valued non empty V38() V39() V40() V41() finite set
bool [:1,1:] is non empty finite V59() set
[:[:1,1:],1:] is Relation-like RAT -valued INT -valued non empty V38() V39() V40() V41() finite set
bool [:[:1,1:],1:] is non empty finite V59() set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial V38() non finite set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial V38() non finite set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial V38() V39() V40() non finite set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial V38() V39() V40() non finite set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial V38() V39() V40() non finite set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() non finite set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() non finite set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
3 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
Seg 1 is non empty trivial V48() V49() V50() V51() V52() V53() finite 1 -element Element of bool NAT
card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
NAT * is functional non empty FinSequence-membered M10( NAT )
<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of NAT
{{}} is functional non empty trivial V48() V49() V50() V51() V52() V53() finite V59() 1 -element set
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V34() V35() V36() V37() V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of REAL
[:NAT,REAL:] is Relation-like non empty non trivial V38() V39() V40() non finite set
Sum (<*> REAL) is ext-real V34() V35() Element of REAL
[:{{}},{{}}:] is Relation-like RAT -valued INT -valued non empty V38() V39() V40() V41() finite set
[:[:{{}},{{}}:],{{}}:] is Relation-like RAT -valued INT -valued non empty V38() V39() V40() V41() finite set
bool [:[:{{}},{{}}:],{{}}:] is non empty finite V59() set
the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:] is Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:]
({{}}, the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:]) is () ()
the carrier of ({{}}, the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:]) is set
s is non empty ()
the carrier of s is non empty set
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
x is Element of the carrier of s
y is Element of the carrier of s
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (x,y) is Element of the carrier of s
the of s . [x,y] is set
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (x,y) is Element of the carrier of s
the of s . [x,y] is set
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
x is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like set
proj1 x is non empty finite V70() set
y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
x . y is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(x . y) `2 is set
branchdeg y is set
(x . y) `1 is set
<*0*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial V38() V39() V40() V41() V42() V43() V44() V45() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
x . (y ^ <*0*>) is set
(x . (y ^ <*0*>)) `1 is set
<*1*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial V38() V39() V40() V41() V42() V43() V44() V45() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
x . (y ^ <*1*>) is set
(x . (y ^ <*1*>)) `1 is set
4 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
5 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
6 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
7 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
z is Element of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[<*z*>,z] is V15() set
{<*z*>,z} is non empty finite set
{<*z*>} is functional non empty trivial finite V59() 1 -element set
{{<*z*>,z},{<*z*>}} is non empty finite V59() set
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
a is Element of the carrier of s
(s,z,a) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (z,a) is Element of the carrier of s
[z,a] is V15() set
{z,a} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,a},{z}} is non empty finite V59() set
the of s . [z,a] is set
[z,(s,z,a)] is V15() set
{z,(s,z,a)} is non empty finite set
{z} is functional non empty trivial finite V59() 1 -element set
{{z,(s,z,a)},{z}} is non empty finite V59() set
<*a*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z ^ <*a*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(z ^ <*a*>),z] is V15() set
{(z ^ <*a*>),z} is non empty finite set
{(z ^ <*a*>)} is functional non empty trivial finite V59() 1 -element set
{{(z ^ <*a*>),z},{(z ^ <*a*>)}} is non empty finite V59() set
b is Element of the carrier of s
<*b*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[<*b*>,b] is V15() set
{<*b*>,b} is non empty finite set
{<*b*>} is functional non empty trivial finite V59() 1 -element set
{{<*b*>,b},{<*b*>}} is non empty finite V59() set
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
X9 is Element of the carrier of s
T9 is Element of the carrier of s
(s,X9,T9) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (X9,T9) is Element of the carrier of s
[X9,T9] is V15() set
{X9,T9} is non empty finite set
{X9} is non empty trivial finite 1 -element set
{{X9,T9},{X9}} is non empty finite V59() set
the of s . [X9,T9] is set
[z,(s,X9,T9)] is V15() set
{z,(s,X9,T9)} is non empty finite set
{z} is functional non empty trivial finite V59() 1 -element set
{{z,(s,X9,T9)},{z}} is non empty finite V59() set
<*X9*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*X9*> ^ z is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(<*X9*> ^ z),T9] is V15() set
{(<*X9*> ^ z),T9} is non empty finite set
{(<*X9*> ^ z)} is functional non empty trivial finite V59() 1 -element set
{{(<*X9*> ^ z),T9},{(<*X9*> ^ z)}} is non empty finite V59() set
Y9 is Element of the carrier of s
<*Y9*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[<*Y9*>,Y9] is V15() set
{<*Y9*>,Y9} is non empty finite set
{<*Y9*>} is functional non empty trivial finite V59() 1 -element set
{{<*Y9*>,Y9},{<*Y9*>}} is non empty finite V59() set
z9 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c16 is Element of the carrier of s
c17 is Element of the carrier of s
(s,c16,c17) is Element of the carrier of s
the of s . (c16,c17) is Element of the carrier of s
[c16,c17] is V15() set
{c16,c17} is non empty finite set
{c16} is non empty trivial finite 1 -element set
{{c16,c17},{c16}} is non empty finite V59() set
the of s . [c16,c17] is set
<*(s,c16,c17)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z9 ^ <*(s,c16,c17)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y9 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(z9 ^ <*(s,c16,c17)*>) ^ y9 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c15 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((z9 ^ <*(s,c16,c17)*>) ^ y9) ^ c15 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c18 is Element of the carrier of s
[(((z9 ^ <*(s,c16,c17)*>) ^ y9) ^ c15),c18] is V15() set
{(((z9 ^ <*(s,c16,c17)*>) ^ y9) ^ c15),c18} is non empty finite set
{(((z9 ^ <*(s,c16,c17)*>) ^ y9) ^ c15)} is functional non empty trivial finite V59() 1 -element set
{{(((z9 ^ <*(s,c16,c17)*>) ^ y9) ^ c15),c18},{(((z9 ^ <*(s,c16,c17)*>) ^ y9) ^ c15)}} is non empty finite V59() set
[y9,c17] is V15() set
{y9,c17} is non empty finite set
{y9} is functional non empty trivial finite V59() 1 -element set
{{y9,c17},{y9}} is non empty finite V59() set
<*c16*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z9 ^ <*c16*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(z9 ^ <*c16*>) ^ c15 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((z9 ^ <*c16*>) ^ c15),c18] is V15() set
{((z9 ^ <*c16*>) ^ c15),c18} is non empty finite set
{((z9 ^ <*c16*>) ^ c15)} is functional non empty trivial finite V59() 1 -element set
{{((z9 ^ <*c16*>) ^ c15),c18},{((z9 ^ <*c16*>) ^ c15)}} is non empty finite V59() set
c19 is Element of the carrier of s
<*c19*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[<*c19*>,c19] is V15() set
{<*c19*>,c19} is non empty finite set
{<*c19*>} is functional non empty trivial finite V59() 1 -element set
{{<*c19*>,c19},{<*c19*>}} is non empty finite V59() set
c21 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c20 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c21 ^ c20 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c24 is Element of the carrier of s
c23 is Element of the carrier of s
(s,c24,c23) is Element of the carrier of s
the of s . (c24,c23) is Element of the carrier of s
[c24,c23] is V15() set
{c24,c23} is non empty finite set
{c24} is non empty trivial finite 1 -element set
{{c24,c23},{c24}} is non empty finite V59() set
the of s . [c24,c23] is set
<*(s,c24,c23)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c21 ^ c20) ^ <*(s,c24,c23)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c22 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((c21 ^ c20) ^ <*(s,c24,c23)*>) ^ c22 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c25 is Element of the carrier of s
[(((c21 ^ c20) ^ <*(s,c24,c23)*>) ^ c22),c25] is V15() set
{(((c21 ^ c20) ^ <*(s,c24,c23)*>) ^ c22),c25} is non empty finite set
{(((c21 ^ c20) ^ <*(s,c24,c23)*>) ^ c22)} is functional non empty trivial finite V59() 1 -element set
{{(((c21 ^ c20) ^ <*(s,c24,c23)*>) ^ c22),c25},{(((c21 ^ c20) ^ <*(s,c24,c23)*>) ^ c22)}} is non empty finite V59() set
[c20,c24] is V15() set
{c20,c24} is non empty finite set
{c20} is functional non empty trivial finite V59() 1 -element set
{{c20,c24},{c20}} is non empty finite V59() set
<*c23*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c21 ^ <*c23*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c21 ^ <*c23*>) ^ c22 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c21 ^ <*c23*>) ^ c22),c25] is V15() set
{((c21 ^ <*c23*>) ^ c22),c25} is non empty finite set
{((c21 ^ <*c23*>) ^ c22)} is functional non empty trivial finite V59() 1 -element set
{{((c21 ^ <*c23*>) ^ c22),c25},{((c21 ^ <*c23*>) ^ c22)}} is non empty finite V59() set
c26 is Element of the carrier of s
<*c26*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[<*c26*>,c26] is V15() set
{<*c26*>,c26} is non empty finite set
{<*c26*>} is functional non empty trivial finite V59() 1 -element set
{{<*c26*>,c26},{<*c26*>}} is non empty finite V59() set
c27 is Element of the carrier of s
c28 is Element of the carrier of s
<*c28*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[<*c28*>,c28] is V15() set
{<*c28*>,c28} is non empty finite set
{<*c28*>} is functional non empty trivial finite V59() 1 -element set
{{<*c28*>,c28},{<*c28*>}} is non empty finite V59() set
c29 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c30 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c29 ^ c30 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c31 is Element of the carrier of s
c32 is Element of the carrier of s
(s,c31,c32) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (c31,c32) is Element of the carrier of s
[c31,c32] is V15() set
{c31,c32} is non empty finite set
{c31} is non empty trivial finite 1 -element set
{{c31,c32},{c31}} is non empty finite V59() set
the of s . [c31,c32] is set
[(c29 ^ c30),(s,c31,c32)] is V15() set
{(c29 ^ c30),(s,c31,c32)} is non empty finite set
{(c29 ^ c30)} is functional non empty trivial finite V59() 1 -element set
{{(c29 ^ c30),(s,c31,c32)},{(c29 ^ c30)}} is non empty finite V59() set
[c29,c31] is V15() set
{c29,c31} is non empty finite set
{c29} is functional non empty trivial finite V59() 1 -element set
{{c29,c31},{c29}} is non empty finite V59() set
[c30,c32] is V15() set
{c30,c32} is non empty finite set
{c30} is functional non empty trivial finite V59() 1 -element set
{{c30,c32},{c30}} is non empty finite V59() set
c33 is Element of the carrier of s
<*c33*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[<*c33*>,c33] is V15() set
{<*c33*>,c33} is non empty finite set
{<*c33*>} is functional non empty trivial finite V59() 1 -element set
{{<*c33*>,c33},{<*c33*>}} is non empty finite V59() set
c35 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c34 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c35 ^ c34 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c36 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c35 ^ c34) ^ c36 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c38 is Element of the carrier of s
[((c35 ^ c34) ^ c36),c38] is V15() set
{((c35 ^ c34) ^ c36),c38} is non empty finite set
{((c35 ^ c34) ^ c36)} is functional non empty trivial finite V59() 1 -element set
{{((c35 ^ c34) ^ c36),c38},{((c35 ^ c34) ^ c36)}} is non empty finite V59() set
c37 is Element of the carrier of s
[c34,c37] is V15() set
{c34,c37} is non empty finite set
{c34} is functional non empty trivial finite V59() 1 -element set
{{c34,c37},{c34}} is non empty finite V59() set
<*c37*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c35 ^ <*c37*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c35 ^ <*c37*>) ^ c36 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c35 ^ <*c37*>) ^ c36),c38] is V15() set
{((c35 ^ <*c37*>) ^ c36),c38} is non empty finite set
{((c35 ^ <*c37*>) ^ c36)} is functional non empty trivial finite V59() 1 -element set
{{((c35 ^ <*c37*>) ^ c36),c38},{((c35 ^ <*c37*>) ^ c36)}} is non empty finite V59() set
c39 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c40 is Element of the carrier of s
c41 is Element of the carrier of s
(s,c40,c41) is Element of the carrier of s
the of s . (c40,c41) is Element of the carrier of s
[c40,c41] is V15() set
{c40,c41} is non empty finite set
{c40} is non empty trivial finite 1 -element set
{{c40,c41},{c40}} is non empty finite V59() set
the of s . [c40,c41] is set
[c39,(s,c40,c41)] is V15() set
{c39,(s,c40,c41)} is non empty finite set
{c39} is functional non empty trivial finite V59() 1 -element set
{{c39,(s,c40,c41)},{c39}} is non empty finite V59() set
<*c41*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c39 ^ <*c41*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(c39 ^ <*c41*>),c40] is V15() set
{(c39 ^ <*c41*>),c40} is non empty finite set
{(c39 ^ <*c41*>)} is functional non empty trivial finite V59() 1 -element set
{{(c39 ^ <*c41*>),c40},{(c39 ^ <*c41*>)}} is non empty finite V59() set
c42 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c44 is Element of the carrier of s
c43 is Element of the carrier of s
(s,c44,c43) is Element of the carrier of s
the of s . (c44,c43) is Element of the carrier of s
[c44,c43] is V15() set
{c44,c43} is non empty finite set
{c44} is non empty trivial finite 1 -element set
{{c44,c43},{c44}} is non empty finite V59() set
the of s . [c44,c43] is set
[c42,(s,c44,c43)] is V15() set
{c42,(s,c44,c43)} is non empty finite set
{c42} is functional non empty trivial finite V59() 1 -element set
{{c42,(s,c44,c43)},{c42}} is non empty finite V59() set
<*c44*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*c44*> ^ c42 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(<*c44*> ^ c42),c43] is V15() set
{(<*c44*> ^ c42),c43} is non empty finite set
{(<*c44*> ^ c42)} is functional non empty trivial finite V59() 1 -element set
{{(<*c44*> ^ c42),c43},{(<*c44*> ^ c42)}} is non empty finite V59() set
c45 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c46 is Element of the carrier of s
c47 is Element of the carrier of s
(s,c46,c47) is Element of the carrier of s
the of s . (c46,c47) is Element of the carrier of s
[c46,c47] is V15() set
{c46,c47} is non empty finite set
{c46} is non empty trivial finite 1 -element set
{{c46,c47},{c46}} is non empty finite V59() set
the of s . [c46,c47] is set
[c45,(s,c46,c47)] is V15() set
{c45,(s,c46,c47)} is non empty finite set
{c45} is functional non empty trivial finite V59() 1 -element set
{{c45,(s,c46,c47)},{c45}} is non empty finite V59() set
<*c47*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c45 ^ <*c47*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(c45 ^ <*c47*>),c46] is V15() set
{(c45 ^ <*c47*>),c46} is non empty finite set
{(c45 ^ <*c47*>)} is functional non empty trivial finite V59() 1 -element set
{{(c45 ^ <*c47*>),c46},{(c45 ^ <*c47*>)}} is non empty finite V59() set
c49 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c51 is Element of the carrier of s
c52 is Element of the carrier of s
(s,c51,c52) is Element of the carrier of s
the of s . (c51,c52) is Element of the carrier of s
[c51,c52] is V15() set
{c51,c52} is non empty finite set
{c51} is non empty trivial finite 1 -element set
{{c51,c52},{c51}} is non empty finite V59() set
the of s . [c51,c52] is set
<*(s,c51,c52)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c49 ^ <*(s,c51,c52)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c48 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c49 ^ <*(s,c51,c52)*>) ^ c48 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c50 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((c49 ^ <*(s,c51,c52)*>) ^ c48) ^ c50 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c53 is Element of the carrier of s
[(((c49 ^ <*(s,c51,c52)*>) ^ c48) ^ c50),c53] is V15() set
{(((c49 ^ <*(s,c51,c52)*>) ^ c48) ^ c50),c53} is non empty finite set
{(((c49 ^ <*(s,c51,c52)*>) ^ c48) ^ c50)} is functional non empty trivial finite V59() 1 -element set
{{(((c49 ^ <*(s,c51,c52)*>) ^ c48) ^ c50),c53},{(((c49 ^ <*(s,c51,c52)*>) ^ c48) ^ c50)}} is non empty finite V59() set
[c48,c52] is V15() set
{c48,c52} is non empty finite set
{c48} is functional non empty trivial finite V59() 1 -element set
{{c48,c52},{c48}} is non empty finite V59() set
<*c51*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c49 ^ <*c51*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c49 ^ <*c51*>) ^ c50 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c49 ^ <*c51*>) ^ c50),c53] is V15() set
{((c49 ^ <*c51*>) ^ c50),c53} is non empty finite set
{((c49 ^ <*c51*>) ^ c50)} is functional non empty trivial finite V59() 1 -element set
{{((c49 ^ <*c51*>) ^ c50),c53},{((c49 ^ <*c51*>) ^ c50)}} is non empty finite V59() set
c54 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c55 is Element of the carrier of s
c56 is Element of the carrier of s
(s,c55,c56) is Element of the carrier of s
the of s . (c55,c56) is Element of the carrier of s
[c55,c56] is V15() set
{c55,c56} is non empty finite set
{c55} is non empty trivial finite 1 -element set
{{c55,c56},{c55}} is non empty finite V59() set
the of s . [c55,c56] is set
[c54,(s,c55,c56)] is V15() set
{c54,(s,c55,c56)} is non empty finite set
{c54} is functional non empty trivial finite V59() 1 -element set
{{c54,(s,c55,c56)},{c54}} is non empty finite V59() set
<*c56*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c54 ^ <*c56*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(c54 ^ <*c56*>),c55] is V15() set
{(c54 ^ <*c56*>),c55} is non empty finite set
{(c54 ^ <*c56*>)} is functional non empty trivial finite V59() 1 -element set
{{(c54 ^ <*c56*>),c55},{(c54 ^ <*c56*>)}} is non empty finite V59() set
c58 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c57 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c58 ^ c57 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c61 is Element of the carrier of s
c60 is Element of the carrier of s
(s,c61,c60) is Element of the carrier of s
the of s . (c61,c60) is Element of the carrier of s
[c61,c60] is V15() set
{c61,c60} is non empty finite set
{c61} is non empty trivial finite 1 -element set
{{c61,c60},{c61}} is non empty finite V59() set
the of s . [c61,c60] is set
<*(s,c61,c60)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c58 ^ c57) ^ <*(s,c61,c60)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c59 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((c58 ^ c57) ^ <*(s,c61,c60)*>) ^ c59 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c62 is Element of the carrier of s
[(((c58 ^ c57) ^ <*(s,c61,c60)*>) ^ c59),c62] is V15() set
{(((c58 ^ c57) ^ <*(s,c61,c60)*>) ^ c59),c62} is non empty finite set
{(((c58 ^ c57) ^ <*(s,c61,c60)*>) ^ c59)} is functional non empty trivial finite V59() 1 -element set
{{(((c58 ^ c57) ^ <*(s,c61,c60)*>) ^ c59),c62},{(((c58 ^ c57) ^ <*(s,c61,c60)*>) ^ c59)}} is non empty finite V59() set
[c57,c61] is V15() set
{c57,c61} is non empty finite set
{c57} is functional non empty trivial finite V59() 1 -element set
{{c57,c61},{c57}} is non empty finite V59() set
<*c60*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c58 ^ <*c60*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c58 ^ <*c60*>) ^ c59 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c58 ^ <*c60*>) ^ c59),c62] is V15() set
{((c58 ^ <*c60*>) ^ c59),c62} is non empty finite set
{((c58 ^ <*c60*>) ^ c59)} is functional non empty trivial finite V59() 1 -element set
{{((c58 ^ <*c60*>) ^ c59),c62},{((c58 ^ <*c60*>) ^ c59)}} is non empty finite V59() set
c63 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c64 is Element of the carrier of s
c65 is Element of the carrier of s
(s,c64,c65) is Element of the carrier of s
the of s . (c64,c65) is Element of the carrier of s
[c64,c65] is V15() set
{c64,c65} is non empty finite set
{c64} is non empty trivial finite 1 -element set
{{c64,c65},{c64}} is non empty finite V59() set
the of s . [c64,c65] is set
[c63,(s,c64,c65)] is V15() set
{c63,(s,c64,c65)} is non empty finite set
{c63} is functional non empty trivial finite V59() 1 -element set
{{c63,(s,c64,c65)},{c63}} is non empty finite V59() set
<*c65*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c63 ^ <*c65*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(c63 ^ <*c65*>),c64] is V15() set
{(c63 ^ <*c65*>),c64} is non empty finite set
{(c63 ^ <*c65*>)} is functional non empty trivial finite V59() 1 -element set
{{(c63 ^ <*c65*>),c64},{(c63 ^ <*c65*>)}} is non empty finite V59() set
c66 is Element of the carrier of s
c67 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c68 is Element of the carrier of s
c69 is Element of the carrier of s
(s,c68,c69) is Element of the carrier of s
the of s . (c68,c69) is Element of the carrier of s
[c68,c69] is V15() set
{c68,c69} is non empty finite set
{c68} is non empty trivial finite 1 -element set
{{c68,c69},{c68}} is non empty finite V59() set
the of s . [c68,c69] is set
[c67,(s,c68,c69)] is V15() set
{c67,(s,c68,c69)} is non empty finite set
{c67} is functional non empty trivial finite V59() 1 -element set
{{c67,(s,c68,c69)},{c67}} is non empty finite V59() set
<*c69*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c67 ^ <*c69*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(c67 ^ <*c69*>),c68] is V15() set
{(c67 ^ <*c69*>),c68} is non empty finite set
{(c67 ^ <*c69*>)} is functional non empty trivial finite V59() 1 -element set
{{(c67 ^ <*c69*>),c68},{(c67 ^ <*c69*>)}} is non empty finite V59() set
c70 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c71 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c70 ^ c71 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c72 is Element of the carrier of s
c73 is Element of the carrier of s
(s,c72,c73) is Element of the carrier of s
the of s . (c72,c73) is Element of the carrier of s
[c72,c73] is V15() set
{c72,c73} is non empty finite set
{c72} is non empty trivial finite 1 -element set
{{c72,c73},{c72}} is non empty finite V59() set
the of s . [c72,c73] is set
[(c70 ^ c71),(s,c72,c73)] is V15() set
{(c70 ^ c71),(s,c72,c73)} is non empty finite set
{(c70 ^ c71)} is functional non empty trivial finite V59() 1 -element set
{{(c70 ^ c71),(s,c72,c73)},{(c70 ^ c71)}} is non empty finite V59() set
[c70,c72] is V15() set
{c70,c72} is non empty finite set
{c70} is functional non empty trivial finite V59() 1 -element set
{{c70,c72},{c70}} is non empty finite V59() set
[c71,c73] is V15() set
{c71,c73} is non empty finite set
{c71} is functional non empty trivial finite V59() 1 -element set
{{c71,c73},{c71}} is non empty finite V59() set
c74 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c75 is Element of the carrier of s
c76 is Element of the carrier of s
(s,c75,c76) is Element of the carrier of s
the of s . (c75,c76) is Element of the carrier of s
[c75,c76] is V15() set
{c75,c76} is non empty finite set
{c75} is non empty trivial finite 1 -element set
{{c75,c76},{c75}} is non empty finite V59() set
the of s . [c75,c76] is set
[c74,(s,c75,c76)] is V15() set
{c74,(s,c75,c76)} is non empty finite set
{c74} is functional non empty trivial finite V59() 1 -element set
{{c74,(s,c75,c76)},{c74}} is non empty finite V59() set
<*c76*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c74 ^ <*c76*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(c74 ^ <*c76*>),c75] is V15() set
{(c74 ^ <*c76*>),c75} is non empty finite set
{(c74 ^ <*c76*>)} is functional non empty trivial finite V59() 1 -element set
{{(c74 ^ <*c76*>),c75},{(c74 ^ <*c76*>)}} is non empty finite V59() set
c78 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c77 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c78 ^ c77 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c79 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c78 ^ c77) ^ c79 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c81 is Element of the carrier of s
[((c78 ^ c77) ^ c79),c81] is V15() set
{((c78 ^ c77) ^ c79),c81} is non empty finite set
{((c78 ^ c77) ^ c79)} is functional non empty trivial finite V59() 1 -element set
{{((c78 ^ c77) ^ c79),c81},{((c78 ^ c77) ^ c79)}} is non empty finite V59() set
c80 is Element of the carrier of s
[c77,c80] is V15() set
{c77,c80} is non empty finite set
{c77} is functional non empty trivial finite V59() 1 -element set
{{c77,c80},{c77}} is non empty finite V59() set
<*c80*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c78 ^ <*c80*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c78 ^ <*c80*>) ^ c79 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c78 ^ <*c80*>) ^ c79),c81] is V15() set
{((c78 ^ <*c80*>) ^ c79),c81} is non empty finite set
{((c78 ^ <*c80*>) ^ c79)} is functional non empty trivial finite V59() 1 -element set
{{((c78 ^ <*c80*>) ^ c79),c81},{((c78 ^ <*c80*>) ^ c79)}} is non empty finite V59() set
c82 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c84 is Element of the carrier of s
c83 is Element of the carrier of s
(s,c84,c83) is Element of the carrier of s
the of s . (c84,c83) is Element of the carrier of s
[c84,c83] is V15() set
{c84,c83} is non empty finite set
{c84} is non empty trivial finite 1 -element set
{{c84,c83},{c84}} is non empty finite V59() set
the of s . [c84,c83] is set
[c82,(s,c84,c83)] is V15() set
{c82,(s,c84,c83)} is non empty finite set
{c82} is functional non empty trivial finite V59() 1 -element set
{{c82,(s,c84,c83)},{c82}} is non empty finite V59() set
<*c84*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*c84*> ^ c82 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(<*c84*> ^ c82),c83] is V15() set
{(<*c84*> ^ c82),c83} is non empty finite set
{(<*c84*> ^ c82)} is functional non empty trivial finite V59() 1 -element set
{{(<*c84*> ^ c82),c83},{(<*c84*> ^ c82)}} is non empty finite V59() set
c86 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c88 is Element of the carrier of s
c89 is Element of the carrier of s
(s,c88,c89) is Element of the carrier of s
the of s . (c88,c89) is Element of the carrier of s
[c88,c89] is V15() set
{c88,c89} is non empty finite set
{c88} is non empty trivial finite 1 -element set
{{c88,c89},{c88}} is non empty finite V59() set
the of s . [c88,c89] is set
<*(s,c88,c89)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c86 ^ <*(s,c88,c89)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c85 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c86 ^ <*(s,c88,c89)*>) ^ c85 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c87 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((c86 ^ <*(s,c88,c89)*>) ^ c85) ^ c87 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c90 is Element of the carrier of s
[(((c86 ^ <*(s,c88,c89)*>) ^ c85) ^ c87),c90] is V15() set
{(((c86 ^ <*(s,c88,c89)*>) ^ c85) ^ c87),c90} is non empty finite set
{(((c86 ^ <*(s,c88,c89)*>) ^ c85) ^ c87)} is functional non empty trivial finite V59() 1 -element set
{{(((c86 ^ <*(s,c88,c89)*>) ^ c85) ^ c87),c90},{(((c86 ^ <*(s,c88,c89)*>) ^ c85) ^ c87)}} is non empty finite V59() set
[c85,c89] is V15() set
{c85,c89} is non empty finite set
{c85} is functional non empty trivial finite V59() 1 -element set
{{c85,c89},{c85}} is non empty finite V59() set
<*c88*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c86 ^ <*c88*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c86 ^ <*c88*>) ^ c87 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c86 ^ <*c88*>) ^ c87),c90] is V15() set
{((c86 ^ <*c88*>) ^ c87),c90} is non empty finite set
{((c86 ^ <*c88*>) ^ c87)} is functional non empty trivial finite V59() 1 -element set
{{((c86 ^ <*c88*>) ^ c87),c90},{((c86 ^ <*c88*>) ^ c87)}} is non empty finite V59() set
c91 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c93 is Element of the carrier of s
c92 is Element of the carrier of s
(s,c93,c92) is Element of the carrier of s
the of s . (c93,c92) is Element of the carrier of s
[c93,c92] is V15() set
{c93,c92} is non empty finite set
{c93} is non empty trivial finite 1 -element set
{{c93,c92},{c93}} is non empty finite V59() set
the of s . [c93,c92] is set
[c91,(s,c93,c92)] is V15() set
{c91,(s,c93,c92)} is non empty finite set
{c91} is functional non empty trivial finite V59() 1 -element set
{{c91,(s,c93,c92)},{c91}} is non empty finite V59() set
<*c93*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*c93*> ^ c91 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(<*c93*> ^ c91),c92] is V15() set
{(<*c93*> ^ c91),c92} is non empty finite set
{(<*c93*> ^ c91)} is functional non empty trivial finite V59() 1 -element set
{{(<*c93*> ^ c91),c92},{(<*c93*> ^ c91)}} is non empty finite V59() set
c95 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c94 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c95 ^ c94 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c98 is Element of the carrier of s
c97 is Element of the carrier of s
(s,c98,c97) is Element of the carrier of s
the of s . (c98,c97) is Element of the carrier of s
[c98,c97] is V15() set
{c98,c97} is non empty finite set
{c98} is non empty trivial finite 1 -element set
{{c98,c97},{c98}} is non empty finite V59() set
the of s . [c98,c97] is set
<*(s,c98,c97)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c95 ^ c94) ^ <*(s,c98,c97)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c96 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((c95 ^ c94) ^ <*(s,c98,c97)*>) ^ c96 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c99 is Element of the carrier of s
[(((c95 ^ c94) ^ <*(s,c98,c97)*>) ^ c96),c99] is V15() set
{(((c95 ^ c94) ^ <*(s,c98,c97)*>) ^ c96),c99} is non empty finite set
{(((c95 ^ c94) ^ <*(s,c98,c97)*>) ^ c96)} is functional non empty trivial finite V59() 1 -element set
{{(((c95 ^ c94) ^ <*(s,c98,c97)*>) ^ c96),c99},{(((c95 ^ c94) ^ <*(s,c98,c97)*>) ^ c96)}} is non empty finite V59() set
[c94,c98] is V15() set
{c94,c98} is non empty finite set
{c94} is functional non empty trivial finite V59() 1 -element set
{{c94,c98},{c94}} is non empty finite V59() set
<*c97*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c95 ^ <*c97*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c95 ^ <*c97*>) ^ c96 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c95 ^ <*c97*>) ^ c96),c99] is V15() set
{((c95 ^ <*c97*>) ^ c96),c99} is non empty finite set
{((c95 ^ <*c97*>) ^ c96)} is functional non empty trivial finite V59() 1 -element set
{{((c95 ^ <*c97*>) ^ c96),c99},{((c95 ^ <*c97*>) ^ c96)}} is non empty finite V59() set
c100 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c102 is Element of the carrier of s
c101 is Element of the carrier of s
(s,c102,c101) is Element of the carrier of s
the of s . (c102,c101) is Element of the carrier of s
[c102,c101] is V15() set
{c102,c101} is non empty finite set
{c102} is non empty trivial finite 1 -element set
{{c102,c101},{c102}} is non empty finite V59() set
the of s . [c102,c101] is set
[c100,(s,c102,c101)] is V15() set
{c100,(s,c102,c101)} is non empty finite set
{c100} is functional non empty trivial finite V59() 1 -element set
{{c100,(s,c102,c101)},{c100}} is non empty finite V59() set
<*c102*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*c102*> ^ c100 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(<*c102*> ^ c100),c101] is V15() set
{(<*c102*> ^ c100),c101} is non empty finite set
{(<*c102*> ^ c100)} is functional non empty trivial finite V59() 1 -element set
{{(<*c102*> ^ c100),c101},{(<*c102*> ^ c100)}} is non empty finite V59() set
c103 is Element of the carrier of s
c104 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c106 is Element of the carrier of s
c105 is Element of the carrier of s
(s,c106,c105) is Element of the carrier of s
the of s . (c106,c105) is Element of the carrier of s
[c106,c105] is V15() set
{c106,c105} is non empty finite set
{c106} is non empty trivial finite 1 -element set
{{c106,c105},{c106}} is non empty finite V59() set
the of s . [c106,c105] is set
[c104,(s,c106,c105)] is V15() set
{c104,(s,c106,c105)} is non empty finite set
{c104} is functional non empty trivial finite V59() 1 -element set
{{c104,(s,c106,c105)},{c104}} is non empty finite V59() set
<*c106*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*c106*> ^ c104 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(<*c106*> ^ c104),c105] is V15() set
{(<*c106*> ^ c104),c105} is non empty finite set
{(<*c106*> ^ c104)} is functional non empty trivial finite V59() 1 -element set
{{(<*c106*> ^ c104),c105},{(<*c106*> ^ c104)}} is non empty finite V59() set
c107 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c108 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c107 ^ c108 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c109 is Element of the carrier of s
c110 is Element of the carrier of s
(s,c109,c110) is Element of the carrier of s
the of s . (c109,c110) is Element of the carrier of s
[c109,c110] is V15() set
{c109,c110} is non empty finite set
{c109} is non empty trivial finite 1 -element set
{{c109,c110},{c109}} is non empty finite V59() set
the of s . [c109,c110] is set
[(c107 ^ c108),(s,c109,c110)] is V15() set
{(c107 ^ c108),(s,c109,c110)} is non empty finite set
{(c107 ^ c108)} is functional non empty trivial finite V59() 1 -element set
{{(c107 ^ c108),(s,c109,c110)},{(c107 ^ c108)}} is non empty finite V59() set
[c107,c109] is V15() set
{c107,c109} is non empty finite set
{c107} is functional non empty trivial finite V59() 1 -element set
{{c107,c109},{c107}} is non empty finite V59() set
[c108,c110] is V15() set
{c108,c110} is non empty finite set
{c108} is functional non empty trivial finite V59() 1 -element set
{{c108,c110},{c108}} is non empty finite V59() set
c111 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c113 is Element of the carrier of s
c112 is Element of the carrier of s
(s,c113,c112) is Element of the carrier of s
the of s . (c113,c112) is Element of the carrier of s
[c113,c112] is V15() set
{c113,c112} is non empty finite set
{c113} is non empty trivial finite 1 -element set
{{c113,c112},{c113}} is non empty finite V59() set
the of s . [c113,c112] is set
[c111,(s,c113,c112)] is V15() set
{c111,(s,c113,c112)} is non empty finite set
{c111} is functional non empty trivial finite V59() 1 -element set
{{c111,(s,c113,c112)},{c111}} is non empty finite V59() set
<*c113*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*c113*> ^ c111 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[(<*c113*> ^ c111),c112] is V15() set
{(<*c113*> ^ c111),c112} is non empty finite set
{(<*c113*> ^ c111)} is functional non empty trivial finite V59() 1 -element set
{{(<*c113*> ^ c111),c112},{(<*c113*> ^ c111)}} is non empty finite V59() set
c115 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c114 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c115 ^ c114 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c116 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c115 ^ c114) ^ c116 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c118 is Element of the carrier of s
[((c115 ^ c114) ^ c116),c118] is V15() set
{((c115 ^ c114) ^ c116),c118} is non empty finite set
{((c115 ^ c114) ^ c116)} is functional non empty trivial finite V59() 1 -element set
{{((c115 ^ c114) ^ c116),c118},{((c115 ^ c114) ^ c116)}} is non empty finite V59() set
c117 is Element of the carrier of s
[c114,c117] is V15() set
{c114,c117} is non empty finite set
{c114} is functional non empty trivial finite V59() 1 -element set
{{c114,c117},{c114}} is non empty finite V59() set
<*c117*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c115 ^ <*c117*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c115 ^ <*c117*>) ^ c116 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c115 ^ <*c117*>) ^ c116),c118] is V15() set
{((c115 ^ <*c117*>) ^ c116),c118} is non empty finite set
{((c115 ^ <*c117*>) ^ c116)} is functional non empty trivial finite V59() 1 -element set
{{((c115 ^ <*c117*>) ^ c116),c118},{((c115 ^ <*c117*>) ^ c116)}} is non empty finite V59() set
c120 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c122 is Element of the carrier of s
c123 is Element of the carrier of s
(s,c122,c123) is Element of the carrier of s
the of s . (c122,c123) is Element of the carrier of s
[c122,c123] is V15() set
{c122,c123} is non empty finite set
{c122} is non empty trivial finite 1 -element set
{{c122,c123},{c122}} is non empty finite V59() set
the of s . [c122,c123] is set
<*(s,c122,c123)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c120 ^ <*(s,c122,c123)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c119 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c120 ^ <*(s,c122,c123)*>) ^ c119 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c121 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((c120 ^ <*(s,c122,c123)*>) ^ c119) ^ c121 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c124 is Element of the carrier of s
[(((c120 ^ <*(s,c122,c123)*>) ^ c119) ^ c121),c124] is V15() set
{(((c120 ^ <*(s,c122,c123)*>) ^ c119) ^ c121),c124} is non empty finite set
{(((c120 ^ <*(s,c122,c123)*>) ^ c119) ^ c121)} is functional non empty trivial finite V59() 1 -element set
{{(((c120 ^ <*(s,c122,c123)*>) ^ c119) ^ c121),c124},{(((c120 ^ <*(s,c122,c123)*>) ^ c119) ^ c121)}} is non empty finite V59() set
[c119,c123] is V15() set
{c119,c123} is non empty finite set
{c119} is functional non empty trivial finite V59() 1 -element set
{{c119,c123},{c119}} is non empty finite V59() set
<*c122*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c120 ^ <*c122*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c120 ^ <*c122*>) ^ c121 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c120 ^ <*c122*>) ^ c121),c124] is V15() set
{((c120 ^ <*c122*>) ^ c121),c124} is non empty finite set
{((c120 ^ <*c122*>) ^ c121)} is functional non empty trivial finite V59() 1 -element set
{{((c120 ^ <*c122*>) ^ c121),c124},{((c120 ^ <*c122*>) ^ c121)}} is non empty finite V59() set
c126 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c125 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c126 ^ c125 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c129 is Element of the carrier of s
c128 is Element of the carrier of s
(s,c129,c128) is Element of the carrier of s
the of s . (c129,c128) is Element of the carrier of s
[c129,c128] is V15() set
{c129,c128} is non empty finite set
{c129} is non empty trivial finite 1 -element set
{{c129,c128},{c129}} is non empty finite V59() set
the of s . [c129,c128] is set
<*(s,c129,c128)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c126 ^ c125) ^ <*(s,c129,c128)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c127 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((c126 ^ c125) ^ <*(s,c129,c128)*>) ^ c127 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c130 is Element of the carrier of s
[(((c126 ^ c125) ^ <*(s,c129,c128)*>) ^ c127),c130] is V15() set
{(((c126 ^ c125) ^ <*(s,c129,c128)*>) ^ c127),c130} is non empty finite set
{(((c126 ^ c125) ^ <*(s,c129,c128)*>) ^ c127)} is functional non empty trivial finite V59() 1 -element set
{{(((c126 ^ c125) ^ <*(s,c129,c128)*>) ^ c127),c130},{(((c126 ^ c125) ^ <*(s,c129,c128)*>) ^ c127)}} is non empty finite V59() set
[c125,c129] is V15() set
{c125,c129} is non empty finite set
{c125} is functional non empty trivial finite V59() 1 -element set
{{c125,c129},{c125}} is non empty finite V59() set
<*c128*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c126 ^ <*c128*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c126 ^ <*c128*>) ^ c127 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c126 ^ <*c128*>) ^ c127),c130] is V15() set
{((c126 ^ <*c128*>) ^ c127),c130} is non empty finite set
{((c126 ^ <*c128*>) ^ c127)} is functional non empty trivial finite V59() 1 -element set
{{((c126 ^ <*c128*>) ^ c127),c130},{((c126 ^ <*c128*>) ^ c127)}} is non empty finite V59() set
c132 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c134 is Element of the carrier of s
c135 is Element of the carrier of s
(s,c134,c135) is Element of the carrier of s
the of s . (c134,c135) is Element of the carrier of s
[c134,c135] is V15() set
{c134,c135} is non empty finite set
{c134} is non empty trivial finite 1 -element set
{{c134,c135},{c134}} is non empty finite V59() set
the of s . [c134,c135] is set
<*(s,c134,c135)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c132 ^ <*(s,c134,c135)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c131 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c132 ^ <*(s,c134,c135)*>) ^ c131 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c133 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((c132 ^ <*(s,c134,c135)*>) ^ c131) ^ c133 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c136 is Element of the carrier of s
[(((c132 ^ <*(s,c134,c135)*>) ^ c131) ^ c133),c136] is V15() set
{(((c132 ^ <*(s,c134,c135)*>) ^ c131) ^ c133),c136} is non empty finite set
{(((c132 ^ <*(s,c134,c135)*>) ^ c131) ^ c133)} is functional non empty trivial finite V59() 1 -element set
{{(((c132 ^ <*(s,c134,c135)*>) ^ c131) ^ c133),c136},{(((c132 ^ <*(s,c134,c135)*>) ^ c131) ^ c133)}} is non empty finite V59() set
[c131,c135] is V15() set
{c131,c135} is non empty finite set
{c131} is functional non empty trivial finite V59() 1 -element set
{{c131,c135},{c131}} is non empty finite V59() set
<*c134*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c132 ^ <*c134*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c132 ^ <*c134*>) ^ c133 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c132 ^ <*c134*>) ^ c133),c136] is V15() set
{((c132 ^ <*c134*>) ^ c133),c136} is non empty finite set
{((c132 ^ <*c134*>) ^ c133)} is functional non empty trivial finite V59() 1 -element set
{{((c132 ^ <*c134*>) ^ c133),c136},{((c132 ^ <*c134*>) ^ c133)}} is non empty finite V59() set
c137 is Element of the carrier of s
c139 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c141 is Element of the carrier of s
c142 is Element of the carrier of s
(s,c141,c142) is Element of the carrier of s
the of s . (c141,c142) is Element of the carrier of s
[c141,c142] is V15() set
{c141,c142} is non empty finite set
{c141} is non empty trivial finite 1 -element set
{{c141,c142},{c141}} is non empty finite V59() set
the of s . [c141,c142] is set
<*(s,c141,c142)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c139 ^ <*(s,c141,c142)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c138 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c139 ^ <*(s,c141,c142)*>) ^ c138 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c140 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((c139 ^ <*(s,c141,c142)*>) ^ c138) ^ c140 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c143 is Element of the carrier of s
[(((c139 ^ <*(s,c141,c142)*>) ^ c138) ^ c140),c143] is V15() set
{(((c139 ^ <*(s,c141,c142)*>) ^ c138) ^ c140),c143} is non empty finite set
{(((c139 ^ <*(s,c141,c142)*>) ^ c138) ^ c140)} is functional non empty trivial finite V59() 1 -element set
{{(((c139 ^ <*(s,c141,c142)*>) ^ c138) ^ c140),c143},{(((c139 ^ <*(s,c141,c142)*>) ^ c138) ^ c140)}} is non empty finite V59() set
[c138,c142] is V15() set
{c138,c142} is non empty finite set
{c138} is functional non empty trivial finite V59() 1 -element set
{{c138,c142},{c138}} is non empty finite V59() set
<*c141*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c139 ^ <*c141*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c139 ^ <*c141*>) ^ c140 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c139 ^ <*c141*>) ^ c140),c143] is V15() set
{((c139 ^ <*c141*>) ^ c140),c143} is non empty finite set
{((c139 ^ <*c141*>) ^ c140)} is functional non empty trivial finite V59() 1 -element set
{{((c139 ^ <*c141*>) ^ c140),c143},{((c139 ^ <*c141*>) ^ c140)}} is non empty finite V59() set
c144 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c145 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c144 ^ c145 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c146 is Element of the carrier of s
c147 is Element of the carrier of s
(s,c146,c147) is Element of the carrier of s
the of s . (c146,c147) is Element of the carrier of s
[c146,c147] is V15() set
{c146,c147} is non empty finite set
{c146} is non empty trivial finite 1 -element set
{{c146,c147},{c146}} is non empty finite V59() set
the of s . [c146,c147] is set
[(c144 ^ c145),(s,c146,c147)] is V15() set
{(c144 ^ c145),(s,c146,c147)} is non empty finite set
{(c144 ^ c145)} is functional non empty trivial finite V59() 1 -element set
{{(c144 ^ c145),(s,c146,c147)},{(c144 ^ c145)}} is non empty finite V59() set
[c144,c146] is V15() set
{c144,c146} is non empty finite set
{c144} is functional non empty trivial finite V59() 1 -element set
{{c144,c146},{c144}} is non empty finite V59() set
[c145,c147] is V15() set
{c145,c147} is non empty finite set
{c145} is functional non empty trivial finite V59() 1 -element set
{{c145,c147},{c145}} is non empty finite V59() set
c149 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c151 is Element of the carrier of s
c152 is Element of the carrier of s
(s,c151,c152) is Element of the carrier of s
the of s . (c151,c152) is Element of the carrier of s
[c151,c152] is V15() set
{c151,c152} is non empty finite set
{c151} is non empty trivial finite 1 -element set
{{c151,c152},{c151}} is non empty finite V59() set
the of s . [c151,c152] is set
<*(s,c151,c152)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c149 ^ <*(s,c151,c152)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c148 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c149 ^ <*(s,c151,c152)*>) ^ c148 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c150 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((c149 ^ <*(s,c151,c152)*>) ^ c148) ^ c150 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c153 is Element of the carrier of s
[(((c149 ^ <*(s,c151,c152)*>) ^ c148) ^ c150),c153] is V15() set
{(((c149 ^ <*(s,c151,c152)*>) ^ c148) ^ c150),c153} is non empty finite set
{(((c149 ^ <*(s,c151,c152)*>) ^ c148) ^ c150)} is functional non empty trivial finite V59() 1 -element set
{{(((c149 ^ <*(s,c151,c152)*>) ^ c148) ^ c150),c153},{(((c149 ^ <*(s,c151,c152)*>) ^ c148) ^ c150)}} is non empty finite V59() set
[c148,c152] is V15() set
{c148,c152} is non empty finite set
{c148} is functional non empty trivial finite V59() 1 -element set
{{c148,c152},{c148}} is non empty finite V59() set
<*c151*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c149 ^ <*c151*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c149 ^ <*c151*>) ^ c150 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c149 ^ <*c151*>) ^ c150),c153] is V15() set
{((c149 ^ <*c151*>) ^ c150),c153} is non empty finite set
{((c149 ^ <*c151*>) ^ c150)} is functional non empty trivial finite V59() 1 -element set
{{((c149 ^ <*c151*>) ^ c150),c153},{((c149 ^ <*c151*>) ^ c150)}} is non empty finite V59() set
c155 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c154 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c155 ^ c154 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c156 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c155 ^ c154) ^ c156 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c158 is Element of the carrier of s
[((c155 ^ c154) ^ c156),c158] is V15() set
{((c155 ^ c154) ^ c156),c158} is non empty finite set
{((c155 ^ c154) ^ c156)} is functional non empty trivial finite V59() 1 -element set
{{((c155 ^ c154) ^ c156),c158},{((c155 ^ c154) ^ c156)}} is non empty finite V59() set
c157 is Element of the carrier of s
[c154,c157] is V15() set
{c154,c157} is non empty finite set
{c154} is functional non empty trivial finite V59() 1 -element set
{{c154,c157},{c154}} is non empty finite V59() set
<*c157*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c155 ^ <*c157*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c155 ^ <*c157*>) ^ c156 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c155 ^ <*c157*>) ^ c156),c158] is V15() set
{((c155 ^ <*c157*>) ^ c156),c158} is non empty finite set
{((c155 ^ <*c157*>) ^ c156)} is functional non empty trivial finite V59() 1 -element set
{{((c155 ^ <*c157*>) ^ c156),c158},{((c155 ^ <*c157*>) ^ c156)}} is non empty finite V59() set
c160 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c159 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c160 ^ c159 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c163 is Element of the carrier of s
c162 is Element of the carrier of s
(s,c163,c162) is Element of the carrier of s
the of s . (c163,c162) is Element of the carrier of s
[c163,c162] is V15() set
{c163,c162} is non empty finite set
{c163} is non empty trivial finite 1 -element set
{{c163,c162},{c163}} is non empty finite V59() set
the of s . [c163,c162] is set
<*(s,c163,c162)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c160 ^ c159) ^ <*(s,c163,c162)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c161 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((c160 ^ c159) ^ <*(s,c163,c162)*>) ^ c161 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c164 is Element of the carrier of s
[(((c160 ^ c159) ^ <*(s,c163,c162)*>) ^ c161),c164] is V15() set
{(((c160 ^ c159) ^ <*(s,c163,c162)*>) ^ c161),c164} is non empty finite set
{(((c160 ^ c159) ^ <*(s,c163,c162)*>) ^ c161)} is functional non empty trivial finite V59() 1 -element set
{{(((c160 ^ c159) ^ <*(s,c163,c162)*>) ^ c161),c164},{(((c160 ^ c159) ^ <*(s,c163,c162)*>) ^ c161)}} is non empty finite V59() set
[c159,c163] is V15() set
{c159,c163} is non empty finite set
{c159} is functional non empty trivial finite V59() 1 -element set
{{c159,c163},{c159}} is non empty finite V59() set
<*c162*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c160 ^ <*c162*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c160 ^ <*c162*>) ^ c161 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c160 ^ <*c162*>) ^ c161),c164] is V15() set
{((c160 ^ <*c162*>) ^ c161),c164} is non empty finite set
{((c160 ^ <*c162*>) ^ c161)} is functional non empty trivial finite V59() 1 -element set
{{((c160 ^ <*c162*>) ^ c161),c164},{((c160 ^ <*c162*>) ^ c161)}} is non empty finite V59() set
c165 is Element of the carrier of s
c167 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c166 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c167 ^ c166 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c170 is Element of the carrier of s
c169 is Element of the carrier of s
(s,c170,c169) is Element of the carrier of s
the of s . (c170,c169) is Element of the carrier of s
[c170,c169] is V15() set
{c170,c169} is non empty finite set
{c170} is non empty trivial finite 1 -element set
{{c170,c169},{c170}} is non empty finite V59() set
the of s . [c170,c169] is set
<*(s,c170,c169)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c167 ^ c166) ^ <*(s,c170,c169)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c168 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((c167 ^ c166) ^ <*(s,c170,c169)*>) ^ c168 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c171 is Element of the carrier of s
[(((c167 ^ c166) ^ <*(s,c170,c169)*>) ^ c168),c171] is V15() set
{(((c167 ^ c166) ^ <*(s,c170,c169)*>) ^ c168),c171} is non empty finite set
{(((c167 ^ c166) ^ <*(s,c170,c169)*>) ^ c168)} is functional non empty trivial finite V59() 1 -element set
{{(((c167 ^ c166) ^ <*(s,c170,c169)*>) ^ c168),c171},{(((c167 ^ c166) ^ <*(s,c170,c169)*>) ^ c168)}} is non empty finite V59() set
[c166,c170] is V15() set
{c166,c170} is non empty finite set
{c166} is functional non empty trivial finite V59() 1 -element set
{{c166,c170},{c166}} is non empty finite V59() set
<*c169*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c167 ^ <*c169*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c167 ^ <*c169*>) ^ c168 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c167 ^ <*c169*>) ^ c168),c171] is V15() set
{((c167 ^ <*c169*>) ^ c168),c171} is non empty finite set
{((c167 ^ <*c169*>) ^ c168)} is functional non empty trivial finite V59() 1 -element set
{{((c167 ^ <*c169*>) ^ c168),c171},{((c167 ^ <*c169*>) ^ c168)}} is non empty finite V59() set
c172 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c173 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c172 ^ c173 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c174 is Element of the carrier of s
c175 is Element of the carrier of s
(s,c174,c175) is Element of the carrier of s
the of s . (c174,c175) is Element of the carrier of s
[c174,c175] is V15() set
{c174,c175} is non empty finite set
{c174} is non empty trivial finite 1 -element set
{{c174,c175},{c174}} is non empty finite V59() set
the of s . [c174,c175] is set
[(c172 ^ c173),(s,c174,c175)] is V15() set
{(c172 ^ c173),(s,c174,c175)} is non empty finite set
{(c172 ^ c173)} is functional non empty trivial finite V59() 1 -element set
{{(c172 ^ c173),(s,c174,c175)},{(c172 ^ c173)}} is non empty finite V59() set
[c172,c174] is V15() set
{c172,c174} is non empty finite set
{c172} is functional non empty trivial finite V59() 1 -element set
{{c172,c174},{c172}} is non empty finite V59() set
[c173,c175] is V15() set
{c173,c175} is non empty finite set
{c173} is functional non empty trivial finite V59() 1 -element set
{{c173,c175},{c173}} is non empty finite V59() set
c177 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c176 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c177 ^ c176 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c180 is Element of the carrier of s
c179 is Element of the carrier of s
(s,c180,c179) is Element of the carrier of s
the of s . (c180,c179) is Element of the carrier of s
[c180,c179] is V15() set
{c180,c179} is non empty finite set
{c180} is non empty trivial finite 1 -element set
{{c180,c179},{c180}} is non empty finite V59() set
the of s . [c180,c179] is set
<*(s,c180,c179)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c177 ^ c176) ^ <*(s,c180,c179)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c178 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((c177 ^ c176) ^ <*(s,c180,c179)*>) ^ c178 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c181 is Element of the carrier of s
[(((c177 ^ c176) ^ <*(s,c180,c179)*>) ^ c178),c181] is V15() set
{(((c177 ^ c176) ^ <*(s,c180,c179)*>) ^ c178),c181} is non empty finite set
{(((c177 ^ c176) ^ <*(s,c180,c179)*>) ^ c178)} is functional non empty trivial finite V59() 1 -element set
{{(((c177 ^ c176) ^ <*(s,c180,c179)*>) ^ c178),c181},{(((c177 ^ c176) ^ <*(s,c180,c179)*>) ^ c178)}} is non empty finite V59() set
[c176,c180] is V15() set
{c176,c180} is non empty finite set
{c176} is functional non empty trivial finite V59() 1 -element set
{{c176,c180},{c176}} is non empty finite V59() set
<*c179*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c177 ^ <*c179*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c177 ^ <*c179*>) ^ c178 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c177 ^ <*c179*>) ^ c178),c181] is V15() set
{((c177 ^ <*c179*>) ^ c178),c181} is non empty finite set
{((c177 ^ <*c179*>) ^ c178)} is functional non empty trivial finite V59() 1 -element set
{{((c177 ^ <*c179*>) ^ c178),c181},{((c177 ^ <*c179*>) ^ c178)}} is non empty finite V59() set
c183 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c182 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c183 ^ c182 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c184 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c183 ^ c182) ^ c184 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c186 is Element of the carrier of s
[((c183 ^ c182) ^ c184),c186] is V15() set
{((c183 ^ c182) ^ c184),c186} is non empty finite set
{((c183 ^ c182) ^ c184)} is functional non empty trivial finite V59() 1 -element set
{{((c183 ^ c182) ^ c184),c186},{((c183 ^ c182) ^ c184)}} is non empty finite V59() set
c185 is Element of the carrier of s
[c182,c185] is V15() set
{c182,c185} is non empty finite set
{c182} is functional non empty trivial finite V59() 1 -element set
{{c182,c185},{c182}} is non empty finite V59() set
<*c185*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c183 ^ <*c185*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c183 ^ <*c185*>) ^ c184 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c183 ^ <*c185*>) ^ c184),c186] is V15() set
{((c183 ^ <*c185*>) ^ c184),c186} is non empty finite set
{((c183 ^ <*c185*>) ^ c184)} is functional non empty trivial finite V59() 1 -element set
{{((c183 ^ <*c185*>) ^ c184),c186},{((c183 ^ <*c185*>) ^ c184)}} is non empty finite V59() set
c187 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c188 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c187 ^ c188 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c189 is Element of the carrier of s
c190 is Element of the carrier of s
(s,c189,c190) is Element of the carrier of s
the of s . (c189,c190) is Element of the carrier of s
[c189,c190] is V15() set
{c189,c190} is non empty finite set
{c189} is non empty trivial finite 1 -element set
{{c189,c190},{c189}} is non empty finite V59() set
the of s . [c189,c190] is set
[(c187 ^ c188),(s,c189,c190)] is V15() set
{(c187 ^ c188),(s,c189,c190)} is non empty finite set
{(c187 ^ c188)} is functional non empty trivial finite V59() 1 -element set
{{(c187 ^ c188),(s,c189,c190)},{(c187 ^ c188)}} is non empty finite V59() set
[c187,c189] is V15() set
{c187,c189} is non empty finite set
{c187} is functional non empty trivial finite V59() 1 -element set
{{c187,c189},{c187}} is non empty finite V59() set
[c188,c190] is V15() set
{c188,c190} is non empty finite set
{c188} is functional non empty trivial finite V59() 1 -element set
{{c188,c190},{c188}} is non empty finite V59() set
c191 is Element of the carrier of s
c193 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c192 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c193 ^ c192 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c194 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c193 ^ c192) ^ c194 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c196 is Element of the carrier of s
[((c193 ^ c192) ^ c194),c196] is V15() set
{((c193 ^ c192) ^ c194),c196} is non empty finite set
{((c193 ^ c192) ^ c194)} is functional non empty trivial finite V59() 1 -element set
{{((c193 ^ c192) ^ c194),c196},{((c193 ^ c192) ^ c194)}} is non empty finite V59() set
c195 is Element of the carrier of s
[c192,c195] is V15() set
{c192,c195} is non empty finite set
{c192} is functional non empty trivial finite V59() 1 -element set
{{c192,c195},{c192}} is non empty finite V59() set
<*c195*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c193 ^ <*c195*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c193 ^ <*c195*>) ^ c194 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c193 ^ <*c195*>) ^ c194),c196] is V15() set
{((c193 ^ <*c195*>) ^ c194),c196} is non empty finite set
{((c193 ^ <*c195*>) ^ c194)} is functional non empty trivial finite V59() 1 -element set
{{((c193 ^ <*c195*>) ^ c194),c196},{((c193 ^ <*c195*>) ^ c194)}} is non empty finite V59() set
c197 is Element of the carrier of s
c198 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c199 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c198 ^ c199 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c200 is Element of the carrier of s
c201 is Element of the carrier of s
(s,c200,c201) is Element of the carrier of s
the of s . (c200,c201) is Element of the carrier of s
[c200,c201] is V15() set
{c200,c201} is non empty finite set
{c200} is non empty trivial finite 1 -element set
{{c200,c201},{c200}} is non empty finite V59() set
the of s . [c200,c201] is set
[(c198 ^ c199),(s,c200,c201)] is V15() set
{(c198 ^ c199),(s,c200,c201)} is non empty finite set
{(c198 ^ c199)} is functional non empty trivial finite V59() 1 -element set
{{(c198 ^ c199),(s,c200,c201)},{(c198 ^ c199)}} is non empty finite V59() set
[c198,c200] is V15() set
{c198,c200} is non empty finite set
{c198} is functional non empty trivial finite V59() 1 -element set
{{c198,c200},{c198}} is non empty finite V59() set
[c199,c201] is V15() set
{c199,c201} is non empty finite set
{c199} is functional non empty trivial finite V59() 1 -element set
{{c199,c201},{c199}} is non empty finite V59() set
c203 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c202 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c203 ^ c202 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c204 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c203 ^ c202) ^ c204 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c206 is Element of the carrier of s
[((c203 ^ c202) ^ c204),c206] is V15() set
{((c203 ^ c202) ^ c204),c206} is non empty finite set
{((c203 ^ c202) ^ c204)} is functional non empty trivial finite V59() 1 -element set
{{((c203 ^ c202) ^ c204),c206},{((c203 ^ c202) ^ c204)}} is non empty finite V59() set
c205 is Element of the carrier of s
[c202,c205] is V15() set
{c202,c205} is non empty finite set
{c202} is functional non empty trivial finite V59() 1 -element set
{{c202,c205},{c202}} is non empty finite V59() set
<*c205*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
c203 ^ <*c205*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(c203 ^ <*c205*>) ^ c204 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
[((c203 ^ <*c205*>) ^ c204),c206] is V15() set
{((c203 ^ <*c205*>) ^ c204),c206} is non empty finite set
{((c203 ^ <*c205*>) ^ c204)} is functional non empty trivial finite V59() 1 -element set
{{((c203 ^ <*c205*>) ^ c204),c206},{((c203 ^ <*c205*>) ^ c204)}} is non empty finite V59() set
s is non empty ()
the carrier of s is non empty set
s is non empty ()
the carrier of s is non empty set
s is non empty ()
the carrier of s is non empty set
x is Relation-like the carrier of s -valued Function-like finite DecoratedTree-like set
proj1 x is non empty finite V70() set
y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
x . y is set
z is Relation-like the carrier of s -valued Function-like DecoratedTree-like set
proj1 z is non empty V70() set
z is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 z
z . z is Element of the carrier of s
s is non empty ()
the carrier of s is non empty set
s is non empty ()
the carrier of s is non empty set
s is non empty ()
the carrier of s is non empty set
x is Element of the carrier of s
y is Relation-like the carrier of s -valued Function-like finite DecoratedTree-like set
z is Relation-like the carrier of s -valued Function-like finite DecoratedTree-like set
s is non empty ()
the carrier of s is non empty set
x is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is functional non empty trivial finite V59() 1 -element set
{{x,y},{x}} is non empty finite V59() set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
the Element of the carrier of s is Element of the carrier of s
<* the Element of the carrier of s*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,<* the Element of the carrier of s*>, the Element of the carrier of s) is V15() Element of [:( the carrier of s *), the carrier of s:]
{<* the Element of the carrier of s*>, the Element of the carrier of s} is non empty finite set
{<* the Element of the carrier of s*>} is functional non empty trivial finite V59() 1 -element set
{{<* the Element of the carrier of s*>, the Element of the carrier of s},{<* the Element of the carrier of s*>}} is non empty finite V59() set
[(s,<* the Element of the carrier of s*>, the Element of the carrier of s),0] is V15() set
{(s,<* the Element of the carrier of s*>, the Element of the carrier of s),0} is non empty finite set
{(s,<* the Element of the carrier of s*>, the Element of the carrier of s)} is Relation-like Function-like constant non empty trivial finite 1 -element set
{{(s,<* the Element of the carrier of s*>, the Element of the carrier of s),0},{(s,<* the Element of the carrier of s*>, the Element of the carrier of s)}} is non empty finite V59() set
{{}} --> [(s,<* the Element of the carrier of s*>, the Element of the carrier of s),0] is Relation-like {{}} -defined {[(s,<* the Element of the carrier of s*>, the Element of the carrier of s),0]} -valued Function-like V18({{}},{[(s,<* the Element of the carrier of s*>, the Element of the carrier of s),0]}) finite Element of bool [:{{}},{[(s,<* the Element of the carrier of s*>, the Element of the carrier of s),0]}:]
{[(s,<* the Element of the carrier of s*>, the Element of the carrier of s),0]} is Relation-like Function-like constant non empty trivial finite 1 -element set
[:{{}},{[(s,<* the Element of the carrier of s*>, the Element of the carrier of s),0]}:] is Relation-like non empty finite set
bool [:{{}},{[(s,<* the Element of the carrier of s*>, the Element of the carrier of s),0]}:] is non empty finite V59() set
proj1 ({{}} --> [(s,<* the Element of the carrier of s*>, the Element of the carrier of s),0]) is finite set
[:H1(s),NAT:] is Relation-like RAT -valued INT -valued V38() V39() V40() V41() set
z is Relation-like Function-like finite DecoratedTree-like set
proj2 z is finite set
z is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like set
proj1 z is non empty finite V70() set
z is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 z
(proj1 z) -level 1 is finite Level of proj1 z
the Element of (proj1 z) -level 1 is Element of (proj1 z) -level 1
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 z : len b1 = 1 } is set
b is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 z
len b is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
branchdeg z is set
succ z is finite Element of bool (proj1 z)
bool (proj1 z) is non empty finite V59() set
card (succ z) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
z . z is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(z . z) `1 is set
(z . z) `2 is set
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
x is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like (s)
proj1 x is non empty finite V70() set
y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
branchdeg y is set
y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
succ y is finite Element of bool (proj1 x)
bool (proj1 x) is non empty finite V59() set
the Element of succ y is Element of succ y
{ (y ^ <*b1*>) where b1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT : y ^ <*b1*> in proj1 x } is set
z is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial V38() V39() V40() V41() V42() V43() V44() V45() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*z*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
x is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like (s)
proj1 x is non empty finite V70() set
y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
branchdeg y is set
y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
succ y is finite Element of bool (proj1 x)
bool (proj1 x) is non empty finite V59() set
{ (y ^ <*b1*>) where b1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT : y ^ <*b1*> in proj1 x } is set
card (succ y) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
z is set
z is set
{z,z} is non empty finite set
z is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial V38() V39() V40() V41() V42() V43() V44() V45() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*z*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
a is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*a*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial V38() V39() V40() V41() V42() V43() V44() V45() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*a*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
x is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like (s)
proj1 x is non empty finite V70() set
y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
x . y is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(x . y) `2 is set
(x . y) `1 is set
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
x is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like (s)
proj1 x is non empty finite V70() set
y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
x . y is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(x . y) `2 is set
y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
(x . y) `1 is set
x . (y ^ <*0*>) is set
(x . (y ^ <*0*>)) `1 is set
branchdeg y is set
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
z is Element of the carrier of s
(s,z,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (z,z) is Element of the carrier of s
[z,z] is V15() set
{z,z} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,z},{z}} is non empty finite V59() set
the of s . [z,z] is set
(s,z,(s,z,z)) is V15() Element of [:( the carrier of s *), the carrier of s:]
{z,(s,z,z)} is non empty finite set
{z} is functional non empty trivial finite V59() 1 -element set
{{z,(s,z,z)},{z}} is non empty finite V59() set
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,(z ^ <*z*>),z) is V15() Element of [:( the carrier of s *), the carrier of s:]
{(z ^ <*z*>),z} is non empty finite set
{(z ^ <*z*>)} is functional non empty trivial finite V59() 1 -element set
{{(z ^ <*z*>),z},{(z ^ <*z*>)}} is non empty finite V59() set
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
x is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like (s)
proj1 x is non empty finite V70() set
y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
x . y is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(x . y) `2 is set
y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
(x . y) `1 is set
x . (y ^ <*0*>) is set
(x . (y ^ <*0*>)) `1 is set
branchdeg y is set
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
z is Element of the carrier of s
(s,z,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (z,z) is Element of the carrier of s
[z,z] is V15() set
{z,z} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,z},{z}} is non empty finite V59() set
the of s . [z,z] is set
(s,z,(s,z,z)) is V15() Element of [:( the carrier of s *), the carrier of s:]
{z,(s,z,z)} is non empty finite set
{z} is functional non empty trivial finite V59() 1 -element set
{{z,(s,z,z)},{z}} is non empty finite V59() set
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*z*> ^ z is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,(<*z*> ^ z),z) is V15() Element of [:( the carrier of s *), the carrier of s:]
{(<*z*> ^ z),z} is non empty finite set
{(<*z*> ^ z)} is functional non empty trivial finite V59() 1 -element set
{{(<*z*> ^ z),z},{(<*z*> ^ z)}} is non empty finite V59() set
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
x is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like (s)
proj1 x is non empty finite V70() set
y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
x . y is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(x . y) `2 is set
y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
(x . y) `1 is set
x . (y ^ <*0*>) is set
(x . (y ^ <*0*>)) `1 is set
x . (y ^ <*1*>) is set
(x . (y ^ <*1*>)) `1 is set
branchdeg y is set
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
a is Element of the carrier of s
b is Element of the carrier of s
(s,a,b) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (a,b) is Element of the carrier of s
[a,b] is V15() set
{a,b} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is non empty finite V59() set
the of s . [a,b] is set
<*(s,a,b)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z ^ <*(s,a,b)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(z ^ <*(s,a,b)*>) ^ z is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((z ^ <*(s,a,b)*>) ^ z) ^ z is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
(s,(((z ^ <*(s,a,b)*>) ^ z) ^ z),z) is V15() Element of [:( the carrier of s *), the carrier of s:]
{(((z ^ <*(s,a,b)*>) ^ z) ^ z),z} is non empty finite set
{(((z ^ <*(s,a,b)*>) ^ z) ^ z)} is functional non empty trivial finite V59() 1 -element set
{{(((z ^ <*(s,a,b)*>) ^ z) ^ z),z},{(((z ^ <*(s,a,b)*>) ^ z) ^ z)}} is non empty finite V59() set
(s,z,b) is V15() Element of [:( the carrier of s *), the carrier of s:]
{z,b} is non empty finite set
{z} is functional non empty trivial finite V59() 1 -element set
{{z,b},{z}} is non empty finite V59() set
<*a*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z ^ <*a*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(z ^ <*a*>) ^ z is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,((z ^ <*a*>) ^ z),z) is V15() Element of [:( the carrier of s *), the carrier of s:]
{((z ^ <*a*>) ^ z),z} is non empty finite set
{((z ^ <*a*>) ^ z)} is functional non empty trivial finite V59() 1 -element set
{{((z ^ <*a*>) ^ z),z},{((z ^ <*a*>) ^ z)}} is non empty finite V59() set
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
x is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like (s)
proj1 x is non empty finite V70() set
y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
x . y is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(x . y) `2 is set
y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
(x . y) `1 is set
x . (y ^ <*0*>) is set
(x . (y ^ <*0*>)) `1 is set
x . (y ^ <*1*>) is set
(x . (y ^ <*1*>)) `1 is set
branchdeg y is set
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z ^ z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
b is Element of the carrier of s
a is Element of the carrier of s
(s,b,a) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (b,a) is Element of the carrier of s
[b,a] is V15() set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V59() set
the of s . [b,a] is set
<*(s,b,a)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(z ^ z) ^ <*(s,b,a)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((z ^ z) ^ <*(s,b,a)*>) ^ z is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
(s,(((z ^ z) ^ <*(s,b,a)*>) ^ z),z) is V15() Element of [:( the carrier of s *), the carrier of s:]
{(((z ^ z) ^ <*(s,b,a)*>) ^ z),z} is non empty finite set
{(((z ^ z) ^ <*(s,b,a)*>) ^ z)} is functional non empty trivial finite V59() 1 -element set
{{(((z ^ z) ^ <*(s,b,a)*>) ^ z),z},{(((z ^ z) ^ <*(s,b,a)*>) ^ z)}} is non empty finite V59() set
(s,z,b) is V15() Element of [:( the carrier of s *), the carrier of s:]
{z,b} is non empty finite set
{z} is functional non empty trivial finite V59() 1 -element set
{{z,b},{z}} is non empty finite V59() set
<*a*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z ^ <*a*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(z ^ <*a*>) ^ z is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,((z ^ <*a*>) ^ z),z) is V15() Element of [:( the carrier of s *), the carrier of s:]
{((z ^ <*a*>) ^ z),z} is non empty finite set
{((z ^ <*a*>) ^ z)} is functional non empty trivial finite V59() 1 -element set
{{((z ^ <*a*>) ^ z),z},{((z ^ <*a*>) ^ z)}} is non empty finite V59() set
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
x is Element of the carrier of s
y is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like (s)
proj1 y is non empty finite V70() set
z is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 y
y . z is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(y . z) `2 is set
z ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
(y . z) `1 is set
y . (z ^ <*0*>) is set
(y . (z ^ <*0*>)) `1 is set
branchdeg z is set
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
a is Element of the carrier of s
(s,z,a) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (z,a) is Element of the carrier of s
[z,a] is V15() set
{z,a} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,a},{z}} is non empty finite V59() set
the of s . [z,a] is set
<*(s,z,a)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z ^ <*(s,z,a)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
b is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(z ^ <*(s,z,a)*>) ^ b is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,((z ^ <*(s,z,a)*>) ^ b),x) is V15() Element of [:( the carrier of s *), the carrier of s:]
{((z ^ <*(s,z,a)*>) ^ b),x} is non empty finite set
{((z ^ <*(s,z,a)*>) ^ b)} is functional non empty trivial finite V59() 1 -element set
{{((z ^ <*(s,z,a)*>) ^ b),x},{((z ^ <*(s,z,a)*>) ^ b)}} is non empty finite V59() set
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*a*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(z ^ <*z*>) ^ <*a*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((z ^ <*z*>) ^ <*a*>) ^ b is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,(((z ^ <*z*>) ^ <*a*>) ^ b),x) is V15() Element of [:( the carrier of s *), the carrier of s:]
{(((z ^ <*z*>) ^ <*a*>) ^ b),x} is non empty finite set
{(((z ^ <*z*>) ^ <*a*>) ^ b)} is functional non empty trivial finite V59() 1 -element set
{{(((z ^ <*z*>) ^ <*a*>) ^ b),x},{(((z ^ <*z*>) ^ <*a*>) ^ b)}} is non empty finite V59() set
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
x is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like (s)
proj1 x is non empty finite V70() set
y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
x . y is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(x . y) `2 is set
y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
(x . y) `1 is set
x . (y ^ <*0*>) is set
(x . (y ^ <*0*>)) `1 is set
x . (y ^ <*1*>) is set
(x . (y ^ <*1*>)) `1 is set
branchdeg y is set
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z ^ z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
a is Element of the carrier of s
(s,z,a) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (z,a) is Element of the carrier of s
[z,a] is V15() set
{z,a} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,a},{z}} is non empty finite V59() set
the of s . [z,a] is set
(s,(z ^ z),(s,z,a)) is V15() Element of [:( the carrier of s *), the carrier of s:]
{(z ^ z),(s,z,a)} is non empty finite set
{(z ^ z)} is functional non empty trivial finite V59() 1 -element set
{{(z ^ z),(s,z,a)},{(z ^ z)}} is non empty finite V59() set
(s,z,z) is V15() Element of [:( the carrier of s *), the carrier of s:]
{z,z} is non empty finite set
{z} is functional non empty trivial finite V59() 1 -element set
{{z,z},{z}} is non empty finite V59() set
(s,z,a) is V15() Element of [:( the carrier of s *), the carrier of s:]
{z,a} is non empty finite set
{z} is functional non empty trivial finite V59() 1 -element set
{{z,a},{z}} is non empty finite V59() set
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
x is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like (s)
proj1 x is non empty finite V70() set
y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
x . y is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(x . y) `2 is set
y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
(x . y) `1 is set
x . (y ^ <*0*>) is set
(x . (y ^ <*0*>)) `1 is set
x . (y ^ <*1*>) is set
(x . (y ^ <*1*>)) `1 is set
branchdeg y is set
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z ^ z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(z ^ z) ^ z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
b is Element of the carrier of s
(s,((z ^ z) ^ z),b) is V15() Element of [:( the carrier of s *), the carrier of s:]
{((z ^ z) ^ z),b} is non empty finite set
{((z ^ z) ^ z)} is functional non empty trivial finite V59() 1 -element set
{{((z ^ z) ^ z),b},{((z ^ z) ^ z)}} is non empty finite V59() set
a is Element of the carrier of s
(s,z,a) is V15() Element of [:( the carrier of s *), the carrier of s:]
{z,a} is non empty finite set
{z} is functional non empty trivial finite V59() 1 -element set
{{z,a},{z}} is non empty finite V59() set
<*a*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z ^ <*a*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(z ^ <*a*>) ^ z is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,((z ^ <*a*>) ^ z),b) is V15() Element of [:( the carrier of s *), the carrier of s:]
{((z ^ <*a*>) ^ z),b} is non empty finite set
{((z ^ <*a*>) ^ z)} is functional non empty trivial finite V59() 1 -element set
{{((z ^ <*a*>) ^ z),b},{((z ^ <*a*>) ^ z)}} is non empty finite V59() set
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
x is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like (s)
proj1 x is non empty finite V70() set
y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
x . y is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(x . y) `2 is set
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
s is non empty ()
the carrier of s is non empty set
[: the carrier of s,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
bool [: the carrier of s,NAT:] is non empty non trivial non finite set
x is Relation-like the carrier of s -defined NAT -valued Function-like V18( the carrier of s, NAT ) V38() V39() V40() V41() Element of bool [: the carrier of s,NAT:]
y is Relation-like the carrier of s -defined NAT -valued Function-like V18( the carrier of s, NAT ) V38() V39() V40() V41() Element of bool [: the carrier of s,NAT:]
z is Element of the carrier of s
x . z is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
(s,z) is Relation-like the carrier of s -valued Function-like finite DecoratedTree-like set
proj1 (s,z) is non empty finite V70() set
card (proj1 (s,z)) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
y . z is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
s is non empty set
[:s,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
bool [:s,NAT:] is non empty non trivial non finite set
x is Relation-like NAT -defined s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of s
y is Relation-like s -defined NAT -valued Function-like V18(s, NAT ) V38() V39() V40() V41() Element of bool [:s,NAT:]
x (#) y is Relation-like NAT -defined NAT -valued RAT -valued Function-like V38() V39() V40() V41() finite set
rng (x (#) y) is V48() V49() V50() V51() V52() V53() finite Element of bool REAL
s is non empty set
[:s,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
bool [:s,NAT:] is non empty non trivial non finite set
x is Relation-like NAT -defined s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of s
y is Relation-like s -defined NAT -valued Function-like V18(s, NAT ) V38() V39() V40() V41() Element of bool [:s,NAT:]
(s,x,y) is Relation-like NAT -defined REAL -valued NAT -valued RAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (s,x,y) is ext-real V34() V35() Element of REAL
z is Relation-like NAT -defined REAL -valued Function-like V38() V39() V40() finite FinSequence-like FinSubsequence-like FinSequence of REAL
Sum z is ext-real V34() V35() Element of REAL
z is ext-real V34() V35() Element of REAL
<*z*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial V38() V39() V40() V42() V43() V44() V45() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL
z ^ <*z*> is Relation-like NAT -defined REAL -valued Function-like non empty V38() V39() V40() finite FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (z ^ <*z*>) is ext-real V34() V35() Element of REAL
rng (z ^ <*z*>) is non empty V48() V49() V50() finite Element of bool REAL
rng z is V48() V49() V50() finite Element of bool REAL
rng <*z*> is non empty trivial V48() V49() V50() finite 1 -element Element of bool REAL
{z} is non empty trivial V48() V49() V50() finite 1 -element set
a is epsilon-transitive epsilon-connected ordinal natural finite cardinal set
z is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
a + z is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
s is non empty ()
the carrier of s is non empty set
the carrier of s * is functional non empty FinSequence-membered M10( the carrier of s)
[:( the carrier of s *), the carrier of s:] is Relation-like non empty set
[:[:( the carrier of s *), the carrier of s:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
x is Relation-like [:[:( the carrier of s *), the carrier of s:],NAT:] -valued Function-like finite DecoratedTree-like (s)
x . {} is set
(x . {}) `2 is set
(x . {}) `1 is set
x . <*0*> is set
(x . <*0*>) `1 is set
x . <*1*> is set
(x . <*1*>) `1 is set
(s) is Relation-like the carrier of s -defined NAT -valued Function-like V18( the carrier of s, NAT ) V38() V39() V40() V41() Element of bool [: the carrier of s,NAT:]
[: the carrier of s,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
bool [: the carrier of s,NAT:] is non empty non trivial non finite set
{} ^ <*0*> is Relation-like NAT -defined Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like set
{} + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
{} ^ <*1*> is Relation-like NAT -defined Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like set
proj1 x is non empty finite V70() set
y is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*1*> is Relation-like NAT -defined NAT -valued Function-like non empty V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of NAT
x . y is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(x . y) `1 is set
z is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
z is Relation-like NAT -defined NAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like Element of proj1 x
a is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
a ^ z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
b is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(a ^ z) ^ b is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
T9 is Element of the carrier of s
(s,((a ^ z) ^ b),T9) is V15() Element of [:( the carrier of s *), the carrier of s:]
{((a ^ z) ^ b),T9} is non empty finite set
{((a ^ z) ^ b)} is functional non empty trivial finite V59() 1 -element set
{{((a ^ z) ^ b),T9},{((a ^ z) ^ b)}} is non empty finite V59() set
x . z is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(x . z) `1 is set
z is Element of the carrier of s
(s,z,z) is V15() Element of [:( the carrier of s *), the carrier of s:]
{z,z} is non empty finite set
{z} is functional non empty trivial finite V59() 1 -element set
{{z,z},{z}} is non empty finite V59() set
x . z is Element of [:[:( the carrier of s *), the carrier of s:],NAT:]
(x . z) `1 is set
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
a ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(a ^ <*z*>) ^ b is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,((a ^ <*z*>) ^ b),T9) is V15() Element of [:( the carrier of s *), the carrier of s:]
{((a ^ <*z*>) ^ b),T9} is non empty finite set
{((a ^ <*z*>) ^ b)} is functional non empty trivial finite V59() 1 -element set
{{((a ^ <*z*>) ^ b),T9},{((a ^ <*z*>) ^ b)}} is non empty finite V59() set
( the carrier of s,((a ^ z) ^ b),(s)) is Relation-like NAT -defined REAL -valued NAT -valued RAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of REAL
Sum ( the carrier of s,((a ^ z) ^ b),(s)) is ext-real V34() V35() Element of REAL
(s) . z is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
(s) . T9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
((s) . z) + ((s) . T9) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
X9 is epsilon-transitive epsilon-connected ordinal natural finite cardinal set
(((s) . z) + ((s) . T9)) + X9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural finite cardinal set
z is epsilon-transitive epsilon-connected ordinal natural finite cardinal set
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z ^ z is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
a is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(z ^ z) ^ a is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
(s,((z ^ z) ^ a),z) is V15() Element of [:( the carrier of s *), the carrier of s:]
{((z ^ z) ^ a),z} is non empty finite set
{((z ^ z) ^ a)} is functional non empty trivial finite V59() 1 -element set
{{((z ^ z) ^ a),z},{((z ^ z) ^ a)}} is non empty finite V59() set
b is Element of the carrier of s
(s,z,b) is V15() Element of [:( the carrier of s *), the carrier of s:]
{z,b} is non empty finite set
{z} is functional non empty trivial finite V59() 1 -element set
{{z,b},{z}} is non empty finite V59() set
<*b*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z ^ <*b*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(z ^ <*b*>) ^ a is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,((z ^ <*b*>) ^ a),z) is V15() Element of [:( the carrier of s *), the carrier of s:]
{((z ^ <*b*>) ^ a),z} is non empty finite set
{((z ^ <*b*>) ^ a)} is functional non empty trivial finite V59() 1 -element set
{{((z ^ <*b*>) ^ a),z},{((z ^ <*b*>) ^ a)}} is non empty finite V59() set
(s) . b is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
(s) . z is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
((s) . b) + ((s) . z) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
( the carrier of s,((z ^ z) ^ a),(s)) is Relation-like NAT -defined REAL -valued NAT -valued RAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of REAL
Sum ( the carrier of s,((z ^ z) ^ a),(s)) is ext-real V34() V35() Element of REAL
(((s) . b) + ((s) . z)) + (Sum ( the carrier of s,((z ^ z) ^ a),(s))) is set
X9 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
T9 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
X9 ^ T9 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
Y9 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(X9 ^ T9) ^ Y9 is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z9 is Element of the carrier of s
(s,((X9 ^ T9) ^ Y9),z9) is V15() Element of [:( the carrier of s *), the carrier of s:]
{((X9 ^ T9) ^ Y9),z9} is non empty finite set
{((X9 ^ T9) ^ Y9)} is functional non empty trivial finite V59() 1 -element set
{{((X9 ^ T9) ^ Y9),z9},{((X9 ^ T9) ^ Y9)}} is non empty finite V59() set
y9 is Element of the carrier of s
(s,T9,y9) is V15() Element of [:( the carrier of s *), the carrier of s:]
{T9,y9} is non empty finite set
{T9} is functional non empty trivial finite V59() 1 -element set
{{T9,y9},{T9}} is non empty finite V59() set
<*y9*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
X9 ^ <*y9*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(X9 ^ <*y9*>) ^ Y9 is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,((X9 ^ <*y9*>) ^ Y9),z9) is V15() Element of [:( the carrier of s *), the carrier of s:]
{((X9 ^ <*y9*>) ^ Y9),z9} is non empty finite set
{((X9 ^ <*y9*>) ^ Y9)} is functional non empty trivial finite V59() 1 -element set
{{((X9 ^ <*y9*>) ^ Y9),z9},{((X9 ^ <*y9*>) ^ Y9)}} is non empty finite V59() set
(s) . y9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
(s) . z9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
((s) . y9) + ((s) . z9) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
( the carrier of s,((X9 ^ T9) ^ Y9),(s)) is Relation-like NAT -defined REAL -valued NAT -valued RAT -valued Function-like V38() V39() V40() V41() finite FinSequence-like FinSubsequence-like FinSequence of REAL
Sum ( the carrier of s,((X9 ^ T9) ^ Y9),(s)) is ext-real V34() V35() Element of REAL
(((s) . y9) + ((s) . z9)) + (Sum ( the carrier of s,((X9 ^ T9) ^ Y9),(s))) is set
(s,((z ^ z) ^ a),z) `1 is set
(s,z,b) `2 is set
(s,((z ^ z) ^ a),z) `2 is set
s is non empty ()
the carrier of s is non empty set
x is non empty set
x * is functional non empty FinSequence-membered M10(x)
bool (x *) is non empty set
[: the carrier of s,(bool (x *)):] is Relation-like non empty set
bool [: the carrier of s,(bool (x *)):] is non empty set
the carrier of s --> {{}} is Relation-like the carrier of s -defined {{{}}} -valued Function-like V18( the carrier of s,{{{}}}) Element of bool [: the carrier of s,{{{}}}:]
{{{}}} is non empty trivial finite V59() 1 -element set
[: the carrier of s,{{{}}}:] is Relation-like non empty set
bool [: the carrier of s,{{{}}}:] is non empty set
y is Relation-like the carrier of s -defined bool (x *) -valued Function-like V18( the carrier of s, bool (x *)) Element of bool [: the carrier of s,(bool (x *)):]
z is Element of the carrier of s
y . z is functional FinSequence-membered Element of bool (x *)
z is set
z is Element of the carrier of s
y . z is functional FinSequence-membered Element of bool (x *)
z is Element of the carrier of s
y . z is functional FinSequence-membered Element of bool (x *)
z is Element of the carrier of s
(s,z,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (z,z) is Element of the carrier of s
[z,z] is V15() set
{z,z} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,z},{z}} is non empty finite V59() set
the of s . [z,z] is set
y . (s,z,z) is functional FinSequence-membered Element of bool (x *)
y . z is functional FinSequence-membered Element of bool (x *)
{ (b1 ^ b2) where b1, b2 is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like Element of x * : ( b1 in y . z & b2 in y . z ) } is set
(s,z,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (z,z) is Element of the carrier of s
the of s . [z,z] is set
y . (s,z,z) is functional FinSequence-membered Element of bool (x *)
{ b1 where b1 is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like Element of x * : for b2 being Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like Element of x * holds
( not b2 in y . z or b1 ^ b2 in y . z ) } is set
(s,z,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (z,z) is Element of the carrier of s
[z,z] is V15() set
{z,z} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,z},{z}} is non empty finite V59() set
the of s . [z,z] is set
y . (s,z,z) is functional FinSequence-membered Element of bool (x *)
{ b1 where b1 is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like Element of x * : for b2 being Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like Element of x * holds
( not b2 in y . z or b2 ^ b1 in y . z ) } is set
z is set
{} ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
z is set
a is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like Element of x *
b is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like Element of x *
a ^ b is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x
z is set
a is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like Element of x *
{} ^ a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
z is set
a is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like Element of x *
a ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
z is set
a is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like Element of x *
a ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
z is set
a is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like Element of x *
{} ^ a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
[:{{}},{{}}:] is Relation-like RAT -valued INT -valued non empty V38() V39() V40() V41() finite set
[:[:{{}},{{}}:],{{}}:] is Relation-like RAT -valued INT -valued non empty V38() V39() V40() V41() finite set
bool [:[:{{}},{{}}:],{{}}:] is non empty finite V59() set
the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:] is Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:]
{{}} * is functional non empty FinSequence-membered M10({{}})
[:({{}} *),{{}}:] is Relation-like RAT -valued INT -valued non empty V38() V39() V40() V41() set
bool [:({{}} *),{{}}:] is non empty set
the Relation-like {{}} * -defined {{}} -valued V38() V39() V40() V41() Element of bool [:({{}} *),{{}}:] is Relation-like {{}} * -defined {{}} -valued V38() V39() V40() V41() Element of bool [:({{}} *),{{}}:]
({{}}, the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like {{}} * -defined {{}} -valued V38() V39() V40() V41() Element of bool [:({{}} *),{{}}:]) is () ()
the carrier of ({{}}, the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like V18([:{{}},{{}}:],{{}}) V38() V39() V40() V41() finite Element of bool [:[:{{}},{{}}:],{{}}:], the Relation-like {{}} * -defined {{}} -valued V38() V39() V40() V41() Element of bool [:({{}} *),{{}}:]) is set
s is non empty ()
the carrier of s is non empty set
1 * is functional non empty FinSequence-membered M10(1)
[:(1 *),1:] is Relation-like RAT -valued INT -valued non empty V38() V39() V40() V41() set
bool [:(1 *),1:] is non empty set
op2 is Relation-like [:1,1:] -defined 1 -valued Function-like V18([:1,1:],1) V38() V39() V40() V41() finite Element of bool [:[:1,1:],1:]
s is Relation-like 1 * -defined 1 -valued non empty V38() V39() V40() V41() Element of bool [:(1 *),1:]
(1,op2,op2,op2,s) is () ()
x is non empty ()
the carrier of x is non empty set
y is Element of the carrier of x
z is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(x,z,y) is V15() Element of [:( the carrier of x *), the carrier of x:]
the carrier of x * is functional non empty FinSequence-membered M10( the carrier of x)
[:( the carrier of x *), the carrier of x:] is Relation-like non empty set
{z,y} is non empty finite set
{z} is functional non empty trivial finite V59() 1 -element set
{{z,y},{z}} is non empty finite V59() set
y is Element of the carrier of x
<*y*> is Relation-like NAT -defined the carrier of x -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of x
y is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
z is Element of the carrier of x
<*z*> is Relation-like NAT -defined the carrier of x -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of x
y ^ <*z*> is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
z is Element of the carrier of x
(x,z,z) is Element of the carrier of x
the of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the of x . (z,z) is Element of the carrier of x
[z,z] is V15() set
{z,z} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,z},{z}} is non empty finite V59() set
the of x . [z,z] is set
b is Element of the carrier of x
<*b*> is Relation-like NAT -defined the carrier of x -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of x
z is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
<*b*> ^ z is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
a is Element of the carrier of x
(x,b,a) is Element of the carrier of x
the of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the of x . (b,a) is Element of the carrier of x
[b,a] is V15() set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V59() set
the of x . [b,a] is set
z is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
y9 is Element of the carrier of x
T9 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
Y9 is Element of the carrier of x
<*Y9*> is Relation-like NAT -defined the carrier of x -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of x
T9 ^ <*Y9*> is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
X9 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(T9 ^ <*Y9*>) ^ X9 is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
z9 is Element of the carrier of x
(x,Y9,y9) is Element of the carrier of x
the of x . (Y9,y9) is Element of the carrier of x
[Y9,y9] is V15() set
{Y9,y9} is non empty finite set
{Y9} is non empty trivial finite 1 -element set
{{Y9,y9},{Y9}} is non empty finite V59() set
the of x . [Y9,y9] is set
<*(x,Y9,y9)*> is Relation-like NAT -defined the carrier of x -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of x
T9 ^ <*(x,Y9,y9)*> is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(T9 ^ <*(x,Y9,y9)*>) ^ z is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
((T9 ^ <*(x,Y9,y9)*>) ^ z) ^ X9 is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c15 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c19 is Element of the carrier of x
c16 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c18 is Element of the carrier of x
<*c18*> is Relation-like NAT -defined the carrier of x -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c16 ^ <*c18*> is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c17 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(c16 ^ <*c18*>) ^ c17 is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c20 is Element of the carrier of x
c16 ^ c15 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(x,c19,c18) is Element of the carrier of x
the of x . (c19,c18) is Element of the carrier of x
[c19,c18] is V15() set
{c19,c18} is non empty finite set
{c19} is non empty trivial finite 1 -element set
{{c19,c18},{c19}} is non empty finite V59() set
the of x . [c19,c18] is set
<*(x,c19,c18)*> is Relation-like NAT -defined the carrier of x -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(c16 ^ c15) ^ <*(x,c19,c18)*> is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
((c16 ^ c15) ^ <*(x,c19,c18)*>) ^ c17 is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c21 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c23 is Element of the carrier of x
<*c23*> is Relation-like NAT -defined the carrier of x -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c21 ^ <*c23*> is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c24 is Element of the carrier of x
<*c24*> is Relation-like NAT -defined the carrier of x -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(c21 ^ <*c23*>) ^ <*c24*> is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c22 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
((c21 ^ <*c23*>) ^ <*c24*>) ^ c22 is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c25 is Element of the carrier of x
(x,c23,c24) is Element of the carrier of x
the of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the of x . (c23,c24) is Element of the carrier of x
[c23,c24] is V15() set
{c23,c24} is non empty finite set
{c23} is non empty trivial finite 1 -element set
{{c23,c24},{c23}} is non empty finite V59() set
the of x . [c23,c24] is set
<*(x,c23,c24)*> is Relation-like NAT -defined the carrier of x -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c21 ^ <*(x,c23,c24)*> is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(c21 ^ <*(x,c23,c24)*>) ^ c22 is Relation-like NAT -defined the carrier of x -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c26 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c28 is Element of the carrier of x
c27 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
c29 is Element of the carrier of x
c26 ^ c27 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(x,c28,c29) is Element of the carrier of x
the of x . (c28,c29) is Element of the carrier of x
[c28,c29] is V15() set
{c28,c29} is non empty finite set
{c28} is non empty trivial finite 1 -element set
{{c28,c29},{c28}} is non empty finite V59() set
the of x . [c28,c29] is set
s is non empty () ()
the carrier of s is non empty set
x is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
z is Element of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,z,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (z,z) is Element of the carrier of s
[z,z] is V15() set
{z,z} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,z},{z}} is non empty finite V59() set
the of s . [z,z] is set
<*(s,z,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y ^ <*(s,z,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(y ^ <*(s,z,z)*>) ^ x is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
(y ^ <*z*>) ^ H2(s) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((y ^ <*(s,z,z)*>) ^ x) ^ H2(s) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
z is Element of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*z*> ^ y is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,z,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (z,z) is Element of the carrier of s
[z,z] is V15() set
{z,z} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,z},{z}} is non empty finite V59() set
the of s . [z,z] is set
<*(s,z,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,z,z)*> ^ x is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(<*(s,z,z)*> ^ x) ^ y is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
H2(s) ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
{} + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
(H2(s) ^ <*z*>) ^ y is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
H2(s) ^ <*(s,z,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(H2(s) ^ <*(s,z,z)*>) ^ x is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((H2(s) ^ <*(s,z,z)*>) ^ x) ^ y is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Element of the carrier of s
z is Element of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,z,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (z,y) is Element of the carrier of s
[z,y] is V15() set
{z,y} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,y},{z}} is non empty finite V59() set
the of s . [z,y] is set
<*(s,z,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,z,y)*> ^ x is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
H2(s) ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
{} + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
H2(s) ^ <*(s,z,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(H2(s) ^ <*(s,z,y)*>) ^ x is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y ^ x is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
z is Element of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,z,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (z,z) is Element of the carrier of s
[z,z] is V15() set
{z,z} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,z},{z}} is non empty finite V59() set
the of s . [z,z] is set
<*(s,z,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(y ^ x) ^ <*(s,z,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
(y ^ <*z*>) ^ H2(s) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((y ^ x) ^ <*(s,z,z)*>) ^ H2(s) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
z is Element of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*z*> ^ y is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,z,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (z,z) is Element of the carrier of s
[z,z] is V15() set
{z,z} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,z},{z}} is non empty finite V59() set
the of s . [z,z] is set
<*(s,z,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
x ^ <*(s,z,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(x ^ <*(s,z,z)*>) ^ y is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
H2(s) ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
{} + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
(H2(s) ^ <*z*>) ^ y is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
H2(s) ^ x is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(H2(s) ^ x) ^ <*(s,z,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
((H2(s) ^ x) ^ <*(s,z,z)*>) ^ y is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Element of the carrier of s
z is Element of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,y,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (y,z) is Element of the carrier of s
[y,z] is V15() set
{y,z} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,z},{y}} is non empty finite V59() set
the of s . [y,z] is set
<*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
x ^ <*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
H2(s) ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
{} + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
H2(s) ^ x is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(H2(s) ^ x) ^ <*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Element of the carrier of s
<*y*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*y*> ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
(<*y*> ^ <*z*>) ^ x is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,y,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (y,z) is Element of the carrier of s
[y,z] is V15() set
{y,z} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,z},{y}} is non empty finite V59() set
the of s . [y,z] is set
<*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,y,z)*> ^ x is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
H2(s) ^ <*y*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
{} + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
(H2(s) ^ <*y*>) ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite ({} + 1) + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
({} + 1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
((H2(s) ^ <*y*>) ^ <*z*>) ^ x is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
H2(s) ^ <*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(H2(s) ^ <*(s,y,z)*>) ^ x is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Relation-like NAT -defined the carrier of s -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Element of the carrier of s
<*y*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
x ^ <*y*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(x ^ <*y*>) ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,y,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (y,z) is Element of the carrier of s
[y,z] is V15() set
{y,z} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,z},{y}} is non empty finite V59() set
the of s . [y,z] is set
<*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
x ^ <*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
((x ^ <*y*>) ^ <*z*>) ^ H2(s) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(x ^ <*(s,y,z)*>) ^ H2(s) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
<*x*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Element of the carrier of s
<*y*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*x*> ^ <*y*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
(s,x,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
<*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
H2(s) ^ <*x*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
{} + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
(H2(s) ^ <*x*>) ^ <*y*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite ({} + 1) + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
({} + 1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
H2(s) ^ <*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
y is Element of the carrier of s
(s,x,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
<*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*y*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,x,y)*> ^ <*y*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
(s,y,x) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (y,x) is Element of the carrier of s
[y,x] is V15() set
{y,x} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,x},{y}} is non empty finite V59() set
the of s . [y,x] is set
<*(s,y,x)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*y*> ^ <*(s,y,x)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*x*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
<*x*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Element of the carrier of s
(s,x,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
(s,y,(s,x,y)) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (y,(s,x,y)) is Element of the carrier of s
[y,(s,x,y)] is V15() set
{y,(s,x,y)} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,(s,x,y)},{y}} is non empty finite V59() set
the of s . [y,(s,x,y)] is set
(s,y,x) is Element of the carrier of s
the of s . (y,x) is Element of the carrier of s
[y,x] is V15() set
{y,x} is non empty finite set
{{y,x},{y}} is non empty finite V59() set
the of s . [y,x] is set
(s,(s,y,x),y) is Element of the carrier of s
the of s . ((s,y,x),y) is Element of the carrier of s
[(s,y,x),y] is V15() set
{(s,y,x),y} is non empty finite set
{(s,y,x)} is non empty trivial finite 1 -element set
{{(s,y,x),y},{(s,y,x)}} is non empty finite V59() set
the of s . [(s,y,x),y] is set
<*(s,y,x)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,y,x)*> ^ <*x*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*x*> ^ <*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
y is Element of the carrier of s
(s,x,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
<*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
(s,x,z) is Element of the carrier of s
the of s . (x,z) is Element of the carrier of s
[x,z] is V15() set
{x,z} is non empty finite set
{{x,z},{x}} is non empty finite V59() set
the of s . [x,z] is set
(s,y,z) is Element of the carrier of s
the of s . (y,z) is Element of the carrier of s
[y,z] is V15() set
{y,z} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,z},{y}} is non empty finite V59() set
the of s . [y,z] is set
(s,(s,x,z),(s,y,z)) is Element of the carrier of s
the of s . ((s,x,z),(s,y,z)) is Element of the carrier of s
[(s,x,z),(s,y,z)] is V15() set
{(s,x,z),(s,y,z)} is non empty finite set
{(s,x,z)} is non empty trivial finite 1 -element set
{{(s,x,z),(s,y,z)},{(s,x,z)}} is non empty finite V59() set
the of s . [(s,x,z),(s,y,z)] is set
<*y*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,x,y)*> ^ <*y*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,x,y)*> ^ <*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(<*(s,x,y)*> ^ <*(s,y,z)*>) ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(1 + 1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
y is Element of the carrier of s
(s,x,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
<*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
(s,z,x) is Element of the carrier of s
the of s . (z,x) is Element of the carrier of s
[z,x] is V15() set
{z,x} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,x},{z}} is non empty finite V59() set
the of s . [z,x] is set
(s,z,y) is Element of the carrier of s
the of s . (z,y) is Element of the carrier of s
[z,y] is V15() set
{z,y} is non empty finite set
{{z,y},{z}} is non empty finite V59() set
the of s . [z,y] is set
(s,(s,z,x),(s,z,y)) is Element of the carrier of s
the of s . ((s,z,x),(s,z,y)) is Element of the carrier of s
[(s,z,x),(s,z,y)] is V15() set
{(s,z,x),(s,z,y)} is non empty finite set
{(s,z,x)} is non empty trivial finite 1 -element set
{{(s,z,x),(s,z,y)},{(s,z,x)}} is non empty finite V59() set
the of s . [(s,z,x),(s,z,y)] is set
<*x*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*x*> ^ <*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,z,x)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*z*> ^ <*(s,z,x)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(<*z*> ^ <*(s,z,x)*>) ^ <*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(1 + 1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*(s,z,x)*> ^ <*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*z*> ^ (<*(s,z,x)*> ^ <*(s,x,y)*>) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + (1 + 1) -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + (1 + 1) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
<*x*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Element of the carrier of s
z is Element of the carrier of s
(s,x,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (x,z) is Element of the carrier of s
[x,z] is V15() set
{x,z} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,z},{x}} is non empty finite V59() set
the of s . [x,z] is set
<*(s,x,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,y,z) is Element of the carrier of s
the of s . (y,z) is Element of the carrier of s
[y,z] is V15() set
{y,z} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,z},{y}} is non empty finite V59() set
the of s . [y,z] is set
(s,z,x) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (z,x) is Element of the carrier of s
[z,x] is V15() set
{z,x} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,x},{z}} is non empty finite V59() set
the of s . [z,x] is set
<*(s,z,x)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,z,y) is Element of the carrier of s
the of s . (z,y) is Element of the carrier of s
[z,y] is V15() set
{z,y} is non empty finite set
{{z,y},{z}} is non empty finite V59() set
the of s . [z,y] is set
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,x,z)*> ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*z*> ^ <*(s,z,x)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
<*x*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Element of the carrier of s
z is Element of the carrier of s
(s,z,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (z,y) is Element of the carrier of s
[z,y] is V15() set
{z,y} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,y},{z}} is non empty finite V59() set
the of s . [z,y] is set
<*(s,z,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,z,x) is Element of the carrier of s
the of s . (z,x) is Element of the carrier of s
[z,x] is V15() set
{z,x} is non empty finite set
{{z,x},{z}} is non empty finite V59() set
the of s . [z,x] is set
(s,y,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (y,z) is Element of the carrier of s
[y,z] is V15() set
{y,z} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,z},{y}} is non empty finite V59() set
the of s . [y,z] is set
<*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,x,z) is Element of the carrier of s
the of s . (x,z) is Element of the carrier of s
[x,z] is V15() set
{x,z} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,z},{x}} is non empty finite V59() set
the of s . [x,z] is set
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,z,y)*> ^ <*x*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*x*> ^ <*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
y is Element of the carrier of s
(s,x,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
(s,(s,x,y),x) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . ((s,x,y),x) is Element of the carrier of s
[(s,x,y),x] is V15() set
{(s,x,y),x} is non empty finite set
{(s,x,y)} is non empty trivial finite 1 -element set
{{(s,x,y),x},{(s,x,y)}} is non empty finite V59() set
the of s . [(s,x,y),x] is set
(s,x,(s,(s,x,y),x)) is Element of the carrier of s
the of s . (x,(s,(s,x,y),x)) is Element of the carrier of s
[x,(s,(s,x,y),x)] is V15() set
{x,(s,(s,x,y),x)} is non empty finite set
{{x,(s,(s,x,y),x)},{x}} is non empty finite V59() set
the of s . [x,(s,(s,x,y),x)] is set
<*(s,x,(s,(s,x,y),x))*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*y*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
x is Element of the carrier of s
<*x*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Element of the carrier of s
(s,y,x) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (y,x) is Element of the carrier of s
[y,x] is V15() set
{y,x} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,x},{y}} is non empty finite V59() set
the of s . [y,x] is set
(s,x,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
H2(s) ^ <*x*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
{} + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*x*> ^ H2(s) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
x is Element of the carrier of s
(s,x,x) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (x,x) is Element of the carrier of s
[x,x] is V15() set
{x,x} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,x},{x}} is non empty finite V59() set
the of s . [x,x] is set
(s,x,x) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (x,x) is Element of the carrier of s
the of s . [x,x] is set
<*x*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
x is Element of the carrier of s
y is Element of the carrier of s
(s,y,x) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (y,x) is Element of the carrier of s
[y,x] is V15() set
{y,x} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,x},{y}} is non empty finite V59() set
the of s . [y,x] is set
(s,x,(s,y,x)) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (x,(s,y,x)) is Element of the carrier of s
[x,(s,y,x)] is V15() set
{x,(s,y,x)} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,(s,y,x)},{x}} is non empty finite V59() set
the of s . [x,(s,y,x)] is set
(s,(s,x,(s,y,x)),y) is Element of the carrier of s
the of s . ((s,x,(s,y,x)),y) is Element of the carrier of s
[(s,x,(s,y,x)),y] is V15() set
{(s,x,(s,y,x)),y} is non empty finite set
{(s,x,(s,y,x))} is non empty trivial finite 1 -element set
{{(s,x,(s,y,x)),y},{(s,x,(s,y,x))}} is non empty finite V59() set
the of s . [(s,x,(s,y,x)),y] is set
(s,x,y) is Element of the carrier of s
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
(s,(s,x,y),x) is Element of the carrier of s
the of s . ((s,x,y),x) is Element of the carrier of s
[(s,x,y),x] is V15() set
{(s,x,y),x} is non empty finite set
{(s,x,y)} is non empty trivial finite 1 -element set
{{(s,x,y),x},{(s,x,y)}} is non empty finite V59() set
the of s . [(s,x,y),x] is set
(s,y,(s,(s,x,y),x)) is Element of the carrier of s
the of s . (y,(s,(s,x,y),x)) is Element of the carrier of s
[y,(s,(s,x,y),x)] is V15() set
{y,(s,(s,x,y),x)} is non empty finite set
{{y,(s,(s,x,y),x)},{y}} is non empty finite V59() set
the of s . [y,(s,(s,x,y),x)] is set
<*y*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
x is Element of the carrier of s
y is Element of the carrier of s
(s,x,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
(s,y,x) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (y,x) is Element of the carrier of s
[y,x] is V15() set
{y,x} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,x},{y}} is non empty finite V59() set
the of s . [y,x] is set
z is Element of the carrier of s
(s,z,y) is Element of the carrier of s
the of s . (z,y) is Element of the carrier of s
[z,y] is V15() set
{z,y} is non empty finite set
{z} is non empty trivial finite 1 -element set
{{z,y},{z}} is non empty finite V59() set
the of s . [z,y] is set
(s,(s,x,y),(s,z,y)) is Element of the carrier of s
the of s . ((s,x,y),(s,z,y)) is Element of the carrier of s
[(s,x,y),(s,z,y)] is V15() set
{(s,x,y),(s,z,y)} is non empty finite set
{(s,x,y)} is non empty trivial finite 1 -element set
{{(s,x,y),(s,z,y)},{(s,x,y)}} is non empty finite V59() set
the of s . [(s,x,y),(s,z,y)] is set
(s,x,z) is Element of the carrier of s
the of s . (x,z) is Element of the carrier of s
[x,z] is V15() set
{x,z} is non empty finite set
{{x,z},{x}} is non empty finite V59() set
the of s . [x,z] is set
(s,(s,(s,x,y),(s,z,y)),(s,x,z)) is Element of the carrier of s
the of s . ((s,(s,x,y),(s,z,y)),(s,x,z)) is Element of the carrier of s
[(s,(s,x,y),(s,z,y)),(s,x,z)] is V15() set
{(s,(s,x,y),(s,z,y)),(s,x,z)} is non empty finite set
{(s,(s,x,y),(s,z,y))} is non empty trivial finite 1 -element set
{{(s,(s,x,y),(s,z,y)),(s,x,z)},{(s,(s,x,y),(s,z,y))}} is non empty finite V59() set
the of s . [(s,(s,x,y),(s,z,y)),(s,x,z)] is set
(s,z,x) is Element of the carrier of s
the of s . (z,x) is Element of the carrier of s
[z,x] is V15() set
{z,x} is non empty finite set
{{z,x},{z}} is non empty finite V59() set
the of s . [z,x] is set
(s,y,z) is Element of the carrier of s
the of s . (y,z) is Element of the carrier of s
[y,z] is V15() set
{y,z} is non empty finite set
{{y,z},{y}} is non empty finite V59() set
the of s . [y,z] is set
(s,(s,y,z),(s,y,x)) is Element of the carrier of s
the of s . ((s,y,z),(s,y,x)) is Element of the carrier of s
[(s,y,z),(s,y,x)] is V15() set
{(s,y,z),(s,y,x)} is non empty finite set
{(s,y,z)} is non empty trivial finite 1 -element set
{{(s,y,z),(s,y,x)},{(s,y,z)}} is non empty finite V59() set
the of s . [(s,y,z),(s,y,x)] is set
(s,(s,z,x),(s,(s,y,z),(s,y,x))) is Element of the carrier of s
the of s . ((s,z,x),(s,(s,y,z),(s,y,x))) is Element of the carrier of s
[(s,z,x),(s,(s,y,z),(s,y,x))] is V15() set
{(s,z,x),(s,(s,y,z),(s,y,x))} is non empty finite set
{(s,z,x)} is non empty trivial finite 1 -element set
{{(s,z,x),(s,(s,y,z),(s,y,x))},{(s,z,x)}} is non empty finite V59() set
the of s . [(s,z,x),(s,(s,y,z),(s,y,x))] is set
<*(s,x,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,z,x)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
x is Element of the carrier of s
y is Element of the carrier of s
(s,y,x) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (y,x) is Element of the carrier of s
[y,x] is V15() set
{y,x} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,x},{y}} is non empty finite V59() set
the of s . [y,x] is set
(s,y,(s,y,x)) is Element of the carrier of s
the of s . (y,(s,y,x)) is Element of the carrier of s
[y,(s,y,x)] is V15() set
{y,(s,y,x)} is non empty finite set
{{y,(s,y,x)},{y}} is non empty finite V59() set
the of s . [y,(s,y,x)] is set
(s,x,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
(s,(s,x,y),y) is Element of the carrier of s
the of s . ((s,x,y),y) is Element of the carrier of s
[(s,x,y),y] is V15() set
{(s,x,y),y} is non empty finite set
{(s,x,y)} is non empty trivial finite 1 -element set
{{(s,x,y),y},{(s,x,y)}} is non empty finite V59() set
the of s . [(s,x,y),y] is set
<*y*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
H2(s) ^ <*y*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
{} + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*y*> ^ H2(s) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,y,x)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
H2(s) ^ <*(s,y,x)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(H2(s) ^ <*(s,y,x)*>) ^ H2(s) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
H2(s) ^ <*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(H2(s) ^ <*(s,x,y)*>) ^ H2(s) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,x,y)*> ^ H2(s) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
y is Element of the carrier of s
(s,y,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (y,y) is Element of the carrier of s
[y,y] is V15() set
{y,y} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,y},{y}} is non empty finite V59() set
the of s . [y,y] is set
(s,x,(s,y,y)) is Element of the carrier of s
the of s . (x,(s,y,y)) is Element of the carrier of s
[x,(s,y,y)] is V15() set
{x,(s,y,y)} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,(s,y,y)},{x}} is non empty finite V59() set
the of s . [x,(s,y,y)] is set
<*(s,x,(s,y,y))*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*x*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*> the carrier of s is Relation-like non-empty empty-yielding NAT -defined the carrier of s -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V38() V39() V40() V41() V48() V49() V50() V51() V52() V53() V54() finite finite-yielding V59() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of s
[:NAT, the carrier of s:] is Relation-like non empty non trivial non finite set
<*(s,x,(s,y,y))*> ^ H2(s) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
z is Element of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
z is Element of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
y is Element of the carrier of s
(s,x,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
(s,(s,x,y),x) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . ((s,x,y),x) is Element of the carrier of s
[(s,x,y),x] is V15() set
{(s,x,y),x} is non empty finite set
{(s,x,y)} is non empty trivial finite 1 -element set
{{(s,x,y),x},{(s,x,y)}} is non empty finite V59() set
the of s . [(s,x,y),x] is set
(s,x,(s,(s,x,y),x)) is Element of the carrier of s
the of s . (x,(s,(s,x,y),x)) is Element of the carrier of s
[x,(s,(s,x,y),x)] is V15() set
{x,(s,(s,x,y),x)} is non empty finite set
{{x,(s,(s,x,y),x)},{x}} is non empty finite V59() set
the of s . [x,(s,(s,x,y),x)] is set
<*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,x,(s,(s,x,y),x))*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
y is Element of the carrier of s
z is Element of the carrier of s
(s,y,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (y,z) is Element of the carrier of s
[y,z] is V15() set
{y,z} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,z},{y}} is non empty finite V59() set
the of s . [y,z] is set
(s,x,(s,y,z)) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (x,(s,y,z)) is Element of the carrier of s
[x,(s,y,z)] is V15() set
{x,(s,y,z)} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,(s,y,z)},{x}} is non empty finite V59() set
the of s . [x,(s,y,z)] is set
(s,x,z) is Element of the carrier of s
the of s . (x,z) is Element of the carrier of s
[x,z] is V15() set
{x,z} is non empty finite set
{{x,z},{x}} is non empty finite V59() set
the of s . [x,z] is set
(s,(s,x,z),y) is Element of the carrier of s
the of s . ((s,x,z),y) is Element of the carrier of s
[(s,x,z),y] is V15() set
{(s,x,z),y} is non empty finite set
{(s,x,z)} is non empty trivial finite 1 -element set
{{(s,x,z),y},{(s,x,z)}} is non empty finite V59() set
the of s . [(s,x,z),y] is set
<*y*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*x*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*y*> ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*(s,x,(s,y,z))*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,x,(s,y,z))*> ^ (<*y*> ^ <*z*>) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + (1 + 1) -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + (1 + 1) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*(s,x,(s,y,z))*> ^ <*y*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(<*(s,x,(s,y,z))*> ^ <*y*>) ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(1 + 1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*(s,x,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,x,z)*> ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,(s,x,z),y)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,(s,x,z),y)*> ^ <*y*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(<*(s,(s,x,z),y)*> ^ <*y*>) ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,(s,x,z),y)*> ^ <*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
y is Element of the carrier of s
(s,x,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
z is Element of the carrier of s
(s,y,z) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (y,z) is Element of the carrier of s
[y,z] is V15() set
{y,z} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,z},{y}} is non empty finite V59() set
the of s . [y,z] is set
(s,x,(s,y,z)) is Element of the carrier of s
the of s . (x,(s,y,z)) is Element of the carrier of s
[x,(s,y,z)] is V15() set
{x,(s,y,z)} is non empty finite set
{{x,(s,y,z)},{x}} is non empty finite V59() set
the of s . [x,(s,y,z)] is set
<*(s,x,(s,y,z))*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(s,(s,x,y),z) is Element of the carrier of s
the of s . ((s,x,y),z) is Element of the carrier of s
[(s,x,y),z] is V15() set
{(s,x,y),z} is non empty finite set
{(s,x,y)} is non empty trivial finite 1 -element set
{{(s,x,y),z},{(s,x,y)}} is non empty finite V59() set
the of s . [(s,x,y),z] is set
<*x*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*y*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*x*> ^ <*y*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*x*> ^ <*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(<*x*> ^ <*(s,y,z)*>) ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(1 + 1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*(s,x,(s,y,z))*> ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
<*x*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
y is Element of the carrier of s
(s,x,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
(s,(s,x,y),y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . ((s,x,y),y) is Element of the carrier of s
[(s,x,y),y] is V15() set
{(s,x,y),y} is non empty finite set
{(s,x,y)} is non empty trivial finite 1 -element set
{{(s,x,y),y},{(s,x,y)}} is non empty finite V59() set
the of s . [(s,x,y),y] is set
(s,y,x) is Element of the carrier of s
the of s . (y,x) is Element of the carrier of s
[y,x] is V15() set
{y,x} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,x},{y}} is non empty finite V59() set
the of s . [y,x] is set
(s,y,(s,y,x)) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
the of s . (y,(s,y,x)) is Element of the carrier of s
[y,(s,y,x)] is V15() set
{y,(s,y,x)} is non empty finite set
{{y,(s,y,x)},{y}} is non empty finite V59() set
the of s . [y,(s,y,x)] is set
<*y*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*x*> ^ <*y*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*y*> ^ <*x*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
s is non empty () ()
the carrier of s is non empty set
x is Element of the carrier of s
y is Element of the carrier of s
(s,x,y) is Element of the carrier of s
the of s is Relation-like [: the carrier of s, the carrier of s:] -defined the carrier of s -valued Function-like V18([: the carrier of s, the carrier of s:], the carrier of s) Element of bool [:[: the carrier of s, the carrier of s:], the carrier of s:]
[: the carrier of s, the carrier of s:] is Relation-like non empty set
[:[: the carrier of s, the carrier of s:], the carrier of s:] is Relation-like non empty set
bool [:[: the carrier of s, the carrier of s:], the carrier of s:] is non empty set
the of s . (x,y) is Element of the carrier of s
[x,y] is V15() set
{x,y} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is non empty finite V59() set
the of s . [x,y] is set
z is Element of the carrier of s
(s,(s,x,y),z) is Element of the carrier of s
the of s . ((s,x,y),z) is Element of the carrier of s
[(s,x,y),z] is V15() set
{(s,x,y),z} is non empty finite set
{(s,x,y)} is non empty trivial finite 1 -element set
{{(s,x,y),z},{(s,x,y)}} is non empty finite V59() set
the of s . [(s,x,y),z] is set
(s,y,z) is Element of the carrier of s
the of s . (y,z) is Element of the carrier of s
[y,z] is V15() set
{y,z} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,z},{y}} is non empty finite V59() set
the of s . [y,z] is set
(s,x,(s,y,z)) is Element of the carrier of s
the of s . (x,(s,y,z)) is Element of the carrier of s
[x,(s,y,z)] is V15() set
{x,(s,y,z)} is non empty finite set
{{x,(s,y,z)},{x}} is non empty finite V59() set
the of s . [x,(s,y,z)] is set
<*x*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*y*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*z*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*x*> ^ <*y*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
(<*x*> ^ <*y*>) ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
(1 + 1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*x*> ^ <*(s,y,z)*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,x,(s,y,z))*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*y*> ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*x*> ^ (<*y*> ^ <*z*>) is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + (1 + 1) -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
1 + (1 + 1) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() V35() V36() V37() V48() V49() V50() V51() V52() V53() finite cardinal Element of NAT
<*(s,x,y)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,x,y)*> ^ <*z*> is Relation-like NAT -defined the carrier of s -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s
<*(s,(s,x,y),z)*> is Relation-like NAT -defined the carrier of s -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of s