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