:: MSUALG_4 semantic presentation

K170() is V42() countable denumerable Element of K10(K166())
K166() is set
K10(K166()) is set

K10(K137()) is set
K10(K170()) is set
{} is set

1 is non empty set
2 is non empty set
3 is non empty set
S is set

S --> the Relation-like set is Relation-like S -defined {} -valued Function-like constant total V29(S,{}) Element of K10(K11(S,{}))
{} is set
K11(S,{}) is Relation-like set
K10(K11(S,{})) is set

dom F is Element of K10(S)
K10(S) is set
mc is set
F . mc is set
S is 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

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

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

S is non empty 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

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

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

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,()) is Relation-like the Sorts of U1 . () -defined the Sorts of U1 . () -valued Element of K10(K11(( the Sorts of U1 . ()),( the Sorts of U1 . ())))
the Sorts of U1 . () is non empty set
K11(( the Sorts of U1 . ()),( the Sorts of U1 . ())) is Relation-like set
K10(K11(( the Sorts of U1 . ()),( the Sorts of U1 . ()))) 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 () is countable Element of K10(K170())
f is set
S1 . f is set
S2 . f is set
s is V41() set
() . s is set
rng () is Element of K10( the carrier of S)
K10( the carrier of S) is set
qh . (() . s) is set
the Sorts of U1 . (() . s) is set
id ( the Sorts of U1 . (() . s)) is Relation-like the Sorts of U1 . (() . s) -defined the Sorts of U1 . (() . s) -valued V12() V14() V15() V19() Function-like one-to-one total Element of K10(K11(( the Sorts of U1 . (() . s)),( the Sorts of U1 . (() . s))))
K11(( the Sorts of U1 . (() . s)),( the Sorts of U1 . (() . s))) is Relation-like set
K10(K11(( the Sorts of U1 . (() . s)),( the Sorts of U1 . (() . s)))) is set
() /. s 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 . ()) is non empty Relation-like the Sorts of U1 . () -defined the Sorts of U1 . () -valued V12() V14() V15() V19() Function-like one-to-one total Element of K10(K11(( the Sorts of U1 . ()),( the Sorts of U1 . ())))
( 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)

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

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

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

mc is Element of the carrier' of S

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

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

S is non empty 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())

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

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 Relation-like non-empty K170() -defined dom () -defined Function-like total set
dom () is countable Element of K10(K170())
product (() * (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
() /. 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
mc . S1 is set
Class ((S,U2,F,(() /. S1)),(mc . S1)) is Element of K10(( the Sorts of U2 . (() /. S1)))
K10(( the Sorts of U2 . (() /. S1))) is set
S2 is V41() set
() /. S2 is Element of the carrier of S
the Sorts of U2 . (() /. S2) is non empty set
(S,U2,F,(() /. S2)) is Relation-like the Sorts of U2 . (() /. S2) -defined the Sorts of U2 . (() /. S2) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . (() /. S2)),( the Sorts of U2 . (() /. S2))))
K11(( the Sorts of U2 . (() /. S2)),( the Sorts of U2 . (() /. S2))) is Relation-like set
K10(K11(( the Sorts of U2 . (() /. S2)),( the Sorts of U2 . (() /. S2)))) is set
mc . S2 is set
Class ((S,U2,F,(() /. S2)),(mc . S2)) is Element of K10(( the Sorts of U2 . (() /. S2)))
K10(( the Sorts of U2 . (() /. S2))) is set

dom Sq is set
dom (() * (S,U2,F)) is countable Element of K10(K170())
S1 is set
Sq . S1 is set
(() * (S,U2,F)) . S1 is set
() . S1 is set
rng () is Element of K10( the carrier of S)
K10( the carrier of S) is set

dom (() * the Sorts of U2) is countable Element of K10(K170())
(() * the Sorts of U2) . S1 is set
the Sorts of U2 . (() . 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
() /. S2 is Element of the carrier of S
the Sorts of U2 . (() /. S2) is non empty set
(S,U2,F,(() /. S2)) is Relation-like the Sorts of U2 . (() /. S2) -defined the Sorts of U2 . (() /. S2) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . (() /. S2)),( the Sorts of U2 . (() /. S2))))
K11(( the Sorts of U2 . (() /. S2)),( the Sorts of U2 . (() /. S2))) is Relation-like set
K10(K11(( the Sorts of U2 . (() /. S2)),( the Sorts of U2 . (() /. S2)))) is set
mc . S2 is set
Class ((S,U2,F,(() /. S2)),(mc . S2)) is Element of K10(( the Sorts of U2 . (() /. S2)))
K10(( the Sorts of U2 . (() /. S2))) is set
() . 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) . (() . S1) is set
S1 is Relation-like K170() -defined Function-like () * (S,U2,F) -compatible Element of product (() * (S,U2,F))
S2 is V41() set
S1 . S2 is set
() /. S2 is Element of the carrier of S
the Sorts of U2 . (() /. S2) is non empty set
(S,U2,F,(() /. S2)) is Relation-like the Sorts of U2 . (() /. S2) -defined the Sorts of U2 . (() /. S2) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . (() /. S2)),( the Sorts of U2 . (() /. S2))))
K11(( the Sorts of U2 . (() /. S2)),( the Sorts of U2 . (() /. S2))) is Relation-like set
K10(K11(( the Sorts of U2 . (() /. S2)),( the Sorts of U2 . (() /. S2)))) is set
mc . S2 is set
Class ((S,U2,F,(() /. S2)),(mc . S2)) is Element of K10(( the Sorts of U2 . (() /. S2)))
K10(( the Sorts of U2 . (() /. S2))) is set
qa is Relation-like K170() -defined Function-like () * (S,U2,F) -compatible Element of product (() * (S,U2,F))
qh is Relation-like K170() -defined Function-like () * (S,U2,F) -compatible Element of product (() * (S,U2,F))
Sq is set
qa . Sq is set
qh . Sq is set
S1 is V41() set
qa . S1 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
mc . S1 is set
Class ((S,U2,F,(() /. S1)),(mc . S1)) is Element of K10(( the Sorts of U2 . (() /. S1)))
K10(( the Sorts of U2 . (() /. 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 . () is non empty set
K10(( the Sorts of U2 . ())) is set

dom qh is set
(S,U2,F) . () is non empty set
Sq is set
qh . Sq is set
S1 is Element of the Sorts of U2 . ()
qh . S1 is set
(S,U2,F,(),S1) is Element of K10(( the Sorts of U2 . ()))
(S,U2,F,()) is Relation-like the Sorts of U2 . () -defined the Sorts of U2 . () -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . ()),( the Sorts of U2 . ())))
K11(( the Sorts of U2 . ()),( the Sorts of U2 . ())) is Relation-like set
K10(K11(( the Sorts of U2 . ()),( the Sorts of U2 . ()))) is set
Class ((S,U2,F,()),S1) is Element of K10(( the Sorts of U2 . ()))
Class (S,U2,F,()) is a_partition of the Sorts of U2 . ()
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 . ()
Sq . S1 is set
(S,U2,F,(),S1) is Element of K10(( the Sorts of U2 . ()))
(S,U2,F,()) is Relation-like the Sorts of U2 . () -defined the Sorts of U2 . () -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . ()),( the Sorts of U2 . ())))
K11(( the Sorts of U2 . ()),( the Sorts of U2 . ())) is Relation-like set
K10(K11(( the Sorts of U2 . ()),( the Sorts of U2 . ()))) is set
Class ((S,U2,F,()),S1) is Element of K10(( the Sorts of U2 . ()))
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 . ()
Sq . i is set
(S,U2,F,(),i) is Element of K10(( the Sorts of U2 . ()))
K10(( the Sorts of U2 . ())) is set
(S,U2,F,()) is Relation-like the Sorts of U2 . () -defined the Sorts of U2 . () -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . ()),( the Sorts of U2 . ())))
K11(( the Sorts of U2 . ()),( the Sorts of U2 . ())) is Relation-like set
K10(K11(( the Sorts of U2 . ()),( the Sorts of U2 . ()))) is set
Class ((S,U2,F,()),i) is Element of K10(( the Sorts of U2 . ()))
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

() * (S,U2,F) is Relation-like non-empty K170() -defined dom () -defined Function-like total set
dom () is countable Element of K10(K170())
product (() * (S,U2,F)) is non empty functional with_common_domain product-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 Sorts of U2 #) . ( the Arity of S . U1) is non empty set
( the Sorts of U2 #) . () is non empty set
((S,U2,F) #) . () 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 () * (S,U2,F) -compatible Element of product (() * (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 () * (S,U2,F) -compatible Element of product (() * (S,U2,F))

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 Sorts of U2 #) . ( the Arity of S . U1) is non empty set
( the Sorts of U2 #) . () 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 () * (S,U2,F) -compatible Element of product (() * (S,U2,F))
() * (S,U2,F) is Relation-like non-empty K170() -defined dom () -defined Function-like total set
dom () is countable Element of K10(K170())
product (() * (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

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

Sq is 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

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

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

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

Sq is 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

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

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

() * (S,U2,F) is Relation-like non-empty K170() -defined dom () -defined Function-like total set
dom () is countable Element of K10(K170())
product (() * (S,U2,F)) is non empty functional with_common_domain product-like set
dom (() * (S,U2,F)) is countable Element of K10(K170())

dom qh is set
Sq is V41() set
qh . Sq is set
() /. Sq is Element of the carrier of S
the Sorts of U2 . (() /. Sq) is non empty set
(S,U2,F,(() /. Sq)) is Relation-like the Sorts of U2 . (() /. Sq) -defined the Sorts of U2 . (() /. Sq) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . (() /. Sq)),( the Sorts of U2 . (() /. Sq))))
K11(( the Sorts of U2 . (() /. Sq)),( the Sorts of U2 . (() /. Sq))) is Relation-like set
K10(K11(( the Sorts of U2 . (() /. Sq)),( the Sorts of U2 . (() /. Sq)))) is set
Class (S,U2,F,(() /. Sq)) is a_partition of the Sorts of U2 . (() /. Sq)
() . Sq is set
(() * (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
() /. 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

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 () is Element of K10( the carrier of S)

dom (() * the Sorts of U2) is countable Element of K10(K170())
S1 is set
Sq . S1 is set
(() * the Sorts of U2) . S1 is set
qh . S1 is set
(() * (S,U2,F)) . S1 is set
S2 is V41() set
() /. S2 is Element of the carrier of S
() . 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 Sorts of U2) is non empty functional with_common_domain product-like set
S2 is set
i is V41() set
() /. 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 () * (S,U2,F) -compatible Element of product (() * (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

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 () * (S,U2,F) -compatible Element of product (() * (S,U2,F))
() * (S,U2,F) is Relation-like non-empty K170() -defined dom () -defined Function-like total set
dom () is countable Element of K10(K170())
product (() * (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) . () 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 . () 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 () * (S,U2,F) -compatible Element of product (() * (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 . ()
(S,U1,U2,F) . x is set
(S,U2,F,(),x) is Element of K10(( the Sorts of U2 . ()))
K10(( the Sorts of U2 . ())) is set
(S,U2,F,()) is Relation-like the Sorts of U2 . () -defined the Sorts of U2 . () -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . ()),( the Sorts of U2 . ())))
K11(( the Sorts of U2 . ()),( the Sorts of U2 . ())) is Relation-like set
K10(K11(( the Sorts of U2 . ()),( the Sorts of U2 . ()))) is set
Class ((S,U2,F,()),x) is Element of K10(( the Sorts of U2 . ()))
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
() /. a is Element of the carrier of S
(S,U2,F,(() /. a)) is Relation-like the Sorts of U2 . (() /. a) -defined the Sorts of U2 . (() /. a) -valued V12() V14() V19() total Element of K10(K11(( the Sorts of U2 . (() /. a)),( the Sorts of U2 . (() /. a))))
the Sorts of U2 . (() /. a) is non empty set
K11(( the Sorts of U2 . (() /. a)),( the Sorts of U2 . (() /. a))) is Relation-like set
K10(K11(( the Sorts of U2 . (() /. a)),( the Sorts of U2 . (() /. a)))) is set
(S,U1,U2,F,S2) . a is set
Class ((S,U2,F,(() /. a)),(S2 . a)) is Element of K10(( the Sorts of U2 . (() /. a)))
K10(( the Sorts of U2 . (() /. a))) is set
(S,U1,U2,F,f) . a is set
Class ((S,U2,F,(() /. a)),(f . a)) is Element of K10(( the Sorts of U2 . (() /. a)))
dom the Sorts of U2 is non empty Element of K10( the carrier of S)
K10( the carrier of S) is set
rng () is Element of K10( the carrier of S)

dom (() * the Sorts of U2) is countable Element of K10(K170())
(() * the Sorts of U2) . a is set
() . a is set
the Sorts of U2 . (() . a) is set
s is Element of the Sorts of U2 . ()
[s,x] is set
{s,x} is set
{s} is set
{{s,x},{s}} is set
(S,U2,F,(),s) is Element of K10(( the Sorts of U2 . ()))
Class ((S,U2,F,()),s) is Element of K10(( the Sorts of U2 . ()))

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 () * (S,U2,F) -compatible Element of product (() * (S,U2,F))

() * (S,U2,F) is Relation-like non-empty K170() -defined dom () -defined Function-like total set
dom () is countable Element of K10(K170())
product (() * (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

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