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

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

bool [:K309(K310()),NAT:] is non empty set

bool [:NAT,K309(K310()):] is non empty set
2 is non empty set
3 is non empty 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

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

i is set

proj2 (e . i) is set
F . i is 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

proj1 (() . F) is set
proj2 (() . F) is set
Funcs (I,E) is functional set
Funcs (S,(Funcs (I,E))) is functional set
proj2 () is set

proj1 i is set
proj2 i is set

proj1 i is set
proj2 i is set

proj1 i is set
proj2 i is set
I is set

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

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

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

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

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

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

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

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 set
F . e is set

S . e is set
(E . e) " (S . e) is set
s . e is set
I is set

e is set
(s .:.: F) . e is set
E . e is set
i is non empty set

A is Element of i
A . A is set
Z . A is set

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

(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 Element of i
A . A is set
Z . A is set

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

(I,E,F) is Relation-like I -defined Function-like total set
s is 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

(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

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

F is set
(S .:.: E) . F is set
(rngs S) . F is set

E . F is set
(S . F) .: (E . F) is set
proj2 (S . F) is set
I is set

E is set
(S .:.: (doms S)) . E is 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

(I,(rngs S),S) is Relation-like I -defined Function-like total set

E is set
(I,(rngs S),S) . E is 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

I is set

(I,S,(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

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

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

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

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

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

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

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 * (() #), the ResultSort of S * ()
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

the Arity of S * (() #) 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 * () is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (),(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

Den (s,()) is Relation-like Args (s,()) -defined Result (s,()) -valued Function-like non empty total quasi_total Element of bool [:(Args (s,())),(Result (s,())):]
Args (s,()) is functional non empty Element of proj2 ( the Sorts of () #)
the Sorts of () is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of () # is Relation-like the carrier of S * -defined Function-like non empty total set
proj2 ( the Sorts of () #) is non empty set
the Arity of S * ( the Sorts of () #) is Relation-like the carrier' of S -defined Function-like non empty total set
( the Arity of S * ( the Sorts of () #)) . s is set
Result (s,()) is non empty Element of proj2 the Sorts of ()
proj2 the Sorts of () is non empty V155() set
the ResultSort of S * the Sorts of () 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 ()) . s is non empty set
[:(Args (s,())),(Result (s,())):] is Relation-like non empty set
bool [:(Args (s,())),(Result (s,())):] is non empty set
the Charact of () 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 () #), the ResultSort of S * the Sorts of ()
the Charact of () . s is Relation-like Function-like set
e is set
(Den (s,F)) . e is set
(Den (s,())) . 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

product (Carrier (E,)) is set
() . is non empty set

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

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 * (() #), the ResultSort of 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
() # is Relation-like the carrier of I * -defined Function-like non empty total set
the Arity of 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 * () is Relation-like non-empty non empty-yielding the carrier' of I -defined Function-like non empty total set
MSAlgebra(# (),() #) 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

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

the Sorts of () 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

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

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

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)

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)

proj1 s is set

proj1 c14 is set
ff is set
() . ff is set
the Sorts of E . (() . ff) is set
the Sorts of S . (() . ff) is set
[:( the Sorts of E . (() . ff)),( the Sorts of S . (() . ff)):] is Relation-like set
bool [:( the Sorts of E . (() . ff)),( the Sorts of S . (() . ff)):] is non empty set
e . (() . ff) is Relation-like Function-like set
y is V21() V22() V23() V27() set
() . y is set
i . (() . y) is Relation-like Function-like set
aa is Relation-like the Sorts of E . (() . ff) -defined the Sorts of S . (() . ff) -valued Function-like quasi_total Element of bool [:( the Sorts of E . (() . ff)),( the Sorts of S . (() . ff)):]
s . (() . ff) is set
aa | (s . (() . ff)) is Relation-like the Sorts of E . (() . ff) -defined s . (() . ff) -defined the Sorts of E . (() . ff) -defined the Sorts of S . (() . ff) -valued Function-like Element of bool [:( the Sorts of E . (() . ff)),( the Sorts of S . (() . ff)):]

dom (() * the Sorts of F) is finite Element of bool NAT
c14 . ff is set
(() * the Sorts of F) . ff is set
(e # A) . ff is set
(e # A) . y is set
() /. ff is Element of the carrier of I
e . (() /. ff) is Relation-like the Sorts of E . (() /. ff) -defined the Sorts of S . (() /. ff) -valued Function-like total quasi_total Element of bool [:( the Sorts of E . (() /. ff)),( the Sorts of S . (() /. ff)):]
the Sorts of E . (() /. ff) is set
the Sorts of S . (() /. ff) is non empty set
[:( the Sorts of E . (() /. ff)),( the Sorts of S . (() /. ff)):] is Relation-like set
bool [:( the Sorts of E . (() /. ff)),( the Sorts of S . (() /. ff)):] is non empty set
(e . (() /. ff)) . (c14 . ff) is set
(e . (() . ff)) . (c14 . ff) is set
i . (() . ff) is Relation-like Function-like set
(i . (() . ff)) . (c14 . ff) is set
i . (() /. ff) is Relation-like the Sorts of F . (() /. ff) -defined the Sorts of S . (() /. ff) -valued Function-like total quasi_total Element of bool [:( the Sorts of F . (() /. ff)),( the Sorts of S . (() /. ff)):]
the Sorts of F . (() /. ff) is set
[:( the Sorts of F . (() /. ff)),( the Sorts of S . (() /. ff)):] is Relation-like set
bool [:( the Sorts of F . (() /. ff)),( the Sorts of S . (() /. ff)):] is non empty set
s . ff is set
(i . (() /. 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

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

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 . is Relation-like the Sorts of F . -defined the Sorts of S . -valued Function-like total quasi_total Element of bool [:( the Sorts of F . ),( the Sorts of S . ):]
the Sorts of F . is set
the Sorts of S . is non empty set
[:( the Sorts of F . ),( the Sorts of S . ):] is Relation-like set
bool [:( the Sorts of F . ),( the Sorts of S . ):] 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

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

A is Element of Args (A,F)
(Den (A,F)) . A is set
(i . ) . ((Den (A,F)) . A) is set

(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

(Den (A,E)) . A is set
e . is Relation-like the Sorts of E . -defined the Sorts of S . -valued Function-like total quasi_total Element of bool [:( the Sorts of E . ),( the Sorts of S . ):]
the Sorts of E . is set
[:( the Sorts of E . ),( the Sorts of S . ):] is Relation-like set
bool [:( the Sorts of E . ),( the Sorts of S . ):] is non empty set
(e . ) . ((Den (A,E)) . A) is set
Z is Element of Args (A,E)

(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

E is strict non-empty feasible MSAlgebra over I

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

the Sorts of () 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

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

A is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total ManySortedSubset of the Sorts of ()

I is non empty non void feasible ManySortedSign
the carrier of I is non empty set
S is non-empty feasible MSAlgebra over I

E is non-empty feasible MSAlgebra over I

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

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

(A || Z) . G is Relation-like Function-like set
c14 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 . c14 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 . c14)} is non empty finite set
H " {(h . c14)} is Element of bool ( the Sorts of S . G)
bool ( the Sorts of S . G) is non empty set
s 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 F, 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

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

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
c14 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):]
c14 * 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):]
(c14 * 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 (c14 * ff) is Element of bool (Z . H)

(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

MSSub E is non empty set
{ b1 where b1 is Element of MSSub E : ex b2 being Element of S ex b3 being strict non-empty finitely-generated feasible MSSubAlgebra of E st
( b1 = F . b2 & b1 = b3 )
}
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 non empty 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 (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 Element of S
F . h is non-empty feasible MSAlgebra over I

c14 is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of H

ff is Relation-like the carrier of I -defined Function-like non empty total Element of Bool the Sorts of E

[:A,(Bool the Sorts of E):] is Relation-like non empty set
bool [:A,(Bool the Sorts of E):] is non empty set

{ b1 where b1 is Element of bool ( the Sorts of E . a1) : ex b2 being Element of S ex b3 being Relation-like the carrier of I -defined Function-like non empty total set st
( b3 = Z . (F . b2) & b1 = b3 . a1 )
}
is set

union { b1 where b1 is Element of bool ( the Sorts of E . a1) : ex b2 being Element of S ex b3 being Relation-like the carrier of I -defined Function-like non empty total set st
( b3 = Z . (F . b2) & b1 = b3 . a1 )
}
is 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
{ b1 where b1 is Element of bool ( the Sorts of E . h) : ex b2 being Element of S ex b3 being Relation-like the carrier of I -defined Function-like non empty total set st
( b3 = Z . (F . b2) & b1 = b3 . h )
}
is set

union { b1 where b1 is Element of bool ( the Sorts of E . h) : ex b2 being Element of S ex b3 being Relation-like the carrier of I -defined Function-like non empty total set st
( b3 = Z . (F . b2) & b1 = b3 . 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

Z . (F . the Element of S) is Relation-like Function-like set

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 . ff is finite set

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
{ b1 where b1 is Element of bool ( the Sorts of E . ff) : ex b2 being Element of S ex b3 being Relation-like the carrier of I -defined Function-like non empty total set st
( b3 = Z . (F . b2) & b1 = b3 . ff )
}
is set

union { b1 where b1 is Element of bool ( the Sorts of E . ff) : ex b2 being Element of S ex b3 being Relation-like the carrier of I -defined Function-like non empty total set st
( b3 = Z . (F . b2) & b1 = b3 . ff )
}
is set

s is set
the Sorts of E . s is set
bool ( the Sorts of E . s) is non empty set
{ b1 where b1 is Element of bool ( the Sorts of E . s) : ex b2 being Element of S ex b3 being Relation-like the carrier of I -defined Function-like non empty total set st
( b3 = Z . (F . b2) & b1 = b3 . s )
}
is set

Z . (F . the Element of S) is Relation-like Function-like set

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
c14 is set
H . c14 is set
the Sorts of E . c14 is set
bool ( the Sorts of E . c14) is non empty set
{ b1 where b1 is Element of bool ( the Sorts of E . c14) : ex b2 being Element of S ex b3 being Relation-like the carrier of I -defined Function-like non empty total set st
( b3 = Z . (F . b2) & b1 = b3 . c14 )
}
is 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

Z . (F . aa) is Relation-like Function-like set

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 . c14 is finite set
L is Element of ff
[:S,ff:] is Relation-like non empty set
bool [:S,ff:] is non empty set

dom aa is non empty finite Element of bool S
bool S is non empty finite V32() set

proj2 WW is finite set
XX is set
L is Element of bool ( the Sorts of E . c14)

SY is Element of S
F . SY is non-empty feasible MSAlgebra over I
Z . (F . SY) is Relation-like Function-like set
Y . c14 is 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 . c14 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 . c14 is 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 . c14)

WW is Element of S
F . WW is non-empty feasible MSAlgebra over I
Z . (F . WW) is Relation-like Function-like set
XX . c14 is 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 . c14 is set

SY is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of L
union { b1 where b1 is Element of bool ( the Sorts of E . c14) : ex b2 being Element of S ex b3 being Relation-like the carrier of I -defined Function-like non empty total set st
( b3 = Z . (F . b2) & b1 = b3 . c14 )
}
is set

s is Element of S
F . s is non-empty feasible MSAlgebra over I

Z . (F . s) is Relation-like Function-like set

aa is Relation-like the carrier of I -defined Function-like non empty total GeneratorSet of y

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
c14 . XX is finite set
the Sorts of E . XX is set
bool ( the Sorts of E . XX) is non empty set
{ b1 where b1 is Element of bool ( the Sorts of E . XX) : ex b2 being Element of S ex b3 being Relation-like the carrier of I -defined Function-like non empty total set st
( b3 = Z . (F . b2) & b1 = b3 . XX )
}
is set

SY is set
union { b1 where b1 is Element of bool ( the Sorts of E . XX) : ex b2 being Element of S ex b3 being Relation-like the carrier of I -defined Function-like non empty total set st
( b3 = Z . (F . b2) & b1 = b3 . XX )
}
is set

GenMSAlg aa is strict MSSubAlgebra of y

I is non empty non void feasible ManySortedSign
S is non-empty feasible MSAlgebra over I

{0,1} is non empty finite set
s is set