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 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
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
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 the carrier of (MSSign A) -defined Function-like non empty total ManySortedSubset of the Sorts of (MSAlg A)
A2 is Relation-like NAT -defined f -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of f
len A2 is V26() V27() V28() V32() Element of NAT
arity x is V26() V27() V28() V32() Element of NAT
x . A2 is set
dom the charact of A is non empty Element of K19(NAT)
m is set
the charact of A . m is Relation-like Function-like homogeneous set
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)
g2 is Element of the carrier' of (MSSign A)
Args (g2,(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 (g2,(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 (g2,(MSAlg A)) is Relation-like Args (g2,(MSAlg A)) -defined Result (g2,(MSAlg A)) -valued Function-like quasi_total Element of K19(K20((Args (g2,(MSAlg A))),(Result (g2,(MSAlg A)))))
K20((Args (g2,(MSAlg A))),(Result (g2,(MSAlg A)))) is Relation-like set
K19(K20((Args (g2,(MSAlg A))),(Result (g2,(MSAlg A))))) is set
y # is Relation-like the carrier of (MSSign A) * -defined Function-like non empty total set
the Arity of (MSSign A) * (y #) is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total set
( the Arity of (MSSign A) * (y #)) . g2 is set
(Den (g2,(MSAlg A))) | (( the Arity of (MSSign A) * (y #)) . g2) is Relation-like Args (g2,(MSAlg A)) -defined ( the Arity of (MSSign A) * (y #)) . g2 -defined Args (g2,(MSAlg A)) -defined Result (g2,(MSAlg A)) -valued Function-like Element of K19(K20((Args (g2,(MSAlg A))),(Result (g2,(MSAlg A)))))
dom ((Den (g2,(MSAlg A))) | (( the Arity of (MSSign A) * (y #)) . g2)) is set
((Den (g2,(MSAlg A))) | (( the Arity of (MSSign A) * (y #)) . g2)) . A2 is set
(arity x) |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V33() V40( arity x) FinSequence-like FinSubsequence-like Element of (arity x) -tuples_on NAT
(arity x) -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 = arity x } is set
Seg (arity x) is V33() V40( arity x) Element of K19(NAT)
(Seg (arity x)) --> 0 is Relation-like Seg (arity x) -defined Seg (arity x) -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 (arity x)),{0}))
K20((Seg (arity x)),{0}) is Relation-like set
K19(K20((Seg (arity x)),{0})) is set
<*> the carrier of (MSSign A) is Relation-like non-empty empty-yielding NAT -defined the carrier of (MSSign A) -valued 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 FinSequence of the carrier of (MSSign A)
dom ((arity x) |-> 0) is Element of K19(NAT)
rng ((arity x) |-> 0) is set
dom the Arity of (MSSign A) is 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
g3 is Relation-like NAT -defined the carrier of (MSSign A) -valued Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of (MSSign A) *
g3 * the Sorts of (MSAlg A) is Relation-like non-empty NAT -defined Function-like set
(arity x) |-> the carrier of A is Relation-like NAT -defined Function-like V33() V40( arity x) FinSequence-like FinSubsequence-like set
(Seg (arity x)) --> the carrier of A is Relation-like non-empty Seg (arity x) -defined Seg (arity x) -defined { the carrier of A} -valued Function-like constant total total quasi_total V33() FinSequence-like FinSubsequence-like Element of K19(K20((Seg (arity x)),{ the carrier of A}))
K20((Seg (arity x)),{ the carrier of A}) is Relation-like set
K19(K20((Seg (arity x)),{ the carrier of A})) is set
dom A2 is Element of K19(NAT)
dom (g3 * the Sorts of (MSAlg A)) is set
g1 is set
A2 . g1 is set
(g3 * the Sorts of (MSAlg A)) . g1 is set
rng A2 is set
g3 . g1 is set
the Sorts of (MSAlg A) . (g3 . g1) is set
(MSSorts A) . 0 is set
(0 .--> the carrier of A) . 0 is set
dom (Den (g2,(MSAlg 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) #)) . g2 is non empty set
((*--> 0) * (signature A)) . g2 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
( the Sorts of (MSAlg A) #) . (((*--> 0) * (signature A)) . g2) is set
(signature A) . g2 is set
(*--> 0) . ((signature A) . g2) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
( the Sorts of (MSAlg A) #) . ((*--> 0) . ((signature A) . g2)) is set
(*--> 0) . (arity x) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of {0} *
( the Sorts of (MSAlg A) #) . ((*--> 0) . (arity x)) is set
( the Sorts of (MSAlg A) #) . ((arity x) |-> 0) is set
product (g3 * the Sorts of (MSAlg A)) is set
(len A2) -tuples_on f is functional non empty FinSequence-membered FinSequenceSet of f
f * is functional non empty FinSequence-membered FinSequenceSet of f
{ b1 where b1 is Relation-like NAT -defined f -valued Function-like V33() FinSequence-like FinSubsequence-like Element of f * : len b1 = len A2 } 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
dom y is non empty set
dom (*--> 0) is set
dom ((*--> 0) * (signature A)) is set
(y #) . (((*--> 0) * (signature A)) . g2) is set
(y #) . ((*--> 0) . ((signature A) . g2)) is set
(y #) . ((*--> 0) . (arity x)) is set
(y #) . ((arity x) |-> 0) is set
A4 is Relation-like NAT -defined the carrier of (MSSign A) -valued Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of (MSSign A) *
A4 * y is Relation-like NAT -defined Function-like set
product (A4 * y) is set
y . 0 is set
(Seg (arity x)) --> (y . 0) is Relation-like Seg (arity x) -defined Seg (arity x) -defined {(y . 0)} -valued Function-like constant total total quasi_total V33() FinSequence-like FinSubsequence-like Element of K19(K20((Seg (arity x)),{(y . 0)}))
{(y . 0)} is non empty set
K20((Seg (arity x)),{(y . 0)}) is Relation-like set
K19(K20((Seg (arity x)),{(y . 0)})) is set
product ((Seg (arity x)) --> (y . 0)) is set
(Seg (arity x)) --> f is Relation-like non-empty Seg (arity x) -defined Seg (arity x) -defined {f} -valued Function-like constant total total quasi_total V33() FinSequence-like FinSubsequence-like Element of K19(K20((Seg (arity x)),{f}))
{f} is non empty set
K20((Seg (arity x)),{f}) is Relation-like set
K19(K20((Seg (arity x)),{f})) is set
product ((Seg (arity x)) --> f) is set
Funcs ((Seg (arity x)),f) is non empty FUNCTION_DOMAIN of Seg (arity x),f
(arity x) -tuples_on f is functional non empty FinSequence-membered FinSequenceSet of f
{ b1 where b1 is Relation-like NAT -defined f -valued Function-like V33() FinSequence-like FinSubsequence-like Element of f * : len b1 = arity x } is set
(dom (Den (g2,(MSAlg A)))) /\ (( the Arity of (MSSign A) * (y #)) . g2) is set
(Den (g2,(MSAlg A))) . A2 is set
(MSCharact A) . g2 is Relation-like Function-like set
((MSCharact A) . g2) . A2 is set
rng ((Den (g2,(MSAlg A))) | (( the Arity of (MSSign A) * (y #)) . g2)) is set
A4 is set
((Den (g2,(MSAlg A))) | (( the Arity of (MSSign A) * (y #)) . g2)) . A4 is set
the ResultSort of (MSSign A) * y is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total set
( the ResultSort of (MSSign A) * y) . g2 is set
(dom (signature A)) --> 0 is Relation-like dom (signature A) -defined NAT -valued Function-like constant total quasi_total Function-yielding V25() Element of K19(K20((dom (signature A)),NAT))
K20((dom (signature A)),NAT) is Relation-like set
K19(K20((dom (signature A)),NAT)) is set
dom ((dom (signature A)) --> 0) is set
((dom (signature A)) --> 0) . g2 is Relation-like Function-like set
y . (((dom (signature A)) --> 0) . g2) is set
the Sorts of f . 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
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)
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
PFuncs (( the carrier of Z *), the carrier of Z) 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 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
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
the Charact of 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) * ( the Sorts of f #), the ResultSort of (MSSign A) * the Sorts of f
the Sorts of f # is Relation-like the carrier of (MSSign A) * -defined Function-like non empty total set
the Arity of (MSSign A) * ( the Sorts of f #) is Relation-like the carrier' of (MSSign A) -defined Function-like non empty total set
the ResultSort of (MSSign A) * the Sorts of f is Relation-like 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
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
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
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
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
y1 is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)
dom y1 is Element of K19(NAT)
dom the Charact of f is non empty set
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)
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
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)
dom the charact of A is non empty 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
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
dom f is non empty set
A2 is set
the charact of A . A2 is Relation-like Function-like homogeneous set
y1 . A2 is set
m is Relation-like the carrier of A * -defined the carrier of A -valued Function-like non empty homogeneous quasi_total Element of Operations A
m /. 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
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 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) #) 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) * 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
dom the Charact of (MSAlg A) is non empty set
g2 is Element of the carrier' of (MSSign A)
arity m is V26() V27() V28() V32() Element of NAT
(arity m) |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V33() V40( arity m) FinSequence-like FinSubsequence-like Element of (arity m) -tuples_on NAT
(arity m) -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 = arity m } is set
Seg (arity m) is V33() V40( arity m) Element of K19(NAT)
(Seg (arity m)) --> 0 is Relation-like Seg (arity m) -defined Seg (arity m) -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 (arity m)),{0}))
K20((Seg (arity m)),{0}) is Relation-like set
K19(K20((Seg (arity m)),{0})) is set
dom (*--> 0) is set
(signature A) . g2 is set
dom ((*--> 0) * (signature A)) is set
( the Arity of (MSSign A) * (f #)) . g2 is set
((*--> 0) * (signature A)) . g2 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f #) . (((*--> 0) * (signature A)) . g2) is set
(*--> 0) . ((signature A) . g2) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(f #) . ((*--> 0) . ((signature A) . g2)) is set
(*--> 0) . (arity m) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of {0} *
(f #) . ((*--> 0) . (arity m)) is set
(f #) . ((arity m) |-> 0) is set
A4 is Relation-like NAT -defined the carrier of (MSSign A) -valued Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of (MSSign A) *
A4 * f is Relation-like NAT -defined Function-like set
product (A4 * f) is set
f . 0 is set
(Seg (arity m)) --> (f . 0) is Relation-like Seg (arity m) -defined Seg (arity m) -defined {(f . 0)} -valued Function-like constant total total quasi_total V33() FinSequence-like FinSubsequence-like Element of K19(K20((Seg (arity m)),{(f . 0)}))
{(f . 0)} is non empty set
K20((Seg (arity m)),{(f . 0)}) is Relation-like set
K19(K20((Seg (arity m)),{(f . 0)})) is set
product ((Seg (arity m)) --> (f . 0)) is set
(Seg (arity m)) --> y is Relation-like non-empty Seg (arity m) -defined Seg (arity m) -defined {y} -valued Function-like constant total total quasi_total V33() FinSequence-like FinSubsequence-like Element of K19(K20((Seg (arity m)),{y}))
{y} is non empty set
K20((Seg (arity m)),{y}) is Relation-like set
K19(K20((Seg (arity m)),{y})) is set
product ((Seg (arity m)) --> y) is set
Funcs ((Seg (arity m)),y) is non empty FUNCTION_DOMAIN of Seg (arity m),y
(arity m) -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 m } is set
y1 . g2 is set
the Charact of f . g2 is Relation-like Function-like set
g2 /. f is Relation-like ( the Arity of (MSSign A) * (f #)) . g2 -defined ( the ResultSort of (MSSign A) * f) . g2 -valued Function-like quasi_total Element of K19(K20((( the Arity of (MSSign A) * (f #)) . g2),(( the ResultSort of (MSSign A) * f) . g2)))
( the ResultSort of (MSSign A) * f) . g2 is set
K20((( the Arity of (MSSign A) * (f #)) . g2),(( the ResultSort of (MSSign A) * f) . g2)) is Relation-like set
K19(K20((( the Arity of (MSSign A) * (f #)) . g2),(( the ResultSort of (MSSign A) * f) . g2))) is set
Args (g2,(MSAlg A)) is non empty Element of rng ( the Sorts of (MSAlg A) #)
rng ( the Sorts of (MSAlg A) #) is non empty V45() set
Result (g2,(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 (g2,(MSAlg A)) is Relation-like Args (g2,(MSAlg A)) -defined Result (g2,(MSAlg A)) -valued Function-like quasi_total Element of K19(K20((Args (g2,(MSAlg A))),(Result (g2,(MSAlg A)))))
K20((Args (g2,(MSAlg A))),(Result (g2,(MSAlg A)))) is Relation-like set
K19(K20((Args (g2,(MSAlg A))),(Result (g2,(MSAlg A))))) is set
(Den (g2,(MSAlg A))) | (( the Arity of (MSSign A) * (f #)) . g2) is Relation-like ( the Arity of (MSSign A) * (f #)) . g2 -defined Args (g2,(MSAlg A)) -defined Result (g2,(MSAlg A)) -valued Function-like Element of K19(K20((Args (g2,(MSAlg A))),(Result (g2,(MSAlg A)))))
(MSCharact A) . g2 is Relation-like Function-like set
((MSCharact A) . g2) | (( the Arity of (MSSign A) * (f #)) . g2) is Relation-like Function-like set
m | ((arity m) -tuples_on y) is Relation-like the carrier of A * -defined (arity m) -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
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 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)
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
PFuncs (( the carrier of Z *), the carrier of Z) is set
ff1 is non empty Element of K19( the carrier of A)
Opers (A,ff1) is Relation-like NAT -defined PFuncs ((ff1 *),ff1) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((ff1 *),ff1)
ff1 * is functional non empty FinSequence-membered FinSequenceSet of ff1
PFuncs ((ff1 *),ff1) is set
Z is non empty trivial V64() non void 1 -element V70() segmental ManySortedSign
A is non-empty MSAlgebra over Z
1-Alg A is non empty strict partial quasi_total non-empty UAStr
the carrier of (1-Alg A) is non empty set
K19( the carrier of (1-Alg A)) is set
ff1 is non-empty MSSubAlgebra of A
1-Alg ff1 is non empty strict partial quasi_total non-empty UAStr
the carrier of (1-Alg ff1) is non empty set
the Sorts of ff1 is Relation-like non-empty non empty-yielding the carrier of Z -defined Function-like non empty total set
the carrier of Z is non empty trivial V33() set
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of Z -defined Function-like non empty total set
the_sort_of ff1 is non empty set
the_charact_of ff1 is Relation-like NAT -defined PFuncs (((the_sort_of ff1) *),(the_sort_of ff1)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((the_sort_of ff1) *),(the_sort_of ff1))
(the_sort_of ff1) * is functional non empty FinSequence-membered FinSequenceSet of the_sort_of ff1
PFuncs (((the_sort_of ff1) *),(the_sort_of ff1)) is set
UAStr(# (the_sort_of ff1),(the_charact_of ff1) #) is non empty strict UAStr
rng the Sorts of ff1 is non empty V45() set
the_sort_of A is non empty set
the_charact_of A is Relation-like NAT -defined PFuncs (((the_sort_of A) *),(the_sort_of A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))
(the_sort_of A) * is functional non empty FinSequence-membered FinSequenceSet of the_sort_of A
PFuncs (((the_sort_of A) *),(the_sort_of A)) is set
UAStr(# (the_sort_of A),(the_charact_of A) #) is non empty strict UAStr
rng the Sorts of A is non empty V45() set
dom the Sorts of A is non empty set
f is non empty Element of rng the Sorts of A
f is set
the Sorts of A . f is set
dom the Sorts of ff1 is non empty set
f is non empty Element of rng the Sorts of ff1
x is set
the Sorts of ff1 . x is set
Z is non empty trivial V64() non void 1 -element V70() segmental ManySortedSign
A is non-empty MSAlgebra over Z
1-Alg A is non empty strict partial quasi_total non-empty UAStr
the carrier of (1-Alg A) is non empty set
K19( the carrier of (1-Alg A)) is set
ff1 is non-empty MSSubAlgebra of A
1-Alg ff1 is non empty strict partial quasi_total non-empty UAStr
the carrier of (1-Alg ff1) is non empty set
the carrier of Z is non empty trivial V33() set
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of Z -defined Function-like non empty total set
the Sorts of ff1 is Relation-like non-empty non empty-yielding the carrier of Z -defined Function-like non empty total set
f is Relation-like the carrier of Z -defined Function-like non empty total ManySortedSubset of the Sorts of A
the_sort_of ff1 is non empty set
the_charact_of ff1 is Relation-like NAT -defined PFuncs (((the_sort_of ff1) *),(the_sort_of ff1)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((the_sort_of ff1) *),(the_sort_of ff1))
(the_sort_of ff1) * is functional non empty FinSequence-membered FinSequenceSet of the_sort_of ff1
PFuncs (((the_sort_of ff1) *),(the_sort_of ff1)) is set
UAStr(# (the_sort_of ff1),(the_charact_of ff1) #) is non empty strict UAStr
f is non empty Element of K19( the carrier of (1-Alg A))
the_sort_of A is non empty set
the_charact_of A is Relation-like NAT -defined PFuncs (((the_sort_of A) *),(the_sort_of A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))
(the_sort_of A) * is functional non empty FinSequence-membered FinSequenceSet of the_sort_of A
PFuncs (((the_sort_of A) *),(the_sort_of A)) is set
UAStr(# (the_sort_of A),(the_charact_of A) #) is non empty strict UAStr
the carrier of (1-Alg A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (1-Alg A)
Operations (1-Alg A) is non empty PFuncsDomHQN of the carrier of (1-Alg A)
the charact of (1-Alg A) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A))
PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) is set
rng the charact of (1-Alg A) is non empty V45() set
x is Relation-like the carrier of (1-Alg A) * -defined the carrier of (1-Alg A) -valued Function-like non empty homogeneous quasi_total Element of Operations (1-Alg A)
dom the Sorts of A is non empty set
dom the Sorts of ff1 is non empty set
rng the Sorts of ff1 is non empty V45() set
dom the charact of (1-Alg A) is non empty Element of K19(NAT)
C is set
the charact of (1-Alg A) . C is Relation-like Function-like homogeneous set
the Charact of A is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of A #), the ResultSort of Z * the Sorts of A
the carrier' of Z is non empty set
the Arity of Z is Relation-like the carrier' of Z -defined the carrier of Z * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of Z,( the carrier of Z *)))
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
K20( the carrier' of Z,( the carrier of Z *)) is Relation-like set
K19(K20( the carrier' of Z,( the carrier of Z *))) is set
the Sorts of A # is Relation-like non-empty non empty-yielding the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of A #) is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z is Relation-like the carrier' of Z -defined the carrier of Z -valued Function-like quasi_total Element of K19(K20( the carrier' of Z, the carrier of Z))
K20( the carrier' of Z, the carrier of Z) is Relation-like set
K19(K20( the carrier' of Z, the carrier of Z)) is set
the ResultSort of Z * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
dom the Charact of A is non empty set
y is Element of the carrier' of Z
the ResultSort of Z . y is Element of the carrier of Z
f . ( the ResultSort of Z . y) is set
A2 is Relation-like NAT -defined f -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of f
len A2 is V26() V27() V28() V32() Element of NAT
arity x is V26() V27() V28() V32() Element of NAT
x . A2 is set
dom the Arity of Z is set
Args (y,A) is non empty Element of rng ( the Sorts of A #)
rng ( the Sorts of A #) is non empty V45() set
Result (y,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty V45() set
Den (y,A) is Relation-like Args (y,A) -defined Result (y,A) -valued Function-like quasi_total Element of K19(K20((Args (y,A)),(Result (y,A))))
K20((Args (y,A)),(Result (y,A))) is Relation-like set
K19(K20((Args (y,A)),(Result (y,A)))) is set
f # is Relation-like the carrier of Z * -defined Function-like non empty total set
the Arity of Z * (f #) is Relation-like the carrier' of Z -defined Function-like non empty total set
( the Arity of Z * (f #)) . y is set
(Den (y,A)) | (( the Arity of Z * (f #)) . y) is Relation-like Args (y,A) -defined ( the Arity of Z * (f #)) . y -defined Args (y,A) -defined Result (y,A) -valued Function-like Element of K19(K20((Args (y,A)),(Result (y,A))))
dom ((Den (y,A)) | (( the Arity of Z * (f #)) . y)) is set
((Den (y,A)) | (( the Arity of Z * (f #)) . y)) . A2 is set
the Charact of A . y is Relation-like Function-like set
the charact of (1-Alg A) . y is Relation-like Function-like homogeneous set
rng A2 is set
the Arity of Z . y is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of Z *
g2 is Relation-like NAT -defined the carrier of Z -valued Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of Z *
g2 * the Sorts of A is Relation-like non-empty NAT -defined Function-like set
dom x is functional non empty FinSequence-membered with_common_domain set
g3 is set
A3 is Relation-like Function-like set
dom A3 is set
rng A3 is set
dom (Den (y,A)) is set
the_arity_of y is Relation-like NAT -defined the carrier of Z -valued Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of Z *
len (the_arity_of y) is V26() V27() V28() V32() Element of NAT
(len (the_arity_of y)) -tuples_on the carrier of (1-Alg A) is functional non empty FinSequence-membered FinSequenceSet of the carrier of (1-Alg A)
{ b1 where b1 is Relation-like NAT -defined the carrier of (1-Alg A) -valued Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of (1-Alg A) * : len b1 = len (the_arity_of y) } is set
( the Arity of Z * ( the Sorts of A #)) . y is non empty set
( the Sorts of A #) . ( the Arity of Z . y) is non empty set
product (g2 * the Sorts of A) is set
g1 is Relation-like NAT -defined the carrier of (1-Alg A) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (1-Alg A)
len g1 is V26() V27() V28() V32() Element of NAT
m is Relation-like NAT -defined the carrier of (1-Alg A) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (1-Alg A)
len m is V26() V27() V28() V32() Element of NAT
dom A2 is Element of K19(NAT)
Seg (len (the_arity_of y)) is V33() V40( len (the_arity_of y)) Element of K19(NAT)
dom (the_arity_of y) is Element of K19(NAT)
dom g2 is Element of K19(NAT)
g2 * f is Relation-like NAT -defined Function-like set
dom (g2 * f) is set
A3 is set
rng g2 is set
g2 . A3 is set
dom f is non empty set
A3 is set
A2 . A3 is set
(g2 * f) . A3 is set
rng g2 is set
g2 . A3 is set
dom f is non empty set
f . (g2 . A3) is set
rng f is non empty set
g4 is Element of rng f
dom (g2 * the Sorts of A) is set
A3 is set
A3 is set
A2 . A3 is set
(g2 * the Sorts of A) . A3 is set
rng (g2 * the Sorts of A) is V45() set
g4 is non empty Element of rng the Sorts of A
(f #) . g2 is set
product (g2 * f) is set
A3 is set
rng g2 is set
g2 . A3 is set
(dom (Den (y,A))) /\ (( the Arity of Z * (f #)) . y) is set
(Den (y,A)) . A2 is set
rng ((Den (y,A)) | (( the Arity of Z * (f #)) . y)) is set
m is set
((Den (y,A)) | (( the Arity of Z * (f #)) . y)) . m is set
dom the ResultSort of Z is set
the ResultSort of Z * f is Relation-like the carrier' of Z -defined Function-like non empty total set
( the ResultSort of Z * f) . y is set
y1 is non empty Element of rng the Sorts of ff1
y is non empty Element of rng the Sorts of ff1
Z is non empty trivial V64() non void 1 -element V70() segmental ManySortedSign
A is non-empty MSAlgebra over Z
1-Alg A is non empty strict partial quasi_total non-empty UAStr
the carrier of (1-Alg A) is non empty set
K19( the carrier of (1-Alg A)) is set
ff1 is non-empty MSSubAlgebra of A
1-Alg ff1 is non empty strict partial quasi_total non-empty UAStr
the carrier of (1-Alg ff1) is non empty set
the charact of (1-Alg ff1) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (1-Alg ff1) *), the carrier of (1-Alg ff1)) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (1-Alg ff1) *), the carrier of (1-Alg ff1))
the carrier of (1-Alg ff1) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (1-Alg ff1)
PFuncs (( the carrier of (1-Alg ff1) *), the carrier of (1-Alg ff1)) is set
the carrier of Z is non empty trivial V33() set
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of Z -defined Function-like non empty total set
the Sorts of ff1 is Relation-like non-empty non empty-yielding the carrier of Z -defined Function-like non empty total set
the carrier' of Z is non empty set
the Charact of ff1 is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of ff1 #), the ResultSort of Z * the Sorts of ff1
the Arity of Z is Relation-like the carrier' of Z -defined the carrier of Z * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of Z,( the carrier of Z *)))
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
K20( the carrier' of Z,( the carrier of Z *)) is Relation-like set
K19(K20( the carrier' of Z,( the carrier of Z *))) is set
the Sorts of ff1 # is Relation-like non-empty non empty-yielding the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of ff1 #) is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z is Relation-like the carrier' of Z -defined the carrier of Z -valued Function-like quasi_total Element of K19(K20( the carrier' of Z, the carrier of Z))
K20( the carrier' of Z, the carrier of Z) is Relation-like set
K19(K20( the carrier' of Z, the carrier of Z)) is set
the ResultSort of Z * the Sorts of ff1 is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
f is Relation-like the carrier of Z -defined Function-like non empty total ManySortedSubset of the Sorts of A
Opers (A,f) is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * (f #), the ResultSort of Z * f
f # is Relation-like the carrier of Z * -defined Function-like non empty total set
the Arity of Z * (f #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * f is Relation-like the carrier' of Z -defined Function-like non empty total set
the_sort_of A is non empty set
the_charact_of A is Relation-like NAT -defined PFuncs (((the_sort_of A) *),(the_sort_of A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))
(the_sort_of A) * is functional non empty FinSequence-membered FinSequenceSet of the_sort_of A
PFuncs (((the_sort_of A) *),(the_sort_of A)) is set
UAStr(# (the_sort_of A),(the_charact_of A) #) is non empty strict UAStr
y is non empty Element of K19( the carrier of (1-Alg A))
Opers ((1-Alg 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
the_sort_of ff1 is non empty set
the_charact_of ff1 is Relation-like NAT -defined PFuncs (((the_sort_of ff1) *),(the_sort_of ff1)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((the_sort_of ff1) *),(the_sort_of ff1))
(the_sort_of ff1) * is functional non empty FinSequence-membered FinSequenceSet of the_sort_of ff1
PFuncs (((the_sort_of ff1) *),(the_sort_of ff1)) is set
UAStr(# (the_sort_of ff1),(the_charact_of ff1) #) is non empty strict UAStr
C is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)
the carrier of (1-Alg A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (1-Alg A)
Operations (1-Alg A) is non empty PFuncsDomHQN of the carrier of (1-Alg A)
the charact of (1-Alg A) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A))
PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) is set
rng the charact of (1-Alg A) is non empty V45() set
dom C is Element of K19(NAT)
y is set
the charact of (1-Alg A) . y is Relation-like Function-like homogeneous set
C . y is set
y1 is Relation-like the carrier of (1-Alg A) * -defined the carrier of (1-Alg A) -valued Function-like non empty homogeneous quasi_total Element of Operations (1-Alg A)
y1 /. 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
the Charact of A is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of A #), the ResultSort of Z * the Sorts of A
the Sorts of A # is Relation-like non-empty non empty-yielding the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of A #) is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
A2 is Element of the carrier' of Z
the Charact of A . A2 is Relation-like Function-like set
Den (A2,A) is Relation-like Args (A2,A) -defined Result (A2,A) -valued Function-like quasi_total Element of K19(K20((Args (A2,A)),(Result (A2,A))))
Args (A2,A) is non empty Element of rng ( the Sorts of A #)
rng ( the Sorts of A #) is non empty V45() set
Result (A2,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty V45() set
K20((Args (A2,A)),(Result (A2,A))) is Relation-like set
K19(K20((Args (A2,A)),(Result (A2,A)))) is set
dom y1 is functional non empty FinSequence-membered with_common_domain set
the_arity_of A2 is Relation-like NAT -defined the carrier of Z -valued Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of Z *
len (the_arity_of A2) is V26() V27() V28() V32() Element of NAT
(len (the_arity_of A2)) -tuples_on (the_sort_of A) is functional non empty FinSequence-membered FinSequenceSet of the_sort_of A
{ b1 where b1 is Relation-like NAT -defined the_sort_of A -valued Function-like V33() FinSequence-like FinSubsequence-like Element of (the_sort_of A) * : len b1 = len (the_arity_of A2) } is set
the Relation-like NAT -defined the_sort_of A -valued Function-like V33() V40( len (the_arity_of A2)) FinSequence-like FinSubsequence-like Element of (len (the_arity_of A2)) -tuples_on (the_sort_of A) is Relation-like NAT -defined the_sort_of A -valued Function-like V33() V40( len (the_arity_of A2)) FinSequence-like FinSubsequence-like Element of (len (the_arity_of A2)) -tuples_on (the_sort_of A)
g2 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len g2 is V26() V27() V28() V32() Element of NAT
A4 is Relation-like NAT -defined the_sort_of A -valued Function-like V33() FinSequence-like FinSubsequence-like Element of (the_sort_of A) *
len A4 is V26() V27() V28() V32() Element of NAT
arity y1 is V26() V27() V28() V32() Element of NAT
m is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
( the Arity of Z * (f #)) . A2 is set
Args (A2,ff1) is non empty Element of rng ( the Sorts of ff1 #)
rng ( the Sorts of ff1 #) is non empty V45() set
(arity y1) -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 y1 } is set
the Charact of ff1 . A2 is Relation-like Function-like set
A2 /. f is Relation-like ( the Arity of Z * (f #)) . A2 -defined ( the ResultSort of Z * f) . A2 -valued Function-like quasi_total Element of K19(K20((( the Arity of Z * (f #)) . A2),(( the ResultSort of Z * f) . A2)))
( the ResultSort of Z * f) . A2 is set
K20((( the Arity of Z * (f #)) . A2),(( the ResultSort of Z * f) . A2)) is Relation-like set
K19(K20((( the Arity of Z * (f #)) . A2),(( the ResultSort of Z * f) . A2))) is set
(Den (A2,A)) | (( the Arity of Z * (f #)) . A2) is Relation-like Args (A2,A) -defined ( the Arity of Z * (f #)) . A2 -defined Args (A2,A) -defined Result (A2,A) -valued Function-like Element of K19(K20((Args (A2,A)),(Result (A2,A))))
( the Charact of A . A2) | (( the Arity of Z * (f #)) . A2) is Relation-like Function-like set
y1 | ((arity y1) -tuples_on y) is Relation-like the carrier of (1-Alg A) * -defined (arity y1) -tuples_on y -defined the carrier of (1-Alg A) * -defined the carrier of (1-Alg A) -valued Function-like Element of K19(K20(( the carrier of (1-Alg A) *), the carrier of (1-Alg A)))
K20(( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) is Relation-like set
K19(K20(( the carrier of (1-Alg A) *), the carrier of (1-Alg A))) is set
the Charact of A is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of A #), the ResultSort of Z * the Sorts of A
the Sorts of A # is Relation-like non-empty non empty-yielding the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of A #) is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
dom the Charact of A is non empty set
dom the charact of (1-Alg A) is non empty Element of K19(NAT)
Z is non empty trivial V64() non void 1 -element V70() segmental ManySortedSign
A is non-empty MSAlgebra over Z
1-Alg A is non empty strict partial quasi_total non-empty UAStr
ff1 is non-empty MSSubAlgebra of A
1-Alg ff1 is non empty strict partial quasi_total non-empty UAStr
the carrier of (1-Alg ff1) is non empty set
the carrier of (1-Alg A) is non empty set
K19( the carrier of (1-Alg A)) is set
the charact of (1-Alg ff1) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (1-Alg ff1) *), the carrier of (1-Alg ff1)) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (1-Alg ff1) *), the carrier of (1-Alg ff1))
the carrier of (1-Alg ff1) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (1-Alg ff1)
PFuncs (( the carrier of (1-Alg ff1) *), the carrier of (1-Alg ff1)) is set
f is non empty Element of K19( the carrier of (1-Alg A))
Opers ((1-Alg A),f) is Relation-like NAT -defined PFuncs ((f *),f) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((f *),f)
f * is functional non empty FinSequence-membered FinSequenceSet of f
PFuncs ((f *),f) is set
Z is non empty non void V70() ManySortedSign
A is MSAlgebra over Z
ff1 is MSAlgebra over Z
the Sorts of ff1 is Relation-like the carrier of Z -defined Function-like non empty total set
the carrier of Z is non empty set
the Charact of ff1 is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of ff1 #), the ResultSort of Z * the Sorts of ff1
the carrier' of Z is non empty set
the Arity of Z is Relation-like the carrier' of Z -defined the carrier of Z * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of Z,( the carrier of Z *)))
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
K20( the carrier' of Z,( the carrier of Z *)) is Relation-like set
K19(K20( the carrier' of Z,( the carrier of Z *))) is set
the Sorts of ff1 # is Relation-like the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of ff1 #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z is Relation-like the carrier' of Z -defined the carrier of Z -valued Function-like quasi_total Element of K19(K20( the carrier' of Z, the carrier of Z))
K20( the carrier' of Z, the carrier of Z) is Relation-like set
K19(K20( the carrier' of Z, the carrier of Z)) is set
the ResultSort of Z * the Sorts of ff1 is Relation-like the carrier' of Z -defined Function-like non empty total set
MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is strict MSAlgebra over Z
the Sorts of A is Relation-like the carrier of Z -defined Function-like non empty total set
the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is Relation-like the carrier of Z -defined Function-like non empty total set
the Charact of A is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of A #), the ResultSort of Z * the Sorts of A
the Sorts of A # is Relation-like the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of A #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * the Sorts of A is Relation-like the carrier' of Z -defined Function-like non empty total set
f is Relation-like the carrier of Z -defined Function-like non empty total ManySortedSubset of the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)
Opers (MSAlgebra(# the Sorts of ff1, the Charact of ff1 #),f) is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * (f #), the ResultSort of Z * f
f # is Relation-like the carrier of Z * -defined Function-like non empty total set
the Arity of Z * (f #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * f is Relation-like the carrier' of Z -defined Function-like non empty total set
f is Relation-like the carrier of Z -defined Function-like non empty total ManySortedSubset of the Sorts of ff1
f is Element of the carrier' of Z
Den (f,ff1) is Relation-like Args (f,ff1) -defined Result (f,ff1) -valued Function-like quasi_total Element of K19(K20((Args (f,ff1)),(Result (f,ff1))))
Args (f,ff1) is Element of rng ( the Sorts of ff1 #)
rng ( the Sorts of ff1 #) is non empty set
Result (f,ff1) is Element of rng the Sorts of ff1
rng the Sorts of ff1 is non empty set
K20((Args (f,ff1)),(Result (f,ff1))) is Relation-like set
K19(K20((Args (f,ff1)),(Result (f,ff1)))) is set
the Charact of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #), the ResultSort of Z * the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)
the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) # is Relation-like the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the Charact of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) . f is Relation-like Function-like set
Den (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) is Relation-like Args (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -defined Result (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -valued Function-like quasi_total Element of K19(K20((Args (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)))))
Args (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) is Element of rng ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #)
rng ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #) is non empty set
Result (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) is Element of rng the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)
rng the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is non empty set
K20((Args (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)))) is Relation-like set
K19(K20((Args (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))))) is set
( the Arity of Z * (f #)) . f is set
(Den (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))) | (( the Arity of Z * (f #)) . f) is Relation-like Args (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -defined ( the Arity of Z * (f #)) . f -defined Args (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -defined Result (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -valued Function-like Element of K19(K20((Args (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)))))
rng ((Den (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))) | (( the Arity of Z * (f #)) . f)) is set
( the ResultSort of Z * f) . f is set
f is set
the Charact of A . f is Relation-like Function-like set
(Opers (MSAlgebra(# the Sorts of ff1, the Charact of ff1 #),f)) . f is Relation-like Function-like set
x is Element of the carrier' of Z
Den (x,ff1) is Relation-like Args (x,ff1) -defined Result (x,ff1) -valued Function-like quasi_total Element of K19(K20((Args (x,ff1)),(Result (x,ff1))))
Args (x,ff1) is Element of rng ( the Sorts of ff1 #)
rng ( the Sorts of ff1 #) is non empty set
Result (x,ff1) is Element of rng the Sorts of ff1
rng the Sorts of ff1 is non empty set
K20((Args (x,ff1)),(Result (x,ff1))) is Relation-like set
K19(K20((Args (x,ff1)),(Result (x,ff1)))) is set
the Charact of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #), the ResultSort of Z * the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)
the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) # is Relation-like the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the Charact of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) . x is Relation-like Function-like set
Den (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) is Relation-like Args (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -defined Result (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -valued Function-like quasi_total Element of K19(K20((Args (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)))))
Args (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) is Element of rng ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #)
rng ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #) is non empty set
Result (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) is Element of rng the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)
rng the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is non empty set
K20((Args (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)))) is Relation-like set
K19(K20((Args (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))))) is set
Opers (ff1,f) is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * (f #), the ResultSort of Z * f
f # is Relation-like the carrier of Z * -defined Function-like non empty total set
the Arity of Z * (f #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * f is Relation-like the carrier' of Z -defined Function-like non empty total set
(Opers (ff1,f)) . x is Relation-like Function-like set
x /. f is Relation-like ( the Arity of Z * (f #)) . x -defined ( the ResultSort of Z * f) . x -valued Function-like quasi_total Element of K19(K20((( the Arity of Z * (f #)) . x),(( the ResultSort of Z * f) . x)))
( the Arity of Z * (f #)) . x is set
( the ResultSort of Z * f) . x is set
K20((( the Arity of Z * (f #)) . x),(( the ResultSort of Z * f) . x)) is Relation-like set
K19(K20((( the Arity of Z * (f #)) . x),(( the ResultSort of Z * f) . x))) is set
( the Arity of Z * (f #)) . x is set
(Den (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))) | (( the Arity of Z * (f #)) . x) is Relation-like Args (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -defined ( the Arity of Z * (f #)) . x -defined Args (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -defined Result (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -valued Function-like Element of K19(K20((Args (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)))))
x /. f is Relation-like ( the Arity of Z * (f #)) . x -defined ( the ResultSort of Z * f) . x -valued Function-like quasi_total Element of K19(K20((( the Arity of Z * (f #)) . x),(( the ResultSort of Z * f) . x)))
( the ResultSort of Z * f) . x is set
K20((( the Arity of Z * (f #)) . x),(( the ResultSort of Z * f) . x)) is Relation-like set
K19(K20((( the Arity of Z * (f #)) . x),(( the ResultSort of Z * f) . x))) is set
(Opers (MSAlgebra(# the Sorts of ff1, the Charact of ff1 #),f)) . x is Relation-like Function-like set
the Sorts of A is Relation-like the carrier of Z -defined Function-like non empty total set
the Charact of A is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of A #), the ResultSort of Z * the Sorts of A
the Sorts of A # is Relation-like the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of A #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * the Sorts of A is Relation-like the carrier' of Z -defined Function-like non empty total set
f is Relation-like the carrier of Z -defined Function-like non empty total ManySortedSubset of the Sorts of ff1
Opers (ff1,f) is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * (f #), the ResultSort of Z * f
f # is Relation-like the carrier of Z * -defined Function-like non empty total set
the Arity of Z * (f #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * f is Relation-like the carrier' of Z -defined Function-like non empty total set
the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is Relation-like the carrier of Z -defined Function-like non empty total set
f is Relation-like the carrier of Z -defined Function-like non empty total ManySortedSubset of the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)
f is Element of the carrier' of Z
Den (f,ff1) is Relation-like Args (f,ff1) -defined Result (f,ff1) -valued Function-like quasi_total Element of K19(K20((Args (f,ff1)),(Result (f,ff1))))
Args (f,ff1) is Element of rng ( the Sorts of ff1 #)
rng ( the Sorts of ff1 #) is non empty set
Result (f,ff1) is Element of rng the Sorts of ff1
rng the Sorts of ff1 is non empty set
K20((Args (f,ff1)),(Result (f,ff1))) is Relation-like set
K19(K20((Args (f,ff1)),(Result (f,ff1)))) is set
the Charact of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #), the ResultSort of Z * the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)
the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) # is Relation-like the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the Charact of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) . f is Relation-like Function-like set
Den (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) is Relation-like Args (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -defined Result (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -valued Function-like quasi_total Element of K19(K20((Args (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)))))
Args (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) is Element of rng ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #)
rng ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #) is non empty set
Result (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) is Element of rng the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)
rng the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is non empty set
K20((Args (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)))) is Relation-like set
K19(K20((Args (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (f,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))))) is set
( the Arity of Z * (f #)) . f is set
(Den (f,ff1)) | (( the Arity of Z * (f #)) . f) is Relation-like Args (f,ff1) -defined ( the Arity of Z * (f #)) . f -defined Args (f,ff1) -defined Result (f,ff1) -valued Function-like Element of K19(K20((Args (f,ff1)),(Result (f,ff1))))
rng ((Den (f,ff1)) | (( the Arity of Z * (f #)) . f)) is set
( the ResultSort of Z * f) . f is set
f is set
the Charact of A . f is Relation-like Function-like set
(Opers (ff1,f)) . f is Relation-like Function-like set
x is Element of the carrier' of Z
Den (x,ff1) is Relation-like Args (x,ff1) -defined Result (x,ff1) -valued Function-like quasi_total Element of K19(K20((Args (x,ff1)),(Result (x,ff1))))
Args (x,ff1) is Element of rng ( the Sorts of ff1 #)
rng ( the Sorts of ff1 #) is non empty set
Result (x,ff1) is Element of rng the Sorts of ff1
rng the Sorts of ff1 is non empty set
K20((Args (x,ff1)),(Result (x,ff1))) is Relation-like set
K19(K20((Args (x,ff1)),(Result (x,ff1)))) is set
the Charact of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #), the ResultSort of Z * the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)
the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) # is Relation-like the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the Charact of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) . x is Relation-like Function-like set
Den (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) is Relation-like Args (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -defined Result (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) -valued Function-like quasi_total Element of K19(K20((Args (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)))))
Args (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) is Element of rng ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #)
rng ( the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) #) is non empty set
Result (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)) is Element of rng the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)
rng the Sorts of MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is non empty set
K20((Args (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #)))) is Relation-like set
K19(K20((Args (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))),(Result (x,MSAlgebra(# the Sorts of ff1, the Charact of ff1 #))))) is set
Opers (MSAlgebra(# the Sorts of ff1, the Charact of ff1 #),f) is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * (f #), the ResultSort of Z * f
f # is Relation-like the carrier of Z * -defined Function-like non empty total set
the Arity of Z * (f #) is Relation-like the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * f is Relation-like the carrier' of Z -defined Function-like non empty total set
(Opers (MSAlgebra(# the Sorts of ff1, the Charact of ff1 #),f)) . x is Relation-like Function-like set
x /. f is Relation-like ( the Arity of Z * (f #)) . x -defined ( the ResultSort of Z * f) . x -valued Function-like quasi_total Element of K19(K20((( the Arity of Z * (f #)) . x),(( the ResultSort of Z * f) . x)))
( the Arity of Z * (f #)) . x is set
( the ResultSort of Z * f) . x is set
K20((( the Arity of Z * (f #)) . x),(( the ResultSort of Z * f) . x)) is Relation-like set
K19(K20((( the Arity of Z * (f #)) . x),(( the ResultSort of Z * f) . x))) is set
( the Arity of Z * (f #)) . x is set
(Den (x,ff1)) | (( the Arity of Z * (f #)) . x) is Relation-like Args (x,ff1) -defined ( the Arity of Z * (f #)) . x -defined Args (x,ff1) -defined Result (x,ff1) -valued Function-like Element of K19(K20((Args (x,ff1)),(Result (x,ff1))))
x /. f is Relation-like ( the Arity of Z * (f #)) . x -defined ( the ResultSort of Z * f) . x -valued Function-like quasi_total Element of K19(K20((( the Arity of Z * (f #)) . x),(( the ResultSort of Z * f) . x)))
( the ResultSort of Z * f) . x is set
K20((( the Arity of Z * (f #)) . x),(( the ResultSort of Z * f) . x)) is Relation-like set
K19(K20((( the Arity of Z * (f #)) . x),(( the ResultSort of Z * f) . x))) is set
(Opers (ff1,f)) . x is Relation-like Function-like set
Z is non empty partial quasi_total non-empty UAStr
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
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
dom (signature Z) is Element of K19(NAT)
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} *)))
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} *)))
ff1 is Relation-like dom (signature Z) -defined {0} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20((dom (signature Z)),({0} *)))
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
ManySortedSign(# {0},(dom (signature Z)),ff1,((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} *)))
(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
ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is non empty V70() strict ManySortedSign
f is V26() V27() V28() V32() set
(signature Z) . f is set
dom ((*--> 0) * (signature Z)) is set
(signature A) . f is set
(*--> 0) . ((signature A) . f) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
((*--> 0) * (signature Z)) . f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(*--> 0) . ((signature Z) . f) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
x is V26() V27() V28() V32() Element of NAT
(*--> 0) . x is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of {0} *
f is V26() V27() V28() V32() Element of NAT
(*--> 0) . f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of {0} *
C is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len C is V26() V27() V28() V32() Element of NAT
y is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
len y is V26() V27() V28() V32() Element of NAT
Z is non empty partial quasi_total non-empty UAStr
signature Z is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
A is non empty partial quasi_total non-empty UAStr
signature A is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
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
Z is non empty partial quasi_total non-empty UAStr
signature Z is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
A is non empty partial quasi_total non-empty UAStr
signature A is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
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
ff1 is non empty partial quasi_total non-empty UAStr
MSSign ff1 is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
f is non empty partial quasi_total non-empty UAStr
MSSign f is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
signature ff1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
signature f is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
Z is non empty trivial V64() non void 1 -element V70() segmental ManySortedSign
the carrier of Z is non empty trivial V33() set
the carrier' of Z is non empty set
the Arity of Z is Relation-like the carrier' of Z -defined the carrier of Z * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of Z,( the carrier of Z *)))
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
K20( the carrier' of Z,( the carrier of Z *)) is Relation-like set
K19(K20( the carrier' of Z,( the carrier of Z *))) is set
the ResultSort of Z is Relation-like the carrier' of Z -defined the carrier of Z -valued Function-like quasi_total Element of K19(K20( the carrier' of Z, the carrier of Z))
K20( the carrier' of Z, the carrier of Z) is Relation-like set
K19(K20( the carrier' of Z, the carrier of Z)) is set
ManySortedSign(# the carrier of Z, the carrier' of Z, the Arity of Z, the ResultSort of Z #) is non empty V70() strict ManySortedSign
A is non-empty MSAlgebra over Z
1-Alg A is non empty strict partial quasi_total non-empty UAStr
MSSign (1-Alg A) is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
signature (1-Alg A) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
dom (signature (1-Alg A)) is Element of K19(NAT)
K20((dom (signature (1-Alg A))),({0} *)) is Relation-like set
K19(K20((dom (signature (1-Alg A))),({0} *))) is set
(*--> 0) * (signature (1-Alg A)) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V25() Element of K19(K20(NAT,({0} *)))
ff1 is Relation-like dom (signature (1-Alg A)) -defined {0} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20((dom (signature (1-Alg A))),({0} *)))
z is Relation-like Function-like Element of {0}
(dom (signature (1-Alg A))) --> z is Relation-like dom (signature (1-Alg A)) -defined {0} -valued Function-like constant total quasi_total Function-yielding V25() Element of K19(K20((dom (signature (1-Alg A))),{0}))
K20((dom (signature (1-Alg A))),{0}) is Relation-like set
K19(K20((dom (signature (1-Alg A))),{0})) is set
{z} is functional non empty set
K20((dom (signature (1-Alg A))),{z}) is Relation-like set
ManySortedSign(# {0},(dom (signature (1-Alg A))),ff1,((dom (signature (1-Alg A))) --> z) #) is non empty V70() strict ManySortedSign
dom the ResultSort of Z is set
rng the ResultSort of Z is set
f is V26() V27() V28() V32() set
Seg f is V33() V40(f) Element of K19(NAT)
the_sort_of A is non empty set
the_charact_of A is Relation-like NAT -defined PFuncs (((the_sort_of A) *),(the_sort_of A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))
(the_sort_of A) * is functional non empty FinSequence-membered FinSequenceSet of the_sort_of A
PFuncs (((the_sort_of A) *),(the_sort_of A)) is set
UAStr(# (the_sort_of A),(the_charact_of A) #) is non empty strict UAStr
len (signature (1-Alg A)) is V26() V27() V28() V32() Element of NAT
the charact of (1-Alg A) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A))
the carrier of (1-Alg A) is non empty set
the carrier of (1-Alg A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (1-Alg A)
PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) is set
len the charact of (1-Alg A) is V26() V27() V28() V32() Element of NAT
dom the charact of (1-Alg A) is non empty Element of K19(NAT)
the Charact of A is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of A #), the ResultSort of Z * the Sorts of A
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of Z -defined Function-like non empty total set
the Sorts of A # is Relation-like non-empty non empty-yielding the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of A #) is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
dom the Charact of A is non empty set
dom ff1 is set
f is set
((*--> 0) * (signature (1-Alg A))) . f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
the Arity of Z . f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
f is Element of the carrier' of Z
x is V26() V27() V28() V32() set
K20(( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) is Relation-like set
K19(K20(( the carrier of (1-Alg A) *), the carrier of (1-Alg A))) is set
the charact of (1-Alg A) . x is Relation-like Function-like homogeneous set
y is Relation-like the carrier of (1-Alg A) * -defined the carrier of (1-Alg A) -valued Function-like Element of K19(K20(( the carrier of (1-Alg A) *), the carrier of (1-Alg A)))
C is Relation-like the carrier of (1-Alg A) * -defined the carrier of (1-Alg A) -valued Function-like non empty homogeneous quasi_total Element of K19(K20(( the carrier of (1-Alg A) *), the carrier of (1-Alg A)))
dom C is functional non empty FinSequence-membered with_common_domain set
the Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of dom C is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of dom C
arity C is V26() V27() V28() V32() Element of NAT
A2 is Relation-like NAT -defined the carrier of (1-Alg A) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (1-Alg A)
the Charact of A . f is Relation-like Function-like set
Den (f,A) is Relation-like Args (f,A) -defined Result (f,A) -valued Function-like quasi_total Element of K19(K20((Args (f,A)),(Result (f,A))))
Args (f,A) is non empty Element of rng ( the Sorts of A #)
rng ( the Sorts of A #) is non empty V45() set
Result (f,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty V45() set
K20((Args (f,A)),(Result (f,A))) is Relation-like set
K19(K20((Args (f,A)),(Result (f,A)))) is set
the_arity_of f is Relation-like NAT -defined the carrier of Z -valued Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of Z *
len (the_arity_of f) is V26() V27() V28() V32() Element of NAT
(len (the_arity_of f)) -tuples_on (the_sort_of A) is functional non empty FinSequence-membered FinSequenceSet of the_sort_of A
{ b1 where b1 is Relation-like NAT -defined the_sort_of A -valued Function-like V33() FinSequence-like FinSubsequence-like Element of (the_sort_of A) * : len b1 = len (the_arity_of f) } is set
len A2 is V26() V27() V28() V32() Element of NAT
((*--> 0) * (signature (1-Alg A))) . f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(signature (1-Alg A)) . f is set
(*--> 0) . ((signature (1-Alg A)) . f) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(*--> 0) . (arity C) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of {0} *
(arity C) |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V33() V40( arity C) FinSequence-like FinSubsequence-like Element of (arity C) -tuples_on NAT
(arity C) -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 = arity C } is set
Seg (arity C) is V33() V40( arity C) Element of K19(NAT)
(Seg (arity C)) --> 0 is Relation-like Seg (arity C) -defined Seg (arity C) -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 (arity C)),{0}))
K20((Seg (arity C)),{0}) is Relation-like set
K19(K20((Seg (arity C)),{0})) is set
the Arity of Z . f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of Z *
dom the Arity of Z is set
the carrier' of (MSSign (1-Alg A)) is non empty set
the carrier of (MSSign (1-Alg A)) is non empty trivial V33() set
the ResultSort of (MSSign (1-Alg A)) is Relation-like the carrier' of (MSSign (1-Alg A)) -defined the carrier of (MSSign (1-Alg A)) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign (1-Alg A)), the carrier of (MSSign (1-Alg A))))
K20( the carrier' of (MSSign (1-Alg A)), the carrier of (MSSign (1-Alg A))) is Relation-like set
K19(K20( the carrier' of (MSSign (1-Alg A)), the carrier of (MSSign (1-Alg A)))) is set
Z is non empty trivial V64() non void 1 -element V70() segmental ManySortedSign
A is non-empty MSAlgebra over Z
1-Alg A is non empty strict partial quasi_total non-empty UAStr
ff1 is non-empty MSAlgebra over Z
1-Alg ff1 is non empty strict partial quasi_total non-empty UAStr
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of Z -defined Function-like non empty total set
the carrier of Z is non empty trivial V33() set
the Charact of A is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of A #), the ResultSort of Z * the Sorts of A
the carrier' of Z is non empty set
the Arity of Z is Relation-like the carrier' of Z -defined the carrier of Z * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of Z,( the carrier of Z *)))
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
K20( the carrier' of Z,( the carrier of Z *)) is Relation-like set
K19(K20( the carrier' of Z,( the carrier of Z *))) is set
the Sorts of A # is Relation-like non-empty non empty-yielding the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of A #) is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z is Relation-like the carrier' of Z -defined the carrier of Z -valued Function-like quasi_total Element of K19(K20( the carrier' of Z, the carrier of Z))
K20( the carrier' of Z, the carrier of Z) is Relation-like set
K19(K20( the carrier' of Z, the carrier of Z)) is set
the ResultSort of Z * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
MSAlgebra(# the Sorts of A, the Charact of A #) is strict non-empty MSAlgebra over Z
the Sorts of ff1 is Relation-like non-empty non empty-yielding the carrier of Z -defined Function-like non empty total set
the Charact of ff1 is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of ff1 #), the ResultSort of Z * the Sorts of ff1
the Sorts of ff1 # is Relation-like non-empty non empty-yielding the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of ff1 #) is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * the Sorts of ff1 is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
MSAlgebra(# the Sorts of ff1, the Charact of ff1 #) is strict non-empty MSAlgebra over Z
the_sort_of ff1 is non empty set
the_charact_of ff1 is Relation-like NAT -defined PFuncs (((the_sort_of ff1) *),(the_sort_of ff1)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((the_sort_of ff1) *),(the_sort_of ff1))
(the_sort_of ff1) * is functional non empty FinSequence-membered FinSequenceSet of the_sort_of ff1
PFuncs (((the_sort_of ff1) *),(the_sort_of ff1)) is set
UAStr(# (the_sort_of ff1),(the_charact_of ff1) #) is non empty strict UAStr
the_sort_of A is non empty set
the_charact_of A is Relation-like NAT -defined PFuncs (((the_sort_of A) *),(the_sort_of A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))
(the_sort_of A) * is functional non empty FinSequence-membered FinSequenceSet of the_sort_of A
PFuncs (((the_sort_of A) *),(the_sort_of A)) is set
UAStr(# (the_sort_of A),(the_charact_of A) #) is non empty strict UAStr
f is set
rng the Sorts of ff1 is non empty V45() set
the Sorts of ff1 . f is set
f is non empty Element of rng the Sorts of ff1
rng the Sorts of A is non empty V45() set
the Sorts of A . f is set
f is non empty Element of rng the Sorts of A
f is non empty Element of rng the Sorts of A
f is non empty Element of rng the Sorts of ff1
the charact of (1-Alg A) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A))
the carrier of (1-Alg A) is non empty set
the carrier of (1-Alg A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (1-Alg A)
PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) is set
Z is non empty trivial V64() non void 1 -element V70() segmental ManySortedSign
the carrier of Z is non empty trivial V33() set
A is non-empty MSAlgebra over Z
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of Z -defined Function-like non empty total set
1-Alg A is non empty strict partial quasi_total non-empty UAStr
MSSign (1-Alg A) is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSAlg (1-Alg A) is strict non-empty MSAlgebra over MSSign (1-Alg A)
the Sorts of (MSAlg (1-Alg A)) is Relation-like non-empty non empty-yielding the carrier of (MSSign (1-Alg A)) -defined Function-like non empty total set
the carrier of (MSSign (1-Alg A)) is non empty trivial V33() set
ff1 is set
rng the Sorts of A is non empty V45() set
the Sorts of A . ff1 is set
f is non empty Element of rng the Sorts of A
the_sort_of A is non empty set
{0} --> (the_sort_of A) is Relation-like non-empty non empty-yielding {0} -defined {(the_sort_of A)} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{(the_sort_of A)}))
{(the_sort_of A)} is non empty set
K20({0},{(the_sort_of A)}) is Relation-like set
K19(K20({0},{(the_sort_of A)})) is set
({0} --> (the_sort_of A)) . ff1 is set
f is non empty Element of rng the Sorts of A
the_charact_of A is Relation-like NAT -defined PFuncs (((the_sort_of A) *),(the_sort_of A)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))
(the_sort_of A) * is functional non empty FinSequence-membered FinSequenceSet of the_sort_of A
PFuncs (((the_sort_of A) *),(the_sort_of A)) is set
UAStr(# (the_sort_of A),(the_charact_of A) #) is non empty strict UAStr
MSSorts (1-Alg A) is Relation-like non-empty non empty-yielding the carrier of (MSSign (1-Alg A)) -defined Function-like non empty total set
MSCharact (1-Alg A) is Relation-like the carrier' of (MSSign (1-Alg A)) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign (1-Alg A)) * ((MSSorts (1-Alg A)) #), the ResultSort of (MSSign (1-Alg A)) * (MSSorts (1-Alg A))
the carrier' of (MSSign (1-Alg A)) is non empty set
the Arity of (MSSign (1-Alg A)) is Relation-like the carrier' of (MSSign (1-Alg A)) -defined the carrier of (MSSign (1-Alg A)) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign (1-Alg A)),( the carrier of (MSSign (1-Alg A)) *)))
the carrier of (MSSign (1-Alg A)) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign (1-Alg A))
K20( the carrier' of (MSSign (1-Alg A)),( the carrier of (MSSign (1-Alg A)) *)) is Relation-like set
K19(K20( the carrier' of (MSSign (1-Alg A)),( the carrier of (MSSign (1-Alg A)) *))) is set
(MSSorts (1-Alg A)) # is Relation-like non-empty non empty-yielding the carrier of (MSSign (1-Alg A)) * -defined Function-like non empty total set
the Arity of (MSSign (1-Alg A)) * ((MSSorts (1-Alg A)) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign (1-Alg A)) -defined Function-like non empty total set
the ResultSort of (MSSign (1-Alg A)) is Relation-like the carrier' of (MSSign (1-Alg A)) -defined the carrier of (MSSign (1-Alg A)) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign (1-Alg A)), the carrier of (MSSign (1-Alg A))))
K20( the carrier' of (MSSign (1-Alg A)), the carrier of (MSSign (1-Alg A))) is Relation-like set
K19(K20( the carrier' of (MSSign (1-Alg A)), the carrier of (MSSign (1-Alg A)))) is set
the ResultSort of (MSSign (1-Alg A)) * (MSSorts (1-Alg A)) is Relation-like non-empty non empty-yielding the carrier' of (MSSign (1-Alg A)) -defined Function-like non empty total set
MSAlgebra(# (MSSorts (1-Alg A)),(MSCharact (1-Alg A)) #) is strict MSAlgebra over MSSign (1-Alg A)
0 .--> (the_sort_of A) is Relation-like NAT -defined {0} -defined Function-like one-to-one set
Z is non empty trivial V64() non void 1 -element V70() segmental ManySortedSign
the carrier of Z is non empty trivial V33() set
A is non-empty MSAlgebra over Z
1-Alg A is non empty strict partial quasi_total non-empty UAStr
MSAlg (1-Alg A) is strict non-empty MSAlgebra over MSSign (1-Alg A)
MSSign (1-Alg A) is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of Z -defined Function-like non empty total set
the Charact of A is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of A #), the ResultSort of Z * the Sorts of A
the carrier' of Z is non empty set
the Arity of Z is Relation-like the carrier' of Z -defined the carrier of Z * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of Z,( the carrier of Z *)))
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
K20( the carrier' of Z,( the carrier of Z *)) is Relation-like set
K19(K20( the carrier' of Z,( the carrier of Z *))) is set
the Sorts of A # is Relation-like non-empty non empty-yielding the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of A #) is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z is Relation-like the carrier' of Z -defined the carrier of Z -valued Function-like quasi_total Element of K19(K20( the carrier' of Z, the carrier of Z))
K20( the carrier' of Z, the carrier of Z) is Relation-like set
K19(K20( the carrier' of Z, the carrier of Z)) is set
the ResultSort of Z * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
MSAlgebra(# the Sorts of A, the Charact of A #) is strict non-empty MSAlgebra over Z
the Sorts of (MSAlg (1-Alg A)) is Relation-like non-empty non empty-yielding the carrier of (MSSign (1-Alg A)) -defined Function-like non empty total set
the carrier of (MSSign (1-Alg A)) is non empty trivial V33() set
rng the Sorts of (MSAlg (1-Alg A)) is non empty V45() set
the_sort_of (MSAlg (1-Alg A)) is non empty set
ManySortedSign(# the carrier of Z, the carrier' of Z, the Arity of Z, the ResultSort of Z #) is non empty V70() strict ManySortedSign
f is strict MSAlgebra over Z
f is strict non-empty MSAlgebra over Z
1-Alg f is non empty strict partial quasi_total non-empty UAStr
the_sort_of f is non empty set
the_charact_of f is Relation-like NAT -defined PFuncs (((the_sort_of f) *),(the_sort_of f)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((the_sort_of f) *),(the_sort_of f))
(the_sort_of f) * is functional non empty FinSequence-membered FinSequenceSet of the_sort_of f
PFuncs (((the_sort_of f) *),(the_sort_of f)) is set
UAStr(# (the_sort_of f),(the_charact_of f) #) is non empty strict UAStr
the Sorts of f is Relation-like non-empty non empty-yielding the carrier of Z -defined Function-like non empty total set
rng the Sorts of f is non empty V45() set
ff1 is non empty Element of rng the Sorts of (MSAlg (1-Alg A))
1-Alg (MSAlg (1-Alg A)) is non empty strict partial quasi_total non-empty UAStr
the_charact_of (MSAlg (1-Alg A)) is Relation-like NAT -defined PFuncs (((the_sort_of (MSAlg (1-Alg A))) *),(the_sort_of (MSAlg (1-Alg A)))) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((the_sort_of (MSAlg (1-Alg A))) *),(the_sort_of (MSAlg (1-Alg A))))
(the_sort_of (MSAlg (1-Alg A))) * is functional non empty FinSequence-membered FinSequenceSet of the_sort_of (MSAlg (1-Alg A))
PFuncs (((the_sort_of (MSAlg (1-Alg A))) *),(the_sort_of (MSAlg (1-Alg A)))) is set
UAStr(# (the_sort_of (MSAlg (1-Alg A))),(the_charact_of (MSAlg (1-Alg A))) #) is non empty strict UAStr
the charact of (1-Alg A) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A))
the carrier of (1-Alg A) is non empty set
the carrier of (1-Alg A) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (1-Alg A)
PFuncs (( the carrier of (1-Alg A) *), the carrier of (1-Alg A)) is set
the Charact of f is Relation-like the carrier' of Z -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of Z * ( the Sorts of f #), the ResultSort of Z * the Sorts of f
the Sorts of f # is Relation-like non-empty non empty-yielding the carrier of Z * -defined Function-like non empty total set
the Arity of Z * ( the Sorts of f #) is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
the ResultSort of Z * the Sorts of f is Relation-like non-empty non empty-yielding the carrier' of Z -defined Function-like non empty total set
the charact of (1-Alg f) is Relation-like non-empty NAT -defined PFuncs (( the carrier of (1-Alg f) *), the carrier of (1-Alg f)) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (1-Alg f) *), the carrier of (1-Alg f))
the carrier of (1-Alg f) is non empty set
the carrier of (1-Alg f) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (1-Alg f)
PFuncs (( the carrier of (1-Alg f) *), the carrier of (1-Alg f)) is set
f is non empty Element of rng the Sorts of f
Z 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 carrier of (MSSign Z) is non empty trivial V33() set
A is strict non-empty MSSubAlgebra of MSAlg Z
1-Alg A is non empty strict partial quasi_total non-empty UAStr
MSAlg (1-Alg A) is strict non-empty MSAlgebra over MSSign (1-Alg A)
MSSign (1-Alg A) is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the Charact of A 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 A #), the ResultSort of (MSSign Z) * the Sorts of A
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 A # 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 A #) 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 A is Relation-like non-empty non empty-yielding the carrier' of (MSSign Z) -defined Function-like non empty total set
MSAlgebra(# the Sorts of A, the Charact of A #) is strict non-empty MSAlgebra over MSSign Z
Z 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 carrier of (MSSign Z) is non empty trivial V33() set
A is non empty strict partial quasi_total non-empty SubAlgebra of Z
MSAlg A is strict non-empty MSAlgebra over MSSign A
MSSign A is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
ff1 is non empty strict partial quasi_total non-empty SubAlgebra of Z
MSAlg ff1 is strict non-empty MSAlgebra over MSSign ff1
MSSign ff1 is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
the carrier of A is non empty set
the carrier of ff1 is non empty set
the carrier of A \/ the carrier of ff1 is non empty set
0 .--> ( the carrier of A \/ the carrier of ff1) is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> ( the carrier of A \/ the carrier of ff1) is Relation-like non-empty non empty-yielding {0} -defined {( the carrier of A \/ the carrier of ff1)} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{( the carrier of A \/ the carrier of ff1)}))
{( the carrier of A \/ the carrier of ff1)} is non empty set
K20({0},{( the carrier of A \/ the carrier of ff1)}) is Relation-like set
K19(K20({0},{( the carrier of A \/ the carrier of ff1)})) is set
f is strict non-empty MSSubAlgebra of MSAlg Z
f is strict non-empty MSSubAlgebra of MSAlg Z
the Sorts of f is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the Sorts of f is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the Sorts of f \/ the Sorts of f is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total 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
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
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)
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} *)))
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} *)))
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
ManySortedSign(# {0},(dom (signature Z)),f,((dom (signature Z)) --> z) #) is non empty V70() strict ManySortedSign
MSSorts ff1 is Relation-like non-empty non empty-yielding the carrier of (MSSign ff1) -defined Function-like non empty total set
the carrier of (MSSign ff1) is non empty trivial V33() set
MSCharact ff1 is Relation-like the carrier' of (MSSign ff1) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign ff1) * ((MSSorts ff1) #), the ResultSort of (MSSign ff1) * (MSSorts ff1)
the carrier' of (MSSign ff1) is non empty set
the Arity of (MSSign ff1) is Relation-like the carrier' of (MSSign ff1) -defined the carrier of (MSSign ff1) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign ff1),( the carrier of (MSSign ff1) *)))
the carrier of (MSSign ff1) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign ff1)
K20( the carrier' of (MSSign ff1),( the carrier of (MSSign ff1) *)) is Relation-like set
K19(K20( the carrier' of (MSSign ff1),( the carrier of (MSSign ff1) *))) is set
(MSSorts ff1) # is Relation-like non-empty non empty-yielding the carrier of (MSSign ff1) * -defined Function-like non empty total set
the Arity of (MSSign ff1) * ((MSSorts ff1) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign ff1) -defined Function-like non empty total set
the ResultSort of (MSSign ff1) is Relation-like the carrier' of (MSSign ff1) -defined the carrier of (MSSign ff1) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign ff1), the carrier of (MSSign ff1)))
K20( the carrier' of (MSSign ff1), the carrier of (MSSign ff1)) is Relation-like set
K19(K20( the carrier' of (MSSign ff1), the carrier of (MSSign ff1))) is set
the ResultSort of (MSSign ff1) * (MSSorts ff1) is Relation-like non-empty non empty-yielding the carrier' of (MSSign ff1) -defined Function-like non empty total set
MSAlgebra(# (MSSorts ff1),(MSCharact ff1) #) is strict MSAlgebra over MSSign ff1
y is set
x is Relation-like the carrier of (MSSign Z) -defined Function-like non empty total set
x . y is set
(0 .--> ( the carrier of A \/ the carrier of ff1)) . 0 is set
(0 .--> the carrier of A) . 0 is set
((0 .--> the carrier of A) . 0) \/ the carrier of ff1 is non empty set
0 .--> the carrier of ff1 is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> the carrier of ff1 is Relation-like non-empty non empty-yielding {0} -defined { the carrier of ff1} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{ the carrier of ff1}))
{ the carrier of ff1} is non empty set
K20({0},{ the carrier of ff1}) is Relation-like set
K19(K20({0},{ the carrier of ff1})) is set
(0 .--> the carrier of ff1) . 0 is set
((0 .--> the carrier of A) . 0) \/ ((0 .--> the carrier of ff1) . 0) is set
the Sorts of f . y is set
the Sorts of f . y is set
( the Sorts of f . y) \/ ( the Sorts of f . y) is set
Z 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 carrier of (MSSign Z) is non empty trivial V33() set
A is non empty strict partial quasi_total non-empty SubAlgebra of Z
MSAlg A is strict non-empty MSAlgebra over MSSign A
MSSign A is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
ff1 is non empty strict partial quasi_total non-empty SubAlgebra of Z
MSAlg ff1 is strict non-empty MSAlgebra over MSSign ff1
MSSign ff1 is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
the carrier of A is non empty set
the carrier of ff1 is non empty set
the carrier of A /\ the carrier of ff1 is set
0 .--> ( the carrier of A /\ the carrier of ff1) is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> ( the carrier of A /\ the carrier of ff1) is Relation-like {0} -defined {( the carrier of A /\ the carrier of ff1)} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{( the carrier of A /\ the carrier of ff1)}))
{( the carrier of A /\ the carrier of ff1)} is non empty set
K20({0},{( the carrier of A /\ the carrier of ff1)}) is Relation-like set
K19(K20({0},{( the carrier of A /\ the carrier of ff1)})) is set
f is strict non-empty MSSubAlgebra of MSAlg Z
f is strict non-empty MSSubAlgebra of MSAlg Z
the Sorts of f is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the Sorts of f is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the Sorts of f /\ the Sorts of f is Relation-like the carrier of (MSSign Z) -defined Function-like non empty total 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
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
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)
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} *)))
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} *)))
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
ManySortedSign(# {0},(dom (signature Z)),f,((dom (signature Z)) --> z) #) is non empty V70() strict ManySortedSign
MSSorts ff1 is Relation-like non-empty non empty-yielding the carrier of (MSSign ff1) -defined Function-like non empty total set
the carrier of (MSSign ff1) is non empty trivial V33() set
MSCharact ff1 is Relation-like the carrier' of (MSSign ff1) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign ff1) * ((MSSorts ff1) #), the ResultSort of (MSSign ff1) * (MSSorts ff1)
the carrier' of (MSSign ff1) is non empty set
the Arity of (MSSign ff1) is Relation-like the carrier' of (MSSign ff1) -defined the carrier of (MSSign ff1) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign ff1),( the carrier of (MSSign ff1) *)))
the carrier of (MSSign ff1) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign ff1)
K20( the carrier' of (MSSign ff1),( the carrier of (MSSign ff1) *)) is Relation-like set
K19(K20( the carrier' of (MSSign ff1),( the carrier of (MSSign ff1) *))) is set
(MSSorts ff1) # is Relation-like non-empty non empty-yielding the carrier of (MSSign ff1) * -defined Function-like non empty total set
the Arity of (MSSign ff1) * ((MSSorts ff1) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign ff1) -defined Function-like non empty total set
the ResultSort of (MSSign ff1) is Relation-like the carrier' of (MSSign ff1) -defined the carrier of (MSSign ff1) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign ff1), the carrier of (MSSign ff1)))
K20( the carrier' of (MSSign ff1), the carrier of (MSSign ff1)) is Relation-like set
K19(K20( the carrier' of (MSSign ff1), the carrier of (MSSign ff1))) is set
the ResultSort of (MSSign ff1) * (MSSorts ff1) is Relation-like non-empty non empty-yielding the carrier' of (MSSign ff1) -defined Function-like non empty total set
MSAlgebra(# (MSSorts ff1),(MSCharact ff1) #) is strict MSAlgebra over MSSign ff1
y is set
x is Relation-like the carrier of (MSSign Z) -defined Function-like non empty total set
x . y is set
(0 .--> the carrier of A) . 0 is set
((0 .--> the carrier of A) . 0) /\ the carrier of ff1 is set
0 .--> the carrier of ff1 is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> the carrier of ff1 is Relation-like non-empty non empty-yielding {0} -defined { the carrier of ff1} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{ the carrier of ff1}))
{ the carrier of ff1} is non empty set
K20({0},{ the carrier of ff1}) is Relation-like set
K19(K20({0},{ the carrier of ff1})) is set
(0 .--> the carrier of ff1) . 0 is set
((0 .--> the carrier of A) . 0) /\ ((0 .--> the carrier of ff1) . 0) is set
the Sorts of f . y is set
the Sorts of f . y is set
( the Sorts of f . y) /\ ( the Sorts of f . y) is set
Z is non empty strict 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
A is non empty strict partial quasi_total non-empty SubAlgebra of Z
MSAlg A is strict non-empty MSAlgebra over MSSign A
MSSign A is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
ff1 is non empty strict partial quasi_total non-empty SubAlgebra of Z
MSAlg ff1 is strict non-empty MSAlgebra over MSSign ff1
MSSign ff1 is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
A "\/" ff1 is non empty strict partial quasi_total non-empty SubAlgebra of Z
MSAlg (A "\/" ff1) is strict non-empty MSAlgebra over MSSign (A "\/" ff1)
MSSign (A "\/" ff1) is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
f is strict non-empty MSSubAlgebra of MSAlg Z
f is strict non-empty MSSubAlgebra of MSAlg Z
f "\/" f is strict MSSubAlgebra of MSAlg Z
f is MSSubAlgebra of MSAlg Z
the carrier of (MSSign Z) is non empty trivial V33() 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 Sorts of f is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the Sorts of f is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the Sorts of f \/ the Sorts of f is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
x is strict non-empty MSSubAlgebra of MSAlg Z
the carrier of A is non empty set
the carrier of Z is non empty set
K19( the carrier of Z) is set
the carrier of ff1 is non empty set
the carrier of A \/ the carrier of ff1 is non empty set
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)
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} *)))
the Sorts of x is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
C is Relation-like dom (signature Z) -defined {0} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20((dom (signature Z)),({0} *)))
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
ManySortedSign(# {0},(dom (signature Z)),C,((dom (signature Z)) --> z) #) is non empty V70() strict ManySortedSign
m is Relation-like the carrier of (MSSign Z) -defined Function-like non empty total ManySortedSubset of the Sorts of (MSAlg Z)
GenMSAlg m is strict MSSubAlgebra of MSAlg Z
g2 is MSSubAlgebra of MSAlg Z
the Sorts of g2 is Relation-like the carrier of (MSSign Z) -defined Function-like non empty total set
A4 is non-empty MSSubAlgebra of MSAlg Z
1-Alg A4 is non empty strict partial quasi_total non-empty UAStr
1-Alg (MSAlg Z) is non empty strict partial quasi_total non-empty UAStr
the Sorts of A4 is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
A2 is Element of the carrier of (MSSign Z)
m . A2 is set
the Sorts of A4 . A2 is non empty set
the Charact of A4 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 A4 #), the ResultSort of (MSSign Z) * the Sorts of A4
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 A4 # 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 A4 #) 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 A4 is Relation-like non-empty non empty-yielding the carrier' of (MSSign Z) -defined Function-like non empty total set
MSAlgebra(# the Sorts of A4, the Charact of A4 #) is strict non-empty MSAlgebra over MSSign Z
MSAlg (1-Alg A4) is strict non-empty MSAlgebra over MSSign (1-Alg A4)
MSSign (1-Alg A4) is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSSorts (1-Alg A4) is Relation-like non-empty non empty-yielding the carrier of (MSSign (1-Alg A4)) -defined Function-like non empty total set
the carrier of (MSSign (1-Alg A4)) is non empty trivial V33() set
MSCharact (1-Alg A4) is Relation-like the carrier' of (MSSign (1-Alg A4)) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign (1-Alg A4)) * ((MSSorts (1-Alg A4)) #), the ResultSort of (MSSign (1-Alg A4)) * (MSSorts (1-Alg A4))
the carrier' of (MSSign (1-Alg A4)) is non empty set
the Arity of (MSSign (1-Alg A4)) is Relation-like the carrier' of (MSSign (1-Alg A4)) -defined the carrier of (MSSign (1-Alg A4)) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign (1-Alg A4)),( the carrier of (MSSign (1-Alg A4)) *)))
the carrier of (MSSign (1-Alg A4)) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign (1-Alg A4))
K20( the carrier' of (MSSign (1-Alg A4)),( the carrier of (MSSign (1-Alg A4)) *)) is Relation-like set
K19(K20( the carrier' of (MSSign (1-Alg A4)),( the carrier of (MSSign (1-Alg A4)) *))) is set
(MSSorts (1-Alg A4)) # is Relation-like non-empty non empty-yielding the carrier of (MSSign (1-Alg A4)) * -defined Function-like non empty total set
the Arity of (MSSign (1-Alg A4)) * ((MSSorts (1-Alg A4)) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign (1-Alg A4)) -defined Function-like non empty total set
the ResultSort of (MSSign (1-Alg A4)) is Relation-like the carrier' of (MSSign (1-Alg A4)) -defined the carrier of (MSSign (1-Alg A4)) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign (1-Alg A4)), the carrier of (MSSign (1-Alg A4))))
K20( the carrier' of (MSSign (1-Alg A4)), the carrier of (MSSign (1-Alg A4))) is Relation-like set
K19(K20( the carrier' of (MSSign (1-Alg A4)), the carrier of (MSSign (1-Alg A4)))) is set
the ResultSort of (MSSign (1-Alg A4)) * (MSSorts (1-Alg A4)) is Relation-like non-empty non empty-yielding the carrier' of (MSSign (1-Alg A4)) -defined Function-like non empty total set
MSAlgebra(# (MSSorts (1-Alg A4)),(MSCharact (1-Alg A4)) #) is strict MSAlgebra over MSSign (1-Alg A4)
the Sorts of A4 . 0 is set
the carrier of (1-Alg A4) is non empty set
0 .--> the carrier of (1-Alg A4) is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> the carrier of (1-Alg A4) is Relation-like non-empty non empty-yielding {0} -defined { the carrier of (1-Alg A4)} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{ the carrier of (1-Alg A4)}))
{ the carrier of (1-Alg A4)} is non empty set
K20({0},{ the carrier of (1-Alg A4)}) is Relation-like set
K19(K20({0},{ the carrier of (1-Alg A4)})) is set
(0 .--> the carrier of (1-Alg A4)) . 0 is set
m . 0 is set
y is non empty Element of K19( the carrier of Z)
0 .--> y is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> y is Relation-like non-empty non empty-yielding {0} -defined {y} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{y}))
{y} is non empty set
K20({0},{y}) is Relation-like set
K19(K20({0},{y})) is set
(0 .--> y) . 0 is set
g3 is non empty strict partial quasi_total non-empty SubAlgebra of Z
the carrier of g3 is non empty set
GenUnivAlg y is non empty strict partial quasi_total non-empty SubAlgebra of Z
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
the Element of the carrier of A is Element of the carrier of A
A2 is Element of the carrier of (MSSign Z)
m . A2 is set
the Sorts of g2 . A2 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 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
A4 is Relation-like the carrier of (MSSign Z) -defined Function-like non empty total set
A4 \/ the Sorts of f is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
A4 . A2 is set
the Sorts of f . A2 is non empty set
(A4 . A2) \/ ( the Sorts of f . A2) is non empty set
g1 is set
the Sorts of g2 . g1 is set
MSSorts (A "\/" ff1) is Relation-like non-empty non empty-yielding the carrier of (MSSign (A "\/" ff1)) -defined Function-like non empty total set
the carrier of (MSSign (A "\/" ff1)) is non empty trivial V33() set
MSCharact (A "\/" ff1) is Relation-like the carrier' of (MSSign (A "\/" ff1)) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign (A "\/" ff1)) * ((MSSorts (A "\/" ff1)) #), the ResultSort of (MSSign (A "\/" ff1)) * (MSSorts (A "\/" ff1))
the carrier' of (MSSign (A "\/" ff1)) is non empty set
the Arity of (MSSign (A "\/" ff1)) is Relation-like the carrier' of (MSSign (A "\/" ff1)) -defined the carrier of (MSSign (A "\/" ff1)) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign (A "\/" ff1)),( the carrier of (MSSign (A "\/" ff1)) *)))
the carrier of (MSSign (A "\/" ff1)) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign (A "\/" ff1))
K20( the carrier' of (MSSign (A "\/" ff1)),( the carrier of (MSSign (A "\/" ff1)) *)) is Relation-like set
K19(K20( the carrier' of (MSSign (A "\/" ff1)),( the carrier of (MSSign (A "\/" ff1)) *))) is set
(MSSorts (A "\/" ff1)) # is Relation-like non-empty non empty-yielding the carrier of (MSSign (A "\/" ff1)) * -defined Function-like non empty total set
the Arity of (MSSign (A "\/" ff1)) * ((MSSorts (A "\/" ff1)) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign (A "\/" ff1)) -defined Function-like non empty total set
the ResultSort of (MSSign (A "\/" ff1)) is Relation-like the carrier' of (MSSign (A "\/" ff1)) -defined the carrier of (MSSign (A "\/" ff1)) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign (A "\/" ff1)), the carrier of (MSSign (A "\/" ff1))))
K20( the carrier' of (MSSign (A "\/" ff1)), the carrier of (MSSign (A "\/" ff1))) is Relation-like set
K19(K20( the carrier' of (MSSign (A "\/" ff1)), the carrier of (MSSign (A "\/" ff1)))) is set
the ResultSort of (MSSign (A "\/" ff1)) * (MSSorts (A "\/" ff1)) is Relation-like non-empty non empty-yielding the carrier' of (MSSign (A "\/" ff1)) -defined Function-like non empty total set
MSAlgebra(# (MSSorts (A "\/" ff1)),(MSCharact (A "\/" ff1)) #) is strict MSAlgebra over MSSign (A "\/" ff1)
the carrier of (A "\/" ff1) is non empty set
0 .--> the carrier of (A "\/" ff1) is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> the carrier of (A "\/" ff1) is Relation-like non-empty non empty-yielding {0} -defined { the carrier of (A "\/" ff1)} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{ the carrier of (A "\/" ff1)}))
{ the carrier of (A "\/" ff1)} is non empty set
K20({0},{ the carrier of (A "\/" ff1)}) is Relation-like set
K19(K20({0},{ the carrier of (A "\/" ff1)})) is set
y1 is Relation-like the carrier of (MSSign Z) -defined Function-like non empty total set
g2 is set
( the Sorts of f \/ the Sorts of f) . g2 is set
y1 . g2 is set
y is non empty Element of K19( the carrier of Z)
GenUnivAlg y is non empty strict partial quasi_total non-empty SubAlgebra of Z
(0 .--> the carrier of (A "\/" ff1)) . 0 is set
( the Sorts of f \/ the Sorts of f) . 0 is set
0 .--> ( the carrier of A \/ the carrier of ff1) is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> ( the carrier of A \/ the carrier of ff1) is Relation-like non-empty non empty-yielding {0} -defined {( the carrier of A \/ the carrier of ff1)} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{( the carrier of A \/ the carrier of ff1)}))
{( the carrier of A \/ the carrier of ff1)} is non empty set
K20({0},{( the carrier of A \/ the carrier of ff1)}) is Relation-like set
K19(K20({0},{( the carrier of A \/ the carrier of ff1)})) is set
(0 .--> ( the carrier of A \/ the carrier of ff1)) . 0 is set
Z is non empty partial quasi_total non-empty with_const_op UAStr
MSSign Z 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)
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} *)))
A is Relation-like dom (signature Z) -defined {0} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20((dom (signature Z)),({0} *)))
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
ManySortedSign(# {0},(dom (signature Z)),A,((dom (signature Z)) --> z) #) is non empty V70() strict ManySortedSign
the carrier of (MSSign Z) is non empty trivial V33() set
ff1 is Element of the carrier of (MSSign Z)
the carrier of Z is non empty set
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
Operations Z is non empty PFuncsDomHQN of the carrier of Z
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
rng the charact of Z is non empty V45() set
f is Relation-like the carrier of Z * -defined the carrier of Z -valued Function-like non empty homogeneous quasi_total Element of Operations Z
arity f is V26() V27() V28() V32() Element of NAT
len the charact of Z is V26() V27() V28() V32() Element of NAT
Seg (len the charact of Z) is V33() V40( len the charact of Z) Element of K19(NAT)
dom the charact of Z is non empty Element of K19(NAT)
f is V26() V27() V28() V32() set
the charact of Z . f is Relation-like Function-like homogeneous set
len (signature Z) is V26() V27() V28() V32() Element of NAT
the carrier' of (MSSign Z) is non empty set
f is Element of the carrier' of (MSSign Z)
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 Arity of (MSSign Z) . f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like 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) . f is set
(signature Z) . f is set
(*--> 0) . ((signature Z) . f) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like set
(*--> 0) . 0 is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of {0} *
the Arity of (MSSign Z) . f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like Element of the carrier of (MSSign Z) *
the ResultSort of (MSSign Z) . f is Element of the carrier of (MSSign Z)
Z is non empty partial quasi_total non-empty with_const_op UAStr
MSSign Z is non empty trivial V64() non void 1 -element V70() strict segmental all-with_const_op ManySortedSign
MSAlg Z is strict non-empty MSAlgebra over MSSign Z
A is non empty strict partial quasi_total non-empty SubAlgebra of Z
MSAlg A is strict non-empty MSAlgebra over MSSign A
MSSign A is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
ff1 is non empty strict partial quasi_total non-empty SubAlgebra of Z
MSAlg ff1 is strict non-empty MSAlgebra over MSSign ff1
MSSign ff1 is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
A /\ ff1 is non empty strict partial quasi_total non-empty SubAlgebra of Z
MSAlg (A /\ ff1) is strict non-empty MSAlgebra over MSSign (A /\ ff1)
MSSign (A /\ ff1) 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)
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} *)))
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} *)))
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
ManySortedSign(# {0},(dom (signature Z)),f,((dom (signature Z)) --> z) #) is non empty V70() strict ManySortedSign
MSSorts (A /\ ff1) is Relation-like non-empty non empty-yielding the carrier of (MSSign (A /\ ff1)) -defined Function-like non empty total set
the carrier of (MSSign (A /\ ff1)) is non empty trivial V33() set
MSCharact (A /\ ff1) is Relation-like the carrier' of (MSSign (A /\ ff1)) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign (A /\ ff1)) * ((MSSorts (A /\ ff1)) #), the ResultSort of (MSSign (A /\ ff1)) * (MSSorts (A /\ ff1))
the carrier' of (MSSign (A /\ ff1)) is non empty set
the Arity of (MSSign (A /\ ff1)) is Relation-like the carrier' of (MSSign (A /\ ff1)) -defined the carrier of (MSSign (A /\ ff1)) * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20( the carrier' of (MSSign (A /\ ff1)),( the carrier of (MSSign (A /\ ff1)) *)))
the carrier of (MSSign (A /\ ff1)) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (MSSign (A /\ ff1))
K20( the carrier' of (MSSign (A /\ ff1)),( the carrier of (MSSign (A /\ ff1)) *)) is Relation-like set
K19(K20( the carrier' of (MSSign (A /\ ff1)),( the carrier of (MSSign (A /\ ff1)) *))) is set
(MSSorts (A /\ ff1)) # is Relation-like non-empty non empty-yielding the carrier of (MSSign (A /\ ff1)) * -defined Function-like non empty total set
the Arity of (MSSign (A /\ ff1)) * ((MSSorts (A /\ ff1)) #) is Relation-like non-empty non empty-yielding the carrier' of (MSSign (A /\ ff1)) -defined Function-like non empty total set
the ResultSort of (MSSign (A /\ ff1)) is Relation-like the carrier' of (MSSign (A /\ ff1)) -defined the carrier of (MSSign (A /\ ff1)) -valued Function-like quasi_total Element of K19(K20( the carrier' of (MSSign (A /\ ff1)), the carrier of (MSSign (A /\ ff1))))
K20( the carrier' of (MSSign (A /\ ff1)), the carrier of (MSSign (A /\ ff1))) is Relation-like set
K19(K20( the carrier' of (MSSign (A /\ ff1)), the carrier of (MSSign (A /\ ff1)))) is set
the ResultSort of (MSSign (A /\ ff1)) * (MSSorts (A /\ ff1)) is Relation-like non-empty non empty-yielding the carrier' of (MSSign (A /\ ff1)) -defined Function-like non empty total set
MSAlgebra(# (MSSorts (A /\ ff1)),(MSCharact (A /\ ff1)) #) is strict MSAlgebra over MSSign (A /\ ff1)
the Sorts of (MSAlg (A /\ ff1)) is Relation-like non-empty non empty-yielding the carrier of (MSSign (A /\ ff1)) -defined Function-like non empty total set
the carrier of (A /\ ff1) is non empty set
0 .--> the carrier of (A /\ ff1) is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> the carrier of (A /\ ff1) is Relation-like non-empty non empty-yielding {0} -defined { the carrier of (A /\ ff1)} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{ the carrier of (A /\ ff1)}))
{ the carrier of (A /\ ff1)} is non empty set
K20({0},{ the carrier of (A /\ ff1)}) is Relation-like set
K19(K20({0},{ the carrier of (A /\ ff1)})) is set
dom the Sorts of (MSAlg (A /\ ff1)) is non empty set
the carrier of (MSSign Z) is non empty trivial V33() set
f is strict non-empty MSSubAlgebra of MSAlg Z
x is strict non-empty MSSubAlgebra of MSAlg Z
f /\ x is strict MSSubAlgebra of MSAlg Z
the carrier of A is non empty set
the carrier of ff1 is non empty set
y is set
f is Relation-like the carrier of (MSSign Z) -defined Function-like non empty total set
f . y is set
(0 .--> the carrier of (A /\ ff1)) . 0 is set
the carrier of A /\ the carrier of ff1 is set
0 .--> ( the carrier of A /\ the carrier of ff1) is Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> ( the carrier of A /\ the carrier of ff1) is Relation-like {0} -defined {( the carrier of A /\ the carrier of ff1)} -valued Function-like constant non empty total quasi_total Element of K19(K20({0},{( the carrier of A /\ the carrier of ff1)}))
{( the carrier of A /\ the carrier of ff1)} is non empty set
K20({0},{( the carrier of A /\ the carrier of ff1)}) is Relation-like set
K19(K20({0},{( the carrier of A /\ the carrier of ff1)})) is set
(0 .--> ( the carrier of A /\ the carrier of ff1)) . 0 is set
the Sorts of f is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the Sorts of x is Relation-like non-empty non empty-yielding the carrier of (MSSign Z) -defined Function-like non empty total set
the Sorts of f /\ the Sorts of x is Relation-like the carrier of (MSSign Z) -defined Function-like non empty total set
( the Sorts of f /\ the Sorts of x) . 0 is set
( the Sorts of f /\ the Sorts of x) . y 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
y is strict non-empty MSSubAlgebra of MSAlg Z
the Sorts of y 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 set
the Charact of y 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 y #), the ResultSort of (MSSign Z) * the Sorts of y
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 y # 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 y #) 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 y is Relation-like non-empty non empty-yielding the carrier' of (MSSign Z) -defined Function-like non empty total set
C is Relation-like the carrier of (MSSign Z) -defined Function-like non empty total ManySortedSubset of the Sorts of (MSAlg Z)
Opers ((MSAlg Z),C) is Relation-like the carrier' of (MSSign Z) -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of (MSSign Z) * (C #), the ResultSort of (MSSign Z) * C
C # is Relation-like the carrier of (MSSign Z) * -defined Function-like non empty total set
the Arity of (MSSign Z) * (C #) is Relation-like the carrier' of (MSSign Z) -defined Function-like non empty total set
the ResultSort of (MSSign Z) * C is Relation-like the carrier' of (MSSign Z) -defined Function-like non empty total set
Z is quasi_total UAStr
the carrier of Z is set
the charact of Z is Relation-like NAT -defined PFuncs (( the carrier of Z *), the carrier of Z) -valued Function-like V33() FinSequence-like FinSubsequence-like quasi_total FinSequence of PFuncs (( the carrier of Z *), the carrier of Z)
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
PFuncs (( the carrier of Z *), the carrier of Z) is set
UAStr(# the carrier of Z, the charact of Z #) is strict UAStr
the carrier of UAStr(# the carrier of Z, the charact of Z #) is set
the charact of UAStr(# the carrier of Z, the charact of Z #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# the carrier of Z, the charact of Z #) *), the carrier of UAStr(# the carrier of Z, the charact of Z #)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# the carrier of Z, the charact of Z #) *), the carrier of UAStr(# the carrier of Z, the charact of Z #))
the carrier of UAStr(# the carrier of Z, the charact of Z #) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of UAStr(# the carrier of Z, the charact of Z #)
PFuncs (( the carrier of UAStr(# the carrier of Z, the charact of Z #) *), the carrier of UAStr(# the carrier of Z, the charact of Z #)) is set
Z is partial UAStr
the carrier of Z is set
the charact of Z is Relation-like NAT -defined PFuncs (( the carrier of Z *), the carrier of Z) -valued Function-like V33() FinSequence-like FinSubsequence-like homogeneous FinSequence of PFuncs (( the carrier of Z *), the carrier of Z)
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
PFuncs (( the carrier of Z *), the carrier of Z) is set
UAStr(# the carrier of Z, the charact of Z #) is strict UAStr
the carrier of UAStr(# the carrier of Z, the charact of Z #) is set
the charact of UAStr(# the carrier of Z, the charact of Z #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# the carrier of Z, the charact of Z #) *), the carrier of UAStr(# the carrier of Z, the charact of Z #)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# the carrier of Z, the charact of Z #) *), the carrier of UAStr(# the carrier of Z, the charact of Z #))
the carrier of UAStr(# the carrier of Z, the charact of Z #) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of UAStr(# the carrier of Z, the charact of Z #)
PFuncs (( the carrier of UAStr(# the carrier of Z, the charact of Z #) *), the carrier of UAStr(# the carrier of Z, the charact of Z #)) is set
Z is non-empty UAStr
the carrier of Z 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 V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of Z *), the carrier of Z)
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
PFuncs (( the carrier of Z *), the carrier of Z) is set
UAStr(# the carrier of Z, the charact of Z #) is strict UAStr
the charact of UAStr(# the carrier of Z, the charact of Z #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# the carrier of Z, the charact of Z #) *), the carrier of UAStr(# the carrier of Z, the charact of Z #)) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# the carrier of Z, the charact of Z #) *), the carrier of UAStr(# the carrier of Z, the charact of Z #))
the carrier of UAStr(# the carrier of Z, the charact of Z #) is set
the carrier of UAStr(# the carrier of Z, the charact of Z #) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of UAStr(# the carrier of Z, the charact of Z #)
PFuncs (( the carrier of UAStr(# the carrier of Z, the charact of Z #) *), the carrier of UAStr(# the carrier of Z, the charact of Z #)) is set
Z is non empty partial quasi_total non-empty with_const_op UAStr
the carrier of Z is non empty 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)
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
PFuncs (( the carrier of Z *), the carrier of Z) is set
UAStr(# the carrier of Z, the charact of Z #) is non empty strict partial quasi_total non-empty UAStr
Operations Z is non empty PFuncsDomHQN of the carrier of Z
rng the charact of Z is non empty V45() set
A is Relation-like the carrier of Z * -defined the carrier of Z -valued Function-like non empty homogeneous quasi_total Element of Operations Z
arity A is V26() V27() V28() V32() Element of NAT
the carrier of UAStr(# the carrier of Z, the charact of Z #) is non empty set
the carrier of UAStr(# the carrier of Z, the charact of Z #) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of UAStr(# the carrier of Z, the charact of Z #)
Operations UAStr(# the carrier of Z, the charact of Z #) is non empty PFuncsDomHQN of the carrier of UAStr(# the carrier of Z, the charact of Z #)
the charact of UAStr(# the carrier of Z, the charact of Z #) is Relation-like non-empty NAT -defined PFuncs (( the carrier of UAStr(# the carrier of Z, the charact of Z #) *), the carrier of UAStr(# the carrier of Z, the charact of Z #)) -valued Function-like non empty Function-yielding V25() V33() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of UAStr(# the carrier of Z, the charact of Z #) *), the carrier of UAStr(# the carrier of Z, the charact of Z #))
PFuncs (( the carrier of UAStr(# the carrier of Z, the charact of Z #) *), the carrier of UAStr(# the carrier of Z, the charact of Z #)) is set
rng the charact of UAStr(# the carrier of Z, the charact of Z #) is non empty V45() set
ff1 is Relation-like the carrier of UAStr(# the carrier of Z, the charact of Z #) * -defined the carrier of UAStr(# the carrier of Z, the charact of Z #) -valued Function-like non empty homogeneous quasi_total Element of Operations UAStr(# the carrier of Z, the charact of Z #)
arity ff1 is V26() V27() V28() V32() Element of NAT
Z is non empty partial quasi_total non-empty with_const_op UAStr
the carrier of Z is non empty 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)
the carrier of Z * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z
PFuncs (( the carrier of Z *), the carrier of Z) is set
UAStr(# the carrier of Z, the charact of Z #) is non empty strict partial quasi_total non-empty with_const_op UAStr
UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #) is non empty strict Lattice-like LattStr
Sub UAStr(# the carrier of Z, the charact of Z #) is non empty set
UniAlg_join UAStr(# the carrier of Z, the charact of Z #) is Relation-like K20((Sub UAStr(# the carrier of Z, the charact of Z #)),(Sub UAStr(# the carrier of Z, the charact of Z #))) -defined Sub UAStr(# the carrier of Z, the charact of Z #) -valued Function-like quasi_total Element of K19(K20(K20((Sub UAStr(# the carrier of Z, the charact of Z #)),(Sub UAStr(# the carrier of Z, the charact of Z #))),(Sub UAStr(# the carrier of Z, the charact of Z #))))
K20((Sub UAStr(# the carrier of Z, the charact of Z #)),(Sub UAStr(# the carrier of Z, the charact of Z #))) is Relation-like set
K20(K20((Sub UAStr(# the carrier of Z, the charact of Z #)),(Sub UAStr(# the carrier of Z, the charact of Z #))),(Sub UAStr(# the carrier of Z, the charact of Z #))) is Relation-like set
K19(K20(K20((Sub UAStr(# the carrier of Z, the charact of Z #)),(Sub UAStr(# the carrier of Z, the charact of Z #))),(Sub UAStr(# the carrier of Z, the charact of Z #)))) is set
UniAlg_meet UAStr(# the carrier of Z, the charact of Z #) is Relation-like K20((Sub UAStr(# the carrier of Z, the charact of Z #)),(Sub UAStr(# the carrier of Z, the charact of Z #))) -defined Sub UAStr(# the carrier of Z, the charact of Z #) -valued Function-like quasi_total Element of K19(K20(K20((Sub UAStr(# the carrier of Z, the charact of Z #)),(Sub UAStr(# the carrier of Z, the charact of Z #))),(Sub UAStr(# the carrier of Z, the charact of Z #))))
LattStr(# (Sub UAStr(# the carrier of Z, the charact of Z #)),(UniAlg_join UAStr(# the carrier of Z, the charact of Z #)),(UniAlg_meet UAStr(# the carrier of Z, the charact of Z #)) #) is strict LattStr
MSSign UAStr(# the carrier of Z, the charact of Z #) is non empty trivial V64() non void 1 -element V70() strict segmental all-with_const_op ManySortedSign
MSAlg UAStr(# the carrier of Z, the charact of Z #) is strict non-empty MSAlgebra over MSSign UAStr(# the carrier of Z, the charact of Z #)
MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)) is non empty strict Lattice-like V86() LattStr
MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)) is non empty set
MSAlg_join (MSAlg UAStr(# the carrier of Z, the charact of Z #)) is Relation-like K20((MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)))) -defined MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)) -valued Function-like quasi_total Element of K19(K20(K20((MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)))),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)))))
K20((MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)))) is Relation-like set
K20(K20((MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)))),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)))) is Relation-like set
K19(K20(K20((MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)))),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))))) is set
MSAlg_meet (MSAlg UAStr(# the carrier of Z, the charact of Z #)) is Relation-like K20((MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)))) -defined MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)) -valued Function-like quasi_total Element of K19(K20(K20((MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)))),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)))))
LattStr(# (MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))),(MSAlg_join (MSAlg UAStr(# the carrier of Z, the charact of Z #))),(MSAlg_meet (MSAlg UAStr(# the carrier of Z, the charact of Z #))) #) is strict LattStr
signature UAStr(# the carrier of Z, the charact of Z #) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
dom (signature UAStr(# the carrier of Z, the charact of Z #)) is Element of K19(NAT)
K20((dom (signature UAStr(# the carrier of Z, the charact of Z #))),({0} *)) is Relation-like set
K19(K20((dom (signature UAStr(# the carrier of Z, the charact of Z #))),({0} *))) is set
(*--> 0) * (signature UAStr(# the carrier of Z, the charact of Z #)) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V25() Element of K19(K20(NAT,({0} *)))
ff1 is Relation-like dom (signature UAStr(# the carrier of Z, the charact of Z #)) -defined {0} * -valued Function-like quasi_total Function-yielding V25() Element of K19(K20((dom (signature UAStr(# the carrier of Z, the charact of Z #))),({0} *)))
z is Relation-like Function-like Element of {0}
(dom (signature UAStr(# the carrier of Z, the charact of Z #))) --> z is Relation-like dom (signature UAStr(# the carrier of Z, the charact of Z #)) -defined {0} -valued Function-like constant total quasi_total Function-yielding V25() Element of K19(K20((dom (signature UAStr(# the carrier of Z, the charact of Z #))),{0}))
K20((dom (signature UAStr(# the carrier of Z, the charact of Z #))),{0}) is Relation-like set
K19(K20((dom (signature UAStr(# the carrier of Z, the charact of Z #))),{0})) is set
{z} is functional non empty set
K20((dom (signature UAStr(# the carrier of Z, the charact of Z #))),{z}) is Relation-like set
ManySortedSign(# {0},(dom (signature UAStr(# the carrier of Z, the charact of Z #))),ff1,((dom (signature UAStr(# the carrier of Z, the charact of Z #))) --> z) #) is non empty V70() strict ManySortedSign
f is Element of Sub UAStr(# the carrier of Z, the charact of Z #)
f is non empty strict partial quasi_total non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #)
MSSign f is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSAlg f is strict non-empty MSAlgebra over MSSign f
f is Element of MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))
K20((Sub UAStr(# the carrier of Z, the charact of Z #)),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)))) is Relation-like set
K19(K20((Sub UAStr(# the carrier of Z, the charact of Z #)),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #))))) is set
f is Relation-like Sub UAStr(# the carrier of Z, the charact of Z #) -defined MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)) -valued Function-like quasi_total Element of K19(K20((Sub UAStr(# the carrier of Z, the charact of Z #)),(MSSub (MSAlg UAStr(# the carrier of Z, the charact of Z #)))))
the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)) is non empty set
the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) is non empty set
K20( the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))) is Relation-like set
K19(K20( the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))))) is set
f is Relation-like the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)) -defined the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) -valued Function-like quasi_total Element of K19(K20( the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))))
f is Element of the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #))
x is Element of the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #))
f "\/" x is Element of the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #))
f . (f "\/" x) is Element of the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
f . f is Element of the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
f . x is Element of the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
(f . f) "\/" (f . x) is Element of the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
f "/\" x is Element of the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #))
f . (f "/\" x) is Element of the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
(f . f) "/\" (f . x) is Element of the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
y is Element of Sub UAStr(# the carrier of Z, the charact of Z #)
C is Element of Sub UAStr(# the carrier of Z, the charact of Z #)
y is non empty strict partial quasi_total non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #)
y1 is non empty strict partial quasi_total non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #)
y "\/" y1 is non empty strict partial quasi_total non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #)
y /\ y1 is non empty strict partial quasi_total non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #)
A2 is Element of Sub UAStr(# the carrier of Z, the charact of Z #)
f . A2 is set
MSSign y1 is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSAlg y1 is strict non-empty MSAlgebra over MSSign y1
f . y1 is set
A4 is non empty strict partial quasi_total non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #)
MSAlg A4 is strict non-empty MSAlgebra over MSSign A4
MSSign A4 is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSSign y is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
MSAlg y is strict non-empty MSAlgebra over MSSign y
f . y is set
A3 is non empty strict partial quasi_total non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #)
MSAlg A3 is strict non-empty MSAlgebra over MSSign A3
MSSign A3 is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
m is Element of Sub UAStr(# the carrier of Z, the charact of Z #)
f . m is set
f "/\" x is Element of the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #))
f . (f "/\" x) is Element of the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
(UniAlg_meet UAStr(# the carrier of Z, the charact of Z #)) . (y,C) is Element of Sub UAStr(# the carrier of Z, the charact of Z #)
f . ((UniAlg_meet UAStr(# the carrier of Z, the charact of Z #)) . (y,C)) is set
MSAlg (y /\ y1) is strict non-empty MSAlgebra over MSSign (y /\ y1)
MSSign (y /\ y1) is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
g1 is strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #)
g2 is strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #)
g1 /\ g2 is strict MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #)
the L_meet of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) is Relation-like K20( the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))) -defined the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))))
K20( the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))) is Relation-like set
K20(K20( the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))) is Relation-like set
K19(K20(K20( the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))))) is set
the L_meet of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) . ((f . f),(f . x)) is Element of the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
(f . f) "/\" (f . x) is Element of the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
f is non empty strict partial quasi_total non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #)
MSAlg f is strict non-empty MSAlgebra over MSSign f
MSSign f is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
f "\/" x is Element of the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #))
f . (f "\/" x) is Element of the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
(UniAlg_join UAStr(# the carrier of Z, the charact of Z #)) . (y,C) is Element of Sub UAStr(# the carrier of Z, the charact of Z #)
f . ((UniAlg_join UAStr(# the carrier of Z, the charact of Z #)) . (y,C)) is set
MSAlg (y "\/" y1) is strict non-empty MSAlgebra over MSSign (y "\/" y1)
MSSign (y "\/" y1) is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
g4 is strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #)
g3 is strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #)
g4 "\/" g3 is strict MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #)
the L_join of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) is Relation-like K20( the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))) -defined the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))), the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))))
the L_join of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) . ((f . f),(f . x)) is Element of the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
(f . f) "\/" (f . x) is Element of the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #)))
f is non empty strict partial quasi_total non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #)
MSAlg f is strict non-empty MSAlgebra over MSSign f
MSSign f is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
f is Relation-like the carrier of (UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #)) -defined the carrier of (MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))) -valued Function-like quasi_total Homomorphism of UnSubAlLattice UAStr(# the carrier of Z, the charact of Z #), MSSubAlLattice (MSAlg UAStr(# the carrier of Z, the charact of Z #))
x is set
dom f is set
y is set
f . x is set
f . y is set
C is Element of Sub UAStr(# the carrier of Z, the charact of Z #)
f . C is set
y1 is non empty strict partial quasi_total non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #)
MSAlg y1 is strict non-empty MSAlgebra over MSSign y1
MSSign y1 is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
y is Element of Sub UAStr(# the carrier of Z, the charact of Z #)
f . y is set
A2 is non empty strict partial quasi_total non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #)
MSAlg A2 is strict non-empty MSAlgebra over MSSign A2
MSSign A2 is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign
1-Alg (MSAlg y1) is non empty strict partial quasi_total non-empty UAStr
rng f is set
x is set
the carrier of (MSSign UAStr(# the carrier of Z, the charact of Z #)) is non empty trivial V33() set
y is strict MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #)
the Sorts of y is Relation-like the carrier of (MSSign UAStr(# the carrier of Z, the charact of Z #)) -defined Function-like non empty total set
Constants (MSAlg UAStr(# the carrier of Z, the charact of Z #)) is Relation-like non-empty non empty-yielding the carrier of (MSSign UAStr(# the carrier of Z, the charact of Z #)) -defined Function-like non empty total ManySortedSubset of the Sorts of (MSAlg UAStr(# the carrier of Z, the charact of Z #))
the Sorts of (MSAlg UAStr(# the carrier of Z, the charact of Z #)) is Relation-like non-empty non empty-yielding the carrier of (MSSign UAStr(# the carrier of Z, the charact of Z #)) -defined Function-like non empty total set
C is Relation-like the carrier of (MSSign UAStr(# the carrier of Z, the charact of Z #)) -defined Function-like non empty total ManySortedSubset of the Sorts of y
y is strict non-empty MSSubAlgebra of MSAlg UAStr(# the carrier of Z, the charact of Z #)
1-Alg y is non empty strict partial quasi_total non-empty UAStr
1-Alg (MSAlg UAStr(# the carrier of Z, the charact of Z #)) is non empty strict partial quasi_total non-empty UAStr
y1 is Element of Sub UAStr(# the carrier of Z, the charact of Z #)
f . y1 is set
f . (1-Alg y) is set
A2 is non empty strict partial quasi_total non-empty SubAlgebra of UAStr(# the carrier of Z, the charact of Z #)
MSAlg A2 is strict non-empty MSAlgebra over MSSign A2
MSSign A2 is non empty trivial V64() non void 1 -element V70() strict segmental ManySortedSign