:: MSUALG_4 semantic presentation

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