:: MSSUBLAT semantic presentation

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

{ b

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

{ b

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

{ b

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)

{ b

(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

{ b

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

{ b

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

{ b

A3 -tuples_on the carrier of Z is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z

{ b

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

{ b

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

{ b

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