:: 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₅ is Relation-like S1 \/ S2 -defined Function-like 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
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₅ is set
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₅ is Relation-like non-empty A2 -defined Function-like total set
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₅,S
g +* IV is Relation-like S1 \/ A2 -defined Function-like total Function-yielding V22() set
S1 \/ A2 is set
S2 +* c₅ is Relation-like non-empty S1 \/ A2 -defined Function-like total set
A1 +* S is Relation-like non-empty S1 \/ A2 -defined Function-like total set
proj1 A1 is set
proj1 c₅ is set
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₅) . SORTS is set
(A1 +* S) . SORTS is set
K20(((S2 +* c₅) . SORTS),((A1 +* S) . SORTS)) is Relation-like set
K19(K20(((S2 +* c₅) . SORTS),((A1 +* S) . SORTS))) is set
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₅ . SORTS is set
S . SORTS is set
K20((c₅ . SORTS),(S . SORTS)) is Relation-like set
K19(K20((c₅ . SORTS),(S . SORTS))) 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 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₅ is non empty non void V65() ManySortedSign
the carrier' of c₅ is non empty set
the ResultSort of c₅ is Relation-like the carrier' of c₅ -defined the carrier of c₅ -valued Function-like V18( the carrier' of c₅, the carrier of c₅) Element of K19(K20( the carrier' of c₅, the carrier of c₅))
the carrier of c₅ is non empty set
K20( the carrier' of c₅, the carrier of c₅) is Relation-like set
K19(K20( the carrier' of c₅, the carrier of c₅)) is set
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₅ . g is Element of the carrier 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₅ . IV is Element of the carrier 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₁₁ is Element of the carrier' of v
the_result_sort_of c₁₁ is Element of the carrier of v
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₁₁ is Element of the carrier of v
the ResultSort of S1 . c₁₁ is set
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₁₁ is Element of the carrier' of v
the_result_sort_of c₁₁ is Element of the carrier of v
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₁₁ is Element of the carrier of v
the ResultSort of S2 . c₁₁ is set
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₅ is Element of the carrier' of A1
the_result_sort_of c₅ is Element of the carrier of A1
the ResultSort of A1 . c₅ is Element of the carrier of A1
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₅ is Element of the carrier of S2
action_at c₅ is Element of the carrier' of S2
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₅ is strict non-empty MSAlgebra over (S1,S2)
the Sorts of c₅ 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 non empty set
the Charact of c₅ 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 c₅ #), the ResultSort of (S1,S2) * the Sorts 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₅ # 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 c₅ #) is Relation-like non-empty the carrier' of (S1,S2) -defined Function-like total 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,S2) * the Sorts of c₅ is Relation-like non-empty the carrier' of (S1,S2) -defined Function-like total set
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