:: MSUALG_2 semantic presentation

K168() is Element of bool K164()

K164() is set

bool K164() is non empty set

K101() is set

bool K101() is non empty set

bool K168() is non empty set

{} is empty Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered set

the empty Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered set is empty Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered set

1 is non empty set

2 is non empty set

3 is non empty set

product {} is set

{{}} is non empty functional set

S is set

U0 is Relation-like S -defined Function-like V17(S) set

A is Relation-like non-empty S -defined Function-like V17(S) set

U0 \/ A is Relation-like S -defined Function-like V17(S) set

x is set

(U0 \/ A) . x is set

U0 . x is set

A . x is set

(U0 . x) \/ (A . x) is set

A \/ U0 is Relation-like non-empty S -defined Function-like V17(S) set

S is non empty set

S * is non empty functional FinSequence-membered M12(S)

U0 is non empty Relation-like S -defined Function-like V17(S) set

A is non empty Relation-like S -defined Function-like V17(S) set

U0 /\ A is non empty Relation-like S -defined Function-like V17(S) set

x is Relation-like K168() -defined S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of S *

x * (U0 /\ A) is Relation-like K168() -defined Function-like set

product (x * (U0 /\ A)) is set

x * U0 is Relation-like K168() -defined Function-like set

product (x * U0) is set

x * A is Relation-like K168() -defined Function-like set

product (x * A) is set

(product (x * U0)) /\ (product (x * A)) is set

rng x is set

dom U0 is non empty set

dom (x * U0) is set

dom x is Element of bool K168()

dom (U0 /\ A) is non empty set

dom (x * (U0 /\ A)) is set

dom A is non empty set

dom (x * A) is set

L is set

G1 is Relation-like Function-like set

dom G1 is set

a is set

G1 . a is set

(x * A) . a is set

(x * (U0 /\ A)) . a is set

x . a is set

(U0 /\ A) . (x . a) is set

U0 . (x . a) is set

A . (x . a) is set

(U0 . (x . a)) /\ (A . (x . a)) is set

a is set

G1 . a is set

(x * U0) . a is set

(x * (U0 /\ A)) . a is set

x . a is set

(U0 /\ A) . (x . a) is set

U0 . (x . a) is set

A . (x . a) is set

(U0 . (x . a)) /\ (A . (x . a)) is set

L is set

G1 is Relation-like Function-like set

dom G1 is set

a is set

G1 . a is set

(x * (U0 /\ A)) . a is set

x . a is set

(x * U0) . a is set

U0 . (x . a) is set

(x * A) . a is set

a1 is Relation-like Function-like set

dom a1 is set

A . (x . a) is set

(U0 . (x . a)) /\ (A . (x . a)) is set

(U0 /\ A) . (x . a) is set

S is non empty V60() ManySortedSign

S is non empty V60() ManySortedSign

the carrier of S is non empty set

U0 is set

S is non empty set

S * is non empty functional FinSequence-membered M12(S)

[:U0,(S *):] is Relation-like set

bool [:U0,(S *):] is non empty set

[:U0,S:] is Relation-like set

bool [:U0,S:] is non empty set

A is Relation-like U0 -defined S * -valued Function-like V17(U0) quasi_total Element of bool [:U0,(S *):]

x is Relation-like U0 -defined S -valued Function-like V17(U0) quasi_total Element of bool [:U0,S:]

ManySortedSign(# S,U0,A,x #) is strict ManySortedSign

the set is set

{ the set } is non empty set

<*> { the set } is empty Relation-like non-empty empty-yielding K168() -defined { the set } -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of { the set }

{(<*> { the set })} is non empty functional set

A is Relation-like Function-like set

dom A is set

rng A is set

{ the set } * is non empty functional FinSequence-membered M12({ the set })

x is set

[:{ the set },({ the set } *):] is non empty Relation-like set

bool [:{ the set },({ the set } *):] is non empty set

L is Relation-like Function-like set

dom L is set

rng L is set

[:{ the set },{ the set }:] is non empty Relation-like set

bool [:{ the set },{ the set }:] is non empty set

x is non empty Relation-like { the set } -defined { the set } * -valued Function-like V17({ the set }) quasi_total Element of bool [:{ the set },({ the set } *):]

G1 is non empty Relation-like { the set } -defined { the set } -valued Function-like V17({ the set }) quasi_total Element of bool [:{ the set },{ the set }:]

ManySortedSign(# { the set },{ the set },x,G1 #) is non empty V60() strict ManySortedSign

the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) is non empty set

the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #) is set

a2 is Element of the carrier of ManySortedSign(# { the set },{ the set },x,G1 #)

a1 is Element of the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #)

the Arity of ManySortedSign(# { the set },{ the set },x,G1 #) is Relation-like the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #) -defined the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) * -valued Function-like V17( the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #)) quasi_total Element of bool [: the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #),( the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) *):]

the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) * is non empty functional FinSequence-membered M12( the carrier of ManySortedSign(# { the set },{ the set },x,G1 #))

[: the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #),( the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) *):] is Relation-like set

bool [: the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #),( the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) *):] is non empty set

the Arity of ManySortedSign(# { the set },{ the set },x,G1 #) . a1 is Relation-like K168() -defined Function-like V34() FinSequence-like FinSubsequence-like set

the ResultSort of ManySortedSign(# { the set },{ the set },x,G1 #) is Relation-like the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #) -defined the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) -valued Function-like V17( the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #)) quasi_total Element of bool [: the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #), the carrier of ManySortedSign(# { the set },{ the set },x,G1 #):]

[: the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #), the carrier of ManySortedSign(# { the set },{ the set },x,G1 #):] is Relation-like set

bool [: the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #), the carrier of ManySortedSign(# { the set },{ the set },x,G1 #):] is non empty set

the ResultSort of ManySortedSign(# { the set },{ the set },x,G1 #) . a1 is set

x . a1 is Relation-like K168() -defined Function-like V34() FinSequence-like FinSubsequence-like set

rng x is non empty set

G1 . a1 is set

rng G1 is non empty set

S is non empty non void V60() ManySortedSign

the carrier of S is non empty set

U0 is MSAlgebra over S

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

A is Element of the carrier of S

the Sorts of U0 . A is set

bool ( the Sorts of U0 . A) is non empty set

the carrier' of S is non empty set

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

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

x is non empty set

{ b

( the Arity of S . b

G1 is set

a is Element of the Sorts of U0 . A

a1 is Element of the carrier' of S

the Arity of S . a1 is Relation-like K168() -defined Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *

the ResultSort of S . a1 is Element of the carrier of S

Den (a1,U0) is Relation-like Args (a1,U0) -defined Result (a1,U0) -valued Function-like quasi_total Element of bool [:(Args (a1,U0)),(Result (a1,U0)):]

Args (a1,U0) is Element of rng ( the Sorts of U0 #)

the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

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

Result (a1,U0) is Element of rng the Sorts of U0

rng the Sorts of U0 is non empty set

[:(Args (a1,U0)),(Result (a1,U0)):] is Relation-like set

bool [:(Args (a1,U0)),(Result (a1,U0)):] is non empty set

rng (Den (a1,U0)) is set

G1 is Element of bool ( the Sorts of U0 . A)

a1 is non empty set

a is Element of bool ( the Sorts of U0 . A)

{ b

( the Arity of S . b

{} ( the Sorts of U0 . A) is empty Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool ( the Sorts of U0 . A)

a is non empty set

L is Element of bool ( the Sorts of U0 . A)

{ b

( the Arity of S . b

a1 is non empty set

G1 is Element of bool ( the Sorts of U0 . A)

{ b

( the Arity of S . b

a2 is Element of bool ( the Sorts of U0 . A)

u23 is Element of bool ( the Sorts of U0 . A)

S is non empty non void V60() ManySortedSign

the carrier of S is non empty set

U0 is MSAlgebra over S

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

A is Relation-like Function-like set

dom A is set

x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

L is set

x . L is set

the Sorts of U0 . L is set

G1 is Element of the carrier of S

x . G1 is set

(S,U0,G1) is Element of bool ( the Sorts of U0 . G1)

the Sorts of U0 . G1 is set

bool ( the Sorts of U0 . G1) is non empty set

L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0

G1 is Element of the carrier of S

L . G1 is set

(S,U0,G1) is Element of bool ( the Sorts of U0 . G1)

the Sorts of U0 . G1 is set

bool ( the Sorts of U0 . G1) is non empty set

A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0

x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0

L is set

A . L is set

x . L is set

G1 is Element of the carrier of S

A . G1 is set

(S,U0,G1) is Element of bool ( the Sorts of U0 . G1)

the Sorts of U0 . G1 is set

bool ( the Sorts of U0 . G1) is non empty set

S is non empty non void V60() () ManySortedSign

the carrier of S is non empty set

U0 is non-empty MSAlgebra over S

A is Element of the carrier of S

(S,U0,A) is Element of bool ( the Sorts of U0 . A)

the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set

the Sorts of U0 . A is non empty set

bool ( the Sorts of U0 . A) is non empty set

dom {} is empty Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool K168()

rng {} is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered set

[:{},{}:] is Relation-like set

bool [:{},{}:] is non empty set

the carrier' of S is non empty set

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

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

L is Element of the carrier' of S

the Arity of S . L is Relation-like K168() -defined Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *

the ResultSort of S . L is Element of the carrier of S

dom the Arity of S is non empty set

the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

dom ( the Sorts of U0 #) is non empty set

rng the Arity of S is non empty set

the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

dom ( the Arity of S * ( the Sorts of U0 #)) is non empty set

Args (L,U0) is non empty Element of rng ( the Sorts of U0 #)

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

( the Arity of S * ( the Sorts of U0 #)) . L is set

( the Sorts of U0 #) . ( the Arity of S . L) is set

the_arity_of L is Relation-like K168() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *

( the Sorts of U0 #) . (the_arity_of L) is set

(the_arity_of L) * the Sorts of U0 is Relation-like non-empty K168() -defined Function-like set

product ((the_arity_of L) * the Sorts of U0) is set

x is empty Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional V17( {} ) quasi_total V34() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [:{},{}:]

x * the Sorts of U0 is empty Relation-like non-empty empty-yielding K168() -defined {} -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered set

product (x * the Sorts of U0) is set

Den (L,U0) is non empty Relation-like Args (L,U0) -defined Result (L,U0) -valued Function-like V17( Args (L,U0)) quasi_total Element of bool [:(Args (L,U0)),(Result (L,U0)):]

Result (L,U0) is non empty Element of rng the Sorts of U0

rng the Sorts of U0 is non empty with_non-empty_elements set

[:(Args (L,U0)),(Result (L,U0)):] is non empty Relation-like set

bool [:(Args (L,U0)),(Result (L,U0)):] is non empty set

rng (Den (L,U0)) is non empty set

dom (Den (L,U0)) is non empty set

(Den (L,U0)) . {} is set

dom the ResultSort of S is non empty set

dom the Sorts of U0 is non empty set

rng the ResultSort of S is non empty set

the ResultSort of S * the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V17( the carrier' of S) set

dom ( the ResultSort of S * the Sorts of U0) is non empty set

( the ResultSort of S * the Sorts of U0) . L is non empty set

a is Element of the Sorts of U0 . A

a1 is non empty set

{ b

( the Arity of S . b

S is non empty non void V60() () ManySortedSign

U0 is non-empty MSAlgebra over S

(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0

the carrier of S is non empty set

the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set

A is set

x is Element of the carrier of S

(S,U0) . x is set

(S,U0,x) is non empty Element of bool ( the Sorts of U0 . x)

the Sorts of U0 . x is non empty set

bool ( the Sorts of U0 . x) is non empty set

(S,U0) . A is set

S is non empty non void V60() ManySortedSign

the carrier' of S is non empty set

the carrier of S is non empty set

U0 is MSAlgebra over S

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

S is non empty non void V60() ManySortedSign

the carrier of S is non empty set

U0 is MSAlgebra over S

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

S is non empty non void V60() ManySortedSign

the carrier' of S is non empty set

the carrier of S is non empty set

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

U0 is Element of the carrier' of S

A is MSAlgebra over S

the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A

L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A

x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

( the Arity of S * (x #)) . U0 is set

L # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (L #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

( the Arity of S * (L #)) . U0 is set

the Arity of S . U0 is Relation-like K168() -defined Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *

G1 is Relation-like K168() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *

rng G1 is set

dom x is non empty set

G1 * x is Relation-like K168() -defined Function-like set

dom (G1 * x) is set

dom G1 is Element of bool K168()

G1 * L is Relation-like K168() -defined Function-like set

a is set

(G1 * x) . a is set

(G1 * L) . a is set

G1 . a is set

x . (G1 . a) is set

L . (G1 . a) is set

dom the Arity of S is non empty set

dom ( the Arity of S * (x #)) is non empty set

(x #) . G1 is set

product (G1 * x) is set

dom ( the Arity of S * (L #)) is non empty set

(L #) . G1 is set

product (G1 * L) is set

dom L is non empty set

dom (G1 * L) is set

S is non empty non void V60() ManySortedSign

the carrier' of S is non empty set

the carrier of S is non empty set

U0 is MSAlgebra over S

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

A is Element of the carrier' of S

x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0

Den (A,U0) is Relation-like Args (A,U0) -defined Result (A,U0) -valued Function-like quasi_total Element of bool [:(Args (A,U0)),(Result (A,U0)):]

Args (A,U0) is Element of rng ( the Sorts of U0 #)

the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

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

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

Result (A,U0) is Element of rng the Sorts of U0

rng the Sorts of U0 is non empty set

[:(Args (A,U0)),(Result (A,U0)):] is Relation-like set

bool [:(Args (A,U0)),(Result (A,U0)):] is non empty set

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

( the Arity of S * (x #)) . A is set

(Den (A,U0)) | (( the Arity of S * (x #)) . A) is Relation-like ( the Arity of S * (x #)) . A -defined Args (A,U0) -defined Result (A,U0) -valued Function-like set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

( the ResultSort of S * x) . A is set

[:(( the Arity of S * (x #)) . A),(( the ResultSort of S * x) . A):] is Relation-like set

bool [:(( the Arity of S * (x #)) . A),(( the ResultSort of S * x) . A):] is non empty set

dom the ResultSort of S is non empty set

rng ((Den (A,U0)) | (( the Arity of S * (x #)) . A)) is set

a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0

rng ((Den (A,U0)) | (( the Arity of S * (x #)) . A)) is set

the ResultSort of S . A is Element of the carrier of S

x . ( the ResultSort of S . A) is set

the Sorts of U0 . ( the ResultSort of S . A) is set

the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

( the ResultSort of S * the Sorts of U0) . A is set

dom (Den (A,U0)) is set

the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

( the Arity of S * ( the Sorts of U0 #)) . A is set

dom ((Den (A,U0)) | (( the Arity of S * (x #)) . A)) is set

(( the Arity of S * ( the Sorts of U0 #)) . A) /\ (( the Arity of S * (x #)) . A) is set

S is non empty non void V60() ManySortedSign

the carrier of S is non empty set

U0 is MSAlgebra over S

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the carrier' of S is non empty set

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0

A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

G1 is set

a is Element of the carrier' of S

(S,U0,a,A) is Relation-like ( the Arity of S * (A #)) . a -defined ( the ResultSort of S * A) . a -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):]

( the Arity of S * (A #)) . a is set

( the ResultSort of S * A) . a is set

[:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):] is Relation-like set

bool [:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):] is non empty set

a1 is Element of the carrier' of S

(S,U0,a1,A) is Relation-like ( the Arity of S * (A #)) . a1 -defined ( the ResultSort of S * A) . a1 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . a1),(( the ResultSort of S * A) . a1):]

( the Arity of S * (A #)) . a1 is set

( the ResultSort of S * A) . a1 is set

[:(( the Arity of S * (A #)) . a1),(( the ResultSort of S * A) . a1):] is Relation-like set

bool [:(( the Arity of S * (A #)) . a1),(( the ResultSort of S * A) . a1):] is non empty set

G1 is Relation-like Function-like set

dom G1 is set

a is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

dom a is non empty set

a1 is set

a . a1 is set

a2 is Element of the carrier' of S

a . a2 is set

(S,U0,a2,A) is Relation-like ( the Arity of S * (A #)) . a2 -defined ( the ResultSort of S * A) . a2 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . a2),(( the ResultSort of S * A) . a2):]

( the Arity of S * (A #)) . a2 is set

( the ResultSort of S * A) . a2 is set

[:(( the Arity of S * (A #)) . a2),(( the ResultSort of S * A) . a2):] is Relation-like set

bool [:(( the Arity of S * (A #)) . a2),(( the ResultSort of S * A) . a2):] is non empty set

a1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() set

a2 is set

a1 . a2 is set

( the Arity of S * (A #)) . a2 is set

( the ResultSort of S * A) . a2 is set

[:(( the Arity of S * (A #)) . a2),(( the ResultSort of S * A) . a2):] is Relation-like set

bool [:(( the Arity of S * (A #)) . a2),(( the ResultSort of S * A) . a2):] is non empty set

u23 is Element of the carrier' of S

a1 . u23 is set

(S,U0,u23,A) is Relation-like ( the Arity of S * (A #)) . u23 -defined ( the ResultSort of S * A) . u23 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . u23),(( the ResultSort of S * A) . u23):]

( the Arity of S * (A #)) . u23 is set

( the ResultSort of S * A) . u23 is set

[:(( the Arity of S * (A #)) . u23),(( the ResultSort of S * A) . u23):] is Relation-like set

bool [:(( the Arity of S * (A #)) . u23),(( the ResultSort of S * A) . u23):] is non empty set

a2 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (A #), the ResultSort of S * A

u23 is Element of the carrier' of S

a2 . u23 is set

(S,U0,u23,A) is Relation-like ( the Arity of S * (A #)) . u23 -defined ( the ResultSort of S * A) . u23 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . u23),(( the ResultSort of S * A) . u23):]

( the Arity of S * (A #)) . u23 is set

( the ResultSort of S * A) . u23 is set

[:(( the Arity of S * (A #)) . u23),(( the ResultSort of S * A) . u23):] is Relation-like set

bool [:(( the Arity of S * (A #)) . u23),(( the ResultSort of S * A) . u23):] is non empty set

x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (A #), the ResultSort of S * A

L is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (A #), the ResultSort of S * A

G1 is set

x . G1 is set

L . G1 is set

a is Element of the carrier' of S

x . a is set

(S,U0,a,A) is Relation-like ( the Arity of S * (A #)) . a -defined ( the ResultSort of S * A) . a -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):]

( the Arity of S * (A #)) . a is set

( the ResultSort of S * A) . a is set

[:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):] is Relation-like set

bool [:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):] is non empty set

S is non empty non void V60() ManySortedSign

the carrier of S is non empty set

the carrier' of S is non empty set

U0 is MSAlgebra over S

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0

x is Element of the carrier' of S

Result (x,U0) is Element of rng the Sorts of U0

rng the Sorts of U0 is non empty set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

( the ResultSort of S * A) . x is set

Den (x,U0) is Relation-like Args (x,U0) -defined Result (x,U0) -valued Function-like quasi_total Element of bool [:(Args (x,U0)),(Result (x,U0)):]

Args (x,U0) is Element of rng ( the Sorts of U0 #)

the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

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

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

[:(Args (x,U0)),(Result (x,U0)):] is Relation-like set

bool [:(Args (x,U0)),(Result (x,U0)):] is non empty set

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

( the Arity of S * (A #)) . x is set

(Den (x,U0)) | (( the Arity of S * (A #)) . x) is Relation-like ( the Arity of S * (A #)) . x -defined Args (x,U0) -defined Result (x,U0) -valued Function-like set

rng ((Den (x,U0)) | (( the Arity of S * (A #)) . x)) is set

x is Element of the carrier' of S

(S,U0,x,A) is Relation-like ( the Arity of S * (A #)) . x -defined ( the ResultSort of S * A) . x -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . x),(( the ResultSort of S * A) . x):]

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

( the Arity of S * (A #)) . x is set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

( the ResultSort of S * A) . x is set

[:(( the Arity of S * (A #)) . x),(( the ResultSort of S * A) . x):] is Relation-like set

bool [:(( the Arity of S * (A #)) . x),(( the ResultSort of S * A) . x):] is non empty set

Den (x,U0) is Relation-like Args (x,U0) -defined Result (x,U0) -valued Function-like quasi_total Element of bool [:(Args (x,U0)),(Result (x,U0)):]

Args (x,U0) is Element of rng ( the Sorts of U0 #)

the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

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

Result (x,U0) is Element of rng the Sorts of U0

rng the Sorts of U0 is non empty set

[:(Args (x,U0)),(Result (x,U0)):] is Relation-like set

bool [:(Args (x,U0)),(Result (x,U0)):] is non empty set

(Den (x,U0)) | (( the Arity of S * (A #)) . x) is Relation-like ( the Arity of S * (A #)) . x -defined Args (x,U0) -defined Result (x,U0) -valued Function-like set

dom (Den (x,U0)) is set

S is non empty non void V60() ManySortedSign

the carrier of S is non empty set

the carrier' of S is non empty set

U0 is MSAlgebra over S

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0

(S,U0,A) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (A #), the ResultSort of S * A

A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S * A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

G1 is set

the Charact of U0 . G1 is set

(S,U0,A) . G1 is set

a is Element of the carrier' of S

the Charact of U0 . a is set

Den (a,U0) is Relation-like Args (a,U0) -defined Result (a,U0) -valued Function-like quasi_total Element of bool [:(Args (a,U0)),(Result (a,U0)):]

Args (a,U0) is Element of rng ( the Sorts of U0 #)

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

Result (a,U0) is Element of rng the Sorts of U0

rng the Sorts of U0 is non empty set

[:(Args (a,U0)),(Result (a,U0)):] is Relation-like set

bool [:(Args (a,U0)),(Result (a,U0)):] is non empty set

(S,U0,A) . a is set

(S,U0,a,A) is Relation-like ( the Arity of S * (A #)) . a -defined ( the ResultSort of S * A) . a -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):]

( the Arity of S * (A #)) . a is set

( the ResultSort of S * A) . a is set

[:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):] is Relation-like set

bool [:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):] is non empty set

S is non empty non void V60() ManySortedSign

the carrier of S is non empty set

U0 is MSAlgebra over S

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the carrier' of S is non empty set

A is MSAlgebra over S

the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0

(S,U0,x) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (x #), the ResultSort of S * x

x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S * x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

a is set

the Charact of A . a is set

(S,U0,x) . a is set

a1 is Element of the carrier' of S

the Charact of A . a1 is set

Den (a1,A) is Relation-like Args (a1,A) -defined Result (a1,A) -valued Function-like quasi_total Element of bool [:(Args (a1,A)),(Result (a1,A)):]

Args (a1,A) is Element of rng ( the Sorts of A #)

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

Result (a1,A) is Element of rng the Sorts of A

rng the Sorts of A is non empty set

[:(Args (a1,A)),(Result (a1,A)):] is Relation-like set

bool [:(Args (a1,A)),(Result (a1,A)):] is non empty set

(S,U0,x) . a1 is set

(S,U0,a1,x) is Relation-like ( the Arity of S * (x #)) . a1 -defined ( the ResultSort of S * x) . a1 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (x #)) . a1),(( the ResultSort of S * x) . a1):]

( the Arity of S * (x #)) . a1 is set

( the ResultSort of S * x) . a1 is set

[:(( the Arity of S * (x #)) . a1),(( the ResultSort of S * x) . a1):] is Relation-like set

bool [:(( the Arity of S * (x #)) . a1),(( the ResultSort of S * x) . a1):] is non empty set

S is non empty non void V60() ManySortedSign

U0 is MSAlgebra over S

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the carrier of S is non empty set

the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0

the carrier' of S is non empty set

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S

A is strict MSAlgebra over S

the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A

the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0

(S,U0,x) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (x #), the ResultSort of S * x

x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S * x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

a is set

the Charact of A . a is set

(S,U0,x) . a is set

a1 is Element of the carrier' of S

the Charact of A . a1 is set

Den (a1,U0) is Relation-like Args (a1,U0) -defined Result (a1,U0) -valued Function-like quasi_total Element of bool [:(Args (a1,U0)),(Result (a1,U0)):]

Args (a1,U0) is Element of rng ( the Sorts of U0 #)

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

Result (a1,U0) is Element of rng the Sorts of U0

rng the Sorts of U0 is non empty set

[:(Args (a1,U0)),(Result (a1,U0)):] is Relation-like set

bool [:(Args (a1,U0)),(Result (a1,U0)):] is non empty set

(S,U0,x) . a1 is set

(S,U0,a1,x) is Relation-like ( the Arity of S * (x #)) . a1 -defined ( the ResultSort of S * x) . a1 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (x #)) . a1),(( the ResultSort of S * x) . a1):]

( the Arity of S * (x #)) . a1 is set

( the ResultSort of S * x) . a1 is set

[:(( the Arity of S * (x #)) . a1),(( the ResultSort of S * x) . a1):] is Relation-like set

bool [:(( the Arity of S * (x #)) . a1),(( the ResultSort of S * x) . a1):] is non empty set

S is non empty non void V60() ManySortedSign

U0 is MSAlgebra over S

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the carrier of S is non empty set

the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0

the carrier' of S is non empty set

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S

S is non empty non void V60() ManySortedSign

U0 is non-empty MSAlgebra over S

the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set

the carrier of S is non empty set

the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0

the carrier' of S is non empty set

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V17( the carrier' of S) set

MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S

S is non empty non void V60() ManySortedSign

U0 is non-empty MSAlgebra over S

the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set

the carrier of S is non empty set

the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0

the carrier' of S is non empty set

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V17( the carrier' of S) set

MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict non-empty MSAlgebra over S

S is non empty non void V60() ManySortedSign

U0 is MSAlgebra over S

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the carrier of S is non empty set

the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0

the carrier' of S is non empty set

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S

A is MSAlgebra over S

the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A

the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

MSAlgebra(# the Sorts of A, the Charact of A #) is strict MSAlgebra over S

x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A

(S,A,x) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (x #), the ResultSort of S * x

x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S * x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

a is Element of the carrier' of S

Den (a,A) is Relation-like Args (a,A) -defined Result (a,A) -valued Function-like quasi_total Element of bool [:(Args (a,A)),(Result (a,A)):]

Args (a,A) is Element of rng ( the Sorts of A #)

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

Result (a,A) is Element of rng the Sorts of A

rng the Sorts of A is non empty set

[:(Args (a,A)),(Result (a,A)):] is Relation-like set

bool [:(Args (a,A)),(Result (a,A)):] is non empty set

( the Arity of S * (x #)) . a is set

(Den (a,A)) | (( the Arity of S * (x #)) . a) is Relation-like ( the Arity of S * (x #)) . a -defined Args (a,A) -defined Result (a,A) -valued Function-like set

rng ((Den (a,A)) | (( the Arity of S * (x #)) . a)) is set

rng (Den (a,A)) is set

( the ResultSort of S * x) . a is set

a is set

the Charact of U0 . a is set

(S,A,x) . a is set

S is non empty non void V60() ManySortedSign

U0 is MSAlgebra over S

A is MSAlgebra over S

x is MSAlgebra over S

the carrier of S is non empty set

the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A

the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of x

the carrier' of S is non empty set

the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

(S,x,G1) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (G1 #), the ResultSort of S * G1

G1 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (G1 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S * G1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0

the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

a1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of x

(S,x,a1) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (a1 #), the ResultSort of S * a1

a1 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (a1 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S * a1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

(S,A,L) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (L #), the ResultSort of S * L

L # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (L #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S * L is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

u12 is Element of the carrier' of S

Den (u12,A) is Relation-like Args (u12,A) -defined Result (u12,A) -valued Function-like quasi_total Element of bool [:(Args (u12,A)),(Result (u12,A)):]

Args (u12,A) is Element of rng ( the Sorts of A #)

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

Result (u12,A) is Element of rng the Sorts of A

rng the Sorts of A is non empty set

[:(Args (u12,A)),(Result (u12,A)):] is Relation-like set

bool [:(Args (u12,A)),(Result (u12,A)):] is non empty set

(S,x,G1) . u12 is set

(S,x,u12,G1) is Relation-like ( the Arity of S * (G1 #)) . u12 -defined ( the ResultSort of S * G1) . u12 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (G1 #)) . u12),(( the ResultSort of S * G1) . u12):]

( the Arity of S * (G1 #)) . u12 is set

( the ResultSort of S * G1) . u12 is set

[:(( the Arity of S * (G1 #)) . u12),(( the ResultSort of S * G1) . u12):] is Relation-like set

bool [:(( the Arity of S * (G1 #)) . u12),(( the ResultSort of S * G1) . u12):] is non empty set

Den (u12,x) is Relation-like Args (u12,x) -defined Result (u12,x) -valued Function-like quasi_total Element of bool [:(Args (u12,x)),(Result (u12,x)):]

Args (u12,x) is Element of rng ( the Sorts of x #)

the Sorts of x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

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

Result (u12,x) is Element of rng the Sorts of x

rng the Sorts of x is non empty set

[:(Args (u12,x)),(Result (u12,x)):] is Relation-like set

bool [:(Args (u12,x)),(Result (u12,x)):] is non empty set

(Den (u12,x)) | (( the Arity of S * (G1 #)) . u12) is Relation-like ( the Arity of S * (G1 #)) . u12 -defined Args (u12,x) -defined Result (u12,x) -valued Function-like set

( the Arity of S * (L #)) . u12 is set

a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A

a # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * (a #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

( the Arity of S * (a #)) . u12 is set

Den (u12,U0) is Relation-like Args (u12,U0) -defined Result (u12,U0) -valued Function-like quasi_total Element of bool [:(Args (u12,U0)),(Result (u12,U0)):]

Args (u12,U0) is Element of rng ( the Sorts of U0 #)

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

Result (u12,U0) is Element of rng the Sorts of U0

rng the Sorts of U0 is non empty set

[:(Args (u12,U0)),(Result (u12,U0)):] is Relation-like set

bool [:(Args (u12,U0)),(Result (u12,U0)):] is non empty set

(S,A,L) . u12 is set

(S,A,u12,L) is Relation-like ( the Arity of S * (L #)) . u12 -defined ( the ResultSort of S * L) . u12 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (L #)) . u12),(( the ResultSort of S * L) . u12):]

( the ResultSort of S * L) . u12 is set

[:(( the Arity of S * (L #)) . u12),(( the ResultSort of S * L) . u12):] is Relation-like set

bool [:(( the Arity of S * (L #)) . u12),(( the ResultSort of S * L) . u12):] is non empty set

((Den (u12,x)) | (( the Arity of S * (G1 #)) . u12)) | (( the Arity of S * (L #)) . u12) is Relation-like ( the Arity of S * (L #)) . u12 -defined ( the Arity of S * (G1 #)) . u12 -defined Result (u12,x) -valued Function-like set

(( the Arity of S * (G1 #)) . u12) /\ (( the Arity of S * (L #)) . u12) is set

(Den (u12,x)) | ((( the Arity of S * (G1 #)) . u12) /\ (( the Arity of S * (L #)) . u12)) is Relation-like (( the Arity of S * (G1 #)) . u12) /\ (( the Arity of S * (L #)) . u12) -defined Args (u12,x) -defined Result (u12,x) -valued Function-like set

(Den (u12,x)) | (( the Arity of S * (L #)) . u12) is Relation-like ( the Arity of S * (L #)) . u12 -defined Args (u12,x) -defined Result (u12,x) -valued Function-like set

rng ((Den (u12,x)) | (( the Arity of S * (L #)) . u12)) is set

( the ResultSort of S * the Sorts of U0) . u12 is set

u12 is set

the Charact of U0 . u12 is set

(S,x,a1) . u12 is set

C is Element of the carrier' of S

Den (C,A) is Relation-like Args (C,A) -defined Result (C,A) -valued Function-like quasi_total Element of bool [:(Args (C,A)),(Result (C,A)):]

Args (C,A) is Element of rng ( the Sorts of A #)

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

Result (C,A) is Element of rng the Sorts of A

rng the Sorts of A is non empty set

[:(Args (C,A)),(Result (C,A)):] is Relation-like set

bool [:(Args (C,A)),(Result (C,A)):] is non empty set

(S,x,G1) . C is set

(S,x,C,G1) is Relation-like ( the Arity of S * (G1 #)) . C -defined ( the ResultSort of S * G1) . C -valued Function-like quasi_total Element of bool [:(( the Arity of S * (G1 #)) . C),(( the ResultSort of S * G1) . C):]

( the Arity of S * (G1 #)) . C is set

( the ResultSort of S * G1) . C is set

[:(( the Arity of S * (G1 #)) . C),(( the ResultSort of S * G1) . C):] is Relation-like set

bool [:(( the Arity of S * (G1 #)) . C),(( the ResultSort of S * G1) . C):] is non empty set

Den (C,x) is Relation-like Args (C,x) -defined Result (C,x) -valued Function-like quasi_total Element of bool [:(Args (C,x)),(Result (C,x)):]

Args (C,x) is Element of rng ( the Sorts of x #)

the Sorts of x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

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

Result (C,x) is Element of rng the Sorts of x

rng the Sorts of x is non empty set

[:(Args (C,x)),(Result (C,x)):] is Relation-like set

bool [:(Args (C,x)),(Result (C,x)):] is non empty set

(Den (C,x)) | (( the Arity of S * (G1 #)) . C) is Relation-like ( the Arity of S * (G1 #)) . C -defined Args (C,x) -defined Result (C,x) -valued Function-like set

(S,A,C,L) is Relation-like ( the Arity of S * (L #)) . C -defined ( the ResultSort of S * L) . C -valued Function-like quasi_total Element of bool [:(( the Arity of S * (L #)) . C),(( the ResultSort of S * L) . C):]

( the Arity of S * (L #)) . C is set

( the ResultSort of S * L) . C is set

[:(( the Arity of S * (L #)) . C),(( the ResultSort of S * L) . C):] is Relation-like set

bool [:(( the Arity of S * (L #)) . C),(( the ResultSort of S * L) . C):] is non empty set

((Den (C,x)) | (( the Arity of S * (G1 #)) . C)) | (( the Arity of S * (L #)) . C) is Relation-like ( the Arity of S * (L #)) . C -defined ( the Arity of S * (G1 #)) . C -defined Result (C,x) -valued Function-like set

(( the Arity of S * (G1 #)) . C) /\ (( the Arity of S * (L #)) . C) is set

(Den (C,x)) | ((( the Arity of S * (G1 #)) . C) /\ (( the Arity of S * (L #)) . C)) is Relation-like (( the Arity of S * (G1 #)) . C) /\ (( the Arity of S * (L #)) . C) -defined Args (C,x) -defined Result (C,x) -valued Function-like set

( the Arity of S * (a1 #)) . C is set

(Den (C,x)) | (( the Arity of S * (a1 #)) . C) is Relation-like ( the Arity of S * (a1 #)) . C -defined Args (C,x) -defined Result (C,x) -valued Function-like set

(S,x,C,a1) is Relation-like ( the Arity of S * (a1 #)) . C -defined ( the ResultSort of S * a1) . C -valued Function-like quasi_total Element of bool [:(( the Arity of S * (a1 #)) . C),(( the ResultSort of S * a1) . C):]

( the ResultSort of S * a1) . C is set

[:(( the Arity of S * (a1 #)) . C),(( the ResultSort of S * a1) . C):] is Relation-like set

bool [:(( the Arity of S * (a1 #)) . C),(( the ResultSort of S * a1) . C):] is non empty set

S is non empty non void V60() ManySortedSign

U0 is MSAlgebra over S

the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the carrier of S is non empty set

the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0

the carrier' of S is non empty set

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S

A is MSAlgebra over S

the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set

the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A

the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set

the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set

MSAlgebra(# the Sorts of A, the Charact of A #) is strict MSAlgebra over S

x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A

(S,A,x) is non