:: CIRCCOMB semantic presentation

REAL is set

NAT is non empty V12() V23() V24() V25() non finite countable denumerable Element of K19(REAL)

K19(REAL) is set

NAT is non empty V12() V23() V24() V25() non finite countable denumerable set

K19(NAT) is set

K19(NAT) is set

BOOLEAN is non empty set

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V22() V23() V24() V25() V27() V28() V29() finite finite-yielding V34() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable Element of NAT

the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V22() V23() V24() V25() V27() V28() V29() finite finite-yielding V34() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V22() V23() V24() V25() V27() V28() V29() finite finite-yielding V34() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable set

1 is non empty V23() V24() V25() V29() Element of NAT

{0,1} is non empty finite countable set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V22() V23() V24() V25() V27() V28() V29() finite finite-yielding V34() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable set

{{},1} is non empty finite countable set

K260() is set

K19(K260()) is set

K261() is Element of K19(K260())

K301() is non empty V89() L10()

the carrier of K301() is non empty set

K264( the carrier of K301()) is non empty M24( the carrier of K301())

K300(K301()) is Element of K19(K264( the carrier of K301()))

K19(K264( the carrier of K301())) is set

K20(K300(K301()),NAT) is Relation-like set

K19(K20(K300(K301()),NAT)) is set

K20(NAT,K300(K301())) is Relation-like set

K19(K20(NAT,K300(K301()))) is set

2 is non empty V23() V24() V25() V29() Element of NAT

3 is non empty V23() V24() V25() V29() Element of NAT

S1 is V23() V24() V25() V29() Element of NAT

Seg S1 is finite S1 -element countable Element of K19(NAT)

S2 is non empty set

(Seg S1) --> S2 is Relation-like non-empty Seg S1 -defined Seg S1 -defined {S2} -valued Function-like constant total total V18( Seg S1,{S2}) finite FinSequence-like FinSubsequence-like countable Element of K19(K20((Seg S1),{S2}))

{S2} is non empty finite countable set

K20((Seg S1),{S2}) is Relation-like finite countable set

K19(K20((Seg S1),{S2})) is finite V34() countable set

product ((Seg S1) --> S2) is functional non empty with_common_domain product-like set

S1 |-> S2 is Relation-like NAT -defined Function-like finite S1 -element FinSequence-like FinSubsequence-like countable set

product (S1 |-> S2) is functional with_common_domain product-like set

S1 -tuples_on S2 is functional non empty FinSequence-membered FinSequenceSet of S2

S1 is set

S2 is set

S1 \/ S2 is set

A1 is Relation-like S1 -defined Function-like total set

A2 is Relation-like S2 -defined Function-like total set

A1 +* A2 is Relation-like Function-like set

proj1 A2 is set

proj1 A1 is set

proj1 (A1 +* A2) is set

S1 is set

S2 is set

S1 \/ S2 is set

A1 is Relation-like S1 -defined Function-like total set

A2 is Relation-like S2 -defined Function-like total set

A1 +* A2 is Relation-like S1 \/ S2 -defined Function-like set

proj1 A2 is set

proj1 A1 is set

proj1 (A1 +* A2) is set

c

S1 is set

{S1} is non empty finite countable set

S2 is set

S1 .--> S2 is Relation-like {S1} -defined Function-like one-to-one constant V12() finite countable set

{S1} --> S2 is Relation-like {S1} -defined {S2} -valued Function-like constant non empty total V18({S1},{S2}) finite countable Element of K19(K20({S1},{S2}))

{S2} is non empty finite countable set

K20({S1},{S2}) is Relation-like finite countable set

K19(K20({S1},{S2})) is finite V34() countable set

S1 is set

{S1} is non empty finite countable set

S2 is set

S1 .--> S2 is Relation-like {S1} -defined Function-like one-to-one constant V12() finite countable set

{S1} --> S2 is Relation-like {S1} -defined {S2} -valued Function-like constant non empty total V18({S1},{S2}) finite countable Element of K19(K20({S1},{S2}))

{S2} is non empty finite countable set

K20({S1},{S2}) is Relation-like finite countable set

K19(K20({S1},{S2})) is finite V34() countable set

A1 is Relation-like {S1} -defined Function-like set

S1 is set

S2 is non empty set

S1 .--> S2 is Relation-like {S1} -defined Function-like one-to-one constant non empty V12() total finite countable set

{S1} is non empty finite countable set

{S1} --> S2 is Relation-like non-empty non empty-yielding {S1} -defined {S2} -valued Function-like constant non empty total V18({S1},{S2}) finite countable Element of K19(K20({S1},{S2}))

{S2} is non empty finite countable set

K20({S1},{S2}) is Relation-like finite countable set

K19(K20({S1},{S2})) is finite V34() countable set

S1 is set

S2 is set

A1 is Relation-like S1 -defined Function-like total set

A1 # is Relation-like S1 * -defined Function-like non empty total set

S1 * is functional non empty FinSequence-membered FinSequenceSet of S1

A2 is Relation-like S2 -defined Function-like total set

A2 # is Relation-like S2 * -defined Function-like non empty total set

S2 * is functional non empty FinSequence-membered FinSequenceSet of S2

proj1 A1 is set

proj1 A2 is set

proj1 (A2 #) is non empty set

c

S is set

g is set

[S,g] is V15() set

{S,g} is non empty finite countable set

{S} is non empty finite countable set

{{S,g},{S}} is non empty finite V34() countable set

proj1 (A1 #) is non empty set

IV is Relation-like NAT -defined S1 -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of S1 *

proj2 IV is finite countable set

v is Relation-like NAT -defined S2 -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of S2 *

proj2 v is finite countable set

(A1 #) . IV is set

IV * A1 is Relation-like NAT -defined Function-like finite countable set

product (IV * A1) is functional with_common_domain product-like set

v * A2 is Relation-like NAT -defined Function-like finite countable set

product (v * A2) is functional with_common_domain product-like set

(A2 #) . v is set

S1 is set

S2 is non empty set

S1 --> S2 is Relation-like non-empty S1 -defined {S2} -valued Function-like constant total V18(S1,{S2}) Element of K19(K20(S1,{S2}))

{S2} is non empty finite countable set

K20(S1,{S2}) is Relation-like set

K19(K20(S1,{S2})) is set

(S1 --> S2) # is Relation-like non-empty non empty-yielding S1 * -defined Function-like non empty total set

S1 * is functional non empty FinSequence-membered FinSequenceSet of S1

A1 is Relation-like NAT -defined S1 -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of S1

((S1 --> S2) #) . A1 is set

len A1 is V23() V24() V25() V29() Element of NAT

(len A1) -tuples_on S2 is functional non empty FinSequence-membered FinSequenceSet of S2

proj2 A1 is finite countable set

(proj2 A1) /\ S1 is finite countable set

A1 " S1 is finite countable set

A1 " (proj2 A1) is finite countable set

dom A1 is finite countable Element of K19(NAT)

(S1 --> S2) * A1 is Relation-like non-empty NAT -defined {S2} -valued Function-like finite countable Element of K19(K20(NAT,{S2}))

K20(NAT,{S2}) is Relation-like set

K19(K20(NAT,{S2})) is set

product ((S1 --> S2) * A1) is functional non empty with_common_domain product-like set

(A1 " S1) --> S2 is Relation-like non-empty A1 " S1 -defined {S2} -valued Function-like constant total V18(A1 " S1,{S2}) finite countable Element of K19(K20((A1 " S1),{S2}))

K20((A1 " S1),{S2}) is Relation-like finite countable set

K19(K20((A1 " S1),{S2})) is finite V34() countable set

product ((A1 " S1) --> S2) is functional non empty with_common_domain product-like set

Seg (len A1) is finite len A1 -element countable Element of K19(NAT)

(Seg (len A1)) --> S2 is Relation-like non-empty Seg (len A1) -defined Seg (len A1) -defined {S2} -valued Function-like constant total total V18( Seg (len A1),{S2}) finite FinSequence-like FinSubsequence-like countable Element of K19(K20((Seg (len A1)),{S2}))

K20((Seg (len A1)),{S2}) is Relation-like finite countable set

K19(K20((Seg (len A1)),{S2})) is finite V34() countable set

product ((Seg (len A1)) --> S2) is functional non empty with_common_domain product-like set

S1 is set

A2 is set

S2 is Relation-like non-empty S1 -defined Function-like total set

A1 is Relation-like non-empty S1 -defined Function-like total set

c

S is Relation-like non-empty A2 -defined Function-like total set

g is Relation-like S1 -defined Function-like total Function-yielding V22() ManySortedFunction of S2,A1

IV is Relation-like A2 -defined Function-like total Function-yielding V22() ManySortedFunction of c

g +* IV is Relation-like S1 \/ A2 -defined Function-like total Function-yielding V22() set

S1 \/ A2 is set

S2 +* c

A1 +* S is Relation-like non-empty S1 \/ A2 -defined Function-like total set

proj1 A1 is set

proj1 c

proj1 S is set

proj1 IV is set

proj1 g is set

proj1 S2 is set

CHARACT is Relation-like S1 \/ A2 -defined Function-like total Function-yielding V22() set

SORTS is set

CHARACT . SORTS is Relation-like Function-like set

(S2 +* c

(A1 +* S) . SORTS is set

K20(((S2 +* c

K19(K20(((S2 +* c

g . SORTS is Relation-like Function-like set

S2 . SORTS is set

A1 . SORTS is set

K20((S2 . SORTS),(A1 . SORTS)) is Relation-like set

K19(K20((S2 . SORTS),(A1 . SORTS))) is set

IV . SORTS is Relation-like Function-like set

c

S . SORTS is set

K20((c

K19(K20((c

A1 is ManySortedSign

the Arity of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 * -valued Function-like V18( the carrier' of A1, the carrier of A1 * ) Function-yielding V22() Element of K19(K20( the carrier' of A1,( the carrier of A1 *)))

the carrier' of A1 is set

the carrier of A1 is set

the carrier of A1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of A1

K20( the carrier' of A1,( the carrier of A1 *)) is Relation-like set

K19(K20( the carrier' of A1,( the carrier of A1 *))) is set

A2 is ManySortedSign

the ResultSort of A2 is Relation-like the carrier' of A2 -defined the carrier of A2 -valued Function-like V18( the carrier' of A2, the carrier of A2) Element of K19(K20( the carrier' of A2, the carrier of A2))

the carrier' of A2 is set

the carrier of A2 is set

K20( the carrier' of A2, the carrier of A2) is Relation-like set

K19(K20( the carrier' of A2, the carrier of A2)) is set

A1 is ManySortedSign

the Arity of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 * -valued Function-like V18( the carrier' of A1, the carrier of A1 * ) Function-yielding V22() Element of K19(K20( the carrier' of A1,( the carrier of A1 *)))

the carrier' of A1 is set

the carrier of A1 is set

the carrier of A1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of A1

K20( the carrier' of A1,( the carrier of A1 *)) is Relation-like set

K19(K20( the carrier' of A1,( the carrier of A1 *))) is set

A2 is ManySortedSign

the Arity of A2 is Relation-like the carrier' of A2 -defined the carrier of A2 * -valued Function-like V18( the carrier' of A2, the carrier of A2 * ) Function-yielding V22() Element of K19(K20( the carrier' of A2,( the carrier of A2 *)))

the carrier' of A2 is set

the carrier of A2 is set

the carrier of A2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of A2

K20( the carrier' of A2,( the carrier of A2 *)) is Relation-like set

K19(K20( the carrier' of A2,( the carrier of A2 *))) is set

the ResultSort of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 -valued Function-like V18( the carrier' of A1, the carrier of A1) Element of K19(K20( the carrier' of A1, the carrier of A1))

K20( the carrier' of A1, the carrier of A1) is Relation-like set

K19(K20( the carrier' of A1, the carrier of A1)) is set

the ResultSort of A2 is Relation-like the carrier' of A2 -defined the carrier of A2 -valued Function-like V18( the carrier' of A2, the carrier of A2) Element of K19(K20( the carrier' of A2, the carrier of A2))

K20( the carrier' of A2, the carrier of A2) is Relation-like set

K19(K20( the carrier' of A2, the carrier of A2)) is set

S1 is non empty V65() ManySortedSign

the carrier of S1 is non empty set

S2 is non empty V65() ManySortedSign

the carrier of S2 is non empty set

the carrier of S1 \/ the carrier of S2 is non empty set

the carrier' of S1 is set

the carrier' of S2 is set

the carrier' of S1 \/ the carrier' of S2 is set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V18( the carrier' of S1, the carrier of S1 * ) Function-yielding V22() Element of K19(K20( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S1

K20( the carrier' of S1,( the carrier of S1 *)) is Relation-like set

K19(K20( the carrier' of S1,( the carrier of S1 *))) is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like V18( the carrier' of S2, the carrier of S2 * ) Function-yielding V22() Element of K19(K20( the carrier' of S2,( the carrier of S2 *)))

the carrier of S2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S2

K20( the carrier' of S2,( the carrier of S2 *)) is Relation-like set

K19(K20( the carrier' of S2,( the carrier of S2 *))) is set

the Arity of S1 +* the Arity of S2 is Relation-like Function-like Function-yielding V22() set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

the ResultSort of S1 +* the ResultSort of S2 is Relation-like Function-like set

proj1 the ResultSort of S2 is set

proj1 the ResultSort of S1 is set

proj1 ( the ResultSort of S1 +* the ResultSort of S2) is set

S is non empty set

proj2 the ResultSort of S2 is set

proj2 the ResultSort of S1 is set

(proj2 the ResultSort of S1) \/ (proj2 the ResultSort of S2) is set

proj2 ( the ResultSort of S1 +* the ResultSort of S2) is set

K20(( the carrier' of S1 \/ the carrier' of S2),S) is Relation-like set

K19(K20(( the carrier' of S1 \/ the carrier' of S2),S)) is set

proj1 the Arity of S2 is set

proj1 the Arity of S1 is set

proj1 ( the Arity of S1 +* the Arity of S2) is set

proj2 the Arity of S1 is set

proj2 the Arity of S2 is set

S * is functional non empty FinSequence-membered FinSequenceSet of S

(proj2 the Arity of S1) \/ (proj2 the Arity of S2) is set

proj2 ( the Arity of S1 +* the Arity of S2) is set

K20(( the carrier' of S1 \/ the carrier' of S2),(S *)) is Relation-like set

K19(K20(( the carrier' of S1 \/ the carrier' of S2),(S *))) is set

IV is Relation-like the carrier' of S1 \/ the carrier' of S2 -defined S * -valued Function-like V18( the carrier' of S1 \/ the carrier' of S2,S * ) Function-yielding V22() Element of K19(K20(( the carrier' of S1 \/ the carrier' of S2),(S *)))

g is Relation-like the carrier' of S1 \/ the carrier' of S2 -defined S -valued Function-like V18( the carrier' of S1 \/ the carrier' of S2,S) Element of K19(K20(( the carrier' of S1 \/ the carrier' of S2),S))

ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) is non empty V65() strict ManySortedSign

the carrier of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) is non empty set

the carrier' of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) is set

the Arity of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) is Relation-like the carrier' of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) -defined the carrier of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) * -valued Function-like V18( the carrier' of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #), the carrier of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) * ) Function-yielding V22() Element of K19(K20( the carrier' of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #),( the carrier of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) *)))

the carrier of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #)

K20( the carrier' of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #),( the carrier of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) *)) is Relation-like set

K19(K20( the carrier' of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #),( the carrier of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) *))) is set

the ResultSort of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) is Relation-like the carrier' of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) -defined the carrier of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #) -valued Function-like V18( the carrier' of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #), the carrier of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #)) Element of K19(K20( the carrier' of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #), the carrier of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #)))

K20( the carrier' of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #), the carrier of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #)) is Relation-like set

K19(K20( the carrier' of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #), the carrier of ManySortedSign(# S,( the carrier' of S1 \/ the carrier' of S2),IV,g #))) is set

A1 is non empty V65() strict ManySortedSign

the carrier of A1 is non empty set

the carrier' of A1 is set

the Arity of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 * -valued Function-like V18( the carrier' of A1, the carrier of A1 * ) Function-yielding V22() Element of K19(K20( the carrier' of A1,( the carrier of A1 *)))

the carrier of A1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of A1

K20( the carrier' of A1,( the carrier of A1 *)) is Relation-like set

K19(K20( the carrier' of A1,( the carrier of A1 *))) is set

the ResultSort of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 -valued Function-like V18( the carrier' of A1, the carrier of A1) Element of K19(K20( the carrier' of A1, the carrier of A1))

K20( the carrier' of A1, the carrier of A1) is Relation-like set

K19(K20( the carrier' of A1, the carrier of A1)) is set

A2 is non empty V65() strict ManySortedSign

the carrier of A2 is non empty set

the carrier' of A2 is set

the Arity of A2 is Relation-like the carrier' of A2 -defined the carrier of A2 * -valued Function-like V18( the carrier' of A2, the carrier of A2 * ) Function-yielding V22() Element of K19(K20( the carrier' of A2,( the carrier of A2 *)))

the carrier of A2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of A2

K20( the carrier' of A2,( the carrier of A2 *)) is Relation-like set

K19(K20( the carrier' of A2,( the carrier of A2 *))) is set

the ResultSort of A2 is Relation-like the carrier' of A2 -defined the carrier of A2 -valued Function-like V18( the carrier' of A2, the carrier of A2) Element of K19(K20( the carrier' of A2, the carrier of A2))

K20( the carrier' of A2, the carrier of A2) is Relation-like set

K19(K20( the carrier' of A2, the carrier of A2)) is set

S1 is non empty V65() ManySortedSign

S2 is non empty V65() ManySortedSign

A1 is non empty V65() ManySortedSign

(S1,S2) is non empty V65() strict ManySortedSign

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V18( the carrier' of S1, the carrier of S1 * ) Function-yielding V22() Element of K19(K20( the carrier' of S1,( the carrier of S1 *)))

the carrier' of S1 is set

the carrier of S1 is non empty set

the carrier of S1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S1

K20( the carrier' of S1,( the carrier of S1 *)) is Relation-like set

K19(K20( the carrier' of S1,( the carrier of S1 *))) is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like V18( the carrier' of S2, the carrier of S2 * ) Function-yielding V22() Element of K19(K20( the carrier' of S2,( the carrier of S2 *)))

the carrier' of S2 is set

the carrier of S2 is non empty set

the carrier of S2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S2

K20( the carrier' of S2,( the carrier of S2 *)) is Relation-like set

K19(K20( the carrier' of S2,( the carrier of S2 *))) is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

the Arity of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 * -valued Function-like V18( the carrier' of A1, the carrier of A1 * ) Function-yielding V22() Element of K19(K20( the carrier' of A1,( the carrier of A1 *)))

the carrier' of A1 is set

the carrier of A1 is non empty set

the carrier of A1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of A1

K20( the carrier' of A1,( the carrier of A1 *)) is Relation-like set

K19(K20( the carrier' of A1,( the carrier of A1 *))) is set

the ResultSort of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 -valued Function-like V18( the carrier' of A1, the carrier of A1) Element of K19(K20( the carrier' of A1, the carrier of A1))

K20( the carrier' of A1, the carrier of A1) is Relation-like set

K19(K20( the carrier' of A1, the carrier of A1)) is set

the Arity of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) * -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2) * ) Function-yielding V22() Element of K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)))

the carrier' of (S1,S2) is set

the carrier of (S1,S2) is non empty set

the carrier of (S1,S2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (S1,S2)

K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)) is Relation-like set

K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *))) is set

the Arity of S1 +* the Arity of S2 is Relation-like Function-like Function-yielding V22() set

the ResultSort of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2)) Element of K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2)))

K20( the carrier' of (S1,S2), the carrier of (S1,S2)) is Relation-like set

K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2))) is set

the ResultSort of S1 +* the ResultSort of S2 is Relation-like Function-like set

S1 is non empty V65() ManySortedSign

(S1,S1) is non empty V65() strict ManySortedSign

the carrier of S1 is non empty set

the carrier' of S1 is set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V18( the carrier' of S1, the carrier of S1 * ) Function-yielding V22() Element of K19(K20( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S1

K20( the carrier' of S1,( the carrier of S1 *)) is Relation-like set

K19(K20( the carrier' of S1,( the carrier of S1 *))) is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) is non empty V65() strict ManySortedSign

the carrier' of S1 \/ the carrier' of S1 is set

the Arity of S1 +* the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like Function-yielding V22() Element of K19(K20( the carrier' of S1,( the carrier of S1 *)))

the ResultSort of S1 +* the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like Element of K19(K20( the carrier' of S1, the carrier of S1))

the carrier of S1 \/ the carrier of S1 is non empty set

S1 is non empty V65() ManySortedSign

S2 is non empty V65() ManySortedSign

(S1,S2) is non empty V65() strict ManySortedSign

(S2,S1) is non empty V65() strict ManySortedSign

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V18( the carrier' of S1, the carrier of S1 * ) Function-yielding V22() Element of K19(K20( the carrier' of S1,( the carrier of S1 *)))

the carrier' of S1 is set

the carrier of S1 is non empty set

the carrier of S1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S1

K20( the carrier' of S1,( the carrier of S1 *)) is Relation-like set

K19(K20( the carrier' of S1,( the carrier of S1 *))) is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like V18( the carrier' of S2, the carrier of S2 * ) Function-yielding V22() Element of K19(K20( the carrier' of S2,( the carrier of S2 *)))

the carrier' of S2 is set

the carrier of S2 is non empty set

the carrier of S2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S2

K20( the carrier' of S2,( the carrier of S2 *)) is Relation-like set

K19(K20( the carrier' of S2,( the carrier of S2 *))) is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

the carrier' of (S1,S2) is set

the carrier' of S1 \/ the carrier' of S2 is set

the ResultSort of S1 +* the ResultSort of S2 is Relation-like Function-like set

the ResultSort of S2 +* the ResultSort of S1 is Relation-like Function-like set

the ResultSort of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2)) Element of K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2)))

the carrier of (S1,S2) is non empty set

K20( the carrier' of (S1,S2), the carrier of (S1,S2)) is Relation-like set

K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2))) is set

the Arity of S1 +* the Arity of S2 is Relation-like Function-like Function-yielding V22() set

the Arity of S2 +* the Arity of S1 is Relation-like Function-like Function-yielding V22() set

the Arity of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) * -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2) * ) Function-yielding V22() Element of K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)))

the carrier of (S1,S2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (S1,S2)

K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)) is Relation-like set

K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *))) is set

the carrier of S1 \/ the carrier of S2 is non empty set

S1 is non empty V65() ManySortedSign

S2 is non empty V65() ManySortedSign

(S1,S2) is non empty V65() strict ManySortedSign

A1 is non empty V65() ManySortedSign

((S1,S2),A1) is non empty V65() strict ManySortedSign

(S2,A1) is non empty V65() strict ManySortedSign

(S1,(S2,A1)) is non empty V65() strict ManySortedSign

the carrier of (S2,A1) is non empty set

the carrier of S2 is non empty set

the carrier of A1 is non empty set

the carrier of S2 \/ the carrier of A1 is non empty set

the carrier of ((S1,S2),A1) is non empty set

the carrier of (S1,S2) is non empty set

the carrier of (S1,S2) \/ the carrier of A1 is non empty set

the carrier of (S1,(S2,A1)) is non empty set

the carrier of S1 is non empty set

the carrier of S1 \/ the carrier of (S2,A1) is non empty set

the carrier of S1 \/ the carrier of S2 is non empty set

the carrier' of (S2,A1) is set

the carrier' of S2 is set

the carrier' of A1 is set

the carrier' of S2 \/ the carrier' of A1 is set

the carrier' of ((S1,S2),A1) is set

the carrier' of (S1,S2) is set

the carrier' of (S1,S2) \/ the carrier' of A1 is set

the Arity of (S2,A1) is Relation-like the carrier' of (S2,A1) -defined the carrier of (S2,A1) * -valued Function-like V18( the carrier' of (S2,A1), the carrier of (S2,A1) * ) Function-yielding V22() Element of K19(K20( the carrier' of (S2,A1),( the carrier of (S2,A1) *)))

the carrier of (S2,A1) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (S2,A1)

K20( the carrier' of (S2,A1),( the carrier of (S2,A1) *)) is Relation-like set

K19(K20( the carrier' of (S2,A1),( the carrier of (S2,A1) *))) is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like V18( the carrier' of S2, the carrier of S2 * ) Function-yielding V22() Element of K19(K20( the carrier' of S2,( the carrier of S2 *)))

the carrier of S2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S2

K20( the carrier' of S2,( the carrier of S2 *)) is Relation-like set

K19(K20( the carrier' of S2,( the carrier of S2 *))) is set

the Arity of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 * -valued Function-like V18( the carrier' of A1, the carrier of A1 * ) Function-yielding V22() Element of K19(K20( the carrier' of A1,( the carrier of A1 *)))

the carrier of A1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of A1

K20( the carrier' of A1,( the carrier of A1 *)) is Relation-like set

K19(K20( the carrier' of A1,( the carrier of A1 *))) is set

the Arity of S2 +* the Arity of A1 is Relation-like Function-like Function-yielding V22() set

the Arity of (S1,(S2,A1)) is Relation-like the carrier' of (S1,(S2,A1)) -defined the carrier of (S1,(S2,A1)) * -valued Function-like V18( the carrier' of (S1,(S2,A1)), the carrier of (S1,(S2,A1)) * ) Function-yielding V22() Element of K19(K20( the carrier' of (S1,(S2,A1)),( the carrier of (S1,(S2,A1)) *)))

the carrier' of (S1,(S2,A1)) is set

the carrier of (S1,(S2,A1)) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (S1,(S2,A1))

K20( the carrier' of (S1,(S2,A1)),( the carrier of (S1,(S2,A1)) *)) is Relation-like set

K19(K20( the carrier' of (S1,(S2,A1)),( the carrier of (S1,(S2,A1)) *))) is set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V18( the carrier' of S1, the carrier of S1 * ) Function-yielding V22() Element of K19(K20( the carrier' of S1,( the carrier of S1 *)))

the carrier' of S1 is set

the carrier of S1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S1

K20( the carrier' of S1,( the carrier of S1 *)) is Relation-like set

K19(K20( the carrier' of S1,( the carrier of S1 *))) is set

the Arity of S1 +* the Arity of (S2,A1) is Relation-like Function-like Function-yielding V22() set

the carrier' of S1 \/ the carrier' of (S2,A1) is set

the carrier' of S1 \/ the carrier' of S2 is set

the ResultSort of (S1,(S2,A1)) is Relation-like the carrier' of (S1,(S2,A1)) -defined the carrier of (S1,(S2,A1)) -valued Function-like V18( the carrier' of (S1,(S2,A1)), the carrier of (S1,(S2,A1))) Element of K19(K20( the carrier' of (S1,(S2,A1)), the carrier of (S1,(S2,A1))))

K20( the carrier' of (S1,(S2,A1)), the carrier of (S1,(S2,A1))) is Relation-like set

K19(K20( the carrier' of (S1,(S2,A1)), the carrier of (S1,(S2,A1)))) is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

the ResultSort of (S2,A1) is Relation-like the carrier' of (S2,A1) -defined the carrier of (S2,A1) -valued Function-like V18( the carrier' of (S2,A1), the carrier of (S2,A1)) Element of K19(K20( the carrier' of (S2,A1), the carrier of (S2,A1)))

K20( the carrier' of (S2,A1), the carrier of (S2,A1)) is Relation-like set

K19(K20( the carrier' of (S2,A1), the carrier of (S2,A1))) is set

the ResultSort of S1 +* the ResultSort of (S2,A1) is Relation-like Function-like set

the ResultSort of ((S1,S2),A1) is Relation-like the carrier' of ((S1,S2),A1) -defined the carrier of ((S1,S2),A1) -valued Function-like V18( the carrier' of ((S1,S2),A1), the carrier of ((S1,S2),A1)) Element of K19(K20( the carrier' of ((S1,S2),A1), the carrier of ((S1,S2),A1)))

K20( the carrier' of ((S1,S2),A1), the carrier of ((S1,S2),A1)) is Relation-like set

K19(K20( the carrier' of ((S1,S2),A1), the carrier of ((S1,S2),A1))) is set

the ResultSort of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2)) Element of K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2)))

K20( the carrier' of (S1,S2), the carrier of (S1,S2)) is Relation-like set

K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2))) is set

the ResultSort of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 -valued Function-like V18( the carrier' of A1, the carrier of A1) Element of K19(K20( the carrier' of A1, the carrier of A1))

K20( the carrier' of A1, the carrier of A1) is Relation-like set

K19(K20( the carrier' of A1, the carrier of A1)) is set

the ResultSort of (S1,S2) +* the ResultSort of A1 is Relation-like Function-like set

the Arity of ((S1,S2),A1) is Relation-like the carrier' of ((S1,S2),A1) -defined the carrier of ((S1,S2),A1) * -valued Function-like V18( the carrier' of ((S1,S2),A1), the carrier of ((S1,S2),A1) * ) Function-yielding V22() Element of K19(K20( the carrier' of ((S1,S2),A1),( the carrier of ((S1,S2),A1) *)))

the carrier of ((S1,S2),A1) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of ((S1,S2),A1)

K20( the carrier' of ((S1,S2),A1),( the carrier of ((S1,S2),A1) *)) is Relation-like set

K19(K20( the carrier' of ((S1,S2),A1),( the carrier of ((S1,S2),A1) *))) is set

the Arity of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) * -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2) * ) Function-yielding V22() Element of K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)))

the carrier of (S1,S2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (S1,S2)

K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)) is Relation-like set

K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *))) is set

the Arity of (S1,S2) +* the Arity of A1 is Relation-like Function-like Function-yielding V22() set

the Arity of S1 +* the Arity of S2 is Relation-like Function-like Function-yielding V22() set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

the ResultSort of S2 +* the ResultSort of A1 is Relation-like Function-like set

the ResultSort of S1 +* the ResultSort of S2 is Relation-like Function-like set

S1 is Relation-like Function-like one-to-one set

S2 is non empty V65() Circuit-like ManySortedSign

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

the carrier' of S2 is set

the carrier of S2 is non empty set

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

A1 is non empty V65() Circuit-like ManySortedSign

the ResultSort of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 -valued Function-like V18( the carrier' of A1, the carrier of A1) Element of K19(K20( the carrier' of A1, the carrier of A1))

the carrier' of A1 is set

the carrier of A1 is non empty set

K20( the carrier' of A1, the carrier of A1) is Relation-like set

K19(K20( the carrier' of A1, the carrier of A1)) is set

(S2,A1) is non empty V65() strict ManySortedSign

A2 is non empty non void V65() ManySortedSign

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 V18( the carrier' of A2, the carrier of A2) Element of K19(K20( the carrier' of A2, the carrier of A2))

the carrier of A2 is non empty set

K20( the carrier' of A2, the carrier of A2) is Relation-like set

K19(K20( the carrier' of A2, the carrier of A2)) is set

the ResultSort of S2 +* the ResultSort of A1 is Relation-like Function-like set

the ResultSort of S2 \/ the ResultSort of A1 is Relation-like set

proj1 the ResultSort of A2 is set

proj1 S1 is set

IV is Element of the carrier' of A2

the_result_sort_of IV is Element of the carrier of A2

the ResultSort of A2 . IV is Element of the carrier of A2

v is Element of the carrier' of A2

the_result_sort_of v is Element of the carrier of A2

the ResultSort of A2 . v is Element of the carrier of A2

S1 . v is set

S1 . IV is set

S1 is non empty V65() Circuit-like ManySortedSign

InnerVertices S1 is Element of K19( the carrier of S1)

the carrier of S1 is non empty set

K19( the carrier of S1) is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

the carrier' of S1 is set

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

K367( the carrier of S1, the ResultSort of S1) is Element of K19( the carrier of S1)

S2 is non empty V65() Circuit-like ManySortedSign

InnerVertices S2 is Element of K19( the carrier of S2)

the carrier of S2 is non empty set

K19( the carrier of S2) is set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

the carrier' of S2 is set

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

K367( the carrier of S2, the ResultSort of S2) is Element of K19( the carrier of S2)

(S1,S2) is non empty V65() strict ManySortedSign

c

the carrier' of c

the ResultSort of c

the carrier of c

K20( the carrier' of c

K19(K20( the carrier' of c

proj1 the ResultSort of S1 is set

the ResultSort of S1 +* the ResultSort of S2 is Relation-like Function-like set

proj1 the ResultSort of S2 is set

g is Element of the carrier' of c

the_result_sort_of g is Element of the carrier of c

the ResultSort of c

IV is Element of the carrier' of c

the_result_sort_of IV is Element of the carrier of c

the ResultSort of c

the carrier' of S1 \/ the carrier' of S2 is set

the ResultSort of S1 . g is set

proj2 the ResultSort of S1 is set

the ResultSort of S2 . g is set

proj2 the ResultSort of S2 is set

the ResultSort of S1 . IV is set

the ResultSort of S2 . IV is set

v is non empty non void V65() Circuit-like ManySortedSign

the carrier' of v is non empty set

c

the_result_sort_of c

the carrier of v is non empty set

the ResultSort of v is Relation-like the carrier' of v -defined the carrier of v -valued Function-like V18( the carrier' of v, the carrier of v) Element of K19(K20( the carrier' of v, the carrier of v))

K20( the carrier' of v, the carrier of v) is Relation-like set

K19(K20( the carrier' of v, the carrier of v)) is set

the ResultSort of v . c

the ResultSort of S1 . c

o is Element of the carrier' of v

the_result_sort_of o is Element of the carrier of v

the ResultSort of v . o is Element of the carrier of v

the ResultSort of S1 . o is set

v is non empty non void V65() Circuit-like ManySortedSign

the carrier' of v is non empty set

c

the_result_sort_of c

the carrier of v is non empty set

the ResultSort of v is Relation-like the carrier' of v -defined the carrier of v -valued Function-like V18( the carrier' of v, the carrier of v) Element of K19(K20( the carrier' of v, the carrier of v))

K20( the carrier' of v, the carrier of v) is Relation-like set

K19(K20( the carrier' of v, the carrier of v)) is set

the ResultSort of v . c

the ResultSort of S2 . c

o is Element of the carrier' of v

the_result_sort_of o is Element of the carrier of v

the ResultSort of v . o is Element of the carrier of v

the ResultSort of S2 . o is set

S1 is non empty V65() ManySortedSign

S2 is non empty V65() ManySortedSign

(S1,S2) is non empty V65() strict ManySortedSign

the carrier' of (S1,S2) is set

the carrier' of S1 is set

the carrier' of S2 is set

the carrier' of S1 \/ the carrier' of S2 is set

S1 is non empty finite V65() ManySortedSign

S2 is non empty finite V65() ManySortedSign

(S1,S2) is non empty V65() strict ManySortedSign

the carrier of S1 is non empty finite countable set

the carrier of S2 is non empty finite countable set

the carrier of (S1,S2) is non empty set

A1 is finite countable set

A2 is finite countable set

A1 \/ A2 is finite countable set

S1 is non empty non void V65() ManySortedSign

S2 is non empty V65() ManySortedSign

(S1,S2) is non empty V65() strict ManySortedSign

(S2,S1) is non empty V65() strict ManySortedSign

S1 is non empty V65() ManySortedSign

S2 is non empty V65() ManySortedSign

(S1,S2) is non empty V65() strict ManySortedSign

InnerVertices (S1,S2) is Element of K19( the carrier of (S1,S2))

the carrier of (S1,S2) is non empty set

K19( the carrier of (S1,S2)) is set

the ResultSort of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2)) Element of K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2)))

the carrier' of (S1,S2) is set

K20( the carrier' of (S1,S2), the carrier of (S1,S2)) is Relation-like set

K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2))) is set

K367( the carrier of (S1,S2), the ResultSort of (S1,S2)) is Element of K19( the carrier of (S1,S2))

InnerVertices S1 is Element of K19( the carrier of S1)

the carrier of S1 is non empty set

K19( the carrier of S1) is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

the carrier' of S1 is set

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

K367( the carrier of S1, the ResultSort of S1) is Element of K19( the carrier of S1)

InnerVertices S2 is Element of K19( the carrier of S2)

the carrier of S2 is non empty set

K19( the carrier of S2) is set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

the carrier' of S2 is set

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

K367( the carrier of S2, the ResultSort of S2) is Element of K19( the carrier of S2)

(InnerVertices S1) \/ (InnerVertices S2) is set

InputVertices (S1,S2) is Element of K19( the carrier of (S1,S2))

the carrier of (S1,S2) \ K367( the carrier of (S1,S2), the ResultSort of (S1,S2)) is Element of K19( the carrier of (S1,S2))

InputVertices S1 is Element of K19( the carrier of S1)

the carrier of S1 \ K367( the carrier of S1, the ResultSort of S1) is Element of K19( the carrier of S1)

InputVertices S2 is Element of K19( the carrier of S2)

the carrier of S2 \ K367( the carrier of S2, the ResultSort of S2) is Element of K19( the carrier of S2)

(InputVertices S1) \/ (InputVertices S2) is set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V18( the carrier' of S1, the carrier of S1 * ) Function-yielding V22() Element of K19(K20( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S1

K20( the carrier' of S1,( the carrier of S1 *)) is Relation-like set

K19(K20( the carrier' of S1,( the carrier of S1 *))) is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like V18( the carrier' of S2, the carrier of S2 * ) Function-yielding V22() Element of K19(K20( the carrier' of S2,( the carrier of S2 *)))

the carrier of S2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S2

K20( the carrier' of S2,( the carrier of S2 *)) is Relation-like set

K19(K20( the carrier' of S2,( the carrier of S2 *))) is set

the ResultSort of S1 +* the ResultSort of S2 is Relation-like Function-like set

proj2 the ResultSort of S1 is set

proj2 the ResultSort of (S1,S2) is set

proj2 the ResultSort of S2 is set

(proj2 the ResultSort of S1) \/ (proj2 the ResultSort of S2) is set

g is set

the carrier of S1 \/ the carrier of S2 is non empty set

the carrier of S1 \ (proj2 the ResultSort of S1) is Element of K19( the carrier of S1)

the carrier of S2 \ (proj2 the ResultSort of S2) is Element of K19( the carrier of S2)

S2 is non empty V65() ManySortedSign

the carrier of S2 is non empty set

S1 is non empty V65() ManySortedSign

(S1,S2) is non empty V65() strict ManySortedSign

InputVertices (S1,S2) is Element of K19( the carrier of (S1,S2))

the carrier of (S1,S2) is non empty set

K19( the carrier of (S1,S2)) is set

the ResultSort of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2)) Element of K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2)))

the carrier' of (S1,S2) is set

K20( the carrier' of (S1,S2), the carrier of (S1,S2)) is Relation-like set

K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2))) is set

K367( the carrier of (S1,S2), the ResultSort of (S1,S2)) is Element of K19( the carrier of (S1,S2))

the carrier of (S1,S2) \ K367( the carrier of (S1,S2), the ResultSort of (S1,S2)) is Element of K19( the carrier of (S1,S2))

InputVertices S2 is Element of K19( the carrier of S2)

K19( the carrier of S2) is set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

the carrier' of S2 is set

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

K367( the carrier of S2, the ResultSort of S2) is Element of K19( the carrier of S2)

the carrier of S2 \ K367( the carrier of S2, the ResultSort of S2) is Element of K19( the carrier of S2)

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

the carrier' of S1 is set

the carrier of S1 is non empty set

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

g is Element of the carrier of S2

the ResultSort of S1 +* the ResultSort of S2 is Relation-like Function-like set

proj2 the ResultSort of S2 is set

proj2 the ResultSort of (S1,S2) is set

S1 is non empty V65() ManySortedSign

S2 is non empty V65() ManySortedSign

the carrier of S1 is non empty set

(S1,S2) is non empty V65() strict ManySortedSign

InputVertices (S1,S2) is Element of K19( the carrier of (S1,S2))

the carrier of (S1,S2) is non empty set

K19( the carrier of (S1,S2)) is set

the ResultSort of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2)) Element of K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2)))

the carrier' of (S1,S2) is set

K20( the carrier' of (S1,S2), the carrier of (S1,S2)) is Relation-like set

K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2))) is set

K367( the carrier of (S1,S2), the ResultSort of (S1,S2)) is Element of K19( the carrier of (S1,S2))

the carrier of (S1,S2) \ K367( the carrier of (S1,S2), the ResultSort of (S1,S2)) is Element of K19( the carrier of (S1,S2))

InputVertices S1 is Element of K19( the carrier of S1)

K19( the carrier of S1) is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

the carrier' of S1 is set

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

K367( the carrier of S1, the ResultSort of S1) is Element of K19( the carrier of S1)

the carrier of S1 \ K367( the carrier of S1, the ResultSort of S1) is Element of K19( the carrier of S1)

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V18( the carrier' of S1, the carrier of S1 * ) Function-yielding V22() Element of K19(K20( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S1

K20( the carrier' of S1,( the carrier of S1 *)) is Relation-like set

K19(K20( the carrier' of S1,( the carrier of S1 *))) is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like V18( the carrier' of S2, the carrier of S2 * ) Function-yielding V22() Element of K19(K20( the carrier' of S2,( the carrier of S2 *)))

the carrier' of S2 is set

the carrier of S2 is non empty set

the carrier of S2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S2

K20( the carrier' of S2,( the carrier of S2 *)) is Relation-like set

K19(K20( the carrier' of S2,( the carrier of S2 *))) is set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

the ResultSort of S1 +* the ResultSort of S2 is Relation-like Function-like set

proj2 the ResultSort of S1 is set

proj2 the ResultSort of (S1,S2) is set

g is Element of the carrier of S1

S1 is non empty V65() ManySortedSign

S2 is non empty non void V65() ManySortedSign

the carrier' of S2 is non empty set

(S1,S2) is non empty non void V65() strict ManySortedSign

the carrier' of (S1,S2) is non empty set

A1 is Element of the carrier' of S2

the_arity_of A1 is Relation-like NAT -defined the carrier of S2 -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of S2 *

the carrier of S2 is non empty set

the carrier of S2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S2

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like V18( the carrier' of S2, the carrier of S2 * ) Function-yielding V22() Element of K19(K20( the carrier' of S2,( the carrier of S2 *)))

K20( the carrier' of S2,( the carrier of S2 *)) is Relation-like set

K19(K20( the carrier' of S2,( the carrier of S2 *))) is set

the Arity of S2 . A1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of S2 *

the_result_sort_of A1 is Element of the carrier of S2

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

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

A2 is Element of the carrier' of (S1,S2)

the_arity_of A2 is Relation-like NAT -defined the carrier of (S1,S2) -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of (S1,S2) *

the carrier of (S1,S2) is non empty set

the carrier of (S1,S2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (S1,S2)

the Arity of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) * -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2) * ) Function-yielding V22() Element of K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)))

K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)) is Relation-like set

K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *))) is set

the Arity of (S1,S2) . A2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of (S1,S2) *

the_result_sort_of A2 is Element of the carrier of (S1,S2)

the ResultSort of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2)) Element of K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2)))

K20( the carrier' of (S1,S2), the carrier of (S1,S2)) is Relation-like set

K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2))) is set

the ResultSort of (S1,S2) . A2 is Element of the carrier of (S1,S2)

proj1 the Arity of S2 is set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V18( the carrier' of S1, the carrier of S1 * ) Function-yielding V22() Element of K19(K20( the carrier' of S1,( the carrier of S1 *)))

the carrier' of S1 is set

the carrier of S1 is non empty set

the carrier of S1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S1

K20( the carrier' of S1,( the carrier of S1 *)) is Relation-like set

K19(K20( the carrier' of S1,( the carrier of S1 *))) is set

the Arity of S1 +* the Arity of S2 is Relation-like Function-like Function-yielding V22() set

proj1 the ResultSort of S2 is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

the ResultSort of S1 +* the ResultSort of S2 is Relation-like Function-like set

S1 is non empty V65() ManySortedSign

A1 is non empty non void V65() Circuit-like ManySortedSign

S2 is non empty non void V65() Circuit-like ManySortedSign

(S1,S2) is non empty non void V65() strict ManySortedSign

the carrier of S2 is non empty set

InnerVertices S2 is non empty Element of K19( the carrier of S2)

K19( the carrier of S2) is set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

the carrier' of S2 is non empty set

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

K367( the carrier of S2, the ResultSort of S2) is Element of K19( the carrier of S2)

the carrier of A1 is non empty set

InnerVertices A1 is non empty Element of K19( the carrier of A1)

K19( the carrier of A1) is set

the ResultSort of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 -valued Function-like V18( the carrier' of A1, the carrier of A1) Element of K19(K20( the carrier' of A1, the carrier of A1))

the carrier' of A1 is non empty set

K20( the carrier' of A1, the carrier of A1) is Relation-like set

K19(K20( the carrier' of A1, the carrier of A1)) is set

K367( the carrier of A1, the ResultSort of A1) is Element of K19( the carrier of A1)

A2 is Element of the carrier of S2

action_at A2 is Element of the carrier' of S2

the carrier' of S1 is set

the carrier' of S1 \/ the carrier' of S2 is non empty set

S is Element of the carrier of A1

action_at S is Element of the carrier' of A1

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

the carrier of S1 is non empty set

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

the ResultSort of S1 +* the ResultSort of S2 is Relation-like Function-like set

the_result_sort_of (action_at A2) is Element of the carrier of S2

the ResultSort of S2 . (action_at A2) is Element of the carrier of S2

c

the_result_sort_of c

the ResultSort of A1 . c

S1 is non empty non void V65() ManySortedSign

the carrier' of S1 is non empty set

S2 is non empty V65() ManySortedSign

(S1,S2) is non empty non void V65() strict ManySortedSign

the carrier' of (S1,S2) is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V18( the carrier' of S1, the carrier of S1 * ) Function-yielding V22() Element of K19(K20( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 is non empty set

the carrier of S1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S1

K20( the carrier' of S1,( the carrier of S1 *)) is Relation-like set

K19(K20( the carrier' of S1,( the carrier of S1 *))) is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like V18( the carrier' of S2, the carrier of S2 * ) Function-yielding V22() Element of K19(K20( the carrier' of S2,( the carrier of S2 *)))

the carrier' of S2 is set

the carrier of S2 is non empty set

the carrier of S2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S2

K20( the carrier' of S2,( the carrier of S2 *)) is Relation-like set

K19(K20( the carrier' of S2,( the carrier of S2 *))) is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

A1 is Element of the carrier' of S1

the_arity_of A1 is Relation-like NAT -defined the carrier of S1 -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of S1 *

the Arity of S1 . A1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of S1 *

the_result_sort_of A1 is Element of the carrier of S1

the ResultSort of S1 . A1 is Element of the carrier of S1

A2 is Element of the carrier' of (S1,S2)

the_arity_of A2 is Relation-like NAT -defined the carrier of (S1,S2) -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of (S1,S2) *

the carrier of (S1,S2) is non empty set

the carrier of (S1,S2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (S1,S2)

the Arity of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) * -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2) * ) Function-yielding V22() Element of K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)))

K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)) is Relation-like set

K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *))) is set

the Arity of (S1,S2) . A2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of (S1,S2) *

the_result_sort_of A2 is Element of the carrier of (S1,S2)

the ResultSort of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2)) Element of K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2)))

K20( the carrier' of (S1,S2), the carrier of (S1,S2)) is Relation-like set

K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2))) is set

the ResultSort of (S1,S2) . A2 is Element of the carrier of (S1,S2)

proj1 the Arity of S1 is set

the Arity of S1 +* the Arity of S2 is Relation-like Function-like Function-yielding V22() set

proj1 the ResultSort of S1 is set

the ResultSort of S1 +* the ResultSort of S2 is Relation-like Function-like set

S1 is non empty non void V65() Circuit-like ManySortedSign

S2 is non empty non void V65() Circuit-like ManySortedSign

the carrier of S1 is non empty set

InnerVertices S1 is non empty Element of K19( the carrier of S1)

K19( the carrier of S1) is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

the carrier' of S1 is non empty set

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

K367( the carrier of S1, the ResultSort of S1) is Element of K19( the carrier of S1)

the carrier of S2 is non empty set

InnerVertices S2 is non empty Element of K19( the carrier of S2)

K19( the carrier of S2) is set

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

the carrier' of S2 is non empty set

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

K367( the carrier of S2, the ResultSort of S2) is Element of K19( the carrier of S2)

A1 is non empty V65() ManySortedSign

(S1,A1) is non empty non void V65() strict ManySortedSign

A2 is Element of the carrier of S1

action_at A2 is Element of the carrier' of S1

c

action_at c

InnerVertices A1 is Element of K19( the carrier of A1)

the carrier of A1 is non empty set

K19( the carrier of A1) is set

the ResultSort of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 -valued Function-like V18( the carrier' of A1, the carrier of A1) Element of K19(K20( the carrier' of A1, the carrier of A1))

the carrier' of A1 is set

K20( the carrier' of A1, the carrier of A1) is Relation-like set

K19(K20( the carrier' of A1, the carrier of A1)) is set

K367( the carrier of A1, the ResultSort of A1) is Element of K19( the carrier of A1)

(InnerVertices S1) \/ (InnerVertices A1) is non empty set

the carrier' of S1 \/ the carrier' of A1 is non empty set

the_result_sort_of (action_at A2) is Element of the carrier of S1

the ResultSort of S1 . (action_at A2) is Element of the carrier of S1

S is Element of the carrier' of S2

the_result_sort_of S is Element of the carrier of S2

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

S1 is non empty V65() ManySortedSign

S2 is non empty V65() ManySortedSign

S1 is non empty V65() ManySortedSign

S2 is non empty V65() ManySortedSign

A1 is non-empty MSAlgebra over S1

the Sorts of A1 is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

the carrier of S1 is non empty set

A2 is non-empty MSAlgebra over S2

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

the carrier of S2 is non empty set

(S1,S2) is non empty V65() strict ManySortedSign

the Sorts of A1 +* the Sorts of A2 is Relation-like non-empty non empty-yielding the carrier of S1 \/ the carrier of S2 -defined Function-like non empty total set

the carrier of S1 \/ the carrier of S2 is non empty set

the carrier' of S1 is set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V18( the carrier' of S1, the carrier of S1 * ) Function-yielding V22() Element of K19(K20( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S1

K20( the carrier' of S1,( the carrier of S1 *)) is Relation-like set

K19(K20( the carrier' of S1,( the carrier of S1 *))) is set

the Sorts of A1 # is Relation-like non-empty non empty-yielding the carrier of S1 * -defined Function-like non empty total set

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

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

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

the carrier' of S2 is set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like V18( the carrier' of S2, the carrier of S2 * ) Function-yielding V22() Element of K19(K20( the carrier' of S2,( the carrier of S2 *)))

the carrier of S2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S2

K20( the carrier' of S2,( the carrier of S2 *)) is Relation-like set

K19(K20( the carrier' of S2,( the carrier of S2 *))) is set

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

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

the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V18( the carrier' of S2, the carrier of S2) Element of K19(K20( the carrier' of S2, the carrier of S2))

K20( the carrier' of S2, the carrier of S2) is Relation-like set

K19(K20( the carrier' of S2, the carrier of S2)) is set

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

the Charact of A1 is Relation-like the carrier' of S1 -defined Function-like total Function-yielding V22() ManySortedFunction of the Arity of S1 * ( the Sorts of A1 #), the ResultSort of S1 * the Sorts of A1

the Charact of A2 is Relation-like the carrier' of S2 -defined Function-like total Function-yielding V22() ManySortedFunction of the Arity of S2 * ( the Sorts of A2 #), the ResultSort of S2 * the Sorts of A2

( the carrier' of S1,( the Arity of S1 * ( the Sorts of A1 #)),( the ResultSort of S1 * the Sorts of A1), the carrier' of S2,( the Arity of S2 * ( the Sorts of A2 #)),( the ResultSort of S2 * the Sorts of A2), the Charact of A1, the Charact of A2) is Relation-like the carrier' of S1 \/ the carrier' of S2 -defined Function-like total Function-yielding V22() ManySortedFunction of ( the Arity of S1 * ( the Sorts of A1 #)) +* ( the Arity of S2 * ( the Sorts of A2 #)),( the ResultSort of S1 * the Sorts of A1) +* ( the ResultSort of S2 * the Sorts of A2)

the carrier' of S1 \/ the carrier' of S2 is set

( the Arity of S1 * ( the Sorts of A1 #)) +* ( the Arity of S2 * ( the Sorts of A2 #)) is Relation-like non-empty the carrier' of S1 \/ the carrier' of S2 -defined Function-like total set

( the ResultSort of S1 * the Sorts of A1) +* ( the ResultSort of S2 * the Sorts of A2) is Relation-like non-empty the carrier' of S1 \/ the carrier' of S2 -defined Function-like total set

c

the Sorts of c

the carrier of (S1,S2) is non empty set

the Charact of c

the carrier' of (S1,S2) is set

the Arity of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) * -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2) * ) Function-yielding V22() Element of K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)))

the carrier of (S1,S2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (S1,S2)

K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)) is Relation-like set

K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *))) is set

the Sorts of c

the Arity of (S1,S2) * ( the Sorts of c

the ResultSort of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2)) Element of K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2)))

K20( the carrier' of (S1,S2), the carrier of (S1,S2)) is Relation-like set

K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2))) is set

the ResultSort of (S1,S2) * the Sorts of c

S is strict non-empty MSAlgebra over (S1,S2)

the Sorts of S is Relation-like non-empty non empty-yielding the carrier of (S1,S2) -defined Function-like non empty total set

the Charact of S is Relation-like the carrier' of (S1,S2) -defined Function-like total Function-yielding V22() ManySortedFunction of the Arity of (S1,S2) * ( the Sorts of S #), the ResultSort of (S1,S2) * the Sorts of S

the Sorts of S # is Relation-like non-empty non empty-yielding the carrier of (S1,S2) * -defined Function-like non empty total set

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

the ResultSort of (S1,S2) * the Sorts of S is Relation-like non-empty the carrier' of (S1,S2) -defined Function-like total set

the carrier of (S1,S2) is non empty set

( the Sorts of A1 #) +* ( the Sorts of A2 #) is Relation-like non-empty non empty-yielding ( the carrier of S1 *) \/ ( the carrier of S2 *) -defined Function-like non empty total set

( the carrier of S1 *) \/ ( the carrier of S2 *) is non empty set

proj1 ( the Sorts of A2 #) is non empty set

the ResultSort of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2)) Element of K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2)))

the carrier' of (S1,S2) is set

K20( the carrier' of (S1,S2), the carrier of (S1,S2)) is Relation-like set

K19(K20( the carrier' of (S1,S2), the carrier of (S1,S2))) is set

the ResultSort of S1 +* the ResultSort of S2 is Relation-like Function-like set

proj2 the ResultSort of S2 is set

proj1 the Sorts of A2 is non empty set

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

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

the carrier of (S1,S2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (S1,S2)

proj1 (SORTS #) is non empty set

the Sorts of A1 \/ the Sorts of A2 is Relation-like non empty set

proj1 (( the Sorts of A1 #) +* ( the Sorts of A2 #)) is non empty set

proj1 the Sorts of A1 is non empty set

proj2 the ResultSort of S1 is set

( the ResultSort of S1 +* the ResultSort of S2) * ( the Sorts of A1 +* the Sorts of A2) is Relation-like non-empty Function-like set

proj2 the Arity of S2 is set

proj1 ( the Sorts of A1 #) is non empty set

pp is set

(proj1 ( the Sorts of A1 #)) /\ (proj1 ( the Sorts of A2 #)) is set

( the Sorts of A1 #) . pp is set

( the Sorts of A2 #) . pp is set

CHARACT is Relation-like NAT -defined the carrier of S1 -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of S1 *

proj2 CHARACT is finite countable set

A is Relation-like NAT -defined the carrier of S2 -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of S2 *

proj2 A is finite countable set

CHARACT * the Sorts of A1 is Relation-like non-empty NAT -defined Function-like finite countable set

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

A * the Sorts of A2 is Relation-like non-empty NAT -defined Function-like finite countable set

product (A * the Sorts of A2) is functional non empty with_common_domain product-like set

( the Sorts of A1 #) \/ ( the Sorts of A2 #) is Relation-like non empty set

the Arity of (S1,S2) is Relation-like the carrier' of (S1,S2) -defined the carrier of (S1,S2) * -valued Function-like V18( the carrier' of (S1,S2), the carrier of (S1,S2) * ) Function-yielding V22() Element of K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)))

K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *)) is Relation-like set

K19(K20( the carrier' of (S1,S2),( the carrier of (S1,S2) *))) is set

proj2 the Arity of (S1,S2) is set

proj2 the Arity of S1 is set

(proj2 the Arity of S1) \/ (proj2 the Arity of S2) is set

the Arity of S1 +* the Arity of S2 is Relation-like Function-like Function-yielding V22() set

( the Arity of S1 +* the Arity of S2) * (( the Sorts of A1 #) +* ( the Sorts of A2 #)) is Relation-like non-empty Function-like set

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

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

pp is Relation-like the carrier' of (S1,S2) -defined Function-like total Function-yielding V22() ManySortedFunction of the Arity of (S1,S2) * (SORTS #), the ResultSort of (S1,S2) * SORTS

MSAlgebra(# SORTS,pp #) is strict MSAlgebra over (S1,S2)

CHARACT is strict non-empty MSAlgebra over (S1,S2)

the Sorts of CHARACT is Relation-like non-empty non empty-yielding the carrier of (S1,S2) -defined Function-like non empty total set

the Charact of CHARACT is Relation-like the carrier' of (S1,S2) -defined Function-like total Function-yielding V22() ManySortedFunction of the Arity of (S1,S2) * ( the Sorts of CHARACT #), the ResultSort of (S1,S2) * the Sorts of CHARACT

the Sorts of CHARACT # is Relation-like non-empty non empty-yielding the carrier of (S1,S2) * -defined Function-like non empty total set

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

the ResultSort of (S1,S2) * the Sorts of CHARACT is Relation-like non-empty the carrier' of (S1,S2) -defined Function-like total set

S1 is non empty non void V65() ManySortedSign

S2 is MSAlgebra over S1

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

the carrier of S1 is non empty set

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

the carrier' of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V18( the carrier' of S1, the carrier of S1 * ) Function-yielding V22() Element of K19(K20( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S1

K20( the carrier' of S1,( the carrier of S1 *)) is Relation-like set

K19(K20( the carrier' of S1,( the carrier of S1 *))) is set

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

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

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

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

S1 is non empty non void V65() ManySortedSign

S2 is non empty non void V65() ManySortedSign

A1 is MSAlgebra over S1

A2 is MSAlgebra over S2

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

the carrier of S1 is non empty set

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

the carrier of S2 is non empty set

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

the carrier' of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V18( the carrier' of S1, the carrier of S1 * ) Function-yielding V22() Element of K19(K20( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of S1

K20( the carrier' of S1,( the carrier of S1 *)) is Relation-like set

K19(K20( the carrier' of S1,( the carrier of S1 *))) is set

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

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

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V18( the carrier' of S1, the carrier of S1) Element of K19(K20( the carrier' of S1, the carrier of S1))

K20( the carrier' of S1, the carrier of S1) is Relation-like set

K19(K20( the carrier' of S1, the carrier of S1)) is set

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

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

the carrier' of S2 is non empty set

the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like V18( the carrier' of S2, the carrier of S2 * ) Function-yielding V22() Element of K19(K20( the