:: MSUHOM_1 semantic presentation

REAL is set

NAT is non empty V23() V24() V25() Element of K19(REAL)

K19(REAL) is set

NAT is non empty V23() V24() V25() set

K19(NAT) is set

K19(NAT) is set

K219() is set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V22() V23() V24() V25() V27() V28() V29() V30() FinSequence-like FinSubsequence-like FinSequence-membered V119() V120() ext-real set

1 is non empty V23() V24() V25() V29() V119() V120() ext-real Element of NAT

2 is non empty V23() V24() V25() V29() V119() V120() ext-real Element of NAT

3 is non empty V23() V24() V25() V29() V119() V120() ext-real Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V22() V23() V24() V25() V27() V28() V29() V30() FinSequence-like FinSubsequence-like FinSequence-membered V119() V120() ext-real Element of NAT

{0} is functional non empty set

{0} * is functional non empty FinSequence-membered FinSequenceSet of {0}

*--> 0 is Relation-like NAT -defined {0} * -valued Function-like non empty total V18( NAT ,{0} * ) Function-yielding V22() Element of K19(K20(NAT,({0} *)))

K20(NAT,({0} *)) is Relation-like set

K19(K20(NAT,({0} *))) is set

U1 is Relation-like Function-like set

rng U1 is set

U2 is Relation-like Function-like set

U1 * U2 is Relation-like Function-like set

U3 is set

U2 | U3 is Relation-like Function-like set

U1 * (U2 | U3) is Relation-like Function-like set

U3 |` U1 is Relation-like Function-like set

(U3 |` U1) * U2 is Relation-like Function-like set

U1 is set

K19(U1) is set

U1 * is functional non empty FinSequence-membered FinSequenceSet of U1

U2 is Element of K19(U1)

U2 * is functional non empty FinSequence-membered FinSequenceSet of U2

U3 is set

h1 is Relation-like NAT -defined U2 -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of U2

rng h1 is Element of K19(U2)

K19(U2) is set

U1 is Relation-like Function-like set

U2 is set

U1 | U2 is Relation-like Function-like set

U1 is set

K19(U1) is set

U2 is Element of K19(U1)

U2 * is functional non empty FinSequence-membered FinSequenceSet of U2

U3 is Relation-like U1 -defined Function-like total set

U3 | U2 is Relation-like U1 -defined U2 -defined U1 -defined Function-like total set

(U3 | U2) # is Relation-like U2 * -defined Function-like non empty total set

U3 # is Relation-like U1 * -defined Function-like non empty total set

U1 * is functional non empty FinSequence-membered FinSequenceSet of U1

(U3 #) | (U2 *) is Relation-like U2 * -defined U1 * -defined Function-like set

dom (U3 #) is functional non empty FinSequence-membered Element of K19((U1 *))

K19((U1 *)) is set

dom ((U3 #) | (U2 *)) is functional FinSequence-membered Element of K19((U2 *))

K19((U2 *)) is set

h2 is Relation-like NAT -defined U2 -valued Function-like V30() FinSequence-like FinSubsequence-like Element of U2 *

((U3 #) | (U2 *)) . h2 is set

h2 * (U3 | U2) is Relation-like NAT -defined Function-like set

product (h2 * (U3 | U2)) is set

rng h2 is Element of K19(U2)

K19(U2) is set

h1 is Relation-like U2 * -defined Function-like non empty total set

dom h1 is functional non empty FinSequence-membered Element of K19((U2 *))

h1 . h2 is set

dom (h2 * (U3 | U2)) is Element of K19(NAT)

h is set

(U3 #) . h2 is set

h2 * U3 is Relation-like NAT -defined Function-like set

product (h2 * U3) is set

dom (h2 * U3) is Element of K19(NAT)

a is Relation-like Function-like set

dom a is set

f is Relation-like Function-like set

dom f is set

g is set

f . g is set

(h2 * (U3 | U2)) . g is set

(h2 * U3) . g is set

a is Relation-like Function-like set

dom a is set

f is set

a . f is set

(h2 * U3) . f is set

(h2 * (U3 | U2)) . f is set

h1 is Relation-like U2 * -defined Function-like non empty total set

U3 is non empty V67() ManySortedSign

the carrier of U3 is non empty set

the carrier' of U3 is set

the carrier of U3 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U3

the Arity of U3 is Relation-like the carrier' of U3 -defined the carrier of U3 * -valued Function-like total V18( the carrier' of U3, the carrier of U3 * ) Function-yielding V22() Element of K19(K20( the carrier' of U3,( the carrier of U3 *)))

K20( the carrier' of U3,( the carrier of U3 *)) is Relation-like set

K19(K20( the carrier' of U3,( the carrier of U3 *))) is set

the Arity of U3 | the carrier' of U3 is Relation-like the carrier' of U3 -defined the carrier' of U3 -defined the carrier of U3 * -valued Function-like Function-yielding V22() Element of K19(K20( the carrier' of U3,( the carrier of U3 *)))

the ResultSort of U3 is Relation-like the carrier' of U3 -defined the carrier of U3 -valued Function-like total V18( the carrier' of U3, the carrier of U3) Element of K19(K20( the carrier' of U3, the carrier of U3))

K20( the carrier' of U3, the carrier of U3) is Relation-like set

K19(K20( the carrier' of U3, the carrier of U3)) is set

the ResultSort of U3 | the carrier' of U3 is Relation-like the carrier' of U3 -defined the carrier' of U3 -defined the carrier of U3 -valued Function-like Element of K19(K20( the carrier' of U3, the carrier of U3))

U1 is non empty V67() ManySortedSign

U2 is non empty V67() ManySortedSign

U3 is non empty V67() ManySortedSign

the carrier of U1 is non empty set

the carrier of U2 is non empty set

the carrier of U3 is non empty set

the carrier' of U1 is set

the carrier' of U3 is set

the carrier of U3 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U3

the Arity of U3 is Relation-like the carrier' of U3 -defined the carrier of U3 * -valued Function-like total V18( the carrier' of U3, the carrier of U3 * ) Function-yielding V22() Element of K19(K20( the carrier' of U3,( the carrier of U3 *)))

K20( the carrier' of U3,( the carrier of U3 *)) is Relation-like set

K19(K20( the carrier' of U3,( the carrier of U3 *))) is set

the Arity of U3 | the carrier' of U1 is Relation-like the carrier' of U1 -defined the carrier' of U3 -defined the carrier of U3 * -valued Function-like Function-yielding V22() Element of K19(K20( the carrier' of U3,( the carrier of U3 *)))

the Arity of U1 is Relation-like the carrier' of U1 -defined the carrier of U1 * -valued Function-like total V18( the carrier' of U1, the carrier of U1 * ) Function-yielding V22() Element of K19(K20( the carrier' of U1,( the carrier of U1 *)))

the carrier of U1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U1

K20( the carrier' of U1,( the carrier of U1 *)) is Relation-like set

K19(K20( the carrier' of U1,( the carrier of U1 *))) is set

the ResultSort of U3 is Relation-like the carrier' of U3 -defined the carrier of U3 -valued Function-like total V18( the carrier' of U3, the carrier of U3) Element of K19(K20( the carrier' of U3, the carrier of U3))

K20( the carrier' of U3, the carrier of U3) is Relation-like set

K19(K20( the carrier' of U3, the carrier of U3)) is set

the ResultSort of U3 | the carrier' of U1 is Relation-like the carrier' of U1 -defined the carrier' of U3 -defined the carrier of U3 -valued Function-like Element of K19(K20( the carrier' of U3, the carrier of U3))

the ResultSort of U1 is Relation-like the carrier' of U1 -defined the carrier of U1 -valued Function-like total V18( the carrier' of U1, the carrier of U1) Element of K19(K20( the carrier' of U1, the carrier of U1))

K20( the carrier' of U1, the carrier of U1) is Relation-like set

K19(K20( the carrier' of U1, the carrier of U1)) is set

the carrier' of U2 is set

the carrier' of U2 /\ the carrier' of U1 is set

the Arity of U3 | ( the carrier' of U2 /\ the carrier' of U1) is Relation-like the carrier' of U3 -defined the carrier' of U2 /\ the carrier' of U1 -defined the carrier' of U3 -defined the carrier of U3 * -valued Function-like Function-yielding V22() Element of K19(K20( the carrier' of U3,( the carrier of U3 *)))

the Arity of U3 | the carrier' of U2 is Relation-like the carrier' of U3 -defined the carrier' of U2 -defined the carrier' of U3 -defined the carrier of U3 * -valued Function-like Function-yielding V22() Element of K19(K20( the carrier' of U3,( the carrier of U3 *)))

( the Arity of U3 | the carrier' of U2) | the carrier' of U1 is Relation-like the carrier' of U1 -defined the carrier' of U3 -defined the carrier of U3 * -valued Function-like Function-yielding V22() Element of K19(K20( the carrier' of U3,( the carrier of U3 *)))

the carrier of U2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U2

the Arity of U2 is Relation-like the carrier' of U2 -defined the carrier of U2 * -valued Function-like total V18( the carrier' of U2, the carrier of U2 * ) Function-yielding V22() Element of K19(K20( the carrier' of U2,( the carrier of U2 *)))

K20( the carrier' of U2,( the carrier of U2 *)) is Relation-like set

K19(K20( the carrier' of U2,( the carrier of U2 *))) is set

the Arity of U2 | the carrier' of U1 is Relation-like the carrier' of U1 -defined the carrier' of U2 -defined the carrier of U2 * -valued Function-like Function-yielding V22() Element of K19(K20( the carrier' of U2,( the carrier of U2 *)))

the ResultSort of U3 | ( the carrier' of U2 /\ the carrier' of U1) is Relation-like the carrier' of U3 -defined the carrier' of U2 /\ the carrier' of U1 -defined the carrier' of U3 -defined the carrier of U3 -valued Function-like Element of K19(K20( the carrier' of U3, the carrier of U3))

the ResultSort of U3 | the carrier' of U2 is Relation-like the carrier' of U3 -defined the carrier' of U2 -defined the carrier' of U3 -defined the carrier of U3 -valued Function-like Element of K19(K20( the carrier' of U3, the carrier of U3))

( the ResultSort of U3 | the carrier' of U2) | the carrier' of U1 is Relation-like the carrier' of U1 -defined the carrier' of U3 -defined the carrier of U3 -valued Function-like Element of K19(K20( the carrier' of U3, the carrier of U3))

the ResultSort of U2 is Relation-like the carrier' of U2 -defined the carrier of U2 -valued Function-like total V18( the carrier' of U2, the carrier of U2) Element of K19(K20( the carrier' of U2, the carrier of U2))

K20( the carrier' of U2, the carrier of U2) is Relation-like set

K19(K20( the carrier' of U2, the carrier of U2)) is set

the ResultSort of U2 | the carrier' of U1 is Relation-like the carrier' of U1 -defined the carrier' of U2 -defined the carrier of U2 -valued Function-like Element of K19(K20( the carrier' of U2, the carrier of U2))

U1 is non empty V67() strict ManySortedSign

U2 is non empty V67() strict ManySortedSign

the carrier' of U2 is set

the carrier' of U1 is set

the ResultSort of U2 is Relation-like the carrier' of U2 -defined the carrier of U2 -valued Function-like total V18( the carrier' of U2, the carrier of U2) Element of K19(K20( the carrier' of U2, the carrier of U2))

the carrier of U2 is non empty set

K20( the carrier' of U2, the carrier of U2) is Relation-like set

K19(K20( the carrier' of U2, the carrier of U2)) is set

dom the ResultSort of U2 is Element of K19( the carrier' of U2)

K19( the carrier' of U2) is set

the ResultSort of U2 | the carrier' of U1 is Relation-like the carrier' of U2 -defined the carrier' of U1 -defined the carrier' of U2 -defined the carrier of U2 -valued Function-like Element of K19(K20( the carrier' of U2, the carrier of U2))

the ResultSort of U1 is Relation-like the carrier' of U1 -defined the carrier of U1 -valued Function-like total V18( the carrier' of U1, the carrier of U1) Element of K19(K20( the carrier' of U1, the carrier of U1))

the carrier of U1 is non empty set

K20( the carrier' of U1, the carrier of U1) is Relation-like set

K19(K20( the carrier' of U1, the carrier of U1)) is set

the Arity of U2 is Relation-like the carrier' of U2 -defined the carrier of U2 * -valued Function-like total V18( the carrier' of U2, the carrier of U2 * ) Function-yielding V22() Element of K19(K20( the carrier' of U2,( the carrier of U2 *)))

the carrier of U2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U2

K20( the carrier' of U2,( the carrier of U2 *)) is Relation-like set

K19(K20( the carrier' of U2,( the carrier of U2 *))) is set

dom the Arity of U2 is Element of K19( the carrier' of U2)

the Arity of U2 | the carrier' of U1 is Relation-like the carrier' of U2 -defined the carrier' of U1 -defined the carrier' of U2 -defined the carrier of U2 * -valued Function-like Function-yielding V22() Element of K19(K20( the carrier' of U2,( the carrier of U2 *)))

the Arity of U1 is Relation-like the carrier' of U1 -defined the carrier of U1 * -valued Function-like total V18( the carrier' of U1, the carrier of U1 * ) Function-yielding V22() Element of K19(K20( the carrier' of U1,( the carrier of U1 *)))

the carrier of U1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U1

K20( the carrier' of U1,( the carrier of U1 *)) is Relation-like set

K19(K20( the carrier' of U1,( the carrier of U1 *))) is set

U1 is V23() V24() V25() V29() V119() V120() ext-real set

U2 is non empty set

U3 is Relation-like Function-like set

h1 is Element of U2

h1 .--> U3 is Relation-like U2 -defined {h1} -defined Function-like one-to-one Function-yielding V22() set

{h1} is non empty set

{h1} --> U3 is Relation-like {h1} -defined {U3} -valued Function-like constant non empty total V18({h1},{U3}) Function-yielding V22() Element of K19(K20({h1},{U3}))

{U3} is functional non empty set

K20({h1},{U3}) is Relation-like set

K19(K20({h1},{U3})) is set

U1 |-> h1 is Relation-like NAT -defined U2 -valued Function-like V30() FinSequence-like FinSubsequence-like Element of U1 -tuples_on U2

U1 -tuples_on U2 is FinSequenceSet of U2

U2 * is functional non empty FinSequence-membered FinSequenceSet of U2

{ b

Seg U1 is V30() V37(U1) Element of K19(NAT)

(Seg U1) --> h1 is Relation-like Seg U1 -defined U2 -valued {h1} -valued Function-like constant total V18( Seg U1,{h1}) Element of K19(K20((Seg U1),{h1}))

K20((Seg U1),{h1}) is Relation-like set

K19(K20((Seg U1),{h1})) is set

h2 is V23() V24() V25() V29() V119() V120() ext-real set

(U1 |-> h1) /. h2 is Element of U2

(h1 .--> U3) . ((U1 |-> h1) /. h2) is Relation-like Function-like set

dom (U1 |-> h1) is Element of K19(NAT)

(U1 |-> h1) . h2 is set

U1 is set

K19(U1) is set

U2 is Element of K19(U1)

U3 is Relation-like U1 -defined Function-like total set

h1 is Relation-like U1 -defined Function-like total set

U3 | U2 is Relation-like U1 -defined U2 -defined U1 -defined Function-like total set

h1 | U2 is Relation-like U1 -defined U2 -defined U1 -defined Function-like total set

h2 is Relation-like U1 -defined Function-like total Function-yielding V22() ManySortedFunction of U3,h1

h2 | U2 is Relation-like U1 -defined U2 -defined U1 -defined Function-like total Function-yielding V22() set

h is Relation-like U2 -defined Function-like total set

a is Relation-like U2 -defined Function-like total set

dom h is Element of K19(U2)

K19(U2) is set

dom (h2 | U2) is Element of K19(U2)

dom a is Element of K19(U2)

g is set

h1 . g is set

a . g is set

f is Relation-like U2 -defined Function-like total Function-yielding V22() set

f . g is Relation-like Function-like set

h2 . g is Relation-like Function-like set

U3 . g is set

h . g is set

K20((h . g),(a . g)) is Relation-like set

K19(K20((h . g),(a . g))) is set

U2 is non empty non void V67() strict ManySortedSign

U1 is non empty non void V67() strict ManySortedSign

U3 is strict non-empty MSAlgebra over U2

the Sorts of U3 is Relation-like non-empty non empty-yielding the carrier of U2 -defined Function-like non empty total set

the carrier of U2 is non empty set

the carrier of U1 is non empty set

the Sorts of U3 | the carrier of U1 is Relation-like non-empty the carrier of U1 -defined the carrier of U2 -defined Function-like set

the Charact of U3 is Relation-like the carrier' of U2 -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Arity of U2 * ( the Sorts of U3 #), the ResultSort of U2 * the Sorts of U3

the carrier' of U2 is non empty set

the Arity of U2 is Relation-like the carrier' of U2 -defined the carrier of U2 * -valued Function-like non empty total V18( the carrier' of U2, the carrier of U2 * ) Function-yielding V22() Element of K19(K20( the carrier' of U2,( the carrier of U2 *)))

the carrier of U2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U2

K20( the carrier' of U2,( the carrier of U2 *)) is Relation-like set

K19(K20( the carrier' of U2,( the carrier of U2 *))) is set

the Sorts of U3 # is Relation-like the carrier of U2 * -defined Function-like non empty total set

the Arity of U2 * ( the Sorts of U3 #) is Relation-like the carrier' of U2 -defined Function-like non empty total set

the ResultSort of U2 is Relation-like the carrier' of U2 -defined the carrier of U2 -valued Function-like non empty total V18( the carrier' of U2, the carrier of U2) Element of K19(K20( the carrier' of U2, the carrier of U2))

K20( the carrier' of U2, the carrier of U2) is Relation-like set

K19(K20( the carrier' of U2, the carrier of U2)) is set

the ResultSort of U2 * the Sorts of U3 is Relation-like non-empty non empty-yielding the carrier' of U2 -defined Function-like non empty total set

the carrier' of U1 is non empty set

the Charact of U3 | the carrier' of U1 is Relation-like the carrier' of U1 -defined the carrier' of U2 -defined Function-like Function-yielding V22() set

the carrier of U1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U1

the Arity of U1 is Relation-like the carrier' of U1 -defined the carrier of U1 * -valued Function-like non empty total V18( the carrier' of U1, the carrier of U1 * ) Function-yielding V22() Element of K19(K20( the carrier' of U1,( the carrier of U1 *)))

K20( the carrier' of U1,( the carrier of U1 *)) is Relation-like set

K19(K20( the carrier' of U1,( the carrier of U1 *))) is set

rng the Arity of U1 is functional non empty FinSequence-membered Element of K19(( the carrier of U1 *))

K19(( the carrier of U1 *)) is set

the ResultSort of U1 is Relation-like the carrier' of U1 -defined the carrier of U1 -valued Function-like non empty total V18( the carrier' of U1, the carrier of U1) Element of K19(K20( the carrier' of U1, the carrier of U1))

K20( the carrier' of U1, the carrier of U1) is Relation-like set

K19(K20( the carrier' of U1, the carrier of U1)) is set

rng the ResultSort of U1 is non empty Element of K19( the carrier of U1)

K19( the carrier of U1) is set

a is Relation-like the carrier of U1 -defined Function-like non empty total set

the ResultSort of U1 * a is Relation-like the carrier' of U1 -defined Function-like non empty total set

the ResultSort of U1 * the Sorts of U3 is Relation-like non-empty the carrier' of U1 -defined Function-like set

the ResultSort of U2 | the carrier' of U1 is Relation-like the carrier' of U2 -defined the carrier' of U1 -defined the carrier' of U2 -defined the carrier of U2 -valued Function-like Element of K19(K20( the carrier' of U2, the carrier of U2))

( the ResultSort of U2 | the carrier' of U1) * the Sorts of U3 is Relation-like non-empty the carrier' of U2 -defined Function-like set

( the ResultSort of U2 * the Sorts of U3) | the carrier' of U1 is Relation-like non-empty the carrier' of U1 -defined the carrier' of U2 -defined Function-like set

a # is Relation-like the carrier of U1 * -defined Function-like non empty total set

the Arity of U1 * (a #) is Relation-like the carrier' of U1 -defined Function-like non empty total set

( the Sorts of U3 #) | ( the carrier of U1 *) is Relation-like the carrier of U1 * -defined the carrier of U2 * -defined Function-like set

the Arity of U1 * (( the Sorts of U3 #) | ( the carrier of U1 *)) is Relation-like the carrier' of U1 -defined Function-like set

the Arity of U1 * ( the Sorts of U3 #) is Relation-like the carrier' of U1 -defined Function-like set

the Arity of U2 | the carrier' of U1 is Relation-like the carrier' of U2 -defined the carrier' of U1 -defined the carrier' of U2 -defined the carrier of U2 * -valued Function-like Function-yielding V22() Element of K19(K20( the carrier' of U2,( the carrier of U2 *)))

( the Arity of U2 | the carrier' of U1) * ( the Sorts of U3 #) is Relation-like the carrier' of U2 -defined Function-like set

( the Arity of U2 * ( the Sorts of U3 #)) | the carrier' of U1 is Relation-like the carrier' of U1 -defined the carrier' of U2 -defined Function-like set

h is Relation-like the carrier' of U1 -defined Function-like non empty total set

f is Relation-like the carrier' of U1 -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Arity of U1 * (a #), the ResultSort of U1 * a

MSAlgebra(# a,f #) is strict MSAlgebra over U1

g is strict non-empty MSAlgebra over U1

the Sorts of g is Relation-like non-empty non empty-yielding the carrier of U1 -defined Function-like non empty total set

the Charact of g is Relation-like the carrier' of U1 -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Arity of U1 * ( the Sorts of g #), the ResultSort of U1 * the Sorts of g

the Sorts of g # is Relation-like the carrier of U1 * -defined Function-like non empty total set

the Arity of U1 * ( the Sorts of g #) is Relation-like the carrier' of U1 -defined Function-like non empty total set

the ResultSort of U1 * the Sorts of g is Relation-like non-empty non empty-yielding the carrier' of U1 -defined Function-like non empty total set

h1 is strict non-empty MSAlgebra over U1

the Sorts of h1 is Relation-like non-empty non empty-yielding the carrier of U1 -defined Function-like non empty total set

the Charact of h1 is Relation-like the carrier' of U1 -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Arity of U1 * ( the Sorts of h1 #), the ResultSort of U1 * the Sorts of h1

the Arity of U1 is Relation-like the carrier' of U1 -defined the carrier of U1 * -valued Function-like non empty total V18( the carrier' of U1, the carrier of U1 * ) Function-yielding V22() Element of K19(K20( the carrier' of U1,( the carrier of U1 *)))

the carrier of U1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U1

K20( the carrier' of U1,( the carrier of U1 *)) is Relation-like set

K19(K20( the carrier' of U1,( the carrier of U1 *))) is set

the Sorts of h1 # is Relation-like the carrier of U1 * -defined Function-like non empty total set

the Arity of U1 * ( the Sorts of h1 #) is Relation-like the carrier' of U1 -defined Function-like non empty total set

the ResultSort of U1 is Relation-like the carrier' of U1 -defined the carrier of U1 -valued Function-like non empty total V18( the carrier' of U1, the carrier of U1) Element of K19(K20( the carrier' of U1, the carrier of U1))

K20( the carrier' of U1, the carrier of U1) is Relation-like set

K19(K20( the carrier' of U1, the carrier of U1)) is set

the ResultSort of U1 * the Sorts of h1 is Relation-like non-empty non empty-yielding the carrier' of U1 -defined Function-like non empty total set

h2 is strict non-empty MSAlgebra over U1

the Sorts of h2 is Relation-like non-empty non empty-yielding the carrier of U1 -defined Function-like non empty total set

the Charact of h2 is Relation-like the carrier' of U1 -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Arity of U1 * ( the Sorts of h2 #), the ResultSort of U1 * the Sorts of h2

the Sorts of h2 # is Relation-like the carrier of U1 * -defined Function-like non empty total set

the Arity of U1 * ( the Sorts of h2 #) is Relation-like the carrier' of U1 -defined Function-like non empty total set

the ResultSort of U1 * the Sorts of h2 is Relation-like non-empty non empty-yielding the carrier' of U1 -defined Function-like non empty total set

U1 is non empty non void V67() strict ManySortedSign

U2 is strict non-empty MSAlgebra over U1

(U1,U1,U2) is strict non-empty MSAlgebra over U1

the Charact of (U1,U1,U2) is Relation-like the carrier' of U1 -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Arity of U1 * ( the Sorts of (U1,U1,U2) #), the ResultSort of U1 * the Sorts of (U1,U1,U2)

the carrier' of U1 is non empty set

the Arity of U1 is Relation-like the carrier' of U1 -defined the carrier of U1 * -valued Function-like non empty total V18( the carrier' of U1, the carrier of U1 * ) Function-yielding V22() Element of K19(K20( the carrier' of U1,( the carrier of U1 *)))

the carrier of U1 is non empty set

the carrier of U1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U1

K20( the carrier' of U1,( the carrier of U1 *)) is Relation-like set

K19(K20( the carrier' of U1,( the carrier of U1 *))) is set

the Sorts of (U1,U1,U2) is Relation-like non-empty non empty-yielding the carrier of U1 -defined Function-like non empty total set

the Sorts of (U1,U1,U2) # is Relation-like the carrier of U1 * -defined Function-like non empty total set

the Arity of U1 * ( the Sorts of (U1,U1,U2) #) is Relation-like the carrier' of U1 -defined Function-like non empty total set

the ResultSort of U1 is Relation-like the carrier' of U1 -defined the carrier of U1 -valued Function-like non empty total V18( the carrier' of U1, the carrier of U1) Element of K19(K20( the carrier' of U1, the carrier of U1))

K20( the carrier' of U1, the carrier of U1) is Relation-like set

K19(K20( the carrier' of U1, the carrier of U1)) is set

the ResultSort of U1 * the Sorts of (U1,U1,U2) is Relation-like non-empty non empty-yielding the carrier' of U1 -defined Function-like non empty total set

the Charact of U2 is Relation-like the carrier' of U1 -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Arity of U1 * ( the Sorts of U2 #), the ResultSort of U1 * the Sorts of U2

the Sorts of U2 is Relation-like non-empty non empty-yielding the carrier of U1 -defined Function-like non empty total set

the Sorts of U2 # is Relation-like the carrier of U1 * -defined Function-like non empty total set

the Arity of U1 * ( the Sorts of U2 #) is Relation-like the carrier' of U1 -defined Function-like non empty total set

the ResultSort of U1 * the Sorts of U2 is Relation-like non-empty non empty-yielding the carrier' of U1 -defined Function-like non empty total set

the Charact of U2 | the carrier' of U1 is Relation-like the carrier' of U1 -defined the carrier' of U1 -defined Function-like Function-yielding V22() set

the Sorts of U2 | the carrier of U1 is Relation-like non-empty the carrier of U1 -defined the carrier of U1 -defined Function-like set

U1 is non empty V91() V92() non-empty UAStr

MSSign U1 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

U2 is non empty V91() V92() non-empty UAStr

MSSign U2 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

signature U1 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature U1) is Element of K19(NAT)

K20((dom (signature U1)),({0} *)) is Relation-like set

K19(K20((dom (signature U1)),({0} *))) is set

(*--> 0) * (signature U1) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V22() Element of K19(K20(NAT,({0} *)))

the carrier of (MSSign U1) is non empty V12() V30() set

the carrier' of (MSSign U1) is non empty set

the carrier of (MSSign U1) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign U1)

the Arity of (MSSign U1) is Relation-like the carrier' of (MSSign U1) -defined the carrier of (MSSign U1) * -valued Function-like non empty total V18( the carrier' of (MSSign U1), the carrier of (MSSign U1) * ) Function-yielding V22() Element of K19(K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *)))

K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *)) is Relation-like set

K19(K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *))) is set

U3 is Relation-like dom (signature U1) -defined {0} * -valued Function-like total V18( dom (signature U1),{0} * ) Function-yielding V22() Element of K19(K20((dom (signature U1)),({0} *)))

signature U2 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature U2) is Element of K19(NAT)

K20((dom (signature U2)),({0} *)) is Relation-like set

K19(K20((dom (signature U2)),({0} *))) is set

(*--> 0) * (signature U2) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V22() Element of K19(K20(NAT,({0} *)))

the carrier' of (MSSign U2) is non empty set

the carrier of (MSSign U2) is non empty V12() V30() set

the carrier of (MSSign U2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign U2)

the Arity of (MSSign U2) is Relation-like the carrier' of (MSSign U2) -defined the carrier of (MSSign U2) * -valued Function-like non empty total V18( the carrier' of (MSSign U2), the carrier of (MSSign U2) * ) Function-yielding V22() Element of K19(K20( the carrier' of (MSSign U2),( the carrier of (MSSign U2) *)))

K20( the carrier' of (MSSign U2),( the carrier of (MSSign U2) *)) is Relation-like set

K19(K20( the carrier' of (MSSign U2),( the carrier of (MSSign U2) *))) is set

h1 is Relation-like dom (signature U2) -defined {0} * -valued Function-like total V18( dom (signature U2),{0} * ) Function-yielding V22() Element of K19(K20((dom (signature U2)),({0} *)))

the ResultSort of (MSSign U2) is Relation-like the carrier' of (MSSign U2) -defined the carrier of (MSSign U2) -valued Function-like non empty total V18( the carrier' of (MSSign U2), the carrier of (MSSign U2)) Element of K19(K20( the carrier' of (MSSign U2), the carrier of (MSSign U2)))

K20( the carrier' of (MSSign U2), the carrier of (MSSign U2)) is Relation-like set

K19(K20( the carrier' of (MSSign U2), the carrier of (MSSign U2))) is set

(dom (signature U2)) --> 0 is Relation-like dom (signature U2) -defined NAT -valued Function-like constant total V18( dom (signature U2), NAT ) Function-yielding V22() Element of K19(K20((dom (signature U2)),NAT))

K20((dom (signature U2)),NAT) is Relation-like set

K19(K20((dom (signature U2)),NAT)) is set

K20((dom (signature U2)),{0}) is Relation-like set

the ResultSort of (MSSign U1) is Relation-like the carrier' of (MSSign U1) -defined the carrier of (MSSign U1) -valued Function-like non empty total V18( the carrier' of (MSSign U1), the carrier of (MSSign U1)) Element of K19(K20( the carrier' of (MSSign U1), the carrier of (MSSign U1)))

K20( the carrier' of (MSSign U1), the carrier of (MSSign U1)) is Relation-like set

K19(K20( the carrier' of (MSSign U1), the carrier of (MSSign U1))) is set

(dom (signature U1)) --> 0 is Relation-like dom (signature U1) -defined NAT -valued Function-like constant total V18( dom (signature U1), NAT ) Function-yielding V22() Element of K19(K20((dom (signature U1)),NAT))

K20((dom (signature U1)),NAT) is Relation-like set

K19(K20((dom (signature U1)),NAT)) is set

K20((dom (signature U1)),{0}) is Relation-like set

U1 is non empty V91() V92() non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() V92() non-empty UAStr

the carrier of U2 is non empty set

K20( the carrier of U1, the carrier of U2) is Relation-like set

K19(K20( the carrier of U1, the carrier of U2)) is set

MSSign U1 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

MSSign U2 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

U3 is Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like non empty total V18( the carrier of U1, the carrier of U2) Element of K19(K20( the carrier of U1, the carrier of U2))

0 .--> U3 is Relation-like NAT -defined {0} -defined Function-like one-to-one Function-yielding V22() set

{0} --> U3 is Relation-like non-empty non empty-yielding {0} -defined {U3} -valued Function-like constant non empty total V18({0},{U3}) Function-yielding V22() Element of K19(K20({0},{U3}))

{U3} is functional non empty set

K20({0},{U3}) is Relation-like set

K19(K20({0},{U3})) is set

the carrier of (MSSign U1) is non empty V12() V30() set

MSAlg U1 is strict non-empty MSAlgebra over MSSign U1

the Sorts of (MSAlg U1) is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set

MSAlg U2 is strict non-empty MSAlgebra over MSSign U2

((MSSign U1),(MSSign U2),(MSAlg U2)) is strict non-empty MSAlgebra over MSSign U1

the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set

the carrier of (MSSign U2) is non empty V12() V30() set

the Sorts of (MSAlg U2) is Relation-like non-empty non empty-yielding the carrier of (MSSign U2) -defined Function-like non empty total set

MSSorts U2 is Relation-like non-empty non empty-yielding the carrier of (MSSign U2) -defined Function-like non empty total set

MSCharact U2 is Relation-like the carrier' of (MSSign U2) -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Arity of (MSSign U2) * ((MSSorts U2) #), the ResultSort of (MSSign U2) * (MSSorts U2)

the carrier' of (MSSign U2) is non empty set

the Arity of (MSSign U2) is Relation-like the carrier' of (MSSign U2) -defined the carrier of (MSSign U2) * -valued Function-like non empty total V18( the carrier' of (MSSign U2), the carrier of (MSSign U2) * ) Function-yielding V22() Element of K19(K20( the carrier' of (MSSign U2),( the carrier of (MSSign U2) *)))

the carrier of (MSSign U2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign U2)

K20( the carrier' of (MSSign U2),( the carrier of (MSSign U2) *)) is Relation-like set

K19(K20( the carrier' of (MSSign U2),( the carrier of (MSSign U2) *))) is set

(MSSorts U2) # is Relation-like the carrier of (MSSign U2) * -defined Function-like non empty total set

the Arity of (MSSign U2) * ((MSSorts U2) #) is Relation-like the carrier' of (MSSign U2) -defined Function-like non empty total set

the ResultSort of (MSSign U2) is Relation-like the carrier' of (MSSign U2) -defined the carrier of (MSSign U2) -valued Function-like non empty total V18( the carrier' of (MSSign U2), the carrier of (MSSign U2)) Element of K19(K20( the carrier' of (MSSign U2), the carrier of (MSSign U2)))

K20( the carrier' of (MSSign U2), the carrier of (MSSign U2)) is Relation-like set

K19(K20( the carrier' of (MSSign U2), the carrier of (MSSign U2))) is set

the ResultSort of (MSSign U2) * (MSSorts U2) is Relation-like non-empty non empty-yielding the carrier' of (MSSign U2) -defined Function-like non empty total set

MSAlgebra(# (MSSorts U2),(MSCharact U2) #) is strict MSAlgebra over MSSign U2

the Sorts of (MSAlg U2) . 0 is set

0 .--> the carrier of U2 is Relation-like NAT -defined {0} -defined Function-like one-to-one set

{0} --> the carrier of U2 is Relation-like non-empty non empty-yielding {0} -defined { the carrier of U2} -valued Function-like constant non empty total V18({0},{ the carrier of U2}) Element of K19(K20({0},{ the carrier of U2}))

{ the carrier of U2} is non empty set

K20({0},{ the carrier of U2}) is Relation-like set

K19(K20({0},{ the carrier of U2})) is set

(0 .--> the carrier of U2) . 0 is set

MSSorts U1 is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set

MSCharact U1 is Relation-like the carrier' of (MSSign U1) -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Arity of (MSSign U1) * ((MSSorts U1) #), the ResultSort of (MSSign U1) * (MSSorts U1)

the carrier' of (MSSign U1) is non empty set

the Arity of (MSSign U1) is Relation-like the carrier' of (MSSign U1) -defined the carrier of (MSSign U1) * -valued Function-like non empty total V18( the carrier' of (MSSign U1), the carrier of (MSSign U1) * ) Function-yielding V22() Element of K19(K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *)))

the carrier of (MSSign U1) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign U1)

K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *)) is Relation-like set

K19(K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *))) is set

(MSSorts U1) # is Relation-like the carrier of (MSSign U1) * -defined Function-like non empty total set

the Arity of (MSSign U1) * ((MSSorts U1) #) is Relation-like the carrier' of (MSSign U1) -defined Function-like non empty total set

the ResultSort of (MSSign U1) is Relation-like the carrier' of (MSSign U1) -defined the carrier of (MSSign U1) -valued Function-like non empty total V18( the carrier' of (MSSign U1), the carrier of (MSSign U1)) Element of K19(K20( the carrier' of (MSSign U1), the carrier of (MSSign U1)))

K20( the carrier' of (MSSign U1), the carrier of (MSSign U1)) is Relation-like set

K19(K20( the carrier' of (MSSign U1), the carrier of (MSSign U1))) is set

the ResultSort of (MSSign U1) * (MSSorts U1) is Relation-like non-empty non empty-yielding the carrier' of (MSSign U1) -defined Function-like non empty total set

MSAlgebra(# (MSSorts U1),(MSCharact U1) #) is strict MSAlgebra over MSSign U1

the Sorts of (MSAlg U1) . 0 is set

0 .--> the carrier of U1 is Relation-like NAT -defined {0} -defined Function-like one-to-one set

{0} --> the carrier of U1 is Relation-like non-empty non empty-yielding {0} -defined { the carrier of U1} -valued Function-like constant non empty total V18({0},{ the carrier of U1}) Element of K19(K20({0},{ the carrier of U1}))

{ the carrier of U1} is non empty set

K20({0},{ the carrier of U1}) is Relation-like set

K19(K20({0},{ the carrier of U1})) is set

(0 .--> the carrier of U1) . 0 is set

a is set

(0 .--> U3) . a is Relation-like Function-like set

the Sorts of (MSAlg U1) . a is set

the Sorts of (MSAlg U2) . a is set

K20(( the Sorts of (MSAlg U1) . a),( the Sorts of (MSAlg U2) . a)) is Relation-like set

K19(K20(( the Sorts of (MSAlg U1) . a),( the Sorts of (MSAlg U2) . a))) is set

h is Relation-like {0} -defined Function-like non empty total set

h1 is Relation-like {0} -defined Function-like non empty total set

U1 is non empty V91() V92() non-empty UAStr

the carrier of U1 is non empty set

MSSign U1 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

the carrier' of (MSSign U1) is non empty set

MSAlg U1 is strict non-empty MSAlgebra over MSSign U1

the Sorts of (MSAlg U1) is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set

the carrier of (MSSign U1) is non empty V12() V30() set

U2 is non empty V91() V92() non-empty UAStr

the carrier of U2 is non empty set

K20( the carrier of U1, the carrier of U2) is Relation-like set

K19(K20( the carrier of U1, the carrier of U2)) is set

MSSign U2 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

MSAlg U2 is strict non-empty MSAlgebra over MSSign U2

((MSSign U1),(MSSign U2),(MSAlg U2)) is strict non-empty MSAlgebra over MSSign U1

the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set

U3 is Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like non empty total V18( the carrier of U1, the carrier of U2) Element of K19(K20( the carrier of U1, the carrier of U2))

(U1,U2,U3) is Relation-like the carrier of (MSSign U1) -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Sorts of (MSAlg U1), the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))

h2 is Element of the carrier' of (MSSign U1)

the_result_sort_of h2 is Element of the carrier of (MSSign U1)

the Sorts of (MSAlg U1) . (the_result_sort_of h2) is non empty set

the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of h2) is non empty set

(U1,U2,U3) . (the_result_sort_of h2) is Relation-like the Sorts of (MSAlg U1) . (the_result_sort_of h2) -defined the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of h2) -valued Function-like non empty total V18( the Sorts of (MSAlg U1) . (the_result_sort_of h2), the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of h2)) Element of K19(K20(( the Sorts of (MSAlg U1) . (the_result_sort_of h2)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of h2))))

K20(( the Sorts of (MSAlg U1) . (the_result_sort_of h2)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of h2))) is Relation-like set

K19(K20(( the Sorts of (MSAlg U1) . (the_result_sort_of h2)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of h2)))) is set

signature U1 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature U1) is Element of K19(NAT)

the ResultSort of (MSSign U1) is Relation-like the carrier' of (MSSign U1) -defined the carrier of (MSSign U1) -valued Function-like non empty total V18( the carrier' of (MSSign U1), the carrier of (MSSign U1)) Element of K19(K20( the carrier' of (MSSign U1), the carrier of (MSSign U1)))

K20( the carrier' of (MSSign U1), the carrier of (MSSign U1)) is Relation-like set

K19(K20( the carrier' of (MSSign U1), the carrier of (MSSign U1))) is set

(dom (signature U1)) --> 0 is Relation-like dom (signature U1) -defined NAT -valued Function-like constant total V18( dom (signature U1), NAT ) Function-yielding V22() Element of K19(K20((dom (signature U1)),NAT))

K20((dom (signature U1)),NAT) is Relation-like set

K19(K20((dom (signature U1)),NAT)) is set

K20((dom (signature U1)),{0}) is Relation-like set

h is V23() V24() V25() V29() V119() V120() ext-real set

Seg h is V30() V37(h) Element of K19(NAT)

h |-> 0 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like Element of h -tuples_on NAT

h -tuples_on NAT is FinSequenceSet of NAT

NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT

{ b

(Seg h) --> 0 is Relation-like Seg h -defined NAT -valued {0} -valued Function-like constant total V18( Seg h,{0}) Function-yielding V22() Element of K19(K20((Seg h),{0}))

K20((Seg h),{0}) is Relation-like set

K19(K20((Seg h),{0})) is set

(h |-> 0) . h2 is set

the ResultSort of (MSSign U1) . h2 is Element of the carrier of (MSSign U1)

(U1,U2,U3) . ( the ResultSort of (MSSign U1) . h2) is Relation-like the Sorts of (MSAlg U1) . ( the ResultSort of (MSSign U1) . h2) -defined the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ( the ResultSort of (MSSign U1) . h2) -valued Function-like non empty total V18( the Sorts of (MSAlg U1) . ( the ResultSort of (MSSign U1) . h2), the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ( the ResultSort of (MSSign U1) . h2)) Element of K19(K20(( the Sorts of (MSAlg U1) . ( the ResultSort of (MSSign U1) . h2)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ( the ResultSort of (MSSign U1) . h2))))

the Sorts of (MSAlg U1) . ( the ResultSort of (MSSign U1) . h2) is non empty set

the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ( the ResultSort of (MSSign U1) . h2) is non empty set

K20(( the Sorts of (MSAlg U1) . ( the ResultSort of (MSSign U1) . h2)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ( the ResultSort of (MSSign U1) . h2))) is Relation-like set

K19(K20(( the Sorts of (MSAlg U1) . ( the ResultSort of (MSSign U1) . h2)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ( the ResultSort of (MSSign U1) . h2)))) is set

0 .--> U3 is Relation-like NAT -defined {0} -defined Function-like one-to-one Function-yielding V22() set

{0} --> U3 is Relation-like non-empty non empty-yielding {0} -defined {U3} -valued Function-like constant non empty total V18({0},{U3}) Function-yielding V22() Element of K19(K20({0},{U3}))

{U3} is functional non empty set

K20({0},{U3}) is Relation-like set

K19(K20({0},{U3})) is set

(0 .--> U3) . 0 is Relation-like Function-like set

U1 is non empty V91() V92() non-empty UAStr

MSSign U1 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

the carrier' of (MSSign U1) is non empty set

MSAlg U1 is strict non-empty MSAlgebra over MSSign U1

the charact of U1 is Relation-like NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 is non empty set

the carrier of U1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is set

U2 is Element of the carrier' of (MSSign U1)

Den (U2,(MSAlg U1)) is Relation-like Args (U2,(MSAlg U1)) -defined Result (U2,(MSAlg U1)) -valued Function-like non empty total V18( Args (U2,(MSAlg U1)), Result (U2,(MSAlg U1))) Element of K19(K20((Args (U2,(MSAlg U1))),(Result (U2,(MSAlg U1)))))

Args (U2,(MSAlg U1)) is functional non empty Element of rng ( the Sorts of (MSAlg U1) #)

the carrier of (MSSign U1) is non empty V12() V30() set

the Sorts of (MSAlg U1) is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set

the Sorts of (MSAlg U1) # is Relation-like the carrier of (MSSign U1) * -defined Function-like non empty total set

the carrier of (MSSign U1) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign U1)

rng ( the Sorts of (MSAlg U1) #) is non empty set

Result (U2,(MSAlg U1)) is non empty Element of rng the Sorts of (MSAlg U1)

rng the Sorts of (MSAlg U1) is non empty V42() set

K20((Args (U2,(MSAlg U1))),(Result (U2,(MSAlg U1)))) is Relation-like set

K19(K20((Args (U2,(MSAlg U1))),(Result (U2,(MSAlg U1))))) is set

the charact of U1 . U2 is set

MSSorts U1 is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set

MSCharact U1 is Relation-like the carrier' of (MSSign U1) -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Arity of (MSSign U1) * ((MSSorts U1) #), the ResultSort of (MSSign U1) * (MSSorts U1)

the Arity of (MSSign U1) is Relation-like the carrier' of (MSSign U1) -defined the carrier of (MSSign U1) * -valued Function-like non empty total V18( the carrier' of (MSSign U1), the carrier of (MSSign U1) * ) Function-yielding V22() Element of K19(K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *)))

K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *)) is Relation-like set

K19(K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *))) is set

(MSSorts U1) # is Relation-like the carrier of (MSSign U1) * -defined Function-like non empty total set

the Arity of (MSSign U1) * ((MSSorts U1) #) is Relation-like the carrier' of (MSSign U1) -defined Function-like non empty total set

the ResultSort of (MSSign U1) is Relation-like the carrier' of (MSSign U1) -defined the carrier of (MSSign U1) -valued Function-like non empty total V18( the carrier' of (MSSign U1), the carrier of (MSSign U1)) Element of K19(K20( the carrier' of (MSSign U1), the carrier of (MSSign U1)))

K20( the carrier' of (MSSign U1), the carrier of (MSSign U1)) is Relation-like set

K19(K20( the carrier' of (MSSign U1), the carrier of (MSSign U1))) is set

the ResultSort of (MSSign U1) * (MSSorts U1) is Relation-like non-empty non empty-yielding the carrier' of (MSSign U1) -defined Function-like non empty total set

MSAlgebra(# (MSSorts U1),(MSCharact U1) #) is strict MSAlgebra over MSSign U1

(MSCharact U1) . U2 is Relation-like ( the Arity of (MSSign U1) * ((MSSorts U1) #)) . U2 -defined ( the ResultSort of (MSSign U1) * (MSSorts U1)) . U2 -valued Function-like total V18(( the Arity of (MSSign U1) * ((MSSorts U1) #)) . U2,( the ResultSort of (MSSign U1) * (MSSorts U1)) . U2) Element of K19(K20((( the Arity of (MSSign U1) * ((MSSorts U1) #)) . U2),(( the ResultSort of (MSSign U1) * (MSSorts U1)) . U2)))

( the Arity of (MSSign U1) * ((MSSorts U1) #)) . U2 is set

( the ResultSort of (MSSign U1) * (MSSorts U1)) . U2 is non empty set

K20((( the Arity of (MSSign U1) * ((MSSorts U1) #)) . U2),(( the ResultSort of (MSSign U1) * (MSSorts U1)) . U2)) is Relation-like set

K19(K20((( the Arity of (MSSign U1) * ((MSSorts U1) #)) . U2),(( the ResultSort of (MSSign U1) * (MSSorts U1)) . U2))) is set

U1 is non empty V91() V92() non-empty UAStr

signature U1 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature U1) is Element of K19(NAT)

the charact of U1 is Relation-like NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 is non empty set

the carrier of U1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is set

dom the charact of U1 is Element of K19(NAT)

len (signature U1) is V23() V24() V25() V29() V119() V120() ext-real Element of NAT

Seg (len (signature U1)) is V30() V37( len (signature U1)) Element of K19(NAT)

len the charact of U1 is V23() V24() V25() V29() V119() V120() ext-real Element of NAT

Seg (len the charact of U1) is V30() V37( len the charact of U1) Element of K19(NAT)

U1 is non empty V91() V92() non-empty UAStr

MSSign U1 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

the carrier' of (MSSign U1) is non empty set

MSAlg U1 is strict non-empty MSAlgebra over MSSign U1

the carrier of U1 is non empty set

the carrier of U1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U1

Operations U1 is non empty M15( the carrier of U1)

the charact of U1 is Relation-like NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

PFuncs (( the carrier of U1 *), the carrier of U1) is set

rng the charact of U1 is set

U2 is Element of the carrier' of (MSSign U1)

Den (U2,(MSAlg U1)) is Relation-like Args (U2,(MSAlg U1)) -defined Result (U2,(MSAlg U1)) -valued Function-like non empty total V18( Args (U2,(MSAlg U1)), Result (U2,(MSAlg U1))) Element of K19(K20((Args (U2,(MSAlg U1))),(Result (U2,(MSAlg U1)))))

Args (U2,(MSAlg U1)) is functional non empty Element of rng ( the Sorts of (MSAlg U1) #)

the carrier of (MSSign U1) is non empty V12() V30() set

the Sorts of (MSAlg U1) is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set

the Sorts of (MSAlg U1) # is Relation-like the carrier of (MSSign U1) * -defined Function-like non empty total set

the carrier of (MSSign U1) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign U1)

rng ( the Sorts of (MSAlg U1) #) is non empty set

Result (U2,(MSAlg U1)) is non empty Element of rng the Sorts of (MSAlg U1)

rng the Sorts of (MSAlg U1) is non empty V42() set

K20((Args (U2,(MSAlg U1))),(Result (U2,(MSAlg U1)))) is Relation-like set

K19(K20((Args (U2,(MSAlg U1))),(Result (U2,(MSAlg U1))))) is set

signature U1 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature U1) is Element of K19(NAT)

dom the charact of U1 is Element of K19(NAT)

the charact of U1 . U2 is set

U1 is non empty V91() V92() non-empty UAStr

MSSign U1 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

the carrier' of (MSSign U1) is non empty set

U2 is non empty V91() V92() non-empty UAStr

MSSign U2 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

MSAlg U2 is strict non-empty MSAlgebra over MSSign U2

((MSSign U1),(MSSign U2),(MSAlg U2)) is strict non-empty MSAlgebra over MSSign U1

the carrier of U2 is non empty set

the carrier of U2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U2

Operations U2 is non empty M15( the carrier of U2)

the charact of U2 is Relation-like NAT -defined PFuncs (( the carrier of U2 *), the carrier of U2) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of U2 *), the carrier of U2)

PFuncs (( the carrier of U2 *), the carrier of U2) is set

rng the charact of U2 is set

MSSorts U2 is Relation-like non-empty non empty-yielding the carrier of (MSSign U2) -defined Function-like non empty total set

the carrier of (MSSign U2) is non empty V12() V30() set

MSCharact U2 is Relation-like the carrier' of (MSSign U2) -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Arity of (MSSign U2) * ((MSSorts U2) #), the ResultSort of (MSSign U2) * (MSSorts U2)

the carrier' of (MSSign U2) is non empty set

the Arity of (MSSign U2) is Relation-like the carrier' of (MSSign U2) -defined the carrier of (MSSign U2) * -valued Function-like non empty total V18( the carrier' of (MSSign U2), the carrier of (MSSign U2) * ) Function-yielding V22() Element of K19(K20( the carrier' of (MSSign U2),( the carrier of (MSSign U2) *)))

the carrier of (MSSign U2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign U2)

K20( the carrier' of (MSSign U2),( the carrier of (MSSign U2) *)) is Relation-like set

K19(K20( the carrier' of (MSSign U2),( the carrier of (MSSign U2) *))) is set

(MSSorts U2) # is Relation-like the carrier of (MSSign U2) * -defined Function-like non empty total set

the Arity of (MSSign U2) * ((MSSorts U2) #) is Relation-like the carrier' of (MSSign U2) -defined Function-like non empty total set

the ResultSort of (MSSign U2) is Relation-like the carrier' of (MSSign U2) -defined the carrier of (MSSign U2) -valued Function-like non empty total V18( the carrier' of (MSSign U2), the carrier of (MSSign U2)) Element of K19(K20( the carrier' of (MSSign U2), the carrier of (MSSign U2)))

K20( the carrier' of (MSSign U2), the carrier of (MSSign U2)) is Relation-like set

K19(K20( the carrier' of (MSSign U2), the carrier of (MSSign U2))) is set

the ResultSort of (MSSign U2) * (MSSorts U2) is Relation-like non-empty non empty-yielding the carrier' of (MSSign U2) -defined Function-like non empty total set

MSAlgebra(# (MSSorts U2),(MSCharact U2) #) is strict MSAlgebra over MSSign U2

h1 is Element of the carrier' of (MSSign U1)

Den (h1,((MSSign U1),(MSSign U2),(MSAlg U2))) is Relation-like Args (h1,((MSSign U1),(MSSign U2),(MSAlg U2))) -defined Result (h1,((MSSign U1),(MSSign U2),(MSAlg U2))) -valued Function-like non empty total V18( Args (h1,((MSSign U1),(MSSign U2),(MSAlg U2))), Result (h1,((MSSign U1),(MSSign U2),(MSAlg U2)))) Element of K19(K20((Args (h1,((MSSign U1),(MSSign U2),(MSAlg U2)))),(Result (h1,((MSSign U1),(MSSign U2),(MSAlg U2))))))

Args (h1,((MSSign U1),(MSSign U2),(MSAlg U2))) is functional non empty Element of rng ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)

the carrier of (MSSign U1) is non empty V12() V30() set

the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set

the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) # is Relation-like the carrier of (MSSign U1) * -defined Function-like non empty total set

the carrier of (MSSign U1) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign U1)

rng ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #) is non empty set

Result (h1,((MSSign U1),(MSSign U2),(MSAlg U2))) is non empty Element of rng the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))

rng the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) is non empty V42() set

K20((Args (h1,((MSSign U1),(MSSign U2),(MSAlg U2)))),(Result (h1,((MSSign U1),(MSSign U2),(MSAlg U2))))) is Relation-like set

K19(K20((Args (h1,((MSSign U1),(MSSign U2),(MSAlg U2)))),(Result (h1,((MSSign U1),(MSSign U2),(MSAlg U2)))))) is set

the Arity of (MSSign U1) is Relation-like the carrier' of (MSSign U1) -defined the carrier of (MSSign U1) * -valued Function-like non empty total V18( the carrier' of (MSSign U1), the carrier of (MSSign U1) * ) Function-yielding V22() Element of K19(K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *)))

K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *)) is Relation-like set

K19(K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *))) is set

the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #) is Relation-like the carrier' of (MSSign U1) -defined Function-like non empty total set

the ResultSort of (MSSign U1) is Relation-like the carrier' of (MSSign U1) -defined the carrier of (MSSign U1) -valued Function-like non empty total V18( the carrier' of (MSSign U1), the carrier of (MSSign U1)) Element of K19(K20( the carrier' of (MSSign U1), the carrier of (MSSign U1)))

K20( the carrier' of (MSSign U1), the carrier of (MSSign U1)) is Relation-like set

K19(K20( the carrier' of (MSSign U1), the carrier of (MSSign U1))) is set

the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) is Relation-like non-empty non empty-yielding the carrier' of (MSSign U1) -defined Function-like non empty total set

the Charact of ((MSSign U1),(MSSign U2),(MSAlg U2)) is Relation-like the carrier' of (MSSign U1) -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #), the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))

the Charact of ((MSSign U1),(MSSign U2),(MSAlg U2)) . h1 is Relation-like ( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . h1 -defined ( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . h1 -valued Function-like total V18(( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . h1,( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . h1) Element of K19(K20((( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . h1),(( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . h1)))

( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . h1 is set

( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . h1 is non empty set

K20((( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . h1),(( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . h1)) is Relation-like set

K19(K20((( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . h1),(( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . h1))) is set

(MSCharact U2) . h1 is Relation-like Function-like set

the charact of U2 . h1 is set

signature U1 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature U1) is Element of K19(NAT)

the charact of U1 is Relation-like NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 is non empty set

the carrier of U1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is set

dom the charact of U1 is Element of K19(NAT)

signature U2 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom the charact of U2 is Element of K19(NAT)

U1 is non empty V91() V92() non-empty UAStr

MSSign U1 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

the carrier' of (MSSign U1) is non empty set

MSAlg U1 is strict non-empty MSAlgebra over MSSign U1

the carrier of U1 is non empty set

U2 is Element of the carrier' of (MSSign U1)

Args (U2,(MSAlg U1)) is functional non empty Element of rng ( the Sorts of (MSAlg U1) #)

the carrier of (MSSign U1) is non empty V12() V30() set

the Sorts of (MSAlg U1) is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set

the Sorts of (MSAlg U1) # is Relation-like the carrier of (MSSign U1) * -defined Function-like non empty total set

the carrier of (MSSign U1) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign U1)

rng ( the Sorts of (MSAlg U1) #) is non empty set

U3 is Relation-like Function-like Element of Args (U2,(MSAlg U1))

Den (U2,(MSAlg U1)) is Relation-like Args (U2,(MSAlg U1)) -defined Result (U2,(MSAlg U1)) -valued Function-like non empty total V18( Args (U2,(MSAlg U1)), Result (U2,(MSAlg U1))) Element of K19(K20((Args (U2,(MSAlg U1))),(Result (U2,(MSAlg U1)))))

Result (U2,(MSAlg U1)) is non empty Element of rng the Sorts of (MSAlg U1)

rng the Sorts of (MSAlg U1) is non empty V42() set

K20((Args (U2,(MSAlg U1))),(Result (U2,(MSAlg U1)))) is Relation-like set

K19(K20((Args (U2,(MSAlg U1))),(Result (U2,(MSAlg U1))))) is set

the charact of U1 is Relation-like NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is set

the charact of U1 . U2 is set

signature U1 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature U1) is Element of K19(NAT)

dom the charact of U1 is Element of K19(NAT)

Operations U1 is non empty M15( the carrier of U1)

rng the charact of U1 is set

h2 is Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like non empty V101() V102( the carrier of U1) M16( the carrier of U1, Operations U1)

dom h2 is functional non empty FinSequence-membered Element of K19(( the carrier of U1 *))

K19(( the carrier of U1 *)) is set

U1 is non empty V91() V92() non-empty UAStr

the carrier of U1 is non empty set

MSSign U1 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

the carrier' of (MSSign U1) is non empty set

MSAlg U1 is strict non-empty MSAlgebra over MSSign U1

U2 is non empty V91() V92() non-empty UAStr

the carrier of U2 is non empty set

K20( the carrier of U1, the carrier of U2) is Relation-like set

K19(K20( the carrier of U1, the carrier of U2)) is set

MSSign U2 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

MSAlg U2 is strict non-empty MSAlgebra over MSSign U2

((MSSign U1),(MSSign U2),(MSAlg U2)) is strict non-empty MSAlgebra over MSSign U1

U3 is Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like non empty total V18( the carrier of U1, the carrier of U2) Element of K19(K20( the carrier of U1, the carrier of U2))

(U1,U2,U3) is Relation-like the carrier of (MSSign U1) -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Sorts of (MSAlg U1), the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))

the carrier of (MSSign U1) is non empty V12() V30() set

the Sorts of (MSAlg U1) is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set

the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set

signature U1 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature U1) is Element of K19(NAT)

K20((dom (signature U1)),({0} *)) is Relation-like set

K19(K20((dom (signature U1)),({0} *))) is set

(*--> 0) * (signature U1) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V22() Element of K19(K20(NAT,({0} *)))

h2 is Element of the carrier' of (MSSign U1)

Args (h2,(MSAlg U1)) is functional non empty Element of rng ( the Sorts of (MSAlg U1) #)

the Sorts of (MSAlg U1) # is Relation-like the carrier of (MSSign U1) * -defined Function-like non empty total set

the carrier of (MSSign U1) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign U1)

rng ( the Sorts of (MSAlg U1) #) is non empty set

the carrier' of (MSSign U2) is non empty set

signature U2 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature U2) is Element of K19(NAT)

h1 is Relation-like dom (signature U1) -defined {0} * -valued Function-like total V18( dom (signature U1),{0} * ) Function-yielding V22() Element of K19(K20((dom (signature U1)),({0} *)))

dom h1 is Element of K19((dom (signature U1)))

K19((dom (signature U1))) is set

((*--> 0) * (signature U1)) . h2 is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

(signature U1) . h2 is set

(*--> 0) . ((signature U1) . h2) is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

h is Relation-like Function-like Element of Args (h2,(MSAlg U1))

(U1,U2,U3) # h is Relation-like Function-like Element of Args (h2,((MSSign U1),(MSSign U2),(MSAlg U2)))

Args (h2,((MSSign U1),(MSSign U2),(MSAlg U2))) is functional non empty Element of rng ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)

the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) # is Relation-like the carrier of (MSSign U1) * -defined Function-like non empty total set

rng ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #) is non empty set

h * U3 is Relation-like the carrier of U2 -valued Function-like set

dom (h * U3) is set

dom U3 is non empty Element of K19( the carrier of U1)

K19( the carrier of U1) is set

rng h is set

dom h is set

the Arity of (MSSign U1) is Relation-like the carrier' of (MSSign U1) -defined the carrier of (MSSign U1) * -valued Function-like non empty total V18( the carrier' of (MSSign U1), the carrier of (MSSign U1) * ) Function-yielding V22() Element of K19(K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *)))

K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *)) is Relation-like set

K19(K20( the carrier' of (MSSign U1),( the carrier of (MSSign U1) *))) is set

the_arity_of h2 is Relation-like NAT -defined the carrier of (MSSign U1) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (MSSign U1) *

rng (signature U1) is Element of K19(NAT)

x is V23() V24() V25() V29() V119() V120() ext-real Element of NAT

x |-> 0 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like Element of x -tuples_on NAT

x -tuples_on NAT is FinSequenceSet of NAT

NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT

{ b

Seg x is V30() V37(x) Element of K19(NAT)

(Seg x) --> 0 is Relation-like Seg x -defined NAT -valued {0} -valued Function-like constant total V18( Seg x,{0}) Function-yielding V22() Element of K19(K20((Seg x),{0}))

K20((Seg x),{0}) is Relation-like set

K19(K20((Seg x),{0})) is set

O1 is V23() V24() V25() V29() V119() V120() ext-real set

(the_arity_of h2) /. O1 is Element of the carrier of (MSSign U1)

y is Relation-like NAT -defined the carrier of (MSSign U1) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (MSSign U1) *

y /. O1 is Element of the carrier of (MSSign U1)

dom (x |-> 0) is Element of K19(NAT)

dom (the_arity_of h2) is Element of K19(NAT)

y . O1 is set

(U1,U2,U3) . ((the_arity_of h2) /. O1) is Relation-like the Sorts of (MSAlg U1) . ((the_arity_of h2) /. O1) -defined the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ((the_arity_of h2) /. O1) -valued Function-like non empty total V18( the Sorts of (MSAlg U1) . ((the_arity_of h2) /. O1), the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ((the_arity_of h2) /. O1)) Element of K19(K20(( the Sorts of (MSAlg U1) . ((the_arity_of h2) /. O1)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ((the_arity_of h2) /. O1))))

the Sorts of (MSAlg U1) . ((the_arity_of h2) /. O1) is non empty set

the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ((the_arity_of h2) /. O1) is non empty set

K20(( the Sorts of (MSAlg U1) . ((the_arity_of h2) /. O1)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ((the_arity_of h2) /. O1))) is Relation-like set

K19(K20(( the Sorts of (MSAlg U1) . ((the_arity_of h2) /. O1)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ((the_arity_of h2) /. O1)))) is set

0 .--> U3 is Relation-like NAT -defined {0} -defined Function-like one-to-one Function-yielding V22() set

{0} --> U3 is Relation-like non-empty non empty-yielding {0} -defined {U3} -valued Function-like constant non empty total V18({0},{U3}) Function-yielding V22() Element of K19(K20({0},{U3}))

{U3} is functional non empty set

K20({0},{U3}) is Relation-like set

K19(K20({0},{U3})) is set

(0 .--> U3) . 0 is Relation-like Function-like set

y is V23() V24() V25() V29() V119() V120() ext-real set

((U1,U2,U3) # h) . y is set

(the_arity_of h2) /. y is Element of the carrier of (MSSign U1)

(U1,U2,U3) . ((the_arity_of h2) /. y) is Relation-like the Sorts of (MSAlg U1) . ((the_arity_of h2) /. y) -defined the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ((the_arity_of h2) /. y) -valued Function-like non empty total V18( the Sorts of (MSAlg U1) . ((the_arity_of h2) /. y), the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ((the_arity_of h2) /. y)) Element of K19(K20(( the Sorts of (MSAlg U1) . ((the_arity_of h2) /. y)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ((the_arity_of h2) /. y))))

the Sorts of (MSAlg U1) . ((the_arity_of h2) /. y) is non empty set

the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ((the_arity_of h2) /. y) is non empty set

K20(( the Sorts of (MSAlg U1) . ((the_arity_of h2) /. y)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ((the_arity_of h2) /. y))) is Relation-like set

K19(K20(( the Sorts of (MSAlg U1) . ((the_arity_of h2) /. y)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . ((the_arity_of h2) /. y)))) is set

h . y is set

((U1,U2,U3) . ((the_arity_of h2) /. y)) . (h . y) is set

U3 . (h . y) is set

g is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

g . y is set

dom ((U1,U2,U3) # h) is set

U1 is non empty V91() V92() non-empty UAStr

the carrier of U1 is non empty set

MSSign U1 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign

MSAlg U1 is strict non-empty MSAlgebra over MSSign U1

U2 is non empty V91() V92() non-empty