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

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

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

A2 is Element of the carrier of S2
(SORTS A1) . A2 is non empty set

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

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

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

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,i) is set
[s,i] is V15() set
{s,i} is non empty set
{{s,i},{s}} is non empty 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)

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)

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

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

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)

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)

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 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,g) is set
[g,g] is V15() set
{g,g} is non empty set
{{g,g},{g}} is non empty 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)

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

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

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

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

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

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

(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

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

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

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

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

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

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

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

[(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 . (s,j) is 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

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

(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

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

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)

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

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

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

A2 is Relation-like the InternalRel of S1 -defined Function-like total Function-yielding V42() (S1,S2,A1)
{ b1 where b1 is Relation-like the carrier of S1 -defined Function-like Carrier (A1,a1) -compatible non empty total Element of product (Carrier (A1,a1)) : for b2, b3 being Element of the carrier of S1 holds
( not b3 <= b2 or ((S1,S2,A1,A2,b2,b3) . a1) . (b1 . b2) = b1 . b3 )
}
is 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

{ b1 where b1 is Relation-like the carrier of S1 -defined Function-like Carrier (A1,f) -compatible non empty total Element of product (Carrier (A1,f)) : S1[b1] } is set
(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

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

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

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

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

(f #) . () is 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) . is functional non empty 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) . is Relation-like the Sorts of (A1 . i) . -defined the Sorts of (A1 . j) . -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (A1 . i) . ),( the Sorts of (A1 . j) . ):]
the Sorts of (A1 . i) . is non empty set
the Sorts of (A1 . j) . is non empty set
[:( the Sorts of (A1 . i) . ),( the Sorts of (A1 . j) . ):] is Relation-like non empty set
bool [:( the Sorts of (A1 . i) . ),( the Sorts of (A1 . j) . ):] is non empty set
((S1,S2,A1,A2,i,j) . ) . (x1 . i) is set
x1 . j is set

proj1 y is set
dom (() * j) is countable Element of bool K138()
rng () 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 () is countable Element of bool K138()
len () is V21() V22() V23() V27() Element of K138()
Seg (len ()) is V28() V35( len ()) 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
() . E is set
() /. E is Element of the carrier of S2
(() * j) . E is set
j . (() . 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

{ b1 where b1 is Relation-like the carrier of S1 -defined Function-like Carrier (A1,F) -compatible non empty total Element of product (Carrier (A1,F)) : for b2, b3 being Element of the carrier of S1 holds
( not b3 <= b2 or ((S1,S2,A1,A2,b2,b3) . F) . (b1 . b2) = b1 . b3 )
}
is 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))

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 . b1).| where b1 is Element of the carrier of S1 : verum } is set
union { |.(A1 . b1).| where b1 is Element of the carrier of S1 : verum } is set
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 ())),(Funcs ( the carrier of S1,|.A1.|))) is functional non empty FUNCTION_DOMAIN of Seg (len ()), Funcs ( the carrier of S1,|.A1.|)

doms (A1 ?. i) is Relation-like Function-like set
proj1 (doms (A1 ?. i)) is 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 ())),|.A1.|) is functional non empty FUNCTION_DOMAIN of Seg (len ()),|.A1.|
Funcs ( the carrier of S1,(Funcs ((Seg (len ())),|.A1.|))) is functional non empty FUNCTION_DOMAIN of the carrier of S1, Funcs ((Seg (len ())),|.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 Sorts of (A1 . E) is Relation-like non-empty K138() -defined Function-like set
product (() * the Sorts of (A1 . E)) is functional non empty with_common_domain product-like set
dom (() * the Sorts of (A1 . E)) is countable Element of bool K138()

g is set
F . g is set
(() * the Sorts of (A1 . E)) . g is set
() /. g is Element of the carrier of S2
Carrier (A1,(() /. g)) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set
dom (Carrier (A1,(() /. g))) is non empty Element of bool the carrier of S1
bool the carrier of S1 is non empty set
y . g is set
(() * j) . g is set
() . g is set
j . (() . g) is set

j . (() /. g) is 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

{ b1 where b1 is Relation-like the carrier of S1 -defined Function-like Carrier (A1,y2) -compatible non empty total Element of product (Carrier (A1,y2)) : for b2, b3 being Element of the carrier of S1 holds
( not b3 <= b2 or ((S1,S2,A1,A2,b2,b3) . y2) . (b1 . b2) = b1 . b3 )
}
is set

n . E is set
(Carrier (A1,(() /. 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) . (() . 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 . (() /. g) is set
proj2 Co is set

proj1 g is set
proj2 g is set

proj1 g is set
proj2 g is 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

Funcs ((Seg (len ())),|.A1.|) is functional non empty FUNCTION_DOMAIN of Seg (len ()),|.A1.|
Funcs ( the carrier of S1,(Funcs ((Seg (len ())),|.A1.|))) is functional non empty FUNCTION_DOMAIN of the carrier of S1, Funcs ((Seg (len ())),|.A1.|)
proj1 Co is set

proj1 co is set
proj2 co is 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 ((),{},(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)) . () is Relation-like Function-like set
(A1 ?. i) .. () is Relation-like Function-like set
(A1 ?. i) . i is Relation-like Function-like set
((A1 ?. i) . i) . (() . 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

(Den (i,(A1 . i))) . co is set
Funcs ((Seg (len ())),|.A1.|) is functional non empty FUNCTION_DOMAIN of Seg (len ()),|.A1.|
Funcs ( the carrier of S1,(Funcs ((Seg (len ())),|.A1.|))) is functional non empty FUNCTION_DOMAIN of the carrier of S1, Funcs ((Seg (len ())),|.A1.|)
() * the Sorts of (A1 . i) is Relation-like non-empty K138() -defined Function-like set
product (() * the Sorts of (A1 . i)) is functional non empty with_common_domain product-like set
dom (() * the Sorts of (A1 . i)) is countable Element of bool K138()

E is set
co . E is set
(() * the Sorts of (A1 . i)) . E is set
() /. E is Element of the carrier of S2
Carrier (A1,(() /. E)) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set
dom (Carrier (A1,(() /. E))) is non empty Element of bool the carrier of S1
y . E is set
(() * j) . E is set
() . E is set
j . (() . E) is set

j . (() /. 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

{ b1 where b1 is Relation-like the carrier of S1 -defined Function-like Carrier (A1,F) -compatible non empty total Element of product (Carrier (A1,F)) : for b2, b3 being Element of the carrier of S1 holds
( not b3 <= b2 or ((S1,S2,A1,A2,b2,b3) . F) . (b1 . b2) = b1 . b3 )
}
is set

y2 . i is set
(Carrier (A1,(() /. 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) . (() . 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 . (() /. E) is set
Co . i is set
proj2 Co is set

proj1 E is set
proj2 E is set

proj1 E is set
proj2 E is 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

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

Co . j is set
proj2 Co is set

proj1 Two is set
proj2 Two is set

proj1 Two is set
proj2 Two is set

proj1 n is set
proj2 n is set
Co . i is set

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

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

proj1 c31 is set
proj2 c31 is set
proj1 y2 is set
(() * j) . n is set

proj1 c31 is set
proj2 c31 is set

proj1 c31 is set
proj2 c31 is set
() . n is 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

{ b1 where b1 is Relation-like the carrier of S1 -defined Function-like Carrier (A1,Pi) -compatible non empty total Element of product (Carrier (A1,Pi)) : for b2, b3 being Element of the carrier of S1 holds
( not b3 <= b2 or ((S1,S2,A1,A2,b2,b3) . Pi) . (b1 . b2) = b1 . b3 )
}
is set

E . n is set
yn . i is set

proj1 c31 is set
proj2 c31 is set
((S1,S2,A1,A2,i,j) # E) . n is set
(S1,S2,A1,A2,i,j) . (() /. n) is Relation-like the Sorts of (A1 . i) . (() /. n) -defined the Sorts of (A1 . j) . (() /. n) -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (A1 . i) . (() /. n)),( the Sorts of (A1 . j) . (() /. n)):]
the Sorts of (A1 . i) . (() /. n) is non empty set
the Sorts of (A1 . j) . (() /. n) is non empty set
[:( the Sorts of (A1 . i) . (() /. n)),( the Sorts of (A1 . j) . (() /. n)):] is Relation-like non empty set
bool [:( the Sorts of (A1 . i) . (() /. n)),( the Sorts of (A1 . j) . (() /. n)):] is non empty set
((S1,S2,A1,A2,i,j) . (() /. n)) . (yn . i) is set
yn . j is set

proj1 c31 is set
proj2 c31 is set

proj1 c32 is set
proj2 c32 is set
c31 is Relation-like the carrier of S1 -defined Function-like Carrier (A1,Pi) -compatible non empty total Element of product (Carrier (A1,Pi))
y2 . n is set

proj1 c31 is set
proj2 c31 is set

n is V21() V22() V23() V27() set
F . n is set
Two . n is set

proj1 yn is set
proj2 yn is set

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