REAL is set
NAT is non empty V26() V27() V28() Element of K19(REAL)
K19(REAL) is set
NAT is non empty V26() V27() V28() set
K19(NAT) is set
K19(NAT) is set
BOOLEAN is non empty set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain set
1 is non empty V26() V27() V28() V32() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain Element of NAT
2 is non empty V26() V27() V28() V32() Element of NAT
3 is non empty V26() V27() V28() V32() 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 quasi_total Function-yielding V25() Element of K19(K20(NAT,({0} *)))
K20(NAT,({0} *)) is Relation-like set
K19(K20(NAT,({0} *))) is set
z is set
{z} is non empty set
{z} * is functional non empty FinSequence-membered FinSequenceSet of {z}
*--> z is Relation-like NAT -defined {z} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20(NAT,({z} *)))
K20(NAT,({z} *)) is Relation-like set
K19(K20(NAT,({z} *))) is set
(*--> z) . 0 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of {z} *
0 |-> z is Relation-like NAT -defined Function-like V33() V40( 0 ) FinSequence-like FinSubsequence-like set
Seg 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() V40( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain Element of K19(NAT)
(Seg 0) --> z is Relation-like non-empty empty-yielding Seg 0 -defined Seg 0 -defined {z} -valued Function-like one-to-one constant functional empty total total quasi_total Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain Element of K19(K20((Seg 0),{z}))
K20((Seg 0),{z}) is Relation-like set
K19(K20((Seg 0),{z})) is set
z is set
{z} is non empty set
{z} * is functional non empty FinSequence-membered FinSequenceSet of {z}
*--> z is Relation-like NAT -defined {z} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20(NAT,({z} *)))
K20(NAT,({z} *)) is Relation-like set
K19(K20(NAT,({z} *))) is set
(*--> z) . 1 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of {z} *
<*z*> is Relation-like NAT -defined Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like set
1 |-> z is Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
Seg 1 is non empty V33() V40(1) Element of K19(NAT)
(Seg 1) --> z is Relation-like Seg 1 -defined Seg 1 -defined {z} -valued Function-like constant non empty total total quasi_total V33() FinSequence-like FinSubsequence-like Element of K19(K20((Seg 1),{z}))
K20((Seg 1),{z}) is Relation-like set
K19(K20((Seg 1),{z})) is set
z is set
{z} is non empty set
{z} * is functional non empty FinSequence-membered FinSequenceSet of {z}
*--> z is Relation-like NAT -defined {z} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20(NAT,({z} *)))
K20(NAT,({z} *)) is Relation-like set
K19(K20(NAT,({z} *))) is set
(*--> z) . 2 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of {z} *
<*z,z*> is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like set
2 |-> z is Relation-like NAT -defined Function-like V33() V40(2) FinSequence-like FinSubsequence-like set
Seg 2 is non empty V33() V40(2) Element of K19(NAT)
(Seg 2) --> z is Relation-like Seg 2 -defined Seg 2 -defined {z} -valued Function-like constant non empty total total quasi_total V33() FinSequence-like FinSubsequence-like Element of K19(K20((Seg 2),{z}))
K20((Seg 2),{z}) is Relation-like set
K19(K20((Seg 2),{z})) is set
z is set
{z} is non empty set
{z} * is functional non empty FinSequence-membered FinSequenceSet of {z}
*--> z is Relation-like NAT -defined {z} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20(NAT,({z} *)))
K20(NAT,({z} *)) is Relation-like set
K19(K20(NAT,({z} *))) is set
(*--> z) . 3 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of {z} *
<*z,z,z*> is Relation-like NAT -defined Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like set
3 |-> z is Relation-like NAT -defined Function-like V33() V40(3) FinSequence-like FinSubsequence-like set
Seg 3 is non empty V33() V40(3) Element of K19(NAT)
(Seg 3) --> z is Relation-like Seg 3 -defined Seg 3 -defined {z} -valued Function-like constant non empty total total quasi_total V33() FinSequence-like FinSubsequence-like Element of K19(K20((Seg 3),{z}))
K20((Seg 3),{z}) is Relation-like set
K19(K20((Seg 3),{z})) is set
z is V26() V27() V28() V32() set
z |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V33() V40(z) FinSequence-like FinSubsequence-like Element of z -tuples_on NAT
z -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = z } is set
Seg z is V33() V40(z) Element of K19(NAT)
(Seg z) --> 0 is Relation-like Seg z -defined Seg z -defined NAT -valued {0} -valued Function-like constant total total quasi_total Function-yielding V25() V33() FinSequence-like FinSubsequence-like Element of K19(K20((Seg z),{0}))
K20((Seg z),{0}) is Relation-like set
K19(K20((Seg z),{0})) is set
Z is Relation-like NAT -defined {0} -valued Function-like Function-yielding V25() V33() FinSequence-like FinSubsequence-like FinSequence of {0}
len Z is V26() V27() V28() V32() Element of NAT
dom Z is Element of K19(NAT)
0 |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V33() V40( 0 ) FinSequence-like FinSubsequence-like Element of 0 -tuples_on NAT
0 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = 0 } is set
Seg 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() V40( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain Element of K19(NAT)
(Seg 0) --> 0 is Relation-like non-empty empty-yielding Seg 0 -defined Seg 0 -defined NAT -valued {0} -valued Function-like one-to-one constant functional empty total total quasi_total Function-yielding V25() V26() V27() V28() V30() V31() V32() V33() FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain Element of K19(K20((Seg 0),{0}))
K20((Seg 0),{0}) is Relation-like set
K19(K20((Seg 0),{0})) is set
rng Z is set
z is V26() V27() V28() V32() set
(*--> 0) . z is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
Z is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len Z is V26() V27() V28() V32() Element of NAT
z |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V33() V40(z) FinSequence-like FinSubsequence-like Element of z -tuples_on NAT
z -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = z } is set
Seg z is V33() V40(z) Element of K19(NAT)
(Seg z) --> 0 is Relation-like Seg z -defined Seg z -defined NAT -valued {0} -valued Function-like constant total total quasi_total Function-yielding V25() V33() FinSequence-like FinSubsequence-like Element of K19(K20((Seg z),{0}))
K20((Seg z),{0}) is Relation-like set
K19(K20((Seg z),{0})) is set
Z is non empty partial quasi_total non-empty UAStr
A is non empty partial quasi_total non-empty UAStr
MSSign Z is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSSign A is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
signature Z is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
dom (signature Z) is Element of K19(NAT)
z is Relation-like Function-like Element of {0}
(dom (signature Z)) --> z is Relation-like dom (signature Z) -defined {0} -valued Function-like constant total quasi_total Function-yielding V25() Element of K19(K20((dom (signature Z)),{0}))
K20((dom (signature Z)),{0}) is Relation-like set
K19(K20((dom (signature Z)),{0})) is set
{z} is functional non empty set
K20((dom (signature Z)),{z}) is Relation-like set
signature A is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
dom (signature A) is Element of K19(NAT)
(dom (signature A)) --> z is Relation-like dom (signature A) -defined {0} -valued Function-like constant total quasi_total Function-yielding V25() Element of K19(K20((dom (signature A)),{0}))
K20((dom (signature A)),{0}) is Relation-like set
K19(K20((dom (signature A)),{0})) is set
K20((dom (signature A)),{z}) is Relation-like set
K20((dom (signature Z)),({0} *)) is Relation-like set
K19(K20((dom (signature Z)),({0} *))) is set
(*--> 0) * (signature Z) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V25() Element of K19(K20(NAT,({0} *)))
K20((dom (signature A)),({0} *)) is Relation-like set
K19(K20((dom (signature A)),({0} *))) is set
(*--> 0) * (signature A) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V25() Element of K19(K20(NAT,({0} *)))
f is Relation-like dom (signature Z) -defined {0} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20((dom (signature Z)),({0} *)))
ManySortedSign(# {0},(dom (signature Z)),f,((dom (signature Z)) --> z) #) is non empty V70() strict ManySortedSign
f is Relation-like dom (signature A) -defined {0} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20((dom (signature A)),({0} *)))
ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is non empty V70() strict ManySortedSign
the carrier' of (MSSign Z) is non empty set
the carrier' of (MSSign A) is non empty set
Z is non empty partial quasi_total non-empty UAStr
A is non empty partial quasi_total non-empty UAStr
MSSign A is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
the carrier of (MSSign A) is non empty trivial V33() set
MSAlg A is strict non-empty MSAlgebra over MSSign A
the Sorts of (MSAlg A) is Relation-like non-empty non empty-yielding the carrier of (MSSign A) -defined Function-like non empty total set
MSSign Z is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSAlg Z is strict non-empty MSAlgebra over MSSign Z
the Sorts of (MSAlg Z) is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the carrier of (MSSign Z) is non empty trivial V33() set
the carrier' of (MSSign A) is non empty set
the carrier' of (MSSign Z) is non empty set
ff1 is Relation-like the carrier of (MSSign A) -defined Function-like non empty total ManySortedSubset of the Sorts of (MSAlg A)
f is Element of the carrier' of (MSSign A)
Args (f,(MSAlg A)) is non empty Element of rng ( the Sorts of (MSAlg A) #)
the Sorts of (MSAlg A) # is Relation-like non-empty non empty-yielding the carrier of (MSSign A) * -defined Function-like non empty total set
the carrier of (MSSign A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign A)
rng ( the Sorts of (MSAlg A) #) is non empty V45() set
Result (f,(MSAlg A)) is non empty Element of rng the Sorts of (MSAlg A)
rng the Sorts of (MSAlg A) is non empty V45() set
Den (f,(MSAlg A)) is Relation-like Args (f,(MSAlg A)) -defined Result (f,(MSAlg A)) -valued Function-like quasi_total Element of K19(K20((Args (f,(MSAlg A))),(Result (f,(MSAlg A)))))
K20((Args (f,(MSAlg A))),(Result (f,(MSAlg A)))) is Relation-like set
K19(K20((Args (f,(MSAlg A))),(Result (f,(MSAlg A))))) is set
f is Element of the carrier' of (MSSign Z)
Args (f,(MSAlg Z)) is non empty Element of rng ( the Sorts of (MSAlg Z) #)
the Sorts of (MSAlg Z) # is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) * -defined Function-like non empty total set
the carrier of (MSSign Z) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign Z)
rng ( the Sorts of (MSAlg Z) #) is non empty V45() set
Den (f,(MSAlg Z)) is Relation-like Args (f,(MSAlg Z)) -defined Result (f,(MSAlg Z)) -valued Function-like quasi_total Element of K19(K20((Args (f,(MSAlg Z))),(Result (f,(MSAlg Z)))))
Result (f,(MSAlg Z)) is non empty Element of rng the Sorts of (MSAlg Z)
rng the Sorts of (MSAlg Z) is non empty V45() set
K20((Args (f,(MSAlg Z))),(Result (f,(MSAlg Z)))) is Relation-like set
K19(K20((Args (f,(MSAlg Z))),(Result (f,(MSAlg Z))))) is set
dom (Den (f,(MSAlg Z))) is set
the Arity of (MSSign Z) is Relation-like the carrier' of (MSSign Z) -defined the carrier of (MSSign Z) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *)))
K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *)) is Relation-like set
K19(K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *))) is set
ff1 # is Relation-like the carrier of (MSSign A) * -defined Function-like non empty total set
the Arity of (MSSign Z) * (ff1 #) is Relation-like the carrier' of (MSSign Z) -defined Function-like set
( the Arity of (MSSign Z) * (ff1 #)) . f is set
the Arity of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)))
K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)) is Relation-like set
K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *))) is set
the Arity of (MSSign A) * ( the Sorts of (MSAlg A) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign A) -defined Function-like non empty total set
( the Arity of (MSSign A) * ( the Sorts of (MSAlg A) #)) . f is non empty set
dom (Den (f,(MSAlg A))) is set
(Den (f,(MSAlg A))) | (Args (f,(MSAlg Z))) is Relation-like Args (f,(MSAlg A)) -defined Args (f,(MSAlg Z)) -defined Args (f,(MSAlg A)) -defined Result (f,(MSAlg A)) -valued Function-like Element of K19(K20((Args (f,(MSAlg A))),(Result (f,(MSAlg A)))))
dom ((Den (f,(MSAlg A))) | (Args (f,(MSAlg Z)))) is set
(dom (Den (f,(MSAlg A)))) /\ (Args (f,(MSAlg Z))) is set
MSSorts Z is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
MSCharact Z is Relation-like the carrier' of (MSSign Z) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign Z) * ((MSSorts Z) #), the ResultSort of (MSSign Z) * (MSSorts Z)
(MSSorts Z) # is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) * -defined Function-like non empty total set
the Arity of (MSSign Z) * ((MSSorts Z) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign Z) -defined Function-like non empty total set
the ResultSort of (MSSign Z) is Relation-like the carrier' of (MSSign Z) -defined the carrier of (MSSign Z) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign Z), the carrier of (MSSign Z)))
K20( the carrier' of (MSSign Z), the carrier of (MSSign Z)) is Relation-like set
K19(K20( the carrier' of (MSSign Z), the carrier of (MSSign Z))) is set
the ResultSort of (MSSign Z) * (MSSorts Z) is Relation-like non-empty non empty-yielding the carrier' of (MSSign Z) -defined Function-like non empty total set
MSAlgebra(# (MSSorts Z),(MSCharact Z) #) is strict MSAlgebra over MSSign Z
the carrier of Z is non empty set
0 .--> the carrier of Z is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> the carrier of Z is Relation-like non-empty non empty-yielding {0} -defined { the carrier of Z} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{ the carrier of Z}))
{ the carrier of Z} is non empty set
K20({0},{ the carrier of Z}) is Relation-like set
K19(K20({0},{ the carrier of Z})) is set
the carrier of A is non empty set
K19( the carrier of A) is set
C is set
(Den (f,(MSAlg A))) . C is set
(Den (f,(MSAlg Z))) . C is set
MSSorts A is Relation-like non-empty non empty-yielding the carrier of (MSSign A) -defined Function-like non empty total set
MSCharact A is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign A) * ((MSSorts A) #), the ResultSort of (MSSign A) * (MSSorts A)
(MSSorts A) # is Relation-like non-empty non empty-yielding the carrier of (MSSign A) * -defined Function-like non empty total set
the Arity of (MSSign A) * ((MSSorts A) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign A) -defined Function-like non empty total set
the ResultSort of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A)))
K20( the carrier' of (MSSign A), the carrier of (MSSign A)) is Relation-like set
K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A))) is set
the ResultSort of (MSSign A) * (MSSorts A) is Relation-like non-empty non empty-yielding the carrier' of (MSSign A) -defined Function-like non empty total set
MSAlgebra(# (MSSorts A),(MSCharact A) #) is strict MSAlgebra over MSSign A
signature Z is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
signature A is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
the_arity_of f is Relation-like NAT -defined the carrier of (MSSign Z) -valued Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of (MSSign Z) *
len (the_arity_of f) is V26() V27() V28() V32() Element of NAT
the_sort_of (MSAlg Z) is non empty set
(len (the_arity_of f)) -tuples_on (the_sort_of (MSAlg Z)) is functional non empty FinSequence-membered FinSequenceSet of the_sort_of (MSAlg Z)
(the_sort_of (MSAlg Z)) * is functional non empty FinSequence-membered FinSequenceSet of the_sort_of (MSAlg Z)
{ b1 where b1 is Relation-like NAT -defined the_sort_of (MSAlg Z) -valued Function-like V33() FinSequence-like FinSubsequence-like Element of (the_sort_of (MSAlg Z)) * : len b1 = len (the_arity_of f) } is set
(len (the_arity_of f)) -tuples_on the carrier of Z is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
{ b1 where b1 is Relation-like NAT -defined the carrier of Z -valued Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of Z * : len b1 = len (the_arity_of f) } is set
dom (signature A) is Element of K19(NAT)
K20((dom (signature A)),({0} *)) is Relation-like set
K19(K20((dom (signature A)),({0} *))) is set
(*--> 0) * (signature A) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V25() Element of K19(K20(NAT,({0} *)))
(*--> 0) * (signature Z) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V25() Element of K19(K20(NAT,({0} *)))
dom (signature Z) is Element of K19(NAT)
z is Relation-like Function-like Element of {0}
(dom (signature Z)) --> z is Relation-like dom (signature Z) -defined {0} -valued Function-like constant total quasi_total Function-yielding V25() Element of K19(K20((dom (signature Z)),{0}))
K20((dom (signature Z)),{0}) is Relation-like set
K19(K20((dom (signature Z)),{0})) is set
{z} is functional non empty set
K20((dom (signature Z)),{z}) is Relation-like set
(dom (signature A)) --> z is Relation-like dom (signature A) -defined {0} -valued Function-like constant total quasi_total Function-yielding V25() Element of K19(K20((dom (signature A)),{0}))
K20((dom (signature A)),{0}) is Relation-like set
K19(K20((dom (signature A)),{0})) is set
K20((dom (signature A)),{z}) is Relation-like set
K20((dom (signature Z)),({0} *)) is Relation-like set
K19(K20((dom (signature Z)),({0} *))) is set
A4 is V26() V27() V28() V32() set
Seg A4 is V33() V40(A4) Element of K19(NAT)
y is Relation-like dom (signature A) -defined {0} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20((dom (signature A)),({0} *)))
ManySortedSign(# {0},(dom (signature A)),y,((dom (signature A)) --> z) #) is non empty V70() strict ManySortedSign
the charact of A is Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of A *), the carrier of A)
the carrier of A * is functional non empty FinSequence-membered FinSequenceSet of the carrier of A
PFuncs (( the carrier of A *), the carrier of A) is set
dom the charact of A is non empty Element of K19(NAT)
len the charact of A is V26() V27() V28() V32() Element of NAT
Seg (len the charact of A) is V33() V40( len the charact of A) Element of K19(NAT)
len (signature A) is V26() V27() V28() V32() Element of NAT
Seg (len (signature A)) is V33() V40( len (signature A)) Element of K19(NAT)
Operations A is non empty PFuncsDomHQN of the carrier of A
rng the charact of A is non empty V45() set
the charact of A . f is Relation-like Function-like homogeneous set
rng (signature Z) is set
g1 is V26() V27() V28() V32() Element of NAT
(signature Z) . g1 is set
dom (*--> 0) is set
g2 is Relation-like dom (signature Z) -defined {0} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20((dom (signature Z)),({0} *)))
ManySortedSign(# {0},(dom (signature Z)),g2,((dom (signature Z)) --> z) #) is non empty V70() strict ManySortedSign
dom ((*--> 0) * (signature Z)) is set
the Arity of (MSSign Z) . g1 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(*--> 0) . ((signature Z) . g1) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
A3 is V26() V27() V28() V32() Element of NAT
A3 |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V33() V40(A3) FinSequence-like FinSubsequence-like Element of A3 -tuples_on NAT
A3 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = A3 } is set
Seg A3 is V33() V40(A3) Element of K19(NAT)
(Seg A3) --> 0 is Relation-like Seg A3 -defined Seg A3 -defined NAT -valued {0} -valued Function-like constant total total quasi_total Function-yielding V25() V33() FinSequence-like FinSubsequence-like Element of K19(K20((Seg A3),{0}))
K20((Seg A3),{0}) is Relation-like set
K19(K20((Seg A3),{0})) is set
g4 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len g4 is V26() V27() V28() V32() Element of NAT
(len g4) -tuples_on the carrier of Z is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
{ b1 where b1 is Relation-like NAT -defined the carrier of Z -valued Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of Z * : len b1 = len g4 } is set
A3 -tuples_on the carrier of Z is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
{ b1 where b1 is Relation-like NAT -defined the carrier of Z -valued Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of Z * : len b1 = A3 } is set
g3 is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of Operations A
arity g3 is V26() V27() V28() V32() Element of NAT
(arity g3) -tuples_on the carrier of Z is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
{ b1 where b1 is Relation-like NAT -defined the carrier of Z -valued Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of Z * : len b1 = arity g3 } is set
f is set
y is non empty Element of K19( the carrier of A)
Opers (A,y) is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)
y * is functional non empty FinSequence-membered FinSequenceSet of y
PFuncs ((y *),y) is set
dom (Opers (A,y)) is Element of K19(NAT)
rng (Opers (A,y)) is set
(Opers (A,y)) . f is set
a is Element of the carrier' of (MSSign Z)
Den (a,(MSAlg Z)) is Relation-like Args (a,(MSAlg Z)) -defined Result (a,(MSAlg Z)) -valued Function-like quasi_total Element of K19(K20((Args (a,(MSAlg Z))),(Result (a,(MSAlg Z)))))
Args (a,(MSAlg Z)) is non empty Element of rng ( the Sorts of (MSAlg Z) #)
Result (a,(MSAlg Z)) is non empty Element of rng the Sorts of (MSAlg Z)
K20((Args (a,(MSAlg Z))),(Result (a,(MSAlg Z)))) is Relation-like set
K19(K20((Args (a,(MSAlg Z))),(Result (a,(MSAlg Z))))) is set
(Den (a,(MSAlg Z))) . C is set
(MSCharact Z) . f is Relation-like Function-like set
((MSCharact Z) . f) . C is set
the charact of Z is Relation-like non-empty NAT -defined PFuncs (( the carrier of Z *), the carrier of Z) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of Z *), the carrier of Z)
PFuncs (( the carrier of Z *), the carrier of Z) is set
the charact of Z . f is Relation-like Function-like homogeneous set
( the charact of Z . f) . C is set
f is Relation-like Function-like Function-yielding V25() set
f . f is Relation-like Function-like set
(f . f) . C is set
g3 /. y is Relation-like y * -defined y -valued Function-like non empty homogeneous quasi_total Element of K19(K20((y *),y))
K20((y *),y) is Relation-like set
K19(K20((y *),y)) is set
(g3 /. y) . C is set
(arity g3) -tuples_on y is functional non empty FinSequence-membered FinSequenceSet of y
{ b1 where b1 is Relation-like NAT -defined y -valued Function-like V33() FinSequence-like FinSubsequence-like Element of y * : len b1 = arity g3 } is set
g3 | ((arity g3) -tuples_on y) is Relation-like the carrier of A * -defined (arity g3) -tuples_on y -defined the carrier of A * -defined the carrier of A -valued Function-like Element of K19(K20(( the carrier of A *), the carrier of A))
K20(( the carrier of A *), the carrier of A) is Relation-like set
K19(K20(( the carrier of A *), the carrier of A)) is set
(g3 | ((arity g3) -tuples_on y)) . C is set
the charact of A . f is Relation-like Function-like homogeneous set
( the charact of A . f) . C is set
the Charact of (MSAlg A) is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign A) * ( the Sorts of (MSAlg A) #), the ResultSort of (MSSign A) * the Sorts of (MSAlg A)
the ResultSort of (MSSign A) * the Sorts of (MSAlg A) is Relation-like non-empty non empty-yielding the carrier' of (MSSign A) -defined Function-like non empty total set
the Charact of (MSAlg A) . f is Relation-like Function-like set
( the Charact of (MSAlg A) . f) . C is set
y is Element of the carrier' of (MSSign Z)
Den (y,(MSAlg Z)) is Relation-like Args (y,(MSAlg Z)) -defined Result (y,(MSAlg Z)) -valued Function-like quasi_total Element of K19(K20((Args (y,(MSAlg Z))),(Result (y,(MSAlg Z)))))
Args (y,(MSAlg Z)) is non empty Element of rng ( the Sorts of (MSAlg Z) #)
Result (y,(MSAlg Z)) is non empty Element of rng the Sorts of (MSAlg Z)
K20((Args (y,(MSAlg Z))),(Result (y,(MSAlg Z)))) is Relation-like set
K19(K20((Args (y,(MSAlg Z))),(Result (y,(MSAlg Z))))) is set
(Den (f,(MSAlg A))) | (Args (y,(MSAlg Z))) is Relation-like Args (f,(MSAlg A)) -defined Args (y,(MSAlg Z)) -defined Args (f,(MSAlg A)) -defined Result (f,(MSAlg A)) -valued Function-like Element of K19(K20((Args (f,(MSAlg A))),(Result (f,(MSAlg A)))))
Z is non empty partial quasi_total non-empty UAStr
A is non empty partial quasi_total non-empty UAStr
MSSign Z is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSAlg Z is strict non-empty MSAlgebra over MSSign Z
the Sorts of (MSAlg Z) is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the carrier of (MSSign Z) is non empty trivial V33() set
MSSign A is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
the carrier of (MSSign A) is non empty trivial V33() set
MSAlg A is strict non-empty MSAlgebra over MSSign A
the Sorts of (MSAlg A) is Relation-like non-empty non empty-yielding the carrier of (MSSign A) -defined Function-like non empty total set
signature A is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(*--> 0) * (signature A) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V25() Element of K19(K20(NAT,({0} *)))
dom (signature A) is Element of K19(NAT)
z is Relation-like Function-like Element of {0}
(dom (signature A)) --> z is Relation-like dom (signature A) -defined {0} -valued Function-like constant total quasi_total Function-yielding V25() Element of K19(K20((dom (signature A)),{0}))
K20((dom (signature A)),{0}) is Relation-like set
K19(K20((dom (signature A)),{0})) is set
{z} is functional non empty set
K20((dom (signature A)),{z}) is Relation-like set
K20((dom (signature A)),({0} *)) is Relation-like set
K19(K20((dom (signature A)),({0} *))) is set
f is Relation-like dom (signature A) -defined {0} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20((dom (signature A)),({0} *)))
ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is non empty V70() strict ManySortedSign
MSSorts A is Relation-like non-empty non empty-yielding the carrier of (MSSign A) -defined Function-like non empty total set
MSCharact A is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign A) * ((MSSorts A) #), the ResultSort of (MSSign A) * (MSSorts A)
the carrier' of (MSSign A) is non empty set
the Arity of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)))
the carrier of (MSSign A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign A)
K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)) is Relation-like set
K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *))) is set
(MSSorts A) # is Relation-like non-empty non empty-yielding the carrier of (MSSign A) * -defined Function-like non empty total set
the Arity of (MSSign A) * ((MSSorts A) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign A) -defined Function-like non empty total set
the ResultSort of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A)))
K20( the carrier' of (MSSign A), the carrier of (MSSign A)) is Relation-like set
K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A))) is set
the ResultSort of (MSSign A) * (MSSorts A) is Relation-like non-empty non empty-yielding the carrier' of (MSSign A) -defined Function-like non empty total set
MSAlgebra(# (MSSorts A),(MSCharact A) #) is strict MSAlgebra over MSSign A
the carrier of A is non empty set
0 .--> the carrier of A is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> the carrier of A is Relation-like non-empty non empty-yielding {0} -defined { the carrier of A} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{ the carrier of A}))
{ the carrier of A} is non empty set
K20({0},{ the carrier of A}) is Relation-like set
K19(K20({0},{ the carrier of A})) is set
MSSorts Z is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
MSCharact Z is Relation-like the carrier' of (MSSign Z) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign Z) * ((MSSorts Z) #), the ResultSort of (MSSign Z) * (MSSorts Z)
the carrier' of (MSSign Z) is non empty set
the Arity of (MSSign Z) is Relation-like the carrier' of (MSSign Z) -defined the carrier of (MSSign Z) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *)))
the carrier of (MSSign Z) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign Z)
K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *)) is Relation-like set
K19(K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *))) is set
(MSSorts Z) # is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) * -defined Function-like non empty total set
the Arity of (MSSign Z) * ((MSSorts Z) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign Z) -defined Function-like non empty total set
the ResultSort of (MSSign Z) is Relation-like the carrier' of (MSSign Z) -defined the carrier of (MSSign Z) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign Z), the carrier of (MSSign Z)))
K20( the carrier' of (MSSign Z), the carrier of (MSSign Z)) is Relation-like set
K19(K20( the carrier' of (MSSign Z), the carrier of (MSSign Z))) is set
the ResultSort of (MSSign Z) * (MSSorts Z) is Relation-like non-empty non empty-yielding the carrier' of (MSSign Z) -defined Function-like non empty total set
MSAlgebra(# (MSSorts Z),(MSCharact Z) #) is strict MSAlgebra over MSSign Z
f is non-empty MSAlgebra over MSSign A
the Sorts of f is Relation-like non-empty non empty-yielding the carrier of (MSSign A) -defined Function-like non empty total set
the carrier of Z is non empty set
0 .--> the carrier of Z is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> the carrier of Z is Relation-like non-empty non empty-yielding {0} -defined { the carrier of Z} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{ the carrier of Z}))
{ the carrier of Z} is non empty set
K20({0},{ the carrier of Z}) is Relation-like set
K19(K20({0},{ the carrier of Z})) is set
K19( the carrier of A) is set
x is set
the Sorts of f . x is set
the Sorts of (MSAlg A) . x is set
the Sorts of f . 0 is set
the Sorts of (MSAlg A) . 0 is set
Z is non empty partial quasi_total non-empty UAStr
A is non empty partial quasi_total non-empty UAStr
MSSign A is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
the carrier of (MSSign A) is non empty trivial V33() set
MSAlg A is strict non-empty MSAlgebra over MSSign A
the Sorts of (MSAlg A) is Relation-like non-empty non empty-yielding the carrier of (MSSign A) -defined Function-like non empty total set
MSSign Z is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSAlg Z is strict non-empty MSAlgebra over MSSign Z
the Sorts of (MSAlg Z) is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the carrier of (MSSign Z) is non empty trivial V33() set
ff1 is Relation-like the carrier of (MSSign A) -defined Function-like non empty total ManySortedSubset of the Sorts of (MSAlg A)
the carrier' of (MSSign A) is non empty set
f is Element of the carrier' of (MSSign A)
the carrier' of (MSSign Z) is non empty set
the ResultSort of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A)))
K20( the carrier' of (MSSign A), the carrier of (MSSign A)) is Relation-like set
K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A))) is set
the ResultSort of (MSSign A) * ff1 is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total set
f is Element of the carrier' of (MSSign Z)
( the ResultSort of (MSSign A) * ff1) . f is set
the ResultSort of (MSSign Z) is Relation-like the carrier' of (MSSign Z) -defined the carrier of (MSSign Z) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign Z), the carrier of (MSSign Z)))
K20( the carrier' of (MSSign Z), the carrier of (MSSign Z)) is Relation-like set
K19(K20( the carrier' of (MSSign Z), the carrier of (MSSign Z))) is set
the ResultSort of (MSSign Z) * the Sorts of (MSAlg Z) is Relation-like non-empty non empty-yielding the carrier' of (MSSign Z) -defined Function-like non empty total set
( the ResultSort of (MSSign Z) * the Sorts of (MSAlg Z)) . f is non empty set
Result (f,(MSAlg Z)) is non empty Element of rng the Sorts of (MSAlg Z)
rng the Sorts of (MSAlg Z) is non empty V45() set
Args (f,(MSAlg A)) is non empty Element of rng ( the Sorts of (MSAlg A) #)
the Sorts of (MSAlg A) # is Relation-like non-empty non empty-yielding the carrier of (MSSign A) * -defined Function-like non empty total set
the carrier of (MSSign A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign A)
rng ( the Sorts of (MSAlg A) #) is non empty V45() set
Result (f,(MSAlg A)) is non empty Element of rng the Sorts of (MSAlg A)
rng the Sorts of (MSAlg A) is non empty V45() set
Den (f,(MSAlg A)) is Relation-like Args (f,(MSAlg A)) -defined Result (f,(MSAlg A)) -valued Function-like quasi_total Element of K19(K20((Args (f,(MSAlg A))),(Result (f,(MSAlg A)))))
K20((Args (f,(MSAlg A))),(Result (f,(MSAlg A)))) is Relation-like set
K19(K20((Args (f,(MSAlg A))),(Result (f,(MSAlg A))))) is set
the Arity of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)))
K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)) is Relation-like set
K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *))) is set
ff1 # is Relation-like the carrier of (MSSign A) * -defined Function-like non empty total set
the Arity of (MSSign A) * (ff1 #) is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total set
( the Arity of (MSSign A) * (ff1 #)) . f is set
(Den (f,(MSAlg A))) | (( the Arity of (MSSign A) * (ff1 #)) . f) is Relation-like Args (f,(MSAlg A)) -defined ( the Arity of (MSSign A) * (ff1 #)) . f -defined Args (f,(MSAlg A)) -defined Result (f,(MSAlg A)) -valued Function-like Element of K19(K20((Args (f,(MSAlg A))),(Result (f,(MSAlg A)))))
rng ((Den (f,(MSAlg A))) | (( the Arity of (MSSign A) * (ff1 #)) . f)) is set
Den (f,(MSAlg Z)) is Relation-like Args (f,(MSAlg Z)) -defined Result (f,(MSAlg Z)) -valued Function-like quasi_total Element of K19(K20((Args (f,(MSAlg Z))),(Result (f,(MSAlg Z)))))
Args (f,(MSAlg Z)) is non empty Element of rng ( the Sorts of (MSAlg Z) #)
the Sorts of (MSAlg Z) # is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) * -defined Function-like non empty total set
the carrier of (MSSign Z) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign Z)
rng ( the Sorts of (MSAlg Z) #) is non empty V45() set
K20((Args (f,(MSAlg Z))),(Result (f,(MSAlg Z)))) is Relation-like set
K19(K20((Args (f,(MSAlg Z))),(Result (f,(MSAlg Z))))) is set
rng (Den (f,(MSAlg Z))) is set
(Den (f,(MSAlg A))) | (Args (f,(MSAlg Z))) is Relation-like Args (f,(MSAlg A)) -defined Args (f,(MSAlg Z)) -defined Args (f,(MSAlg A)) -defined Result (f,(MSAlg A)) -valued Function-like Element of K19(K20((Args (f,(MSAlg A))),(Result (f,(MSAlg A)))))
rng ((Den (f,(MSAlg A))) | (Args (f,(MSAlg Z)))) is set
Z is non empty partial quasi_total non-empty UAStr
A is non empty partial quasi_total non-empty UAStr
MSSign A is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
the carrier of (MSSign A) is non empty trivial V33() set
MSAlg A is strict non-empty MSAlgebra over MSSign A
the Sorts of (MSAlg A) is Relation-like non-empty non empty-yielding the carrier of (MSSign A) -defined Function-like non empty total set
MSSign Z is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSAlg Z is strict non-empty MSAlgebra over MSSign Z
the Sorts of (MSAlg Z) is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the carrier of (MSSign Z) is non empty trivial V33() set
the Charact of (MSAlg Z) is Relation-like the carrier' of (MSSign Z) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign Z) * ( the Sorts of (MSAlg Z) #), the ResultSort of (MSSign Z) * the Sorts of (MSAlg Z)
the carrier' of (MSSign Z) is non empty set
the Arity of (MSSign Z) is Relation-like the carrier' of (MSSign Z) -defined the carrier of (MSSign Z) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *)))
the carrier of (MSSign Z) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign Z)
K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *)) is Relation-like set
K19(K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *))) is set
the Sorts of (MSAlg Z) # is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) * -defined Function-like non empty total set
the Arity of (MSSign Z) * ( the Sorts of (MSAlg Z) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign Z) -defined Function-like non empty total set
the ResultSort of (MSSign Z) is Relation-like the carrier' of (MSSign Z) -defined the carrier of (MSSign Z) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign Z), the carrier of (MSSign Z)))
K20( the carrier' of (MSSign Z), the carrier of (MSSign Z)) is Relation-like set
K19(K20( the carrier' of (MSSign Z), the carrier of (MSSign Z))) is set
the ResultSort of (MSSign Z) * the Sorts of (MSAlg Z) is Relation-like non-empty non empty-yielding the carrier' of (MSSign Z) -defined Function-like non empty total set
ff1 is Relation-like the carrier of (MSSign A) -defined Function-like non empty total ManySortedSubset of the Sorts of (MSAlg A)
Opers ((MSAlg A),ff1) is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign A) * (ff1 #), the ResultSort of (MSSign A) * ff1
the carrier' of (MSSign A) is non empty set
the Arity of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)))
the carrier of (MSSign A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign A)
K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)) is Relation-like set
K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *))) is set
ff1 # is Relation-like the carrier of (MSSign A) * -defined Function-like non empty total set
the Arity of (MSSign A) * (ff1 #) is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total set
the ResultSort of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A)))
K20( the carrier' of (MSSign A), the carrier of (MSSign A)) is Relation-like set
K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A))) is set
the ResultSort of (MSSign A) * ff1 is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total set
signature Z is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(*--> 0) * (signature Z) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V25() Element of K19(K20(NAT,({0} *)))
dom (signature Z) is Element of K19(NAT)
z is Relation-like Function-like Element of {0}
(dom (signature Z)) --> z is Relation-like dom (signature Z) -defined {0} -valued Function-like constant total quasi_total Function-yielding V25() Element of K19(K20((dom (signature Z)),{0}))
K20((dom (signature Z)),{0}) is Relation-like set
K19(K20((dom (signature Z)),{0})) is set
{z} is functional non empty set
K20((dom (signature Z)),{z}) is Relation-like set
signature A is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(*--> 0) * (signature A) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V25() Element of K19(K20(NAT,({0} *)))
dom (signature A) is Element of K19(NAT)
(dom (signature A)) --> z is Relation-like dom (signature A) -defined {0} -valued Function-like constant total quasi_total Function-yielding V25() Element of K19(K20((dom (signature A)),{0}))
K20((dom (signature A)),{0}) is Relation-like set
K19(K20((dom (signature A)),{0})) is set
K20((dom (signature A)),{z}) is Relation-like set
K20((dom (signature Z)),({0} *)) is Relation-like set
K19(K20((dom (signature Z)),({0} *))) is set
K20((dom (signature A)),({0} *)) is Relation-like set
K19(K20((dom (signature A)),({0} *))) is set
y1 is Relation-like dom (signature A) -defined {0} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20((dom (signature A)),({0} *)))
ManySortedSign(# {0},(dom (signature A)),y1,((dom (signature A)) --> z) #) is non empty V70() strict ManySortedSign
y is Relation-like dom (signature Z) -defined {0} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20((dom (signature Z)),({0} *)))
ManySortedSign(# {0},(dom (signature Z)),y,((dom (signature Z)) --> z) #) is non empty V70() strict ManySortedSign
f is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total set
x is set
f . x is set
(Opers ((MSAlg A),ff1)) . x is Relation-like Function-like set
y is Element of the carrier' of (MSSign A)
(Opers ((MSAlg A),ff1)) . y is Relation-like Function-like set
y /. ff1 is Relation-like ( the Arity of (MSSign A) * (ff1 #)) . y -defined ( the ResultSort of (MSSign A) * ff1) . y -valued Function-like quasi_total Element of K19(K20((( the Arity of (MSSign A) * (ff1 #)) . y),(( the ResultSort of (MSSign A) * ff1) . y)))
( the Arity of (MSSign A) * (ff1 #)) . y is set
( the ResultSort of (MSSign A) * ff1) . y is set
K20((( the Arity of (MSSign A) * (ff1 #)) . y),(( the ResultSort of (MSSign A) * ff1) . y)) is Relation-like set
K19(K20((( the Arity of (MSSign A) * (ff1 #)) . y),(( the ResultSort of (MSSign A) * ff1) . y))) is set
Args (y,(MSAlg A)) is non empty Element of rng ( the Sorts of (MSAlg A) #)
the Sorts of (MSAlg A) # is Relation-like non-empty non empty-yielding the carrier of (MSSign A) * -defined Function-like non empty total set
rng ( the Sorts of (MSAlg A) #) is non empty V45() set
Result (y,(MSAlg A)) is non empty Element of rng the Sorts of (MSAlg A)
rng the Sorts of (MSAlg A) is non empty V45() set
Den (y,(MSAlg A)) is Relation-like Args (y,(MSAlg A)) -defined Result (y,(MSAlg A)) -valued Function-like quasi_total Element of K19(K20((Args (y,(MSAlg A))),(Result (y,(MSAlg A)))))
K20((Args (y,(MSAlg A))),(Result (y,(MSAlg A)))) is Relation-like set
K19(K20((Args (y,(MSAlg A))),(Result (y,(MSAlg A))))) is set
(Den (y,(MSAlg A))) | (( the Arity of (MSSign A) * (ff1 #)) . y) is Relation-like ( the Arity of (MSSign A) * (ff1 #)) . y -defined Args (y,(MSAlg A)) -defined Result (y,(MSAlg A)) -valued Function-like Element of K19(K20((Args (y,(MSAlg A))),(Result (y,(MSAlg A)))))
the Arity of (MSSign Z) * (ff1 #) is Relation-like the carrier' of (MSSign Z) -defined Function-like set
C is Element of the carrier' of (MSSign Z)
( the Arity of (MSSign Z) * (ff1 #)) . C is set
( the Arity of (MSSign Z) * ( the Sorts of (MSAlg Z) #)) . C is non empty set
(Den (y,(MSAlg A))) | (( the Arity of (MSSign Z) * ( the Sorts of (MSAlg Z) #)) . C) is Relation-like Args (y,(MSAlg A)) -defined ( the Arity of (MSSign Z) * ( the Sorts of (MSAlg Z) #)) . C -defined Args (y,(MSAlg A)) -defined Result (y,(MSAlg A)) -valued Function-like Element of K19(K20((Args (y,(MSAlg A))),(Result (y,(MSAlg A)))))
f . C is set
Den (C,(MSAlg Z)) is Relation-like Args (C,(MSAlg Z)) -defined Result (C,(MSAlg Z)) -valued Function-like quasi_total Element of K19(K20((Args (C,(MSAlg Z))),(Result (C,(MSAlg Z)))))
Args (C,(MSAlg Z)) is non empty Element of rng ( the Sorts of (MSAlg Z) #)
rng ( the Sorts of (MSAlg Z) #) is non empty V45() set
Result (C,(MSAlg Z)) is non empty Element of rng the Sorts of (MSAlg Z)
rng the Sorts of (MSAlg Z) is non empty V45() set
K20((Args (C,(MSAlg Z))),(Result (C,(MSAlg Z)))) is Relation-like set
K19(K20((Args (C,(MSAlg Z))),(Result (C,(MSAlg Z))))) is set
(Den (y,(MSAlg A))) | (Args (C,(MSAlg Z))) is Relation-like Args (y,(MSAlg A)) -defined Args (C,(MSAlg Z)) -defined Args (y,(MSAlg A)) -defined Result (y,(MSAlg A)) -valued Function-like Element of K19(K20((Args (y,(MSAlg A))),(Result (y,(MSAlg A)))))
Z is non empty partial quasi_total non-empty UAStr
A is non empty partial quasi_total non-empty UAStr
MSAlg Z is strict non-empty MSAlgebra over MSSign Z
MSSign Z is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSSign A is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSAlg A is strict non-empty MSAlgebra over MSSign A
ff1 is non-empty MSAlgebra over MSSign A
the Sorts of ff1 is Relation-like non-empty non empty-yielding the carrier of (MSSign A) -defined Function-like non empty total set
the carrier of (MSSign A) is non empty trivial V33() set
the Sorts of (MSAlg A) is Relation-like non-empty non empty-yielding the carrier of (MSSign A) -defined Function-like non empty total set
the carrier' of (MSSign A) is non empty set
the Charact of ff1 is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign A) * ( the Sorts of ff1 #), the ResultSort of (MSSign A) * the Sorts of ff1
the Arity of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)))
the carrier of (MSSign A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign A)
K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)) is Relation-like set
K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *))) is set
the Sorts of ff1 # is Relation-like non-empty non empty-yielding the carrier of (MSSign A) * -defined Function-like non empty total set
the Arity of (MSSign A) * ( the Sorts of ff1 #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign A) -defined Function-like non empty total set
the ResultSort of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A)))
K20( the carrier' of (MSSign A), the carrier of (MSSign A)) is Relation-like set
K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A))) is set
the ResultSort of (MSSign A) * the Sorts of ff1 is Relation-like non-empty non empty-yielding the carrier' of (MSSign A) -defined Function-like non empty total set
f is Relation-like the carrier of (MSSign A) -defined Function-like non empty total ManySortedSubset of the Sorts of (MSAlg A)
Opers ((MSAlg A),f) is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign A) * (f #), the ResultSort of (MSSign A) * f
f # is Relation-like the carrier of (MSSign A) * -defined Function-like non empty total set
the Arity of (MSSign A) * (f #) is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total set
the ResultSort of (MSSign A) * f is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total set
Z is non empty partial quasi_total non-empty UAStr
MSAlg Z is strict non-empty MSAlgebra over MSSign Z
MSSign Z is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
A is non empty partial quasi_total non-empty UAStr
MSSign A is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSAlg A is strict non-empty MSAlgebra over MSSign A
the carrier of Z is non empty set
the carrier of A is non empty set
K19( the carrier of A) is set
the carrier of (MSSign A) is non empty trivial V33() set
the Sorts of (MSAlg A) is Relation-like non-empty non empty-yielding the carrier of (MSSign A) -defined Function-like non empty total set
f is MSAlgebra over MSSign A
the Sorts of f is Relation-like the carrier of (MSSign A) -defined Function-like non empty total set
signature A is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(*--> 0) * (signature A) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V25() Element of K19(K20(NAT,({0} *)))
dom (signature A) is Element of K19(NAT)
z is Relation-like Function-like Element of {0}
(dom (signature A)) --> z is Relation-like dom (signature A) -defined {0} -valued Function-like constant total quasi_total Function-yielding V25() Element of K19(K20((dom (signature A)),{0}))
K20((dom (signature A)),{0}) is Relation-like set
K19(K20((dom (signature A)),{0})) is set
{z} is functional non empty set
K20((dom (signature A)),{z}) is Relation-like set
K20((dom (signature A)),({0} *)) is Relation-like set
K19(K20((dom (signature A)),({0} *))) is set
f is Relation-like the carrier of (MSSign A) -defined Function-like non empty total ManySortedSubset of the Sorts of (MSAlg A)
MSSorts A is Relation-like non-empty non empty-yielding the carrier of (MSSign A) -defined Function-like non empty total set
MSCharact A is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign A) * ((MSSorts A) #), the ResultSort of (MSSign A) * (MSSorts A)
the carrier' of (MSSign A) is non empty set
the Arity of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)))
the carrier of (MSSign A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign A)
K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)) is Relation-like set
K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *))) is set
(MSSorts A) # is Relation-like non-empty non empty-yielding the carrier of (MSSign A) * -defined Function-like non empty total set
the Arity of (MSSign A) * ((MSSorts A) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign A) -defined Function-like non empty total set
the ResultSort of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A)))
K20( the carrier' of (MSSign A), the carrier of (MSSign A)) is Relation-like set
K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A))) is set
the ResultSort of (MSSign A) * (MSSorts A) is Relation-like non-empty non empty-yielding the carrier' of (MSSign A) -defined Function-like non empty total set
MSAlgebra(# (MSSorts A),(MSCharact A) #) is strict MSAlgebra over MSSign A
y is Relation-like the carrier of (MSSign A) -defined Function-like non empty total set
C is Relation-like dom (signature A) -defined {0} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20((dom (signature A)),({0} *)))
ManySortedSign(# {0},(dom (signature A)),C,((dom (signature A)) --> z) #) is non empty V70() strict ManySortedSign
0 .--> the carrier of A is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> the carrier of A is Relation-like non-empty non empty-yielding {0} -defined { the carrier of A} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{ the carrier of A}))
{ the carrier of A} is non empty set
K20({0},{ the carrier of A}) is Relation-like set
K19(K20({0},{ the carrier of A})) is set
MSSorts Z is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the carrier of (MSSign Z) is non empty trivial V33() set
MSCharact Z is Relation-like the carrier' of (MSSign Z) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign Z) * ((MSSorts Z) #), the ResultSort of (MSSign Z) * (MSSorts Z)
the carrier' of (MSSign Z) is non empty set
the Arity of (MSSign Z) is Relation-like the carrier' of (MSSign Z) -defined the carrier of (MSSign Z) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *)))
the carrier of (MSSign Z) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign Z)
K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *)) is Relation-like set
K19(K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *))) is set
(MSSorts Z) # is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) * -defined Function-like non empty total set
the Arity of (MSSign Z) * ((MSSorts Z) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign Z) -defined Function-like non empty total set
the ResultSort of (MSSign Z) is Relation-like the carrier' of (MSSign Z) -defined the carrier of (MSSign Z) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign Z), the carrier of (MSSign Z)))
K20( the carrier' of (MSSign Z), the carrier of (MSSign Z)) is Relation-like set
K19(K20( the carrier' of (MSSign Z), the carrier of (MSSign Z))) is set
the ResultSort of (MSSign Z) * (MSSorts Z) is Relation-like non-empty non empty-yielding the carrier' of (MSSign Z) -defined Function-like non empty total set
MSAlgebra(# (MSSorts Z),(MSCharact Z) #) is strict MSAlgebra over MSSign Z
y . 0 is set
({0} --> the carrier of A) . 0 is set
(MSSorts Z) . 0 is set
0 .--> the carrier of Z is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> the carrier of Z is Relation-like non-empty non empty-yielding {0} -defined { the carrier of Z} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{ the carrier of Z}))
{ the carrier of Z} is non empty set
K20({0},{ the carrier of Z}) is Relation-like set
K19(K20({0},{ the carrier of Z})) is set
(0 .--> the carrier of Z) . 0 is set
Z is non empty partial quasi_total non-empty UAStr
MSAlg Z is strict non-empty MSAlgebra over MSSign Z
MSSign Z is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
A is non empty partial quasi_total non-empty UAStr
MSSign A is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSAlg A is strict non-empty MSAlgebra over MSSign A
the carrier of A is non empty set
K19( the carrier of A) is set
the carrier of Z is non empty set
MSSorts A is Relation-like non-empty non empty-yielding the carrier of (MSSign A) -defined Function-like non empty total set
the carrier of (MSSign A) is non empty trivial V33() set
MSCharact A is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign A) * ((MSSorts A) #), the ResultSort of (MSSign A) * (MSSorts A)
the carrier' of (MSSign A) is non empty set
the Arity of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)))
the carrier of (MSSign A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign A)
K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *)) is Relation-like set
K19(K20( the carrier' of (MSSign A),( the carrier of (MSSign A) *))) is set
(MSSorts A) # is Relation-like non-empty non empty-yielding the carrier of (MSSign A) * -defined Function-like non empty total set
the Arity of (MSSign A) * ((MSSorts A) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign A) -defined Function-like non empty total set
the ResultSort of (MSSign A) is Relation-like the carrier' of (MSSign A) -defined the carrier of (MSSign A) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A)))
K20( the carrier' of (MSSign A), the carrier of (MSSign A)) is Relation-like set
K19(K20( the carrier' of (MSSign A), the carrier of (MSSign A))) is set
the ResultSort of (MSSign A) * (MSSorts A) is Relation-like non-empty non empty-yielding the carrier' of (MSSign A) -defined Function-like non empty total set
MSAlgebra(# (MSSorts A),(MSCharact A) #) is strict MSAlgebra over MSSign A
f is non empty Element of K19( the carrier of A)
the carrier of A * is functional non empty FinSequence-membered FinSequenceSet of the carrier of A
Operations A is non empty PFuncsDomHQN of the carrier of A
the charact of A is Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of A *), the carrier of A)
PFuncs (( the carrier of A *), the carrier of A) is set
rng the charact of A is non empty V45() set
x is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of Operations A
the Sorts of (MSAlg A) is Relation-like non-empty non empty-yielding the carrier of (MSSign A) -defined Function-like non empty total set
f is MSAlgebra over MSSign A
the Sorts of f is Relation-like the carrier of (MSSign A) -defined Function-like non empty total set
MSSorts Z is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the carrier of (MSSign Z) is non empty trivial V33() set
MSCharact Z is Relation-like the carrier' of (MSSign Z) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign Z) * ((MSSorts Z) #), the ResultSort of (MSSign Z) * (MSSorts Z)
the carrier' of (MSSign Z) is non empty set
the Arity of (MSSign Z) is Relation-like the carrier' of (MSSign Z) -defined the carrier of (MSSign Z) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *)))
the carrier of (MSSign Z) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign Z)
K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *)) is Relation-like set
K19(K20( the carrier' of (MSSign Z),( the carrier of (MSSign Z) *))) is set
(MSSorts Z) # is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) * -defined Function-like non empty total set
the Arity of (MSSign Z) * ((MSSorts Z) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign Z) -defined Function-like non empty total set
the ResultSort of (MSSign Z) is Relation-like the carrier' of (MSSign Z) -defined the carrier of (MSSign Z) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign Z), the carrier of (MSSign Z)))
K20( the