:: PRELAMB semantic presentation

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

RAT is non empty non trivial V48() V49() V50() V51() V54() non finite 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
is Relation-like non empty non trivial V38() V39() V40() non finite set
bool 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
is Relation-like non empty non trivial V38() non finite set
bool is non empty non trivial non finite set
is Relation-like non empty non trivial V38() non finite set
bool is non empty non trivial non finite set
is Relation-like non empty non trivial V38() V39() V40() non finite set
bool is non empty non trivial non finite set
is Relation-like RAT -valued non empty non trivial V38() V39() V40() non finite set
bool is non empty non trivial non finite set
is Relation-like RAT -valued non empty non trivial V38() V39() V40() non finite set
bool is non empty non trivial non finite set
is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() non finite set
bool is non empty non trivial non finite set
is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() non finite set
bool is non empty non trivial non finite set
is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
is Relation-like RAT -valued INT -valued non empty non trivial V38() V39() V40() V41() non finite set
bool 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

is functional non empty trivial V48() V49() V50() V51() V52() V53() finite V59() 1 -element set

is Relation-like non empty non trivial V38() V39() V40() non finite set
Sum () is ext-real V34() V35() Element of REAL

bool is non empty finite V59() 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

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

x . () is set
(x . ()) `1 is set

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*>,z] is V15() set
{<*z*>,z} is non empty finite set

{{<*z*>,z},} is non empty finite V59() set

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,(s,z,a)},{z}} is non empty finite V59() set

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

{{<*b*>,b},} is non empty finite V59() set

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,(s,X9,T9)},{z}} is non empty finite V59() set

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

{{<*Y9*>,Y9},{<*Y9*>}} is non empty finite V59() set

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

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

(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

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

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

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

(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

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

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

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

(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

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

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

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

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

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

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

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

(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

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

(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

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

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

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

(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

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

(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

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

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

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

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

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

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

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

(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

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

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

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

(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

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

(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

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

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

(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

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

(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

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

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

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