:: INSTALG1 semantic presentation

REAL is set

NAT is set

1 is non empty set
{{},1} is non empty set
Trees is non empty constituted-Trees set

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

bool () is set

bool is set

bool is set
2 is non empty set
3 is non empty set

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

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))

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

rng f1 is set
g1 is set
dom f1 is Element of bool NAT
f2 is set
f1 . f2 is set

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
() /. g2 is Element of the carrier of S1
(FreeSort S3) . (() /. g2) is non empty set
FreeSort (S3,(() /. g2)) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA S3))
bool (TS (DTConMSA S3)) is set
dom () is Element of bool NAT

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

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

dom () is Element of bool NAT
() /. f1 is Element of the carrier of S1
the Sorts of S2 . (() /. f1) is set
the Sorts of S3 . (() /. 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

(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

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

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

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

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 S1 . g2 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *

Frege (() * g1) is Relation-like product K180((() * g1)) -defined Function-like total V53() V54() set
K180((() * g1)) is Relation-like Function-like set
product K180((() * g1)) is set
(Frege (() * 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 . () is Relation-like the Sorts of X . () -defined the Sorts of f1 . () -valued Function-like V29( the Sorts of X . (), the Sorts of f1 . ()) Element of bool [:( the Sorts of X . ()),( the Sorts of f1 . ()):]
the Sorts of X . () is set
the Sorts of f1 . () is set
[:( the Sorts of X . ()),( the Sorts of f1 . ()):] is Relation-like set
bool [:( the Sorts of X . ()),( the Sorts of f1 . ()):] 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 . ()) . ((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 . () is Relation-like the Sorts of S2 . () -defined the Sorts of S3 . () -valued Function-like V29( the Sorts of S2 . (), the Sorts of S3 . ()) Element of bool [:( the Sorts of S2 . ()),( the Sorts of S3 . ()):]
the Sorts of S2 . () is set
the Sorts of S3 . () is set
[:( the Sorts of S2 . ()),( the Sorts of S3 . ()):] is Relation-like set
bool [:( the Sorts of S2 . ()),( the Sorts of S3 . ()):] 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 . ()) . ((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

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

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

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

(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

(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 * (id the carrier of S2) is Relation-like the carrier of S2 -valued Function-like set

rng f2 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 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 | 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)

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

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

f1 . g1 is set

dom the Arity of S3 is set

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
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

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

f1 . f is 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 * (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

( 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:]