:: EQUATION semantic presentation

NAT is non empty V21() V22() V23() Element of bool REAL
REAL is set
bool REAL is non empty set
NAT is non empty V21() V22() V23() set
bool NAT is non empty set
bool NAT is non empty set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() Function-yielding Relation-yielding FinSequence-like FinSubsequence-like FinSequence-membered set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() Function-yielding Relation-yielding FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() Function-yielding Relation-yielding FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty set
{{},1} is non empty finite set
K269() is set
bool K269() is non empty set
K270() is Element of bool K269()
K310() is non empty V109() L13()
the carrier of K310() is non empty set
K273( the carrier of K310()) is non empty M20( the carrier of K310())
K309(K310()) is Element of bool K273( the carrier of K310())
bool K273( the carrier of K310()) is non empty set
[:K309(K310()),NAT:] is Relation-like set
bool [:K309(K310()),NAT:] is non empty set
[:NAT,K309(K310()):] is Relation-like set
bool [:NAT,K309(K310()):] is non empty set
2 is non empty set
3 is non empty set
product {} is set
{{}} is functional non empty finite V32() set
I is set
S is non empty set
[:I,S:] is Relation-like set
bool [:I,S:] is non empty set
E is non empty set
[:S,E:] is Relation-like non empty set
bool [:S,E:] is non empty set
F is Relation-like I -defined S -valued Function-like total quasi_total Element of bool [:I,S:]
s is Relation-like S -defined E -valued Function-like non empty total quasi_total Element of bool [:S,E:]
s * F is Relation-like I -defined E -valued Function-like total quasi_total Element of bool [:I,E:]
[:I,E:] is Relation-like set
bool [:I,E:] is non empty set
rng (s * F) is Element of bool E
bool E is non empty set
rng s is non empty Element of bool E
e is set
dom (s * F) is Element of bool I
bool I is non empty set
i is set
(s * F) . i is set
dom F is Element of bool I
F . i is set
rng F is Element of bool S
bool S is non empty set
dom s is non empty Element of bool S
s . (F . i) is set
I is set
S is Relation-like I -defined Function-like total set
E is Relation-like non-empty I -defined Function-like total set
F is Relation-like non-empty I -defined Function-like total set
s is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of S,E
e is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of E,F
e ** s is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of S,F
i is set
e . i is Relation-like Function-like set
proj2 (e . i) is set
F . i is set
s . i is Relation-like Function-like set
S . i is set
E . i is set
[:(S . i),(E . i):] is Relation-like set
bool [:(S . i),(E . i):] is non empty set
[:(E . i),(F . i):] is Relation-like set
bool [:(E . i),(F . i):] is non empty set
(s . i) * (e . i) is Relation-like Function-like set
proj2 ((s . i) * (e . i)) is set
(e ** s) . i is Relation-like Function-like set
proj2 ((e ** s) . i) is set
I is non empty set
S is non empty set
E is set
Funcs (S,E) is functional set
Funcs (I,(Funcs (S,E))) is functional set
F is set
s is Relation-like Function-like set
commute s is Relation-like Function-like Function-yielding Relation-yielding set
(commute s) . F is Relation-like Function-like set
proj1 ((commute s) . F) is set
proj2 ((commute s) . F) is set
Funcs (I,E) is functional set
Funcs (S,(Funcs (I,E))) is functional set
proj2 (commute s) is set
i is Relation-like Function-like set
proj1 i is set
proj2 i is set
i is Relation-like Function-like set
proj1 i is set
proj2 i is set
i is Relation-like Function-like set
proj1 i is set
proj2 i is set
I is set
S is Relation-like I -defined Function-like total set
E is Relation-like I -defined Function-like total set
F is Relation-like I -defined Function-like total Function-yielding Relation-yielding set
doms F is Relation-like I -defined Function-like total set
rngs F is Relation-like I -defined Function-like total set
s is set
F . s is Relation-like Function-like set
S . s is set
E . s is set
[:(S . s),(E . s):] is Relation-like set
bool [:(S . s),(E . s):] is non empty set
e is non empty set
i is Element of e
F . i is Relation-like Function-like set
proj1 (F . i) is set
S . i is set
proj2 (F . i) is set
(rngs F) . i is set
E . i is set
I is set
S is Relation-like I -defined Function-like total set
E is Relation-like I -defined Function-like total set
F is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of S,E
s is Relation-like I -defined Function-like total ManySortedSubset of S
e is Relation-like I -defined Function-like total ManySortedSubset of S
F || s is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of s,E
F || e is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of e,E
i is Relation-like I -defined Function-like total ManySortedSubset of s
(F || s) || i is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of i,E
A is set
F . A is Relation-like Function-like set
S . A is set
E . A is set
[:(S . A),(E . A):] is Relation-like set
bool [:(S . A),(E . A):] is non empty set
i . A is set
s . A is set
(F || s) . A is Relation-like Function-like set
[:(s . A),(E . A):] is Relation-like set
bool [:(s . A),(E . A):] is non empty set
(F . A) | (s . A) is Relation-like Function-like set
((F || s) || i) . A is Relation-like Function-like set
((F || s) . A) | (i . A) is Relation-like Function-like set
A is Relation-like s . A -defined E . A -valued Function-like quasi_total Element of bool [:(s . A),(E . A):]
A | (i . A) is Relation-like i . A -defined s . A -defined E . A -valued Function-like Element of bool [:(s . A),(E . A):]
(F . A) | (i . A) is Relation-like Function-like set
(F || e) . A is Relation-like Function-like set
I is set
S is Relation-like non-empty I -defined Function-like total set
E is Relation-like I -defined Function-like total set
F is Relation-like I -defined Function-like total ManySortedSubset of E
s is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of F,S
e is set
E . e is set
S . e is set
F . e is set
[:(F . e),(S . e):] is Relation-like set
bool [:(F . e),(S . e):] is non empty set
s . e is Relation-like Function-like set
A is set
i is Relation-like F . e -defined S . e -valued Function-like quasi_total Element of bool [:(F . e),(S . e):]
i . A is set
A is set
i is Relation-like F . e -defined S . e -valued Function-like quasi_total Element of bool [:(F . e),(S . e):]
i . A is set
e is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of E,S
e || F is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of F,S
i is set
F . i is set
S . i is set
[:(F . i),(S . i):] is Relation-like set
bool [:(F . i),(S . i):] is non empty set
s . i is Relation-like Function-like set
A is Relation-like F . i -defined S . i -valued Function-like quasi_total Element of bool [:(F . i),(S . i):]
dom A is Element of bool (F . i)
bool (F . i) is non empty set
E . i is set
[:(E . i),(S . i):] is Relation-like set
bool [:(E . i),(S . i):] is non empty set
e . i is Relation-like Function-like set
A is Relation-like E . i -defined S . i -valued Function-like quasi_total Element of bool [:(E . i),(S . i):]
A | (F . i) is Relation-like F . i -defined E . i -defined S . i -valued Function-like Element of bool [:(E . i),(S . i):]
Z is set
A . Z is set
(A | (F . i)) . Z is set
A . Z is set
G is Relation-like F . i -defined S . i -valued Function-like quasi_total Element of bool [:(F . i),(S . i):]
G . Z is set
dom A is Element of bool (E . i)
bool (E . i) is non empty set
dom (A | (F . i)) is Element of bool (E . i)
(e || F) . i is Relation-like Function-like set
I is set
E is Relation-like I -defined Function-like total Function-yielding Relation-yielding set
S is Relation-like I -defined Function-like total set
F is Relation-like I -defined Function-like total set
F is Relation-like I -defined Function-like total set
s is Relation-like I -defined Function-like total set
e is set
F . e is set
E . e is Relation-like Function-like set
S . e is set
(E . e) " (S . e) is set
s . e is set
I is set
S is Relation-like I -defined Function-like total set
E is Relation-like I -defined Function-like total set
F is Relation-like I -defined Function-like total set
s is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of S,E
s .:.: F is Relation-like I -defined Function-like total set
e is set
(s .:.: F) . e is set
E . e is set
i is non empty set
A is Relation-like i -defined Function-like non empty total set
Z is Relation-like i -defined Function-like non empty total set
A is Element of i
A . A is set
Z . A is set
G is Relation-like i -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of A,Z
G . A is Relation-like A . A -defined Z . A -valued Function-like quasi_total Element of bool [:(A . A),(Z . A):]
[:(A . A),(Z . A):] is Relation-like set
bool [:(A . A),(Z . A):] is non empty set
F . A is set
(G . A) .: (F . A) is Element of bool (Z . A)
bool (Z . A) is non empty set
E . A is set
I is set
S is Relation-like I -defined Function-like total set
E is Relation-like I -defined Function-like total set
F is Relation-like I -defined Function-like total set
s is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of S,E
(I,F,s) is Relation-like I -defined Function-like total set
e is set
(I,F,s) . e is set
S . e is set
i is non empty set
A is Relation-like i -defined Function-like non empty total set
Z is Relation-like i -defined Function-like non empty total set
A is Element of i
A . A is set
Z . A is set
G is Relation-like i -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of A,Z
G . A is Relation-like A . A -defined Z . A -valued Function-like quasi_total Element of bool [:(A . A),(Z . A):]
[:(A . A),(Z . A):] is Relation-like set
bool [:(A . A),(Z . A):] is non empty set
F . A is set
(G . A) " (F . A) is Element of bool (A . A)
bool (A . A) is non empty set
S . A is set
I is set
S is Relation-like I -defined Function-like total set
E is Relation-like I -defined Function-like total set
F is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of S,E
F .:.: S is Relation-like I -defined Function-like total set
s is set
F . s is Relation-like Function-like set
S . s is set
E . s is set
[:(S . s),(E . s):] is Relation-like set
bool [:(S . s),(E . s):] is non empty set
(F .:.: S) . s is set
(F . s) .: (S . s) is set
proj2 (F . s) is set
(F .:.: S) . s is set
(F . s) .: (S . s) is set
I is set
S is Relation-like I -defined Function-like total set
E is Relation-like I -defined Function-like total set
F is Relation-like I -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of S,E
(I,E,F) is Relation-like I -defined Function-like total set
s is set
F . s is Relation-like Function-like set
S . s is set
E . s is set
[:(S . s),(E . s):] is Relation-like set
bool [:(S . s),(E . s):] is non empty set
(I,E,F) . s is set
(F . s) " (E . s) is set
I is set
S is Relation-like I -defined Function-like total set
E is Relation-like I -defined Function-like total Function-yielding Relation-yielding set
rngs E is Relation-like I -defined Function-like total set
(I,S,E) is Relation-like I -defined Function-like total set
E .:.: (I,S,E) is Relation-like I -defined Function-like total set
F is set
S . F is set
(rngs E) . F is set
E . F is Relation-like Function-like set
proj2 (E . F) is set
(E .:.: (I,S,E)) . F is set
(I,S,E) . F is set
(E . F) .: ((I,S,E) . F) is set
(E . F) " (S . F) is set
(E . F) .: ((E . F) " (S . F)) is set
I is set
S is Relation-like I -defined Function-like total Function-yielding Relation-yielding set
rngs S is Relation-like I -defined Function-like total set
E is Relation-like I -defined Function-like total set
S .:.: E is Relation-like I -defined Function-like total set
F is set
(S .:.: E) . F is set
(rngs S) . F is set
S . F is Relation-like Function-like set
E . F is set
(S . F) .: (E . F) is set
proj2 (S . F) is set
I is set
S is Relation-like I -defined Function-like total Function-yielding Relation-yielding set
doms S is Relation-like I -defined Function-like total set
S .:.: (doms S) is Relation-like I -defined Function-like total set
rngs S is Relation-like I -defined Function-like total set
E is set
(S .:.: (doms S)) . E is set
S . E is Relation-like Function-like set
(doms S) . E is set
(S . E) .: ((doms S) . E) is set
proj1 (S . E) is set
(S . E) .: (proj1 (S . E)) is set
proj2 (S . E) is set
(rngs S) . E is set
I is set
S is Relation-like I -defined Function-like total Function-yielding Relation-yielding set
rngs S is Relation-like I -defined Function-like total set
(I,(rngs S),S) is Relation-like I -defined Function-like total set
doms S is Relation-like I -defined Function-like total set
E is set
(I,(rngs S),S) . E is set
S . E is Relation-like Function-like set
(rngs S) . E is set
(S . E) " ((rngs S) . E) is set
proj2 (S . E) is set
(S . E) " (proj2 (S . E)) is set
proj1 (S . E) is set
(doms S) . E is set
I is set
S is Relation-like I -defined Function-like total set
id S is Relation-like I -defined Function-like total Function-yielding Relation-yielding "1-1" "onto" ManySortedFunction of S,S
(id S) .:.: S is Relation-like I -defined Function-like total set
rngs (id S) is Relation-like I -defined Function-like total set
doms (id S) is Relation-like I -defined Function-like total set
I is set
S is Relation-like I -defined Function-like total set
id S is Relation-like I -defined Function-like total Function-yielding Relation-yielding "1-1" "onto" ManySortedFunction of S,S
(I,S,(id S)) is Relation-like I -defined Function-like total set
rngs (id S) is Relation-like I -defined Function-like total set
doms (id S) is Relation-like I -defined Function-like total set
I is non empty non void feasible ManySortedSign
S is MSAlgebra over I
the Sorts of S is Relation-like the carrier of I -defined Function-like non empty total set
the carrier of I is non empty set
the Charact of S is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of S #), the ResultSort of I * the Sorts of S
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
the Sorts of S # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ( the Sorts of S #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * the Sorts of S is Relation-like the carrier' of I -defined Function-like non empty total set
MSAlgebra(# the Sorts of S, the Charact of S #) is strict MSAlgebra over I
the Sorts of MSAlgebra(# the Sorts of S, the Charact of S #) is Relation-like the carrier of I -defined Function-like non empty total set
F is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of MSAlgebra(# the Sorts of S, the Charact of S #)
Opers (MSAlgebra(# the Sorts of S, the Charact of S #),F) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * (F #), the ResultSort of I * F
F # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * (F #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I * F is Relation-like the carrier' of I -defined Function-like non empty total set
I is non empty non void feasible ManySortedSign
the carrier' of I is non empty set
S is MSAlgebra over I
E is MSSubAlgebra of S
F is Element of the carrier' of I
Args (F,E) is Element of proj2 ( the Sorts of E #)
the carrier of I is non empty set
the Sorts of E is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of E # is Relation-like the carrier of I * -defined Function-like non empty total set
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
proj2 ( the Sorts of E #) is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
the Arity of I * ( the Sorts of E #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of E #)) . F is set
Args (F,S) is Element of proj2 ( the Sorts of S #)
the Sorts of S is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of S # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of S #) is non empty set
the Arity of I * ( the Sorts of S #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of S #)) . F is set
s is set
the Charact of S is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of S #), the ResultSort of I * the Sorts of S
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * the Sorts of S is Relation-like the carrier' of I -defined Function-like non empty total set
MSAlgebra(# the Sorts of S, the Charact of S #) is strict MSAlgebra over I
e is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of S
i is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of S
e # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * (e #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * (e #)) . F is set
i # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * (i #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * (i #)) . F is set
I is non empty non void feasible ManySortedSign
the carrier' of I is non empty set
S is MSAlgebra over I
E is MSSubAlgebra of S
F is Element of the carrier' of I
Args (F,E) is Element of proj2 ( the Sorts of E #)
the carrier of I is non empty set
the Sorts of E is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of E # is Relation-like the carrier of I * -defined Function-like non empty total set
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
proj2 ( the Sorts of E #) is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
the Arity of I * ( the Sorts of E #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of E #)) . F is set
Den (F,E) is Relation-like Args (F,E) -defined Result (F,E) -valued Function-like quasi_total Element of bool [:(Args (F,E)),(Result (F,E)):]
Result (F,E) is Element of proj2 the Sorts of E
proj2 the Sorts of E is non empty set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * the Sorts of E is Relation-like the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of E) . F is set
[:(Args (F,E)),(Result (F,E)):] is Relation-like set
bool [:(Args (F,E)),(Result (F,E)):] is non empty set
the Charact of E is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of E #), the ResultSort of I * the Sorts of E
the Charact of E . F is Relation-like Function-like set
Den (F,S) is Relation-like Args (F,S) -defined Result (F,S) -valued Function-like quasi_total Element of bool [:(Args (F,S)),(Result (F,S)):]
Args (F,S) is Element of proj2 ( the Sorts of S #)
the Sorts of S is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of S # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of S #) is non empty set
the Arity of I * ( the Sorts of S #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of S #)) . F is set
Result (F,S) is Element of proj2 the Sorts of S
proj2 the Sorts of S is non empty set
the ResultSort of I * the Sorts of S is Relation-like the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of S) . F is set
[:(Args (F,S)),(Result (F,S)):] is Relation-like set
bool [:(Args (F,S)),(Result (F,S)):] is non empty set
the Charact of S is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of S #), the ResultSort of I * the Sorts of S
the Charact of S . F is Relation-like Function-like set
s is set
(Den (F,E)) . s is set
(Den (F,S)) . s is set
e is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of S
e # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * (e #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I * e is Relation-like the carrier' of I -defined Function-like non empty total set
Opers (S,e) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * (e #), the ResultSort of I * e
(Opers (S,e)) . F is Relation-like ( the Arity of I * (e #)) . F -defined ( the ResultSort of I * e) . F -valued Function-like quasi_total Element of bool [:(( the Arity of I * (e #)) . F),(( the ResultSort of I * e) . F):]
( the Arity of I * (e #)) . F is set
( the ResultSort of I * e) . F is set
[:(( the Arity of I * (e #)) . F),(( the ResultSort of I * e) . F):] is Relation-like set
bool [:(( the Arity of I * (e #)) . F),(( the ResultSort of I * e) . F):] is non empty set
((Opers (S,e)) . F) . s is set
F /. e is Relation-like ( the Arity of I * (e #)) . F -defined ( the ResultSort of I * e) . F -valued Function-like quasi_total Element of bool [:(( the Arity of I * (e #)) . F),(( the ResultSort of I * e) . F):]
(F /. e) . s is set
(Den (F,S)) | (( the Arity of I * (e #)) . F) is Relation-like Args (F,S) -defined ( the Arity of I * (e #)) . F -defined Args (F,S) -defined Result (F,S) -valued Function-like Element of bool [:(Args (F,S)),(Result (F,S)):]
((Den (F,S)) | (( the Arity of I * (e #)) . F)) . s is set
I is set
S is non empty non void feasible ManySortedSign
the carrier' of S is non empty set
E is Relation-like I -defined Function-like total MSAlgebra-Family of I,S
product E is strict non-empty feasible MSAlgebra over S
SORTS E is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the carrier of S is non empty set
OPS E is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((SORTS E) #), the ResultSort of S * (SORTS E)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is Relation-like non empty set
bool [: the carrier' of S,( the carrier of S *):] is non empty set
(SORTS E) # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ((SORTS E) #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like non empty set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * (SORTS E) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (SORTS E),(OPS E) #) is strict MSAlgebra over S
F is MSSubAlgebra of product E
s is Element of the carrier' of S
Args (s,F) is Element of proj2 ( the Sorts of F #)
the Sorts of F is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of F # is Relation-like the carrier of S * -defined Function-like non empty total set
proj2 ( the Sorts of F #) is non empty set
the Arity of S * ( the Sorts of F #) is Relation-like the carrier' of S -defined Function-like non empty total set
( the Arity of S * ( the Sorts of F #)) . s is set
Den (s,F) is Relation-like Args (s,F) -defined Result (s,F) -valued Function-like quasi_total Element of bool [:(Args (s,F)),(Result (s,F)):]
Result (s,F) is Element of proj2 the Sorts of F
proj2 the Sorts of F is non empty set
the ResultSort of S * the Sorts of F is Relation-like the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of F) . s is set
[:(Args (s,F)),(Result (s,F)):] is Relation-like set
bool [:(Args (s,F)),(Result (s,F)):] is non empty set
the Charact of F is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ( the Sorts of F #), the ResultSort of S * the Sorts of F
the Charact of F . s is Relation-like Function-like set
Den (s,(product E)) is Relation-like Args (s,(product E)) -defined Result (s,(product E)) -valued Function-like non empty total quasi_total Element of bool [:(Args (s,(product E))),(Result (s,(product E))):]
Args (s,(product E)) is functional non empty Element of proj2 ( the Sorts of (product E) #)
the Sorts of (product E) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of (product E) # is Relation-like the carrier of S * -defined Function-like non empty total set
proj2 ( the Sorts of (product E) #) is non empty set
the Arity of S * ( the Sorts of (product E) #) is Relation-like the carrier' of S -defined Function-like non empty total set
( the Arity of S * ( the Sorts of (product E) #)) . s is set
Result (s,(product E)) is non empty Element of proj2 the Sorts of (product E)
proj2 the Sorts of (product E) is non empty V155() set
the ResultSort of S * the Sorts of (product E) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of (product E)) . s is non empty set
[:(Args (s,(product E))),(Result (s,(product E))):] is Relation-like non empty set
bool [:(Args (s,(product E))),(Result (s,(product E))):] is non empty set
the Charact of (product E) is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ( the Sorts of (product E) #), the ResultSort of S * the Sorts of (product E)
the Charact of (product E) . s is Relation-like Function-like set
e is set
(Den (s,F)) . e is set
(Den (s,(product E))) . e is set
the_result_sort_of s is Element of the carrier of S
the ResultSort of S . s is Element of the carrier of S
Carrier (E,(the_result_sort_of s)) is Relation-like non-empty I -defined Function-like total set
product (Carrier (E,(the_result_sort_of s))) is set
(SORTS E) . (the_result_sort_of s) is non empty set
A is Relation-like Function-like Element of (SORTS E) . (the_result_sort_of s)
I is non empty non void feasible ManySortedSign
S is MSAlgebra over I
E is MSSubAlgebra of S
MSSub S is non empty set
F is set
s is set
e is strict MSSubAlgebra of S
F is set
s is set
I is non empty non void feasible ManySortedSign
S is MSAlgebra over I
E is MSSubAlgebra of S
(I,S,E) is set
the Sorts of E is Relation-like the carrier of I -defined Function-like non empty total set
the carrier of I is non empty set
the Charact of E is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of E #), the ResultSort of I * the Sorts of E
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
the Sorts of E # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ( the Sorts of E #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * the Sorts of E is Relation-like the carrier' of I -defined Function-like non empty total set
MSAlgebra(# the Sorts of E, the Charact of E #) is strict MSAlgebra over I
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeMSA the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set is strict non-empty free feasible MSAlgebra over I
FreeSort the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set ) #), the ResultSort of I * (FreeSort the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set )
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set ) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set ) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set ) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set ),(FreeOper the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set ) #) is strict MSAlgebra over I
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
S is non-empty feasible MSAlgebra over I
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
E is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S
GenMSAlg E is strict non-empty feasible MSSubAlgebra of S
F is non empty non void feasible ManySortedSign
the carrier of F is non empty set
s is MSAlgebra over F
the Sorts of s is Relation-like the carrier of F -defined Function-like non empty total set
e is Relation-like the carrier of F -defined Function-like non empty total ManySortedSubset of the Sorts of s
GenMSAlg e is strict MSSubAlgebra of s
i is Relation-like the carrier of F -defined Function-like non empty total GeneratorSet of s
the Sorts of (GenMSAlg E) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
I is non empty non void feasible ManySortedSign
S is non-empty feasible MSAlgebra over I
the carrier of I is non empty set
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S
GenMSAlg the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S is strict non-empty finitely-generated feasible MSSubAlgebra of S
I is non empty non void feasible ManySortedSign
S is feasible MSAlgebra over I
the Sorts of S is Relation-like the carrier of I -defined Function-like non empty total set
the carrier of I is non empty set
the Charact of S is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of S #), the ResultSort of I * the Sorts of S
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
the Sorts of S # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ( the Sorts of S #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * the Sorts of S is Relation-like the carrier' of I -defined Function-like non empty total set
MSAlgebra(# the Sorts of S, the Charact of S #) is strict MSAlgebra over I
E is MSSubAlgebra of S
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
the carrier' of I is non empty set
S is non-empty feasible MSAlgebra over I
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
E is MSAlgebra over I
the Sorts of E is Relation-like the carrier of I -defined Function-like non empty total set
F is MSSubAlgebra of E
the Sorts of F is Relation-like the carrier of I -defined Function-like non empty total set
s is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of E
e is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of E, the Sorts of S
e || s is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of s, the Sorts of S
i is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of F, the Sorts of S
A is Element of the carrier' of I
Args (A,E) is Element of proj2 ( the Sorts of E #)
the Sorts of E # is Relation-like the carrier of I * -defined Function-like non empty total set
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
proj2 ( the Sorts of E #) is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
the Arity of I * ( the Sorts of E #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of E #)) . A is set
Args (A,F) is Element of proj2 ( the Sorts of F #)
the Sorts of F # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of F #) is non empty set
the Arity of I * ( the Sorts of F #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of F #)) . A is set
A is Element of Args (A,E)
e # A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of Args (A,S)
Args (A,S) is functional non empty Element of proj2 ( the Sorts of S #)
the Sorts of S # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of S #) is non empty set
the Arity of I * ( the Sorts of S #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of S #)) . A is set
Z is Element of Args (A,F)
i # Z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of Args (A,S)
the_arity_of A is Relation-like NAT -defined the carrier of I -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of I *
the Arity of I . A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of I *
s is Relation-like Function-like set
proj1 s is set
dom (the_arity_of A) is finite Element of bool NAT
c₁₄ is Relation-like Function-like set
proj1 c₁₄ is set
ff is set
(the_arity_of A) . ff is set
the Sorts of E . ((the_arity_of A) . ff) is set
the Sorts of S . ((the_arity_of A) . ff) is set
[:( the Sorts of E . ((the_arity_of A) . ff)),( the Sorts of S . ((the_arity_of A) . ff)):] is Relation-like set
bool [:( the Sorts of E . ((the_arity_of A) . ff)),( the Sorts of S . ((the_arity_of A) . ff)):] is non empty set
e . ((the_arity_of A) . ff) is Relation-like Function-like set
y is V21() V22() V23() V27() set
(the_arity_of A) . y is set
i . ((the_arity_of A) . y) is Relation-like Function-like set
aa is Relation-like the Sorts of E . ((the_arity_of A) . ff) -defined the Sorts of S . ((the_arity_of A) . ff) -valued Function-like quasi_total Element of bool [:( the Sorts of E . ((the_arity_of A) . ff)),( the Sorts of S . ((the_arity_of A) . ff)):]
s . ((the_arity_of A) . ff) is set
aa | (s . ((the_arity_of A) . ff)) is Relation-like the Sorts of E . ((the_arity_of A) . ff) -defined s . ((the_arity_of A) . ff) -defined the Sorts of E . ((the_arity_of A) . ff) -defined the Sorts of S . ((the_arity_of A) . ff) -valued Function-like Element of bool [:( the Sorts of E . ((the_arity_of A) . ff)),( the Sorts of S . ((the_arity_of A) . ff)):]
(the_arity_of A) * the Sorts of F is Relation-like NAT -defined dom (the_arity_of A) -defined Function-like total finite set
dom ((the_arity_of A) * the Sorts of F) is finite Element of bool NAT
c₁₄ . ff is set
((the_arity_of A) * the Sorts of F) . ff is set
(e # A) . ff is set
(e # A) . y is set
(the_arity_of A) /. ff is Element of the carrier of I
e . ((the_arity_of A) /. ff) is Relation-like the Sorts of E . ((the_arity_of A) /. ff) -defined the Sorts of S . ((the_arity_of A) /. ff) -valued Function-like total quasi_total Element of bool [:( the Sorts of E . ((the_arity_of A) /. ff)),( the Sorts of S . ((the_arity_of A) /. ff)):]
the Sorts of E . ((the_arity_of A) /. ff) is set
the Sorts of S . ((the_arity_of A) /. ff) is non empty set
[:( the Sorts of E . ((the_arity_of A) /. ff)),( the Sorts of S . ((the_arity_of A) /. ff)):] is Relation-like set
bool [:( the Sorts of E . ((the_arity_of A) /. ff)),( the Sorts of S . ((the_arity_of A) /. ff)):] is non empty set
(e . ((the_arity_of A) /. ff)) . (c₁₄ . ff) is set
(e . ((the_arity_of A) . ff)) . (c₁₄ . ff) is set
i . ((the_arity_of A) . ff) is Relation-like Function-like set
(i . ((the_arity_of A) . ff)) . (c₁₄ . ff) is set
i . ((the_arity_of A) /. ff) is Relation-like the Sorts of F . ((the_arity_of A) /. ff) -defined the Sorts of S . ((the_arity_of A) /. ff) -valued Function-like total quasi_total Element of bool [:( the Sorts of F . ((the_arity_of A) /. ff)),( the Sorts of S . ((the_arity_of A) /. ff)):]
the Sorts of F . ((the_arity_of A) /. ff) is set
[:( the Sorts of F . ((the_arity_of A) /. ff)),( the Sorts of S . ((the_arity_of A) /. ff)):] is Relation-like set
bool [:( the Sorts of F . ((the_arity_of A) /. ff)),( the Sorts of S . ((the_arity_of A) /. ff)):] is non empty set
s . ff is set
(i . ((the_arity_of A) /. ff)) . (s . ff) is set
(i # Z) . y is set
(i # Z) . ff is set
dom (e # A) is finite Element of bool NAT
dom (i # Z) is finite Element of bool NAT
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
S is non-empty feasible MSAlgebra over I
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
E is feasible MSAlgebra over I
the Sorts of E is Relation-like the carrier of I -defined Function-like non empty total set
F is feasible MSSubAlgebra of E
the Sorts of F is Relation-like the carrier of I -defined Function-like non empty total set
s is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of E
e is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of E, the Sorts of S
e || s is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of s, the Sorts of S
i is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of F, the Sorts of S
the carrier' of I is non empty set
A is Element of the carrier' of I
Args (A,F) is Element of proj2 ( the Sorts of F #)
the Sorts of F # is Relation-like the carrier of I * -defined Function-like non empty total set
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
proj2 ( the Sorts of F #) is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
the Arity of I * ( the Sorts of F #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of F #)) . A is set
the_result_sort_of A is Element of the carrier of I
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I . A is Element of the carrier of I
i . (the_result_sort_of A) is Relation-like the Sorts of F . (the_result_sort_of A) -defined the Sorts of S . (the_result_sort_of A) -valued Function-like total quasi_total Element of bool [:( the Sorts of F . (the_result_sort_of A)),( the Sorts of S . (the_result_sort_of A)):]
the Sorts of F . (the_result_sort_of A) is set
the Sorts of S . (the_result_sort_of A) is non empty set
[:( the Sorts of F . (the_result_sort_of A)),( the Sorts of S . (the_result_sort_of A)):] is Relation-like set
bool [:( the Sorts of F . (the_result_sort_of A)),( the Sorts of S . (the_result_sort_of A)):] is non empty set
Den (A,F) is Relation-like Args (A,F) -defined Result (A,F) -valued Function-like quasi_total Element of bool [:(Args (A,F)),(Result (A,F)):]
Result (A,F) is Element of proj2 the Sorts of F
proj2 the Sorts of F is non empty set
the ResultSort of I * the Sorts of F is Relation-like the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of F) . A is set
[:(Args (A,F)),(Result (A,F)):] is Relation-like set
bool [:(Args (A,F)),(Result (A,F)):] is non empty set
the Charact of F is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of F #), the ResultSort of I * the Sorts of F
the Charact of F . A is Relation-like Function-like set
Den (A,S) is Relation-like Args (A,S) -defined Result (A,S) -valued Function-like non empty total quasi_total Element of bool [:(Args (A,S)),(Result (A,S)):]
Args (A,S) is functional non empty Element of proj2 ( the Sorts of S #)
the Sorts of S # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of S #) is non empty set
the Arity of I * ( the Sorts of S #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of S #)) . A is set
Result (A,S) is non empty Element of proj2 the Sorts of S
proj2 the Sorts of S is non empty V155() set
the ResultSort of I * the Sorts of S is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of S) . A is non empty set
[:(Args (A,S)),(Result (A,S)):] is Relation-like non empty set
bool [:(Args (A,S)),(Result (A,S)):] is non empty set
the Charact of S is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of S #), the ResultSort of I * the Sorts of S
the Charact of S . A is Relation-like Function-like set
A is Element of Args (A,F)
(Den (A,F)) . A is set
(i . (the_result_sort_of A)) . ((Den (A,F)) . A) is set
i # A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of Args (A,S)
(Den (A,S)) . (i # A) is set
Args (A,E) is Element of proj2 ( the Sorts of E #)
the Sorts of E # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of E #) is non empty set
the Arity of I * ( the Sorts of E #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of E #)) . A is set
the Sorts of F . ( the ResultSort of I . A) is set
Den (A,E) is Relation-like Args (A,E) -defined Result (A,E) -valued Function-like quasi_total Element of bool [:(Args (A,E)),(Result (A,E)):]
Result (A,E) is Element of proj2 the Sorts of E
proj2 the Sorts of E is non empty set
the ResultSort of I * the Sorts of E is Relation-like the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of E) . A is set
[:(Args (A,E)),(Result (A,E)):] is Relation-like set
bool [:(Args (A,E)),(Result (A,E)):] is non empty set
the Charact of E is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of E #), the ResultSort of I * the Sorts of E
the Charact of E . A is Relation-like Function-like set
(Den (A,E)) . A is set
e . (the_result_sort_of A) is Relation-like the Sorts of E . (the_result_sort_of A) -defined the Sorts of S . (the_result_sort_of A) -valued Function-like total quasi_total Element of bool [:( the Sorts of E . (the_result_sort_of A)),( the Sorts of S . (the_result_sort_of A)):]
the Sorts of E . (the_result_sort_of A) is set
[:( the Sorts of E . (the_result_sort_of A)),( the Sorts of S . (the_result_sort_of A)):] is Relation-like set
bool [:( the Sorts of E . (the_result_sort_of A)),( the Sorts of S . (the_result_sort_of A)):] is non empty set
(e . (the_result_sort_of A)) . ((Den (A,E)) . A) is set
Z is Element of Args (A,E)
e # Z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of Args (A,S)
(Den (A,S)) . (e # Z) is Element of Result (A,S)
(Den (A,S)) . (i # A) is Element of Result (A,S)
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
S is non-empty feasible MSAlgebra over I
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
E is strict non-empty feasible MSAlgebra over I
the Sorts of E is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
F is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of S
s is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total GeneratorSet of E
e is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of S, the Sorts of E
e .:.: F is Relation-like the carrier of I -defined Function-like non empty total set
Image e is strict non-empty feasible MSSubAlgebra of E
the Sorts of (Image e) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
e .:.: the Sorts of S is Relation-like the carrier of I -defined Function-like non empty total set
GenMSAlg s is strict non-empty feasible MSSubAlgebra of E
i is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of E
GenMSAlg i is strict non-empty feasible MSSubAlgebra of E
A is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of (Image e)
GenMSAlg A is strict non-empty feasible MSSubAlgebra of Image e
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
S is non-empty feasible MSAlgebra over I
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
E is non-empty feasible MSAlgebra over I
the Sorts of E is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
F is strict non-empty free feasible MSAlgebra over I
the Sorts of F is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
s is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of S, the Sorts of E
A is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of F, the Sorts of E
Z is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of F
A || Z is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of Z, the Sorts of E
G is set
Z . G is set
the Sorts of S . G is set
the Sorts of E . G is set
[:( the Sorts of S . G),( the Sorts of E . G):] is Relation-like set
bool [:( the Sorts of S . G),( the Sorts of E . G):] is non empty set
[:(Z . G),( the Sorts of E . G):] is Relation-like set
bool [:(Z . G),( the Sorts of E . G):] is non empty set
s . G is Relation-like Function-like set
(A || Z) . G is Relation-like Function-like set
c₁₄ is set
h is Relation-like Z . G -defined the Sorts of E . G -valued Function-like quasi_total Element of bool [:(Z . G),( the Sorts of E . G):]
h . c₁₄ is set
proj2 (s . G) is set
H is Relation-like the Sorts of S . G -defined the Sorts of E . G -valued Function-like quasi_total Element of bool [:( the Sorts of S . G),( the Sorts of E . G):]
{(h . c₁₄)} is non empty finite set
H " {(h . c₁₄)} is Element of bool ( the Sorts of S . G)
bool ( the Sorts of S . G) is non empty set
s is set
G is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of Z, the Sorts of S
h is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of F, the Sorts of S
h || Z is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of Z, the Sorts of S
H is set
the Sorts of S . H is set
the Sorts of E . H is set
[:( the Sorts of S . H),( the Sorts of E . H):] is Relation-like set
bool [:( the Sorts of S . H),( the Sorts of E . H):] is non empty set
s . H is Relation-like Function-like set
Z . H is set
[:(Z . H),( the Sorts of E . H):] is Relation-like set
bool [:(Z . H),( the Sorts of E . H):] is non empty set
(A || Z) . H is Relation-like Function-like set
[:(Z . H),( the Sorts of S . H):] is Relation-like set
bool [:(Z . H),( the Sorts of S . H):] is non empty set
G . H is Relation-like Function-like set
ff is Relation-like Z . H -defined the Sorts of S . H -valued Function-like quasi_total Element of bool [:(Z . H),( the Sorts of S . H):]
y is set
ff . y is set
aa is Relation-like the Sorts of S . H -defined the Sorts of E . H -valued Function-like quasi_total Element of bool [:( the Sorts of S . H),( the Sorts of E . H):]
WW is Relation-like Z . H -defined the Sorts of E . H -valued Function-like quasi_total Element of bool [:(Z . H),( the Sorts of E . H):]
WW . y is set
{(WW . y)} is non empty finite set
aa " {(WW . y)} is Element of bool ( the Sorts of S . H)
bool ( the Sorts of S . H) is non empty set
aa . (ff . y) is set
c₁₄ is Relation-like the Sorts of S . H -defined the Sorts of E . H -valued Function-like quasi_total Element of bool [:( the Sorts of S . H),( the Sorts of E . H):]
c₁₄ * ff is Relation-like Z . H -defined the Sorts of E . H -valued Function-like Element of bool [:(Z . H),( the Sorts of E . H):]
(c₁₄ * ff) . y is set
s is Relation-like Z . H -defined the Sorts of E . H -valued Function-like quasi_total Element of bool [:(Z . H),( the Sorts of E . H):]
s . y is set
dom s is Element of bool (Z . H)
bool (Z . H) is non empty set
dom (c₁₄ * ff) is Element of bool (Z . H)
s ** G is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of Z, the Sorts of E
(s ** G) . H is Relation-like Function-like set
s ** (h || Z) is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of Z, the Sorts of E
s ** h is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of F, the Sorts of E
(s ** h) || Z is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of Z, the Sorts of E
I is non empty non void feasible ManySortedSign
S is non empty finite set
E is non-empty feasible MSAlgebra over I
F is Relation-like S -defined Function-like non empty total MSAlgebra-Family of S,I
MSSub E is non empty set
{ b₁ where b₁ is Element of MSSub E : ex b₂ being Element of S ex b₃ being strict non-empty finitely-generated feasible MSSubAlgebra of E st
( b₁ = F . b₂ & b₁ = b₃ ) } is set
the carrier of I is non empty set
the Element of S is Element of S
F . the Element of S is non-empty feasible MSAlgebra over I
A is strict non-empty finitely-generated feasible MSSubAlgebra of E
A is non empty set
the Sorts of E is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
Bool the Sorts of E is functional non empty with_common_domain V123( the carrier of I, the Sorts of E) V124( the carrier of I, the Sorts of E) V125( the carrier of I, the Sorts of E) V126( the carrier of I, the Sorts of E) V127( the carrier of I, the Sorts of E) V128( the carrier of I, the Sorts of E) Element of bool (Bool the Sorts of E)
Bool the Sorts of E is functional non empty with_common_domain set
bool (Bool the Sorts of E) is non empty set
Z is Element of A
G is Element of MSSub E
h is Element of S
F . h is non-empty feasible MSAlgebra over I
H is strict non-empty finitely-generated feasible MSSubAlgebra of E
h is Element of S
F . h is non-empty feasible MSAlgebra over I
H is strict non-empty finitely-generated feasible MSSubAlgebra of E
c₁₄ is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of H
the Sorts of H is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
s is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of H
ff is Relation-like the carrier of I -defined Function-like non empty total Element of Bool the Sorts of E
y is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of H
[:A,(Bool the Sorts of E):] is Relation-like non empty set
bool [:A,(Bool the Sorts of E):] is non empty set
Z is Relation-like A -defined Bool the Sorts of E -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [:A,(Bool the Sorts of E):]
{ b₁ where b₁ is Element of bool ( the Sorts of E . a₁) : ex b₂ being Element of S ex b₃ being Relation-like the carrier of I -defined Function-like non empty total set st
( b₃ = Z . (F . b₂) & b₁ = b₃ . a₁ ) } is set
union { b₁ where b₁ is Element of bool ( the Sorts of E . a₁) : ex b₂ being Element of S ex b₃ being Relation-like the carrier of I -defined Function-like non empty total set st
( b₃ = Z . (F . b₂) & b₁ = b₃ . a₁ ) } is set
G is Relation-like the carrier of I -defined Function-like non empty total set
h is set
G . h is set
the Sorts of E . h is set
H is set
bool ( the Sorts of E . h) is non empty set
{ b₁ where b₁ is Element of bool ( the Sorts of E . h) : ex b₂ being Element of S ex b₃ being Relation-like the carrier of I -defined Function-like non empty total set st
( b₃ = Z . (F . b₂) & b₁ = b₃ . h ) } is set
union { b₁ where b₁ is Element of bool ( the Sorts of E . h) : ex b₂ being Element of S ex b₃ being Relation-like the carrier of I -defined Function-like non empty total set st
( b₃ = Z . (F . b₂) & b₁ = b₃ . h ) } is set
s is set
ff is Element of bool ( the Sorts of E . h)
h is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of E
c₁₄ is strict non-empty finitely-generated feasible MSSubAlgebra of E
Z . (F . the Element of S) is Relation-like Function-like set
ff is strict non-empty feasible MSSubAlgebra of E
y is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of ff
ff is set
h . ff is set
s is Relation-like the carrier of I -defined Function-like non empty total finite-yielding Element of Bool the Sorts of E
s . ff is finite set
y is strict non-empty feasible MSSubAlgebra of E
aa is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of y
y is set
the Sorts of E . ff is set
bool ( the Sorts of E . ff) is non empty set
{ b₁ where b₁ is Element of bool ( the Sorts of E . ff) : ex b₂ being Element of S ex b₃ being Relation-like the carrier of I -defined Function-like non empty total set st
( b₃ = Z . (F . b₂) & b₁ = b₃ . ff ) } is set
union { b₁ where b₁ is Element of bool ( the Sorts of E . ff) : ex b₂ being Element of S ex b₃ being Relation-like the carrier of I -defined Function-like non empty total set st
( b₃ = Z . (F . b₂) & b₁ = b₃ . ff ) } is set
s is set
the Sorts of E . s is set
bool ( the Sorts of E . s) is non empty set
{ b₁ where b₁ is Element of bool ( the Sorts of E . s) : ex b₂ being Element of S ex b₃ being Relation-like the carrier of I -defined Function-like non empty total set st
( b₃ = Z . (F . b₂) & b₁ = b₃ . s ) } is set
y is strict non-empty finitely-generated feasible MSSubAlgebra of E
Z . (F . the Element of S) is Relation-like Function-like set
WW is strict non-empty feasible MSSubAlgebra of E
XX is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of WW
aa is Relation-like the carrier of I -defined Function-like non empty total finite-yielding Element of Bool the Sorts of E
aa . s is finite set
H is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of E
c₁₄ is set
H . c₁₄ is set
the Sorts of E . c₁₄ is set
bool ( the Sorts of E . c₁₄) is non empty set
{ b₁ where b₁ is Element of bool ( the Sorts of E . c₁₄) : ex b₂ being Element of S ex b₃ being Relation-like the carrier of I -defined Function-like non empty total set st
( b₃ = Z . (F . b₂) & b₁ = b₃ . c₁₄ ) } is set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 y is finite set
ff is non empty set
aa is Element of S
F . aa is set
Z . (F . aa) is Relation-like Function-like set
F . aa is non-empty feasible MSAlgebra over I
WW is strict non-empty finitely-generated feasible MSSubAlgebra of E
Z . WW is Relation-like Function-like set
Z . (F . aa) is Relation-like Function-like set
L is strict non-empty feasible MSSubAlgebra of E
SY is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of L
XX is Relation-like the carrier of I -defined Function-like non empty total finite-yielding Element of Bool the Sorts of E
XX . c₁₄ is finite set
L is Element of ff
[:S,ff:] is Relation-like non empty set
bool [:S,ff:] is non empty set
aa is Relation-like S -defined ff -valued Function-like non empty total quasi_total finite Element of bool [:S,ff:]
dom aa is non empty finite Element of bool S
bool S is non empty finite V32() set
y * aa is Relation-like NAT -defined ff -valued Function-like finite set
WW is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 WW is finite set
XX is set
L is Element of bool ( the Sorts of E . c₁₄)
Y is Relation-like the carrier of I -defined Function-like non empty total set
SY is Element of S
F . SY is non-empty feasible MSAlgebra over I
Z . (F . SY) is Relation-like Function-like set
Y . c₁₄ is set
Y is Relation-like the carrier of I -defined Function-like non empty total set
SY is Element of S
F . SY is non-empty feasible MSAlgebra over I
Z . (F . SY) is Relation-like Function-like set
Y . c₁₄ is set
rng aa is non empty finite Element of bool ff
bool ff is non empty set
aa . SY is Element of ff
Y is Relation-like the carrier of I -defined Function-like non empty total set
Y . c₁₄ is set
XX is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 XX is finite set
rng aa is non empty finite Element of bool ff
bool ff is non empty set
L is set
y is set
aa is Element of bool ( the Sorts of E . c₁₄)
XX is Relation-like the carrier of I -defined Function-like non empty total set
WW is Element of S
F . WW is non-empty feasible MSAlgebra over I
Z . (F . WW) is Relation-like Function-like set
XX . c₁₄ is set
XX is Relation-like the carrier of I -defined Function-like non empty total set
WW is Element of S
F . WW is non-empty feasible MSAlgebra over I
Z . (F . WW) is Relation-like Function-like set
XX . c₁₄ is set
L is strict non-empty finitely-generated feasible MSSubAlgebra of E
L is strict non-empty finitely-generated feasible MSSubAlgebra of E
L is strict non-empty feasible MSSubAlgebra of E
SY is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of L
union { b₁ where b₁ is Element of bool ( the Sorts of E . c₁₄) : ex b₂ being Element of S ex b₃ being Relation-like the carrier of I -defined Function-like non empty total set st
( b₃ = Z . (F . b₂) & b₁ = b₃ . c₁₄ ) } is set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 y is finite set
c₁₄ is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of E
GenMSAlg c₁₄ is strict non-empty finitely-generated feasible MSSubAlgebra of E
s is Element of S
F . s is non-empty feasible MSAlgebra over I
ff is strict non-empty finitely-generated feasible MSSubAlgebra of E
Z . (F . s) is Relation-like Function-like set
y is strict non-empty feasible MSSubAlgebra of E
aa is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of y
the Sorts of y is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
WW is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of E
XX is set
WW . XX is set
c₁₄ . XX is finite set
the Sorts of E . XX is set
bool ( the Sorts of E . XX) is non empty set
{ b₁ where b₁ is Element of bool ( the Sorts of E . XX) : ex b₂ being Element of S ex b₃ being Relation-like the carrier of I -defined Function-like non empty total set st
( b₃ = Z . (F . b₂) & b₁ = b₃ . XX ) } is set
SY is set
union { b₁ where b₁ is Element of bool ( the Sorts of E . XX) : ex b₂ being Element of S ex b₃ being Relation-like the carrier of I -defined Function-like non empty total set st
( b₃ = Z . (F . b₂) & b₁ = b₃ . XX ) } is set
GenMSAlg aa is strict MSSubAlgebra of y
GenMSAlg WW is strict non-empty feasible MSSubAlgebra of E
I is non empty non void feasible ManySortedSign
S is non-empty feasible MSAlgebra over I
E is strict non-empty finitely-generated feasible MSSubAlgebra of S
F is strict non-empty finitely-generated feasible MSSubAlgebra of S
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() Function-yielding Relation-yielding FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
{0,1} is non empty finite set
s is set
s is Relation-like {0,1} -defined Function-like non empty total set
e is set
s . e is set
e is Relation-like {0,1} -defined Function-like non empty total MSAlgebra-Family of {0,1},I
i is Element of {0,1}
e . i is non-empty feasible MSAlgebra over I
i is strict non-empty finitely-generated feasible MSSubAlgebra of S
e . 0 is set
e . 1 is set
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
S is non-empty feasible MSAlgebra over I
MSSub S is non empty set
{ b₁ where b₁ is Element of MSSub S : ex b₂ being strict non-empty finitely-generated feasible MSSubAlgebra of S st b₂ = b₁ } is set
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
E is set
F is strict non-empty finitely-generated feasible MSSubAlgebra of S
the strict non-empty finitely-generated feasible MSSubAlgebra of S is strict non-empty finitely-generated feasible MSSubAlgebra of S
i is Relation-like E -defined Function-like total MSAlgebra-Family of E,I
product i is strict non-empty feasible MSAlgebra over I
SORTS i is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
OPS i is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((SORTS i) #), the ResultSort of I * (SORTS i)
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(SORTS i) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((SORTS i) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (SORTS i) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (SORTS i),(OPS i) #) is strict MSAlgebra over I
F is non empty set
A is Relation-like F -defined Function-like non empty total MSAlgebra-Family of F,I
product A is strict non-empty feasible MSAlgebra over I
SORTS A is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
OPS A is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((SORTS A) #), the ResultSort of I * (SORTS A)
(SORTS A) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((SORTS A) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I * (SORTS A) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (SORTS A),(OPS A) #) is strict MSAlgebra over I
Z is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of (product A) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
G is set
Z . G is set
the Sorts of (product A) . G is set
h is set
G is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of (product A)
h is Element of the carrier' of I
the_result_sort_of h is Element of the carrier of I
the ResultSort of I . h is Element of the carrier of I
the_arity_of h is Relation-like NAT -defined the carrier of I -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of I *
the Arity of I . h is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of I *
s is set
Den (h,(product A)) is Relation-like Args (h,(product A)) -defined Result (h,(product A)) -valued Function-like non empty total quasi_total Element of bool [:(Args (h,(product A))),(Result (h,(product A))):]
Args (h,(product A)) is functional non empty Element of proj2 ( the Sorts of (product A) #)
the Sorts of (product A) # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of (product A) #) is non empty set
the Arity of I * ( the Sorts of (product A) #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of (product A) #)) . h is set
Result (h,(product A)) is non empty Element of proj2 the Sorts of (product A)
proj2 the Sorts of (product A) is non empty V155() set
the ResultSort of I * the Sorts of (product A) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of (product A)) . h is non empty set
[:(Args (h,(product A))),(Result (h,(product A))):] is Relation-like non empty set
bool [:(Args (h,(product A))),(Result (h,(product A))):] is non empty set
the Charact of (product A) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of (product A) #), the ResultSort of I * the Sorts of (product A)
the Charact of (product A) . h is Relation-like Function-like set
G # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * (G #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * (G #)) . h is set
(Den (h,(product A))) | (( the Arity of I * (G #)) . h) is Relation-like ( the Arity of I * (G #)) . h -defined Args (h,(product A)) -defined Result (h,(product A)) -valued Function-like set
proj2 ((Den (h,(product A))) | (( the Arity of I * (G #)) . h)) is set
the ResultSort of I * G is Relation-like the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * G) . h is set
(Den (h,(product A))) | (( the Arity of I * (G #)) . h) is Relation-like Args (h,(product A)) -defined ( the Arity of I * (G #)) . h -defined Args (h,(product A)) -defined Result (h,(product A)) -valued Function-like Element of bool [:(Args (h,(product A))),(Result (h,(product A))):]
rng ((Den (h,(product A))) | (( the Arity of I * (G #)) . h)) is Element of bool (Result (h,(product A)))
bool (Result (h,(product A))) is non empty set
(SORTS A) . (the_result_sort_of h) is non empty set
dom ((Den (h,(product A))) | (( the Arity of I * (G #)) . h)) is Element of bool (( the Arity of I * (G #)) . h)
bool (( the Arity of I * (G #)) . h) is non empty set
y is set
((Den (h,(product A))) | (( the Arity of I * (G #)) . h)) . y is set
(Den (h,(product A))) . y is set
dom (Den (h,(product A))) is functional non empty Element of bool (Args (h,(product A)))
bool (Args (h,(product A))) is non empty set
ff is Relation-like Function-like Element of (SORTS A) . (the_result_sort_of h)
Args (h, the strict non-empty finitely-generated feasible MSSubAlgebra of S) is functional non empty Element of proj2 ( the Sorts of the strict non-empty finitely-generated feasible MSSubAlgebra of S #)
the Sorts of the strict non-empty finitely-generated feasible MSSubAlgebra of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of the strict non-empty finitely-generated feasible MSSubAlgebra of S # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of the strict non-empty finitely-generated feasible MSSubAlgebra of S #) is non empty set
the Arity of I * ( the Sorts of the strict non-empty finitely-generated feasible MSSubAlgebra of S #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of the strict non-empty finitely-generated feasible MSSubAlgebra of S #)) . h is set
ff . the strict non-empty finitely-generated feasible MSSubAlgebra of S is set
XX is strict non-empty finitely-generated feasible MSSubAlgebra of S
ff . XX is set
Args (h,XX) is functional non empty Element of proj2 ( the Sorts of XX #)
the Sorts of XX is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of XX # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of XX #) is non empty set
the Arity of I * ( the Sorts of XX #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of XX #)) . h is set
L is Element of F
A . L is non-empty feasible MSAlgebra over I
SY is Element of F
A . SY is non-empty feasible MSAlgebra over I
aa is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of Args (h,(product A))
const (h,(product A)) is Relation-like Function-like set
(const (h,(product A))) . L is set
const (h,(A . L)) is set
Den (h,(A . L)) is Relation-like Args (h,(A . L)) -defined Result (h,(A . L)) -valued Function-like non empty total quasi_total Element of bool [:(Args (h,(A . L))),(Result (h,(A . L))):]
Args (h,(A . L)) is functional non empty Element of proj2 ( the Sorts of (A . L) #)
the Sorts of (A . L) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of (A . L) # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of (A . L) #) is non empty set
the Arity of I * ( the Sorts of (A . L) #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of (A . L) #)) . h is set
Result (h,(A . L)) is non empty Element of proj2 the Sorts of (A . L)
proj2 the Sorts of (A . L) is non empty V155() set
the ResultSort of I * the Sorts of (A . L) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of (A . L)) . h is non empty set
[:(Args (h,(A . L))),(Result (h,(A . L))):] is Relation-like non empty set
bool [:(Args (h,(A . L))),(Result (h,(A . L))):] is non empty set
the Charact of (A . L) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of (A . L) #), the ResultSort of I * the Sorts of (A . L)
the Charact of (A . L) . h is Relation-like Function-like set
(Den (h,(A . L))) . {} is set
Den (h,S) is Relation-like Args (h,S) -defined Result (h,S) -valued Function-like non empty total quasi_total Element of bool [:(Args (h,S)),(Result (h,S)):]
Args (h,S) is functional non empty Element of proj2 ( the Sorts of S #)
the Sorts of S # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of S #) is non empty set
the Arity of I * ( the Sorts of S #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of S #)) . h is set
Result (h,S) is non empty Element of proj2 the Sorts of S
proj2 the Sorts of S is non empty V155() set
the ResultSort of I * the Sorts of S is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of S) . h is non empty set
[:(Args (h,S)),(Result (h,S)):] is Relation-like non empty set
bool [:(Args (h,S)),(Result (h,S)):] is non empty set
the Charact of S is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of S #), the ResultSort of I * the Sorts of S
the Charact of S . h is Relation-like Function-like set
(Den (h,S)) . {} is set
Den (h,(A . SY)) is Relation-like Args (h,(A . SY)) -defined Result (h,(A . SY)) -valued Function-like non empty total quasi_total Element of bool [:(Args (h,(A . SY))),(Result (h,(A . SY))):]
Args (h,(A . SY)) is functional non empty Element of proj2 ( the Sorts of (A . SY) #)
the Sorts of (A . SY) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of (A . SY) # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of (A . SY) #) is non empty set
the Arity of I * ( the Sorts of (A . SY) #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of (A . SY) #)) . h is set
Result (h,(A . SY)) is non empty Element of proj2 the Sorts of (A . SY)
proj2 the Sorts of (A . SY) is non empty V155() set
the ResultSort of I * the Sorts of (A . SY) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of (A . SY)) . h is non empty set
[:(Args (h,(A . SY))),(Result (h,(A . SY))):] is Relation-like non empty set
bool [:(Args (h,(A . SY))),(Result (h,(A . SY))):] is non empty set
the Charact of (A . SY) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of (A . SY) #), the ResultSort of I * the Sorts of (A . SY)
the Charact of (A . SY) . h is Relation-like Function-like set
(Den (h,(A . SY))) . {} is set
const (h,(A . SY)) is set
(const (h,(product A))) . SY is set
dom (the_arity_of h) is finite Element of bool NAT
aa is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of Args (h,(product A))
(G #) . ( the Arity of I . h) is set
(the_arity_of h) * G is Relation-like NAT -defined dom (the_arity_of h) -defined Function-like total finite set
product ((the_arity_of h) * G) is set
dom ((the_arity_of h) * G) is finite Element of bool NAT
dom aa is finite Element of bool NAT
WW is non empty finite set
XX is Element of WW
aa . XX is set
((the_arity_of h) * G) . XX is set
(the_arity_of h) . XX is set
G . ((the_arity_of h) . XX) is set
L is Element of the carrier of I
(SORTS A) . L is non empty set
SY is Relation-like Function-like Element of (SORTS A) . L
Y is strict non-empty finitely-generated feasible MSSubAlgebra of S
SY . Y is set
Y is Element of MSSub S
Y is strict non-empty finitely-generated feasible MSSubAlgebra of S
SY . Y is set
[:WW,(MSSub S):] is Relation-like non empty set
bool [:WW,(MSSub S):] is non empty set
XX is Relation-like WW -defined MSSub S -valued Function-like non empty total quasi_total finite Element of bool [:WW,(MSSub S):]
L is Relation-like WW -defined Function-like non empty total set
SY is set
L . SY is set
aa . SY is set
Y is Relation-like Function-like set
Y is strict non-empty finitely-generated feasible MSSubAlgebra of S
Y . Y is set
SY is Relation-like WW -defined Function-like non empty total MSAlgebra-Family of WW,I
Y is Element of WW
SY . Y is non-empty feasible MSAlgebra over I
aa . Y is set
Y is Relation-like Function-like set
Y is strict non-empty finitely-generated feasible MSSubAlgebra of S
Y . Y is set
Y is strict non-empty finitely-generated feasible MSSubAlgebra of S
ff . Y is set
Y is strict non-empty finitely-generated feasible MSSubAlgebra of S
ff . Y is set
{ ( the Sorts of (A . b₁) . b₂) where b₁ is Element of F, b₂ is Element of the carrier of I : verum } is set
union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of F, b₂ is Element of the carrier of I : verum } is set
Funcs (F,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of F, b₂ is Element of the carrier of I : verum } )) is functional set
Funcs ((dom (the_arity_of h)),(Funcs (F,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of F, b₂ is Element of the carrier of I : verum } )))) is functional set
commute aa is Relation-like Function-like Function-yielding Relation-yielding set
Y is Element of F
(commute aa) . Y is Relation-like Function-like set
proj1 ((commute aa) . Y) is set
Y is Element of F
(commute aa) . Y is Relation-like Function-like set
proj1 ((commute aa) . Y) is set
XX is set
((commute aa) . Y) . XX is set
((commute aa) . Y) . XX is set
aa . XX is set
SY . XX is set
h is Relation-like Function-like set
t is strict non-empty finitely-generated feasible MSSubAlgebra of S
h . t is set
h . Y is set
h . Y is set
A . Y is non-empty feasible MSAlgebra over I
Args (h,(A . Y)) is functional non empty Element of proj2 ( the Sorts of (A . Y) #)
the Sorts of (A . Y) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of (A . Y) # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of (A . Y) #) is non empty set
the Arity of I * ( the Sorts of (A . Y) #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of (A . Y) #)) . h is set
A . Y is non-empty feasible MSAlgebra over I
Args (h,(A . Y)) is functional non empty Element of proj2 ( the Sorts of (A . Y) #)
the Sorts of (A . Y) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of (A . Y) # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of (A . Y) #) is non empty set
the Arity of I * ( the Sorts of (A . Y) #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of (A . Y) #)) . h is set
Den (h,(A . Y)) is Relation-like Args (h,(A . Y)) -defined Result (h,(A . Y)) -valued Function-like non empty total quasi_total Element of bool [:(Args (h,(A . Y))),(Result (h,(A . Y))):]
Result (h,(A . Y)) is non empty Element of proj2 the Sorts of (A . Y)
proj2 the Sorts of (A . Y) is non empty V155() set
the ResultSort of I * the Sorts of (A . Y) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of (A . Y)) . h is non empty set
[:(Args (h,(A . Y))),(Result (h,(A . Y))):] is Relation-like non empty set
bool [:(Args (h,(A . Y))),(Result (h,(A . Y))):] is non empty set
the Charact of (A . Y) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of (A . Y) #), the ResultSort of I * the Sorts of (A . Y)
the Charact of (A . Y) . h is Relation-like Function-like set
(Den (h,(A . Y))) . ((commute aa) . Y) is set
Den (h,S) is Relation-like Args (h,S) -defined Result (h,S) -valued Function-like non empty total quasi_total Element of bool [:(Args (h,S)),(Result (h,S)):]
Args (h,S) is functional non empty Element of proj2 ( the Sorts of S #)
the Sorts of S # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of S #) is non empty set
the Arity of I * ( the Sorts of S #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of S #)) . h is set
Result (h,S) is non empty Element of proj2 the Sorts of S
proj2 the Sorts of S is non empty V155() set
the ResultSort of I * the Sorts of S is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of S) . h is non empty set
[:(Args (h,S)),(Result (h,S)):] is Relation-like non empty set
bool [:(Args (h,S)),(Result (h,S)):] is non empty set
the Charact of S is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of S #), the ResultSort of I * the Sorts of S
the Charact of S . h is Relation-like Function-like set
(Den (h,S)) . ((commute aa) . Y) is set
(Den (h,S)) . ((commute aa) . Y) is set
Den (h,(A . Y)) is Relation-like Args (h,(A . Y)) -defined Result (h,(A . Y)) -valued Function-like non empty total quasi_total Element of bool [:(Args (h,(A . Y))),(Result (h,(A . Y))):]
Result (h,(A . Y)) is non empty Element of proj2 the Sorts of (A . Y)
proj2 the Sorts of (A . Y) is non empty V155() set
the ResultSort of I * the Sorts of (A . Y) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of (A . Y)) . h is non empty set
[:(Args (h,(A . Y))),(Result (h,(A . Y))):] is Relation-like non empty set
bool [:(Args (h,(A . Y))),(Result (h,(A . Y))):] is non empty set
the Charact of (A . Y) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of (A . Y) #), the ResultSort of I * the Sorts of (A . Y)
the Charact of (A . Y) . h is Relation-like Function-like set
(Den (h,(A . Y))) . ((commute aa) . Y) is set
G . (the_result_sort_of h) is set
WW is Element of the carrier of I
(SORTS A) . WW is non empty set
XX is Relation-like Function-like Element of (SORTS A) . WW
L is strict non-empty finitely-generated feasible MSSubAlgebra of S
XX . L is set
(product A) | G is strict MSSubAlgebra of product A
Opers ((product A),G) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * (G #), the ResultSort of I * G
G # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * (G #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I * G is Relation-like the carrier' of I -defined Function-like non empty total set
MSAlgebra(# G,(Opers ((product A),G)) #) is strict MSAlgebra over I
h is set
G . h is set
(I,S, the strict non-empty finitely-generated feasible MSSubAlgebra of S) is non empty set
H is set
c₁₄ is set
s is strict non-empty feasible MSSubAlgebra of S
s is strict non-empty feasible MSSubAlgebra of S
the Sorts of the strict non-empty finitely-generated feasible MSSubAlgebra of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of the strict non-empty finitely-generated feasible MSSubAlgebra of S . h is set
c₁₄ is set
ff is set
y is Element of MSSub S
aa is strict non-empty finitely-generated feasible MSSubAlgebra of S
aa is strict non-empty finitely-generated feasible MSSubAlgebra of S
the Sorts of aa is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of aa . h is set
WW is set
ff is Relation-like F -defined Function-like non empty total set
H --> c₁₄ is Relation-like H -defined {c₁₄} -valued Function-like constant total quasi_total Element of bool [:H,{c₁₄}:]
{c₁₄} is non empty finite set
[:H,{c₁₄}:] is Relation-like set
bool [:H,{c₁₄}:] is non empty set
ff +* (H --> c₁₄) is Relation-like Function-like set
dom (H --> c₁₄) is Element of bool H
bool H is non empty set
s is Element of the carrier of I
Carrier (A,s) is Relation-like non-empty non empty-yielding F -defined Function-like non empty total set
dom (Carrier (A,s)) is non empty Element of bool F
bool F is non empty set
aa is set
(ff +* (H --> c₁₄)) . aa is set
(Carrier (A,s)) . aa is set
A . aa is set
ff . aa is set
WW is MSSubAlgebra of S
XX is set
the Sorts of WW is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of WW . h is set
(H --> c₁₄) . aa is set
L is strict MSSubAlgebra of S
the Sorts of L is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of L . h is set
SY is MSAlgebra over I
the Sorts of SY is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of SY . s is set
L is MSAlgebra over I
the Sorts of L is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of L . s is set
proj1 (ff +* (H --> c₁₄)) is set
dom ff is non empty Element of bool F
(dom ff) \/ (dom (H --> c₁₄)) is non empty set
F \/ (dom (H --> c₁₄)) is non empty set
F \/ H is non empty set
product (Carrier (A,s)) is set
(SORTS A) . s is non empty set
aa is Relation-like Function-like Element of (SORTS A) . s
aa . the strict non-empty finitely-generated feasible MSSubAlgebra of S is set
WW is strict non-empty finitely-generated feasible MSSubAlgebra of S
aa . WW is set
(H --> c₁₄) . the strict non-empty finitely-generated feasible MSSubAlgebra of S is set
(H --> c₁₄) . WW is set
aa is Element of the carrier of I
(SORTS A) . aa is non empty set
WW is Relation-like Function-like Element of (SORTS A) . aa
XX is strict non-empty finitely-generated feasible MSSubAlgebra of S
WW . XX is set
H is Element of the carrier of I
(SORTS A) . H is non empty set
Carrier (A,H) is Relation-like non-empty non empty-yielding F -defined Function-like non empty total set
dom (Carrier (A,H)) is non empty Element of bool F
bool F is non empty set
s is strict non-empty finitely-generated feasible MSSubAlgebra of S
A . s is set
(Carrier (A,H)) . s is set
ff is MSAlgebra over I
the Sorts of ff is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of ff . H is set
product (Carrier (A,H)) is set
c₁₄ is Relation-like Function-like Element of (SORTS A) . H
c₁₄ . s is set
the Sorts of S . H is non empty set
H is set
c₁₄ is set
h is strict non-empty feasible MSSubAlgebra of product i
the Sorts of h is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of h . H is set
s is Element of the carrier of I
(SORTS A) . s is non empty set
ff is Relation-like Function-like Element of (SORTS A) . s
y is strict non-empty finitely-generated feasible MSSubAlgebra of S
ff . y is set
aa is set
the Sorts of S . H is set
H is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of h, the Sorts of S
c₁₄ is Element of the carrier' of I
Args (c₁₄,h) is functional non empty Element of proj2 ( the Sorts of h #)
the Sorts of h # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of h #) is non empty set
the Arity of I * ( the Sorts of h #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of h #)) . c₁₄ is set
the_result_sort_of c₁₄ is Element of the carrier of I
the ResultSort of I . c₁₄ is Element of the carrier of I
H . (the_result_sort_of c₁₄) is Relation-like the Sorts of h . (the_result_sort_of c₁₄) -defined the Sorts of S . (the_result_sort_of c₁₄) -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of h . (the_result_sort_of c₁₄)),( the Sorts of S . (the_result_sort_of c₁₄)):]
the Sorts of h . (the_result_sort_of c₁₄) is non empty set
the Sorts of S . (the_result_sort_of c₁₄) is non empty set
[:( the Sorts of h . (the_result_sort_of c₁₄)),( the Sorts of S . (the_result_sort_of c₁₄)):] is Relation-like non empty set
bool [:( the Sorts of h . (the_result_sort_of c₁₄)),( the Sorts of S . (the_result_sort_of c₁₄)):] is non empty set
Den (c₁₄,h) is Relation-like Args (c₁₄,h) -defined Result (c₁₄,h) -valued Function-like non empty total quasi_total Element of bool [:(Args (c₁₄,h)),(Result (c₁₄,h)):]
Result (c₁₄,h) is non empty Element of proj2 the Sorts of h
proj2 the Sorts of h is non empty V155() set
the ResultSort of I * the Sorts of h is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of h) . c₁₄ is non empty set
[:(Args (c₁₄,h)),(Result (c₁₄,h)):] is Relation-like non empty set
bool [:(Args (c₁₄,h)),(Result (c₁₄,h)):] is non empty set
the Charact of h is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of h #), the ResultSort of I * the Sorts of h
the Charact of h . c₁₄ is Relation-like Function-like set
Den (c₁₄,S) is Relation-like Args (c₁₄,S) -defined Result (c₁₄,S) -valued Function-like non empty total quasi_total Element of bool [:(Args (c₁₄,S)),(Result (c₁₄,S)):]
Args (c₁₄,S) is functional non empty Element of proj2 ( the Sorts of S #)
the Sorts of S # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of S #) is non empty set
the Arity of I * ( the Sorts of S #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of S #)) . c₁₄ is set
Result (c₁₄,S) is non empty Element of proj2 the Sorts of S
proj2 the Sorts of S is non empty V155() set
the ResultSort of I * the Sorts of S is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of S) . c₁₄ is non empty set
[:(Args (c₁₄,S)),(Result (c₁₄,S)):] is Relation-like non empty set
bool [:(Args (c₁₄,S)),(Result (c₁₄,S)):] is non empty set
the Charact of S is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of S #), the ResultSort of I * the Sorts of S
the Charact of S . c₁₄ is Relation-like Function-like set
s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of Args (c₁₄,h)
(Den (c₁₄,h)) . s is set
(H . (the_result_sort_of c₁₄)) . ((Den (c₁₄,h)) . s) is set
H # s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of Args (c₁₄,S)
(Den (c₁₄,S)) . (H # s) is set
the_arity_of c₁₄ is Relation-like NAT -defined the carrier of I -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of I *
the Arity of I . c₁₄ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of I *
aa is Relation-like the Sorts of h . (the_result_sort_of c₁₄) -defined the Sorts of S . (the_result_sort_of c₁₄) -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of h . (the_result_sort_of c₁₄)),( the Sorts of S . (the_result_sort_of c₁₄)):]
(Den (c₁₄,h)) . s is Element of Result (c₁₄,h)
aa . ((Den (c₁₄,h)) . s) is set
WW is Element of the carrier of I
(SORTS A) . WW is non empty set
XX is Relation-like Function-like Element of (SORTS A) . WW
L is strict non-empty finitely-generated feasible MSSubAlgebra of S
XX . L is set
Den (c₁₄,(product A)) is Relation-like Args (c₁₄,(product A)) -defined Result (c₁₄,(product A)) -valued Function-like non empty total quasi_total Element of bool [:(Args (c₁₄,(product A))),(Result (c₁₄,(product A))):]
Args (c₁₄,(product A)) is functional non empty Element of proj2 ( the Sorts of (product A) #)
the Sorts of (product A) # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of (product A) #) is non empty set
the Arity of I * ( the Sorts of (product A) #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of (product A) #)) . c₁₄ is set
Result (c₁₄,(product A)) is non empty Element of proj2 the Sorts of (product A)
proj2 the Sorts of (product A) is non empty V155() set
the ResultSort of I * the Sorts of (product A) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of (product A)) . c₁₄ is non empty set
[:(Args (c₁₄,(product A))),(Result (c₁₄,(product A))):] is Relation-like non empty set
bool [:(Args (c₁₄,(product A))),(Result (c₁₄,(product A))):] is non empty set
the Charact of (product A) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of (product A) #), the ResultSort of I * the Sorts of (product A)
the Charact of (product A) . c₁₄ is Relation-like Function-like set
(Den (c₁₄,(product A))) . s is set
(Den (c₁₄,(product A))) . {} is set
const (c₁₄,(product A)) is Relation-like Function-like set
Args (c₁₄,L) is functional non empty Element of proj2 ( the Sorts of L #)
the Sorts of L is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of L # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of L #) is non empty set
the Arity of I * ( the Sorts of L #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of L #)) . c₁₄ is set
(H . (the_result_sort_of c₁₄)) . ((Den (c₁₄,h)) . s) is set
Y is Relation-like Function-like set
Y . L is set
SY is Element of F
(const (c₁₄,(product A))) . SY is set
A . SY is non-empty feasible MSAlgebra over I
const (c₁₄,(A . SY)) is set
Den (c₁₄,(A . SY)) is Relation-like Args (c₁₄,(A . SY)) -defined Result (c₁₄,(A . SY)) -valued Function-like non empty total quasi_total Element of bool [:(Args (c₁₄,(A . SY))),(Result (c₁₄,(A . SY))):]
Args (c₁₄,(A . SY)) is functional non empty Element of proj2 ( the Sorts of (A . SY) #)
the Sorts of (A . SY) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of (A . SY) # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of (A . SY) #) is non empty set
the Arity of I * ( the Sorts of (A . SY) #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of (A . SY) #)) . c₁₄ is set
Result (c₁₄,(A . SY)) is non empty Element of proj2 the Sorts of (A . SY)
proj2 the Sorts of (A . SY) is non empty V155() set
the ResultSort of I * the Sorts of (A . SY) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of (A . SY)) . c₁₄ is non empty set
[:(Args (c₁₄,(A . SY))),(Result (c₁₄,(A . SY))):] is Relation-like non empty set
bool [:(Args (c₁₄,(A . SY))),(Result (c₁₄,(A . SY))):] is non empty set
the Charact of (A . SY) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of (A . SY) #), the ResultSort of I * the Sorts of (A . SY)
the Charact of (A . SY) . c₁₄ is Relation-like Function-like set
(Den (c₁₄,(A . SY))) . {} is set
Den (c₁₄,L) is Relation-like Args (c₁₄,L) -defined Result (c₁₄,L) -valued Function-like non empty total quasi_total Element of bool [:(Args (c₁₄,L)),(Result (c₁₄,L)):]
Result (c₁₄,L) is non empty Element of proj2 the Sorts of L
proj2 the Sorts of L is non empty V155() set
the ResultSort of I * the Sorts of L is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of L) . c₁₄ is non empty set
[:(Args (c₁₄,L)),(Result (c₁₄,L)):] is Relation-like non empty set
bool [:(Args (c₁₄,L)),(Result (c₁₄,L)):] is non empty set
the Charact of L is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of L #), the ResultSort of I * the Sorts of L
the Charact of L . c₁₄ is Relation-like Function-like set
(Den (c₁₄,L)) . {} is set
(Den (c₁₄,S)) . {} is set
(Den (c₁₄,S)) . (H # s) is Element of Result (c₁₄,S)
dom (the_arity_of c₁₄) is finite Element of bool NAT
SY is non empty finite set
Y is Element of SY
s . Y is set
(the_arity_of c₁₄) . Y is set
H . ((the_arity_of c₁₄) . Y) is Relation-like Function-like set
the Sorts of h . ((the_arity_of c₁₄) . Y) is set
the Sorts of S . ((the_arity_of c₁₄) . Y) is set
[:( the Sorts of h . ((the_arity_of c₁₄) . Y)),( the Sorts of S . ((the_arity_of c₁₄) . Y)):] is Relation-like set
bool [:( the Sorts of h . ((the_arity_of c₁₄) . Y)),( the Sorts of S . ((the_arity_of c₁₄) . Y)):] is non empty set
Y is Relation-like the Sorts of h . ((the_arity_of c₁₄) . Y) -defined the Sorts of S . ((the_arity_of c₁₄) . Y) -valued Function-like quasi_total Element of bool [:( the Sorts of h . ((the_arity_of c₁₄) . Y)),( the Sorts of S . ((the_arity_of c₁₄) . Y)):]
(the_arity_of c₁₄) /. Y is Element of the carrier of I
the Sorts of h . ((the_arity_of c₁₄) /. Y) is non empty set
Y . (s . Y) is set
Y is Element of the carrier of I
(SORTS A) . Y is non empty set
Y is Relation-like Function-like Element of (SORTS A) . Y
XX is strict non-empty finitely-generated feasible MSSubAlgebra of S
Y . XX is set
h is Element of MSSub S
(H . ((the_arity_of c₁₄) . Y)) . Y is set
t is strict non-empty finitely-generated feasible MSSubAlgebra of S
Y . t is set
[:SY,(MSSub S):] is Relation-like non empty set
bool [:SY,(MSSub S):] is non empty set
Y is Relation-like SY -defined MSSub S -valued Function-like non empty total quasi_total finite Element of bool [:SY,(MSSub S):]
Y is Relation-like SY -defined Function-like non empty total set
Y is set
Y . Y is set
s . Y is set
(the_arity_of c₁₄) . Y is set
H . ((the_arity_of c₁₄) . Y) is Relation-like Function-like set
Y is Relation-like Function-like set
XX is strict non-empty finitely-generated feasible MSSubAlgebra of S
Y . XX is set
(H . ((the_arity_of c₁₄) . Y)) . Y is set
Y is Relation-like SY -defined Function-like non empty total MSAlgebra-Family of SY,I
Y is Element of SY
Y . Y is non-empty feasible MSAlgebra over I
s . Y is set
(the_arity_of c₁₄) . Y is set
H . ((the_arity_of c₁₄) . Y) is Relation-like Function-like set
XX is Relation-like Function-like set
h is strict non-empty finitely-generated feasible MSSubAlgebra of S
XX . h is set
(H . ((the_arity_of c₁₄) . Y)) . XX is set
Y is strict non-empty finitely-generated feasible MSSubAlgebra of S
XX is strict non-empty finitely-generated feasible MSSubAlgebra of S
Args (c₁₄,(product A)) is functional non empty Element of proj2 ( the Sorts of (product A) #)
the Sorts of (product A) # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of (product A) #) is non empty set
the Arity of I * ( the Sorts of (product A) #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of (product A) #)) . c₁₄ is set
commute s is Relation-like Function-like Function-yielding Relation-yielding set
h is Element of F
(commute s) . h is Relation-like Function-like set
A . h is non-empty feasible MSAlgebra over I
Args (c₁₄,(A . h)) is functional non empty Element of proj2 ( the Sorts of (A . h) #)
the Sorts of (A . h) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of (A . h) # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of (A . h) #) is non empty set
the Arity of I * ( the Sorts of (A . h) #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of (A . h) #)) . c₁₄ is set
Args (c₁₄,XX) is functional non empty Element of proj2 ( the Sorts of XX #)
the Sorts of XX is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of XX # is Relation-like the carrier of I * -defined Function-like non empty total set
proj2 ( the Sorts of XX #) is non empty set
the Arity of I * ( the Sorts of XX #) is Relation-like the carrier' of I -defined Function-like non empty total set
( the Arity of I * ( the Sorts of XX #)) . c₁₄ is set
{ ( the Sorts of (A . b₁) . b₂) where b₁ is Element of F, b₂ is Element of the carrier of I : verum } is set
union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of F, b₂ is Element of the carrier of I : verum } is set
Funcs (F,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of F, b₂ is Element of the carrier of I : verum } )) is functional set
Funcs ((dom (the_arity_of c₁₄)),(Funcs (F,(union { ( the Sorts of (A . b₁) . b₂) where b₁ is Element of F, b₂ is Element of the carrier of I : verum } )))) is functional set
proj1 ((commute s) . h) is set
A is set
(H # s) . A is set
((commute s) . h) . A is set
(the_arity_of c₁₄) . A is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of Args (c₁₄,XX)
len f is V21() V22() V23() V27() Element of NAT
Seg (len f) is finite V35( len f) Element of bool NAT
s . A is set
MAX is Element of the carrier of I
H . MAX is Relation-like the Sorts of h . MAX -defined the Sorts of S . MAX -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of h . MAX),( the Sorts of S . MAX):]
the Sorts of h . MAX is non empty set
the Sorts of S . MAX is non empty set
[:( the Sorts of h . MAX),( the Sorts of S . MAX):] is Relation-like non empty set
bool [:( the Sorts of h . MAX),( the Sorts of S . MAX):] is non empty set
Y . A is set
kn is Relation-like Function-like set
Ki is strict non-empty finitely-generated feasible MSSubAlgebra of S
kn . Ki is set
(H . MAX) . kn is set
dom s is finite Element of bool NAT
n9 is V21() V22() V23() V27() set
(the_arity_of c₁₄) /. n9 is Element of the carrier of I
H . ((the_arity_of c₁₄) /. n9) is Relation-like the Sorts of h . ((the_arity_of c₁₄) /. n9) -defined the Sorts of S . ((the_arity_of c₁₄) /. n9) -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of h . ((the_arity_of c₁₄) /. n9)),( the Sorts of S . ((the_arity_of c₁₄) /. n9)):]
the Sorts of h . ((the_arity_of c₁₄) /. n9) is non empty set
the Sorts of S . ((the_arity_of c₁₄) /. n9) is non empty set
[:( the Sorts of h . ((the_arity_of c₁₄) /. n9)),( the Sorts of S . ((the_arity_of c₁₄) /. n9)):] is Relation-like non empty set
bool [:( the Sorts of h . ((the_arity_of c₁₄) /. n9)),( the Sorts of S . ((the_arity_of c₁₄) /. n9)):] is non empty set
(H . ((the_arity_of c₁₄) /. n9)) . (s . A) is set
kn . (Y . A) is set
kn . h is set
Den (c₁₄,(product A)) is Relation-like Args (c₁₄,(product A)) -defined Result (c₁₄,(product A)) -valued Function-like non empty total quasi_total Element of bool [:(Args (c₁₄,(product A))),(Result (c₁₄,(product A))):]
Result (c₁₄,(product A)) is non empty Element of proj2 the Sorts of (product A)
proj2 the Sorts of (product A) is non empty V155() set
the ResultSort of I * the Sorts of (product A) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of (product A)) . c₁₄ is non empty set
[:(Args (c₁₄,(product A))),(Result (c₁₄,(product A))):] is Relation-like non empty set
bool [:(Args (c₁₄,(product A))),(Result (c₁₄,(product A))):] is non empty set
the Charact of (product A) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of (product A) #), the ResultSort of I * the Sorts of (product A)
the Charact of (product A) . c₁₄ is Relation-like Function-like set
(Den (c₁₄,(product A))) . s is set
dom (H # s) is finite Element of bool NAT
(H . (the_result_sort_of c₁₄)) . ((Den (c₁₄,h)) . s) is set
XX . XX is set
t is Relation-like Function-like set
t . XX is set
Den (c₁₄,(A . h)) is Relation-like Args (c₁₄,(A . h)) -defined Result (c₁₄,(A . h)) -valued Function-like non empty total quasi_total Element of bool [:(Args (c₁₄,(A . h))),(Result (c₁₄,(A . h))):]
Result (c₁₄,(A . h)) is non empty Element of proj2 the Sorts of (A . h)
proj2 the Sorts of (A . h) is non empty V155() set
the ResultSort of I * the Sorts of (A . h) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of (A . h)) . c₁₄ is non empty set
[:(Args (c₁₄,(A . h))),(Result (c₁₄,(A . h))):] is Relation-like non empty set
bool [:(Args (c₁₄,(A . h))),(Result (c₁₄,(A . h))):] is non empty set
the Charact of (A . h) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of (A . h) #), the ResultSort of I * the Sorts of (A . h)
the Charact of (A . h) . c₁₄ is Relation-like Function-like set
(Den (c₁₄,(A . h))) . ((commute s) . h) is set
Den (c₁₄,XX) is Relation-like Args (c₁₄,XX) -defined Result (c₁₄,XX) -valued Function-like non empty total quasi_total Element of bool [:(Args (c₁₄,XX)),(Result (c₁₄,XX)):]
Result (c₁₄,XX) is non empty Element of proj2 the Sorts of XX
proj2 the Sorts of XX is non empty V155() set
the ResultSort of I * the Sorts of XX is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
( the ResultSort of I * the Sorts of XX) . c₁₄ is non empty set
[:(Args (c₁₄,XX)),(Result (c₁₄,XX)):] is Relation-like non empty set
bool [:(Args (c₁₄,XX)),(Result (c₁₄,XX)):] is non empty set
the Charact of XX is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ( the Sorts of XX #), the ResultSort of I * the Sorts of XX
the Charact of XX . c₁₄ is Relation-like Function-like set
(Den (c₁₄,XX)) . ((commute s) . h) is set
(Den (c₁₄,S)) . ((commute s) . h) is set
(Den (c₁₄,S)) . (H # s) is Element of Result (c₁₄,S)
c₁₄ is set
H . c₁₄ is Relation-like Function-like set
proj2 (H . c₁₄) is set
the Sorts of S . c₁₄ is set
s is Element of the carrier of I
the Sorts of h . s is non empty set
ff is set
the Sorts of S . s is non empty set
H . s is Relation-like the Sorts of h . s -defined the Sorts of S . s -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of h . s),( the Sorts of S . s):]
[:( the Sorts of h . s),( the Sorts of S . s):] is Relation-like non empty set
bool [:( the Sorts of h . s),( the Sorts of S . s):] is non empty set
rng (H . s) is non empty Element of bool ( the Sorts of S . s)
bool ( the Sorts of S . s) is non empty set
y is set
(SORTS A) . s is non empty set
Carrier (A,s) is Relation-like non-empty non empty-yielding F -defined Function-like non empty total set
product (Carrier (A,s)) is set
dom (Carrier (A,s)) is non empty Element of bool F
aa is Relation-like Function-like set
proj1 aa is set
WW is set
WW --> y is Relation-like WW -defined {y} -valued Function-like constant total quasi_total Element of bool [:WW,{y}:]
{y} is non empty finite set
[:WW,{y}:] is Relation-like set
bool [:WW,{y}:] is non empty set
aa +* (WW --> y) is Relation-like Function-like set
dom (WW --> y) is Element of bool WW
bool WW is non empty set
L is Element of F
(aa +* (WW --> y)) . L is set
SY is MSSubAlgebra of S
the Sorts of SY is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of SY . s is set
(WW --> y) . L is set
L is set
(aa +* (WW --> y)) . L is set
(Carrier (A,s)) . L is set
SY is Element of MSSub S
Y is strict non-empty finitely-generated feasible MSSubAlgebra of S
Y is strict non-empty finitely-generated feasible MSSubAlgebra of S
A . Y is set
(Carrier (A,s)) . Y is set
Y is MSSubAlgebra of S
the Sorts of Y is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of Y . s is set
Y is MSAlgebra over I
the Sorts of Y is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of Y . s is set
aa . L is set
Y is MSSubAlgebra of S
the Sorts of Y is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of Y . s is set
L is set
the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S
dom (H . s) is non empty Element of bool ( the Sorts of h . s)
bool ( the Sorts of h . s) is non empty set
{s} is non empty finite set
{s} --> {y} is Relation-like non-empty non empty-yielding {s} -defined {{y}} -valued Function-like constant non empty total quasi_total finite Element of bool [:{s},{{y}}:]
{{y}} is non empty finite V32() set
[:{s},{{y}}:] is Relation-like non empty finite set
bool [:{s},{{y}}:] is non empty finite V32() set
the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S +* ({s} --> {y}) is Relation-like Function-like set
proj1 ( the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S +* ({s} --> {y})) is set
dom the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S is non empty Element of bool the carrier of I
bool the carrier of I is non empty set
dom ({s} --> {y}) is non empty finite Element of bool {s}
bool {s} is non empty finite V32() set
(dom the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S) \/ (dom ({s} --> {y})) is non empty set
the carrier of I \/ (dom ({s} --> {y})) is non empty set
the carrier of I \/ {s} is non empty set
Y is Relation-like the carrier of I -defined Function-like non empty total set
Y . s is set
({s} --> {y}) . s is set
Y is set
Y . Y is set
the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S . Y is finite set
Y is set
Y . Y is set
the Sorts of S . Y is set
Y is set
the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S . Y is finite set
Y is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of S
Y is set
Y . Y is set
the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S . Y is finite set
Y is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of S
Y is set
Y . Y is set
the Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S . Y is finite set
Y is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total finite-yielding ManySortedSubset of the Sorts of S
GenMSAlg Y is strict non-empty finitely-generated feasible MSSubAlgebra of S
the Sorts of (GenMSAlg Y) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
Y . s is non empty finite set
the Sorts of (GenMSAlg Y) . s is non empty set
proj1 (aa +* (WW --> y)) is set
(proj1 aa) \/ (dom (WW --> y)) is set
F \/ (dom (WW --> y)) is non empty set
F \/ WW is non empty set
h is Relation-like the Sorts of h . s -defined the Sorts of S . s -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of h . s),( the Sorts of S . s):]
XX is Relation-like Function-like Element of (SORTS A) . s
t is strict non-empty finitely-generated feasible MSSubAlgebra of S
XX . t is set
f is strict non-empty finitely-generated feasible MSSubAlgebra of S
XX . f is set
the Sorts of t is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of f is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of t . s is non empty set
the Sorts of f . s is non empty set
G . s is set
t is Element of the carrier of I
(SORTS A) . t is non empty set
f is Relation-like Function-like Element of (SORTS A) . t
A is strict non-empty finitely-generated feasible MSSubAlgebra of S
f . A is set
h . XX is set
t is Element of the carrier of I
(SORTS A) . t is non empty set
f is Relation-like Function-like Element of (SORTS A) . t
A is strict non-empty finitely-generated feasible MSSubAlgebra of S
f . A is set
t is Element of the carrier of I
f is Relation-like Function-like Element of (SORTS A) . s
A is strict non-empty finitely-generated feasible MSSubAlgebra of S
f . A is set
MAX is strict non-empty finitely-generated feasible MSSubAlgebra of S
the Sorts of MAX is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of MAX . s is non empty set
XX . MAX is set
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
S is free feasible MSAlgebra over I
the Sorts of S is Relation-like the carrier of I -defined Function-like non empty total set
E is Relation-like the carrier of I -defined Function-like non empty total free GeneratorSet of S
F is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of S
GenMSAlg F is strict MSSubAlgebra of S
the Sorts of (GenMSAlg F) is Relation-like the carrier of I -defined Function-like non empty total set
s is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of (GenMSAlg F)
GenMSAlg s is strict MSSubAlgebra of GenMSAlg F
the Sorts of (GenMSAlg s) is Relation-like the carrier of I -defined Function-like non empty total set
e is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of GenMSAlg F
A is non-empty feasible MSAlgebra over I
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
Z is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of e, the Sorts of A
i is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of E
G is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of E, the Sorts of A
G || i is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of i, the Sorts of A
h is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of S, the Sorts of A
h || E is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of E, the Sorts of A
A is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of S
h || A is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of A, the Sorts of A
H is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (GenMSAlg F), the Sorts of A
H || e is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of e, the Sorts of A
h || F is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of F, the Sorts of A
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
I is non empty non void feasible ManySortedSign
(I) is MSAlgebra over I
the carrier of I is non empty set
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
I is non empty non void feasible ManySortedSign
(I) is Relation-like the carrier of I -defined Function-like non empty total set
the carrier of I is non empty set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
S is Element of the carrier of I
the Sorts of (I) . S is non empty set
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
S is Element of the carrier of I
the Sorts of (I) . S is non empty set
E is Element of the Sorts of (I) . S
F is Element of the Sorts of (I) . S
[E,F] is V15() set
{E,F} is non empty finite set
{E} is non empty finite set
{{E,F},{E}} is non empty finite V32() set
(I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
(I) . S is non empty set
[:( the Sorts of (I) . S),( the Sorts of (I) . S):] is Relation-like non empty set
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
S is Element of the carrier of I
(I) . S is non empty set
the Sorts of (I) . S is non empty set
E is Element of (I) . S
E `1 is set
[:( the Sorts of (I) . S),( the Sorts of (I) . S):] is Relation-like non empty set
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
S is Element of the carrier of I
(I) . S is non empty set
the Sorts of (I) . S is non empty set
E is Element of (I) . S
E `2 is set
[:( the Sorts of (I) . S),( the Sorts of (I) . S):] is Relation-like non empty set
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
E is Element of the carrier of I
(I) . E is non empty set
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
S is non-empty feasible MSAlgebra over I
E is Element of the carrier of I
(I) . E is non empty set
F is Element of (I) . E
s is strict non-empty feasible MSSubAlgebra of S
the Sorts of s is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
e is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (I), the Sorts of s
e . E is Relation-like the Sorts of (I) . E -defined the Sorts of s . E -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (I) . E),( the Sorts of s . E):]
the Sorts of (I) . E is non empty set
the Sorts of s . E is non empty set
[:( the Sorts of (I) . E),( the Sorts of s . E):] is Relation-like non empty set
bool [:( the Sorts of (I) . E),( the Sorts of s . E):] is non empty set
F `1 is set
(e . E) . (F `1) is set
F `2 is set
(e . E) . (F `2) is set
i is set
the Sorts of s . i is set
the Sorts of (I) . i is set
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
i is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (I), the Sorts of S
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
S is non-empty feasible MSAlgebra over I
E is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of (I)
F is strict non-empty feasible MSSubAlgebra of S
s is Element of the carrier of I
(I) . s is non empty set
E . s is set
e is Element of (I) . s
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
S is non-empty feasible MSAlgebra over I
E is non-empty feasible MSAlgebra over I
F is Element of the carrier of I
(I) . F is non empty set
s is Element of (I) . F
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of E is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
e is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of S, the Sorts of E
e "" is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of E, the Sorts of S
i is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of E, the Sorts of S
i . F is Relation-like the Sorts of E . F -defined the Sorts of S . F -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of E . F),( the Sorts of S . F):]
the Sorts of E . F is non empty set
the Sorts of S . F is non empty set
[:( the Sorts of E . F),( the Sorts of S . F):] is Relation-like non empty set
bool [:( the Sorts of E . F),( the Sorts of S . F):] is non empty set
e . F is Relation-like the Sorts of S . F -defined the Sorts of E . F -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of S . F),( the Sorts of E . F):]
[:( the Sorts of S . F),( the Sorts of E . F):] is Relation-like non empty set
bool [:( the Sorts of S . F),( the Sorts of E . F):] is non empty set
(e . F) " is Relation-like Function-like set
rng (e . F) is non empty Element of bool ( the Sorts of E . F)
bool ( the Sorts of E . F) is non empty set
A is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (I), the Sorts of E
A . F is Relation-like the Sorts of (I) . F -defined the Sorts of E . F -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (I) . F),( the Sorts of E . F):]
the Sorts of (I) . F is non empty set
[:( the Sorts of (I) . F),( the Sorts of E . F):] is Relation-like non empty set
bool [:( the Sorts of (I) . F),( the Sorts of E . F):] is non empty set
s `1 is set
(A . F) . (s `1) is set
s `2 is set
(A . F) . (s `2) is set
i ** A is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (I), the Sorts of S
(i ** A) . F is Relation-like the Sorts of (I) . F -defined the Sorts of S . F -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (I) . F),( the Sorts of S . F):]
[:( the Sorts of (I) . F),( the Sorts of S . F):] is Relation-like non empty set
bool [:( the Sorts of (I) . F),( the Sorts of S . F):] is non empty set
(i . F) * (A . F) is Relation-like the Sorts of (I) . F -defined the Sorts of S . F -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (I) . F),( the Sorts of S . F):]
(e . F) * ((i ** A) . F) is Relation-like the Sorts of (I) . F -defined the Sorts of E . F -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (I) . F),( the Sorts of E . F):]
(e . F) * (i . F) is Relation-like the Sorts of E . F -defined the Sorts of E . F -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of E . F),( the Sorts of E . F):]
[:( the Sorts of E . F),( the Sorts of E . F):] is Relation-like non empty set
bool [:( the Sorts of E . F),( the Sorts of E . F):] is non empty set
((e . F) * (i . F)) * (A . F) is Relation-like the Sorts of (I) . F -defined the Sorts of E . F -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (I) . F),( the Sorts of E . F):]
id ( the Sorts of E . F) is Relation-like the Sorts of E . F -defined the Sorts of E . F -valued Function-like one-to-one non empty total quasi_total Element of bool [:( the Sorts of E . F),( the Sorts of E . F):]
(id ( the Sorts of E . F)) * (A . F) is Relation-like the Sorts of (I) . F -defined the Sorts of E . F -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (I) . F),( the Sorts of E . F):]
dom ((i ** A) . F) is non empty Element of bool ( the Sorts of (I) . F)
bool ( the Sorts of (I) . F) is non empty set
((i ** A) . F) . (s `1) is set
(e . F) . (((i ** A) . F) . (s `1)) is set
((i ** A) . F) . (s `2) is set
(e . F) . (((i ** A) . F) . (s `2)) is set
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
S is non-empty feasible MSAlgebra over I
E is non-empty feasible MSAlgebra over I
F is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of (I)
s is Element of the carrier of I
(I) . s is non empty set
F . s is set
e is Element of (I) . s
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
S is non-empty feasible MSAlgebra over I
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
E is Element of the carrier of I
(I) . E is non empty set
F is Element of (I) . E
s is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total Relation-yielding MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of S, the Sorts of S
QuotMSAlg (S,s) is strict non-empty feasible MSAlgebra over I
the Sorts of (QuotMSAlg (S,s)) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
MSNat_Hom (S,s) is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of S, the Sorts of (QuotMSAlg (S,s))
(MSNat_Hom (S,s)) . E is Relation-like the Sorts of S . E -defined the Sorts of (QuotMSAlg (S,s)) . E -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of S . E),( the Sorts of (QuotMSAlg (S,s)) . E):]
the Sorts of S . E is non empty set
the Sorts of (QuotMSAlg (S,s)) . E is non empty set
[:( the Sorts of S . E),( the Sorts of (QuotMSAlg (S,s)) . E):] is Relation-like non empty set
bool [:( the Sorts of S . E),( the Sorts of (QuotMSAlg (S,s)) . E):] is non empty set
i is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (I), the Sorts of (QuotMSAlg (S,s))
i . E is Relation-like the Sorts of (I) . E -defined the Sorts of (QuotMSAlg (S,s)) . E -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (I) . E),( the Sorts of (QuotMSAlg (S,s)) . E):]
the Sorts of (I) . E is non empty set
[:( the Sorts of (I) . E),( the Sorts of (QuotMSAlg (S,s)) . E):] is Relation-like non empty set
bool [:( the Sorts of (I) . E),( the Sorts of (QuotMSAlg (S,s)) . E):] is non empty set
F `1 is set
(i . E) . (F `1) is set
F `2 is set
(i . E) . (F `2) is set
A is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (I), the Sorts of S
(MSNat_Hom (S,s)) ** A is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (I), the Sorts of (QuotMSAlg (S,s))
A . E is Relation-like the Sorts of (I) . E -defined the Sorts of S . E -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (I) . E),( the Sorts of S . E):]
[:( the Sorts of (I) . E),( the Sorts of S . E):] is Relation-like non empty set
bool [:( the Sorts of (I) . E),( the Sorts of S . E):] is non empty set
dom (A . E) is non empty Element of bool ( the Sorts of (I) . E)
bool ( the Sorts of (I) . E) is non empty set
((MSNat_Hom (S,s)) . E) * (A . E) is Relation-like the Sorts of (I) . E -defined the Sorts of (QuotMSAlg (S,s)) . E -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (I) . E),( the Sorts of (QuotMSAlg (S,s)) . E):]
(((MSNat_Hom (S,s)) . E) * (A . E)) . (F `1) is set
(A . E) . (F `1) is set
((MSNat_Hom (S,s)) . E) . ((A . E) . (F `1)) is set
(A . E) . (F `2) is set
((MSNat_Hom (S,s)) . E) . ((A . E) . (F `2)) is set
(((MSNat_Hom (S,s)) . E) * (A . E)) . (F `2) is set
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
S is non-empty feasible MSAlgebra over I
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
E is Relation-like the carrier of I -defined Function-like non empty total ManySortedSubset of (I)
F is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total Relation-yielding MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of S, the Sorts of S
QuotMSAlg (S,F) is strict non-empty feasible MSAlgebra over I
s is Element of the carrier of I
(I) . s is non empty set
E . s is set
e is Element of (I) . s
I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
(I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
(I) is strict non-empty free feasible MSAlgebra over I
the carrier of I --> NAT is Relation-like non-empty non empty-yielding the carrier of I -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of I,(bool REAL):]
[: the carrier of I,(bool REAL):] is Relation-like non empty set
bool [: the carrier of I,(bool REAL):] is non empty set
FreeMSA ( the carrier of I --> NAT) is strict non-empty free feasible MSAlgebra over I
FreeSort ( the carrier of I --> NAT) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
FreeOper ( the carrier of I --> NAT) is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #), the ResultSort of I * (FreeSort ( the carrier of I --> NAT))
the carrier' of I is non empty set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty FinSequence-membered M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like non empty set
bool [: the carrier' of I,( the carrier of I *):] is non empty set
(FreeSort ( the carrier of I --> NAT)) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((FreeSort ( the carrier of I --> NAT)) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like non empty total quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like non empty set
bool [: the carrier' of I, the carrier of I:] is non empty set
the ResultSort of I * (FreeSort ( the carrier of I --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of I --> NAT)),(FreeOper ( the carrier of I --> NAT)) #) is strict MSAlgebra over I
the Sorts of (I) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of (I), the Sorts of (I)|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
S is Element of the carrier of I
(I) . S is non empty set
E is Element of (I) . S
the Sorts of (I) . S is non empty set
E `2 is set
E `1 is set
e is non empty set
i is Relation-like e -defined Function-like non empty total MSAlgebra-Family of e,I
product i is strict non-empty feasible MSAlgebra over I
SORTS i is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
OPS i is Relation-like the carrier' of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of I * ((SORTS i) #), the ResultSort of I * (SORTS i)
(SORTS i) # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of I * ((SORTS i) #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I * (SORTS i) is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (SORTS i),(OPS i) #) is strict MSAlgebra over I
the Sorts of (product i) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
A is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (I), the Sorts of (product i)
A . S is Relation-like the Sorts of (I) . S -defined the Sorts of (product i) . S -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (I) . S),( the Sorts of (product i) . S):]
the Sorts of (product i) . S is non empty set
[:( the Sorts of (I) . S),( the Sorts of (product i) . S):] is Relation-like non empty set
bool [:( the Sorts of (I) . S),( the Sorts of (product i) . S):] is non empty set
(A . S) . (E `1) is set
(A . S) . (E `2) is set
dom (A . S) is non empty Element of bool ( the Sorts of (I) . S)
bool ( the Sorts of (I) . S) is non empty set
A is Element of e
i . A is non-empty feasible MSAlgebra over I
the Sorts of (i . A) is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
proj (i,A) is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (product i), the Sorts of (i . A)
(proj (i,A)) ** A is Relation-like the carrier of I -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (I), the Sorts of (i . A)
Carrier (i,S) is Relation-like non-empty non empty-yielding e -defined Function-like non empty total set
proj ((Carrier (i,S)),A) is Relation-like Function-like set
s is Element of the Sorts of (I) . S
(A . S) . s is Element of the Sorts of (product i) . S
(proj ((Carrier (i,S)),A)) . ((A . S) . s) is set
the Sorts of (i . A) . S is non empty set
(proj (i,A)) . S is Relation-like the Sorts of (product i) . S -defined the Sorts of (i . A) . S -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (product i) . S),( the Sorts of (i . A) . S):]
[:( the Sorts of (product i) . S),( the Sorts of (i . A) . S):] is Relation-like non empty set
bool [:( the Sorts of (product i) . S),( the Sorts of (i . A) . S):] is non empty set
((proj (i,A)) . S) . ((A . S) . s) is Element of the Sorts of (i . A) . S
((proj (i,A)) . S) * (A . S) is Relation-like the Sorts of (I) . S -defined the Sorts of (i . A) . S -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (I) . S),( the Sorts of (i . A) . S):]
[:( the Sorts of (I) . S),( the Sorts of (i . A) . S):] is Relation-like non empty set
bool [:( the Sorts of (I) . S),( the Sorts of (i . A) . S):] is non empty set
(((proj (i,A)) . S) * (A . S)) . s is Element of the Sorts of (i . A) . S
((proj (i,A)) ** A) . S is Relation-like the Sorts of (I) . S -defined the Sorts of (i . A) . S -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (I) . S),( the Sorts of (i . A) . S):]
(((proj (i,A)) ** A) . S) . s is Element of the Sorts of (i . A) . S
F is Element of the Sorts of (I) . S
(((proj (i,A)) ** A) . S) . F is Element of the Sorts of (i . A) . S
(((proj (i,A)) . S) * (A . S)) . F is Element of the Sorts of (i . A) . S
(A . S) . F is Element of the Sorts of (product i) . S
((proj (i,A)) . S) . ((A . S) . F) is Element of the Sorts of (i . A) . S
(proj ((Carrier (i,S)),A)) . ((A . S) . F) is set
product (Carrier (i,S)) is set
I is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
(S) is strict non-empty free feasible MSAlgebra over S
the carrier of S --> NAT is Relation-like non-empty non empty-yielding the carrier of S -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of S,(bool REAL):]
[: the carrier of S,(bool REAL):] is Relation-like non empty set
bool [: the carrier of S,(bool REAL):] is non empty set
FreeMSA ( the carrier of S --> NAT) is strict non-empty free feasible MSAlgebra over S
FreeSort ( the carrier of S --> NAT) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
FreeOper ( the carrier of S --> NAT) is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((FreeSort ( the carrier of S --> NAT)) #), the ResultSort of S * (FreeSort ( the carrier of S --> NAT))
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is Relation-like non empty set
bool [: the carrier' of S,( the carrier of S *):] is non empty set
(FreeSort ( the carrier of S --> NAT)) # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ((FreeSort ( the carrier of S --> NAT)) #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like non empty set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * (FreeSort ( the carrier of S --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of S --> NAT)),(FreeOper ( the carrier of S --> NAT)) #) is strict MSAlgebra over S
the Sorts of (S) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
[| the Sorts of (S), the Sorts of (S)|] is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
E is Element of the carrier of S
(S) . E is non empty set
F is Element of (S) . E
s is Relation-like I -defined Function-like total MSAlgebra-Family of I,S
product s is strict non-empty feasible MSAlgebra over S
SORTS s is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
OPS s is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((SORTS s) #), the ResultSort of S * (SORTS s)
(SORTS s) # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ((SORTS s) #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S * (SORTS s) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (SORTS s),(OPS s) #) is strict MSAlgebra over S
e is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() Function-yielding Relation-yielding FinSequence-like FinSubsequence-like FinSequence-membered set
the Sorts of (product s) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
A is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (S), the Sorts of (product s)
A . E is Relation-like the Sorts of (S) . E -defined the Sorts of (product s) . E -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (S) . E),( the Sorts of (product s) . E):]
the Sorts of (S) . E is non empty set
the Sorts of (product s) . E is non empty set
[:( the Sorts of (S) . E),( the Sorts of (product s) . E):] is Relation-like non empty set
bool [:( the Sorts of (S) . E),( the Sorts of (product s) . E):] is non empty set
F `1 is set
(A . E) . (F `1) is set
F `2 is set
(A . E) . (F `2) is set
i is Relation-like non-empty empty-yielding e -defined Function-like one-to-one constant functional empty total V21() V22() V23() V25() V26() V27() finite finite-yielding V32() Function-yielding Relation-yielding FinSequence-like FinSubsequence-like FinSequence-membered MSAlgebra-Family of e,S
product i is strict non-empty feasible MSAlgebra over S
SORTS i is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
OPS i is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((SORTS i) #), the ResultSort of S * (SORTS i)
(SORTS i) # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ((SORTS i) #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S * (SORTS i) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (SORTS i),(OPS i) #) is strict MSAlgebra over S
the Sorts of (product i) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of (product i) . E is non empty set
Carrier (i,E) is Relation-like non-empty empty-yielding e -defined Function-like one-to-one constant functional empty total V21() V22() V23() V25() V26() V27() finite finite-yielding V32() Function-yielding Relation-yielding FinSequence-like FinSubsequence-like FinSequence-membered set
product (Carrier (i,E)) is set
e is non empty set
i is Relation-like e -defined Function-like non empty total MSAlgebra-Family of e,S
A is Element of e
i . A is non-empty feasible MSAlgebra over S
A is MSAlgebra over S
I is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
(S) is strict non-empty free feasible MSAlgebra over S
the carrier of S --> NAT is Relation-like non-empty non empty-yielding the carrier of S -defined bool REAL -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of S,(bool REAL):]
[: the carrier of S,(bool REAL):] is Relation-like non empty set
bool [: the carrier of S,(bool REAL):] is non empty set
FreeMSA ( the carrier of S --> NAT) is strict non-empty free feasible MSAlgebra over S
FreeSort ( the carrier of S --> NAT) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
FreeOper ( the carrier of S --> NAT) is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((FreeSort ( the carrier of S --> NAT)) #), the ResultSort of S * (FreeSort ( the carrier of S --> NAT))
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total quasi_total Function-yielding Relation-yielding Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is Relation-like non empty set
bool [: the carrier' of S,( the carrier of S *):] is non empty set
(FreeSort ( the carrier of S --> NAT)) # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ((FreeSort ( the carrier of S --> NAT)) #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like non empty set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * (FreeSort ( the carrier of S --> NAT)) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (FreeSort ( the carrier of S --> NAT)),(FreeOper ( the carrier of S --> NAT)) #) is strict MSAlgebra over S
the Sorts of (S) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
[| the Sorts of (S), the Sorts of (S)|] is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
E is Relation-like the carrier of S -defined Function-like non empty total ManySortedSubset of (S)
F is Relation-like I -defined Function-like total MSAlgebra-Family of I,S
product F is strict non-empty feasible MSAlgebra over S
SORTS F is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
OPS F is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Arity of S * ((SORTS F) #), the ResultSort of S * (SORTS F)
(SORTS F) # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ((SORTS F) #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S * (SORTS F) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (SORTS F),(OPS F) #) is strict MSAlgebra over S
s is Element of the carrier of S
(S) . s is non empty set
E . s is set
e is Element of (S) . s
i is set
F . i is set
A is MSAlgebra over S
A is MSAlgebra over S