:: INSTALG1 semantic presentation

NAT is Element of bool REAL

REAL is set

bool REAL is set

NAT is set

bool NAT is set

bool NAT is set

{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

1 is non empty set

{{},1} is non empty set

Trees is non empty constituted-Trees set

bool Trees is set

FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees

PeanoNat is non empty strict L13()

the carrier of PeanoNat is non empty set

FinTrees the carrier of PeanoNat is non empty functional constituted-DTrees DTree-set of the carrier of PeanoNat

TS PeanoNat is functional constituted-DTrees Element of bool (FinTrees the carrier of PeanoNat)

bool (FinTrees the carrier of PeanoNat) is set

[:(TS PeanoNat),NAT:] is Relation-like set

bool [:(TS PeanoNat),NAT:] is set

[:NAT,(TS PeanoNat):] is Relation-like set

bool [:NAT,(TS PeanoNat):] is set

2 is non empty set

3 is non empty set

dom {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

rng {} is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V133() set

K33() is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of NAT

K300(K33()) is non empty V113() set

S1 is non empty non void feasible ManySortedSign

the carrier' of S1 is non empty set

the carrier of S1 is non empty set

S2 is Element of the carrier' of S1

S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set

DTConMSA S3 is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()

the carrier of (DTConMSA S3) is non empty set

FinTrees the carrier of (DTConMSA S3) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA S3)

Sym (S2,S3) is Element of K358((DTConMSA S3))

K358((DTConMSA S3)) is non empty Element of bool the carrier of (DTConMSA S3)

bool the carrier of (DTConMSA S3) is set

FreeMSA S3 is strict non-empty V132(S1) MSAlgebra over S1

Args (S2,(FreeMSA S3)) is non empty functional Element of rng ( the Sorts of (FreeMSA S3) #)

the Sorts of (FreeMSA S3) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set

the Sorts of (FreeMSA S3) # is non empty Relation-like the carrier of S1 * -defined Function-like total set

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

rng ( the Sorts of (FreeMSA S3) #) is non empty set

the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

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

( the Arity of S1 * ( the Sorts of (FreeMSA S3) #)) . S2 is set

X is set

TS (DTConMSA S3) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA S3))

bool (FinTrees the carrier of (DTConMSA S3)) is set

S1 -Terms S3 is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA S3))

FreeSort S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set

FreeOper S3 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ((FreeSort S3) #), the ResultSort of S1 * (FreeSort S3)

(FreeSort S3) # is non empty Relation-like the carrier of S1 * -defined Function-like total set

the Arity of S1 * ((FreeSort S3) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set

the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

the ResultSort of S1 * (FreeSort S3) is non empty Relation-like non-empty non empty-yielding the carrier' of S1 -defined Function-like total set

MSAlgebra(# (FreeSort S3),(FreeOper S3) #) is strict MSAlgebra over S1

f1 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like V53() V54() DTree-yielding ArgumentSeq of Sym (S2,S3)

g1 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like V53() V54() FinSequence of TS (DTConMSA S3)

roots g1 is Relation-like NAT -defined the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA S3)

f1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of Args (S2,(FreeMSA S3))

rng f1 is set

g1 is set

dom f1 is Element of bool NAT

f2 is set

f1 . f2 is set

the_arity_of S2 is Relation-like NAT -defined the carrier of S1 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *

the Arity of S1 . S2 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *

g2 is Element of NAT

(the_arity_of S2) /. g2 is Element of the carrier of S1

(FreeSort S3) . ((the_arity_of S2) /. g2) is non empty set

FreeSort (S3,((the_arity_of S2) /. g2)) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA S3))

bool (TS (DTConMSA S3)) is set

dom (the_arity_of S2) is Element of bool NAT

g1 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like V53() V54() FinSequence of TS (DTConMSA S3)

roots g1 is Relation-like NAT -defined the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA S3)

S1 is non empty non void feasible ManySortedSign

the carrier of S1 is non empty set

the carrier' of S1 is non empty set

S3 is Element of the carrier' of S1

S2 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set

FreeMSA S2 is strict non-empty V132(S1) MSAlgebra over S1

Args (S3,(FreeMSA S2)) is non empty functional Element of rng ( the Sorts of (FreeMSA S2) #)

the Sorts of (FreeMSA S2) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set

the Sorts of (FreeMSA S2) # is non empty Relation-like the carrier of S1 * -defined Function-like total set

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

rng ( the Sorts of (FreeMSA S2) #) is non empty set

the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

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

( the Arity of S1 * ( the Sorts of (FreeMSA S2) #)) . S3 is set

X is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of Args (S3,(FreeMSA S2))

S1 is non empty non void feasible ManySortedSign

the carrier of S1 is non empty set

the carrier' of S1 is non empty set

S2 is MSAlgebra over S1

the Sorts of S2 is non empty Relation-like the carrier of S1 -defined Function-like total set

S3 is MSAlgebra over S1

the Sorts of S3 is non empty Relation-like the carrier of S1 -defined Function-like total set

X is Element of the carrier' of S1

Args (X,S2) is Element of rng ( the Sorts of S2 #)

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

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

rng ( the Sorts of S2 #) is non empty set

the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

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

( the Arity of S1 * ( the Sorts of S2 #)) . X is set

Args (X,S3) is Element of rng ( the Sorts of S3 #)

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

rng ( the Sorts of S3 #) is non empty set

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

( the Arity of S1 * ( the Sorts of S3 #)) . X is set

f1 is Element of NAT

the_arity_of X is Relation-like NAT -defined the carrier of S1 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *

the Arity of S1 . X is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *

dom (the_arity_of X) is Element of bool NAT

(the_arity_of X) /. f1 is Element of the carrier of S1

the Sorts of S2 . ((the_arity_of X) /. f1) is set

the Sorts of S3 . ((the_arity_of X) /. f1) is set

S1 is non empty non void feasible ManySortedSign

the carrier' of S1 is non empty set

the carrier of S1 is non empty set

S2 is Element of the carrier' of S1

[S2, the carrier of S1] is set

{S2, the carrier of S1} is non empty set

{S2} is non empty set

{{S2, the carrier of S1},{S2}} is non empty set

S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set

FreeMSA S3 is strict non-empty V132(S1) MSAlgebra over S1

Args (S2,(FreeMSA S3)) is non empty functional Element of rng ( the Sorts of (FreeMSA S3) #)

the Sorts of (FreeMSA S3) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set

the Sorts of (FreeMSA S3) # is non empty Relation-like the carrier of S1 * -defined Function-like total set

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

rng ( the Sorts of (FreeMSA S3) #) is non empty set

the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

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

( the Arity of S1 * ( the Sorts of (FreeMSA S3) #)) . S2 is set

Result (S2,(FreeMSA S3)) is non empty Element of rng the Sorts of (FreeMSA S3)

rng the Sorts of (FreeMSA S3) is non empty V133() set

the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

the ResultSort of S1 * the Sorts of (FreeMSA S3) is non empty Relation-like non-empty non empty-yielding the carrier' of S1 -defined Function-like total set

( the ResultSort of S1 * the Sorts of (FreeMSA S3)) . S2 is non empty set

Den (S2,(FreeMSA S3)) is non empty Relation-like Args (S2,(FreeMSA S3)) -defined Result (S2,(FreeMSA S3)) -valued Function-like total V29( Args (S2,(FreeMSA S3)), Result (S2,(FreeMSA S3))) Element of bool [:(Args (S2,(FreeMSA S3))),(Result (S2,(FreeMSA S3))):]

[:(Args (S2,(FreeMSA S3))),(Result (S2,(FreeMSA S3))):] is Relation-like set

bool [:(Args (S2,(FreeMSA S3))),(Result (S2,(FreeMSA S3))):] is set

the Charact of (FreeMSA S3) is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of (FreeMSA S3) #), the ResultSort of S1 * the Sorts of (FreeMSA S3)

the Charact of (FreeMSA S3) . S2 is Relation-like Function-like set

X is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like DTree-yielding Element of Args (S2,(FreeMSA S3))

(Den (S2,(FreeMSA S3))) . X is Element of Result (S2,(FreeMSA S3))

[S2, the carrier of S1] -tree X is Relation-like Function-like V117() set

FreeSort S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set

FreeOper S3 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ((FreeSort S3) #), the ResultSort of S1 * (FreeSort S3)

(FreeSort S3) # is non empty Relation-like the carrier of S1 * -defined Function-like total set

the Arity of S1 * ((FreeSort S3) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set

the ResultSort of S1 * (FreeSort S3) is non empty Relation-like non-empty non empty-yielding the carrier' of S1 -defined Function-like total set

MSAlgebra(# (FreeSort S3),(FreeOper S3) #) is strict MSAlgebra over S1

DTConMSA S3 is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()

the carrier of (DTConMSA S3) is non empty set

FinTrees the carrier of (DTConMSA S3) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA S3)

Sym (S2,S3) is Element of K358((DTConMSA S3))

K358((DTConMSA S3)) is non empty Element of bool the carrier of (DTConMSA S3)

bool the carrier of (DTConMSA S3) is set

f1 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like V53() V54() DTree-yielding ArgumentSeq of Sym (S2,S3)

TS (DTConMSA S3) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA S3))

bool (FinTrees the carrier of (DTConMSA S3)) is set

roots f1 is Relation-like NAT -defined the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA S3)

DenOp (S2,S3) is Relation-like ( the Arity of S1 * ((FreeSort S3) #)) . S2 -defined ( the ResultSort of S1 * (FreeSort S3)) . S2 -valued Function-like total V29(( the Arity of S1 * ((FreeSort S3) #)) . S2,( the ResultSort of S1 * (FreeSort S3)) . S2) Element of bool [:(( the Arity of S1 * ((FreeSort S3) #)) . S2),(( the ResultSort of S1 * (FreeSort S3)) . S2):]

( the Arity of S1 * ((FreeSort S3) #)) . S2 is set

( the ResultSort of S1 * (FreeSort S3)) . S2 is non empty set

[:(( the Arity of S1 * ((FreeSort S3) #)) . S2),(( the ResultSort of S1 * (FreeSort S3)) . S2):] is Relation-like set

bool [:(( the Arity of S1 * ((FreeSort S3) #)) . S2),(( the ResultSort of S1 * (FreeSort S3)) . S2):] is set

(DenOp (S2,S3)) . X is set

S1 is non empty non void feasible ManySortedSign

the carrier' of S1 is non empty set

S2 is MSAlgebra over S1

the Sorts of S2 is non empty Relation-like the carrier of S1 -defined Function-like total set

the carrier of S1 is non empty set

the Charact of S2 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S2 #), the ResultSort of S1 * the Sorts of S2

the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

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

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

the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

the ResultSort of S1 * the Sorts of S2 is non empty Relation-like the carrier' of S1 -defined Function-like total set

MSAlgebra(# the Sorts of S2, the Charact of S2 #) is strict MSAlgebra over S1

S3 is MSAlgebra over S1

the Sorts of S3 is non empty Relation-like the carrier of S1 -defined Function-like total set

the Charact of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S3 #), the ResultSort of S1 * the Sorts of S3

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

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

the ResultSort of S1 * the Sorts of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total set

MSAlgebra(# the Sorts of S3, the Charact of S3 #) is strict MSAlgebra over S1

X is Element of the carrier' of S1

Den (X,S2) is Relation-like Args (X,S2) -defined Result (X,S2) -valued Function-like V29( Args (X,S2), Result (X,S2)) Element of bool [:(Args (X,S2)),(Result (X,S2)):]

Args (X,S2) is Element of rng ( the Sorts of S2 #)

rng ( the Sorts of S2 #) is non empty set

( the Arity of S1 * ( the Sorts of S2 #)) . X is set

Result (X,S2) is Element of rng the Sorts of S2

rng the Sorts of S2 is non empty set

( the ResultSort of S1 * the Sorts of S2) . X is set

[:(Args (X,S2)),(Result (X,S2)):] is Relation-like set

bool [:(Args (X,S2)),(Result (X,S2)):] is set

the Charact of S2 . X is Relation-like Function-like set

Den (X,S3) is Relation-like Args (X,S3) -defined Result (X,S3) -valued Function-like V29( Args (X,S3), Result (X,S3)) Element of bool [:(Args (X,S3)),(Result (X,S3)):]

Args (X,S3) is Element of rng ( the Sorts of S3 #)

rng ( the Sorts of S3 #) is non empty set

( the Arity of S1 * ( the Sorts of S3 #)) . X is set

Result (X,S3) is Element of rng the Sorts of S3

rng the Sorts of S3 is non empty set

( the ResultSort of S1 * the Sorts of S3) . X is set

[:(Args (X,S3)),(Result (X,S3)):] is Relation-like set

bool [:(Args (X,S3)),(Result (X,S3)):] is set

the Charact of S3 . X is Relation-like Function-like set

S1 is non empty non void feasible ManySortedSign

the carrier of S1 is non empty set

the carrier' of S1 is non empty set

S2 is MSAlgebra over S1

the Sorts of S2 is non empty Relation-like the carrier of S1 -defined Function-like total set

the Charact of S2 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S2 #), the ResultSort of S1 * the Sorts of S2

the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

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

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

the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

the ResultSort of S1 * the Sorts of S2 is non empty Relation-like the carrier' of S1 -defined Function-like total set

MSAlgebra(# the Sorts of S2, the Charact of S2 #) is strict MSAlgebra over S1

X is MSAlgebra over S1

the Sorts of X is non empty Relation-like the carrier of S1 -defined Function-like total set

the Charact of X is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of X #), the ResultSort of S1 * the Sorts of X

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

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

the ResultSort of S1 * the Sorts of X is non empty Relation-like the carrier' of S1 -defined Function-like total set

MSAlgebra(# the Sorts of X, the Charact of X #) is strict MSAlgebra over S1

S3 is MSAlgebra over S1

the Sorts of S3 is non empty Relation-like the carrier of S1 -defined Function-like total set

the Charact of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S3 #), the ResultSort of S1 * the Sorts of S3

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

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

the ResultSort of S1 * the Sorts of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total set

MSAlgebra(# the Sorts of S3, the Charact of S3 #) is strict MSAlgebra over S1

f1 is MSAlgebra over S1

the Sorts of f1 is non empty Relation-like the carrier of S1 -defined Function-like total set

the Charact of f1 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of f1 #), the ResultSort of S1 * the Sorts of f1

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

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

the ResultSort of S1 * the Sorts of f1 is non empty Relation-like the carrier' of S1 -defined Function-like total set

MSAlgebra(# the Sorts of f1, the Charact of f1 #) is strict MSAlgebra over S1

g1 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of S2, the Sorts of S3

f2 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of X, the Sorts of f1

g2 is Element of the carrier' of S1

Args (g2,S2) is Element of rng ( the Sorts of S2 #)

rng ( the Sorts of S2 #) is non empty set

( the Arity of S1 * ( the Sorts of S2 #)) . g2 is set

Args (g2,S3) is Element of rng ( the Sorts of S3 #)

rng ( the Sorts of S3 #) is non empty set

( the Arity of S1 * ( the Sorts of S3 #)) . g2 is set

Args (g2,X) is Element of rng ( the Sorts of X #)

rng ( the Sorts of X #) is non empty set

( the Arity of S1 * ( the Sorts of X #)) . g2 is set

f is Element of Args (g2,S2)

g1 # f is Element of Args (g2,S3)

g is Element of Args (g2,X)

f2 # g is Element of Args (g2,f1)

Args (g2,f1) is Element of rng ( the Sorts of f1 #)

rng ( the Sorts of f1 #) is non empty set

( the Arity of S1 * ( the Sorts of f1 #)) . g2 is set

the_arity_of g2 is Relation-like NAT -defined the carrier of S1 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *

the Arity of S1 . g2 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *

(the_arity_of g2) * g1 is Relation-like NAT -defined Function-like V53() V54() set

Frege ((the_arity_of g2) * g1) is Relation-like product K180(((the_arity_of g2) * g1)) -defined Function-like total V53() V54() set

K180(((the_arity_of g2) * g1)) is Relation-like Function-like set

product K180(((the_arity_of g2) * g1)) is set

(Frege ((the_arity_of g2) * g1)) . f is Relation-like Function-like set

S1 is non empty non void feasible ManySortedSign

the carrier of S1 is non empty set

S2 is MSAlgebra over S1

the Sorts of S2 is non empty Relation-like the carrier of S1 -defined Function-like total set

the Charact of S2 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S2 #), the ResultSort of S1 * the Sorts of S2

the carrier' of S1 is non empty set

the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

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

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

the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

the ResultSort of S1 * the Sorts of S2 is non empty Relation-like the carrier' of S1 -defined Function-like total set

MSAlgebra(# the Sorts of S2, the Charact of S2 #) is strict MSAlgebra over S1

X is MSAlgebra over S1

the Sorts of X is non empty Relation-like the carrier of S1 -defined Function-like total set

the Charact of X is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of X #), the ResultSort of S1 * the Sorts of X

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

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

the ResultSort of S1 * the Sorts of X is non empty Relation-like the carrier' of S1 -defined Function-like total set

MSAlgebra(# the Sorts of X, the Charact of X #) is strict MSAlgebra over S1

S3 is MSAlgebra over S1

the Sorts of S3 is non empty Relation-like the carrier of S1 -defined Function-like total set

the Charact of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S3 #), the ResultSort of S1 * the Sorts of S3

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

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

the ResultSort of S1 * the Sorts of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total set

MSAlgebra(# the Sorts of S3, the Charact of S3 #) is strict MSAlgebra over S1

f1 is MSAlgebra over S1

the Sorts of f1 is non empty Relation-like the carrier of S1 -defined Function-like total set

the Charact of f1 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of f1 #), the ResultSort of S1 * the Sorts of f1

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

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

the ResultSort of S1 * the Sorts of f1 is non empty Relation-like the carrier' of S1 -defined Function-like total set

MSAlgebra(# the Sorts of f1, the Charact of f1 #) is strict MSAlgebra over S1

g1 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of S2, the Sorts of S3

f2 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of X, the Sorts of f1

g2 is Element of the carrier' of S1

Args (g2,X) is Element of rng ( the Sorts of X #)

rng ( the Sorts of X #) is non empty set

( the Arity of S1 * ( the Sorts of X #)) . g2 is set

the_result_sort_of g2 is Element of the carrier of S1

the ResultSort of S1 . g2 is Element of the carrier of S1

f2 . (the_result_sort_of g2) is Relation-like the Sorts of X . (the_result_sort_of g2) -defined the Sorts of f1 . (the_result_sort_of g2) -valued Function-like V29( the Sorts of X . (the_result_sort_of g2), the Sorts of f1 . (the_result_sort_of g2)) Element of bool [:( the Sorts of X . (the_result_sort_of g2)),( the Sorts of f1 . (the_result_sort_of g2)):]

the Sorts of X . (the_result_sort_of g2) is set

the Sorts of f1 . (the_result_sort_of g2) is set

[:( the Sorts of X . (the_result_sort_of g2)),( the Sorts of f1 . (the_result_sort_of g2)):] is Relation-like set

bool [:( the Sorts of X . (the_result_sort_of g2)),( the Sorts of f1 . (the_result_sort_of g2)):] is set

Den (g2,X) is Relation-like Args (g2,X) -defined Result (g2,X) -valued Function-like V29( Args (g2,X), Result (g2,X)) Element of bool [:(Args (g2,X)),(Result (g2,X)):]

Result (g2,X) is Element of rng the Sorts of X

rng the Sorts of X is non empty set

( the ResultSort of S1 * the Sorts of X) . g2 is set

[:(Args (g2,X)),(Result (g2,X)):] is Relation-like set

bool [:(Args (g2,X)),(Result (g2,X)):] is set

the Charact of X . g2 is Relation-like Function-like set

Den (g2,f1) is Relation-like Args (g2,f1) -defined Result (g2,f1) -valued Function-like V29( Args (g2,f1), Result (g2,f1)) Element of bool [:(Args (g2,f1)),(Result (g2,f1)):]

Args (g2,f1) is Element of rng ( the Sorts of f1 #)

rng ( the Sorts of f1 #) is non empty set

( the Arity of S1 * ( the Sorts of f1 #)) . g2 is set

Result (g2,f1) is Element of rng the Sorts of f1

rng the Sorts of f1 is non empty set

( the ResultSort of S1 * the Sorts of f1) . g2 is set

[:(Args (g2,f1)),(Result (g2,f1)):] is Relation-like set

bool [:(Args (g2,f1)),(Result (g2,f1)):] is set

the Charact of f1 . g2 is Relation-like Function-like set

f is Element of Args (g2,X)

(Den (g2,X)) . f is set

(f2 . (the_result_sort_of g2)) . ((Den (g2,X)) . f) is set

f2 # f is Element of Args (g2,f1)

(Den (g2,f1)) . (f2 # f) is set

Args (g2,S2) is Element of rng ( the Sorts of S2 #)

rng ( the Sorts of S2 #) is non empty set

( the Arity of S1 * ( the Sorts of S2 #)) . g2 is set

g1 . (the_result_sort_of g2) is Relation-like the Sorts of S2 . (the_result_sort_of g2) -defined the Sorts of S3 . (the_result_sort_of g2) -valued Function-like V29( the Sorts of S2 . (the_result_sort_of g2), the Sorts of S3 . (the_result_sort_of g2)) Element of bool [:( the Sorts of S2 . (the_result_sort_of g2)),( the Sorts of S3 . (the_result_sort_of g2)):]

the Sorts of S2 . (the_result_sort_of g2) is set

the Sorts of S3 . (the_result_sort_of g2) is set

[:( the Sorts of S2 . (the_result_sort_of g2)),( the Sorts of S3 . (the_result_sort_of g2)):] is Relation-like set

bool [:( the Sorts of S2 . (the_result_sort_of g2)),( the Sorts of S3 . (the_result_sort_of g2)):] is set

Den (g2,S2) is Relation-like Args (g2,S2) -defined Result (g2,S2) -valued Function-like V29( Args (g2,S2), Result (g2,S2)) Element of bool [:(Args (g2,S2)),(Result (g2,S2)):]

Result (g2,S2) is Element of rng the Sorts of S2

rng the Sorts of S2 is non empty set

( the ResultSort of S1 * the Sorts of S2) . g2 is set

[:(Args (g2,S2)),(Result (g2,S2)):] is Relation-like set

bool [:(Args (g2,S2)),(Result (g2,S2)):] is set

the Charact of S2 . g2 is Relation-like Function-like set

g is Element of Args (g2,S2)

(Den (g2,S2)) . g is set

(g1 . (the_result_sort_of g2)) . ((Den (g2,S2)) . g) is set

Den (g2,S3) is Relation-like Args (g2,S3) -defined Result (g2,S3) -valued Function-like V29( Args (g2,S3), Result (g2,S3)) Element of bool [:(Args (g2,S3)),(Result (g2,S3)):]

Args (g2,S3) is Element of rng ( the Sorts of S3 #)

rng ( the Sorts of S3 #) is non empty set

( the Arity of S1 * ( the Sorts of S3 #)) . g2 is set

Result (g2,S3) is Element of rng the Sorts of S3

rng the Sorts of S3 is non empty set

( the ResultSort of S1 * the Sorts of S3) . g2 is set

[:(Args (g2,S3)),(Result (g2,S3)):] is Relation-like set

bool [:(Args (g2,S3)),(Result (g2,S3)):] is set

the Charact of S3 . g2 is Relation-like Function-like set

g1 # g is Element of Args (g2,S3)

(Den (g2,S3)) . (g1 # g) is set

S1 is ManySortedSign

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

the carrier' of S1 is set

the carrier of S1 is set

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

dom the ResultSort of S1 is set

S1 is ManySortedSign

the carrier of S1 is set

the carrier' of S1 is set

S1 is ManySortedSign

the carrier of S1 is set

the carrier' of S1 is set

S1 is ManySortedSign

the carrier of S1 is set

the carrier' of S1 is set

S1 is ManySortedSign

the non empty non void feasible () ManySortedSign is non empty non void feasible () ManySortedSign

S1 is () ManySortedSign

the carrier of S1 is set

id the carrier of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one total V29( the carrier of S1, the carrier of S1) Element of bool [: the carrier of S1, the carrier of S1:]

[: the carrier of S1, the carrier of S1:] is Relation-like set

bool [: the carrier of S1, the carrier of S1:] is set

the carrier' of S1 is set

id the carrier' of S1 is Relation-like the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one total V29( the carrier' of S1, the carrier' of S1) Element of bool [: the carrier' of S1, the carrier' of S1:]

[: the carrier' of S1, the carrier' of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier' of S1:] is set

S2 is non empty non void feasible () ManySortedSign

S1 is ManySortedSign

S2 is ManySortedSign

the carrier of S1 is set

the carrier of S2 is set

[: the carrier of S1, the carrier of S2:] is Relation-like set

bool [: the carrier of S1, the carrier of S2:] is set

the carrier' of S1 is set

the carrier' of S2 is set

[: the carrier' of S1, the carrier' of S2:] is Relation-like set

bool [: the carrier' of S1, the carrier' of S2:] is set

S3 is Relation-like Function-like set

X is Relation-like Function-like set

dom S3 is set

rng S3 is set

dom X is set

rng X is set

S1 is () ManySortedSign

the carrier of S1 is set

id the carrier of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one total V29( the carrier of S1, the carrier of S1) Element of bool [: the carrier of S1, the carrier of S1:]

[: the carrier of S1, the carrier of S1:] is Relation-like set

bool [: the carrier of S1, the carrier of S1:] is set

the carrier' of S1 is set

id the carrier' of S1 is Relation-like the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one total V29( the carrier' of S1, the carrier' of S1) Element of bool [: the carrier' of S1, the carrier' of S1:]

[: the carrier' of S1, the carrier' of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier' of S1:] is set

S1 is () ManySortedSign

the carrier of S1 is set

the carrier' of S1 is set

S2 is (S1)

the carrier of S2 is set

the carrier' of S2 is set

id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]

[: the carrier' of S2, the carrier' of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier' of S2:] is set

id the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]

[: the carrier of S2, the carrier of S2:] is Relation-like set

bool [: the carrier of S2, the carrier of S2:] is set

rng (id the carrier of S2) is set

rng (id the carrier' of S2) is set

S1 is () ManySortedSign

S2 is (S1)

the carrier of S2 is set

id the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]

[: the carrier of S2, the carrier of S2:] is Relation-like set

bool [: the carrier of S2, the carrier of S2:] is set

the carrier' of S2 is set

id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]

[: the carrier' of S2, the carrier' of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier' of S2:] is set

dom (id the carrier' of S2) is set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]

[: the carrier' of S2, the carrier of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier of S2:] is set

(id the carrier of S2) * the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]

the carrier' of S1 is set

the carrier of S1 is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

the ResultSort of S1 * (id the carrier' of S2) is Relation-like the carrier' of S2 -defined the carrier of S1 -valued Function-like Element of bool [: the carrier' of S2, the carrier of S1:]

[: the carrier' of S2, the carrier of S1:] is Relation-like set

bool [: the carrier' of S2, the carrier of S1:] is set

dom the ResultSort of S1 is set

rng (id the carrier' of S2) is set

S1 is () ManySortedSign

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

the carrier' of S1 is set

the carrier of S1 is set

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

S2 is () (S1)

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]

the carrier' of S2 is set

the carrier of S2 is set

[: the carrier' of S2, the carrier of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier of S2:] is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]

the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)

[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set

bool [: the carrier' of S2,( the carrier of S2 *):] is set

id the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]

[: the carrier of S2, the carrier of S2:] is Relation-like set

bool [: the carrier of S2, the carrier of S2:] is set

id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]

[: the carrier' of S2, the carrier' of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier' of S2:] is set

dom the Arity of S2 is set

rng the Arity of S2 is set

f1 is set

the Arity of S2 . f1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set

(id the carrier' of S2) . f1 is set

g1 is Relation-like NAT -defined the carrier of S2 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S2 *

rng g1 is set

(id the carrier of S2) * g1 is Relation-like NAT -defined the carrier of S2 -valued Function-like Element of bool [:NAT, the carrier of S2:]

[:NAT, the carrier of S2:] is Relation-like set

bool [:NAT, the carrier of S2:] is set

the Arity of S1 . f1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set

(id the carrier of S2) * the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]

the ResultSort of S1 * (id the carrier' of S2) is Relation-like the carrier' of S2 -defined the carrier of S1 -valued Function-like Element of bool [: the carrier' of S2, the carrier of S1:]

[: the carrier' of S2, the carrier of S1:] is Relation-like set

bool [: the carrier' of S2, the carrier of S1:] is set

dom the Arity of S1 is set

S1 is () ManySortedSign

the carrier' of S1 is set

the carrier of S1 is set

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

S2 is () (S1)

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]

the carrier' of S2 is set

the carrier of S2 is set

the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)

[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set

bool [: the carrier' of S2,( the carrier of S2 *):] is set

the Arity of S1 | the carrier' of S2 is Relation-like the carrier' of S1 -defined the carrier' of S2 -defined the carrier' of S1 -defined the carrier of S1 * -valued Function-like V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]

[: the carrier' of S2, the carrier of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier of S2:] is set

the ResultSort of S1 | the carrier' of S2 is Relation-like the carrier' of S1 -defined the carrier' of S2 -defined the carrier' of S1 -defined the carrier of S1 -valued Function-like Element of bool [: the carrier' of S1, the carrier of S1:]

dom the ResultSort of S2 is set

dom the Arity of S2 is set

S2 is () ManySortedSign

the carrier of S2 is set

S1 is () ManySortedSign

the carrier of S1 is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]

the carrier' of S2 is set

the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)

[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set

bool [: the carrier' of S2,( the carrier of S2 *):] is set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

the carrier' of S1 is set

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]

[: the carrier' of S2, the carrier of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier of S2:] is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

id the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]

[: the carrier of S2, the carrier of S2:] is Relation-like set

bool [: the carrier of S2, the carrier of S2:] is set

id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]

[: the carrier' of S2, the carrier' of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier' of S2:] is set

dom (id the carrier of S2) is set

dom (id the carrier' of S2) is set

rng (id the carrier of S2) is set

rng (id the carrier' of S2) is set

the ResultSort of S2 * (id the carrier of S2) is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like set

(id the carrier' of S2) * the ResultSort of S1 is Relation-like the carrier' of S2 -defined the carrier of S1 -valued Function-like set

dom the Arity of S2 is set

dom the Arity of S1 is set

dom the ResultSort of S2 is set

rng the ResultSort of S2 is set

(id the carrier of S2) * the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]

the ResultSort of S1 | the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S1 -defined the carrier of S1 -valued Function-like Element of bool [: the carrier' of S1, the carrier of S1:]

the ResultSort of S1 * (id the carrier' of S2) is Relation-like the carrier' of S2 -defined the carrier of S1 -valued Function-like Element of bool [: the carrier' of S2, the carrier of S1:]

[: the carrier' of S2, the carrier of S1:] is Relation-like set

bool [: the carrier' of S2, the carrier of S1:] is set

f1 is set

the Arity of S2 . f1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set

(id the carrier' of S2) . f1 is set

the Arity of S1 . ((id the carrier' of S2) . f1) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set

g1 is Relation-like Function-like set

g1 * (id the carrier of S2) is Relation-like the carrier of S2 -valued Function-like set

f2 is Relation-like NAT -defined the carrier of S2 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S2 *

rng f2 is set

the Arity of S1 . f1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set

S2 is () ManySortedSign

the carrier of S2 is set

S1 is () ManySortedSign

the carrier of S1 is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]

the carrier' of S2 is set

the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)

[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set

bool [: the carrier' of S2,( the carrier of S2 *):] is set

the carrier' of S1 is set

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

the Arity of S1 | the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S1 -defined the carrier of S1 * -valued Function-like V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]

[: the carrier' of S2, the carrier of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier of S2:] is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

the ResultSort of S1 | the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S1 -defined the carrier of S1 -valued Function-like Element of bool [: the carrier' of S1, the carrier of S1:]

S1 is () ManySortedSign

the carrier of S1 is set

id the carrier of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one total V29( the carrier of S1, the carrier of S1) Element of bool [: the carrier of S1, the carrier of S1:]

[: the carrier of S1, the carrier of S1:] is Relation-like set

bool [: the carrier of S1, the carrier of S1:] is set

the carrier' of S1 is set

id the carrier' of S1 is Relation-like the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one total V29( the carrier' of S1, the carrier' of S1) Element of bool [: the carrier' of S1, the carrier' of S1:]

[: the carrier' of S1, the carrier' of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier' of S1:] is set

S1 is () ManySortedSign

S2 is () (S1)

S3 is () (S2)

the carrier of S3 is set

id the carrier of S3 is Relation-like the carrier of S3 -defined the carrier of S3 -valued Function-like one-to-one total V29( the carrier of S3, the carrier of S3) Element of bool [: the carrier of S3, the carrier of S3:]

[: the carrier of S3, the carrier of S3:] is Relation-like set

bool [: the carrier of S3, the carrier of S3:] is set

rng (id the carrier of S3) is set

the carrier of S2 is set

id the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]

[: the carrier of S2, the carrier of S2:] is Relation-like set

bool [: the carrier of S2, the carrier of S2:] is set

(id the carrier of S2) * (id the carrier of S3) is Relation-like the carrier of S3 -defined the carrier of S2 -valued Function-like one-to-one Element of bool [: the carrier of S3, the carrier of S2:]

[: the carrier of S3, the carrier of S2:] is Relation-like set

bool [: the carrier of S3, the carrier of S2:] is set

the carrier' of S3 is set

id the carrier' of S3 is Relation-like the carrier' of S3 -defined the carrier' of S3 -valued Function-like one-to-one total V29( the carrier' of S3, the carrier' of S3) Element of bool [: the carrier' of S3, the carrier' of S3:]

[: the carrier' of S3, the carrier' of S3:] is Relation-like set

bool [: the carrier' of S3, the carrier' of S3:] is set

rng (id the carrier' of S3) is set

the carrier' of S2 is set

id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]

[: the carrier' of S2, the carrier' of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier' of S2:] is set

(id the carrier' of S2) * (id the carrier' of S3) is Relation-like the carrier' of S3 -defined the carrier' of S2 -valued Function-like one-to-one Element of bool [: the carrier' of S3, the carrier' of S2:]

[: the carrier' of S3, the carrier' of S2:] is Relation-like set

bool [: the carrier' of S3, the carrier' of S2:] is set

S1 is () ManySortedSign

the carrier of S1 is set

the carrier' of S1 is set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) is strict ManySortedSign

S2 is () (S1)

the carrier of S2 is set

the carrier' of S2 is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]

the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)

[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set

bool [: the carrier' of S2,( the carrier of S2 *):] is set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]

[: the carrier' of S2, the carrier of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier of S2:] is set

ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) is strict ManySortedSign

S1 is non empty feasible () ManySortedSign

S2 is () (S1)

S1 is non empty non void feasible () ManySortedSign

S2 is () (S1)

S1 is () ManySortedSign

S2 is () (S1)

the carrier of S2 is set

the carrier' of S2 is set

S3 is ManySortedSign

X is Relation-like Function-like set

f1 is Relation-like Function-like set

X | the carrier of S2 is Relation-like Function-like set

f1 | the carrier' of S2 is Relation-like Function-like set

id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]

[: the carrier' of S2, the carrier' of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier' of S2:] is set

(id the carrier' of S2) * f1 is Relation-like the carrier' of S2 -defined Function-like set

id the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]

[: the carrier of S2, the carrier of S2:] is Relation-like set

bool [: the carrier of S2, the carrier of S2:] is set

(id the carrier of S2) * X is Relation-like the carrier of S2 -defined Function-like set

S1 is ManySortedSign

S2 is () ManySortedSign

S3 is () (S2)

X is Relation-like Function-like set

f1 is Relation-like Function-like set

rng X is set

the carrier of S3 is set

id the carrier of S3 is Relation-like the carrier of S3 -defined the carrier of S3 -valued Function-like one-to-one total V29( the carrier of S3, the carrier of S3) Element of bool [: the carrier of S3, the carrier of S3:]

[: the carrier of S3, the carrier of S3:] is Relation-like set

bool [: the carrier of S3, the carrier of S3:] is set

X * (id the carrier of S3) is Relation-like the carrier of S3 -valued Function-like set

rng f1 is set

the carrier' of S3 is set

id the carrier' of S3 is Relation-like the carrier' of S3 -defined the carrier' of S3 -valued Function-like one-to-one total V29( the carrier' of S3, the carrier' of S3) Element of bool [: the carrier' of S3, the carrier' of S3:]

[: the carrier' of S3, the carrier' of S3:] is Relation-like set

bool [: the carrier' of S3, the carrier' of S3:] is set

f1 * (id the carrier' of S3) is Relation-like the carrier' of S3 -valued Function-like set

S1 is ManySortedSign

S2 is () ManySortedSign

S3 is () (S2)

the carrier of S3 is set

the carrier' of S3 is set

X is Relation-like Function-like set

f1 is Relation-like Function-like set

rng X is set

rng f1 is set

dom X is set

the carrier of S1 is set

dom f1 is set

the carrier' of S1 is set

the carrier of S2 is set

the carrier' of S2 is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

the ResultSort of S1 * X is Relation-like the carrier' of S1 -defined Function-like set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]

[: the carrier' of S2, the carrier of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier of S2:] is set

f1 * the ResultSort of S2 is Relation-like the carrier of S2 -valued Function-like set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]

the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)

[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set

bool [: the carrier' of S2,( the carrier of S2 *):] is set

the ResultSort of S3 is Relation-like the carrier' of S3 -defined the carrier of S3 -valued Function-like V29( the carrier' of S3, the carrier of S3) Element of bool [: the carrier' of S3, the carrier of S3:]

[: the carrier' of S3, the carrier of S3:] is Relation-like set

bool [: the carrier' of S3, the carrier of S3:] is set

f1 * the ResultSort of S3 is Relation-like the carrier of S3 -valued Function-like set

the Arity of S3 is Relation-like the carrier' of S3 -defined the carrier of S3 * -valued Function-like total V29( the carrier' of S3, the carrier of S3 * ) V53() V54() Element of bool [: the carrier' of S3,( the carrier of S3 *):]

the carrier of S3 * is non empty functional FinSequence-membered M12( the carrier of S3)

[: the carrier' of S3,( the carrier of S3 *):] is Relation-like set

bool [: the carrier' of S3,( the carrier of S3 *):] is set

id the carrier' of S3 is Relation-like the carrier' of S3 -defined the carrier' of S3 -valued Function-like one-to-one total V29( the carrier' of S3, the carrier' of S3) Element of bool [: the carrier' of S3, the carrier' of S3:]

[: the carrier' of S3, the carrier' of S3:] is Relation-like set

bool [: the carrier' of S3, the carrier' of S3:] is set

f1 * (id the carrier' of S3) is Relation-like the carrier' of S3 -valued Function-like set

(f1 * (id the carrier' of S3)) * the ResultSort of S2 is Relation-like the carrier of S2 -valued Function-like set

the ResultSort of S2 * (id the carrier' of S3) is Relation-like the carrier' of S3 -defined the carrier of S2 -valued Function-like Element of bool [: the carrier' of S3, the carrier of S2:]

[: the carrier' of S3, the carrier of S2:] is Relation-like set

bool [: the carrier' of S3, the carrier of S2:] is set

f1 * ( the ResultSort of S2 * (id the carrier' of S3)) is Relation-like the carrier of S2 -valued Function-like set

the ResultSort of S2 | the carrier' of S3 is Relation-like the carrier' of S3 -defined the carrier' of S2 -defined the carrier of S2 -valued Function-like Element of bool [: the carrier' of S2, the carrier of S2:]

f1 * ( the ResultSort of S2 | the carrier' of S3) is Relation-like the carrier of S2 -valued Function-like set

g1 is set

the Arity of S1 . g1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set

f1 . g1 is set

the Arity of S3 . (f1 . g1) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set

f2 is Relation-like Function-like set

f2 * X is Relation-like Function-like set

dom the Arity of S3 is set

the Arity of S2 . (f1 . g1) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set

S2 is non empty feasible () ManySortedSign

S1 is non empty feasible () ManySortedSign

X is Relation-like Function-like set

f1 is Relation-like Function-like set

S3 is MSAlgebra over S2

the Sorts of S3 is non empty Relation-like the carrier of S2 -defined Function-like total set

the carrier of S2 is non empty set

X * the Sorts of S3 is Relation-like Function-like set

the Charact of S3 is Relation-like the carrier' of S2 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S2 * ( the Sorts of S3 #), the ResultSort of S2 * the Sorts of S3

the carrier' of S2 is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]

the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)

[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set

bool [: the carrier' of S2,( the carrier of S2 *):] is set

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

the Arity of S2 * ( the Sorts of S3 #) is Relation-like the carrier' of S2 -defined Function-like total set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like total V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]

[: the carrier' of S2, the carrier of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier of S2:] is set

the ResultSort of S2 * the Sorts of S3 is Relation-like the carrier' of S2 -defined Function-like total set

f1 * the Charact of S3 is Relation-like Function-like V53() V54() set

dom X is set

the carrier of S1 is non empty set

rng X is set

[: the carrier of S1, the carrier of S2:] is Relation-like set

bool [: the carrier of S1, the carrier of S2:] is set

rng f1 is set

dom f1 is set

the carrier' of S1 is set

[: the carrier' of S1, the carrier' of S2:] is Relation-like set

bool [: the carrier' of S1, the carrier' of S2:] is set

dom the Charact of S3 is set

f2 is Relation-like the carrier' of S1 -defined the carrier' of S2 -valued Function-like V29( the carrier' of S1, the carrier' of S2) Element of bool [: the carrier' of S1, the carrier' of S2:]

f2 * the Charact of S3 is Relation-like the carrier' of S1 -defined Function-like V53() V54() set

dom (f2 * the Charact of S3) is set

g2 is Relation-like the carrier' of S1 -defined Function-like total set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

g1 is non empty Relation-like the carrier of S1 -defined the carrier of S2 -valued Function-like total V29( the carrier of S1, the carrier of S2) Element of bool [: the carrier of S1, the carrier of S2:]

g1 * the Sorts of S3 is non empty Relation-like the carrier of S1 -defined Function-like total set

(g1 * the Sorts of S3) # is non empty Relation-like the carrier of S1 * -defined Function-like total set

the Arity of S1 * ((g1 * the Sorts of S3) #) is Relation-like the carrier' of S1 -defined Function-like total set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

the ResultSort of S1 * (g1 * the Sorts of S3) is Relation-like the carrier' of S1 -defined Function-like total set

f is set

g2 . f is set

( the Arity of S1 * ((g1 * the Sorts of S3) #)) . f is set

( the ResultSort of S1 * (g1 * the Sorts of S3)) . f is set

[:(( the Arity of S1 * ((g1 * the Sorts of S3) #)) . f),(( the ResultSort of S1 * (g1 * the Sorts of S3)) . f):] is Relation-like set

bool [:(( the Arity of S1 * ((g1 * the Sorts of S3) #)) . f),(( the ResultSort of S1 * (g1 * the Sorts of S3)) . f):] is set

the Arity of S1 . f is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set

f1 . f is set

the Arity of S2 . (f1 . f) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set

Af1 is Element of the carrier' of S1

g2 . Af1 is set

f2 . Af1 is set

the Charact of S3 . (f2 . Af1) is Relation-like Function-like set

g1 * the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S2 -valued Function-like total V29( the carrier' of S1, the carrier of S2) Element of bool [: the carrier' of S1, the carrier of S2:]

[: the carrier' of S1, the carrier of S2:] is Relation-like set

bool [: the carrier' of S1, the carrier of S2:] is set

(g1 * the ResultSort of S1) * the Sorts of S3 is Relation-like the carrier' of S1 -defined Function-like total set

f1 * the ResultSort of S2 is Relation-like the carrier of S2 -valued Function-like set

(f1 * the ResultSort of S2) * the Sorts of S3 is Relation-like Function-like set

f1 * ( the ResultSort of S2 * the Sorts of S3) is Relation-like Function-like set

( the ResultSort of S1 * (g1 * the Sorts of S3)) . Af1 is set

( the ResultSort of S2 * the Sorts of S3) . (f2 . Af1) is set

g is Relation-like NAT -defined the carrier of S1 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *

g * (g1 * the Sorts of S3) is Relation-like NAT -defined Function-like set

g1 * g is Relation-like NAT -defined the carrier of S2 -valued Function-like Element of bool [:NAT, the carrier of S2:]

[:NAT, the carrier of S2:] is Relation-like set

bool [:NAT, the carrier of S2:] is set

(g1 * g) * the Sorts of S3 is Relation-like NAT -defined Function-like set

Af is Relation-like NAT -defined the carrier of S2 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S2 *

Af * the Sorts of S3 is Relation-like NAT -defined Function-like set

( the Arity of S1 * ((g1 * the Sorts of S3) #)) . Af1 is set

((g1 * the Sorts of S3) #) . g is set

product (g * (g1 * the Sorts of S3)) is set

( the Sorts of S3 #) . Af is set

( the Arity of S2 * ( the Sorts of S3 #)) . (f2 . Af1) is set

f is Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ((g1 * the Sorts of S3) #), the ResultSort of S1 * (g1 * the Sorts of S3)

MSAlgebra(# (g1 * the Sorts of S3),f #) is strict MSAlgebra over S1

the Sorts of MSAlgebra(# (g1 * the Sorts of S3),f #) is non empty Relation-like the carrier of S1 -defined Function-like total set

the Charact of MSAlgebra(# (g1 * the Sorts of S3),f #) is Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of MSAlgebra(# (g1 * the Sorts of S3),f #) #), the ResultSort of S1 * the Sorts of MSAlgebra(# (g1 * the Sorts of S3),f #)

the Sorts of MSAlgebra(# (g1 * the Sorts of S3),f #) # is non empty Relation-like the carrier of S1 * -defined Function-like total set

the Arity of S1 * ( the Sorts of MSAlgebra(# (g1 * the Sorts of S3),f #) #) is Relation-like the carrier' of S1 -defined Function-like total set

the ResultSort of S1 * the Sorts of MSAlgebra(# (g1 * the Sorts of S3),f #) is Relation-like the carrier' of S1 -defined Function-like total set

g1 is strict MSAlgebra over S1

the Sorts of g1 is non empty Relation-like the carrier of S1 -defined Function-like total set

the carrier of S1 is non empty set

the Charact of g1 is Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of g1 #), the ResultSort of S1 * the Sorts of g1

the carrier' of S1 is set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]

the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)

[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set

bool [: the carrier' of S1,( the carrier of S1 *):] is set

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

the Arity of S1 * ( the Sorts of g1 #) is Relation-like the carrier' of S1 -defined Function-like total set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]

[: the carrier' of S1, the carrier of S1:] is Relation-like set

bool [: the carrier' of S1, the carrier of S1:] is set

the ResultSort of S1 * the Sorts of g1 is Relation-like the carrier' of S1 -defined Function-like total set

f2 is strict MSAlgebra over S1

the Sorts of f2 is non empty Relation-like the carrier of S1 -defined Function-like total set

the Charact of f2 is Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of f2 #), the ResultSort of S1 * the Sorts of f2

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

the Arity of S1 * ( the Sorts of f2 #) is Relation-like the carrier' of S1 -defined Function-like total set

the ResultSort of S1 * the Sorts of f2 is Relation-like the carrier' of S1 -defined Function-like total set

S1 is non empty feasible () ManySortedSign

S2 is non empty feasible () ManySortedSign

S3 is MSAlgebra over S1

the carrier of S2 is non empty set

id the carrier of S2 is non empty Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]

[: the carrier of S2, the carrier of S2:] is Relation-like set

bool [: the carrier of S2, the carrier of S2:] is set

the carrier' of S2 is set

id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]

[: the carrier' of S2, the carrier' of S2:] is Relation-like set

bool [: the carrier' of S2, the carrier' of S2:] is set

(S2,S1,S3,(id the carrier of S2),(id the carrier' of S2)) is strict MSAlgebra over S2

S2 is non empty feasible () ManySortedSign

S1 is non empty feasible () ManySortedSign

S3 is MSAlgebra over S2

the Sorts of S3 is non empty Relation-like the carrier of S2 -defined Function-like total set

the carrier of S2 is non empty set

the Charact of S3 is Relation-like the carrier' of S2 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S2 * ( the Sorts of S3 #), the ResultSort of S2 * the Sorts of S3

the carrier' of S2 is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]

the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)

[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set

bool [: the carrier' of S2,( the carrier of S2 *):] is set

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

the Arity of S2 * ( the Sorts of S3 #) is Relation-like the carrier' of S2 -defined Function-like total set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like total V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]

[: