:: 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₁ where b₁ is Relation-like the carrier of S1 -defined Function-like Carrier (A1,a₁) -compatible non empty total Element of product (Carrier (A1,a₁)) : for b₂, b₃ being Element of the carrier of S1 holds
( not b₃ <= b₂ or ((S1,S2,A1,A2,b₂,b₃) . a₁) . (b₁ . b₂) = b₁ . b₃ ) } is set
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₁ where b₁ is Relation-like the carrier of S1 -defined Function-like Carrier (A1,f) -compatible non empty total Element of product (Carrier (A1,f)) : S₁[b₁] } 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
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₁ where b₁ is Relation-like the carrier of S1 -defined Function-like Carrier (A1,F) -compatible non empty total Element of product (Carrier (A1,F)) : for b₂, b₃ being Element of the carrier of S1 holds
( not b₃ <= b₂ or ((S1,S2,A1,A2,b₂,b₃) . F) . (b₁ . b₂) = b₁ . b₃ ) } 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))
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₁).| where b₁ is Element of the carrier of S1 : verum } is set
union { |.(A1 . b₁).| where b₁ 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 (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₁ where b₁ is Relation-like the carrier of S1 -defined Function-like Carrier (A1,y2) -compatible non empty total Element of product (Carrier (A1,y2)) : for b₂, b₃ being Element of the carrier of S1 holds
( not b₃ <= b₂ or ((S1,S2,A1,A2,b₂,b₃) . y2) . (b₁ . b₂) = b₁ . b₃ ) } is set
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₁ where b₁ is Relation-like the carrier of S1 -defined Function-like Carrier (A1,F) -compatible non empty total Element of product (Carrier (A1,F)) : for b₂, b₃ being Element of the carrier of S1 holds
( not b₃ <= b₂ or ((S1,S2,A1,A2,b₂,b₃) . F) . (b₁ . b₂) = b₁ . b₃ ) } is set
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₃₁ is Relation-like Function-like set
proj1 c₃₁ is set
proj2 c₃₁ is set
proj1 y2 is set
((the_arity_of i) * j) . n is set
c₃₁ is Relation-like Function-like set
proj1 c₃₁ is set
proj2 c₃₁ is set
c₃₁ is Relation-like Function-like set
proj1 c₃₁ is set
proj2 c₃₁ is set
(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₁ where b₁ is Relation-like the carrier of S1 -defined Function-like Carrier (A1,Pi) -compatible non empty total Element of product (Carrier (A1,Pi)) : for b₂, b₃ being Element of the carrier of S1 holds
( not b₃ <= b₂ or ((S1,S2,A1,A2,b₂,b₃) . Pi) . (b₁ . b₂) = b₁ . b₃ ) } is set
E . n is set
yn . i is set
c₃₁ is Relation-like Function-like set
proj1 c₃₁ is set
proj2 c₃₁ is set
((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₃₁ is Relation-like Function-like set
proj1 c₃₁ is set
proj2 c₃₁ is set
c₃₂ is Relation-like Function-like set
proj1 c₃₂ is set
proj2 c₃₂ is set
c₃₁ 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
c₃₁ is Relation-like Function-like set
proj1 c₃₁ is set
proj2 c₃₁ is set
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 (A1 . j)
proj2 the Sorts of (A1 . j) is non empty V108() set
Den (i,(A1 . j)) is Relation-like Args (i,(A1 . j)) -defined Result (i,(A1 . j)) -valued Function-like non empty total quasi_total Element of bool [:(Args (i,(A1 . j))),(Result (i,(A1 . j))):]
[:(Args (i,(A1 . j))),(Result (i,(A1 . j))):] is Relation-like non empty set
bool [:(Args (i,(A1 . j))),(Result (i,(A1 . j))):] is non empty set
(Den (i,(A1 . j))) . ((S1,S2,A1,A2,i,j) # E) is Element of Result (i,(A1 . j))
(A1 ?. i) . j is Relation-like Function-like set
((A1 ?. i) . j) . ((commute y) . j) is set
A1 ?. i is Relation-like the carrier of S1 -defined Function-like non empty total Function-yielding V42() set
commute (A1 ?. i) is Relation-like Function-like Function-yielding V42() set
(commute (A1 ?. i)) . y is Relation-like Function-like set
{} * j 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
co is Relation-like Function-like set
uncurry (A1 ?. i) is Relation-like Function-like set
curry' (uncurry (A1 ?. i)) is Relation-like Function-like set
(curry' (uncurry (A1 ?. i))) . y is set
dom (A1 ?. i) is non empty Element of bool the carrier of S1
bool the carrier of S1 is non empty set
Frege (A1 ?. i) is Relation-like product (doms (A1 ?. i)) -defined Function-like total Function-yielding V42() set
doms (A1 ?. i) is Relation-like Function-like set
product (doms (A1 ?. i)) is functional with_common_domain product-like 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
F is Element of the carrier of S1
x1 . F is set
A1 . F is non-empty MSAlgebra over S2
Den (i,(A1 . F)) is Relation-like Args (i,(A1 . F)) -defined Result (i,(A1 . F)) -valued Function-like non empty total quasi_total Element of bool [:(Args (i,(A1 . F))),(Result (i,(A1 . F))):]
Args (i,(A1 . F)) is functional non empty Element of proj2 ( the Sorts of (A1 . F) #)
the Sorts of (A1 . F) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set
the Sorts of (A1 . F) # is Relation-like the carrier of S2 * -defined Function-like non empty total set
proj2 ( the Sorts of (A1 . F) #) is non empty set
Result (i,(A1 . F)) is non empty Element of proj2 the Sorts of (A1 . F)
proj2 the Sorts of (A1 . F) is non empty V108() set
[:(Args (i,(A1 . F))),(Result (i,(A1 . F))):] is Relation-like non empty set
bool [:(Args (i,(A1 . F))),(Result (i,(A1 . F))):] is non empty set
(Den (i,(A1 . F))) . {} is set
(A1 ?. i) . F is Relation-like Function-like set
g is Relation-like Function-like set
proj1 g is set
[F,y] is V15() set
{F,y} is non empty set
{F} is non empty set
{{F,y},{F}} is non empty set
proj1 (uncurry (A1 ?. i)) is set
co . F is set
E is Relation-like Function-like set
E . F is set
(uncurry (A1 ?. i)) . (F,y) is set
(uncurry (A1 ?. i)) . [F,y] is set
g . y is set
(Den (i,(A1 . F))) . y 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))) . {} is set
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
Result (i,(A1 . j)) is non empty Element of proj2 the Sorts of (A1 . j)
proj2 the Sorts of (A1 . j) is non empty V108() set
Den (i,(A1 . j)) is Relation-like Args (i,(A1 . j)) -defined Result (i,(A1 . j)) -valued Function-like non empty total quasi_total Element of bool [:(Args (i,(A1 . j))),(Result (i,(A1 . j))):]
[:(Args (i,(A1 . j))),(Result (i,(A1 . j))):] is Relation-like non empty set
bool [:(Args (i,(A1 . j))),(Result (i,(A1 . j))):] is non empty 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))
(Den (i,(A1 . j))) . ((S1,S2,A1,A2,i,j) # E) is Element of Result (i,(A1 . j))
(Den (i,(A1 . j))) . {} is set
{ b₁ where b₁ is Relation-like the carrier of S1 -defined Function-like Carrier (A1,(the_result_sort_of i)) -compatible non empty total Element of product (Carrier (A1,(the_result_sort_of i))) : for b₂, b₃ being Element of the carrier of S1 holds
( not b₃ <= b₂ or ((S1,S2,A1,A2,b₂,b₃) . (the_result_sort_of i)) . (b₁ . b₂) = b₁ . b₃ ) } is set
f . (the_result_sort_of i) is set
f . ( the ResultSort of S2 . i) is set
x is non-empty MSAlgebra over S2
the Sorts of x is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set
i is Relation-like the carrier of S2 -defined Function-like non empty total ManySortedSubset of the Sorts of x
x | i is strict MSSubAlgebra of x
Opers (x,i) is Relation-like the carrier' of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of S2 * (i #), the ResultSort of S2 * i
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 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
i # is Relation-like the carrier of S2 * -defined Function-like non empty total set
the Arity of S2 * (i #) 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 * i is Relation-like the carrier' of S2 -defined Function-like non empty total set
MSAlgebra(# i,(Opers (x,i)) #) is strict MSAlgebra over S2
s is Element of the carrier of S2
(SORTS A1) . s is functional non empty set
f is Relation-like Function-like Element of (SORTS A1) . s
Carrier (A1,s) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set
product (Carrier (A1,s)) is functional non empty with_common_domain product-like set
the Sorts of (x | i) is Relation-like the carrier of S2 -defined Function-like non empty total set
the Sorts of (x | i) . s is set
{ b₁ where b₁ is Relation-like the carrier of S1 -defined Function-like Carrier (A1,s) -compatible non empty total Element of product (Carrier (A1,s)) : for b₂, b₃ being Element of the carrier of S1 holds
( not b₃ <= b₂ or ((S1,S2,A1,A2,b₂,b₃) . s) . (b₁ . b₂) = b₁ . b₃ ) } is set
x1 is Element of the carrier of S1
y is Element of the carrier of S1
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
A1 . x1 is non-empty MSAlgebra over S2
the Sorts of (A1 . x1) is Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like non empty total set
(S1,S2,A1,A2,y,x1) is Relation-like the carrier of S2 -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (A1 . y), the Sorts of (A1 . x1)
(S1,S2,A1,A2,y,x1) . s is Relation-like the Sorts of (A1 . y) . s -defined the Sorts of (A1 . x1) . s -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (A1 . y) . s),( the Sorts of (A1 . x1) . s):]
the Sorts of (A1 . y) . s is non empty set
the Sorts of (A1 . x1) . s is non empty set
[:( the Sorts of (A1 . y) . s),( the Sorts of (A1 . x1) . s):] is Relation-like non empty set
bool [:( the Sorts of (A1 . y) . s),( the Sorts of (A1 . x1) . s):] is non empty set
f . y is set
((S1,S2,A1,A2,y,x1) . s) . (f . y) is set
f . x1 is set
s is Relation-like the carrier of S1 -defined Function-like Carrier (A1,s) -compatible non empty total Element of product (Carrier (A1,s))
x is strict MSSubAlgebra of product A1
the Sorts of x is Relation-like the carrier of S2 -defined Function-like non empty total set
g is strict MSSubAlgebra of product A1
the Sorts of g is Relation-like the carrier of S2 -defined Function-like non empty total set
e is set
the Sorts of x . e is set
the Sorts of g . e is set
i is 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
f is Element of the carrier of S2
the Sorts of x . f is set
(SORTS A1) . f is functional non empty set
j is Relation-like Function-like Element of (SORTS A1) . f
f is Element of the carrier of S1
s is Element of the carrier of S1
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
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) . f is Relation-like the Sorts of (A1 . s) . f -defined the Sorts of (A1 . f) . f -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (A1 . s) . f),( the Sorts of (A1 . f) . f):]
the Sorts of (A1 . s) . f is non empty set
the Sorts of (A1 . f) . f is non empty set
[:( the Sorts of (A1 . s) . f),( the Sorts of (A1 . f) . f):] is Relation-like non empty set
bool [:( the Sorts of (A1 . s) . f),( the Sorts of (A1 . f) . f):] is non empty set
j . s is set
((S1,S2,A1,A2,s,f) . f) . (j . s) is set
j . f is set
i is 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
f is Element of the carrier of S2
the Sorts of g . f is set
(SORTS A1) . f is functional non empty set
j is Relation-like Function-like Element of (SORTS A1) . f
f is Element of the carrier of S1
s is Element of the carrier of S1
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
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) . f is Relation-like the Sorts of (A1 . s) . f -defined the Sorts of (A1 . f) . f -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (A1 . s) . f),( the Sorts of (A1 . f) . f):]
the Sorts of (A1 . s) . f is non empty set
the Sorts of (A1 . f) . f is non empty set
[:( the Sorts of (A1 . s) . f),( the Sorts of (A1 . f) . f):] is Relation-like non empty set
bool [:( the Sorts of (A1 . s) . f),( the Sorts of (A1 . f) . f):] is non empty set
j . s is set
((S1,S2,A1,A2,s,f) . f) . (j . s) is set
j . f is set
S1 is non empty total reflexive transitive antisymmetric discrete 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)
product A1 is strict non-empty MSAlgebra over 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 strict MSSubAlgebra of product A1
the carrier of S2 is non empty set
the Sorts of (S1,S2,A1,A2) is Relation-like the carrier of S2 -defined Function-like non empty total 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
x is set
the Sorts of (S1,S2,A1,A2) . x is set
the Sorts of (product A1) . x is set
e is set
g is Element of the carrier of S2
the Sorts of (S1,S2,A1,A2) . g is set
the Sorts of (product A1) . g is non empty set
e is set
SORTS A1 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 S2
(SORTS A1) . g is functional non empty set
f is Relation-like Function-like Element of (SORTS A1) . g
j is Element of the carrier of S1
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
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) . g is Relation-like the Sorts of (A1 . i) . g -defined the Sorts of (A1 . j) . g -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (A1 . i) . g),( the Sorts of (A1 . j) . g):]
the Sorts of (A1 . i) . g is non empty set
the Sorts of (A1 . j) . g is non empty set
[:( the Sorts of (A1 . i) . g),( the Sorts of (A1 . j) . g):] is Relation-like non empty set
bool [:( the Sorts of (A1 . i) . g),( the Sorts of (A1 . j) . g):] is non empty set
f . i is set
((S1,S2,A1,A2,i,j) . g) . (f . i) is set
f . j is set
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
product (Carrier (A1,g)) is functional non empty with_common_domain product-like set
(Carrier (A1,g)) . i is non empty set
(S1,S2,A1,A2,i,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)
A2 . (i,i) is set
[i,i] is V15() set
{i,i} is non empty set
{i} is non empty set
{{i,i},{i}} is non empty set
A2 . [i,i] is Relation-like Function-like 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,i) . g is Relation-like the Sorts of (A1 . i) . g -defined the Sorts of (A1 . i) . g -valued Function-like non empty total quasi_total Element of bool [:( the Sorts of (A1 . i) . g),( the Sorts of (A1 . i) . g):]
[:( the Sorts of (A1 . i) . g),( the Sorts of (A1 . i) . g):] is Relation-like non empty set
bool [:( the Sorts of (A1 . i) . g),( the Sorts of (A1 . i) . g):] is non empty set
id ( the Sorts of (A1 . i) . g) is Relation-like the Sorts of (A1 . i) . g -defined the Sorts of (A1 . i) . g -valued Function-like one-to-one non empty total quasi_total Element of bool [:( the Sorts of (A1 . i) . g),( the Sorts of (A1 . i) . g):]
s is MSAlgebra over S2
the Sorts of s is Relation-like the carrier of S2 -defined Function-like non empty total set
the Sorts of s . g is set
the non empty non void V56() strict ManySortedSign is non empty non void V56() strict ManySortedSign
{ the non empty non void V56() strict ManySortedSign } is non empty set
A1 is set
{} --> {} is Relation-like non-empty empty-yielding {} -defined {{}} -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [:{},{{}}:]
[:{},{{}}:] is Relation-like set
bool [:{},{{}}:] is non empty set
dom ({} --> {}) is Relation-like non-empty empty-yielding K138() -defined Function-like one-to-one constant functional empty non proper V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool {}
bool {} is non empty set
rng ({} --> {}) is Relation-like non-empty empty-yielding K138() -defined Function-like one-to-one constant functional empty trivial proper V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding with_common_domain countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered V108() Element of bool {{}}
bool {{}} is non empty set
[:{},{}:] is Relation-like set
bool [:{},{}:] is non empty set
{} * is functional non empty FinSequence-membered M8( {} )
[:{},({} *):] is Relation-like set
bool [:{},({} *):] is non empty set
S2 is Relation-like non-empty empty-yielding {} -defined {} * -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [:{},({} *):]
S1 is Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [:{},{}:]
ManySortedSign(# {},{},S2,S1 #) is strict ManySortedSign
S1 is strict ManySortedSign
S2 is strict ManySortedSign
the carrier of S1 is set
the carrier' of S1 is set
[:{},{}:] is Relation-like set
bool [:{},{}:] is non empty set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like quasi_total Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is non empty set
the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like quasi_total Element of bool [: the carrier' of S2, the carrier of S2:]
the carrier' of S2 is set
the carrier of S2 is set
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is non empty set
A2 is Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [:{},{}:]
id {} is Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [:{},{}:]
{(id {})} is functional non empty with_common_domain set
A1 is Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [:{},{}:]
() is strict ManySortedSign
S1 is empty trivial V50() void V55( {} ) V56() trivial' ManySortedSign
the carrier of S1 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 set
id the carrier of S1 is Relation-like non-empty empty-yielding the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is Relation-like set
bool [: the carrier of S1, the carrier of S1:] is non empty set
the carrier' of S1 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 set
id the carrier' of S1 is Relation-like non-empty empty-yielding the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [: the carrier' of S1, the carrier' of S1:]
[: the carrier' of S1, the carrier' of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S1:] is non empty set
the ResultSort of S1 is Relation-like non-empty empty-yielding the carrier' of S1 -defined the carrier of S1 -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is non empty set
the ResultSort of S1 * {} is Relation-like non-empty empty-yielding K138() -defined the carrier' of S1 -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 ResultSort of S1 is Relation-like non-empty empty-yielding K138() -defined the carrier of S1 -valued 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 Arity of S1 is Relation-like non-empty empty-yielding the carrier' of S1 -defined the carrier of S1 * -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is functional non empty FinSequence-membered M8( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is non empty set
A1 is set
A2 is Relation-like Function-like set
the Arity of S1 . A1 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
A2 * (id the carrier of S1) is Relation-like non-empty empty-yielding K138() -defined the carrier of S1 -valued 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
(id the carrier of S1) . A1 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 Arity of S1 . ((id the carrier of S1) . A1) 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
S1 is non empty void V56() trivial' ManySortedSign
the carrier of S1 is non empty set
id the carrier of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one non empty total quasi_total 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 S1 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 set
id the carrier' of S1 is Relation-like non-empty empty-yielding the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [: the carrier' of S1, the carrier' of S1:]
[: the carrier' of S1, the carrier' of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S1:] is non empty set
rng (id the carrier of S1) is non empty Element of bool the carrier of S1
bool the carrier of S1 is non empty set
rng (id the carrier' of S1) is Relation-like non-empty empty-yielding K138() -defined Function-like one-to-one constant functional empty trivial non proper V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered V108() Element of bool the carrier' of S1
bool the carrier' of S1 is non empty set
the ResultSort of S1 is Relation-like non-empty empty-yielding the carrier' of S1 -defined the carrier of S1 -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is non empty set
(id the carrier of S1) * the ResultSort of S1 is Relation-like non-empty empty-yielding K138() -defined the carrier' of S1 -defined the carrier of S1 -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [: the carrier' of S1, the carrier of S1:]
the ResultSort of S1 * (id the carrier' of S1) is Relation-like non-empty empty-yielding K138() -defined the carrier' of S1 -defined the carrier of S1 -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [: the carrier' of S1, the carrier of S1:]
the Arity of S1 is Relation-like non-empty empty-yielding the carrier' of S1 -defined the carrier of S1 * -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is functional non empty FinSequence-membered M8( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is non empty set
A2 is set
x is Relation-like Function-like set
the Arity of S1 . A2 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
x * (id the carrier of S1) is Relation-like the carrier of S1 -valued Function-like set
(id the carrier' of S1) . A2 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 Arity of S1 . ((id the carrier' of S1) . A2) 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
dom (id the carrier of S1) is non empty Element of bool the carrier of S1
dom (id the carrier' of S1) is Relation-like non-empty empty-yielding K138() -defined Function-like one-to-one constant functional empty trivial non proper V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool the carrier' of S1
S1 is void V56() trivial' ManySortedSign
the carrier of S1 is set
id the carrier of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is Relation-like set
bool [: the carrier of S1, the carrier of S1:] is non empty set
the carrier' of S1 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 set
id the carrier' of S1 is Relation-like non-empty empty-yielding the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one constant functional empty total quasi_total V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [: the carrier' of S1, the carrier' of S1:]
[: the carrier' of S1, the carrier' of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S1:] is non empty set
S1 is non empty set
S2 is set
A1 is set
A2 is set
x is non empty non void V56() strict ManySortedSign
the carrier of x is non empty set
the carrier' of x is non empty set
the Arity of x is Relation-like the carrier' of x -defined the carrier of x * -valued Function-like non empty total quasi_total Function-yielding V42() Element of bool [: the carrier' of x,( the carrier of x *):]
the carrier of x * is functional non empty FinSequence-membered M8( the carrier of x)
[: the carrier' of x,( the carrier of x *):] is Relation-like non empty set
bool [: the carrier' of x,( the carrier of x *):] is non empty set
the ResultSort of x is Relation-like the carrier' of x -defined the carrier of x -valued Function-like non empty total quasi_total Element of bool [: the carrier' of x, the carrier of x:]
[: the carrier' of x, the carrier of x:] is Relation-like non empty set
bool [: the carrier' of x, the carrier of x:] is non empty set
[ the carrier of x, the carrier' of x, the Arity of x, the ResultSort of x] is V15() V16() V17() set
[ the carrier of x, the carrier' of x, the Arity of x] is V15() V16() set
[ the carrier of x, the carrier' of x] is V15() set
{ the carrier of x, the carrier' of x} is non empty set
{ the carrier of x} is non empty set
{{ the carrier of x, the carrier' of x},{ the carrier of x}} is non empty set
[[ the carrier of x, the carrier' of x], the Arity of x] is V15() set
{[ the carrier of x, the carrier' of x], the Arity of x} is non empty set
{[ the carrier of x, the carrier' of x]} is Relation-like Function-like non empty set
{{[ the carrier of x, the carrier' of x], the Arity of x},{[ the carrier of x, the carrier' of x]}} is non empty set
[[ the carrier of x, the carrier' of x, the Arity of x], the ResultSort of x] is V15() set
{[ the carrier of x, the carrier' of x, the Arity of x], the ResultSort of x} is non empty set
{[ the carrier of x, the carrier' of x, the Arity of x]} is non empty set
{{[ the carrier of x, the carrier' of x, the Arity of x], the ResultSort of x},{[ the carrier of x, the carrier' of x, the Arity of x]}} is non empty set
g is non empty non void V56() strict ManySortedSign
the carrier of g is non empty set
the carrier' of g is non empty set
the Arity of g is Relation-like the carrier' of g -defined the carrier of g * -valued Function-like non empty total quasi_total Function-yielding V42() Element of bool [: the carrier' of g,( the carrier of g *):]
the carrier of g * is functional non empty FinSequence-membered M8( the carrier of g)
[: the carrier' of g,( the carrier of g *):] is Relation-like non empty set
bool [: the carrier' of g,( the carrier of g *):] is non empty set
the ResultSort of g is Relation-like the carrier' of g -defined the carrier of g -valued Function-like non empty total quasi_total Element of bool [: the carrier' of g, the carrier of g:]
[: the carrier' of g, the carrier of g:] is Relation-like non empty set
bool [: the carrier' of g, the carrier of g:] is non empty set
[ the carrier of g, the carrier' of g, the Arity of g, the ResultSort of g] is V15() V16() V17() set
[ the carrier of g, the carrier' of g, the Arity of g] is V15() V16() set
[ the carrier of g, the carrier' of g] is V15() set
{ the carrier of g, the carrier' of g} is non empty set
{ the carrier of g} is non empty set
{{ the carrier of g, the carrier' of g},{ the carrier of g}} is non empty set
[[ the carrier of g, the carrier' of g], the Arity of g] is V15() set
{[ the carrier of g, the carrier' of g], the Arity of g} is non empty set
{[ the carrier of g, the carrier' of g]} is Relation-like Function-like non empty set
{{[ the carrier of g, the carrier' of g], the Arity of g},{[ the carrier of g, the carrier' of g]}} is non empty set
[[ the carrier of g, the carrier' of g, the Arity of g], the ResultSort of g] is V15() set
{[ the carrier of g, the carrier' of g, the Arity of g], the ResultSort of g} is non empty set
{[ the carrier of g, the carrier' of g, the Arity of g]} is non empty set
{{[ the carrier of g, the carrier' of g, the Arity of g], the ResultSort of g},{[ the carrier of g, the carrier' of g, the Arity of g]}} is non empty set
x is non empty non void V56() strict ManySortedSign
the carrier of x is non empty set
the carrier' of x is non empty set
the Arity of x is Relation-like the carrier' of x -defined the carrier of x * -valued Function-like non empty total quasi_total Function-yielding V42() Element of bool [: the carrier' of x,( the carrier of x *):]
the carrier of x * is functional non empty FinSequence-membered M8( the carrier of x)
[: the carrier' of x,( the carrier of x *):] is Relation-like non empty set
bool [: the carrier' of x,( the carrier of x *):] is non empty set
the ResultSort of x is Relation-like the carrier' of x -defined the carrier of x -valued Function-like non empty total quasi_total Element of bool [: the carrier' of x, the carrier of x:]
[: the carrier' of x, the carrier of x:] is Relation-like non empty set
bool [: the carrier' of x, the carrier of x:] is non empty set
[ the carrier of x, the carrier' of x, the Arity of x, the ResultSort of x] is V15() V16() V17() set
[ the carrier of x, the carrier' of x, the Arity of x] is V15() V16() set
[ the carrier of x, the carrier' of x] is V15() set
{ the carrier of x, the carrier' of x} is non empty set
{ the carrier of x} is non empty set
{{ the carrier of x, the carrier' of x},{ the carrier of x}} is non empty set
[[ the carrier of x, the carrier' of x], the Arity of x] is V15() set
{[ the carrier of x, the carrier' of x], the Arity of x} is non empty set
{[ the carrier of x, the carrier' of x]} is Relation-like Function-like non empty set
{{[ the carrier of x, the carrier' of x], the Arity of x},{[ the carrier of x, the carrier' of x]}} is non empty set
[[ the carrier of x, the carrier' of x, the Arity of x], the ResultSort of x] is V15() set
{[ the carrier of x, the carrier' of x, the Arity of x], the ResultSort of x} is non empty set
{[ the carrier of x, the carrier' of x, the Arity of x]} is non empty set
{{[ the carrier of x, the carrier' of x, the Arity of x], the ResultSort of x},{[ the carrier of x, the carrier' of x, the Arity of x]}} is non empty set
g is non empty non void V56() strict ManySortedSign
the carrier of g is non empty set
the carrier' of g is non empty set
the Arity of g is Relation-like the carrier' of g -defined the carrier of g * -valued Function-like non empty total quasi_total Function-yielding V42() Element of bool [: the carrier' of g,( the carrier of g *):]
the carrier of g * is functional non empty FinSequence-membered M8( the carrier of g)
[: the carrier' of g,( the carrier of g *):] is Relation-like non empty set
bool [: the carrier' of g,( the carrier of g *):] is non empty set
the ResultSort of g is Relation-like the carrier' of g -defined the carrier of g -valued Function-like non empty total quasi_total Element of bool [: the carrier' of g, the carrier of g:]
[: the carrier' of g, the carrier of g:] is Relation-like non empty set
bool [: the carrier' of g, the carrier of g:] is non empty set
[ the carrier of g, the carrier' of g, the Arity of g, the ResultSort of g] is V15() V16() V17() set
[ the carrier of g, the carrier' of g, the Arity of g] is V15() V16() set
[ the carrier of g, the carrier' of g] is V15() set
{ the carrier of g, the carrier' of g} is non empty set
{ the carrier of g} is non empty set
{{ the carrier of g, the carrier' of g},{ the carrier of g}} is non empty set
[[ the carrier of g, the carrier' of g], the Arity of g] is V15() set
{[ the carrier of g, the carrier' of g], the Arity of g} is non empty set
{[ the carrier of g, the carrier' of g]} is Relation-like Function-like non empty set
{{[ the carrier of g, the carrier' of g], the Arity of g},{[ the carrier of g, the carrier' of g]}} is non empty set
[[ the carrier of g, the carrier' of g, the Arity of g], the ResultSort of g] is V15() set
{[ the carrier of g, the carrier' of g, the Arity of g], the ResultSort of g} is non empty set
{[ the carrier of g, the carrier' of g, the Arity of g]} is non empty set
{{[ the carrier of g, the carrier' of g, the Arity of g], the ResultSort of g},{[ the carrier of g, the carrier' of g, the Arity of g]}} is non empty set
bool S1 is non empty set
S1 * is functional non empty FinSequence-membered M8(S1)
PFuncs (S1,(S1 *)) is set
PFuncs (S1,S1) is set
[:(bool S1),(bool S1),(PFuncs (S1,(S1 *))),(PFuncs (S1,S1)):] is set
S2 is set
A1 is set
A2 is set
x is non empty non void V56() strict ManySortedSign
the carrier of x is non empty set
the carrier' of x is non empty set
the Arity of x is Relation-like the carrier' of x -defined the carrier of x * -valued Function-like non empty total quasi_total Function-yielding V42() Element of bool [: the carrier' of x,( the carrier of x *):]
the carrier of x * is functional non empty FinSequence-membered M8( the carrier of x)
[: the carrier' of x,( the carrier of x *):] is Relation-like non empty set
bool [: the carrier' of x,( the carrier of x *):] is non empty set
the ResultSort of x is Relation-like the carrier' of x -defined the carrier of x -valued Function-like non empty total quasi_total Element of bool [: the carrier' of x, the carrier of x:]
[: the carrier' of x, the carrier of x:] is Relation-like non empty set
bool [: the carrier' of x, the carrier of x:] is non empty set
[ the carrier of x, the carrier' of x, the Arity of x, the ResultSort of x] is V15() V16() V17() set
[ the carrier of x, the carrier' of x, the Arity of x] is V15() V16() set
[ the carrier of x, the carrier' of x] is V15() set
{ the carrier of x, the carrier' of x} is non empty set
{ the carrier of x} is non empty set
{{ the carrier of x, the carrier' of x},{ the carrier of x}} is non empty set
[[ the carrier of x, the carrier' of x], the Arity of x] is V15() set
{[ the carrier of x, the carrier' of x], the Arity of x} is non empty set
{[ the carrier of x, the carrier' of x]} is Relation-like Function-like non empty set
{{[ the carrier of x, the carrier' of x], the Arity of x},{[ the carrier of x, the carrier' of x]}} is non empty set
[[ the carrier of x, the carrier' of x, the Arity of x], the ResultSort of x] is V15() set
{[ the carrier of x, the carrier' of x, the Arity of x], the ResultSort of x} is non empty set
{[ the carrier of x, the carrier' of x, the Arity of x]} is non empty set
{{[ the carrier of x, the carrier' of x, the Arity of x], the ResultSort of x},{[ the carrier of x, the carrier' of x, the Arity of x]}} is non empty set
x is non empty non void V56() strict ManySortedSign
the carrier of x is non empty set
the carrier' of x is non empty set
the Arity of x is Relation-like the carrier' of x -defined the carrier of x * -valued Function-like non empty total quasi_total Function-yielding V42() Element of bool [: the carrier' of x,( the carrier of x *):]
the carrier of x * is functional non empty FinSequence-membered M8( the carrier of x)
[: the carrier' of x,( the carrier of x *):] is Relation-like non empty set
bool [: the carrier' of x,( the carrier of x *):] is non empty set
the ResultSort of x is Relation-like the carrier' of x -defined the carrier of x -valued Function-like non empty total quasi_total Element of bool [: the carrier' of x, the carrier of x:]
[: the carrier' of x, the carrier of x:] is Relation-like non empty set
bool [: the carrier' of x, the carrier of x:] is non empty set
[ the carrier of x, the carrier' of x, the Arity of x, the ResultSort of x] is V15() V16() V17() set
[ the carrier of x, the carrier' of x, the Arity of x] is V15() V16() set
[ the carrier of x, the carrier' of x] is V15() set
{ the carrier of x, the carrier' of x} is non empty set
{ the carrier of x} is non empty set
{{ the carrier of x, the carrier' of x},{ the carrier of x}} is non empty set
[[ the carrier of x, the carrier' of x], the Arity of x] is V15() set
{[ the carrier of x, the carrier' of x], the Arity of x} is non empty set
{[ the carrier of x, the carrier' of x]} is Relation-like Function-like non empty set
{{[ the carrier of x, the carrier' of x], the Arity of x},{[ the carrier of x, the carrier' of x]}} is non empty set
[[ the carrier of x, the carrier' of x, the Arity of x], the ResultSort of x] is V15() set
{[ the carrier of x, the carrier' of x, the Arity of x], the ResultSort of x} is non empty set
{[ the carrier of x, the carrier' of x, the Arity of x]} is non empty set
{{[ the carrier of x, the carrier' of x, the Arity of x], the ResultSort of x},{[ the carrier of x, the carrier' of x, the Arity of x]}} is non empty set
g is non empty non void V56() strict ManySortedSign
the carrier of g is non empty set
the carrier' of g is non empty set
the Arity of g is Relation-like the carrier' of g -defined the carrier of g * -valued Function-like non empty total quasi_total Function-yielding V42() Element of bool [: the carrier' of g,( the carrier of g *):]
the carrier of g * is functional non empty FinSequence-membered M8( the carrier of g)
[: the carrier' of g,( the carrier of g *):] is Relation-like non empty set
bool [: the carrier' of g,( the carrier of g *):] is non empty set
the ResultSort of g is Relation-like the carrier' of g -defined the carrier of g -valued Function-like non empty total quasi_total Element of bool [: the carrier' of g, the carrier of g:]
[: the carrier' of g, the carrier of g:] is Relation-like non empty set
bool [: the carrier' of g, the carrier of g:] is non empty set
[ the carrier of g, the carrier' of g, the Arity of g, the ResultSort of g] is V15() V16() V17() set
[ the carrier of g, the carrier' of g, the Arity of g] is V15() V16() set
[ the carrier of g, the carrier' of g] is V15() set
{ the carrier of g, the carrier' of g} is non empty set
{ the carrier of g} is non empty set
{{ the carrier of g, the carrier' of g},{ the carrier of g}} is non empty set
[[ the carrier of g, the carrier' of g], the Arity of g] is V15() set
{[ the carrier of g, the carrier' of g], the Arity of g} is non empty set
{[ the carrier of g, the carrier' of g]} is Relation-like Function-like non empty set
{{[ the carrier of g, the carrier' of g], the Arity of g},{[ the carrier of g, the carrier' of g]}} is non empty set
[[ the carrier of g, the carrier' of g, the Arity of g], the ResultSort of g] is V15() set
{[ the carrier of g, the carrier' of g, the Arity of g], the ResultSort of g} is non empty set
{[ the carrier of g, the carrier' of g, the Arity of g]} is non empty set
{{[ the carrier of g, the carrier' of g, the Arity of g], the ResultSort of g},{[ the carrier of g, the carrier' of g, the Arity of g]}} is non empty set
A2 is non empty non void V56() strict ManySortedSign
the carrier of A2 is non empty set
the carrier' of A2 is non empty set
the ResultSort of A2 is Relation-like the carrier' of A2 -defined the carrier of A2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of A2, the carrier of A2:]
[: the carrier' of A2, the carrier of A2:] is Relation-like non empty set
bool [: the carrier' of A2, the carrier of A2:] is non empty set
dom the ResultSort of A2 is non empty Element of bool the carrier' of A2
bool the carrier' of A2 is non empty set
rng the ResultSort of A2 is non empty Element of bool the carrier of A2
bool the carrier of A2 is non empty set
the Arity of A2 is Relation-like the carrier' of A2 -defined the carrier of A2 * -valued Function-like non empty total quasi_total Function-yielding V42() Element of bool [: the carrier' of A2,( the carrier of A2 *):]
the carrier of A2 * is functional non empty FinSequence-membered M8( the carrier of A2)
[: the carrier' of A2,( the carrier of A2 *):] is Relation-like non empty set
bool [: the carrier' of A2,( the carrier of A2 *):] is non empty set
[ the carrier of A2, the carrier' of A2, the Arity of A2, the ResultSort of A2] is V15() V16() V17() set
[ the carrier of A2, the carrier' of A2, the Arity of A2] is V15() V16() set
[ the carrier of A2, the carrier' of A2] is V15() set
{ the carrier of A2, the carrier' of A2} is non empty set
{ the carrier of A2} is non empty set
{{ the carrier of A2, the carrier' of A2},{ the carrier of A2}} is non empty set
[[ the carrier of A2, the carrier' of A2], the Arity of A2] is V15() set
{[ the carrier of A2, the carrier' of A2], the Arity of A2} is non empty set
{[ the carrier of A2, the carrier' of A2]} is Relation-like Function-like non empty set
{{[ the carrier of A2, the carrier' of A2], the Arity of A2},{[ the carrier of A2, the carrier' of A2]}} is non empty set
[[ the carrier of A2, the carrier' of A2, the Arity of A2], the ResultSort of A2] is V15() set
{[ the carrier of A2, the carrier' of A2, the Arity of A2], the ResultSort of A2} is non empty set
{[ the carrier of A2, the carrier' of A2, the Arity of A2]} is non empty set
{{[ the carrier of A2, the carrier' of A2, the Arity of A2], the ResultSort of A2},{[ the carrier of A2, the carrier' of A2, the Arity of A2]}} is non empty set
g is set
x is Element of bool S1
x * is functional non empty FinSequence-membered M8(x)
rng the Arity of A2 is functional non empty FinSequence-membered Element of bool ( the carrier of A2 *)
bool ( the carrier of A2 *) is non empty set
dom the Arity of A2 is non empty Element of bool the carrier' of A2
S2 is set
A1 is set
A2 is set
x is non empty non void V56() strict ManySortedSign
the carrier of x is non empty set
the carrier' of x is non empty set
A2 is set
x is non empty non void V56() strict ManySortedSign
the carrier of x is non empty set
the carrier' of x is non empty set
S1 is non empty set
(S1) is set
the Element of S1 is Element of S1
{ the Element of S1} is non empty set
{ the Element of S1} --> the Element of S1 is Relation-like { the Element of S1} -defined S1 -valued Function-like constant non empty total quasi_total Element of bool [:{ the Element of S1},S1:]
[:{ the Element of S1},S1:] is Relation-like non empty set
bool [:{ the Element of S1},S1:] is non empty set
dom ({ the Element of S1} --> the Element of S1) is non empty Element of bool { the Element of S1}
bool { the Element of S1} is non empty set
rng ({ the Element of S1} --> the Element of S1) is non empty trivial Element of bool S1
bool S1 is non empty set
[:{ the Element of S1},{ the Element of S1}:] is Relation-like non empty set
bool [:{ the Element of S1},{ the Element of S1}:] is non empty set
<* the Element of S1*> is Relation-like K138() -defined S1 -valued Function-like non empty V28() V35(1) countable FinSequence-like FinSubsequence-like FinSequence of S1
{ the Element of S1} * is functional non empty FinSequence-membered M8({ the Element of S1})
[:{ the Element of S1},({ the Element of S1} *):] is Relation-like non empty set
bool [:{ the Element of S1},({ the Element of S1} *):] is non empty set
[:K138(),S1:] is Relation-like non empty set
bool [:K138(),S1:] is non empty set
{ the Element of S1} --> <* the Element of S1*> is Relation-like non-empty non empty-yielding { the Element of S1} -defined bool [:K138(),S1:] -valued bool [:K138(),S1:] -valued Function-like constant non empty total quasi_total Function-yielding V42() Element of bool [:{ the Element of S1},(bool [:K138(),S1:]):]
[:{ the Element of S1},(bool [:K138(),S1:]):] is Relation-like non empty set
bool [:{ the Element of S1},(bool [:K138(),S1:]):] is non empty set
x is Relation-like { the Element of S1} -defined { the Element of S1} * -valued Function-like non empty total quasi_total Function-yielding V42() Element of bool [:{ the Element of S1},({ the Element of S1} *):]
A2 is Relation-like { the Element of S1} -defined { the Element of S1} -valued Function-like non empty total quasi_total Element of bool [:{ the Element of S1},{ the Element of S1}:]
ManySortedSign(# { the Element of S1},{ the Element of S1},x,A2 #) is non empty V56() strict ManySortedSign
g is set
e is non empty non void V56() strict ManySortedSign
the carrier of e is non empty set
the carrier' of e is non empty set
S1 is non empty () set
S2 is Element of S1
S1 is ManySortedSign
S2 is ManySortedSign
the carrier of S1 is set
the carrier of S2 is set
PFuncs ( the carrier of S1, the carrier of S2) is set
the carrier' of S1 is set
the carrier' of S2 is set
PFuncs ( the carrier' of S1, the carrier' of S2) is set
[:(PFuncs ( the carrier of S1, the carrier of S2)),(PFuncs ( the carrier' of S1, the carrier' of S2)):] is Relation-like set
A1 is set
A2 is set
x is Relation-like Function-like set
g is Relation-like Function-like set
[x,g] is V15() set
{x,g} is functional non empty set
{x} is functional non empty with_common_domain set
{{x,g},{x}} is non empty set
proj1 g is set
proj2 g is set
proj1 x is set
proj2 x is set
A1 is set
A2 is set
x is set
g is Relation-like Function-like set
e is Relation-like Function-like set
[g,e] is V15() set
{g,e} is functional non empty set
{g} is functional non empty with_common_domain set
{{g,e},{g}} is non empty set
x is set
g is Relation-like Function-like set
e is Relation-like Function-like set
[g,e] is V15() set
{g,e} is functional non empty set
{g} is functional non empty with_common_domain set
{{g,e},{g}} is non empty set