K170() is V42() countable denumerable Element of K10(K166())
K166() is set
K10(K166()) is set
K137() is V42() countable denumerable set
K10(K137()) is set
K10(K170()) is set
{} is set
the empty Relation-like non-empty empty-yielding K170() -defined Function-like one-to-one constant functional Function-yielding Relation-yielding V42() Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered set is empty Relation-like non-empty empty-yielding K170() -defined Function-like one-to-one constant functional Function-yielding Relation-yielding V42() Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty set
2 is non empty set
3 is non empty set
S is set
the Relation-like set is Relation-like set
S --> the Relation-like set is Relation-like S -defined { the Relation-like set } -valued Function-like constant total V29(S,{ the Relation-like set }) Element of K10(K11(S,{ the Relation-like set }))
{ the Relation-like set } is set
K11(S,{ the Relation-like set }) is Relation-like set
K10(K11(S,{ the Relation-like set })) is set
F is Relation-like S -defined Function-like total set
dom F is Element of K10(S)
K10(S) is set
mc is set
F . mc is set
S is set
U1 is Relation-like S -defined Function-like total set
U2 is Relation-like S -defined Function-like total set
F is Relation-like set
S --> F is Relation-like S -defined {F} -valued Function-like constant total V29(S,{F}) Element of K10(K11(S,{F}))
{F} is set
K11(S,{F}) is Relation-like set
K10(K11(S,{F})) is set
qa is Relation-like S -defined Function-like total set
qh is set
qa . qh is set
U1 . qh is set
U2 . qh is set
K11((U1 . qh),(U2 . qh)) is Relation-like set
K10(K11((U1 . qh),(U2 . qh))) is set
qh is set
qa . qh is set
U1 . qh is set
U2 . qh is set
K11((U1 . qh),(U2 . qh)) is Relation-like set
K10(K11((U1 . qh),(U2 . qh))) is set
S is set
U1 is Relation-like S -defined Function-like total set
U2 is Relation-like S -defined Function-like total set
F is Relation-like S -defined Function-like total (S,U1,U2)
mc is set
dom F is set
F . mc is set
dom F is Element of K10(S)
K10(S) is set
S is set
S is set
U1 is Relation-like S -defined Function-like total set
S is non empty set
U1 is non empty Relation-like S -defined Function-like total set
U2 is non empty Relation-like S -defined Function-like total set
F is non empty Relation-like S -defined Function-like total Relation-yielding (S,U1,U2)
mc is Element of S
F . mc is set
U1 . mc is set
U2 . mc is set
K11((U1 . mc),(U2 . mc)) is Relation-like set
K10(K11((U1 . mc),(U2 . mc))) is set
S is non empty V68() ManySortedSign
S is non empty V68() ManySortedSign
the carrier of S is non empty set
U1 is MSAlgebra over S
the Sorts of U1 is non empty Relation-like the carrier of S -defined Function-like total set
S is non empty non void V68() ManySortedSign
the carrier of S is non empty set
U1 is MSAlgebra over S
the Sorts of U1 is non empty Relation-like the carrier of S -defined Function-like total set
U2 is Relation-like Function-like set
dom U2 is set
F is non empty Relation-like the carrier of S -defined Function-like total set
mc is set
F . mc is set
the Sorts of U1 . mc is set
K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc)) is Relation-like set
K10(K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc))) is set
id ( the Sorts of U1 . mc) is Relation-like the Sorts of U1 . mc -defined the Sorts of U1 . mc -valued V12() V14() V15() V19() Function-like one-to-one total Element of K10(K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc)))
mc is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ( the carrier of S, the Sorts of U1, the Sorts of U1)
qa is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ( the carrier of S, the Sorts of U1, the Sorts of U1)
qh is set
the Sorts of U1 . qh is set
K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh)) is Relation-like set
K10(K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh))) is set
qa . qh is set
Sq is Relation-like the Sorts of U1 . qh -defined the Sorts of U1 . qh -valued Element of K10(K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh)))
id ( the Sorts of U1 . qh) is Relation-like the Sorts of U1 . qh -defined the Sorts of U1 . qh -valued V12() V14() V15() V19() Function-like one-to-one total Element of K10(K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh)))
S is non empty non void V68() ManySortedSign
the carrier of S is non empty set
U1 is MSAlgebra over S
the Sorts of U1 is non empty Relation-like the carrier of S -defined Function-like total set
U2 is Element of the carrier of S
the Sorts of U1 . U2 is set
K11(( the Sorts of U1 . U2),( the Sorts of U1 . U2)) is Relation-like set
K10(K11(( the Sorts of U1 . U2),( the Sorts of U1 . U2))) is set
F is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
( the carrier of S, the Sorts of U1, the Sorts of U1,F,U2) is Relation-like the Sorts of U1 . U2 -defined the Sorts of U1 . U2 -valued Element of K10(K11(( the Sorts of U1 . U2),( the Sorts of U1 . U2)))
S is non empty non void V68() ManySortedSign
U1 is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
S is non empty non void V68() ManySortedSign
U1 is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 is Relation-like Function-like set
dom U2 is set
F is non empty Relation-like the carrier of S -defined Function-like total set
mc is set
F . mc is set
the Sorts of U1 . mc is set
K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc)) is Relation-like set
K10(K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc))) is set
id ( the Sorts of U1 . mc) is Relation-like the Sorts of U1 . mc -defined the Sorts of U1 . mc -valued V12() V14() V15() V19() Function-like one-to-one total Element of K10(K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc)))
mc is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ( the carrier of S, the Sorts of U1, the Sorts of U1)
qa is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ( the carrier of S, the Sorts of U1, the Sorts of U1)
qh is set
the Sorts of U1 . qh is set
K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh)) is Relation-like set
K10(K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh))) is set
qa . qh is set
Sq is Relation-like the Sorts of U1 . qh -defined the Sorts of U1 . qh -valued Element of K10(K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh)))
id ( the Sorts of U1 . qh) is Relation-like the Sorts of U1 . qh -defined the Sorts of U1 . qh -valued V12() V14() V15() V19() Function-like one-to-one total Element of K10(K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh)))
qh is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
the carrier' of S is non empty set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
dom the ResultSort of S is Element of K10( the carrier' of S)
K10( the carrier' of S) is set
the ResultSort of S * the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
dom ( the ResultSort of S * the Sorts of U1) is non empty Element of K10( the carrier' of S)
Sq is Element of the carrier' of S
Args (Sq,U1) is non empty functional Element of rng ( the Sorts of U1 #)
the Sorts of U1 # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
rng ( the Sorts of U1 #) is non empty V4() set
the_arity_of Sq is Relation-like K170() -defined the carrier of S -valued Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
Result (Sq,U1) is non empty Element of rng the Sorts of U1
rng the Sorts of U1 is non empty V4() set
Den (Sq,U1) is Relation-like Args (Sq,U1) -defined Result (Sq,U1) -valued Function-like V29( Args (Sq,U1), Result (Sq,U1)) Element of K10(K11((Args (Sq,U1)),(Result (Sq,U1))))
K11((Args (Sq,U1)),(Result (Sq,U1))) is Relation-like set
K10(K11((Args (Sq,U1)),(Result (Sq,U1)))) is set
the_result_sort_of Sq is Element of the carrier of S
( the carrier of S, the Sorts of U1, the Sorts of U1,qh,(the_result_sort_of Sq)) is Relation-like the Sorts of U1 . (the_result_sort_of Sq) -defined the Sorts of U1 . (the_result_sort_of Sq) -valued Element of K10(K11(( the Sorts of U1 . (the_result_sort_of Sq)),( the Sorts of U1 . (the_result_sort_of Sq))))
the Sorts of U1 . (the_result_sort_of Sq) is non empty set
K11(( the Sorts of U1 . (the_result_sort_of Sq)),( the Sorts of U1 . (the_result_sort_of Sq))) is Relation-like set
K10(K11(( the Sorts of U1 . (the_result_sort_of Sq)),( the Sorts of U1 . (the_result_sort_of Sq)))) is set
S1 is Relation-like Function-like Element of Args (Sq,U1)
dom S1 is set
S2 is Relation-like Function-like Element of Args (Sq,U1)
(Den (Sq,U1)) . S1 is Element of Result (Sq,U1)
(Den (Sq,U1)) . S2 is Element of Result (Sq,U1)
[((Den (Sq,U1)) . S1),((Den (Sq,U1)) . S2)] is set
{((Den (Sq,U1)) . S1),((Den (Sq,U1)) . S2)} is set
{((Den (Sq,U1)) . S1)} is set
{{((Den (Sq,U1)) . S1),((Den (Sq,U1)) . S2)},{((Den (Sq,U1)) . S1)}} is set
dom (the_arity_of Sq) is countable Element of K10(K170())
f is set
S1 . f is set
S2 . f is set
s is V41() set
(the_arity_of Sq) . s is set
rng (the_arity_of Sq) is Element of K10( the carrier of S)
K10( the carrier of S) is set
qh . ((the_arity_of Sq) . s) is set
the Sorts of U1 . ((the_arity_of Sq) . s) is set
id ( the Sorts of U1 . ((the_arity_of Sq) . s)) is Relation-like the Sorts of U1 . ((the_arity_of Sq) . s) -defined the Sorts of U1 . ((the_arity_of Sq) . s) -valued V12() V14() V15() V19() Function-like one-to-one total Element of K10(K11(( the Sorts of U1 . ((the_arity_of Sq) . s)),( the Sorts of U1 . ((the_arity_of Sq) . s))))
K11(( the Sorts of U1 . ((the_arity_of Sq) . s)),( the Sorts of U1 . ((the_arity_of Sq) . s))) is Relation-like set
K10(K11(( the Sorts of U1 . ((the_arity_of Sq) . s)),( the Sorts of U1 . ((the_arity_of Sq) . s)))) is set
(the_arity_of Sq) /. s is Element of the carrier of S
S1 . s is set
S2 . s is set
[(S1 . s),(S2 . s)] is set
{(S1 . s),(S2 . s)} is set
{(S1 . s)} is set
{{(S1 . s),(S2 . s)},{(S1 . s)}} is set
id ( the Sorts of U1 . (the_result_sort_of Sq)) is non empty Relation-like the Sorts of U1 . (the_result_sort_of Sq) -defined the Sorts of U1 . (the_result_sort_of Sq) -valued V12() V14() V15() V19() Function-like one-to-one total Element of K10(K11(( the Sorts of U1 . (the_result_sort_of Sq)),( the Sorts of U1 . (the_result_sort_of Sq))))
( the ResultSort of S * the Sorts of U1) . Sq is non empty set
the ResultSort of S . Sq is Element of the carrier of S
the Sorts of U1 . ( the ResultSort of S . Sq) is non empty set
dom S2 is set
S is non empty non void V68() ManySortedSign
S is non empty non void V68() ManySortedSign
U1 is MSAlgebra over S
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like the carrier of S -defined Function-like total set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
F is Element of the carrier of S
U2 . F is set
the Sorts of U1 . F is set
K11(( the Sorts of U1 . F),( the Sorts of U1 . F)) is Relation-like set
K10(K11(( the Sorts of U1 . F),( the Sorts of U1 . F))) is set
S is non empty non void V68() ManySortedSign
U1 is MSAlgebra over S
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like the carrier of S -defined Function-like total set
F is Element of the carrier of S
the Sorts of U1 . F is set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
(S,U1,U2,F) is Relation-like the Sorts of U1 . F -defined the Sorts of U1 . F -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . F),( the Sorts of U1 . F)))
K11(( the Sorts of U1 . F),( the Sorts of U1 . F)) is Relation-like set
K10(K11(( the Sorts of U1 . F),( the Sorts of U1 . F))) is set
mc is Element of the Sorts of U1 . F
Class ((S,U1,U2,F),mc) is Element of K10(( the Sorts of U1 . F))
K10(( the Sorts of U1 . F)) is set
S is non empty non void V68() ManySortedSign
U1 is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
F is Relation-like Function-like set
dom F is set
mc is non empty Relation-like the carrier of S -defined Function-like total set
qa is set
mc . qa is set
qh is Element of the carrier of S
the Sorts of U1 . qh is non empty set
Sq is set
mc . qh is set
(S,U1,U2,qh) is Relation-like the Sorts of U1 . qh -defined the Sorts of U1 . qh -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh)))
K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh)) is Relation-like set
K10(K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh))) is set
Class (S,U1,U2,qh) is a_partition of the Sorts of U1 . qh
S1 is Element of the Sorts of U1 . qh
Class ((S,U1,U2,qh),S1) is Element of K10(( the Sorts of U1 . qh))
K10(( the Sorts of U1 . qh)) is set
qa is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
qh is Element of the carrier of S
qa . qh is non empty set
the Sorts of U1 . qh is non empty set
(S,U1,U2,qh) is Relation-like the Sorts of U1 . qh -defined the Sorts of U1 . qh -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh)))
K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh)) is Relation-like set
K10(K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh))) is set
Class (S,U1,U2,qh) is a_partition of the Sorts of U1 . qh
F is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
mc is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
qa is set
qh is Element of the carrier of S
F . qh is non empty set
the Sorts of U1 . qh is non empty set
(S,U1,U2,qh) is Relation-like the Sorts of U1 . qh -defined the Sorts of U1 . qh -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh)))
K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh)) is Relation-like set
K10(K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh))) is set
Class (S,U1,U2,qh) is a_partition of the Sorts of U1 . qh
F . qa is set
mc . qa is set
S is non empty non void V68() ManySortedSign
the carrier' of S is non empty set
U1 is non empty Relation-like the carrier' of S -defined Function-like total set
U2 is non empty Relation-like the carrier' of S -defined Function-like total set
F is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of U1,U2
mc is Element of the carrier' of S
F . mc is Relation-like Function-like set
U1 . mc is set
U2 . mc is set
K11((U1 . mc),(U2 . mc)) is Relation-like set
K10(K11((U1 . mc),(U2 . mc))) is set
S is non empty set
U1 is Relation-like K170() -defined S -valued Function-like V42() countable FinSequence-like FinSubsequence-like FinSequence of S
U2 is non empty Relation-like S -defined Function-like total set
U1 * U2 is Relation-like K170() -defined Function-like set
dom U1 is countable Element of K10(K170())
rng U1 is Element of K10(S)
K10(S) is set
dom U2 is non empty Element of K10(S)
dom (U1 * U2) is countable Element of K10(K170())
F is Relation-like dom U1 -defined Function-like total set
mc is Relation-like Function-like set
S is non empty set
U1 is Relation-like K170() -defined S -valued Function-like V42() countable FinSequence-like FinSubsequence-like FinSequence of S
dom U1 is countable Element of K10(K170())
U2 is non empty Relation-like S -defined Function-like total set
U1 * U2 is Relation-like K170() -defined dom U1 -defined Function-like set
rng U1 is Element of K10(S)
K10(S) is set
dom U2 is non empty Element of K10(S)
dom (U1 * U2) is countable Element of K10(K170())
F is Relation-like dom U1 -defined Function-like total set
mc is Relation-like dom U1 -defined Function-like set
S is non empty non void V68() ManySortedSign
the carrier' of S is non empty set
U2 is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U1 is Element of the carrier' of S
Args (U1,U2) is non empty functional Element of rng ( the Sorts of U2 #)
the Sorts of U2 # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
rng ( the Sorts of U2 #) is non empty V4() set
the_arity_of U1 is Relation-like K170() -defined the carrier of S -valued Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
F is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U2) (S,U2) ( the carrier of S, the Sorts of U2, the Sorts of U2)
(S,U2,F) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(the_arity_of U1) * (S,U2,F) is Relation-like non-empty K170() -defined dom (the_arity_of U1) -defined Function-like total set
dom (the_arity_of U1) is countable Element of K10(K170())
product ((the_arity_of U1) * (S,U2,F)) is non empty functional with_common_domain product-like set
mc is Relation-like Function-like Element of Args (U1,U2)
Sq is set
S1 is V41() set
(the_arity_of U1) /. S1 is Element of the carrier of S
the Sorts of U2 . ((the_arity_of U1) /. S1) is non empty set
(S,U2,F,((the_arity_of U1) /. S1)) is Relation-like the Sorts of U2 . ((the_arity_of U1) /. S1) -defined the Sorts of U2 . ((the_arity_of U1) /. S1) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. S1)),( the Sorts of U2 . ((the_arity_of U1) /. S1))))
K11(( the Sorts of U2 . ((the_arity_of U1) /. S1)),( the Sorts of U2 . ((the_arity_of U1) /. S1))) is Relation-like set
K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. S1)),( the Sorts of U2 . ((the_arity_of U1) /. S1)))) is set
mc . S1 is set
Class ((S,U2,F,((the_arity_of U1) /. S1)),(mc . S1)) is Element of K10(( the Sorts of U2 . ((the_arity_of U1) /. S1)))
K10(( the Sorts of U2 . ((the_arity_of U1) /. S1))) is set
S2 is V41() set
(the_arity_of U1) /. S2 is Element of the carrier of S
the Sorts of U2 . ((the_arity_of U1) /. S2) is non empty set
(S,U2,F,((the_arity_of U1) /. S2)) is Relation-like the Sorts of U2 . ((the_arity_of U1) /. S2) -defined the Sorts of U2 . ((the_arity_of U1) /. S2) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. S2)),( the Sorts of U2 . ((the_arity_of U1) /. S2))))
K11(( the Sorts of U2 . ((the_arity_of U1) /. S2)),( the Sorts of U2 . ((the_arity_of U1) /. S2))) is Relation-like set
K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. S2)),( the Sorts of U2 . ((the_arity_of U1) /. S2)))) is set
mc . S2 is set
Class ((S,U2,F,((the_arity_of U1) /. S2)),(mc . S2)) is Element of K10(( the Sorts of U2 . ((the_arity_of U1) /. S2)))
K10(( the Sorts of U2 . ((the_arity_of U1) /. S2))) is set
Sq is Relation-like Function-like set
dom Sq is set
dom ((the_arity_of U1) * (S,U2,F)) is countable Element of K10(K170())
S1 is set
Sq . S1 is set
((the_arity_of U1) * (S,U2,F)) . S1 is set
(the_arity_of U1) . S1 is set
rng (the_arity_of U1) is Element of K10( the carrier of S)
K10( the carrier of S) is set
(the_arity_of U1) * the Sorts of U2 is Relation-like non-empty K170() -defined dom (the_arity_of U1) -defined Function-like total set
dom ((the_arity_of U1) * the Sorts of U2) is countable Element of K10(K170())
((the_arity_of U1) * the Sorts of U2) . S1 is set
the Sorts of U2 . ((the_arity_of U1) . S1) is set
mc . S1 is set
i is Element of the carrier of S
the Sorts of U2 . i is non empty set
S2 is V41() set
Sq . S2 is set
(the_arity_of U1) /. S2 is Element of the carrier of S
the Sorts of U2 . ((the_arity_of U1) /. S2) is non empty set
(S,U2,F,((the_arity_of U1) /. S2)) is Relation-like the Sorts of U2 . ((the_arity_of U1) /. S2) -defined the Sorts of U2 . ((the_arity_of U1) /. S2) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. S2)),( the Sorts of U2 . ((the_arity_of U1) /. S2))))
K11(( the Sorts of U2 . ((the_arity_of U1) /. S2)),( the Sorts of U2 . ((the_arity_of U1) /. S2))) is Relation-like set
K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. S2)),( the Sorts of U2 . ((the_arity_of U1) /. S2)))) is set
mc . S2 is set
Class ((S,U2,F,((the_arity_of U1) /. S2)),(mc . S2)) is Element of K10(( the Sorts of U2 . ((the_arity_of U1) /. S2)))
K10(( the Sorts of U2 . ((the_arity_of U1) /. S2))) is set
(the_arity_of U1) . S2 is set
(S,U2,F,i) is Relation-like the Sorts of U2 . i -defined the Sorts of U2 . i -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . i),( the Sorts of U2 . i)))
K11(( the Sorts of U2 . i),( the Sorts of U2 . i)) is Relation-like set
K10(K11(( the Sorts of U2 . i),( the Sorts of U2 . i))) is set
Class (S,U2,F,i) is a_partition of the Sorts of U2 . i
(S,U2,F) . ((the_arity_of U1) . S1) is set
S1 is Relation-like K170() -defined Function-like (the_arity_of U1) * (S,U2,F) -compatible Element of product ((the_arity_of U1) * (S,U2,F))
S2 is V41() set
S1 . S2 is set
(the_arity_of U1) /. S2 is Element of the carrier of S
the Sorts of U2 . ((the_arity_of U1) /. S2) is non empty set
(S,U2,F,((the_arity_of U1) /. S2)) is Relation-like the Sorts of U2 . ((the_arity_of U1) /. S2) -defined the Sorts of U2 . ((the_arity_of U1) /. S2) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. S2)),( the Sorts of U2 . ((the_arity_of U1) /. S2))))
K11(( the Sorts of U2 . ((the_arity_of U1) /. S2)),( the Sorts of U2 . ((the_arity_of U1) /. S2))) is Relation-like set
K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. S2)),( the Sorts of U2 . ((the_arity_of U1) /. S2)))) is set
mc . S2 is set
Class ((S,U2,F,((the_arity_of U1) /. S2)),(mc . S2)) is Element of K10(( the Sorts of U2 . ((the_arity_of U1) /. S2)))
K10(( the Sorts of U2 . ((the_arity_of U1) /. S2))) is set
qa is Relation-like K170() -defined Function-like (the_arity_of U1) * (S,U2,F) -compatible Element of product ((the_arity_of U1) * (S,U2,F))
qh is Relation-like K170() -defined Function-like (the_arity_of U1) * (S,U2,F) -compatible Element of product ((the_arity_of U1) * (S,U2,F))
Sq is set
qa . Sq is set
qh . Sq is set
S1 is V41() set
qa . S1 is set
(the_arity_of U1) /. S1 is Element of the carrier of S
the Sorts of U2 . ((the_arity_of U1) /. S1) is non empty set
(S,U2,F,((the_arity_of U1) /. S1)) is Relation-like the Sorts of U2 . ((the_arity_of U1) /. S1) -defined the Sorts of U2 . ((the_arity_of U1) /. S1) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. S1)),( the Sorts of U2 . ((the_arity_of U1) /. S1))))
K11(( the Sorts of U2 . ((the_arity_of U1) /. S1)),( the Sorts of U2 . ((the_arity_of U1) /. S1))) is Relation-like set
K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. S1)),( the Sorts of U2 . ((the_arity_of U1) /. S1)))) is set
mc . S1 is set
Class ((S,U2,F,((the_arity_of U1) /. S1)),(mc . S1)) is Element of K10(( the Sorts of U2 . ((the_arity_of U1) /. S1)))
K10(( the Sorts of U2 . ((the_arity_of U1) /. S1))) is set
dom qh is countable Element of K10(K170())
dom qa is countable Element of K10(K170())
S is non empty non void V68() ManySortedSign
the carrier' of S is non empty set
U2 is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
the ResultSort of S * the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
U1 is Element of the carrier' of S
( the ResultSort of S * the Sorts of U2) . U1 is non empty set
F is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U2) (S,U2) ( the carrier of S, the Sorts of U2, the Sorts of U2)
(S,U2,F) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the ResultSort of S * (S,U2,F) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
( the ResultSort of S * (S,U2,F)) . U1 is non empty set
K11((( the ResultSort of S * the Sorts of U2) . U1),(( the ResultSort of S * (S,U2,F)) . U1)) is Relation-like set
K10(K11((( the ResultSort of S * the Sorts of U2) . U1),(( the ResultSort of S * (S,U2,F)) . U1))) is set
the_result_sort_of U1 is Element of the carrier of S
the Sorts of U2 . (the_result_sort_of U1) is non empty set
K10(( the Sorts of U2 . (the_result_sort_of U1))) is set
qh is Relation-like Function-like set
dom qh is set
(S,U2,F) . (the_result_sort_of U1) is non empty set
Sq is set
qh . Sq is set
S1 is Element of the Sorts of U2 . (the_result_sort_of U1)
qh . S1 is set
(S,U2,F,(the_result_sort_of U1),S1) is Element of K10(( the Sorts of U2 . (the_result_sort_of U1)))
(S,U2,F,(the_result_sort_of U1)) is Relation-like the Sorts of U2 . (the_result_sort_of U1) -defined the Sorts of U2 . (the_result_sort_of U1) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . (the_result_sort_of U1)),( the Sorts of U2 . (the_result_sort_of U1))))
K11(( the Sorts of U2 . (the_result_sort_of U1)),( the Sorts of U2 . (the_result_sort_of U1))) is Relation-like set
K10(K11(( the Sorts of U2 . (the_result_sort_of U1)),( the Sorts of U2 . (the_result_sort_of U1)))) is set
Class ((S,U2,F,(the_result_sort_of U1)),S1) is Element of K10(( the Sorts of U2 . (the_result_sort_of U1)))
Class (S,U2,F,(the_result_sort_of U1)) is a_partition of the Sorts of U2 . (the_result_sort_of U1)
dom ( the ResultSort of S * the Sorts of U2) is non empty Element of K10( the carrier' of S)
K10( the carrier' of S) is set
the ResultSort of S . U1 is Element of the carrier of S
the Sorts of U2 . ( the ResultSort of S . U1) is non empty set
dom the ResultSort of S is Element of K10( the carrier' of S)
dom ( the ResultSort of S * (S,U2,F)) is non empty Element of K10( the carrier' of S)
(S,U2,F) . ( the ResultSort of S . U1) is non empty set
Sq is Relation-like ( the ResultSort of S * the Sorts of U2) . U1 -defined ( the ResultSort of S * (S,U2,F)) . U1 -valued Function-like V29(( the ResultSort of S * the Sorts of U2) . U1,( the ResultSort of S * (S,U2,F)) . U1) Element of K10(K11((( the ResultSort of S * the Sorts of U2) . U1),(( the ResultSort of S * (S,U2,F)) . U1)))
S1 is Element of the Sorts of U2 . (the_result_sort_of U1)
Sq . S1 is set
(S,U2,F,(the_result_sort_of U1),S1) is Element of K10(( the Sorts of U2 . (the_result_sort_of U1)))
(S,U2,F,(the_result_sort_of U1)) is Relation-like the Sorts of U2 . (the_result_sort_of U1) -defined the Sorts of U2 . (the_result_sort_of U1) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . (the_result_sort_of U1)),( the Sorts of U2 . (the_result_sort_of U1))))
K11(( the Sorts of U2 . (the_result_sort_of U1)),( the Sorts of U2 . (the_result_sort_of U1))) is Relation-like set
K10(K11(( the Sorts of U2 . (the_result_sort_of U1)),( the Sorts of U2 . (the_result_sort_of U1)))) is set
Class ((S,U2,F,(the_result_sort_of U1)),S1) is Element of K10(( the Sorts of U2 . (the_result_sort_of U1)))
Sq is Relation-like ( the ResultSort of S * the Sorts of U2) . U1 -defined ( the ResultSort of S * (S,U2,F)) . U1 -valued Function-like V29(( the ResultSort of S * the Sorts of U2) . U1,( the ResultSort of S * (S,U2,F)) . U1) Element of K10(K11((( the ResultSort of S * the Sorts of U2) . U1),(( the ResultSort of S * (S,U2,F)) . U1)))
S1 is Relation-like ( the ResultSort of S * the Sorts of U2) . U1 -defined ( the ResultSort of S * (S,U2,F)) . U1 -valued Function-like V29(( the ResultSort of S * the Sorts of U2) . U1,( the ResultSort of S * (S,U2,F)) . U1) Element of K10(K11((( the ResultSort of S * the Sorts of U2) . U1),(( the ResultSort of S * (S,U2,F)) . U1)))
S2 is set
i is Element of the Sorts of U2 . (the_result_sort_of U1)
Sq . i is set
(S,U2,F,(the_result_sort_of U1),i) is Element of K10(( the Sorts of U2 . (the_result_sort_of U1)))
K10(( the Sorts of U2 . (the_result_sort_of U1))) is set
(S,U2,F,(the_result_sort_of U1)) is Relation-like the Sorts of U2 . (the_result_sort_of U1) -defined the Sorts of U2 . (the_result_sort_of U1) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . (the_result_sort_of U1)),( the Sorts of U2 . (the_result_sort_of U1))))
K11(( the Sorts of U2 . (the_result_sort_of U1)),( the Sorts of U2 . (the_result_sort_of U1))) is Relation-like set
K10(K11(( the Sorts of U2 . (the_result_sort_of U1)),( the Sorts of U2 . (the_result_sort_of U1)))) is set
Class ((S,U2,F,(the_result_sort_of U1)),i) is Element of K10(( the Sorts of U2 . (the_result_sort_of U1)))
Sq . S2 is set
S1 . S2 is set
dom ( the ResultSort of S * the Sorts of U2) is non empty Element of K10( the carrier' of S)
K10( the carrier' of S) is set
the ResultSort of S . U1 is Element of the carrier of S
the Sorts of U2 . ( the ResultSort of S . U1) is non empty set
dom Sq is Element of K10((( the ResultSort of S * the Sorts of U2) . U1))
K10((( the ResultSort of S * the Sorts of U2) . U1)) is set
dom S1 is Element of K10((( the ResultSort of S * the Sorts of U2) . U1))
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
the Sorts of U2 # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ( the Sorts of U2 #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
( the Arity of S * ( the Sorts of U2 #)) . U1 is non empty set
(S,U2,F) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U2,F) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
( the Arity of S * ((S,U2,F) #)) . U1 is non empty set
K11((( the Arity of S * ( the Sorts of U2 #)) . U1),(( the Arity of S * ((S,U2,F) #)) . U1)) is Relation-like set
K10(K11((( the Arity of S * ( the Sorts of U2 #)) . U1),(( the Arity of S * ((S,U2,F) #)) . U1))) is set
Args (U1,U2) is non empty functional Element of rng ( the Sorts of U2 #)
rng ( the Sorts of U2 #) is non empty V4() set
the_arity_of U1 is Relation-like K170() -defined the carrier of S -valued Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of U1) * (S,U2,F) is Relation-like non-empty K170() -defined dom (the_arity_of U1) -defined Function-like total set
dom (the_arity_of U1) is countable Element of K10(K170())
product ((the_arity_of U1) * (S,U2,F)) is non empty functional with_common_domain product-like set
qh is Relation-like Function-like set
dom qh is set
dom ( the Arity of S * ( the Sorts of U2 #)) is non empty Element of K10( the carrier' of S)
K10( the carrier' of S) is set
the Arity of S . U1 is Relation-like K170() -defined Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
( the Sorts of U2 #) . ( the Arity of S . U1) is non empty set
( the Sorts of U2 #) . (the_arity_of U1) is non empty set
((S,U2,F) #) . (the_arity_of U1) is non empty set
Sq is set
qh . Sq is set
S1 is Relation-like Function-like Element of Args (U1,U2)
qh . S1 is set
(S,U1,U2,F,S1) is Relation-like K170() -defined Function-like (the_arity_of U1) * (S,U2,F) -compatible Element of product ((the_arity_of U1) * (S,U2,F))
dom ( the Arity of S * ((S,U2,F) #)) is non empty Element of K10( the carrier' of S)
((S,U2,F) #) . ( the Arity of S . U1) is non empty set
Sq is Relation-like ( the Arity of S * ( the Sorts of U2 #)) . U1 -defined ( the Arity of S * ((S,U2,F) #)) . U1 -valued Function-like V29(( the Arity of S * ( the Sorts of U2 #)) . U1,( the Arity of S * ((S,U2,F) #)) . U1) Element of K10(K11((( the Arity of S * ( the Sorts of U2 #)) . U1),(( the Arity of S * ((S,U2,F) #)) . U1)))
S1 is Relation-like Function-like Element of Args (U1,U2)
Sq . S1 is set
(S,U1,U2,F,S1) is Relation-like K170() -defined Function-like (the_arity_of U1) * (S,U2,F) -compatible Element of product ((the_arity_of U1) * (S,U2,F))
the_arity_of U1 is Relation-like K170() -defined the carrier of S -valued Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
qa is Relation-like ( the Arity of S * ( the Sorts of U2 #)) . U1 -defined ( the Arity of S * ((S,U2,F) #)) . U1 -valued Function-like V29(( the Arity of S * ( the Sorts of U2 #)) . U1,( the Arity of S * ((S,U2,F) #)) . U1) Element of K10(K11((( the Arity of S * ( the Sorts of U2 #)) . U1),(( the Arity of S * ((S,U2,F) #)) . U1)))
qh is Relation-like ( the Arity of S * ( the Sorts of U2 #)) . U1 -defined ( the Arity of S * ((S,U2,F) #)) . U1 -valued Function-like V29(( the Arity of S * ( the Sorts of U2 #)) . U1,( the Arity of S * ((S,U2,F) #)) . U1) Element of K10(K11((( the Arity of S * ( the Sorts of U2 #)) . U1),(( the Arity of S * ((S,U2,F) #)) . U1)))
dom ( the Arity of S * ( the Sorts of U2 #)) is non empty Element of K10( the carrier' of S)
K10( the carrier' of S) is set
the Arity of S . U1 is Relation-like K170() -defined Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
( the Sorts of U2 #) . ( the Arity of S . U1) is non empty set
( the Sorts of U2 #) . (the_arity_of U1) is non empty set
Sq is set
S1 is Relation-like Function-like Element of Args (U1,U2)
qa . S1 is set
(S,U1,U2,F,S1) is Relation-like K170() -defined Function-like (the_arity_of U1) * (S,U2,F) -compatible Element of product ((the_arity_of U1) * (S,U2,F))
(the_arity_of U1) * (S,U2,F) is Relation-like non-empty K170() -defined dom (the_arity_of U1) -defined Function-like total set
dom (the_arity_of U1) is countable Element of K10(K170())
product ((the_arity_of U1) * (S,U2,F)) is non empty functional with_common_domain product-like set
qa . Sq is set
qh . Sq is set
dom qa is Element of K10((( the Arity of S * ( the Sorts of U2 #)) . U1))
K10((( the Arity of S * ( the Sorts of U2 #)) . U1)) is set
dom qh is Element of K10((( the Arity of S * ( the Sorts of U2 #)) . U1))
S is non empty non void V68() ManySortedSign
U1 is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the carrier' of S is non empty set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
the ResultSort of S * the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
(S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the ResultSort of S * (S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
mc is set
qa is Element of the carrier' of S
(S,qa,U1,U2) is Relation-like ( the ResultSort of S * the Sorts of U1) . qa -defined ( the ResultSort of S * (S,U1,U2)) . qa -valued Function-like V29(( the ResultSort of S * the Sorts of U1) . qa,( the ResultSort of S * (S,U1,U2)) . qa) Element of K10(K11((( the ResultSort of S * the Sorts of U1) . qa),(( the ResultSort of S * (S,U1,U2)) . qa)))
( the ResultSort of S * the Sorts of U1) . qa is non empty set
( the ResultSort of S * (S,U1,U2)) . qa is non empty set
K11((( the ResultSort of S * the Sorts of U1) . qa),(( the ResultSort of S * (S,U1,U2)) . qa)) is Relation-like set
K10(K11((( the ResultSort of S * the Sorts of U1) . qa),(( the ResultSort of S * (S,U1,U2)) . qa))) is set
qh is Element of the carrier' of S
(S,qh,U1,U2) is Relation-like ( the ResultSort of S * the Sorts of U1) . qh -defined ( the ResultSort of S * (S,U1,U2)) . qh -valued Function-like V29(( the ResultSort of S * the Sorts of U1) . qh,( the ResultSort of S * (S,U1,U2)) . qh) Element of K10(K11((( the ResultSort of S * the Sorts of U1) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)))
( the ResultSort of S * the Sorts of U1) . qh is non empty set
( the ResultSort of S * (S,U1,U2)) . qh is non empty set
K11((( the ResultSort of S * the Sorts of U1) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)) is Relation-like set
K10(K11((( the ResultSort of S * the Sorts of U1) . qh),(( the ResultSort of S * (S,U1,U2)) . qh))) is set
mc is Relation-like Function-like set
dom mc is set
qa is non empty Relation-like the carrier' of S -defined Function-like total set
dom qa is non empty Element of K10( the carrier' of S)
K10( the carrier' of S) is set
qh is set
qa . qh is set
Sq is Element of the carrier' of S
qa . Sq is set
(S,Sq,U1,U2) is Relation-like ( the ResultSort of S * the Sorts of U1) . Sq -defined ( the ResultSort of S * (S,U1,U2)) . Sq -valued Function-like V29(( the ResultSort of S * the Sorts of U1) . Sq,( the ResultSort of S * (S,U1,U2)) . Sq) Element of K10(K11((( the ResultSort of S * the Sorts of U1) . Sq),(( the ResultSort of S * (S,U1,U2)) . Sq)))
( the ResultSort of S * the Sorts of U1) . Sq is non empty set
( the ResultSort of S * (S,U1,U2)) . Sq is non empty set
K11((( the ResultSort of S * the Sorts of U1) . Sq),(( the ResultSort of S * (S,U1,U2)) . Sq)) is Relation-like set
K10(K11((( the ResultSort of S * the Sorts of U1) . Sq),(( the ResultSort of S * (S,U1,U2)) . Sq))) is set
qh is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding set
Sq is set
qh . Sq is Relation-like Function-like set
( the ResultSort of S * the Sorts of U1) . Sq is set
( the ResultSort of S * (S,U1,U2)) . Sq is set
K11((( the ResultSort of S * the Sorts of U1) . Sq),(( the ResultSort of S * (S,U1,U2)) . Sq)) is Relation-like set
K10(K11((( the ResultSort of S * the Sorts of U1) . Sq),(( the ResultSort of S * (S,U1,U2)) . Sq))) is set
S1 is Element of the carrier' of S
qh . S1 is Relation-like Function-like set
(S,S1,U1,U2) is Relation-like ( the ResultSort of S * the Sorts of U1) . S1 -defined ( the ResultSort of S * (S,U1,U2)) . S1 -valued Function-like V29(( the ResultSort of S * the Sorts of U1) . S1,( the ResultSort of S * (S,U1,U2)) . S1) Element of K10(K11((( the ResultSort of S * the Sorts of U1) . S1),(( the ResultSort of S * (S,U1,U2)) . S1)))
( the ResultSort of S * the Sorts of U1) . S1 is non empty set
( the ResultSort of S * (S,U1,U2)) . S1 is non empty set
K11((( the ResultSort of S * the Sorts of U1) . S1),(( the ResultSort of S * (S,U1,U2)) . S1)) is Relation-like set
K10(K11((( the ResultSort of S * the Sorts of U1) . S1),(( the ResultSort of S * (S,U1,U2)) . S1))) is set
Sq is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the ResultSort of S * the Sorts of U1, the ResultSort of S * (S,U1,U2)
S1 is Element of the carrier' of S
( the ResultSort of S * the Sorts of U1) . S1 is non empty set
( the ResultSort of S * (S,U1,U2)) . S1 is non empty set
(S,( the ResultSort of S * the Sorts of U1),( the ResultSort of S * (S,U1,U2)),Sq,S1) is Relation-like ( the ResultSort of S * the Sorts of U1) . S1 -defined ( the ResultSort of S * (S,U1,U2)) . S1 -valued Function-like V29(( the ResultSort of S * the Sorts of U1) . S1,( the ResultSort of S * (S,U1,U2)) . S1) Element of K10(K11((( the ResultSort of S * the Sorts of U1) . S1),(( the ResultSort of S * (S,U1,U2)) . S1)))
K11((( the ResultSort of S * the Sorts of U1) . S1),(( the ResultSort of S * (S,U1,U2)) . S1)) is Relation-like set
K10(K11((( the ResultSort of S * the Sorts of U1) . S1),(( the ResultSort of S * (S,U1,U2)) . S1))) is set
(S,S1,U1,U2) is Relation-like ( the ResultSort of S * the Sorts of U1) . S1 -defined ( the ResultSort of S * (S,U1,U2)) . S1 -valued Function-like V29(( the ResultSort of S * the Sorts of U1) . S1,( the ResultSort of S * (S,U1,U2)) . S1) Element of K10(K11((( the ResultSort of S * the Sorts of U1) . S1),(( the ResultSort of S * (S,U1,U2)) . S1)))
F is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the ResultSort of S * the Sorts of U1, the ResultSort of S * (S,U1,U2)
mc is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the ResultSort of S * the Sorts of U1, the ResultSort of S * (S,U1,U2)
qa is set
qh is Element of the carrier' of S
( the ResultSort of S * the Sorts of U1) . qh is non empty set
( the ResultSort of S * (S,U1,U2)) . qh is non empty set
(S,( the ResultSort of S * the Sorts of U1),( the ResultSort of S * (S,U1,U2)),F,qh) is Relation-like ( the ResultSort of S * the Sorts of U1) . qh -defined ( the ResultSort of S * (S,U1,U2)) . qh -valued Function-like V29(( the ResultSort of S * the Sorts of U1) . qh,( the ResultSort of S * (S,U1,U2)) . qh) Element of K10(K11((( the ResultSort of S * the Sorts of U1) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)))
K11((( the ResultSort of S * the Sorts of U1) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)) is Relation-like set
K10(K11((( the ResultSort of S * the Sorts of U1) . qh),(( the ResultSort of S * (S,U1,U2)) . qh))) is set
(S,qh,U1,U2) is Relation-like ( the ResultSort of S * the Sorts of U1) . qh -defined ( the ResultSort of S * (S,U1,U2)) . qh -valued Function-like V29(( the ResultSort of S * the Sorts of U1) . qh,( the ResultSort of S * (S,U1,U2)) . qh) Element of K10(K11((( the ResultSort of S * the Sorts of U1) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)))
F . qa is Relation-like Function-like set
mc . qa is Relation-like Function-like set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
the Sorts of U1 # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ( the Sorts of U1 #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
(S,U1,U2) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U1,U2) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
mc is set
qa is Element of the carrier' of S
(S,qa,U1,U2) is Relation-like ( the Arity of S * ( the Sorts of U1 #)) . qa -defined ( the Arity of S * ((S,U1,U2) #)) . qa -valued Function-like V29(( the Arity of S * ( the Sorts of U1 #)) . qa,( the Arity of S * ((S,U1,U2) #)) . qa) Element of K10(K11((( the Arity of S * ( the Sorts of U1 #)) . qa),(( the Arity of S * ((S,U1,U2) #)) . qa)))
( the Arity of S * ( the Sorts of U1 #)) . qa is non empty set
( the Arity of S * ((S,U1,U2) #)) . qa is non empty set
K11((( the Arity of S * ( the Sorts of U1 #)) . qa),(( the Arity of S * ((S,U1,U2) #)) . qa)) is Relation-like set
K10(K11((( the Arity of S * ( the Sorts of U1 #)) . qa),(( the Arity of S * ((S,U1,U2) #)) . qa))) is set
qh is Element of the carrier' of S
(S,qh,U1,U2) is Relation-like ( the Arity of S * ( the Sorts of U1 #)) . qh -defined ( the Arity of S * ((S,U1,U2) #)) . qh -valued Function-like V29(( the Arity of S * ( the Sorts of U1 #)) . qh,( the Arity of S * ((S,U1,U2) #)) . qh) Element of K10(K11((( the Arity of S * ( the Sorts of U1 #)) . qh),(( the Arity of S * ((S,U1,U2) #)) . qh)))
( the Arity of S * ( the Sorts of U1 #)) . qh is non empty set
( the Arity of S * ((S,U1,U2) #)) . qh is non empty set
K11((( the Arity of S * ( the Sorts of U1 #)) . qh),(( the Arity of S * ((S,U1,U2) #)) . qh)) is Relation-like set
K10(K11((( the Arity of S * ( the Sorts of U1 #)) . qh),(( the Arity of S * ((S,U1,U2) #)) . qh))) is set
mc is Relation-like Function-like set
dom mc is set
qa is non empty Relation-like the carrier' of S -defined Function-like total set
dom qa is non empty Element of K10( the carrier' of S)
K10( the carrier' of S) is set
qh is set
qa . qh is set
Sq is Element of the carrier' of S
qa . Sq is set
(S,Sq,U1,U2) is Relation-like ( the Arity of S * ( the Sorts of U1 #)) . Sq -defined ( the Arity of S * ((S,U1,U2) #)) . Sq -valued Function-like V29(( the Arity of S * ( the Sorts of U1 #)) . Sq,( the Arity of S * ((S,U1,U2) #)) . Sq) Element of K10(K11((( the Arity of S * ( the Sorts of U1 #)) . Sq),(( the Arity of S * ((S,U1,U2) #)) . Sq)))
( the Arity of S * ( the Sorts of U1 #)) . Sq is non empty set
( the Arity of S * ((S,U1,U2) #)) . Sq is non empty set
K11((( the Arity of S * ( the Sorts of U1 #)) . Sq),(( the Arity of S * ((S,U1,U2) #)) . Sq)) is Relation-like set
K10(K11((( the Arity of S * ( the Sorts of U1 #)) . Sq),(( the Arity of S * ((S,U1,U2) #)) . Sq))) is set
qh is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding set
Sq is set
qh . Sq is Relation-like Function-like set
( the Arity of S * ( the Sorts of U1 #)) . Sq is set
( the Arity of S * ((S,U1,U2) #)) . Sq is set
K11((( the Arity of S * ( the Sorts of U1 #)) . Sq),(( the Arity of S * ((S,U1,U2) #)) . Sq)) is Relation-like set
K10(K11((( the Arity of S * ( the Sorts of U1 #)) . Sq),(( the Arity of S * ((S,U1,U2) #)) . Sq))) is set
S1 is Element of the carrier' of S
qh . S1 is Relation-like Function-like set
(S,S1,U1,U2) is Relation-like ( the Arity of S * ( the Sorts of U1 #)) . S1 -defined ( the Arity of S * ((S,U1,U2) #)) . S1 -valued Function-like V29(( the Arity of S * ( the Sorts of U1 #)) . S1,( the Arity of S * ((S,U1,U2) #)) . S1) Element of K10(K11((( the Arity of S * ( the Sorts of U1 #)) . S1),(( the Arity of S * ((S,U1,U2) #)) . S1)))
( the Arity of S * ( the Sorts of U1 #)) . S1 is non empty set
( the Arity of S * ((S,U1,U2) #)) . S1 is non empty set
K11((( the Arity of S * ( the Sorts of U1 #)) . S1),(( the Arity of S * ((S,U1,U2) #)) . S1)) is Relation-like set
K10(K11((( the Arity of S * ( the Sorts of U1 #)) . S1),(( the Arity of S * ((S,U1,U2) #)) . S1))) is set
Sq is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ( the Sorts of U1 #), the Arity of S * ((S,U1,U2) #)
S1 is Element of the carrier' of S
( the Arity of S * ( the Sorts of U1 #)) . S1 is non empty set
( the Arity of S * ((S,U1,U2) #)) . S1 is non empty set
(S,( the Arity of S * ( the Sorts of U1 #)),( the Arity of S * ((S,U1,U2) #)),Sq,S1) is Relation-like ( the Arity of S * ( the Sorts of U1 #)) . S1 -defined ( the Arity of S * ((S,U1,U2) #)) . S1 -valued Function-like V29(( the Arity of S * ( the Sorts of U1 #)) . S1,( the Arity of S * ((S,U1,U2) #)) . S1) Element of K10(K11((( the Arity of S * ( the Sorts of U1 #)) . S1),(( the Arity of S * ((S,U1,U2) #)) . S1)))
K11((( the Arity of S * ( the Sorts of U1 #)) . S1),(( the Arity of S * ((S,U1,U2) #)) . S1)) is Relation-like set
K10(K11((( the Arity of S * ( the Sorts of U1 #)) . S1),(( the Arity of S * ((S,U1,U2) #)) . S1))) is set
(S,S1,U1,U2) is Relation-like ( the Arity of S * ( the Sorts of U1 #)) . S1 -defined ( the Arity of S * ((S,U1,U2) #)) . S1 -valued Function-like V29(( the Arity of S * ( the Sorts of U1 #)) . S1,( the Arity of S * ((S,U1,U2) #)) . S1) Element of K10(K11((( the Arity of S * ( the Sorts of U1 #)) . S1),(( the Arity of S * ((S,U1,U2) #)) . S1)))
F is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ( the Sorts of U1 #), the Arity of S * ((S,U1,U2) #)
mc is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ( the Sorts of U1 #), the Arity of S * ((S,U1,U2) #)
qa is set
qh is Element of the carrier' of S
( the Arity of S * ( the Sorts of U1 #)) . qh is non empty set
( the Arity of S * ((S,U1,U2) #)) . qh is non empty set
(S,( the Arity of S * ( the Sorts of U1 #)),( the Arity of S * ((S,U1,U2) #)),F,qh) is Relation-like ( the Arity of S * ( the Sorts of U1 #)) . qh -defined ( the Arity of S * ((S,U1,U2) #)) . qh -valued Function-like V29(( the Arity of S * ( the Sorts of U1 #)) . qh,( the Arity of S * ((S,U1,U2) #)) . qh) Element of K10(K11((( the Arity of S * ( the Sorts of U1 #)) . qh),(( the Arity of S * ((S,U1,U2) #)) . qh)))
K11((( the Arity of S * ( the Sorts of U1 #)) . qh),(( the Arity of S * ((S,U1,U2) #)) . qh)) is Relation-like set
K10(K11((( the Arity of S * ( the Sorts of U1 #)) . qh),(( the Arity of S * ((S,U1,U2) #)) . qh))) is set
(S,qh,U1,U2) is Relation-like ( the Arity of S * ( the Sorts of U1 #)) . qh -defined ( the Arity of S * ((S,U1,U2) #)) . qh -valued Function-like V29(( the Arity of S * ( the Sorts of U1 #)) . qh,( the Arity of S * ((S,U1,U2) #)) . qh) Element of K10(K11((( the Arity of S * ( the Sorts of U1 #)) . qh),(( the Arity of S * ((S,U1,U2) #)) . qh)))
F . qa is Relation-like Function-like set
mc . qa is Relation-like Function-like set
S is non empty non void V68() ManySortedSign
the carrier' of S is non empty set
the carrier of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
U1 is Element of the carrier' of S
U2 is non-empty MSAlgebra over S
the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Args (U1,U2) is non empty functional Element of rng ( the Sorts of U2 #)
the Sorts of U2 # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
rng ( the Sorts of U2 #) is non empty V4() set
F is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U2) (S,U2) ( the carrier of S, the Sorts of U2, the Sorts of U2)
(S,U2,F) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U2,F) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U2,F) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
( the Arity of S * ((S,U2,F) #)) . U1 is non empty set
mc is set
the_arity_of U1 is Relation-like K170() -defined the carrier of S -valued Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . U1 is Relation-like K170() -defined Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of U1) * (S,U2,F) is Relation-like non-empty K170() -defined dom (the_arity_of U1) -defined Function-like total set
dom (the_arity_of U1) is countable Element of K10(K170())
product ((the_arity_of U1) * (S,U2,F)) is non empty functional with_common_domain product-like set
dom ((the_arity_of U1) * (S,U2,F)) is countable Element of K10(K170())
qh is Relation-like Function-like set
dom qh is set
Sq is V41() set
qh . Sq is set
(the_arity_of U1) /. Sq is Element of the carrier of S
the Sorts of U2 . ((the_arity_of U1) /. Sq) is non empty set
(S,U2,F,((the_arity_of U1) /. Sq)) is Relation-like the Sorts of U2 . ((the_arity_of U1) /. Sq) -defined the Sorts of U2 . ((the_arity_of U1) /. Sq) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. Sq)),( the Sorts of U2 . ((the_arity_of U1) /. Sq))))
K11(( the Sorts of U2 . ((the_arity_of U1) /. Sq)),( the Sorts of U2 . ((the_arity_of U1) /. Sq))) is Relation-like set
K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. Sq)),( the Sorts of U2 . ((the_arity_of U1) /. Sq)))) is set
Class (S,U2,F,((the_arity_of U1) /. Sq)) is a_partition of the Sorts of U2 . ((the_arity_of U1) /. Sq)
(the_arity_of U1) . Sq is set
((the_arity_of U1) * (S,U2,F)) . Sq is set
S1 is Element of the carrier of S
(S,U2,F) . S1 is non empty set
the Sorts of U2 . S1 is non empty set
(S,U2,F,S1) is Relation-like the Sorts of U2 . S1 -defined the Sorts of U2 . S1 -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . S1),( the Sorts of U2 . S1)))
K11(( the Sorts of U2 . S1),( the Sorts of U2 . S1)) is Relation-like set
K10(K11(( the Sorts of U2 . S1),( the Sorts of U2 . S1))) is set
Class (S,U2,F,S1) is a_partition of the Sorts of U2 . S1
Sq is set
qh . Sq is set
(the_arity_of U1) /. Sq is Element of the carrier of S
S2 is V41() set
qh . S2 is set
S1 is Element of the carrier of S
the Sorts of U2 . S1 is non empty set
(S,U2,F,S1) is Relation-like the Sorts of U2 . S1 -defined the Sorts of U2 . S1 -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . S1),( the Sorts of U2 . S1)))
K11(( the Sorts of U2 . S1),( the Sorts of U2 . S1)) is Relation-like set
K10(K11(( the Sorts of U2 . S1),( the Sorts of U2 . S1))) is set
Class (S,U2,F,S1) is a_partition of the Sorts of U2 . S1
i is set
Class ((S,U2,F,S1),i) is Element of K10(( the Sorts of U2 . S1))
K10(( the Sorts of U2 . S1)) is set
Sq is Relation-like Function-like set
dom Sq is set
dom the Sorts of U2 is non empty Element of K10( the carrier of S)
K10( the carrier of S) is set
rng (the_arity_of U1) is Element of K10( the carrier of S)
(the_arity_of U1) * the Sorts of U2 is Relation-like non-empty K170() -defined dom (the_arity_of U1) -defined Function-like total set
dom ((the_arity_of U1) * the Sorts of U2) is countable Element of K10(K170())
S1 is set
Sq . S1 is set
((the_arity_of U1) * the Sorts of U2) . S1 is set
qh . S1 is set
((the_arity_of U1) * (S,U2,F)) . S1 is set
S2 is V41() set
(the_arity_of U1) /. S2 is Element of the carrier of S
(the_arity_of U1) . S2 is set
i is Element of the carrier of S
(S,U2,F) . i is non empty set
the Sorts of U2 . i is non empty set
(S,U2,F,i) is Relation-like the Sorts of U2 . i -defined the Sorts of U2 . i -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . i),( the Sorts of U2 . i)))
K11(( the Sorts of U2 . i),( the Sorts of U2 . i)) is Relation-like set
K10(K11(( the Sorts of U2 . i),( the Sorts of U2 . i))) is set
Class (S,U2,F,i) is a_partition of the Sorts of U2 . i
Sq . S2 is set
the Arity of S * ( the Sorts of U2 #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
( the Arity of S * ( the Sorts of U2 #)) . U1 is non empty set
product ((the_arity_of U1) * the Sorts of U2) is non empty functional with_common_domain product-like set
S2 is set
i is V41() set
(the_arity_of U1) /. i is Element of the carrier of S
qh . i is set
f is Element of the carrier of S
the Sorts of U2 . f is non empty set
(S,U2,F,f) is Relation-like the Sorts of U2 . f -defined the Sorts of U2 . f -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . f),( the Sorts of U2 . f)))
K11(( the Sorts of U2 . f),( the Sorts of U2 . f)) is Relation-like set
K10(K11(( the Sorts of U2 . f),( the Sorts of U2 . f))) is set
Class (S,U2,F,f) is a_partition of the Sorts of U2 . f
s is set
Class ((S,U2,F,f),s) is Element of K10(( the Sorts of U2 . f))
K10(( the Sorts of U2 . f)) is set
S1 is Relation-like Function-like Element of Args (U1,U2)
S1 . i is set
Class ((S,U2,F,f),(S1 . i)) is Element of K10(( the Sorts of U2 . f))
qh . S2 is set
(S,U1,U2,F,S1) is Relation-like K170() -defined Function-like (the_arity_of U1) * (S,U2,F) -compatible Element of product ((the_arity_of U1) * (S,U2,F))
(S,U1,U2,F,S1) . S2 is set
dom (S,U1,U2,F,S1) is countable Element of K10(K170())
S is non empty non void V68() ManySortedSign
the carrier' of S is non empty set
U2 is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
F is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U2) (S,U2) ( the carrier of S, the Sorts of U2, the Sorts of U2)
(S,U2,F) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U2,F) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U2,F) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
U1 is Element of the carrier' of S
( the Arity of S * ((S,U2,F) #)) . U1 is non empty set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
the ResultSort of S * (S,U2,F) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
( the ResultSort of S * (S,U2,F)) . U1 is non empty set
K11((( the Arity of S * ((S,U2,F) #)) . U1),(( the ResultSort of S * (S,U2,F)) . U1)) is Relation-like set
K10(K11((( the Arity of S * ((S,U2,F) #)) . U1),(( the ResultSort of S * (S,U2,F)) . U1))) is set
Args (U1,U2) is non empty functional Element of rng ( the Sorts of U2 #)
the Sorts of U2 # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
rng ( the Sorts of U2 #) is non empty V4() set
Result (U1,U2) is non empty Element of rng the Sorts of U2
rng the Sorts of U2 is non empty V4() set
the ResultSort of S * the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
( the ResultSort of S * the Sorts of U2) . U1 is non empty set
Den (U1,U2) is Relation-like Args (U1,U2) -defined Result (U1,U2) -valued Function-like V29( Args (U1,U2), Result (U1,U2)) Element of K10(K11((Args (U1,U2)),(Result (U1,U2))))
K11((Args (U1,U2)),(Result (U1,U2))) is Relation-like set
K10(K11((Args (U1,U2)),(Result (U1,U2)))) is set
(S,U1,U2,F) is Relation-like ( the ResultSort of S * the Sorts of U2) . U1 -defined ( the ResultSort of S * (S,U2,F)) . U1 -valued Function-like V29(( the ResultSort of S * the Sorts of U2) . U1,( the ResultSort of S * (S,U2,F)) . U1) Element of K10(K11((( the ResultSort of S * the Sorts of U2) . U1),(( the ResultSort of S * (S,U2,F)) . U1)))
K11((( the ResultSort of S * the Sorts of U2) . U1),(( the ResultSort of S * (S,U2,F)) . U1)) is Relation-like set
K10(K11((( the ResultSort of S * the Sorts of U2) . U1),(( the ResultSort of S * (S,U2,F)) . U1))) is set
(S,U1,U2,F) * (Den (U1,U2)) is Relation-like Args (U1,U2) -defined ( the ResultSort of S * (S,U2,F)) . U1 -valued Function-like Element of K10(K11((Args (U1,U2)),(( the ResultSort of S * (S,U2,F)) . U1)))
K11((Args (U1,U2)),(( the ResultSort of S * (S,U2,F)) . U1)) is Relation-like set
K10(K11((Args (U1,U2)),(( the ResultSort of S * (S,U2,F)) . U1))) is set
the_result_sort_of U1 is Element of the carrier of S
the_arity_of U1 is Relation-like K170() -defined the carrier of S -valued Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
S1 is set
S2 is Relation-like Function-like Element of Args (U1,U2)
(S,U1,U2,F,S2) is Relation-like K170() -defined Function-like (the_arity_of U1) * (S,U2,F) -compatible Element of product ((the_arity_of U1) * (S,U2,F))
(the_arity_of U1) * (S,U2,F) is Relation-like non-empty K170() -defined dom (the_arity_of U1) -defined Function-like total set
dom (the_arity_of U1) is countable Element of K10(K170())
product ((the_arity_of U1) * (S,U2,F)) is non empty functional with_common_domain product-like set
((S,U1,U2,F) * (Den (U1,U2))) . S2 is set
i is set
dom ( the ResultSort of S * (S,U2,F)) is non empty Element of K10( the carrier' of S)
K10( the carrier' of S) is set
the ResultSort of S . U1 is Element of the carrier of S
(S,U2,F) . ( the ResultSort of S . U1) is non empty set
(S,U2,F) . (the_result_sort_of U1) is non empty set
dom ( the ResultSort of S * the Sorts of U2) is non empty Element of K10( the carrier' of S)
the Sorts of U2 . ( the ResultSort of S . U1) is non empty set
the Sorts of U2 . (the_result_sort_of U1) is non empty set
dom (S,U1,U2,F) is Element of K10((( the ResultSort of S * the Sorts of U2) . U1))
K10((( the ResultSort of S * the Sorts of U2) . U1)) is set
rng (Den (U1,U2)) is Element of K10((Result (U1,U2)))
K10((Result (U1,U2))) is set
dom (Den (U1,U2)) is functional Element of K10((Args (U1,U2)))
K10((Args (U1,U2))) is set
dom ((S,U1,U2,F) * (Den (U1,U2))) is functional Element of K10((Args (U1,U2)))
(Den (U1,U2)) . S2 is Element of Result (U1,U2)
(S,U1,U2,F) . ((Den (U1,U2)) . S2) is set
rng (S,U1,U2,F) is Element of K10((( the ResultSort of S * (S,U2,F)) . U1))
K10((( the ResultSort of S * (S,U2,F)) . U1)) is set
f is Relation-like Function-like Element of Args (U1,U2)
(S,U1,U2,F,f) is Relation-like K170() -defined Function-like (the_arity_of U1) * (S,U2,F) -compatible Element of product ((the_arity_of U1) * (S,U2,F))
((S,U1,U2,F) * (Den (U1,U2))) . f is set
(Den (U1,U2)) . f is Element of Result (U1,U2)
x is Element of the Sorts of U2 . (the_result_sort_of U1)
(S,U1,U2,F) . x is set
(S,U2,F,(the_result_sort_of U1),x) is Element of K10(( the Sorts of U2 . (the_result_sort_of U1)))
K10(( the Sorts of U2 . (the_result_sort_of U1))) is set
(S,U2,F,(the_result_sort_of U1)) is Relation-like the Sorts of U2 . (the_result_sort_of U1) -defined the Sorts of U2 . (the_result_sort_of U1) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . (the_result_sort_of U1)),( the Sorts of U2 . (the_result_sort_of U1))))
K11(( the Sorts of U2 . (the_result_sort_of U1)),( the Sorts of U2 . (the_result_sort_of U1))) is Relation-like set
K10(K11(( the Sorts of U2 . (the_result_sort_of U1)),( the Sorts of U2 . (the_result_sort_of U1)))) is set
Class ((S,U2,F,(the_result_sort_of U1)),x) is Element of K10(( the Sorts of U2 . (the_result_sort_of U1)))
dom S2 is set
a is V41() set
S2 . a is set
f . a is set
[(S2 . a),(f . a)] is set
{(S2 . a),(f . a)} is set
{(S2 . a)} is set
{{(S2 . a),(f . a)},{(S2 . a)}} is set
(the_arity_of U1) /. a is Element of the carrier of S
(S,U2,F,((the_arity_of U1) /. a)) is Relation-like the Sorts of U2 . ((the_arity_of U1) /. a) -defined the Sorts of U2 . ((the_arity_of U1) /. a) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. a)),( the Sorts of U2 . ((the_arity_of U1) /. a))))
the Sorts of U2 . ((the_arity_of U1) /. a) is non empty set
K11(( the Sorts of U2 . ((the_arity_of U1) /. a)),( the Sorts of U2 . ((the_arity_of U1) /. a))) is Relation-like set
K10(K11(( the Sorts of U2 . ((the_arity_of U1) /. a)),( the Sorts of U2 . ((the_arity_of U1) /. a)))) is set
(S,U1,U2,F,S2) . a is set
Class ((S,U2,F,((the_arity_of U1) /. a)),(S2 . a)) is Element of K10(( the Sorts of U2 . ((the_arity_of U1) /. a)))
K10(( the Sorts of U2 . ((the_arity_of U1) /. a))) is set
(S,U1,U2,F,f) . a is set
Class ((S,U2,F,((the_arity_of U1) /. a)),(f . a)) is Element of K10(( the Sorts of U2 . ((the_arity_of U1) /. a)))
dom the Sorts of U2 is non empty Element of K10( the carrier of S)
K10( the carrier of S) is set
rng (the_arity_of U1) is Element of K10( the carrier of S)
(the_arity_of U1) * the Sorts of U2 is Relation-like non-empty K170() -defined dom (the_arity_of U1) -defined Function-like total set
dom ((the_arity_of U1) * the Sorts of U2) is countable Element of K10(K170())
((the_arity_of U1) * the Sorts of U2) . a is set
(the_arity_of U1) . a is set
the Sorts of U2 . ((the_arity_of U1) . a) is set
s is Element of the Sorts of U2 . (the_result_sort_of U1)
[s,x] is set
{s,x} is set
{s} is set
{{s,x},{s}} is set
(S,U2,F,(the_result_sort_of U1),s) is Element of K10(( the Sorts of U2 . (the_result_sort_of U1)))
Class ((S,U2,F,(the_result_sort_of U1)),s) is Element of K10(( the Sorts of U2 . (the_result_sort_of U1)))
qh is Relation-like Function-like set
dom qh is set
rng qh is set
Sq is Relation-like ( the Arity of S * ((S,U2,F) #)) . U1 -defined ( the ResultSort of S * (S,U2,F)) . U1 -valued Function-like V29(( the Arity of S * ((S,U2,F) #)) . U1,( the ResultSort of S * (S,U2,F)) . U1) Element of K10(K11((( the Arity of S * ((S,U2,F) #)) . U1),(( the ResultSort of S * (S,U2,F)) . U1)))
S1 is Relation-like Function-like Element of Args (U1,U2)
(S,U1,U2,F,S1) is Relation-like K170() -defined Function-like (the_arity_of U1) * (S,U2,F) -compatible Element of product ((the_arity_of U1) * (S,U2,F))
the_arity_of U1 is Relation-like K170() -defined the carrier of S -valued Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of U1) * (S,U2,F) is Relation-like non-empty K170() -defined dom (the_arity_of U1) -defined Function-like total set
dom (the_arity_of U1) is countable Element of K10(K170())
product ((the_arity_of U1) * (S,U2,F)) is non empty functional with_common_domain product-like set
Sq . (S,U1,U2,F,S1) is set
((S,U1,U2,F) * (Den (U1,U2))) . S1 is set
the_arity_of U1 is Relation-like K170() -defined the carrier of S -valued Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
qa is Relation-like ( the Arity of S * ((S,U2,F) #)) . U1 -defined ( the ResultSort of S * (S,U2,F)) . U1 -valued Function-like V29(( the Arity of S * ((S,U2,F) #)) . U1,( the ResultSort of S * (S,U2,F)) . U1) Element of K10(K11((( the Arity of S * ((S,U2,F) #)) . U1),(( the ResultSort of S * (S,U2,F)) . U1)))
qh is Relation-like ( the Arity of S * ((S,U2,F) #)) . U1 -defined ( the ResultSort of S * (S,U2,F)) . U1 -valued Function-like V29(( the Arity of S * ((S,U2,F) #)) . U1,( the ResultSort of S * (S,U2,F)) . U1) Element of K10(K11((( the Arity of S * ((S,U2,F) #)) . U1),(( the ResultSort of S * (S,U2,F)) . U1)))
dom the Arity of S is Element of K10( the carrier' of S)
K10( the carrier' of S) is set
dom ( the Arity of S * ((S,U2,F) #)) is non empty Element of K10( the carrier' of S)
the Arity of S . U1 is Relation-like K170() -defined Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
((S,U2,F) #) . ( the Arity of S . U1) is non empty set
((S,U2,F) #) . (the_arity_of U1) is non empty set
Sq is set
S1 is Relation-like Function-like Element of Args (U1,U2)
(S,U1,U2,F,S1) is Relation-like K170() -defined Function-like (the_arity_of U1) * (S,U2,F) -compatible Element of product ((the_arity_of U1) * (S,U2,F))
(the_arity_of U1) * (S,U2,F) is Relation-like non-empty K170() -defined dom (the_arity_of U1) -defined Function-like total set
dom (the_arity_of U1) is countable Element of K10(K170())
product ((the_arity_of U1) * (S,U2,F)) is non empty functional with_common_domain product-like set
qa . Sq is set
((S,U1,U2,F) * (Den (U1,U2))) . S1 is set
qh . Sq is set
dom qa is Element of K10((( the Arity of S * ((S,U2,F) #)) . U1))
K10((( the Arity of S * ((S,U2,F) #)) . U1)) is set
dom qh is Element of K10((( the Arity of S * ((S,U2,F) #)) . U1))
S is non empty non void V68() ManySortedSign
U1 is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
(S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1,U2) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U1,U2) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
the ResultSort of S * (S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
mc is set
qa is Element of the carrier' of S
(S,qa,U1,U2) is Relation-like ( the Arity of S * ((S,U1,U2) #)) . qa -defined ( the ResultSort of S * (S,U1,U2)) . qa -valued Function-like V29(( the Arity of S * ((S,U1,U2) #)) . qa,( the ResultSort of S * (S,U1,U2)) . qa) Element of K10(K11((( the Arity of S * ((S,U1,U2) #)) . qa),(( the ResultSort of S * (S,U1,U2)) . qa)))
( the Arity of S * ((S,U1,U2) #)) . qa is non empty set
( the ResultSort of S * (S,U1,U2)) . qa is non empty set
K11((( the Arity of S * ((S,U1,U2) #)) . qa),(( the ResultSort of S * (S,U1,U2)) . qa)) is Relation-like set
K10(K11((( the Arity of S * ((S,U1,U2) #)) . qa),(( the ResultSort of S * (S,U1,U2)) . qa))) is set
qh is Element of the carrier' of S
(S,qh,U1,U2) is Relation-like ( the Arity of S * ((S,U1,U2) #)) . qh -defined ( the ResultSort of S * (S,U1,U2)) . qh -valued Function-like V29(( the Arity of S * ((S,U1,U2) #)) . qh,( the ResultSort of S * (S,U1,U2)) . qh) Element of K10(K11((( the Arity of S * ((S,U1,U2) #)) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)))
( the Arity of S * ((S,U1,U2) #)) . qh is non empty set
( the ResultSort of S * (S,U1,U2)) . qh is non empty set
K11((( the Arity of S * ((S,U1,U2) #)) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)) is Relation-like set
K10(K11((( the Arity of S * ((S,U1,U2) #)) . qh),(( the ResultSort of S * (S,U1,U2)) . qh))) is set
mc is Relation-like Function-like set
dom mc is set
qa is non empty Relation-like the carrier' of S -defined Function-like total set
dom qa is non empty Element of K10( the carrier' of S)
K10( the carrier' of S) is set
qh is set
qa . qh is set
Sq is Element of the carrier' of S
qa . Sq is set
(S,Sq,U1,U2) is Relation-like ( the Arity of S * ((S,U1,U2) #)) . Sq -defined ( the ResultSort of S * (S,U1,U2)) . Sq -valued Function-like V29(( the Arity of S * ((S,U1,U2) #)) . Sq,( the ResultSort of S * (S,U1,U2)) . Sq) Element of K10(K11((( the Arity of S * ((S,U1,U2) #)) . Sq),(( the ResultSort of S * (S,U1,U2)) . Sq)))
( the Arity of S * ((S,U1,U2) #)) . Sq is non empty set
( the ResultSort of S * (S,U1,U2)) . Sq is non empty set
K11((( the Arity of S * ((S,U1,U2) #)) . Sq),(( the ResultSort of S * (S,U1,U2)) . Sq)) is Relation-like set
K10(K11((( the Arity of S * ((S,U1,U2) #)) . Sq),(( the ResultSort of S * (S,U1,U2)) . Sq))) is set
qh is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding set
Sq is set
qh . Sq is Relation-like Function-like set
( the Arity of S * ((S,U1,U2) #)) . Sq is set
( the ResultSort of S * (S,U1,U2)) . Sq is set
K11((( the Arity of S * ((S,U1,U2) #)) . Sq),(( the ResultSort of S * (S,U1,U2)) . Sq)) is Relation-like set
K10(K11((( the Arity of S * ((S,U1,U2) #)) . Sq),(( the ResultSort of S * (S,U1,U2)) . Sq))) is set
S1 is Element of the carrier' of S
qh . S1 is Relation-like Function-like set
(S,S1,U1,U2) is Relation-like ( the Arity of S * ((S,U1,U2) #)) . S1 -defined ( the ResultSort of S * (S,U1,U2)) . S1 -valued Function-like V29(( the Arity of S * ((S,U1,U2) #)) . S1,( the ResultSort of S * (S,U1,U2)) . S1) Element of K10(K11((( the Arity of S * ((S,U1,U2) #)) . S1),(( the ResultSort of S * (S,U1,U2)) . S1)))
( the Arity of S * ((S,U1,U2) #)) . S1 is non empty set
( the ResultSort of S * (S,U1,U2)) . S1 is non empty set
K11((( the Arity of S * ((S,U1,U2) #)) . S1),(( the ResultSort of S * (S,U1,U2)) . S1)) is Relation-like set
K10(K11((( the Arity of S * ((S,U1,U2) #)) . S1),(( the ResultSort of S * (S,U1,U2)) . S1))) is set
Sq is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((S,U1,U2) #), the ResultSort of S * (S,U1,U2)
S1 is Element of the carrier' of S
( the Arity of S * ((S,U1,U2) #)) . S1 is non empty set
( the ResultSort of S * (S,U1,U2)) . S1 is non empty set
(S,( the Arity of S * ((S,U1,U2) #)),( the ResultSort of S * (S,U1,U2)),Sq,S1) is Relation-like ( the Arity of S * ((S,U1,U2) #)) . S1 -defined ( the ResultSort of S * (S,U1,U2)) . S1 -valued Function-like V29(( the Arity of S * ((S,U1,U2) #)) . S1,( the ResultSort of S * (S,U1,U2)) . S1) Element of K10(K11((( the Arity of S * ((S,U1,U2) #)) . S1),(( the ResultSort of S * (S,U1,U2)) . S1)))
K11((( the Arity of S * ((S,U1,U2) #)) . S1),(( the ResultSort of S * (S,U1,U2)) . S1)) is Relation-like set
K10(K11((( the Arity of S * ((S,U1,U2) #)) . S1),(( the ResultSort of S * (S,U1,U2)) . S1))) is set
(S,S1,U1,U2) is Relation-like ( the Arity of S * ((S,U1,U2) #)) . S1 -defined ( the ResultSort of S * (S,U1,U2)) . S1 -valued Function-like V29(( the Arity of S * ((S,U1,U2) #)) . S1,( the ResultSort of S * (S,U1,U2)) . S1) Element of K10(K11((( the Arity of S * ((S,U1,U2) #)) . S1),(( the ResultSort of S * (S,U1,U2)) . S1)))
F is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((S,U1,U2) #), the ResultSort of S * (S,U1,U2)
mc is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((S,U1,U2) #), the ResultSort of S * (S,U1,U2)
qa is set
qh is Element of the carrier' of S
( the Arity of S * ((S,U1,U2) #)) . qh is non empty set
( the ResultSort of S * (S,U1,U2)) . qh is non empty set
(S,( the Arity of S * ((S,U1,U2) #)),( the ResultSort of S * (S,U1,U2)),F,qh) is Relation-like ( the Arity of S * ((S,U1,U2) #)) . qh -defined ( the ResultSort of S * (S,U1,U2)) . qh -valued Function-like V29(( the Arity of S * ((S,U1,U2) #)) . qh,( the ResultSort of S * (S,U1,U2)) . qh) Element of K10(K11((( the Arity of S * ((S,U1,U2) #)) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)))
K11((( the Arity of S * ((S,U1,U2) #)) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)) is Relation-like set
K10(K11((( the Arity of S * ((S,U1,U2) #)) . qh),(( the ResultSort of S * (S,U1,U2)) . qh))) is set
(S,qh,U1,U2) is Relation-like ( the Arity of S * ((S,U1,U2) #)) . qh -defined ( the ResultSort of S * (S,U1,U2)) . qh -valued Function-like V29(( the Arity of S * ((S,U1,U2) #)) . qh,( the ResultSort of S * (S,U1,U2)) . qh) Element of K10(K11((( the Arity of S * ((S,U1,U2) #)) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)))
F . qa is Relation-like Function-like set
mc . qa is Relation-like Function-like set
S is non empty non void V68() ManySortedSign
U1 is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
(S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1,U2) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((S,U1,U2) #), the ResultSort of S * (S,U1,U2)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
(S,U1,U2) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U1,U2) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
the ResultSort of S * (S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1,U2),(S,U1,U2) #) is strict MSAlgebra over S
S is non empty non void V68() ManySortedSign
U1 is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
(S,U1,U2) is MSAlgebra over S
(S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1,U2) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((S,U1,U2) #), the ResultSort of S * (S,U1,U2)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
(S,U1,U2) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U1,U2) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
the ResultSort of S * (S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1,U2),(S,U1,U2) #) is strict MSAlgebra over S
S is non empty non void V68() ManySortedSign
U1 is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
F is Element of the carrier of S
the Sorts of U1 . F is non empty set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
(S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1,U2) . F is non empty set
K11(( the Sorts of U1 . F),((S,U1,U2) . F)) is Relation-like set
K10(K11(( the Sorts of U1 . F),((S,U1,U2) . F))) is set
(S,U1,U2,F) is Relation-like the Sorts of U1 . F -defined the Sorts of U1 . F -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . F),( the Sorts of U1 . F)))
K11(( the Sorts of U1 . F),( the Sorts of U1 . F)) is Relation-like set
K10(K11(( the Sorts of U1 . F),( the Sorts of U1 . F))) is set
K10(( the Sorts of U1 . F)) is set
mc is Relation-like Function-like set
dom mc is set
qa is set
mc . qa is set
Class ((S,U1,U2,F),qa) is Element of K10(( the Sorts of U1 . F))
Class (S,U1,U2,F) is a_partition of the Sorts of U1 . F
qa is Relation-like the Sorts of U1 . F -defined (S,U1,U2) . F -valued Function-like V29( the Sorts of U1 . F,(S,U1,U2) . F) Element of K10(K11(( the Sorts of U1 . F),((S,U1,U2) . F)))
qh is set
qa . qh is set
Class ((S,U1,U2,F),qh) is Element of K10(( the Sorts of U1 . F))
mc is Relation-like the Sorts of U1 . F -defined (S,U1,U2) . F -valued Function-like V29( the Sorts of U1 . F,(S,U1,U2) . F) Element of K10(K11(( the Sorts of U1 . F),((S,U1,U2) . F)))
qa is Relation-like the Sorts of U1 . F -defined (S,U1,U2) . F -valued Function-like V29( the Sorts of U1 . F,(S,U1,U2) . F) Element of K10(K11(( the Sorts of U1 . F),((S,U1,U2) . F)))
qh is set
mc . qh is set
Class ((S,U1,U2,F),qh) is Element of K10(( the Sorts of U1 . F))
K10(( the Sorts of U1 . F)) is set
qa . qh is set
dom mc is Element of K10(( the Sorts of U1 . F))
dom qa is Element of K10(( the Sorts of U1 . F))
S is non empty non void V68() ManySortedSign
U1 is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
(S,U1,U2) is strict non-empty MSAlgebra over S
(S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1,U2) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((S,U1,U2) #), the ResultSort of S * (S,U1,U2)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
(S,U1,U2) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U1,U2) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
the ResultSort of S * (S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1,U2),(S,U1,U2) #) is strict MSAlgebra over S
the Sorts of (S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
F is Relation-like Function-like set
dom F is set
mc is non empty Relation-like the carrier of S -defined Function-like total set
dom mc is non empty Element of K10( the carrier of S)
K10( the carrier of S) is set
qa is set
mc . qa is set
qh is Element of the carrier of S
mc . qh is set
(S,U1,U2,qh) is Relation-like the Sorts of U1 . qh -defined (S,U1,U2) . qh -valued Function-like V29( the Sorts of U1 . qh,(S,U1,U2) . qh) Element of K10(K11(( the Sorts of U1 . qh),((S,U1,U2) . qh)))
the Sorts of U1 . qh is non empty set
(S,U1,U2) . qh is non empty set
K11(( the Sorts of U1 . qh),((S,U1,U2) . qh)) is Relation-like set
K10(K11(( the Sorts of U1 . qh),((S,U1,U2) . qh))) is set
qa is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding set
qh is set
qa . qh is Relation-like Function-like set
the Sorts of U1 . qh is set
(S,U1,U2) . qh is set
K11(( the Sorts of U1 . qh),((S,U1,U2) . qh)) is Relation-like set
K10(K11(( the Sorts of U1 . qh),((S,U1,U2) . qh))) is set
Sq is Element of the carrier of S
qa . Sq is Relation-like Function-like set
(S,U1,U2,Sq) is Relation-like the Sorts of U1 . Sq -defined (S,U1,U2) . Sq -valued Function-like V29( the Sorts of U1 . Sq,(S,U1,U2) . Sq) Element of K10(K11(( the Sorts of U1 . Sq),((S,U1,U2) . Sq)))
the Sorts of U1 . Sq is non empty set
(S,U1,U2) . Sq is non empty set
K11(( the Sorts of U1 . Sq),((S,U1,U2) . Sq)) is Relation-like set
K10(K11(( the Sorts of U1 . Sq),((S,U1,U2) . Sq))) is set
qh is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of U1,(S,U1,U2)
Sq is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of U1, the Sorts of (S,U1,U2)
S1 is Element of the carrier of S
the Sorts of U1 . S1 is non empty set
the Sorts of (S,U1,U2) . S1 is non empty set
(S,U1,U2) . S1 is non empty set
Sq . S1 is Relation-like the Sorts of U1 . S1 -defined the Sorts of (S,U1,U2) . S1 -valued Function-like V29( the Sorts of U1 . S1, the Sorts of (S,U1,U2) . S1) Element of K10(K11(( the Sorts of U1 . S1),( the Sorts of (S,U1,U2) . S1)))
K11(( the Sorts of U1 . S1),( the Sorts of (S,U1,U2) . S1)) is Relation-like set
K10(K11(( the Sorts of U1 . S1),( the Sorts of (S,U1,U2) . S1))) is set
(S,U1,U2,S1) is Relation-like the Sorts of U1 . S1 -defined (S,U1,U2) . S1 -valued Function-like V29( the Sorts of U1 . S1,(S,U1,U2) . S1) Element of K10(K11(( the Sorts of U1 . S1),((S,U1,U2) . S1)))
K11(( the Sorts of U1 . S1),((S,U1,U2) . S1)) is Relation-like set
K10(K11(( the Sorts of U1 . S1),((S,U1,U2) . S1))) is set
F is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of U1, the Sorts of (S,U1,U2)
mc is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of U1, the Sorts of (S,U1,U2)
qa is set
qh is Element of the carrier of S
the Sorts of U1 . qh is non empty set
the Sorts of (S,U1,U2) . qh is non empty set
(S,U1,U2) . qh is non empty set
F . qh is Relation-like the Sorts of U1 . qh -defined the Sorts of (S,U1,U2) . qh -valued Function-like V29( the Sorts of U1 . qh, the Sorts of (S,U1,U2) . qh) Element of K10(K11(( the Sorts of U1 . qh),( the Sorts of (S,U1,U2) . qh)))
K11(( the Sorts of U1 . qh),( the Sorts of (S,U1,U2) . qh)) is Relation-like set
K10(K11(( the Sorts of U1 . qh),( the Sorts of (S,U1,U2) . qh))) is set
(S,U1,U2,qh) is Relation-like the Sorts of U1 . qh -defined (S,U1,U2) . qh -valued Function-like V29( the Sorts of U1 . qh,(S,U1,U2) . qh) Element of K10(K11(( the Sorts of U1 . qh),((S,U1,U2) . qh)))
K11(( the Sorts of U1 . qh),((S,U1,U2) . qh)) is Relation-like set
K10(K11(( the Sorts of U1 . qh),((S,U1,U2) . qh))) is set
F . qa is Relation-like Function-like set
mc . qa is Relation-like Function-like set
S is non empty non void V68() ManySortedSign
the carrier of S is non empty set
U1 is non-empty MSAlgebra over S
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
(S,U1,U2) is strict non-empty MSAlgebra over S
(S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1,U2) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((S,U1,U2) #), the ResultSort of S * (S,U1,U2)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
(S,U1,U2) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U1,U2) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
the ResultSort of S * (S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1,U2),(S,U1,U2) #) is strict MSAlgebra over S
(S,U1,U2) is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of U1, the Sorts of (S,U1,U2)
the Sorts of (S,U1,U2) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
qh is Element of the carrier' of S
Args (qh,U1) is non empty functional Element of rng ( the Sorts of U1 #)
the Sorts of U1 # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
rng ( the Sorts of U1 #) is non empty V4() set
the_result_sort_of qh is Element of the carrier of S
(S,U1,U2) . (the_result_sort_of qh) is Relation-like the Sorts of U1 . (the_result_sort_of qh) -defined the Sorts of (S,U1,U2) . (the_result_sort_of qh) -valued Function-like V29( the Sorts of U1 . (the_result_sort_of qh), the Sorts of (S,U1,U2) . (the_result_sort_of qh)) Element of K10(K11(( the Sorts of U1 . (the_result_sort_of qh)),( the Sorts of (S,U1,U2) . (the_result_sort_of qh))))
the Sorts of U1 . (the_result_sort_of qh) is non empty set
the Sorts of (S,U1,U2) . (the_result_sort_of qh) is non empty set
K11(( the Sorts of U1 . (the_result_sort_of qh)),( the Sorts of (S,U1,U2) . (the_result_sort_of qh))) is Relation-like set
K10(K11(( the Sorts of U1 . (the_result_sort_of qh)),( the Sorts of (S,U1,U2) . (the_result_sort_of qh)))) is set
Result (qh,U1) is non empty Element of rng the Sorts of U1
rng the Sorts of U1 is non empty V4() set
Den (qh,U1) is Relation-like Args (qh,U1) -defined Result (qh,U1) -valued Function-like V29( Args (qh,U1), Result (qh,U1)) Element of K10(K11((Args (qh,U1)),(Result (qh,U1))))
K11((Args (qh,U1)),(Result (qh,U1))) is Relation-like set
K10(K11((Args (qh,U1)),(Result (qh,U1)))) is set
Args (qh,(S,U1,U2)) is non empty functional Element of rng ( the Sorts of (S,U1,U2) #)
the Sorts of (S,U1,U2) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
rng ( the Sorts of (S,U1,U2) #) is non empty V4() set
Result (qh,(S,U1,U2)) is non empty Element of rng the Sorts of (S,U1,U2)
rng the Sorts of (S,U1,U2) is non empty V4() set
Den (qh,(S,U1,U2)) is Relation-like Args (qh,(S,U1,U2)) -defined Result (qh,(S,U1,U2)) -valued Function-like V29( Args (qh,(S,U1,U2)), Result (qh,(S,U1,U2))) Element of K10(K11((Args (qh,(S,U1,U2))),(Result (qh,(S,U1,U2)))))
K11((Args (qh,(S,U1,U2))),(Result (qh,(S,U1,U2)))) is Relation-like set
K10(K11((Args (qh,(S,U1,U2))),(Result (qh,(S,U1,U2))))) is set
Sq is Relation-like Function-like Element of Args (qh,U1)
(Den (qh,U1)) . Sq is Element of Result (qh,U1)
((S,U1,U2) . (the_result_sort_of qh)) . ((Den (qh,U1)) . Sq) is set
(S,U1,U2) # Sq is Relation-like Function-like Element of Args (qh,(S,U1,U2))
(Den (qh,(S,U1,U2))) . ((S,U1,U2) # Sq) is Element of Result (qh,(S,U1,U2))
the_arity_of qh is Relation-like K170() -defined the carrier of S -valued Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . qh is Relation-like K170() -defined Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
( the Arity of S * ((S,U1,U2) #)) . qh is non empty set
(the_arity_of qh) * (S,U1,U2) is Relation-like non-empty K170() -defined dom (the_arity_of qh) -defined Function-like total set
dom (the_arity_of qh) is countable Element of K10(K170())
product ((the_arity_of qh) * (S,U1,U2)) is non empty functional with_common_domain product-like set
dom Sq is set
(S,qh,U1,U2,Sq) is Relation-like K170() -defined Function-like (the_arity_of qh) * (S,U1,U2) -compatible Element of product ((the_arity_of qh) * (S,U1,U2))
i is set
((S,U1,U2) # Sq) . i is set
(S,qh,U1,U2,Sq) . i is set
f is V41() set
(the_arity_of qh) /. f is Element of the carrier of S
(S,U1,U2,((the_arity_of qh) /. f)) is Relation-like the Sorts of U1 . ((the_arity_of qh) /. f) -defined (S,U1,U2) . ((the_arity_of qh) /. f) -valued Function-like V29( the Sorts of U1 . ((the_arity_of qh) /. f),(S,U1,U2) . ((the_arity_of qh) /. f)) Element of K10(K11(( the Sorts of U1 . ((the_arity_of qh) /. f)),((S,U1,U2) . ((the_arity_of qh) /. f))))
the Sorts of U1 . ((the_arity_of qh) /. f) is non empty set
(S,U1,U2) . ((the_arity_of qh) /. f) is non empty set
K11(( the Sorts of U1 . ((the_arity_of qh) /. f)),((S,U1,U2) . ((the_arity_of qh) /. f))) is Relation-like set
K10(K11(( the Sorts of U1 . ((the_arity_of qh) /. f)),((S,U1,U2) . ((the_arity_of qh) /. f)))) is set
(the_arity_of qh) * the Sorts of U1 is Relation-like non-empty K170() -defined dom (the_arity_of qh) -defined Function-like total set
dom ((the_arity_of qh) * the Sorts of U1) is countable Element of K10(K170())
((the_arity_of qh) * the Sorts of U1) . f is set
(the_arity_of qh) . f is set
the Sorts of U1 . ((the_arity_of qh) . f) is set
Sq . f is set
(S,U1,U2) . ((the_arity_of qh) /. f) is Relation-like the Sorts of U1 . ((the_arity_of qh) /. f) -defined the Sorts of (S,U1,U2) . ((the_arity_of qh) /. f) -valued Function-like V29( the Sorts of U1 . ((the_arity_of qh) /. f), the Sorts of (S,U1,U2) . ((the_arity_of qh) /. f)) Element of K10(K11(( the Sorts of U1 . ((the_arity_of qh) /. f)),( the Sorts of (S,U1,U2) . ((the_arity_of qh) /. f))))
the Sorts of (S,U1,U2) . ((the_arity_of qh) /. f) is non empty set
K11(( the Sorts of U1 . ((the_arity_of qh) /. f)),( the Sorts of (S,U1,U2) . ((the_arity_of qh) /. f))) is Relation-like set
K10(K11(( the Sorts of U1 . ((the_arity_of qh) /. f)),( the Sorts of (S,U1,U2) . ((the_arity_of qh) /. f)))) is set
((S,U1,U2) . ((the_arity_of qh) /. f)) . (Sq . f) is set
a is Element of the Sorts of U1 . ((the_arity_of qh) /. f)
(S,U1,U2,((the_arity_of qh) /. f)) . a is Element of (S,U1,U2) . ((the_arity_of qh) /. f)
(S,U1,U2,((the_arity_of qh) /. f)) is Relation-like the Sorts of U1 . ((the_arity_of qh) /. f) -defined the Sorts of U1 . ((the_arity_of qh) /. f) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . ((the_arity_of qh) /. f)),( the Sorts of U1 . ((the_arity_of qh) /. f))))
K11(( the Sorts of U1 . ((the_arity_of qh) /. f)),( the Sorts of U1 . ((the_arity_of qh) /. f))) is Relation-like set
K10(K11(( the Sorts of U1 . ((the_arity_of qh) /. f)),( the Sorts of U1 . ((the_arity_of qh) /. f)))) is set
Class ((S,U1,U2,((the_arity_of qh) /. f)),(Sq . f)) is Element of K10(( the Sorts of U1 . ((the_arity_of qh) /. f)))
K10(( the Sorts of U1 . ((the_arity_of qh) /. f))) is set
dom the Sorts of U1 is non empty Element of K10( the carrier of S)
K10( the carrier of S) is set
rng the ResultSort of S is Element of K10( the carrier of S)
dom the ResultSort of S is Element of K10( the carrier' of S)
K10( the carrier' of S) is set
the ResultSort of S * the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
dom ( the ResultSort of S * the Sorts of U1) is non empty Element of K10( the carrier' of S)
( the ResultSort of S * the Sorts of U1) . qh is non empty set
the ResultSort of S . qh is Element of the carrier of S
the Sorts of U1 . ( the ResultSort of S . qh) is non empty set
rng (Den (qh,U1)) is Element of K10((Result (qh,U1)))
K10((Result (qh,U1))) is set
(S,qh,U1,U2) is Relation-like ( the ResultSort of S * the Sorts of U1) . qh -defined ( the ResultSort of S * (S,U1,U2)) . qh -valued Function-like V29(( the ResultSort of S * the Sorts of U1) . qh,( the ResultSort of S * (S,U1,U2)) . qh) Element of K10(K11((( the ResultSort of S * the Sorts of U1) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)))
( the ResultSort of S * (S,U1,U2)) . qh is non empty set
K11((( the ResultSort of S * the Sorts of U1) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)) is Relation-like set
K10(K11((( the ResultSort of S * the Sorts of U1) . qh),(( the ResultSort of S * (S,U1,U2)) . qh))) is set
dom (S,qh,U1,U2) is Element of K10((( the ResultSort of S * the Sorts of U1) . qh))
K10((( the ResultSort of S * the Sorts of U1) . qh)) is set
dom (Den (qh,U1)) is functional Element of K10((Args (qh,U1)))
K10((Args (qh,U1))) is set
(S,qh,U1,U2) * (Den (qh,U1)) is Relation-like Args (qh,U1) -defined ( the ResultSort of S * (S,U1,U2)) . qh -valued Function-like Element of K10(K11((Args (qh,U1)),(( the ResultSort of S * (S,U1,U2)) . qh)))
K11((Args (qh,U1)),(( the ResultSort of S * (S,U1,U2)) . qh)) is Relation-like set
K10(K11((Args (qh,U1)),(( the ResultSort of S * (S,U1,U2)) . qh))) is set
dom ((S,qh,U1,U2) * (Den (qh,U1))) is functional Element of K10((Args (qh,U1)))
dom (S,U1,U2) is non empty Element of K10( the carrier of S)
dom (S,qh,U1,U2,Sq) is countable Element of K10(K170())
dom ((the_arity_of qh) * (S,U1,U2)) is countable Element of K10(K170())
rng (the_arity_of qh) is Element of K10( the carrier of S)
dom ((S,U1,U2) # Sq) is set
(S,( the Arity of S * ((S,U1,U2) #)),( the ResultSort of S * (S,U1,U2)),(S,U1,U2),qh) is Relation-like ( the Arity of S * ((S,U1,U2) #)) . qh -defined ( the ResultSort of S * (S,U1,U2)) . qh -valued Function-like V29(( the Arity of S * ((S,U1,U2) #)) . qh,( the ResultSort of S * (S,U1,U2)) . qh) Element of K10(K11((( the Arity of S * ((S,U1,U2) #)) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)))
K11((( the Arity of S * ((S,U1,U2) #)) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)) is Relation-like set
K10(K11((( the Arity of S * ((S,U1,U2) #)) . qh),(( the ResultSort of S * (S,U1,U2)) . qh))) is set
(S,qh,U1,U2) is Relation-like ( the Arity of S * ((S,U1,U2) #)) . qh -defined ( the ResultSort of S * (S,U1,U2)) . qh -valued Function-like V29(( the Arity of S * ((S,U1,U2) #)) . qh,( the ResultSort of S * (S,U1,U2)) . qh) Element of K10(K11((( the Arity of S * ((S,U1,U2) #)) . qh),(( the ResultSort of S * (S,U1,U2)) . qh)))
((S,qh,U1,U2) * (Den (qh,U1))) . Sq is set
i is Element of the Sorts of U1 . (the_result_sort_of qh)
(S,qh,U1,U2) . i is set
(S,U1,U2,(the_result_sort_of qh),i) is Element of K10(( the Sorts of U1 . (the_result_sort_of qh)))
K10(( the Sorts of U1 . (the_result_sort_of qh))) is set
(S,U1,U2,(the_result_sort_of qh)) is Relation-like the Sorts of U1 . (the_result_sort_of qh) -defined the Sorts of U1 . (the_result_sort_of qh) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . (the_result_sort_of qh)),( the Sorts of U1 . (the_result_sort_of qh))))
K11(( the Sorts of U1 . (the_result_sort_of qh)),( the Sorts of U1 . (the_result_sort_of qh))) is Relation-like set
K10(K11(( the Sorts of U1 . (the_result_sort_of qh)),( the Sorts of U1 . (the_result_sort_of qh)))) is set
Class ((S,U1,U2,(the_result_sort_of qh)),i) is Element of K10(( the Sorts of U1 . (the_result_sort_of qh)))
(S,U1,U2) . (the_result_sort_of qh) is non empty set
(S,U1,U2,(the_result_sort_of qh)) is Relation-like the Sorts of U1 . (the_result_sort_of qh) -defined (S,U1,U2) . (the_result_sort_of qh) -valued Function-like V29( the Sorts of U1 . (the_result_sort_of qh),(S,U1,U2) . (the_result_sort_of qh)) Element of K10(K11(( the Sorts of U1 . (the_result_sort_of qh)),((S,U1,U2) . (the_result_sort_of qh))))
K11(( the Sorts of U1 . (the_result_sort_of qh)),((S,U1,U2) . (the_result_sort_of qh))) is Relation-like set
K10(K11(( the Sorts of U1 . (the_result_sort_of qh)),((S,U1,U2) . (the_result_sort_of qh)))) is set
(S,U1,U2,(the_result_sort_of qh)) . i is Element of (S,U1,U2) . (the_result_sort_of qh)
qh is set
(S,U1,U2) . qh is Relation-like Function-like set
rng ((S,U1,U2) . qh) is set
the Sorts of (S,U1,U2) . qh is set
Sq is Element of the carrier of S
the Sorts of U1 . Sq is non empty set
the Sorts of (S,U1,U2) . Sq is non empty set
K11(( the Sorts of U1 . Sq),( the Sorts of (S,U1,U2) . Sq)) is Relation-like set
K10(K11(( the Sorts of U1 . Sq),( the Sorts of (S,U1,U2) . Sq))) is set
S1 is Relation-like the Sorts of U1 . Sq -defined the Sorts of (S,U1,U2) . Sq -valued Function-like V29( the Sorts of U1 . Sq, the Sorts of (S,U1,U2) . Sq) Element of K10(K11(( the Sorts of U1 . Sq),( the Sorts of (S,U1,U2) . Sq)))
dom S1 is Element of K10(( the Sorts of U1 . Sq))
K10(( the Sorts of U1 . Sq)) is set
(S,U1,U2,Sq) is Relation-like the Sorts of U1 . Sq -defined the Sorts of U1 . Sq -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . Sq),( the Sorts of U1 . Sq)))
K11(( the Sorts of U1 . Sq),( the Sorts of U1 . Sq)) is Relation-like set
K10(K11(( the Sorts of U1 . Sq),( the Sorts of U1 . Sq))) is set
Class (S,U1,U2,Sq) is a_partition of the Sorts of U1 . Sq
rng S1 is Element of K10(( the Sorts of (S,U1,U2) . Sq))
K10(( the Sorts of (S,U1,U2) . Sq)) is set
S2 is set
(S,U1,U2) . Sq is non empty set
(S,U1,U2,Sq) is Relation-like the Sorts of U1 . Sq -defined (S,U1,U2) . Sq -valued Function-like V29( the Sorts of U1 . Sq,(S,U1,U2) . Sq) Element of K10(K11(( the Sorts of U1 . Sq),((S,U1,U2) . Sq)))
K11(( the Sorts of U1 . Sq),((S,U1,U2) . Sq)) is Relation-like set
K10(K11(( the Sorts of U1 . Sq),((S,U1,U2) . Sq))) is set
i is set
Class ((S,U1,U2,Sq),i) is Element of K10(( the Sorts of U1 . Sq))
S1 . i is set
S is non empty non void V68() ManySortedSign
the carrier of S is non empty set
U1 is non-empty MSAlgebra over S
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 is non-empty MSAlgebra over S
the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
mc is Element of the carrier of S
the Sorts of U1 . mc is non empty set
K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc)) is Relation-like set
K10(K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc))) is set
the Sorts of U2 . mc is non empty set
F is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of U1, the Sorts of U2
F . mc is Relation-like the Sorts of U1 . mc -defined the Sorts of U2 . mc -valued Function-like V29( the Sorts of U1 . mc, the Sorts of U2 . mc) Element of K10(K11(( the Sorts of U1 . mc),( the Sorts of U2 . mc)))
K11(( the Sorts of U1 . mc),( the Sorts of U2 . mc)) is Relation-like set
K10(K11(( the Sorts of U1 . mc),( the Sorts of U2 . mc))) is set
qh is set
(F . mc) . qh is set
Sq is set
(F . mc) . Sq is set
qh is set
(F . mc) . qh is set
Sq is set
(F . mc) . Sq is set
S1 is set
(F . mc) . S1 is set
qh is set
(F . mc) . qh is set
qh is Relation-like the Sorts of U1 . mc -defined the Sorts of U1 . mc -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc)))
Sq is Element of the Sorts of U1 . mc
S1 is Element of the Sorts of U1 . mc
[Sq,S1] is set
{Sq,S1} is set
{Sq} is set
{{Sq,S1},{Sq}} is set
(F . mc) . Sq is Element of the Sorts of U2 . mc
(F . mc) . S1 is Element of the Sorts of U2 . mc
qa is Relation-like the Sorts of U1 . mc -defined the Sorts of U1 . mc -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc)))
qh is Relation-like the Sorts of U1 . mc -defined the Sorts of U1 . mc -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc)))
Sq is set
S1 is set
[Sq,S1] is set
{Sq,S1} is set
{Sq} is set
{{Sq,S1},{Sq}} is set
S2 is Element of the Sorts of U1 . mc
(F . mc) . S2 is Element of the Sorts of U2 . mc
i is Element of the Sorts of U1 . mc
(F . mc) . i is Element of the Sorts of U2 . mc
S2 is Element of the Sorts of U1 . mc
(F . mc) . S2 is Element of the Sorts of U2 . mc
i is Element of the Sorts of U1 . mc
(F . mc) . i is Element of the Sorts of U2 . mc
S is non empty non void V68() ManySortedSign
the carrier of S is non empty set
U1 is non-empty MSAlgebra over S
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 is non-empty MSAlgebra over S
the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
F is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of U1, the Sorts of U2
mc is Relation-like Function-like set
dom mc is set
qa is non empty Relation-like the carrier of S -defined Function-like total set
qh is set
qa . qh is set
the Sorts of U1 . qh is set
K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh)) is Relation-like set
K10(K11(( the Sorts of U1 . qh),( the Sorts of U1 . qh))) is set
Sq is Element of the carrier of S
(S,U1,U2,F,Sq) is Relation-like the Sorts of U1 . Sq -defined the Sorts of U1 . Sq -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . Sq),( the Sorts of U1 . Sq)))
the Sorts of U1 . Sq is non empty set
K11(( the Sorts of U1 . Sq),( the Sorts of U1 . Sq)) is Relation-like set
K10(K11(( the Sorts of U1 . Sq),( the Sorts of U1 . Sq))) is set
qh is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ( the carrier of S, the Sorts of U1, the Sorts of U1)
Sq is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ( the carrier of S, the Sorts of U1, the Sorts of U1)
S1 is set
the Sorts of U1 . S1 is set
K11(( the Sorts of U1 . S1),( the Sorts of U1 . S1)) is Relation-like set
K10(K11(( the Sorts of U1 . S1),( the Sorts of U1 . S1))) is set
Sq . S1 is set
S2 is Relation-like the Sorts of U1 . S1 -defined the Sorts of U1 . S1 -valued Element of K10(K11(( the Sorts of U1 . S1),( the Sorts of U1 . S1)))
i is Element of the carrier of S
(S,U1,U2,F,i) is Relation-like the Sorts of U1 . i -defined the Sorts of U1 . i -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . i),( the Sorts of U1 . i)))
the Sorts of U1 . i is non empty set
K11(( the Sorts of U1 . i),( the Sorts of U1 . i)) is Relation-like set
K10(K11(( the Sorts of U1 . i),( the Sorts of U1 . i))) is set
the carrier' of S is non empty set
S1 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
S2 is Element of the carrier' of S
Args (S2,U1) is non empty functional Element of rng ( the Sorts of U1 #)
the Sorts of U1 # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
rng ( the Sorts of U1 #) is non empty V4() set
the_arity_of S2 is Relation-like K170() -defined the carrier of S -valued Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
Result (S2,U1) is non empty Element of rng the Sorts of U1
rng the Sorts of U1 is non empty V4() set
Den (S2,U1) is Relation-like Args (S2,U1) -defined Result (S2,U1) -valued Function-like V29( Args (S2,U1), Result (S2,U1)) Element of K10(K11((Args (S2,U1)),(Result (S2,U1))))
K11((Args (S2,U1)),(Result (S2,U1))) is Relation-like set
K10(K11((Args (S2,U1)),(Result (S2,U1)))) is set
the_result_sort_of S2 is Element of the carrier of S
(S,U1,S1,(the_result_sort_of S2)) is Relation-like the Sorts of U1 . (the_result_sort_of S2) -defined the Sorts of U1 . (the_result_sort_of S2) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . (the_result_sort_of S2)),( the Sorts of U1 . (the_result_sort_of S2))))
the Sorts of U1 . (the_result_sort_of S2) is non empty set
K11(( the Sorts of U1 . (the_result_sort_of S2)),( the Sorts of U1 . (the_result_sort_of S2))) is Relation-like set
K10(K11(( the Sorts of U1 . (the_result_sort_of S2)),( the Sorts of U1 . (the_result_sort_of S2)))) is set
i is Relation-like Function-like Element of Args (S2,U1)
dom i is set
f is Relation-like Function-like Element of Args (S2,U1)
(Den (S2,U1)) . i is Element of Result (S2,U1)
(Den (S2,U1)) . f is Element of Result (S2,U1)
[((Den (S2,U1)) . i),((Den (S2,U1)) . f)] is set
{((Den (S2,U1)) . i),((Den (S2,U1)) . f)} is set
{((Den (S2,U1)) . i)} is set
{{((Den (S2,U1)) . i),((Den (S2,U1)) . f)},{((Den (S2,U1)) . i)}} is set
dom (the_arity_of S2) is countable Element of K10(K170())
dom f is set
a is set
F # i is Relation-like Function-like Element of Args (S2,U2)
Args (S2,U2) is non empty functional Element of rng ( the Sorts of U2 #)
the Sorts of U2 # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
rng ( the Sorts of U2 #) is non empty V4() set
a1 is V41() set
(F # i) . a1 is set
(the_arity_of S2) /. a1 is Element of the carrier of S
F . ((the_arity_of S2) /. a1) is Relation-like the Sorts of U1 . ((the_arity_of S2) /. a1) -defined the Sorts of U2 . ((the_arity_of S2) /. a1) -valued Function-like V29( the Sorts of U1 . ((the_arity_of S2) /. a1), the Sorts of U2 . ((the_arity_of S2) /. a1)) Element of K10(K11(( the Sorts of U1 . ((the_arity_of S2) /. a1)),( the Sorts of U2 . ((the_arity_of S2) /. a1))))
the Sorts of U1 . ((the_arity_of S2) /. a1) is non empty set
the Sorts of U2 . ((the_arity_of S2) /. a1) is non empty set
K11(( the Sorts of U1 . ((the_arity_of S2) /. a1)),( the Sorts of U2 . ((the_arity_of S2) /. a1))) is Relation-like set
K10(K11(( the Sorts of U1 . ((the_arity_of S2) /. a1)),( the Sorts of U2 . ((the_arity_of S2) /. a1)))) is set
i . a1 is set
(F . ((the_arity_of S2) /. a1)) . (i . a1) is set
F # f is Relation-like Function-like Element of Args (S2,U2)
(F # f) . a1 is set
f . a1 is set
(F . ((the_arity_of S2) /. a1)) . (f . a1) is set
(the_arity_of S2) . a1 is set
rng (the_arity_of S2) is Element of K10( the carrier of S)
K10( the carrier of S) is set
(the_arity_of S2) * the Sorts of U1 is Relation-like non-empty K170() -defined dom (the_arity_of S2) -defined Function-like total set
dom ((the_arity_of S2) * the Sorts of U1) is countable Element of K10(K170())
((the_arity_of S2) * the Sorts of U1) . a is set
Dy is Element of the carrier of S
the Sorts of U1 . Dy is non empty set
x1 is Element of the Sorts of U1 . Dy
y1 is Element of the Sorts of U1 . Dy
[x1,y1] is set
{x1,y1} is set
{x1} is set
{{x1,y1},{x1}} is set
(S,U1,S1,((the_arity_of S2) /. a1)) is Relation-like the Sorts of U1 . ((the_arity_of S2) /. a1) -defined the Sorts of U1 . ((the_arity_of S2) /. a1) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . ((the_arity_of S2) /. a1)),( the Sorts of U1 . ((the_arity_of S2) /. a1))))
K11(( the Sorts of U1 . ((the_arity_of S2) /. a1)),( the Sorts of U1 . ((the_arity_of S2) /. a1))) is Relation-like set
K10(K11(( the Sorts of U1 . ((the_arity_of S2) /. a1)),( the Sorts of U1 . ((the_arity_of S2) /. a1)))) is set
(S,U1,U2,F,Dy) is Relation-like the Sorts of U1 . Dy -defined the Sorts of U1 . Dy -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . Dy),( the Sorts of U1 . Dy)))
K11(( the Sorts of U1 . Dy),( the Sorts of U1 . Dy)) is Relation-like set
K10(K11(( the Sorts of U1 . Dy),( the Sorts of U1 . Dy))) is set
(F # i) . a is set
(F # f) . a is set
dom (F # i) is set
dom (F # f) is set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
dom the ResultSort of S is Element of K10( the carrier' of S)
K10( the carrier' of S) is set
the ResultSort of S * the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
dom ( the ResultSort of S * the Sorts of U1) is non empty Element of K10( the carrier' of S)
( the ResultSort of S * the Sorts of U1) . S2 is non empty set
the ResultSort of S . S2 is Element of the carrier of S
the Sorts of U1 . ( the ResultSort of S . S2) is non empty set
a is Element of the carrier of S
the Sorts of U1 . a is non empty set
the Sorts of U2 . a is non empty set
F . a is Relation-like the Sorts of U1 . a -defined the Sorts of U2 . a -valued Function-like V29( the Sorts of U1 . a, the Sorts of U2 . a) Element of K10(K11(( the Sorts of U1 . a),( the Sorts of U2 . a)))
K11(( the Sorts of U1 . a),( the Sorts of U2 . a)) is Relation-like set
K10(K11(( the Sorts of U1 . a),( the Sorts of U2 . a))) is set
Dy is Element of the Sorts of U1 . a
(F . a) . Dy is Element of the Sorts of U2 . a
Result (S2,U2) is non empty Element of rng the Sorts of U2
rng the Sorts of U2 is non empty V4() set
Den (S2,U2) is Relation-like Args (S2,U2) -defined Result (S2,U2) -valued Function-like V29( Args (S2,U2), Result (S2,U2)) Element of K10(K11((Args (S2,U2)),(Result (S2,U2))))
K11((Args (S2,U2)),(Result (S2,U2))) is Relation-like set
K10(K11((Args (S2,U2)),(Result (S2,U2)))) is set
(Den (S2,U2)) . (F # f) is Element of Result (S2,U2)
(S,U1,S1,a) is Relation-like the Sorts of U1 . a -defined the Sorts of U1 . a -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . a),( the Sorts of U1 . a)))
K11(( the Sorts of U1 . a),( the Sorts of U1 . a)) is Relation-like set
K10(K11(( the Sorts of U1 . a),( the Sorts of U1 . a))) is set
(S,U1,U2,F,a) is Relation-like the Sorts of U1 . a -defined the Sorts of U1 . a -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . a),( the Sorts of U1 . a)))
a1 is Element of the Sorts of U1 . a
(F . a) . a1 is Element of the Sorts of U2 . a
(Den (S2,U2)) . (F # i) is Element of Result (S2,U2)
S2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
i is Element of the carrier of S
the Sorts of U1 . i is non empty set
(S,U1,S2,i) is Relation-like the Sorts of U1 . i -defined the Sorts of U1 . i -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . i),( the Sorts of U1 . i)))
K11(( the Sorts of U1 . i),( the Sorts of U1 . i)) is Relation-like set
K10(K11(( the Sorts of U1 . i),( the Sorts of U1 . i))) is set
(S,U1,U2,F,i) is Relation-like the Sorts of U1 . i -defined the Sorts of U1 . i -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . i),( the Sorts of U1 . i)))
mc is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
qa is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
qh is set
Sq is Element of the carrier of S
the Sorts of U1 . Sq is non empty set
(S,U1,mc,Sq) is Relation-like the Sorts of U1 . Sq -defined the Sorts of U1 . Sq -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . Sq),( the Sorts of U1 . Sq)))
K11(( the Sorts of U1 . Sq),( the Sorts of U1 . Sq)) is Relation-like set
K10(K11(( the Sorts of U1 . Sq),( the Sorts of U1 . Sq))) is set
(S,U1,U2,F,Sq) is Relation-like the Sorts of U1 . Sq -defined the Sorts of U1 . Sq -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . Sq),( the Sorts of U1 . Sq)))
mc . qh is set
qa . qh is set
S is non empty non void V68() ManySortedSign
the carrier of S is non empty set
U1 is non-empty MSAlgebra over S
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 is non-empty MSAlgebra over S
the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
F is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of U1, the Sorts of U2
(S,U1,U2,F) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
(S,U1,(S,U1,U2,F)) is strict non-empty MSAlgebra over S
(S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1,(S,U1,U2,F)) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((S,U1,(S,U1,U2,F)) #), the ResultSort of S * (S,U1,(S,U1,U2,F))
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
(S,U1,(S,U1,U2,F)) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U1,(S,U1,U2,F)) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
the ResultSort of S * (S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1,(S,U1,U2,F)),(S,U1,(S,U1,U2,F)) #) is strict MSAlgebra over S
the Sorts of (S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
mc is Element of the carrier of S
the Sorts of (S,U1,(S,U1,U2,F)) . mc is non empty set
the Sorts of U2 . mc is non empty set
K11(( the Sorts of (S,U1,(S,U1,U2,F)) . mc),( the Sorts of U2 . mc)) is Relation-like set
K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . mc),( the Sorts of U2 . mc))) is set
the Sorts of U1 . mc is non empty set
(S,U1,U2,F,mc) is Relation-like the Sorts of U1 . mc -defined the Sorts of U1 . mc -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc)))
K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc)) is Relation-like set
K10(K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc))) is set
F . mc is Relation-like the Sorts of U1 . mc -defined the Sorts of U2 . mc -valued Function-like V29( the Sorts of U1 . mc, the Sorts of U2 . mc) Element of K10(K11(( the Sorts of U1 . mc),( the Sorts of U2 . mc)))
K11(( the Sorts of U1 . mc),( the Sorts of U2 . mc)) is Relation-like set
K10(K11(( the Sorts of U1 . mc),( the Sorts of U2 . mc))) is set
(S,U1,(S,U1,U2,F),mc) is Relation-like the Sorts of U1 . mc -defined the Sorts of U1 . mc -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc)))
Class (S,U1,(S,U1,U2,F),mc) is a_partition of the Sorts of U1 . mc
Class (S,U1,U2,F,mc) is a_partition of the Sorts of U1 . mc
S2 is set
K10(( the Sorts of U1 . mc)) is set
i is Element of K10(( the Sorts of U1 . mc))
f is set
Class ((S,U1,U2,F,mc),f) is Element of K10(( the Sorts of U1 . mc))
s is Element of the Sorts of U1 . mc
(F . mc) . s is Element of the Sorts of U2 . mc
x is Element of the Sorts of U2 . mc
a is Element of the Sorts of U1 . mc
Class ((S,U1,U2,F,mc),a) is Element of K10(( the Sorts of U1 . mc))
(F . mc) . a is Element of the Sorts of U2 . mc
Class ((S,U1,U2,F,mc),s) is Element of K10(( the Sorts of U1 . mc))
[a,s] is set
{a,s} is set
{a} is set
{{a,s},{a}} is set
S2 is Relation-like Function-like set
dom S2 is set
rng S2 is set
i is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . mc -defined the Sorts of U2 . mc -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . mc, the Sorts of U2 . mc) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . mc),( the Sorts of U2 . mc)))
f is Element of the Sorts of U1 . mc
Class ((S,U1,U2,F,mc),f) is Element of K10(( the Sorts of U1 . mc))
K10(( the Sorts of U1 . mc)) is set
i . (Class ((S,U1,U2,F,mc),f)) is set
(F . mc) . f is Element of the Sorts of U2 . mc
S2 is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . mc -defined the Sorts of U2 . mc -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . mc, the Sorts of U2 . mc) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . mc),( the Sorts of U2 . mc)))
i is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . mc -defined the Sorts of U2 . mc -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . mc, the Sorts of U2 . mc) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . mc),( the Sorts of U2 . mc)))
(S,U1,(S,U1,U2,F),mc) is Relation-like the Sorts of U1 . mc -defined the Sorts of U1 . mc -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . mc),( the Sorts of U1 . mc)))
Class (S,U1,(S,U1,U2,F),mc) is a_partition of the Sorts of U1 . mc
Class (S,U1,U2,F,mc) is a_partition of the Sorts of U1 . mc
f is set
S2 . f is set
i . f is set
K10(( the Sorts of U1 . mc)) is set
s is Element of K10(( the Sorts of U1 . mc))
x is set
Class ((S,U1,U2,F,mc),x) is Element of K10(( the Sorts of U1 . mc))
a is Element of the Sorts of U1 . mc
(F . mc) . a is Element of the Sorts of U2 . mc
S is non empty non void V68() ManySortedSign
the carrier of S is non empty set
U1 is non-empty MSAlgebra over S
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 is non-empty MSAlgebra over S
the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
F is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of U1, the Sorts of U2
(S,U1,U2,F) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
(S,U1,(S,U1,U2,F)) is strict non-empty MSAlgebra over S
(S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1,(S,U1,U2,F)) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((S,U1,(S,U1,U2,F)) #), the ResultSort of S * (S,U1,(S,U1,U2,F))
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
(S,U1,(S,U1,U2,F)) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U1,(S,U1,U2,F)) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
the ResultSort of S * (S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1,(S,U1,U2,F)),(S,U1,(S,U1,U2,F)) #) is strict MSAlgebra over S
the Sorts of (S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
mc is Relation-like Function-like set
dom mc is set
qa is non empty Relation-like the carrier of S -defined Function-like total set
dom qa is non empty Element of K10( the carrier of S)
K10( the carrier of S) is set
qh is set
qa . qh is set
Sq is Element of the carrier of S
qa . Sq is set
(S,U1,U2,F,Sq) is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . Sq -defined the Sorts of U2 . Sq -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . Sq, the Sorts of U2 . Sq) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . Sq),( the Sorts of U2 . Sq)))
the Sorts of (S,U1,(S,U1,U2,F)) . Sq is non empty set
the Sorts of U2 . Sq is non empty set
K11(( the Sorts of (S,U1,(S,U1,U2,F)) . Sq),( the Sorts of U2 . Sq)) is Relation-like set
K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . Sq),( the Sorts of U2 . Sq))) is set
qh is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding set
Sq is set
qh . Sq is Relation-like Function-like set
the Sorts of (S,U1,(S,U1,U2,F)) . Sq is set
the Sorts of U2 . Sq is set
K11(( the Sorts of (S,U1,(S,U1,U2,F)) . Sq),( the Sorts of U2 . Sq)) is Relation-like set
K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . Sq),( the Sorts of U2 . Sq))) is set
S1 is Element of the carrier of S
qh . S1 is Relation-like Function-like set
(S,U1,U2,F,S1) is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . S1 -defined the Sorts of U2 . S1 -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . S1, the Sorts of U2 . S1) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . S1),( the Sorts of U2 . S1)))
the Sorts of (S,U1,(S,U1,U2,F)) . S1 is non empty set
the Sorts of U2 . S1 is non empty set
K11(( the Sorts of (S,U1,(S,U1,U2,F)) . S1),( the Sorts of U2 . S1)) is Relation-like set
K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . S1),( the Sorts of U2 . S1))) is set
Sq is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (S,U1,(S,U1,U2,F)), the Sorts of U2
S1 is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (S,U1,(S,U1,U2,F)), the Sorts of U2
S2 is Element of the carrier of S
the Sorts of (S,U1,(S,U1,U2,F)) . S2 is non empty set
the Sorts of U2 . S2 is non empty set
S1 . S2 is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . S2 -defined the Sorts of U2 . S2 -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . S2, the Sorts of U2 . S2) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . S2),( the Sorts of U2 . S2)))
K11(( the Sorts of (S,U1,(S,U1,U2,F)) . S2),( the Sorts of U2 . S2)) is Relation-like set
K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . S2),( the Sorts of U2 . S2))) is set
(S,U1,U2,F,S2) is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . S2 -defined the Sorts of U2 . S2 -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . S2, the Sorts of U2 . S2) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . S2),( the Sorts of U2 . S2)))
mc is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (S,U1,(S,U1,U2,F)), the Sorts of U2
qa is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (S,U1,(S,U1,U2,F)), the Sorts of U2
qh is set
Sq is Element of the carrier of S
the Sorts of (S,U1,(S,U1,U2,F)) . Sq is non empty set
the Sorts of U2 . Sq is non empty set
mc . Sq is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . Sq -defined the Sorts of U2 . Sq -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . Sq, the Sorts of U2 . Sq) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . Sq),( the Sorts of U2 . Sq)))
K11(( the Sorts of (S,U1,(S,U1,U2,F)) . Sq),( the Sorts of U2 . Sq)) is Relation-like set
K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . Sq),( the Sorts of U2 . Sq))) is set
(S,U1,U2,F,Sq) is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . Sq -defined the Sorts of U2 . Sq -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . Sq, the Sorts of U2 . Sq) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . Sq),( the Sorts of U2 . Sq)))
mc . qh is Relation-like Function-like set
qa . qh is Relation-like Function-like set
S is non empty non void V68() ManySortedSign
the carrier of S is non empty set
U1 is non-empty MSAlgebra over S
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 is non-empty MSAlgebra over S
the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
F is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of U1, the Sorts of U2
(S,U1,U2,F) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
(S,U1,(S,U1,U2,F)) is strict non-empty MSAlgebra over S
(S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1,(S,U1,U2,F)) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((S,U1,(S,U1,U2,F)) #), the ResultSort of S * (S,U1,(S,U1,U2,F))
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
(S,U1,(S,U1,U2,F)) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U1,(S,U1,U2,F)) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
the ResultSort of S * (S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1,(S,U1,U2,F)),(S,U1,(S,U1,U2,F)) #) is strict MSAlgebra over S
(S,U1,U2,F) is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (S,U1,(S,U1,U2,F)), the Sorts of U2
the Sorts of (S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
S1 is Element of the carrier' of S
Args (S1,(S,U1,(S,U1,U2,F))) is non empty functional Element of rng ( the Sorts of (S,U1,(S,U1,U2,F)) #)
the Sorts of (S,U1,(S,U1,U2,F)) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
rng ( the Sorts of (S,U1,(S,U1,U2,F)) #) is non empty V4() set
the_result_sort_of S1 is Element of the carrier of S
(S,U1,U2,F) . (the_result_sort_of S1) is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . (the_result_sort_of S1) -defined the Sorts of U2 . (the_result_sort_of S1) -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . (the_result_sort_of S1), the Sorts of U2 . (the_result_sort_of S1)) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . (the_result_sort_of S1)),( the Sorts of U2 . (the_result_sort_of S1))))
the Sorts of (S,U1,(S,U1,U2,F)) . (the_result_sort_of S1) is non empty set
the Sorts of U2 . (the_result_sort_of S1) is non empty set
K11(( the Sorts of (S,U1,(S,U1,U2,F)) . (the_result_sort_of S1)),( the Sorts of U2 . (the_result_sort_of S1))) is Relation-like set
K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . (the_result_sort_of S1)),( the Sorts of U2 . (the_result_sort_of S1)))) is set
Result (S1,(S,U1,(S,U1,U2,F))) is non empty Element of rng the Sorts of (S,U1,(S,U1,U2,F))
rng the Sorts of (S,U1,(S,U1,U2,F)) is non empty V4() set
Den (S1,(S,U1,(S,U1,U2,F))) is Relation-like Args (S1,(S,U1,(S,U1,U2,F))) -defined Result (S1,(S,U1,(S,U1,U2,F))) -valued Function-like V29( Args (S1,(S,U1,(S,U1,U2,F))), Result (S1,(S,U1,(S,U1,U2,F)))) Element of K10(K11((Args (S1,(S,U1,(S,U1,U2,F)))),(Result (S1,(S,U1,(S,U1,U2,F))))))
K11((Args (S1,(S,U1,(S,U1,U2,F)))),(Result (S1,(S,U1,(S,U1,U2,F))))) is Relation-like set
K10(K11((Args (S1,(S,U1,(S,U1,U2,F)))),(Result (S1,(S,U1,(S,U1,U2,F)))))) is set
Args (S1,U2) is non empty functional Element of rng ( the Sorts of U2 #)
the Sorts of U2 # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
rng ( the Sorts of U2 #) is non empty V4() set
Result (S1,U2) is non empty Element of rng the Sorts of U2
rng the Sorts of U2 is non empty V4() set
Den (S1,U2) is Relation-like Args (S1,U2) -defined Result (S1,U2) -valued Function-like V29( Args (S1,U2), Result (S1,U2)) Element of K10(K11((Args (S1,U2)),(Result (S1,U2))))
K11((Args (S1,U2)),(Result (S1,U2))) is Relation-like set
K10(K11((Args (S1,U2)),(Result (S1,U2)))) is set
S2 is Relation-like Function-like Element of Args (S1,(S,U1,(S,U1,U2,F)))
(Den (S1,(S,U1,(S,U1,U2,F)))) . S2 is Element of Result (S1,(S,U1,(S,U1,U2,F)))
((S,U1,U2,F) . (the_result_sort_of S1)) . ((Den (S1,(S,U1,(S,U1,U2,F)))) . S2) is set
(S,U1,U2,F) # S2 is Relation-like Function-like Element of Args (S1,U2)
(Den (S1,U2)) . ((S,U1,U2,F) # S2) is Element of Result (S1,U2)
the_arity_of S1 is Relation-like K170() -defined the carrier of S -valued Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
dom S2 is set
dom (the_arity_of S1) is countable Element of K10(K170())
( the Arity of S * ((S,U1,(S,U1,U2,F)) #)) . S1 is non empty set
Args (S1,U1) is non empty functional Element of rng ( the Sorts of U1 #)
the Sorts of U1 # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
rng ( the Sorts of U1 #) is non empty V4() set
s is Relation-like Function-like Element of Args (S1,U1)
(S,S1,U1,(S,U1,U2,F),s) is Relation-like K170() -defined Function-like (the_arity_of S1) * (S,U1,(S,U1,U2,F)) -compatible Element of product ((the_arity_of S1) * (S,U1,(S,U1,U2,F)))
(the_arity_of S1) * (S,U1,(S,U1,U2,F)) is Relation-like non-empty K170() -defined dom (the_arity_of S1) -defined Function-like total set
product ((the_arity_of S1) * (S,U1,(S,U1,U2,F))) is non empty functional with_common_domain product-like set
dom s is set
x is set
a is V41() set
(the_arity_of S1) . a is set
rng (the_arity_of S1) is Element of K10( the carrier of S)
K10( the carrier of S) is set
(the_arity_of S1) /. a is Element of the carrier of S
S2 . a is set
a is Element of the carrier of S
the Sorts of U1 . a is non empty set
(S,U1,(S,U1,U2,F),a) is Relation-like the Sorts of U1 . a -defined the Sorts of U1 . a -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . a),( the Sorts of U1 . a)))
K11(( the Sorts of U1 . a),( the Sorts of U1 . a)) is Relation-like set
K10(K11(( the Sorts of U1 . a),( the Sorts of U1 . a))) is set
s . a is set
Class ((S,U1,(S,U1,U2,F),a),(s . a)) is Element of K10(( the Sorts of U1 . a))
K10(( the Sorts of U1 . a)) is set
(S,U1,U2,F,a) is Relation-like the Sorts of U1 . a -defined the Sorts of U1 . a -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . a),( the Sorts of U1 . a)))
Class ((S,U1,U2,F,a),(s . a)) is Element of K10(( the Sorts of U1 . a))
(the_arity_of S1) * the Sorts of U1 is Relation-like non-empty K170() -defined dom (the_arity_of S1) -defined Function-like total set
dom ((the_arity_of S1) * the Sorts of U1) is countable Element of K10(K170())
((the_arity_of S1) * the Sorts of U1) . a is set
((S,U1,U2,F) # S2) . a is set
(S,U1,U2,F) . a is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . a -defined the Sorts of U2 . a -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . a, the Sorts of U2 . a) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . a),( the Sorts of U2 . a)))
the Sorts of (S,U1,(S,U1,U2,F)) . a is non empty set
the Sorts of U2 . a is non empty set
K11(( the Sorts of (S,U1,(S,U1,U2,F)) . a),( the Sorts of U2 . a)) is Relation-like set
K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . a),( the Sorts of U2 . a))) is set
((S,U1,U2,F) . a) . (S2 . a) is set
(S,U1,U2,F,a) is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . a -defined the Sorts of U2 . a -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . a, the Sorts of U2 . a) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . a),( the Sorts of U2 . a)))
(S,U1,U2,F,a) . (S2 . a) is set
F . a is Relation-like the Sorts of U1 . a -defined the Sorts of U2 . a -valued Function-like V29( the Sorts of U1 . a, the Sorts of U2 . a) Element of K10(K11(( the Sorts of U1 . a),( the Sorts of U2 . a)))
K11(( the Sorts of U1 . a),( the Sorts of U2 . a)) is Relation-like set
K10(K11(( the Sorts of U1 . a),( the Sorts of U2 . a))) is set
a1 is Element of the Sorts of U1 . a
(F . a) . a1 is Element of the Sorts of U2 . a
F # s is Relation-like Function-like Element of Args (S1,U2)
(F # s) . a is set
((S,U1,U2,F) # S2) . x is set
(F # s) . x is set
the ResultSort of S * the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
dom ( the ResultSort of S * the Sorts of U1) is non empty Element of K10( the carrier' of S)
K10( the carrier' of S) is set
( the ResultSort of S * the Sorts of U1) . S1 is non empty set
the ResultSort of S . S1 is Element of the carrier of S
the Sorts of U1 . ( the ResultSort of S . S1) is non empty set
the Sorts of U1 . (the_result_sort_of S1) is non empty set
Result (S1,U1) is non empty Element of rng the Sorts of U1
rng the Sorts of U1 is non empty V4() set
Den (S1,U1) is Relation-like Args (S1,U1) -defined Result (S1,U1) -valued Function-like V29( Args (S1,U1), Result (S1,U1)) Element of K10(K11((Args (S1,U1)),(Result (S1,U1))))
K11((Args (S1,U1)),(Result (S1,U1))) is Relation-like set
K10(K11((Args (S1,U1)),(Result (S1,U1)))) is set
rng (Den (S1,U1)) is Element of K10((Result (S1,U1)))
K10((Result (S1,U1))) is set
(S,S1,U1,(S,U1,U2,F)) is Relation-like ( the ResultSort of S * the Sorts of U1) . S1 -defined ( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1 -valued Function-like V29(( the ResultSort of S * the Sorts of U1) . S1,( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1) Element of K10(K11((( the ResultSort of S * the Sorts of U1) . S1),(( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1)))
( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1 is non empty set
K11((( the ResultSort of S * the Sorts of U1) . S1),(( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1)) is Relation-like set
K10(K11((( the ResultSort of S * the Sorts of U1) . S1),(( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1))) is set
dom (S,S1,U1,(S,U1,U2,F)) is Element of K10((( the ResultSort of S * the Sorts of U1) . S1))
K10((( the ResultSort of S * the Sorts of U1) . S1)) is set
dom (Den (S1,U1)) is functional Element of K10((Args (S1,U1)))
K10((Args (S1,U1))) is set
(S,S1,U1,(S,U1,U2,F)) * (Den (S1,U1)) is Relation-like Args (S1,U1) -defined ( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1 -valued Function-like Element of K10(K11((Args (S1,U1)),(( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1)))
K11((Args (S1,U1)),(( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1)) is Relation-like set
K10(K11((Args (S1,U1)),(( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1))) is set
dom ((S,S1,U1,(S,U1,U2,F)) * (Den (S1,U1))) is functional Element of K10((Args (S1,U1)))
the Arity of S . S1 is Relation-like K170() -defined Function-like V42() countable FinSequence-like FinSubsequence-like Element of the carrier of S *
(Den (S1,U1)) . s is Element of Result (S1,U1)
(S,U1,U2,F,(the_result_sort_of S1)) is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . (the_result_sort_of S1) -defined the Sorts of U2 . (the_result_sort_of S1) -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . (the_result_sort_of S1), the Sorts of U2 . (the_result_sort_of S1)) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . (the_result_sort_of S1)),( the Sorts of U2 . (the_result_sort_of S1))))
(S,( the Arity of S * ((S,U1,(S,U1,U2,F)) #)),( the ResultSort of S * (S,U1,(S,U1,U2,F))),(S,U1,(S,U1,U2,F)),S1) is Relation-like ( the Arity of S * ((S,U1,(S,U1,U2,F)) #)) . S1 -defined ( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1 -valued Function-like V29(( the Arity of S * ((S,U1,(S,U1,U2,F)) #)) . S1,( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1) Element of K10(K11((( the Arity of S * ((S,U1,(S,U1,U2,F)) #)) . S1),(( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1)))
K11((( the Arity of S * ((S,U1,(S,U1,U2,F)) #)) . S1),(( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1)) is Relation-like set
K10(K11((( the Arity of S * ((S,U1,(S,U1,U2,F)) #)) . S1),(( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1))) is set
(S,S1,U1,(S,U1,U2,F)) is Relation-like ( the Arity of S * ((S,U1,(S,U1,U2,F)) #)) . S1 -defined ( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1 -valued Function-like V29(( the Arity of S * ((S,U1,(S,U1,U2,F)) #)) . S1,( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1) Element of K10(K11((( the Arity of S * ((S,U1,(S,U1,U2,F)) #)) . S1),(( the ResultSort of S * (S,U1,(S,U1,U2,F))) . S1)))
((S,S1,U1,(S,U1,U2,F)) * (Den (S1,U1))) . s is set
x is Element of the Sorts of U1 . (the_result_sort_of S1)
(S,S1,U1,(S,U1,U2,F)) . x is set
(S,U1,(S,U1,U2,F),(the_result_sort_of S1),x) is Element of K10(( the Sorts of U1 . (the_result_sort_of S1)))
K10(( the Sorts of U1 . (the_result_sort_of S1))) is set
(S,U1,(S,U1,U2,F),(the_result_sort_of S1)) is Relation-like the Sorts of U1 . (the_result_sort_of S1) -defined the Sorts of U1 . (the_result_sort_of S1) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . (the_result_sort_of S1)),( the Sorts of U1 . (the_result_sort_of S1))))
K11(( the Sorts of U1 . (the_result_sort_of S1)),( the Sorts of U1 . (the_result_sort_of S1))) is Relation-like set
K10(K11(( the Sorts of U1 . (the_result_sort_of S1)),( the Sorts of U1 . (the_result_sort_of S1)))) is set
Class ((S,U1,(S,U1,U2,F),(the_result_sort_of S1)),x) is Element of K10(( the Sorts of U1 . (the_result_sort_of S1)))
(S,U1,U2,F,(the_result_sort_of S1)) is Relation-like the Sorts of U1 . (the_result_sort_of S1) -defined the Sorts of U1 . (the_result_sort_of S1) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . (the_result_sort_of S1)),( the Sorts of U1 . (the_result_sort_of S1))))
Class ((S,U1,U2,F,(the_result_sort_of S1)),x) is Element of K10(( the Sorts of U1 . (the_result_sort_of S1)))
F . (the_result_sort_of S1) is Relation-like the Sorts of U1 . (the_result_sort_of S1) -defined the Sorts of U2 . (the_result_sort_of S1) -valued Function-like V29( the Sorts of U1 . (the_result_sort_of S1), the Sorts of U2 . (the_result_sort_of S1)) Element of K10(K11(( the Sorts of U1 . (the_result_sort_of S1)),( the Sorts of U2 . (the_result_sort_of S1))))
K11(( the Sorts of U1 . (the_result_sort_of S1)),( the Sorts of U2 . (the_result_sort_of S1))) is Relation-like set
K10(K11(( the Sorts of U1 . (the_result_sort_of S1)),( the Sorts of U2 . (the_result_sort_of S1)))) is set
(F . (the_result_sort_of S1)) . ((Den (S1,U1)) . s) is set
(Den (S1,U2)) . (F # s) is Element of Result (S1,U2)
dom ((S,U1,U2,F) # S2) is set
dom (F # s) is set
S1 is set
(S,U1,U2,F) . S1 is Relation-like Function-like set
i is Element of the carrier of S
(S,U1,U2,F,i) is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . i -defined the Sorts of U2 . i -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . i, the Sorts of U2 . i) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . i),( the Sorts of U2 . i)))
the Sorts of (S,U1,(S,U1,U2,F)) . i is non empty set
the Sorts of U2 . i is non empty set
K11(( the Sorts of (S,U1,(S,U1,U2,F)) . i),( the Sorts of U2 . i)) is Relation-like set
K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . i),( the Sorts of U2 . i))) is set
dom ((S,U1,U2,F) . S1) is set
f is set
s is set
((S,U1,U2,F) . S1) . f is set
((S,U1,U2,F) . S1) . s is set
(S,U1,(S,U1,U2,F)) . i is non empty set
the Sorts of U1 . i is non empty set
(S,U1,(S,U1,U2,F),i) is Relation-like the Sorts of U1 . i -defined the Sorts of U1 . i -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . i),( the Sorts of U1 . i)))
K11(( the Sorts of U1 . i),( the Sorts of U1 . i)) is Relation-like set
K10(K11(( the Sorts of U1 . i),( the Sorts of U1 . i))) is set
Class (S,U1,(S,U1,U2,F),i) is a_partition of the Sorts of U1 . i
x is set
Class ((S,U1,(S,U1,U2,F),i),x) is Element of K10(( the Sorts of U1 . i))
K10(( the Sorts of U1 . i)) is set
a is set
Class ((S,U1,(S,U1,U2,F),i),a) is Element of K10(( the Sorts of U1 . i))
(S,U1,U2,F,i) is Relation-like the Sorts of U1 . i -defined the Sorts of U1 . i -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . i),( the Sorts of U1 . i)))
F . i is Relation-like the Sorts of U1 . i -defined the Sorts of U2 . i -valued Function-like V29( the Sorts of U1 . i, the Sorts of U2 . i) Element of K10(K11(( the Sorts of U1 . i),( the Sorts of U2 . i)))
K11(( the Sorts of U1 . i),( the Sorts of U2 . i)) is Relation-like set
K10(K11(( the Sorts of U1 . i),( the Sorts of U2 . i))) is set
a is Element of the Sorts of U1 . i
(F . i) . a is Element of the Sorts of U2 . i
a1 is Element of the Sorts of U1 . i
(F . i) . a1 is Element of the Sorts of U2 . i
[a1,a] is set
{a1,a} is set
{a1} is set
{{a1,a},{a1}} is set
S is non empty non void V68() ManySortedSign
the carrier of S is non empty set
U1 is non-empty MSAlgebra over S
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 is non-empty MSAlgebra over S
the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
F is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of U1, the Sorts of U2
(S,U1,U2,F) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
(S,U1,(S,U1,U2,F)) is strict non-empty MSAlgebra over S
(S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1,(S,U1,U2,F)) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((S,U1,(S,U1,U2,F)) #), the ResultSort of S * (S,U1,(S,U1,U2,F))
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
(S,U1,(S,U1,U2,F)) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U1,(S,U1,U2,F)) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
the ResultSort of S * (S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1,(S,U1,U2,F)),(S,U1,(S,U1,U2,F)) #) is strict MSAlgebra over S
(S,U1,U2,F) is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (S,U1,(S,U1,U2,F)), the Sorts of U2
the Sorts of (S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
i is set
(S,U1,U2,F) . i is Relation-like Function-like set
rng ((S,U1,U2,F) . i) is set
the Sorts of U2 . i is set
s is Element of the carrier of S
the Sorts of U2 . s is non empty set
F . s is Relation-like the Sorts of U1 . s -defined the Sorts of U2 . s -valued Function-like V29( the Sorts of U1 . s, the Sorts of U2 . s) Element of K10(K11(( the Sorts of U1 . s),( the Sorts of U2 . s)))
the Sorts of U1 . s is non empty set
K11(( the Sorts of U1 . s),( the Sorts of U2 . s)) is Relation-like set
K10(K11(( the Sorts of U1 . s),( the Sorts of U2 . s))) is set
rng (F . s) is Element of K10(( the Sorts of U2 . s))
K10(( the Sorts of U2 . s)) is set
(S,U1,U2,F,s) is Relation-like the Sorts of (S,U1,(S,U1,U2,F)) . s -defined the Sorts of U2 . s -valued Function-like V29( the Sorts of (S,U1,(S,U1,U2,F)) . s, the Sorts of U2 . s) Element of K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . s),( the Sorts of U2 . s)))
the Sorts of (S,U1,(S,U1,U2,F)) . s is non empty set
K11(( the Sorts of (S,U1,(S,U1,U2,F)) . s),( the Sorts of U2 . s)) is Relation-like set
K10(K11(( the Sorts of (S,U1,(S,U1,U2,F)) . s),( the Sorts of U2 . s))) is set
x is set
dom (F . s) is Element of K10(( the Sorts of U1 . s))
K10(( the Sorts of U1 . s)) is set
a is set
(F . s) . a is set
(S,U1,U2,F,s) is Relation-like the Sorts of U1 . s -defined the Sorts of U1 . s -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . s),( the Sorts of U1 . s)))
K11(( the Sorts of U1 . s),( the Sorts of U1 . s)) is Relation-like set
K10(K11(( the Sorts of U1 . s),( the Sorts of U1 . s))) is set
(S,U1,(S,U1,U2,F),s) is Relation-like the Sorts of U1 . s -defined the Sorts of U1 . s -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U1 . s),( the Sorts of U1 . s)))
Class (S,U1,(S,U1,U2,F),s) is a_partition of the Sorts of U1 . s
dom ((S,U1,U2,F) . i) is set
a is Element of the Sorts of U1 . s
Class ((S,U1,U2,F,s),a) is Element of K10(( the Sorts of U1 . s))
((S,U1,U2,F) . i) . (Class ((S,U1,U2,F,s),a)) is set
S is non empty non void V68() ManySortedSign
the carrier of S is non empty set
U1 is non-empty MSAlgebra over S
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U2 is non-empty MSAlgebra over S
the Sorts of U2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
F is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of U1, the Sorts of U2
(S,U1,U2,F) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,U1) (S,U1) ( the carrier of S, the Sorts of U1, the Sorts of U1)
(S,U1,(S,U1,U2,F)) is strict non-empty MSAlgebra over S
(S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1,(S,U1,U2,F)) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((S,U1,(S,U1,U2,F)) #), the ResultSort of S * (S,U1,(S,U1,U2,F))
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding Relation-yielding Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is set
(S,U1,(S,U1,U2,F)) # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the Arity of S * ((S,U1,(S,U1,U2,F)) #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is set
the ResultSort of S * (S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1,(S,U1,U2,F)),(S,U1,(S,U1,U2,F)) #) is strict MSAlgebra over S
(S,U1,U2,F) is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (S,U1,(S,U1,U2,F)), the Sorts of U2
the Sorts of (S,U1,(S,U1,U2,F)) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set