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

proj1 c

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

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

(e . ((the_arity_of A) . ff)) . (c

i . ((the_arity_of A) . ff) is Relation-like Function-like set

(i . ((the_arity_of A) . ff)) . (c

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

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

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

H " {(h . c

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

c

(c

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

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

( b

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

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

( b

union { b

( b

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

( b

union { b

( b

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

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

( b

union { b

( b

s is set

the Sorts of E . s is set

bool ( the Sorts of E . s) is non empty set

{ b

( b

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

H . c

the Sorts of E . c

bool ( the Sorts of E . c

{ b

( b

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

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

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

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

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

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

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

( b

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

proj2 y is finite set

c

GenMSAlg c

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

the Sorts of E . XX is set

bool ( the Sorts of E . XX) is non empty set

{ b

( b

SY is set

union { b

( b

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