:: 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₁ where b₁ is Relation-like NAT -defined U2 -valued Function-like V30() FinSequence-like FinSubsequence-like Element of U2 * : len b₁ = U1 } is set
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₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like Element of NAT * : len b₁ = h } is set
(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₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like Element of NAT * : len b₁ = x } is set
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 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
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
the carrier' of (MSSign U1) is non empty set
h is V23() V24() V25() V29() V119() V120() ext-real set
Seg h is V30() V37(h) Element of K19(NAT)
a is Element of the carrier' of (MSSign U1)
Args (a,(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_result_sort_of a is Element of the carrier of (MSSign U1)
(U1,U2,U3) . (the_result_sort_of a) is Relation-like the Sorts of (MSAlg U1) . (the_result_sort_of a) -defined the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of a) -valued Function-like non empty total V18( the Sorts of (MSAlg U1) . (the_result_sort_of a), the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of a)) Element of K19(K20(( the Sorts of (MSAlg U1) . (the_result_sort_of a)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of a))))
the Sorts of (MSAlg U1) . (the_result_sort_of a) is non empty set
the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of a) is non empty set
K20(( the Sorts of (MSAlg U1) . (the_result_sort_of a)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of a))) is Relation-like set
K19(K20(( the Sorts of (MSAlg U1) . (the_result_sort_of a)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of a)))) is set
Den (a,(MSAlg U1)) is Relation-like Args (a,(MSAlg U1)) -defined Result (a,(MSAlg U1)) -valued Function-like non empty total V18( Args (a,(MSAlg U1)), Result (a,(MSAlg U1))) Element of K19(K20((Args (a,(MSAlg U1))),(Result (a,(MSAlg U1)))))
Result (a,(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 (a,(MSAlg U1))),(Result (a,(MSAlg U1)))) is Relation-like set
K19(K20((Args (a,(MSAlg U1))),(Result (a,(MSAlg U1))))) is set
Den (a,((MSSign U1),(MSSign U2),(MSAlg U2))) is Relation-like Args (a,((MSSign U1),(MSSign U2),(MSAlg U2))) -defined Result (a,((MSSign U1),(MSSign U2),(MSAlg U2))) -valued Function-like non empty total V18( Args (a,((MSSign U1),(MSSign U2),(MSAlg U2))), Result (a,((MSSign U1),(MSSign U2),(MSAlg U2)))) Element of K19(K20((Args (a,((MSSign U1),(MSSign U2),(MSAlg U2)))),(Result (a,((MSSign U1),(MSSign U2),(MSAlg U2))))))
Args (a,((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
Result (a,((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 (a,((MSSign U1),(MSSign U2),(MSAlg U2)))),(Result (a,((MSSign U1),(MSSign U2),(MSAlg U2))))) is Relation-like set
K19(K20((Args (a,((MSSign U1),(MSSign U2),(MSAlg U2)))),(Result (a,((MSSign U1),(MSSign U2),(MSAlg U2)))))) is 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
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)) . a is Relation-like ( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . a -defined ( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . a -valued Function-like total V18(( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . a,( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . a) Element of K19(K20((( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . a),(( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . a)))
( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . a is set
( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . a is non empty set
K20((( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . a),(( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . a)) is Relation-like set
K19(K20((( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . a),(( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . a))) is set
(MSCharact U2) . a is Relation-like Function-like set
the charact of U2 . a is set
g is Relation-like the carrier of U2 * -defined the carrier of U2 -valued Function-like non empty V101() V102( the carrier of U2) M16( the carrier of U2, Operations U2)
f is V23() V24() V25() V29() V119() V120() ext-real Element of NAT
the charact of U2 . f is set
y is Relation-like Function-like Element of Args (a,(MSAlg U1))
(Den (a,(MSAlg U1))) . y is set
((U1,U2,U3) . (the_result_sort_of a)) . ((Den (a,(MSAlg U1))) . y) is set
(U1,U2,U3) # y is Relation-like Function-like Element of Args (a,((MSSign U1),(MSSign U2),(MSAlg U2)))
(Den (a,((MSSign U1),(MSSign U2),(MSAlg U2)))) . ((U1,U2,U3) # y) 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 . a 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)
Operations U1 is non empty M15( the carrier of U1)
rng the charact of U1 is set
dom the charact of U1 is Element of K19(NAT)
O1 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 O1 is functional non empty FinSequence-membered Element of K19(( the carrier of U1 *))
K19(( the carrier of U1 *)) is set
O1 . y is set
U3 . (O1 . y) is set
y * U3 is Relation-like the carrier of U2 -valued Function-like set
g . (y * U3) is set
(Den (a,((MSSign U1),(MSSign U2),(MSAlg U2)))) . ((U1,U2,U3) # y) is Element of Result (a,((MSSign U1),(MSSign U2),(MSAlg U2)))
U1 is non empty V91() V92() non-empty UAStr
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)
MSSign U1 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign
the carrier' of (MSSign U1) is non empty 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)
U2 is V23() V24() V25() V29() V119() V120() ext-real 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
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))
MSSign U1 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign
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
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
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
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 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
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
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
(MSSorts U2) . 0 is 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
rng U3 is non empty Element of K19( the carrier of U2)
K19( the carrier of U2) is set
h is set
(U1,U2,U3) . h is Relation-like Function-like set
rng ((U1,U2,U3) . h) is set
the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . h is set
a is Element of the carrier of (MSSign U1)
the Sorts of (MSAlg U1) . a is non empty set
the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . a is non empty set
K20(( the Sorts of (MSAlg U1) . a),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . a)) is Relation-like set
K19(K20(( the Sorts of (MSAlg U1) . a),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . a))) is set
(U1,U2,U3) . 0 is Relation-like Function-like 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
f is Relation-like the Sorts of (MSAlg U1) . a -defined the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . a -valued Function-like non empty total V18( the Sorts of (MSAlg U1) . a, the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . a) Element of K19(K20(( the Sorts of (MSAlg U1) . a),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . a)))
rng f is non empty Element of K19(( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . a))
K19(( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . a)) is set
the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . 0 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 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
dom (U1,U2,U3) is non empty Element of K19( the carrier of (MSSign U1))
K19( the carrier of (MSSign U1)) 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
(U1,U2,U3) . 0 is Relation-like Function-like set
h2 is set
dom (U1,U2,U3) is non empty set
(U1,U2,U3) . h2 is Relation-like Function-like set
h is Relation-like Function-like 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 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
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 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
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
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
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
h is V23() V24() V25() V29() V119() V120() ext-real Element of NAT
the charact of U1 . h is set
the charact of U2 . h is set
the carrier' of (MSSign U1) is non empty set
f 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 f is functional non empty FinSequence-membered Element of K19(( the carrier of U1 *))
K19(( the carrier of U1 *)) is set
g is Relation-like the carrier of U2 * -defined the carrier of U2 -valued Function-like non empty V101() V102( the carrier of U2) M16( the carrier of U2, Operations U2)
a is Element of the carrier' of (MSSign U1)
Den (a,(MSAlg U1)) is Relation-like Args (a,(MSAlg U1)) -defined Result (a,(MSAlg U1)) -valued Function-like non empty total V18( Args (a,(MSAlg U1)), Result (a,(MSAlg U1))) Element of K19(K20((Args (a,(MSAlg U1))),(Result (a,(MSAlg U1)))))
Args (a,(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
Result (a,(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 (a,(MSAlg U1))),(Result (a,(MSAlg U1)))) is Relation-like set
K19(K20((Args (a,(MSAlg U1))),(Result (a,(MSAlg U1))))) is set
x is Relation-like NAT -defined the carrier of U1 -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
f . x is set
U3 . (f . x) is set
K141( the carrier of U1, the carrier of U2,x,U3) is Relation-like NAT -defined the carrier of U2 -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of U2
g . K141( the carrier of U1, the carrier of U2,x,U3) is set
the_result_sort_of a is Element of the carrier of (MSSign U1)
(U1,U2,U3) . (the_result_sort_of a) is Relation-like the Sorts of (MSAlg U1) . (the_result_sort_of a) -defined the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of a) -valued Function-like non empty total V18( the Sorts of (MSAlg U1) . (the_result_sort_of a), the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of a)) Element of K19(K20(( the Sorts of (MSAlg U1) . (the_result_sort_of a)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of a))))
the Sorts of (MSAlg U1) . (the_result_sort_of a) is non empty set
the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of a) is non empty set
K20(( the Sorts of (MSAlg U1) . (the_result_sort_of a)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of a))) is Relation-like set
K19(K20(( the Sorts of (MSAlg U1) . (the_result_sort_of a)),( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) . (the_result_sort_of a)))) is set
y is Relation-like Function-like Element of Args (a,(MSAlg U1))
(Den (a,(MSAlg U1))) . y is Element of Result (a,(MSAlg U1))
((U1,U2,U3) . (the_result_sort_of a)) . ((Den (a,(MSAlg U1))) . y) is set
f . y is set
U3 . (f . y) is set
Args (a,((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
Result (a,((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
Den (a,((MSSign U1),(MSSign U2),(MSAlg U2))) is Relation-like Args (a,((MSSign U1),(MSSign U2),(MSAlg U2))) -defined Result (a,((MSSign U1),(MSSign U2),(MSAlg U2))) -valued Function-like non empty total V18( Args (a,((MSSign U1),(MSSign U2),(MSAlg U2))), Result (a,((MSSign U1),(MSSign U2),(MSAlg U2)))) Element of K19(K20((Args (a,((MSSign U1),(MSSign U2),(MSAlg U2)))),(Result (a,((MSSign U1),(MSSign U2),(MSAlg U2))))))
K20((Args (a,((MSSign U1),(MSSign U2),(MSAlg U2)))),(Result (a,((MSSign U1),(MSSign U2),(MSAlg U2))))) is Relation-like set
K19(K20((Args (a,((MSSign U1),(MSSign U2),(MSAlg U2)))),(Result (a,((MSSign U1),(MSSign U2),(MSAlg U2)))))) is set
(U1,U2,U3) # y is Relation-like Function-like Element of Args (a,((MSSign U1),(MSSign U2),(MSAlg U2)))
(Den (a,((MSSign U1),(MSSign U2),(MSAlg U2)))) . ((U1,U2,U3) # y) is Element of Result (a,((MSSign U1),(MSSign U2),(MSAlg U2)))
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
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)) . a is Relation-like ( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . a -defined ( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . a -valued Function-like total V18(( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . a,( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . a) Element of K19(K20((( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . a),(( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . a)))
( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . a is set
( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . a is non empty set
K20((( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . a),(( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . a)) is Relation-like set
K19(K20((( the Arity of (MSSign U1) * ( the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2)) #)) . a),(( the ResultSort of (MSSign U1) * the Sorts of ((MSSign U1),(MSSign U2),(MSAlg U2))) . a))) is set
(MSCharact U2) . a is Relation-like Function-like 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 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
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
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
(MSSorts U2) . 0 is 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) is Relation-like non-empty non empty-yielding the carrier of (MSSign U2) -defined Function-like non empty total set
(U1,U2,U3) . 0 is Relation-like Function-like 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
rng U3 is non empty Element of K19( the carrier of U2)
K19( the carrier of U2) 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 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
(U1,U2,U3) . 0 is Relation-like Function-like 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
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 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
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 V12() V30() set
the carrier of U1 is non empty set
id the carrier of U1 is Relation-like the carrier of U1 -defined the carrier of U1 -valued Function-like one-to-one 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
(U1,U1,(id the carrier of U1)) 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 U1),(MSAlg U1))
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
((MSSign U1),(MSSign U1),(MSAlg U1)) is strict non-empty MSAlgebra over MSSign U1
the Sorts of ((MSSign U1),(MSSign U1),(MSAlg U1)) is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set
id the Sorts of (MSAlg U1) 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 (MSAlg U1)
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
h1 is Relation-like {0} -defined Function-like non empty total set
h1 . 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
h2 is set
(id the Sorts of (MSAlg U1)) . 0 is Relation-like Function-like set
0 .--> (id the carrier of U1) is Relation-like NAT -defined {0} -defined Function-like one-to-one Function-yielding V22() set
{0} --> (id the carrier of U1) is Relation-like non-empty non empty-yielding {0} -defined {(id the carrier of U1)} -valued Function-like constant non empty total V18({0},{(id the carrier of U1)}) Function-yielding V22() Element of K19(K20({0},{(id the carrier of U1)}))
{(id the carrier of U1)} is functional non empty set
K20({0},{(id the carrier of U1)}) is Relation-like set
K19(K20({0},{(id the carrier of U1)})) is set
(U1,U1,(id the carrier of U1)) . 0 is Relation-like Function-like set
h2 is set
(id the Sorts of (MSAlg U1)) . h2 is Relation-like Function-like set
(U1,U1,(id the carrier of U1)) . h2 is Relation-like Function-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
U3 is non empty V91() V92() non-empty UAStr
the carrier of U3 is non empty set
K20( the carrier of U2, the carrier of U3) is Relation-like set
K19(K20( the carrier of U2, the carrier of U3)) is set
h1 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,h1) 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))
MSSign U1 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign
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
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
h2 is Relation-like the carrier of U2 -defined the carrier of U3 -valued Function-like non empty total V18( the carrier of U2, the carrier of U3) Element of K19(K20( the carrier of U2, the carrier of U3))
(U2,U3,h2) is Relation-like the carrier of (MSSign U2) -defined Function-like non empty total Function-yielding V22() ManySortedFunction of the Sorts of (MSAlg U2), the Sorts of ((MSSign U2),(MSSign U3),(MSAlg U3))
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
MSSign U3 is non empty V60() V61() non void 1 -element V67() strict segmental ManySortedSign
MSAlg U3 is strict non-empty MSAlgebra over MSSign U3
((MSSign U2),(MSSign U3),(MSAlg U3)) is strict non-empty MSAlgebra over MSSign U2
the Sorts of ((MSSign U2),(MSSign U3),(MSAlg U3)) is Relation-like non-empty non empty-yielding the carrier of (MSSign U2) -defined Function-like non empty total set
(U2,U3,h2) ** (U1,U2,h1) is Relation-like Function-like Function-yielding V22() set
h2 * h1 is Relation-like the carrier of U1 -defined the carrier of U3 -valued Function-like non empty total V18( the carrier of U1, the carrier of U3) Element of K19(K20( the carrier of U1, the carrier of U3))
K20( the carrier of U1, the carrier of U3) is Relation-like set
K19(K20( the carrier of U1, the carrier of U3)) is set
(U1,U3,(h2 * h1)) 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 U3),(MSAlg U3))
((MSSign U1),(MSSign U3),(MSAlg U3)) is strict non-empty MSAlgebra over MSSign U1
the Sorts of ((MSSign U1),(MSSign U3),(MSAlg U3)) is Relation-like non-empty non empty-yielding the carrier of (MSSign U1) -defined Function-like non empty total set
dom (U2,U3,h2) is non empty Element of K19( the carrier of (MSSign U2))
K19( the carrier of (MSSign U2)) is set
dom ((U2,U3,h2) ** (U1,U2,h1)) is set
dom (U1,U2,h1) is non empty Element of K19( the carrier of (MSSign U1))
K19( the carrier of (MSSign U1)) is set
(dom (U1,U2,h1)) /\ (dom (U2,U3,h2)) is Element of K19( the carrier of (MSSign U2))
{0} /\ {0} is set
h is set
a is Relation-like Function-like set
(U1,U2,h1) . h is Relation-like Function-like set
f is Relation-like Function-like set
(U2,U3,h2) . h is Relation-like Function-like set
(U2,U3,h2) . 0 is Relation-like Function-like set
0 .--> h2 is Relation-like NAT -defined {0} -defined Function-like one-to-one Function-yielding V22() set
{0} --> h2 is Relation-like non-empty non empty-yielding {0} -defined {h2} -valued Function-like constant non empty total V18({0},{h2}) Function-yielding V22() Element of K19(K20({0},{h2}))
{h2} is functional non empty set
K20({0},{h2}) is Relation-like set
K19(K20({0},{h2})) is set
(0 .--> h2) . 0 is Relation-like Function-like set
(U1,U2,h1) . 0 is Relation-like Function-like set
0 .--> h1 is Relation-like NAT -defined {0} -defined Function-like one-to-one Function-yielding V22() set
{0} --> h1 is Relation-like non-empty non empty-yielding {0} -defined {h1} -valued Function-like constant non empty total V18({0},{h1}) Function-yielding V22() Element of K19(K20({0},{h1}))
{h1} is functional non empty set
K20({0},{h1}) is Relation-like set
K19(K20({0},{h1})) is set
(0 .--> h1) . 0 is Relation-like Function-like set
((U2,U3,h2) ** (U1,U2,h1)) . h is Relation-like Function-like set
a is set
dom (U1,U3,(h2 * h1)) is non empty Element of K19( the carrier of (MSSign U1))
(U1,U3,(h2 * h1)) . 0 is Relation-like Function-like set
0 .--> (h2 * h1) is Relation-like NAT -defined {0} -defined Function-like one-to-one Function-yielding V22() set
{0} --> (h2 * h1) is Relation-like non-empty non empty-yielding {0} -defined {(h2 * h1)} -valued Function-like constant non empty total V18({0},{(h2 * h1)}) Function-yielding V22() Element of K19(K20({0},{(h2 * h1)}))
{(h2 * h1)} is functional non empty set
K20({0},{(h2 * h1)}) is Relation-like set
K19(K20({0},{(h2 * h1)})) is set
(0 .--> (h2 * h1)) . 0 is Relation-like Function-like set
(U1,U3,(h2 * h1)) . a is Relation-like Function-like set
a is set
f is Relation-like Function-like set
(U1,U2,h1) . a is Relation-like Function-like set
g is Relation-like Function-like set
(U2,U3,h2) . a is Relation-like Function-like set
(U1,U3,(h2 * h1)) . a is Relation-like Function-like set
((U2,U3,h2) ** (U1,U2,h1)) . a is Relation-like Function-like set
a is set
((U2,U3,h2) ** (U1,U2,h1)) . a is Relation-like Function-like set
(U1,U3,(h2 * h1)) . a is Relation-like Function-like set
(U1,U2,h1) . a is Relation-like Function-like set
(U2,U3,h2) . a is Relation-like Function-like set