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<