:: MSALIMIT semantic presentation

K138() is non empty V21() V22() V23() V28() countable denumerable Element of bool K134()

K134() is set

bool K134() is non empty set

K87() is non empty V21() V22() V23() V28() countable denumerable set

bool K87() is non empty set

bool K138() is non empty set

K183() is set

{} is Relation-like non-empty empty-yielding K138() -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered set

the Relation-like non-empty empty-yielding K138() -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding K138() -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered set

{{}} is functional non empty with_common_domain set

{{}} * is functional non empty FinSequence-membered M8({{}})

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

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

PFuncs (({{}} *),{{}}) is set

1 is non empty set

{{},1} is non empty set

[:1,1:] is Relation-like non empty set

bool [:1,1:] is non empty set

[:[:1,1:],1:] is Relation-like non empty set

bool [:[:1,1:],1:] is non empty set

2 is non empty set

3 is non empty set

Funcs ({},{}) is functional non empty set

id {} is Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional empty total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered set

{(id {})} is functional non empty with_common_domain set

product {} is functional non empty with_common_domain product-like set

proj1 {} is Relation-like non-empty empty-yielding K138() -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered set

proj2 {} is Relation-like non-empty empty-yielding K138() -defined Function-like one-to-one constant functional empty trivial V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered V108() set

S1 is non empty set

S2 is non empty non void V56() ManySortedSign

the carrier' of S2 is non empty set

A1 is Relation-like S1 -defined Function-like non empty total MSAlgebra-Family of S1,S2

OPER A1 is Relation-like S1 -defined Function-like non empty total Function-yielding V42() set

A2 is Element of S1

(OPER A1) . A2 is Relation-like Function-like set

x is Element of the carrier' of S2

((OPER A1) . A2) . x is set

A1 . A2 is non-empty MSAlgebra over S2

g is MSAlgebra over S2

the Charact of g is Relation-like the carrier' of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of S2 * ( the Sorts of g #), the ResultSort of S2 * the Sorts of g

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

the carrier of S2 is non empty set

the carrier of S2 * is functional non empty FinSequence-membered M8( the carrier of S2)

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

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

the Sorts of g is Relation-like the carrier of S2 -defined Function-like non empty total set

the Sorts of g # is Relation-like the carrier of S2 * -defined Function-like non empty total set

the Arity of S2 * ( the Sorts of g #) is Relation-like the carrier' of S2 -defined Function-like non empty total set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of S2, the carrier of S2:]

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

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

the ResultSort of S2 * the Sorts of g is Relation-like the carrier' of S2 -defined Function-like non empty total set

S1 is non empty set

S2 is non empty non void V56() ManySortedSign

the carrier of S2 is non empty set

A1 is Relation-like S1 -defined Function-like non empty total MSAlgebra-Family of S1,S2

SORTS A1 is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

A2 is Element of the carrier of S2

(SORTS A1) . A2 is non empty set

Carrier (A1,A2) is Relation-like non-empty non empty-yielding S1 -defined Function-like non empty total set

product (Carrier (A1,A2)) is functional non empty with_common_domain product-like set

S1 is non empty total reflexive transitive antisymmetric RelStr

the carrier of S1 is non empty set

S2 is non empty non void V56() ManySortedSign

the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]

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

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

the carrier of S2 is non empty set

the non-empty MSAlgebra over S2 is non-empty MSAlgebra over S2

the carrier of S1 --> the non-empty MSAlgebra over S2 is Relation-like the carrier of S1 -defined { the non-empty MSAlgebra over S2} -valued Function-like constant non empty total quasi_total Element of bool [: the carrier of S1,{ the non-empty MSAlgebra over S2}:]

{ the non-empty MSAlgebra over S2} is non empty set

[: the carrier of S1,{ the non-empty MSAlgebra over S2}:] is Relation-like non empty set

bool [: the carrier of S1,{ the non-empty MSAlgebra over S2}:] is non empty set

x is Relation-like the carrier of S1 -defined Function-like non empty total set

g is set

x . g is set

g is Relation-like the carrier of S1 -defined Function-like non empty total MSAlgebra-Family of the carrier of S1,S2

the Sorts of the non-empty MSAlgebra over S2 is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of the non-empty MSAlgebra over S2 is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of the non-empty MSAlgebra over S2, the Sorts of the non-empty MSAlgebra over S2

the InternalRel of S1 --> (id the Sorts of the non-empty MSAlgebra over S2) is Relation-like non-empty the InternalRel of S1 -defined {(id the Sorts of the non-empty MSAlgebra over S2)} -valued Function-like constant total quasi_total Function-yielding V42() Element of bool [: the InternalRel of S1,{(id the Sorts of the non-empty MSAlgebra over S2)}:]

{(id the Sorts of the non-empty MSAlgebra over S2)} is functional non empty with_common_domain set

[: the InternalRel of S1,{(id the Sorts of the non-empty MSAlgebra over S2)}:] is Relation-like set

bool [: the InternalRel of S1,{(id the Sorts of the non-empty MSAlgebra over S2)}:] is non empty set

f is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() set

i is Element of the carrier of S1

g . i is non-empty MSAlgebra over S2

the Sorts of (g . i) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

j is Element of the carrier of S1

g . j is non-empty MSAlgebra over S2

the Sorts of (g . j) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

f . (j,i) is set

[j,i] is V15() set

{j,i} is non empty set

{j} is non empty set

{{j,i},{j}} is non empty set

f . [j,i] is Relation-like Function-like set

s is Element of the carrier of S1

g . s is non-empty MSAlgebra over S2

the Sorts of (g . s) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

f . (s,j) is set

[s,j] is V15() set

{s,j} is non empty set

{s} is non empty set

{{s,j},{s}} is non empty set

f . [s,j] is Relation-like Function-like set

f . (s,i) is set

[s,i] is V15() set

{s,i} is non empty set

{{s,i},{s}} is non empty set

f . [s,i] is Relation-like Function-like set

f is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (g . j), the Sorts of (g . s)

A1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]

field A1 is set

y is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (g . i), the Sorts of (g . j)

f ** y is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (g . i), the Sorts of (g . s)

S1 is non empty total reflexive transitive antisymmetric RelStr

the carrier of S1 is non empty set

S2 is non empty non void V56() ManySortedSign

the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]

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

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

the carrier of S2 is non empty set

A1 is Relation-like the carrier of S1 -defined Function-like non empty total (S1,S2)

S1 is non empty total reflexive transitive antisymmetric RelStr

the carrier of S1 is non empty set

S2 is non empty non void V56() ManySortedSign

the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]

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

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

A1 is Relation-like the carrier of S1 -defined Function-like non empty total (S1,S2)

g is Element of the carrier of S1

x is Element of the carrier of S1

A2 is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)

A2 . (g,x) is set

[g,x] is V15() set

{g,x} is non empty set

{g} is non empty set

{{g,x},{g}} is non empty set

A2 . [g,x] is Relation-like Function-like set

the carrier of S2 is non empty set

A1 . x is non-empty MSAlgebra over S2

the Sorts of (A1 . x) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

A1 . g is non-empty MSAlgebra over S2

the Sorts of (A1 . g) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

A2 . (g,g) is set

[g,g] is V15() set

{g,g} is non empty set

{{g,g},{g}} is non empty set

A2 . [g,g] is Relation-like Function-like set

e is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . g)

f is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . g), the Sorts of (A1 . g)

f ** e is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . g)

S1 is non empty total reflexive transitive antisymmetric RelStr

the carrier of S1 is non empty set

the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]

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

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

S2 is Element of the carrier of S1

A1 is Element of the carrier of S1

A2 is Element of the carrier of S1

x is non empty non void V56() ManySortedSign

the carrier of x is non empty set

g is Relation-like the carrier of S1 -defined Function-like non empty total (S1,x)

g . S2 is non-empty MSAlgebra over x

the Sorts of (g . S2) is Relation-like non-empty non empty-yielding the carrier of x -defined Function-like non empty total set

g . A1 is non-empty MSAlgebra over x

the Sorts of (g . A1) is Relation-like non-empty non empty-yielding the carrier of x -defined Function-like non empty total set

g . A2 is non-empty MSAlgebra over x

the Sorts of (g . A2) is Relation-like non-empty non empty-yielding the carrier of x -defined Function-like non empty total set

e is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,x,g)

(S1,x,g,e,S2,A1) is Relation-like the carrier of x -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (g . S2), the Sorts of (g . A1)

(S1,x,g,e,A1,A2) is Relation-like the carrier of x -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (g . A1), the Sorts of (g . A2)

(S1,x,g,e,A1,A2) ** (S1,x,g,e,S2,A1) is Relation-like the carrier of x -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (g . S2), the Sorts of (g . A2)

(S1,x,g,e,S2,A2) is Relation-like the carrier of x -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (g . S2), the Sorts of (g . A2)

e . (A1,S2) is set

[A1,S2] is V15() set

{A1,S2} is non empty set

{A1} is non empty set

{{A1,S2},{A1}} is non empty set

e . [A1,S2] is Relation-like Function-like set

e . (A2,A1) is set

[A2,A1] is V15() set

{A2,A1} is non empty set

{A2} is non empty set

{{A2,A1},{A2}} is non empty set

e . [A2,A1] is Relation-like Function-like set

e . (A2,S2) is set

[A2,S2] is V15() set

{A2,S2} is non empty set

{{A2,S2},{A2}} is non empty set

e . [A2,S2] is Relation-like Function-like set

f is Relation-like the carrier of x -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (g . S2), the Sorts of (g . A1)

i is Relation-like the carrier of x -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (g . A1), the Sorts of (g . A2)

i ** f is Relation-like the carrier of x -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (g . S2), the Sorts of (g . A2)

S1 is non empty total reflexive transitive antisymmetric RelStr

the carrier of S1 is non empty set

S2 is non empty non void V56() ManySortedSign

the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]

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

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

A1 is Relation-like the carrier of S1 -defined Function-like non empty total (S1,S2)

S1 is non empty total reflexive transitive antisymmetric RelStr

the carrier of S1 is non empty set

the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]

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

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

S2 is non empty non void V56() ManySortedSign

the carrier of S2 is non empty set

A1 is Relation-like the carrier of S1 -defined Function-like non empty total (S1,S2)

A2 is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)

x is Element of the carrier of S1

A1 . x is non-empty MSAlgebra over S2

the Sorts of (A1 . x) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

g is Element of the carrier of S1

A1 . g is non-empty MSAlgebra over S2

the Sorts of (A1 . g) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,x,g) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . g)

e is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . g)

A2 . (g,x) is set

[g,x] is V15() set

{g,x} is non empty set

{g} is non empty set

{{g,x},{g}} is non empty set

A2 . [g,x] is Relation-like Function-like set

A2 . (g,g) is set

[g,g] is V15() set

{g,g} is non empty set

{{g,g},{g}} is non empty set

A2 . [g,g] is Relation-like Function-like set

f is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . g)

i is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . g), the Sorts of (A1 . g)

i ** f is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . g)

S1 is non empty total reflexive transitive antisymmetric RelStr

the carrier of S1 is non empty set

S2 is non empty non void V56() ManySortedSign

the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]

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

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

A1 is Relation-like the carrier of S1 -defined Function-like non empty total (S1,S2)

the carrier of S2 is non empty set

A2 is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)

x is set

x `1 is set

x `2 is set

e is Element of the carrier of S1

g is Element of the carrier of S1

i is Element of the carrier of S1

f is Element of the carrier of S1

A1 . f is non-empty MSAlgebra over S2

the Sorts of (A1 . f) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . f) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . f)

A1 . i is non-empty MSAlgebra over S2

the Sorts of (A1 . i) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,f,i) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . i)

(S1,S2,A1,A2,f,i) ** (id the Sorts of (A1 . f)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . i)

IFEQ (i,f,(id the Sorts of (A1 . f)),((S1,S2,A1,A2,f,i) ** (id the Sorts of (A1 . f)))) is set

j is Relation-like the InternalRel of S1 -defined Function-like total set

j . x is set

y is Element of the carrier of S1

f is Element of the carrier of S1

[y,f] is V15() set

{y,f} is non empty set

{y} is non empty set

{{y,f},{y}} is non empty set

s is set

A1 . f is non-empty MSAlgebra over S2

the Sorts of (A1 . f) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . f) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . f)

A1 . y is non-empty MSAlgebra over S2

the Sorts of (A1 . y) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,f,y) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . y)

(S1,S2,A1,A2,f,y) ** (id the Sorts of (A1 . f)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . y)

IFEQ (y,f,(id the Sorts of (A1 . f)),((S1,S2,A1,A2,f,y) ** (id the Sorts of (A1 . f)))) is set

x is set

x is Relation-like the InternalRel of S1 -defined Function-like total set

dom x is Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool the InternalRel of S1

bool the InternalRel of S1 is non empty set

g is set

x . g is set

f is Element of the carrier of S1

e is Element of the carrier of S1

[f,e] is V15() set

{f,e} is non empty set

{f} is non empty set

{{f,e},{f}} is non empty set

A1 . e is non-empty MSAlgebra over S2

the Sorts of (A1 . e) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . e) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . e), the Sorts of (A1 . e)

A1 . f is non-empty MSAlgebra over S2

the Sorts of (A1 . f) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,e,f) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . e), the Sorts of (A1 . f)

(S1,S2,A1,A2,e,f) ** (id the Sorts of (A1 . e)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . e), the Sorts of (A1 . f)

IFEQ (f,e,(id the Sorts of (A1 . e)),((S1,S2,A1,A2,e,f) ** (id the Sorts of (A1 . e)))) is set

f is Element of the carrier of S1

e is Element of the carrier of S1

i is Element of the carrier of S1

[f,e] is V15() set

{f,e} is non empty set

{f} is non empty set

{{f,e},{f}} is non empty set

j is set

g is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() set

g . j is Relation-like Function-like set

f is Element of the carrier of S1

s is Element of the carrier of S1

[f,s] is V15() set

{f,s} is non empty set

{f} is non empty set

{{f,s},{f}} is non empty set

A1 . s is non-empty MSAlgebra over S2

the Sorts of (A1 . s) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . s) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . s), the Sorts of (A1 . s)

A1 . f is non-empty MSAlgebra over S2

the Sorts of (A1 . f) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,s,f) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . s), the Sorts of (A1 . f)

(S1,S2,A1,A2,s,f) ** (id the Sorts of (A1 . s)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . s), the Sorts of (A1 . f)

IFEQ (f,s,(id the Sorts of (A1 . s)),((S1,S2,A1,A2,s,f) ** (id the Sorts of (A1 . s)))) is set

g . (f,e) is set

g . [f,e] is Relation-like Function-like set

A1 . e is non-empty MSAlgebra over S2

the Sorts of (A1 . e) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

A1 . f is non-empty MSAlgebra over S2

the Sorts of (A1 . f) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

[i,f] is V15() set

{i,f} is non empty set

{i} is non empty set

{{i,f},{i}} is non empty set

x1 is set

g . x1 is Relation-like Function-like set

OPE is Element of the carrier of S1

s is Element of the carrier of S1

[OPE,s] is V15() set

{OPE,s} is non empty set

{OPE} is non empty set

{{OPE,s},{OPE}} is non empty set

A1 . s is non-empty MSAlgebra over S2

the Sorts of (A1 . s) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . s) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . s), the Sorts of (A1 . s)

A1 . OPE is non-empty MSAlgebra over S2

the Sorts of (A1 . OPE) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,s,OPE) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . s), the Sorts of (A1 . OPE)

(S1,S2,A1,A2,s,OPE) ** (id the Sorts of (A1 . s)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . s), the Sorts of (A1 . OPE)

IFEQ (OPE,s,(id the Sorts of (A1 . s)),((S1,S2,A1,A2,s,OPE) ** (id the Sorts of (A1 . s)))) is set

g . (i,f) is set

g . [i,f] is Relation-like Function-like set

A1 . i is non-empty MSAlgebra over S2

the Sorts of (A1 . i) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

i is Element of the carrier of S1

j is Element of the carrier of S1

g . (j,i) is set

[j,i] is V15() set

{j,i} is non empty set

{j} is non empty set

{{j,i},{j}} is non empty set

g . [j,i] is Relation-like Function-like set

(S1,S2,A1,A2,i,j) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . i), the Sorts of (A1 . j)

A1 . i is non-empty MSAlgebra over S2

the Sorts of (A1 . i) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

A1 . j is non-empty MSAlgebra over S2

the Sorts of (A1 . j) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

Co is set

g . Co is Relation-like Function-like set

co is Element of the carrier of S1

y1 is Element of the carrier of S1

[co,y1] is V15() set

{co,y1} is non empty set

{co} is non empty set

{{co,y1},{co}} is non empty set

A1 . y1 is non-empty MSAlgebra over S2

the Sorts of (A1 . y1) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . y1) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . y1), the Sorts of (A1 . y1)

A1 . co is non-empty MSAlgebra over S2

the Sorts of (A1 . co) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,y1,co) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . y1), the Sorts of (A1 . co)

(S1,S2,A1,A2,y1,co) ** (id the Sorts of (A1 . y1)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . y1), the Sorts of (A1 . co)

IFEQ (co,y1,(id the Sorts of (A1 . y1)),((S1,S2,A1,A2,y1,co) ** (id the Sorts of (A1 . y1)))) is set

id the Sorts of (A1 . i) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . i), the Sorts of (A1 . i)

(S1,S2,A1,A2,i,j) ** (id the Sorts of (A1 . i)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . i), the Sorts of (A1 . j)

g . (i,e) is set

[i,e] is V15() set

{i,e} is non empty set

{{i,e},{i}} is non empty set

g . [i,e] is Relation-like Function-like set

y is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . e), the Sorts of (A1 . f)

y is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . i)

y ** y is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . e), the Sorts of (A1 . i)

id the Sorts of (A1 . f) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . f)

id the Sorts of (A1 . e) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . e), the Sorts of (A1 . e)

id the Sorts of (A1 . f) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . f)

id the Sorts of (A1 . f) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . f)

(S1,S2,A1,A2,f,i) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . i)

(S1,S2,A1,A2,f,i) ** (id the Sorts of (A1 . f)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . i)

id the Sorts of (A1 . e) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . e), the Sorts of (A1 . e)

(S1,S2,A1,A2,e,f) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . e), the Sorts of (A1 . f)

(S1,S2,A1,A2,e,f) ** (id the Sorts of (A1 . e)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . e), the Sorts of (A1 . f)

(S1,S2,A1,A2,e,i) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . e), the Sorts of (A1 . i)

i is Element of the carrier of S1

A1 . i is non-empty MSAlgebra over S2

the Sorts of (A1 . i) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . i) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . i), the Sorts of (A1 . i)

j is Element of the carrier of S1

g . (j,i) is set

[j,i] is V15() set

{j,i} is non empty set

{j} is non empty set

{{j,i},{j}} is non empty set

g . [j,i] is Relation-like Function-like set

Co is set

g . Co is Relation-like Function-like set

co is Element of the carrier of S1

y1 is Element of the carrier of S1

[co,y1] is V15() set

{co,y1} is non empty set

{co} is non empty set

{{co,y1},{co}} is non empty set

A1 . y1 is non-empty MSAlgebra over S2

the Sorts of (A1 . y1) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . y1) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . y1), the Sorts of (A1 . y1)

A1 . co is non-empty MSAlgebra over S2

the Sorts of (A1 . co) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,y1,co) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . y1), the Sorts of (A1 . co)

(S1,S2,A1,A2,y1,co) ** (id the Sorts of (A1 . y1)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . y1), the Sorts of (A1 . co)

IFEQ (co,y1,(id the Sorts of (A1 . y1)),((S1,S2,A1,A2,y1,co) ** (id the Sorts of (A1 . y1)))) is set

g . (e,f) is set

[e,f] is V15() set

{e,f} is non empty set

{e} is non empty set

{{e,f},{e}} is non empty set

g . [e,f] is Relation-like Function-like set

id the Sorts of (A1 . e) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . e), the Sorts of (A1 . e)

(S1,S2,A1,A2,e,f) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . e), the Sorts of (A1 . f)

e is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)

f is Element of the carrier of S1

A1 . f is non-empty MSAlgebra over S2

the Sorts of (A1 . f) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . f) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . f)

i is Element of the carrier of S1

e . (i,f) is set

[i,f] is V15() set

{i,f} is non empty set

{i} is non empty set

{{i,f},{i}} is non empty set

e . [i,f] is Relation-like Function-like set

A1 . i is non-empty MSAlgebra over S2

the Sorts of (A1 . i) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,f,i) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . i)

(S1,S2,A1,A2,f,i) ** (id the Sorts of (A1 . f)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . f), the Sorts of (A1 . i)

IFEQ (i,f,(id the Sorts of (A1 . f)),((S1,S2,A1,A2,f,i) ** (id the Sorts of (A1 . f)))) is set

j is set

e . j is Relation-like Function-like set

f is Element of the carrier of S1

s is Element of the carrier of S1

[f,s] is V15() set

{f,s} is non empty set

{f} is non empty set

{{f,s},{f}} is non empty set

A1 . s is non-empty MSAlgebra over S2

the Sorts of (A1 . s) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . s) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . s), the Sorts of (A1 . s)

A1 . f is non-empty MSAlgebra over S2

the Sorts of (A1 . f) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,s,f) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . s), the Sorts of (A1 . f)

(S1,S2,A1,A2,s,f) ** (id the Sorts of (A1 . s)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . s), the Sorts of (A1 . f)

IFEQ (f,s,(id the Sorts of (A1 . s)),((S1,S2,A1,A2,s,f) ** (id the Sorts of (A1 . s)))) is set

x is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)

g is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)

e is set

e `1 is set

e `2 is set

i is Element of the carrier of S1

f is Element of the carrier of S1

g . e is Relation-like Function-like set

s is Element of the carrier of S1

j is Element of the carrier of S1

g . (s,j) is set

[s,j] is V15() set

{s,j} is non empty set

{s} is non empty set

{{s,j},{s}} is non empty set

g . [s,j] is Relation-like Function-like set

[(e `1),(e `2)] is V15() set

{(e `1),(e `2)} is non empty set

{(e `1)} is non empty set

{{(e `1),(e `2)},{(e `1)}} is non empty set

x . e is Relation-like Function-like set

x . (s,j) is set

x . [s,j] is Relation-like Function-like set

A1 . j is non-empty MSAlgebra over S2

the Sorts of (A1 . j) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . j) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . j), the Sorts of (A1 . j)

A1 . s is non-empty MSAlgebra over S2

the Sorts of (A1 . s) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,j,s) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . j), the Sorts of (A1 . s)

(S1,S2,A1,A2,j,s) ** (id the Sorts of (A1 . j)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . j), the Sorts of (A1 . s)

IFEQ (s,j,(id the Sorts of (A1 . j)),((S1,S2,A1,A2,j,s) ** (id the Sorts of (A1 . j)))) is set

S1 is non empty total reflexive transitive antisymmetric RelStr

the carrier of S1 is non empty set

the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]

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

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

S2 is non empty non void V56() ManySortedSign

A1 is Relation-like the carrier of S1 -defined Function-like non empty total (S1,S2)

A2 is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)

(S1,S2,A1,A2) is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)

x is Element of the carrier of S1

g is Element of the carrier of S1

A2 . (g,x) is set

[g,x] is V15() set

{g,x} is non empty set

{g} is non empty set

{{g,x},{g}} is non empty set

A2 . [g,x] is Relation-like Function-like set

(S1,S2,A1,A2) . (g,x) is set

(S1,S2,A1,A2) . [g,x] is Relation-like Function-like set

the carrier of S2 is non empty set

A1 . x is non-empty MSAlgebra over S2

the Sorts of (A1 . x) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . x) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . x)

A1 . g is non-empty MSAlgebra over S2

the Sorts of (A1 . g) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,x,g) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . g)

(S1,S2,A1,A2,x,g) ** (id the Sorts of (A1 . x)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . g)

IFEQ (g,x,(id the Sorts of (A1 . x)),((S1,S2,A1,A2,x,g) ** (id the Sorts of (A1 . x)))) is set

S1 is non empty total reflexive transitive antisymmetric RelStr

the carrier of S1 is non empty set

S2 is non empty non void V56() ManySortedSign

the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]

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

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

A1 is Relation-like the carrier of S1 -defined Function-like non empty total (S1,S2)

A2 is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)

(S1,S2,A1,A2) is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)

x is Element of the carrier of S1

(S1,S2,A1,A2) . (x,x) is set

[x,x] is V15() set

{x,x} is non empty set

{x} is non empty set

{{x,x},{x}} is non empty set

(S1,S2,A1,A2) . [x,x] is Relation-like Function-like set

the carrier of S2 is non empty set

A1 . x is non-empty MSAlgebra over S2

the Sorts of (A1 . x) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . x) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . x)

(S1,S2,A1,A2,x,x) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . x)

(S1,S2,A1,A2,x,x) ** (id the Sorts of (A1 . x)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . x)

IFEQ (x,x,(id the Sorts of (A1 . x)),((S1,S2,A1,A2,x,x) ** (id the Sorts of (A1 . x)))) is set

S1 is non empty total reflexive transitive antisymmetric RelStr

the carrier of S1 is non empty set

S2 is non empty non void V56() ManySortedSign

the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]

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

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

A1 is Relation-like the carrier of S1 -defined Function-like non empty total (S1,S2)

the Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1) is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)

(S1,S2,A1, the Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)) is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1) (S1,S2,A1)

S1 is non empty total reflexive transitive antisymmetric RelStr

the carrier of S1 is non empty set

the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]

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

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

S2 is non empty non void V56() ManySortedSign

A1 is Relation-like the carrier of S1 -defined Function-like non empty total (S1,S2)

A2 is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1) (S1,S2,A1)

(S1,S2,A1,A2) is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1) (S1,S2,A1)

x is Element of the carrier of S1

g is Element of the carrier of S1

(S1,S2,A1,A2) . (g,x) is set

[g,x] is V15() set

{g,x} is non empty set

{g} is non empty set

{{g,x},{g}} is non empty set

(S1,S2,A1,A2) . [g,x] is Relation-like Function-like set

A2 . (g,x) is set

A2 . [g,x] is Relation-like Function-like set

the carrier of S2 is non empty set

A1 . x is non-empty MSAlgebra over S2

the Sorts of (A1 . x) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

id the Sorts of (A1 . x) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . x)

A1 . g is non-empty MSAlgebra over S2

the Sorts of (A1 . g) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,x,g) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . g)

(S1,S2,A1,A2,x,g) ** (id the Sorts of (A1 . x)) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . x), the Sorts of (A1 . g)

IFEQ (g,x,(id the Sorts of (A1 . x)),((S1,S2,A1,A2,x,g) ** (id the Sorts of (A1 . x)))) is set

S1 is non empty total reflexive transitive antisymmetric RelStr

the carrier of S1 is non empty set

S2 is non empty non void V56() ManySortedSign

the InternalRel of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued total quasi_total reflexive antisymmetric transitive Element of bool [: the carrier of S1, the carrier of S1:]

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

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

A1 is Relation-like the carrier of S1 -defined Function-like non empty total (S1,S2)

product A1 is strict non-empty MSAlgebra over S2

the carrier of S2 is non empty set

SORTS A1 is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

A2 is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)

{ b

( not b

g is Relation-like the carrier of S2 -defined Function-like non empty total set

e is set

g . e is set

(SORTS A1) . e is set

f is Element of the carrier of S2

Carrier (A1,f) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

product (Carrier (A1,f)) is functional non empty with_common_domain product-like set

{ b

(SORTS A1) . f is functional non empty set

the Sorts of (product A1) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

e is Relation-like the carrier of S2 -defined Function-like non empty total ManySortedSubset of SORTS A1

the carrier' of S2 is non empty set

f is Relation-like the carrier of S2 -defined Function-like non empty total ManySortedSubset of the Sorts of (product A1)

i is Element of the carrier' of S2

Result (i,(product A1)) is non empty Element of proj2 the Sorts of (product A1)

proj2 the Sorts of (product A1) is non empty V108() set

Args (i,(product A1)) is functional non empty Element of proj2 ( the Sorts of (product A1) #)

the Sorts of (product A1) # is Relation-like the carrier of S2 * -defined Function-like non empty total set

the carrier of S2 * is functional non empty FinSequence-membered M8( the carrier of S2)

proj2 ( the Sorts of (product A1) #) is non empty set

Den (i,(product A1)) is Relation-like Args (i,(product A1)) -defined Result (i,(product A1)) -valued Function-like non empty total quasi_total Element of bool [:(Args (i,(product A1))),(Result (i,(product A1))):]

[:(Args (i,(product A1))),(Result (i,(product A1))):] is Relation-like non empty set

bool [:(Args (i,(product A1))),(Result (i,(product A1))):] is non empty set

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

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

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

f # is Relation-like the carrier of S2 * -defined Function-like non empty total set

the Arity of S2 * (f #) is Relation-like the carrier' of S2 -defined Function-like non empty total set

( the Arity of S2 * (f #)) . i is set

(Den (i,(product A1))) | (( the Arity of S2 * (f #)) . i) is Relation-like Args (i,(product A1)) -defined ( the Arity of S2 * (f #)) . i -defined Args (i,(product A1)) -defined Result (i,(product A1)) -valued Function-like Element of bool [:(Args (i,(product A1))),(Result (i,(product A1))):]

rng ((Den (i,(product A1))) | (( the Arity of S2 * (f #)) . i)) is Element of bool (Result (i,(product A1)))

bool (Result (i,(product A1))) is non empty set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of S2, the carrier of S2:]

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

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

the ResultSort of S2 * f is Relation-like the carrier' of S2 -defined Function-like non empty total set

( the ResultSort of S2 * f) . i is set

f is set

dom the Arity of S2 is non empty Element of bool the carrier' of S2

bool the carrier' of S2 is non empty set

s is Relation-like Function-like set

proj1 s is set

y is set

s . y is set

dom (Den (i,(product A1))) is functional non empty Element of bool (Args (i,(product A1)))

bool (Args (i,(product A1))) is non empty set

(dom (Den (i,(product A1)))) /\ (( the Arity of S2 * (f #)) . i) is functional Element of bool (Args (i,(product A1)))

the Arity of S2 . i is Relation-like K138() -defined Function-like V28() countable FinSequence-like FinSubsequence-like Element of the carrier of S2 *

(f #) . ( the Arity of S2 . i) is set

the_arity_of i is Relation-like K138() -defined the carrier of S2 -valued Function-like V28() countable FinSequence-like FinSubsequence-like Element of the carrier of S2 *

(f #) . (the_arity_of i) is set

j is Relation-like the carrier of S2 -defined Function-like non empty total set

(the_arity_of i) * j is Relation-like K138() -defined Function-like set

product ((the_arity_of i) * j) is functional with_common_domain product-like set

dom the ResultSort of S2 is non empty Element of bool the carrier' of S2

the ResultSort of S2 * the Sorts of (product A1) is Relation-like non-empty non empty-yielding the carrier' of S2 -defined Function-like non empty total set

( the ResultSort of S2 * the Sorts of (product A1)) . i is non empty set

the ResultSort of S2 . i is Element of the carrier of S2

the Sorts of (product A1) . ( the ResultSort of S2 . i) is non empty set

(SORTS A1) . ( the ResultSort of S2 . i) is functional non empty set

the_result_sort_of i is Element of the carrier of S2

(SORTS A1) . (the_result_sort_of i) is functional non empty set

Carrier (A1,(the_result_sort_of i)) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

product (Carrier (A1,(the_result_sort_of i))) is functional non empty with_common_domain product-like set

x1 is Relation-like Function-like set

(SORTS A1) # is Relation-like the carrier of S2 * -defined Function-like non empty total set

the Arity of S2 * ((SORTS A1) #) is Relation-like the carrier' of S2 -defined Function-like non empty total set

the ResultSort of S2 * (SORTS A1) is Relation-like non-empty non empty-yielding the carrier' of S2 -defined Function-like non empty total set

OPS A1 is Relation-like the carrier' of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of S2 * ((SORTS A1) #), the ResultSort of S2 * (SORTS A1)

(OPS A1) . i is Relation-like ( the Arity of S2 * ((SORTS A1) #)) . i -defined ( the ResultSort of S2 * (SORTS A1)) . i -valued Function-like total quasi_total Element of bool [:(( the Arity of S2 * ((SORTS A1) #)) . i),(( the ResultSort of S2 * (SORTS A1)) . i):]

( the Arity of S2 * ((SORTS A1) #)) . i is set

( the ResultSort of S2 * (SORTS A1)) . i is non empty set

[:(( the Arity of S2 * ((SORTS A1) #)) . i),(( the ResultSort of S2 * (SORTS A1)) . i):] is Relation-like set

bool [:(( the Arity of S2 * ((SORTS A1) #)) . i),(( the ResultSort of S2 * (SORTS A1)) . i):] is non empty set

the Arity of S2 * ( the Sorts of (product A1) #) is Relation-like the carrier' of S2 -defined Function-like non empty total set

the Charact of (product A1) is Relation-like the carrier' of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of S2 * ( the Sorts of (product A1) #), the ResultSort of S2 * the Sorts of (product A1)

the Charact of (product A1) . i is Relation-like ( the Arity of S2 * ( the Sorts of (product A1) #)) . i -defined ( the ResultSort of S2 * the Sorts of (product A1)) . i -valued Function-like total quasi_total Element of bool [:(( the Arity of S2 * ( the Sorts of (product A1) #)) . i),(( the ResultSort of S2 * the Sorts of (product A1)) . i):]

( the Arity of S2 * ( the Sorts of (product A1) #)) . i is set

[:(( the Arity of S2 * ( the Sorts of (product A1) #)) . i),(( the ResultSort of S2 * the Sorts of (product A1)) . i):] is Relation-like set

bool [:(( the Arity of S2 * ( the Sorts of (product A1) #)) . i),(( the ResultSort of S2 * the Sorts of (product A1)) . i):] is non empty set

i is Element of the carrier of S1

A1 . i is non-empty MSAlgebra over S2

the Sorts of (A1 . i) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

x1 . i is set

j is Element of the carrier of S1

A1 . j is non-empty MSAlgebra over S2

the Sorts of (A1 . j) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(S1,S2,A1,A2,i,j) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . i), the Sorts of (A1 . j)

(S1,S2,A1,A2,i,j) . (the_result_sort_of i) is Relation-like the Sorts of (A1 . i) . (the_result_sort_of i) -defined the Sorts of (A1 . j) . (the_result_sort_of i) -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (A1 . i) . (the_result_sort_of i)),( the Sorts of (A1 . j) . (the_result_sort_of i)):]

the Sorts of (A1 . i) . (the_result_sort_of i) is non empty set

the Sorts of (A1 . j) . (the_result_sort_of i) is non empty set

[:( the Sorts of (A1 . i) . (the_result_sort_of i)),( the Sorts of (A1 . j) . (the_result_sort_of i)):] is Relation-like non empty set

bool [:( the Sorts of (A1 . i) . (the_result_sort_of i)),( the Sorts of (A1 . j) . (the_result_sort_of i)):] is non empty set

((S1,S2,A1,A2,i,j) . (the_result_sort_of i)) . (x1 . i) is set

x1 . j is set

y is Relation-like Function-like set

commute y is Relation-like Function-like Function-yielding V42() set

(commute y) . i is Relation-like Function-like set

proj1 y is set

dom ((the_arity_of i) * j) is countable Element of bool K138()

rng (the_arity_of i) is Element of bool the carrier of S2

bool the carrier of S2 is non empty set

dom j is non empty Element of bool the carrier of S2

co is set

dom (the_arity_of i) is countable Element of bool K138()

len (the_arity_of i) is V21() V22() V23() V27() Element of K138()

Seg (len (the_arity_of i)) is V28() V35( len (the_arity_of i)) countable Element of bool K138()

proj2 y is set

|.A1.| is non empty set

Funcs ( the carrier of S1,|.A1.|) is functional non empty FUNCTION_DOMAIN of the carrier of S1,|.A1.|

co is set

E is set

y . E is set

(the_arity_of i) . E is set

(the_arity_of i) /. E is Element of the carrier of S2

((the_arity_of i) * j) . E is set

j . ((the_arity_of i) . E) is set

F is Element of the carrier of S2

Carrier (A1,F) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

product (Carrier (A1,F)) is functional non empty with_common_domain product-like set

{ b

( not b

y2 is Relation-like the carrier of S1 -defined Function-like Carrier (A1,F) -compatible non empty total Element of product (Carrier (A1,F))

g is Relation-like Function-like set

proj1 g is set

dom (Carrier (A1,F)) is non empty Element of bool the carrier of S1

bool the carrier of S1 is non empty set

y2 is Relation-like the carrier of S1 -defined Function-like Carrier (A1,F) -compatible non empty total Element of product (Carrier (A1,F))

proj2 g is set

y2 is set

Two is set

g . Two is set

n is Element of the carrier of S1

yn is Element of the carrier of S1

A1 . Two is set

(Carrier (A1,F)) . Two is set

A1 . yn is non-empty MSAlgebra over S2

|.(A1 . yn).| is non empty set

{ |.(A1 . b

union { |.(A1 . b

the Sorts of (A1 . yn) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

dom the Sorts of (A1 . yn) is non empty Element of bool the carrier of S2

the Sorts of (A1 . yn) . F is non empty set

proj2 the Sorts of (A1 . yn) is non empty V108() set

Pi is Relation-like the carrier of S1 -defined Function-like Carrier (A1,F) -compatible non empty total Element of product (Carrier (A1,F))

Pi is Relation-like the carrier of S1 -defined Function-like Carrier (A1,F) -compatible non empty total Element of product (Carrier (A1,F))

union (proj2 the Sorts of (A1 . yn)) is set

Pi is MSAlgebra over S2

the Sorts of Pi is Relation-like the carrier of S2 -defined Function-like non empty total set

the Sorts of Pi . F is set

Funcs ((Seg (len (the_arity_of i))),(Funcs ( the carrier of S1,|.A1.|))) is functional non empty FUNCTION_DOMAIN of Seg (len (the_arity_of i)), Funcs ( the carrier of S1,|.A1.|)

A1 ?. i is Relation-like the carrier of S1 -defined Function-like non empty total Function-yielding V42() set

doms (A1 ?. i) is Relation-like Function-like set

proj1 (doms (A1 ?. i)) is set

Co is Relation-like Function-like set

co is set

Co . co is set

(doms (A1 ?. i)) . co is set

E is Element of the carrier of S1

Co . E is set

Funcs ((Seg (len (the_arity_of i))),|.A1.|) is functional non empty FUNCTION_DOMAIN of Seg (len (the_arity_of i)),|.A1.|

Funcs ( the carrier of S1,(Funcs ((Seg (len (the_arity_of i))),|.A1.|))) is functional non empty FUNCTION_DOMAIN of the carrier of S1, Funcs ((Seg (len (the_arity_of i))),|.A1.|)

A1 . E is non-empty MSAlgebra over S2

the Sorts of (A1 . E) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set

(the_arity_of i) * the Sorts of (A1 . E) is Relation-like non-empty K138() -defined Function-like set

product ((the_arity_of i) * the Sorts of (A1 . E)) is functional non empty with_common_domain product-like set

dom ((the_arity_of i) * the Sorts of (A1 . E)) is countable Element of bool K138()

F is Relation-like Function-like set

commute (commute y) is Relation-like Function-like Function-yielding V42() set

g is set

F . g is set

((the_arity_of i) * the Sorts of (A1 . E)) . g is set

(the_arity_of i) /. g is Element of the carrier of S2

Carrier (A1,((the_arity_of i) /. g)) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

dom (Carrier (A1,((the_arity_of i) /. g))) is non empty Element of bool the carrier of S1

bool the carrier of S1 is non empty set

y . g is set

((the_arity_of i) * j) . g is set

(the_arity_of i) . g is set

j . ((the_arity_of i) . g) is set

Two is Relation-like Function-like Function-yielding V42() set

Two . g is Relation-like Function-like set

j . ((the_arity_of i) /. g) is set

n is Relation-like Function-like set

y2 is Element of the carrier of S2

Carrier (A1,y2) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

product (Carrier (A1,y2)) is functional non empty with_common_domain product-like set

{ b

( not b

n . E is set

(Carrier (A1,((the_arity_of i) /. g))) . E is non empty set

yn is Relation-like the carrier of S1 -defined Function-like Carrier (A1,y2) -compatible non empty total Element of product (Carrier (A1,y2))

the Sorts of (A1 . E) . ((the_arity_of i) . g) is set

yn is MSAlgebra over S2

the Sorts of yn is Relation-like the carrier of S2 -defined Function-like non empty total set

the Sorts of yn . ((the_arity_of i) /. g) is set

proj2 Co is set

g is Relation-like Function-like set

proj1 g is set

proj2 g is set

g is Relation-like Function-like set

proj1 g is set

proj2 g is set

g is Relation-like Function-like set

proj1 g is set

proj2 g is set

(doms (A1 ?. i)) . E is set

Args (i,(A1 . E)) is functional non empty Element of proj2 ( the Sorts of (A1 . E) #)

the Sorts of (A1 . E) # is Relation-like the carrier of S2 * -defined Function-like non empty total set

proj2 ( the Sorts of (A1 . E) #) is non empty set

product (doms (A1 ?. i)) is functional with_common_domain product-like set

Funcs ((Seg (len (the_arity_of i))),|.A1.|) is functional non empty FUNCTION_DOMAIN of Seg (len (the_arity_of i)),|.A1.|

Funcs ( the carrier of S1,(Funcs ((Seg (len (the_arity_of i))),|.A1.|))) is functional non empty FUNCTION_DOMAIN of the carrier of S1, Funcs ((Seg (len (the_arity_of i))),|.A1.|)

proj1 Co is set

co is Relation-like Function-like set

proj1 co is set

proj2 co is set

OPE is Relation-like Function-like set

commute (A1 ?. i) is Relation-like Function-like Function-yielding V42() set

Frege (A1 ?. i) is Relation-like product (doms (A1 ?. i)) -defined Function-like total Function-yielding V42() set

Commute (Frege (A1 ?. i)) is Relation-like Function-like set

IFEQ ((the_arity_of i),{},(commute (A1 ?. i)),(Commute (Frege (A1 ?. i)))) is set

proj1 (Commute (Frege (A1 ?. i))) is set

dom (A1 ?. i) is non empty Element of bool the carrier of S1

bool the carrier of S1 is non empty set

OPE . y is set

(Commute (Frege (A1 ?. i))) . y is set

(Frege (A1 ?. i)) . (commute y) is Relation-like Function-like set

(A1 ?. i) .. (commute y) is Relation-like Function-like set

(A1 ?. i) . i is Relation-like Function-like set

((A1 ?. i) . i) . ((commute y) . i) is set

Den (i,(A1 . i)) is Relation-like Args (i,(A1 . i)) -defined Result (i,(A1 . i)) -valued Function-like non empty total quasi_total Element of bool [:(Args (i,(A1 . i))),(Result (i,(A1 . i))):]

Args (i,(A1 . i)) is functional non empty Element of proj2 ( the Sorts of (A1 . i) #)

the Sorts of (A1 . i) # is Relation-like the carrier of S2 * -defined Function-like non empty total set

proj2 ( the Sorts of (A1 . i) #) is non empty set

Result (i,(A1 . i)) is non empty Element of proj2 the Sorts of (A1 . i)

proj2 the Sorts of (A1 . i) is non empty V108() set

[:(Args (i,(A1 . i))),(Result (i,(A1 . i))):] is Relation-like non empty set

bool [:(Args (i,(A1 . i))),(Result (i,(A1 . i))):] is non empty set

co is Relation-like Function-like set

(Den (i,(A1 . i))) . co is set

Funcs ((Seg (len (the_arity_of i))),|.A1.|) is functional non empty FUNCTION_DOMAIN of Seg (len (the_arity_of i)),|.A1.|

Funcs ( the carrier of S1,(Funcs ((Seg (len (the_arity_of i))),|.A1.|))) is functional non empty FUNCTION_DOMAIN of the carrier of S1, Funcs ((Seg (len (the_arity_of i))),|.A1.|)

(the_arity_of i) * the Sorts of (A1 . i) is Relation-like non-empty K138() -defined Function-like set

product ((the_arity_of i) * the Sorts of (A1 . i)) is functional non empty with_common_domain product-like set

dom ((the_arity_of i) * the Sorts of (A1 . i)) is countable Element of bool K138()

commute (commute y) is Relation-like Function-like Function-yielding V42() set

E is set

co . E is set

((the_arity_of i) * the Sorts of (A1 . i)) . E is set

(the_arity_of i) /. E is Element of the carrier of S2

Carrier (A1,((the_arity_of i) /. E)) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

dom (Carrier (A1,((the_arity_of i) /. E))) is non empty Element of bool the carrier of S1

y . E is set

((the_arity_of i) * j) . E is set

(the_arity_of i) . E is set

j . ((the_arity_of i) . E) is set

g is Relation-like Function-like Function-yielding V42() set

g . E is Relation-like Function-like set

j . ((the_arity_of i) /. E) is set

y2 is Relation-like Function-like set

F is Element of the carrier of S2

Carrier (A1,F) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

product (Carrier (A1,F)) is functional non empty with_common_domain product-like set

{ b

( not b

y2 . i is set

(Carrier (A1,((the_arity_of i) /. E))) . i is non empty set

Two is Relation-like the carrier of S1 -defined Function-like Carrier (A1,F) -compatible non empty total Element of product (Carrier (A1,F))

the Sorts of (A1 . i) . ((the_arity_of i) . E) is set

Two is MSAlgebra over S2

the Sorts of Two is Relation-like the carrier of S2 -defined Function-like non empty total set

the Sorts of Two . ((the_arity_of i) /. E) is set

Co . i is set

proj2 Co is set

E is Relation-like Function-like set

proj1 E is set

proj2 E is set

E is Relation-like Function-like set

proj1 E is set

proj2 E is set

E is Relation-like Function-like set

proj1 E is set

proj2 E is set

E is Relation-like Function-like Element of Args (i,(A1 . i))

(S1,S2,A1,A2,i,j) # E is Relation-like Function-like Element of Args (i,(A1 . j))

Args (i,(A1 . j)) is functional non empty Element of proj2 ( the Sorts of (A1 . j) #)

the Sorts of (A1 . j) # is Relation-like the carrier of S2 * -defined Function-like non empty total set

proj2 ( the Sorts of (A1 . j) #) is non empty set

(commute y) . j is Relation-like Function-like set

proj1 ((S1,S2,A1,A2,i,j) # E) is set

commute (commute y) is Relation-like Function-like Function-yielding V42() set

g is Relation-like Function-like Function-yielding V42() set

commute g is Relation-like Function-like Function-yielding V42() set

(commute g) . j is Relation-like Function-like set

Co . j is set

proj2 Co is set

Two is Relation-like Function-like set

proj1 Two is set

proj2 Two is set

Two is Relation-like Function-like set

proj1 Two is set

proj2 Two is set

y2 is Relation-like Function-like set

n is Relation-like Function-like set

proj1 n is set

proj2 n is set

Co . i is set

n is Relation-like Function-like set

proj1 n is set

proj2 n is set

n is V21() V22() V23() V27() set

g . n is Relation-like Function-like set

(the_arity_of i) /. n is Element of the carrier of S2

c

proj1 c

proj2 c

proj1 y2 is set

((the_arity_of i) * j) . n is set

c

proj1 c

proj2 c

c

proj1 c

proj2 c

(the_arity_of i) . n is set

yn is Relation-like Function-like set

Pi is Element of the carrier of S2

j . Pi is set

Carrier (A1,Pi) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

product (Carrier (A1,Pi)) is functional non empty with_common_domain product-like set

{ b

( not b

E . n is set

yn . i is set

c

proj1 c

proj2 c

((S1,S2,A1,A2,i,j) # E) . n is set

(S1,S2,A1,A2,i,j) . ((the_arity_of i) /. n) is Relation-like the Sorts of (A1 . i) . ((the_arity_of i) /. n) -defined the Sorts of (A1 . j) . ((the_arity_of i) /. n) -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (A1 . i) . ((the_arity_of i) /. n)),( the Sorts of (A1 . j) . ((the_arity_of i) /. n)):]

the Sorts of (A1 . i) . ((the_arity_of i) /. n) is non empty set

the Sorts of (A1 . j) . ((the_arity_of i) /. n) is non empty set

[:( the Sorts of (A1 . i) . ((the_arity_of i) /. n)),( the Sorts of (A1 . j) . ((the_arity_of i) /. n)):] is Relation-like non empty set

bool [:( the Sorts of (A1 . i) . ((the_arity_of i) /. n)),( the Sorts of (A1 . j) . ((the_arity_of i) /. n)):] is non empty set

((S1,S2,A1,A2,i,j) . ((the_arity_of i) /. n)) . (yn . i) is set

yn . j is set

c

proj1 c

proj2 c

c

proj1 c

proj2 c

c

y2 . n is set

c

proj1 c

proj2 c

F is Relation-like K138() -defined Function-like V28() countable FinSequence-like FinSubsequence-like set

Two is Relation-like K138() -defined Function-like V28() countable FinSequence-like FinSubsequence-like set

n is V21() V22() V23() V27() set

F . n is set

Two . n is set

yn is Relation-like Function-like set

proj1 yn is set

proj2 yn is set

n is Relation-like Function-like set

proj1 n is set

proj2 n is set

Result (i,(A1 . j)) is non empty Element of proj2 the Sorts of (