K93() is set
K97() is Element of K19(K93())
K19(K93()) is set
K92() is set
K19(K92()) is set
K20(K97(),K93()) is Relation-like set
K19(K20(K97(),K93())) is set
K19(K19(K93())) is set
K19(K97()) is set
{} is Relation-like non-empty empty-yielding K97() -defined Function-like one-to-one constant functional empty V31() FinSequence-like FinSubsequence-like FinSequence-membered set
the Relation-like non-empty empty-yielding K97() -defined Function-like one-to-one constant functional empty V31() FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding K97() -defined Function-like one-to-one constant functional empty V31() FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty set
{{},1} is non empty set
K353() is set
K19(K353()) is set
K354() is Element of K19(K353())
K394() is non empty strict L12()
the carrier of K394() is non empty set
K357( the carrier of K394()) is non empty M35( the carrier of K394())
K393(K394()) is Element of K19(K357( the carrier of K394()))
K19(K357( the carrier of K394())) is set
K20(K393(K394()),K97()) is Relation-like set
K19(K20(K393(K394()),K97())) is set
K20(K97(),K393(K394())) is Relation-like set
K19(K20(K97(),K393(K394()))) is set
2 is non empty set
3 is non empty set
S is Relation-like Function-like set
dom S is set
S9 is Relation-like Function-like set
dom S9 is set
(dom S) /\ (dom S9) is set
A is Relation-like Function-like set
dom A is set
S +* S9 is Relation-like Function-like set
(S +* S9) +* A is Relation-like Function-like set
S9 +* S is Relation-like Function-like set
(S9 +* S) +* A is Relation-like Function-like set
dom ((S9 +* S) +* A) is set
dom (S9 +* S) is set
(dom (S9 +* S)) \/ (dom A) is set
dom (S +* S9) is set
(dom S) \/ (dom S9) is set
E is set
((dom S) \/ (dom S9)) \/ (dom A) is set
((S +* S9) +* A) . E is set
A . E is set
((S9 +* S) +* A) . E is set
((S +* S9) +* A) . E is set
(S +* S9) . E is set
(dom S9) \/ (dom S) is set
S . E is set
(S9 +* S) . E is set
S9 . E is set
((S9 +* S) +* A) . E is set
(dom S9) \/ (dom S) is set
dom ((S +* S9) +* A) is set
(dom (S +* S9)) \/ (dom A) is set
S is Relation-like Function-like set
S9 is Relation-like Function-like set
A is Relation-like Function-like set
rng A is set
dom S9 is set
(rng A) /\ (dom S9) is set
dom S is set
A * S9 is Relation-like Function-like set
A * S is Relation-like Function-like set
dom (A * S) is set
dom (A * S9) is set
E is set
A . E is set
dom A is set
E is set
dom A is set
(A * S9) . E is set
A . E is set
S9 . (A . E) is set
(A * S) . E is set
S . (A . E) is set
S is Relation-like Function-like set
dom S is set
A is Relation-like Function-like set
rng A is set
S9 is Relation-like Function-like set
dom A is set
S9 .: (dom A) is set
S9 +* A is Relation-like Function-like set
(S9 +* A) * S is Relation-like Function-like set
S9 * S is Relation-like Function-like set
dom (S9 * S) is set
dom ((S9 +* A) * S) is set
E is set
dom S9 is set
S9 . E is set
(S9 +* A) . E is set
dom (S9 +* A) is set
E is set
(S9 +* A) . E is set
S9 . E is set
A . E is set
E is set
dom S9 is set
S9 . E is set
(S9 +* A) . E is set
dom (S9 +* A) is set
((S9 +* A) * S) . E is set
S . (S9 . E) is set
(S9 * S) . E is set
S is Relation-like Function-like set
S9 is Relation-like Function-like set
A is Relation-like Function-like set
E is Relation-like Function-like set
A * S is Relation-like Function-like set
E * S9 is Relation-like Function-like set
dom S is set
dom S9 is set
(dom S) /\ (dom S9) is set
dom A is set
dom E is set
(dom A) /\ (dom E) is set
x is set
dom (A * S) is set
dom (E * S9) is set
(dom (A * S)) /\ (dom (E * S9)) is set
(A * S) . x is set
(E * S9) . x is set
A . x is set
S . (A . x) is set
E . x is set
S9 . (E . x) is set
S is non empty set
A is non empty set
K20(S,A) is Relation-like set
K19(K20(S,A)) is set
S9 is non empty set
E is non empty set
K20(S9,E) is Relation-like set
K19(K20(S9,E)) is set
S * is functional non empty FinSequence-membered M11(S)
A * is functional non empty FinSequence-membered M11(A)
x is Relation-like S -defined A -valued Function-like non empty total V18(S,A) Element of K19(K20(S,A))
x * is Relation-like S * -defined A * -valued Function-like non empty total V18(S * ,A * ) Element of K19(K20((S *),(A *)))
K20((S *),(A *)) is Relation-like set
K19(K20((S *),(A *))) is set
o is Relation-like S9 -defined E -valued Function-like non empty total V18(S9,E) Element of K19(K20(S9,E))
o * is Relation-like S9 * -defined E * -valued Function-like non empty total V18(S9 * ,E * ) Element of K19(K20((S9 *),(E *)))
S9 * is functional non empty FinSequence-membered M11(S9)
E * is functional non empty FinSequence-membered M11(E)
K20((S9 *),(E *)) is Relation-like set
K19(K20((S9 *),(E *))) is set
dom o is non empty Element of K19(S9)
K19(S9) is set
dom x is non empty Element of K19(S)
K19(S) is set
e is set
p is Relation-like K97() -defined S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of S *
(x *) . p is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of A *
x * p is Relation-like K97() -defined A -valued Function-like V31() FinSequence-like FinSubsequence-like Element of A *
rng p is Element of K19(S)
(rng p) /\ S9 is Element of K19(S)
o * p is Relation-like K97() -defined E -valued Function-like Element of K19(K20(K97(),E))
K20(K97(),E) is Relation-like set
K19(K20(K97(),E)) is set
(x *) . e is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
(o *) . e is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
dom (o *) is functional non empty FinSequence-membered Element of K19((S9 *))
K19((S9 *)) is set
dom (x *) is functional non empty FinSequence-membered Element of K19((S *))
K19((S *)) is set
S is non empty set
A is non empty set
K20(S,A) is Relation-like set
K19(K20(S,A)) is set
S9 is non empty set
E is non empty set
K20(S9,E) is Relation-like set
K19(K20(S9,E)) is set
x is Relation-like S -defined A -valued Function-like non empty total V18(S,A) Element of K19(K20(S,A))
x * is Relation-like S * -defined A * -valued Function-like non empty total V18(S * ,A * ) Element of K19(K20((S *),(A *)))
S * is functional non empty FinSequence-membered M11(S)
A * is functional non empty FinSequence-membered M11(A)
K20((S *),(A *)) is Relation-like set
K19(K20((S *),(A *))) is set
o is Relation-like S9 -defined E -valued Function-like non empty total V18(S9,E) Element of K19(K20(S9,E))
o * is Relation-like S9 * -defined E * -valued Function-like non empty total V18(S9 * ,E * ) Element of K19(K20((S9 *),(E *)))
S9 * is functional non empty FinSequence-membered M11(S9)
E * is functional non empty FinSequence-membered M11(E)
K20((S9 *),(E *)) is Relation-like set
K19(K20((S9 *),(E *))) is set
dom o is non empty Element of K19(S9)
K19(S9) is set
dom x is non empty Element of K19(S)
K19(S) is set
(dom x) /\ (dom o) is Element of K19(S9)
e is set
dom (x *) is non empty set
dom (o *) is non empty set
(dom (x *)) /\ (dom (o *)) is set
(x *) . e is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
(o *) . e is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
dom (x *) is functional non empty FinSequence-membered Element of K19((S *))
K19((S *)) is set
dom (o *) is functional non empty FinSequence-membered Element of K19((S9 *))
K19((S9 *)) is set
(dom (x *)) /\ (dom (o *)) is functional FinSequence-membered Element of K19((S9 *))
p is Relation-like K97() -defined S9 -valued Function-like V31() FinSequence-like FinSubsequence-like Element of S9 *
o * p is Relation-like K97() -defined E -valued Function-like V31() FinSequence-like FinSubsequence-like Element of E *
gg is set
q is Relation-like K97() -defined S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of S *
dom q is Element of K19(K97())
p . gg is set
rng p is Element of K19(S9)
q . gg is set
rng q is Element of K19(S)
x . (q . gg) is set
o . (p . gg) is set
(o * p) . gg is set
x * q is Relation-like K97() -defined A -valued Function-like V31() FinSequence-like FinSubsequence-like Element of A *
(x * q) . gg is set
dom (o * p) is Element of K19(K97())
dom p is Element of K19(K97())
dom (x * q) is Element of K19(K97())
S is set
id S is Relation-like S -defined S -valued Function-like one-to-one total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
S9 is Relation-like Function-like set
S9 | S is Relation-like Function-like set
(id S) +* (S9 | S) is Relation-like Function-like set
dom (id S) is Element of K19(S)
K19(S) is set
dom ((id S) +* (S9 | S)) is set
dom (S9 | S) is set
S \/ (dom (S9 | S)) is set
S is set
S9 is Relation-like Function-like set
(S,S9) is Relation-like S -defined Function-like total set
id S is Relation-like S -defined S -valued Function-like one-to-one total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
S9 | S is Relation-like Function-like set
(id S) +* (S9 | S) is Relation-like Function-like set
rng (S,S9) is set
dom S9 is set
S \ (dom S9) is Element of K19(S)
K19(S) is set
S9 .: S is set
(S \ (dom S9)) \/ (S9 .: S) is set
dom (id S) is Element of K19(S)
dom (S9 | S) is set
S \ (dom (S9 | S)) is Element of K19(S)
(id S) .: (S \ (dom (S9 | S))) is Element of K19(S)
rng (S9 | S) is set
((id S) .: (S \ (dom (S9 | S)))) \/ (rng (S9 | S)) is set
((id S) .: (S \ (dom (S9 | S)))) \/ (S9 .: S) is set
(S \ (dom (S9 | S))) \/ (S9 .: S) is set
(dom S9) /\ S is set
S \ ((dom S9) /\ S) is Element of K19(S)
(S \ ((dom S9) /\ S)) \/ (S9 .: S) is set
S is non empty set
id S is Relation-like S -defined S -valued Function-like one-to-one non empty total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
S9 is Relation-like Function-like set
(S,S9) is Relation-like S -defined Function-like non empty total set
S9 | S is Relation-like Function-like set
(id S) +* (S9 | S) is Relation-like Function-like non empty set
(id S) +* S9 is Relation-like Function-like non empty set
A is Element of S
(S,S9) . A is set
((id S) +* S9) . A is set
((id S) +* S9) | S is Relation-like Function-like set
(id S) | S is Relation-like S -defined S -defined S -valued Function-like Element of K19(K20(S,S))
((id S) | S) +* (S9 | S) is Relation-like Function-like set
dom (id S) is non empty Element of K19(S)
K19(S) is set
(id S) | (dom (id S)) is Relation-like S -defined dom (id S) -defined S -defined S -valued Function-like Element of K19(K20(S,S))
((id S) | (dom (id S))) +* (S9 | S) is Relation-like Function-like set
S9 is set
S is set
A is Relation-like Function-like set
dom A is set
(S,A) is Relation-like S -defined Function-like total set
id S is Relation-like S -defined S -valued Function-like one-to-one total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
A | S is Relation-like Function-like set
(id S) +* (A | S) is Relation-like Function-like set
(S,A) . S9 is set
A . S9 is set
(id S) . S9 is set
(id S) +* A is Relation-like Function-like set
((id S) +* A) . S9 is set
S is set
S9 is Relation-like Function-like set
dom S9 is set
(S,S9) is Relation-like S -defined Function-like total set
id S is Relation-like S -defined S -valued Function-like one-to-one total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
S9 | S is Relation-like Function-like set
(id S) +* (S9 | S) is Relation-like Function-like set
dom (id S) is Element of K19(S)
K19(S) is set
S is set
S9 is Relation-like Function-like set
(S,S9) is Relation-like S -defined Function-like total set
id S is Relation-like S -defined S -valued Function-like one-to-one total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
S9 | S is Relation-like Function-like set
(id S) +* (S9 | S) is Relation-like Function-like set
(S,(S,S9)) is Relation-like S -defined Function-like total set
(S,S9) | S is Relation-like S -defined S -defined Function-like set
(id S) +* ((S,S9) | S) is Relation-like S -defined Function-like total set
dom (S,S9) is Element of K19(S)
K19(S) is set
A is set
(S,(S,S9)) . A is set
(S,S9) . A is set
S is set
id S is Relation-like S -defined S -valued Function-like one-to-one total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
S9 is Relation-like Function-like set
(id S) +* S9 is Relation-like Function-like set
(S,((id S) +* S9)) is Relation-like S -defined Function-like total set
((id S) +* S9) | S is Relation-like Function-like set
(id S) +* (((id S) +* S9) | S) is Relation-like Function-like set
(S,S9) is Relation-like S -defined Function-like total set
S9 | S is Relation-like Function-like set
(id S) +* (S9 | S) is Relation-like Function-like set
(id S) | S is Relation-like S -defined S -defined S -valued Function-like Element of K19(K20(S,S))
((id S) | S) +* (S9 | S) is Relation-like Function-like set
(id S) +* (((id S) | S) +* (S9 | S)) is Relation-like Function-like set
(id S) +* ((id S) +* (S9 | S)) is Relation-like Function-like set
(id S) +* (id S) is Relation-like S -defined S \/ S -defined S -valued Function-like total total V18(S,S) Element of K19(K20(S,S))
S \/ S is set
((id S) +* (id S)) +* (S9 | S) is Relation-like Function-like set
S is set
id S is Relation-like S -defined S -valued Function-like one-to-one total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
S9 is Relation-like Function-like set
(S,S9) is Relation-like S -defined Function-like total set
S9 | S is Relation-like Function-like set
(id S) +* (S9 | S) is Relation-like Function-like set
(id S) +* S9 is Relation-like Function-like set
(S,(id S)) is Relation-like S -defined Function-like total set
(id S) | S is Relation-like S -defined S -defined S -valued Function-like set
(id S) +* ((id S) | S) is Relation-like S -defined S -valued Function-like total set
S is set
(S,{}) is Relation-like S -defined Function-like total set
id S is Relation-like S -defined S -valued Function-like one-to-one total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
{} | S is Relation-like non-empty empty-yielding K97() -defined S -defined K97() -defined Function-like one-to-one constant functional empty V31() FinSequence-like FinSubsequence-like FinSequence-membered set
(id S) +* ({} | S) is Relation-like Function-like set
S is set
S9 is Relation-like Function-like set
dom S9 is set
(S,S9) is Relation-like S -defined Function-like total set
id S is Relation-like S -defined S -valued Function-like one-to-one total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
S9 | S is Relation-like Function-like set
(id S) +* (S9 | S) is Relation-like Function-like set
dom (S9 | S) is set
(S,(S9 | S)) is Relation-like S -defined Function-like total set
(S9 | S) | S is Relation-like Function-like set
(id S) +* ((S9 | S) | S) is Relation-like Function-like set
S is Relation-like Function-like set
({},S) is Relation-like non-empty empty-yielding {} -defined Function-like one-to-one constant functional empty total V31() FinSequence-like FinSubsequence-like FinSequence-membered set
id {} is Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional empty total V18( {} , {} ) V31() FinSequence-like FinSubsequence-like FinSequence-membered Element of K19(K20({},{}))
K20({},{}) is Relation-like set
K19(K20({},{})) is set
S | {} is Relation-like non-empty empty-yielding K97() -defined Function-like one-to-one constant functional empty V31() FinSequence-like FinSubsequence-like FinSequence-membered set
(id {}) +* (S | {}) is Relation-like non-empty Function-like set
S is set
S9 is set
A is Relation-like Function-like set
(S9,A) is Relation-like S9 -defined Function-like total set
id S9 is Relation-like S9 -defined S9 -valued Function-like one-to-one total V18(S9,S9) Element of K19(K20(S9,S9))
K20(S9,S9) is Relation-like set
K19(K20(S9,S9)) is set
A | S9 is Relation-like Function-like set
(id S9) +* (A | S9) is Relation-like Function-like set
(S9,A) | S is Relation-like S -defined S9 -defined Function-like set
(S,A) is Relation-like S -defined Function-like total set
id S is Relation-like S -defined S -valued Function-like one-to-one total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
A | S is Relation-like Function-like set
(id S) +* (A | S) is Relation-like Function-like set
(A | S9) | S is Relation-like Function-like set
(id S9) | S is Relation-like S -defined S9 -defined S9 -valued Function-like Element of K19(K20(S9,S9))
S is set
S9 is set
S \/ S9 is set
A is Relation-like Function-like set
((S \/ S9),A) is Relation-like S \/ S9 -defined Function-like total set
id (S \/ S9) is Relation-like S \/ S9 -defined S \/ S9 -valued Function-like one-to-one total V18(S \/ S9,S \/ S9) Element of K19(K20((S \/ S9),(S \/ S9)))
K20((S \/ S9),(S \/ S9)) is Relation-like set
K19(K20((S \/ S9),(S \/ S9))) is set
A | (S \/ S9) is Relation-like Function-like set
(id (S \/ S9)) +* (A | (S \/ S9)) is Relation-like Function-like set
(S,A) is Relation-like S -defined Function-like total set
id S is Relation-like S -defined S -valued Function-like one-to-one total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
A | S is Relation-like Function-like set
(id S) +* (A | S) is Relation-like Function-like set
(S9,A) is Relation-like S9 -defined Function-like total set
id S9 is Relation-like S9 -defined S9 -valued Function-like one-to-one total V18(S9,S9) Element of K19(K20(S9,S9))
K20(S9,S9) is Relation-like set
K19(K20(S9,S9)) is set
A | S9 is Relation-like Function-like set
(id S9) +* (A | S9) is Relation-like Function-like set
(S,A) +* (S9,A) is Relation-like S \/ S9 -defined Function-like total set
(A | S) \/ (A | S9) is Relation-like set
(A | S) +* (A | S9) is Relation-like Function-like set
dom (A | S) is set
dom A is set
(dom A) /\ S is set
dom (A | S9) is set
(dom A) /\ S9 is set
dom (id S9) is Element of K19(S9)
K19(S9) is set
(dom (A | S)) /\ (dom (id S9)) is Element of K19(S9)
(id S) +* (id S9) is Relation-like S \/ S9 -defined Function-like total set
((id S) +* (id S9)) +* (A | (S \/ S9)) is Relation-like Function-like set
((id S) +* (id S9)) +* ((A | S) +* (A | S9)) is Relation-like Function-like set
(id S9) +* ((A | S) +* (A | S9)) is Relation-like Function-like set
(id S) +* ((id S9) +* ((A | S) +* (A | S9))) is Relation-like Function-like set
(id S9) +* (A | S) is Relation-like Function-like set
((id S9) +* (A | S)) +* (A | S9) is Relation-like Function-like set
(id S) +* (((id S9) +* (A | S)) +* (A | S9)) is Relation-like Function-like set
(A | S) +* (id S9) is Relation-like Function-like set
((A | S) +* (id S9)) +* (A | S9) is Relation-like Function-like set
(id S) +* (((A | S) +* (id S9)) +* (A | S9)) is Relation-like Function-like set
(A | S) +* ((id S9) +* (A | S9)) is Relation-like Function-like set
(id S) +* ((A | S) +* ((id S9) +* (A | S9))) is Relation-like Function-like set
S is set
S9 is set
A is Relation-like Function-like set
(S,A) is Relation-like S -defined Function-like total set
id S is Relation-like S -defined S -valued Function-like one-to-one total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
A | S is Relation-like Function-like set
(id S) +* (A | S) is Relation-like Function-like set
(S9,A) is Relation-like S9 -defined Function-like total set
id S9 is Relation-like S9 -defined S9 -valued Function-like one-to-one total V18(S9,S9) Element of K19(K20(S9,S9))
K20(S9,S9) is Relation-like set
K19(K20(S9,S9)) is set
A | S9 is Relation-like Function-like set
(id S9) +* (A | S9) is Relation-like Function-like set
S \/ S9 is set
((S \/ S9),A) is Relation-like S \/ S9 -defined Function-like total set
id (S \/ S9) is Relation-like S \/ S9 -defined S \/ S9 -valued Function-like one-to-one total V18(S \/ S9,S \/ S9) Element of K19(K20((S \/ S9),(S \/ S9)))
K20((S \/ S9),(S \/ S9)) is Relation-like set
K19(K20((S \/ S9),(S \/ S9))) is set
A | (S \/ S9) is Relation-like Function-like set
(id (S \/ S9)) +* (A | (S \/ S9)) is Relation-like Function-like set
((S \/ S9),A) | S9 is Relation-like S9 -defined S \/ S9 -defined Function-like set
((S \/ S9),A) | S is Relation-like S -defined S \/ S9 -defined Function-like set
S is set
S9 is set
S \/ S9 is set
A is Relation-like Function-like set
((S \/ S9),A) is Relation-like S \/ S9 -defined Function-like total set
id (S \/ S9) is Relation-like S \/ S9 -defined S \/ S9 -valued Function-like one-to-one total V18(S \/ S9,S \/ S9) Element of K19(K20((S \/ S9),(S \/ S9)))
K20((S \/ S9),(S \/ S9)) is Relation-like set
K19(K20((S \/ S9),(S \/ S9))) is set
A | (S \/ S9) is Relation-like Function-like set
(id (S \/ S9)) +* (A | (S \/ S9)) is Relation-like Function-like set
(S,A) is Relation-like S -defined Function-like total set
id S is Relation-like S -defined S -valued Function-like one-to-one total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
A | S is Relation-like Function-like set
(id S) +* (A | S) is Relation-like Function-like set
(S9,A) is Relation-like S9 -defined Function-like total set
id S9 is Relation-like S9 -defined S9 -valued Function-like one-to-one total V18(S9,S9) Element of K19(K20(S9,S9))
K20(S9,S9) is Relation-like set
K19(K20(S9,S9)) is set
A | S9 is Relation-like Function-like set
(id S9) +* (A | S9) is Relation-like Function-like set
(S,A) \/ (S9,A) is Relation-like set
(S,A) +* (S9,A) is Relation-like S \/ S9 -defined Function-like total set
S is non empty set
id S is Relation-like S -defined S -valued Function-like one-to-one non empty total V18(S,S) Element of K19(K20(S,S))
K20(S,S) is Relation-like set
K19(K20(S,S)) is set
A is Relation-like Function-like set
rng A is set
S9 is Relation-like Function-like set
(S,S9) is Relation-like S -defined Function-like non empty total set
S9 | S is Relation-like Function-like set
(id S) +* (S9 | S) is Relation-like Function-like non empty set
A * (S,S9) is Relation-like Function-like set
(id S) +* S9 is Relation-like Function-like non empty set
A * ((id S) +* S9) is Relation-like Function-like set
dom (S,S9) is non empty Element of K19(S)
K19(S) is set
dom (A * (S,S9)) is set
dom A is set
E is set
(A * ((id S) +* S9)) . E is set
A . E is set
((id S) +* S9) . (A . E) is set
(A * (S,S9)) . E is set
(S,S9) . (A . E) is set
dom (id S) is non empty Element of K19(S)
dom ((id S) +* S9) is non empty set
dom S9 is set
S \/ (dom S9) is non empty set
dom (A * ((id S) +* S9)) is set
S is Relation-like Function-like set
dom S is set
S9 is Relation-like Function-like set
dom S9 is set
rng S9 is set
A is set
(A,S9) is Relation-like A -defined Function-like total set
id A is Relation-like A -defined A -valued Function-like one-to-one total V18(A,A) Element of K19(K20(A,A))
K20(A,A) is Relation-like set
K19(K20(A,A)) is set
S9 | A is Relation-like Function-like set
(id A) +* (S9 | A) is Relation-like Function-like set
(A,S9) * S is Relation-like A -defined Function-like set
S | A is Relation-like Function-like set
dom (S | A) is set
dom (S9 | A) is set
(id A) .: (dom (S9 | A)) is Element of K19(A)
K19(A) is set
E is set
dom (id A) is Element of K19(A)
x is set
(id A) . x is set
rng (S9 | A) is set
S9 .: A is set
(S9 .: A) /\ (dom S) is set
rng (A,S9) is set
A \ (dom S9) is Element of K19(A)
(A \ (dom S9)) \/ (S9 .: A) is set
(rng (A,S9)) /\ (dom S) is set
(A \ (dom S9)) /\ (dom S) is Element of K19(A)
((A \ (dom S9)) /\ (dom S)) \/ ((S9 .: A) /\ (dom S)) is set
A /\ (dom S) is set
((id A) +* (S9 | A)) * (S | A) is Relation-like Function-like set
(id A) * (S | A) is Relation-like A -defined Function-like set
S is Relation-like Function-like set
rng S is set
id (rng S) is Relation-like rng S -defined rng S -valued Function-like one-to-one total V18( rng S, rng S) Element of K19(K20((rng S),(rng S)))
K20((rng S),(rng S)) is Relation-like set
K19(K20((rng S),(rng S))) is set
dom (id (rng S)) is Element of K19((rng S))
K19((rng S)) is set
dom S is set
S9 is set
S9 is Relation-like Function-like set
dom S9 is set
rng S9 is set
A is set
S9 * S is Relation-like Function-like set
(S9 * S) . A is set
S9 . A is set
S . (S9 . A) is set
(id (rng S)) . A is set
dom (S9 * S) is set
S9 is Relation-like Function-like set
S is Relation-like Function-like set
rng S9 is set
dom S is set
dom S9 is set
rng S is set
S9 * S is Relation-like Function-like set
id (rng S) is Relation-like rng S -defined rng S -valued Function-like one-to-one total V18( rng S, rng S) Element of K19(K20((rng S),(rng S)))
K20((rng S),(rng S)) is Relation-like set
K19(K20((rng S),(rng S))) is set
dom (S9 * S) is set
S is Relation-like Function-like set
rng S is set
dom S is set
S9 is Relation-like Function-like (S)
A is set
S9 . A is set
S . (S9 . A) is set
rng S9 is set
dom S9 is set
S9 * S is Relation-like Function-like set
(S9 * S) . A is set
id (rng S) is Relation-like rng S -defined rng S -valued Function-like one-to-one total V18( rng S, rng S) Element of K19(K20((rng S),(rng S)))
K20((rng S),(rng S)) is Relation-like set
K19(K20((rng S),(rng S))) is set
(id (rng S)) . A is set
S is Relation-like Function-like set
S " is Relation-like Function-like set
dom (S ") is set
rng S is set
(S ") * S is Relation-like Function-like set
id (rng S) is Relation-like rng S -defined rng S -valued Function-like one-to-one total V18( rng S, rng S) Element of K19(K20((rng S),(rng S)))
K20((rng S),(rng S)) is Relation-like set
K19(K20((rng S),(rng S))) is set
S is Relation-like Function-like set
S " is Relation-like Function-like set
S9 is Relation-like Function-like (S)
rng S is set
dom S9 is set
rng S9 is set
dom S is set
A is set
S . A is set
S9 . (S . A) is set
S . (S9 . (S . A)) is set
A is set
E is set
S9 . E is set
S . (S9 . E) is set
S . A is set
S is Relation-like Function-like set
S9 is Relation-like Function-like set
S +* S9 is Relation-like Function-like set
S \/ S9 is Relation-like set
A is Relation-like Function-like (S)
E is Relation-like Function-like (S9)
A +* E is Relation-like Function-like set
dom A is set
rng S is set
dom E is set
rng S9 is set
dom (A +* E) is set
(dom A) \/ (dom E) is set
rng (S +* S9) is set
(A +* E) * (S +* S9) is Relation-like Function-like set
id (rng (S +* S9)) is Relation-like rng (S +* S9) -defined rng (S +* S9) -valued Function-like one-to-one total V18( rng (S +* S9), rng (S +* S9)) Element of K19(K20((rng (S +* S9)),(rng (S +* S9))))
K20((rng (S +* S9)),(rng (S +* S9))) is Relation-like set
K19(K20((rng (S +* S9)),(rng (S +* S9)))) is set
rng E is set
dom S9 is set
rng A is set
dom S is set
A * S is Relation-like Function-like set
E * S9 is Relation-like Function-like set
(A * S) +* (E * S9) is Relation-like Function-like set
id (rng S) is Relation-like rng S -defined rng S -valued Function-like one-to-one total V18( rng S, rng S) Element of K19(K20((rng S),(rng S)))
K20((rng S),(rng S)) is Relation-like set
K19(K20((rng S),(rng S))) is set
(id (rng S)) +* (E * S9) is Relation-like Function-like set
id (rng S9) is Relation-like rng S9 -defined rng S9 -valued Function-like one-to-one total V18( rng S9, rng S9) Element of K19(K20((rng S9),(rng S9)))
K20((rng S9),(rng S9)) is Relation-like set
K19(K20((rng S9),(rng S9))) is set
(id (rng S)) +* (id (rng S9)) is Relation-like (rng S) \/ (rng S9) -defined Function-like total set
(rng S) \/ (rng S9) is set
id ((rng S) \/ (rng S9)) is Relation-like (rng S) \/ (rng S9) -defined (rng S) \/ (rng S9) -valued Function-like one-to-one total V18((rng S) \/ (rng S9),(rng S) \/ (rng S9)) Element of K19(K20(((rng S) \/ (rng S9)),((rng S) \/ (rng S9))))
K20(((rng S) \/ (rng S9)),((rng S) \/ (rng S9))) is Relation-like set
K19(K20(((rng S) \/ (rng S9)),((rng S) \/ (rng S9)))) is set
S is Relation-like Function-like set
S9 is Relation-like Function-like set
S9 +* S is Relation-like Function-like set
the Relation-like Function-like (S9) is Relation-like Function-like (S9)
E is Relation-like Function-like (S)
the Relation-like Function-like (S9) +* E is Relation-like Function-like set
x is Relation-like Function-like (S9)
S is non empty non void feasible feasible ManySortedSign
the carrier' of S is non empty set
the carrier of S is non empty set
S9 is Relation-like Function-like set
A is Relation-like Function-like set
( the carrier' of S,A) is Relation-like the carrier' of S -defined Function-like non empty total set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
A | the carrier' of S is Relation-like Function-like set
(id the carrier' of S) +* (A | the carrier' of S) is Relation-like Function-like non empty set
( the carrier of S,S9) is Relation-like the carrier of S -defined Function-like non empty total set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
S9 | the carrier of S is Relation-like Function-like set
(id the carrier of S) +* (S9 | the carrier of S) is Relation-like Function-like non empty set
E is Element of the carrier' of S
the_arity_of E is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of S . E is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
rng (the_arity_of E) is Element of K19( the carrier of S)
K19( the carrier of S) is set
x is Element of the carrier' of S
the_arity_of x is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . x is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
rng (the_arity_of x) is Element of K19( the carrier of S)
( the carrier' of S,A) . E is set
( the carrier' of S,A) . x is set
(id the carrier' of S) +* A is Relation-like Function-like non empty set
((id the carrier' of S) +* A) . E is set
((id the carrier' of S) +* A) . x is set
(id the carrier of S) +* S9 is Relation-like Function-like non empty set
(the_arity_of E) * ((id the carrier of S) +* S9) is Relation-like K97() -defined Function-like set
(the_arity_of x) * ((id the carrier of S) +* S9) is Relation-like K97() -defined Function-like set
(the_arity_of E) * ( the carrier of S,S9) is Relation-like K97() -defined Function-like set
(the_arity_of x) * ( the carrier of S,S9) is Relation-like K97() -defined Function-like set
the_result_sort_of E is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S . E is Element of the carrier of S
( the carrier of S,S9) . (the_result_sort_of E) is set
((id the carrier of S) +* S9) . (the_result_sort_of E) is set
the_result_sort_of x is Element of the carrier of S
the ResultSort of S . x is Element of the carrier of S
((id the carrier of S) +* S9) . (the_result_sort_of x) is set
( the carrier of S,S9) . (the_result_sort_of x) is set
E is Element of the carrier' of S
((id the carrier' of S) +* A) . E is set
x is Element of the carrier' of S
((id the carrier' of S) +* A) . x is set
the_arity_of E is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . E is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of E) * ((id the carrier of S) +* S9) is Relation-like K97() -defined Function-like set
the_arity_of x is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . x is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of x) * ((id the carrier of S) +* S9) is Relation-like K97() -defined Function-like set
the_result_sort_of E is Element of the carrier of S
the ResultSort of S . E is Element of the carrier of S
((id the carrier of S) +* S9) . (the_result_sort_of E) is set
the_result_sort_of x is Element of the carrier of S
the ResultSort of S . x is Element of the carrier of S
((id the carrier of S) +* S9) . (the_result_sort_of x) is set
rng (the_arity_of E) is Element of K19( the carrier of S)
rng (the_arity_of x) is Element of K19( the carrier of S)
( the carrier' of S,A) . E is set
( the carrier' of S,A) . x is set
(the_arity_of E) * ( the carrier of S,S9) is Relation-like K97() -defined Function-like set
(the_arity_of x) * ( the carrier of S,S9) is Relation-like K97() -defined Function-like set
( the carrier of S,S9) . (the_result_sort_of E) is set
( the carrier of S,S9) . (the_result_sort_of x) is set
S is non empty non void feasible feasible ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
S9 is Relation-like Function-like set
A is Relation-like Function-like set
( the carrier of S,S9) is Relation-like the carrier of S -defined Function-like non empty total set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
S9 | the carrier of S is Relation-like Function-like set
(id the carrier of S) +* (S9 | the carrier of S) is Relation-like Function-like non empty set
( the carrier' of S,A) is Relation-like the carrier' of S -defined Function-like non empty total set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
A | the carrier' of S is Relation-like Function-like set
(id the carrier' of S) +* (A | the carrier' of S) is Relation-like Function-like non empty set
(id the carrier' of S) +* (id the carrier' of S) is Relation-like the carrier' of S -defined the carrier' of S \/ the carrier' of S -defined the carrier' of S -valued Function-like non empty total total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
the carrier' of S \/ the carrier' of S is non empty set
(id the carrier' of S) +* ((id the carrier' of S) +* (A | the carrier' of S)) is Relation-like Function-like non empty set
(id the carrier of S) +* (id the carrier of S) is Relation-like the carrier of S -defined the carrier of S \/ the carrier of S -defined the carrier of S -valued Function-like non empty total total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
the carrier of S \/ the carrier of S is non empty set
(id the carrier of S) +* ((id the carrier of S) +* (S9 | the carrier of S)) is Relation-like Function-like non empty set
E is Element of the carrier' of S
( the carrier' of S,A) . E is set
x is Element of the carrier' of S
( the carrier' of S,A) . x is set
the_arity_of E is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of S . E is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of E) * ( the carrier of S,S9) is Relation-like K97() -defined Function-like set
the_arity_of x is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . x is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of x) * ( the carrier of S,S9) is Relation-like K97() -defined Function-like set
the_result_sort_of E is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S . E is Element of the carrier of S
( the carrier of S,S9) . (the_result_sort_of E) is set
the_result_sort_of x is Element of the carrier of S
the ResultSort of S . x is Element of the carrier of S
( the carrier of S,S9) . (the_result_sort_of x) is set
E is Element of the carrier' of S
( the carrier' of S,A) . E is set
x is Element of the carrier' of S
( the carrier' of S,A) . x is set
the_arity_of E is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of S . E is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of E) * ( the carrier of S,S9) is Relation-like K97() -defined Function-like set
the_arity_of x is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . x is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of x) * ( the carrier of S,S9) is Relation-like K97() -defined Function-like set
the_result_sort_of E is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S . E is Element of the carrier of S
( the carrier of S,S9) . (the_result_sort_of E) is set
the_result_sort_of x is Element of the carrier of S
the ResultSort of S . x is Element of the carrier of S
( the carrier of S,S9) . (the_result_sort_of x) is set
S is non empty non void feasible feasible ManySortedSign
S9 is non empty non void feasible feasible ManySortedSign
A is Relation-like Function-like set
E is Relation-like Function-like set
the carrier of S is non empty set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
dom (id the carrier of S) is non empty Element of K19( the carrier of S)
K19( the carrier of S) is set
the carrier' of S is non empty set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
dom (id the carrier' of S) is non empty Element of K19( the carrier' of S)
K19( the carrier' of S) is set
dom E is set
(id the carrier' of S) +* E is Relation-like Function-like non empty set
x is Element of the carrier' of S
((id the carrier' of S) +* E) . x is set
o is Element of the carrier' of S
((id the carrier' of S) +* E) . o is set
the_arity_of x is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of S . x is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
(id the carrier of S) +* A is Relation-like Function-like non empty set
(the_arity_of x) * ((id the carrier of S) +* A) is Relation-like K97() -defined Function-like set
the_arity_of o is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . o is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of o) * ((id the carrier of S) +* A) is Relation-like K97() -defined Function-like set
the_result_sort_of x is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S . x is Element of the carrier of S
((id the carrier of S) +* A) . (the_result_sort_of x) is set
the_result_sort_of o is Element of the carrier of S
the ResultSort of S . o is Element of the carrier of S
((id the carrier of S) +* A) . (the_result_sort_of o) is set
dom A is set
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like non empty total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
the carrier' of S9 is non empty set
the carrier of S9 is non empty set
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set
E . x is set
the Arity of S9 . (E . x) is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
K20( the carrier' of S, the carrier' of S9) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S9)) is set
the ResultSort of S * A is Relation-like the carrier' of S -defined Function-like set
( the ResultSort of S * A) . x is set
the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like non empty total V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
K20( the carrier' of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier of S9)) is set
E * the ResultSort of S9 is Relation-like the carrier of S9 -valued Function-like set
(E * the ResultSort of S9) . x is set
e is Relation-like the carrier' of S -defined the carrier' of S9 -valued Function-like non empty total V18( the carrier' of S, the carrier' of S9) Element of K19(K20( the carrier' of S, the carrier' of S9))
e . x is Element of the carrier' of S9
the ResultSort of S9 . (e . x) is Element of the carrier of S9
the ResultSort of S9 * e is Relation-like the carrier' of S -defined the carrier of S9 -valued Function-like non empty total V18( the carrier' of S, the carrier of S9) Element of K19(K20( the carrier' of S, the carrier of S9))
K20( the carrier' of S, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S, the carrier of S9)) is set
( the ResultSort of S9 * e) . o is Element of the carrier of S9
( the ResultSort of S * A) . o is set
S is non empty non void feasible feasible ManySortedSign
S9 is Relation-like Function-like set
the carrier' of S is non empty set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
(id the carrier' of S) +* {} is Relation-like Function-like non empty set
A is Element of the carrier' of S
((id the carrier' of S) +* {}) . A is set
E is Element of the carrier' of S
((id the carrier' of S) +* {}) . E is set
the_arity_of A is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S is non empty set
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of S . A is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
(id the carrier of S) +* S9 is Relation-like Function-like non empty set
(the_arity_of A) * ((id the carrier of S) +* S9) is Relation-like K97() -defined Function-like set
the_arity_of E is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . E is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of E) * ((id the carrier of S) +* S9) is Relation-like K97() -defined Function-like set
the_result_sort_of A is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S . A is Element of the carrier of S
((id the carrier of S) +* S9) . (the_result_sort_of A) is set
the_result_sort_of E is Element of the carrier of S
the ResultSort of S . E is Element of the carrier of S
((id the carrier of S) +* S9) . (the_result_sort_of E) is set
(id the carrier' of S) . E is Element of the carrier' of S
S is non empty non void feasible feasible ManySortedSign
the carrier' of S is non empty set
S9 is Relation-like Function-like set
rng S9 is set
the carrier' of S /\ (rng S9) is set
dom S9 is set
A is Relation-like Function-like set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
(id the carrier' of S) +* S9 is Relation-like Function-like non empty set
E is Element of the carrier' of S
((id the carrier' of S) +* S9) . E is set
x is Element of the carrier' of S
((id the carrier' of S) +* S9) . x is set
the_arity_of E is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S is non empty set
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of S . E is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
(id the carrier of S) +* A is Relation-like Function-like non empty set
(the_arity_of E) * ((id the carrier of S) +* A) is Relation-like K97() -defined Function-like set
the_arity_of x is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . x is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of x) * ((id the carrier of S) +* A) is Relation-like K97() -defined Function-like set
the_result_sort_of E is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S . E is Element of the carrier of S
((id the carrier of S) +* A) . (the_result_sort_of E) is set
the_result_sort_of x is Element of the carrier of S
the ResultSort of S . x is Element of the carrier of S
((id the carrier of S) +* A) . (the_result_sort_of x) is set
(id the carrier' of S) . E is Element of the carrier' of S
(id the carrier' of S) . x is Element of the carrier' of S
S9 . E is set
S9 . x is set
S9 . x is set
S is non empty non void feasible feasible ManySortedSign
the carrier' of S is non empty set
S9 is Relation-like Function-like set
rng S9 is set
A is Relation-like Function-like set
the carrier' of S /\ (rng S9) is set
dom S9 is set
S9 is non empty set
S is set
S * is functional non empty FinSequence-membered M11(S)
K20(S9,(S *)) is Relation-like set
K19(K20(S9,(S *))) is set
K20(S9,S) is Relation-like set
K19(K20(S9,S)) is set
A is Relation-like S9 -defined S * -valued Function-like non empty total V18(S9,S * ) Element of K19(K20(S9,(S *)))
E is Relation-like S9 -defined S -valued Function-like V18(S9,S) Element of K19(K20(S9,S))
ManySortedSign(# S,S9,A,E #) is strict ManySortedSign
S is non empty non void feasible feasible ManySortedSign
S9 is Relation-like Function-like set
A is Relation-like Function-like set
the carrier of S is non empty set
( the carrier of S,S9) is Relation-like the carrier of S -defined Function-like non empty total set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
S9 | the carrier of S is Relation-like Function-like set
(id the carrier of S) +* (S9 | the carrier of S) is Relation-like Function-like non empty set
the carrier' of S is non empty set
( the carrier' of S,A) is Relation-like the carrier' of S -defined Function-like non empty total set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
A | the carrier' of S is Relation-like Function-like set
(id the carrier' of S) +* (A | the carrier' of S) is Relation-like Function-like non empty set
rng ( the carrier of S,S9) is non empty set
rng ( the carrier' of S,A) is non empty set
p is non empty non void feasible strict feasible ManySortedSign
the carrier of p is non empty set
the carrier' of p is non empty set
q is non empty non void feasible strict feasible ManySortedSign
the carrier of q is non empty set
the carrier' of q is non empty set
the ResultSort of p is Relation-like the carrier' of p -defined the carrier of p -valued Function-like non empty total V18( the carrier' of p, the carrier of p) Element of K19(K20( the carrier' of p, the carrier of p))
K20( the carrier' of p, the carrier of p) is Relation-like set
K19(K20( the carrier' of p, the carrier of p)) is set
the ResultSort of q is Relation-like the carrier' of q -defined the carrier of q -valued Function-like non empty total V18( the carrier' of q, the carrier of q) Element of K19(K20( the carrier' of q, the carrier of q))
K20( the carrier' of q, the carrier of q) is Relation-like set
K19(K20( the carrier' of q, the carrier of q)) is set
gg is Element of the carrier' of p
the ResultSort of p . gg is set
the ResultSort of q . gg is set
dom ( the carrier' of S,A) is non empty Element of K19( the carrier' of S)
K19( the carrier' of S) is set
FS is set
( the carrier' of S,A) . FS is set
p is set
( the carrier' of S,A) . p is set
the ResultSort of p . gg is Element of the carrier of p
( the carrier' of S,A) * the ResultSort of p is Relation-like the carrier' of S -defined the carrier of p -valued Function-like set
a is Element of the carrier' of S
(( the carrier' of S,A) * the ResultSort of p) . a is set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S * ( the carrier of S,S9) is Relation-like the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * ( the carrier of S,S9)) . a is set
the_result_sort_of a is Element of the carrier of S
the ResultSort of S . a is Element of the carrier of S
( the carrier of S,S9) . (the_result_sort_of a) is set
r is Element of the carrier' of S
the_result_sort_of r is Element of the carrier of S
the ResultSort of S . r is Element of the carrier of S
( the carrier of S,S9) . (the_result_sort_of r) is set
( the ResultSort of S * ( the carrier of S,S9)) . r is set
( the carrier' of S,A) * the ResultSort of q is Relation-like the carrier' of S -defined the carrier of q -valued Function-like set
(( the carrier' of S,A) * the ResultSort of q) . r is set
the carrier of p * is functional non empty FinSequence-membered M11( the carrier of p)
the carrier of q * is functional non empty FinSequence-membered M11( the carrier of q)
the Arity of p is Relation-like the carrier' of p -defined the carrier of p * -valued Function-like non empty total V18( the carrier' of p, the carrier of p * ) Element of K19(K20( the carrier' of p,( the carrier of p *)))
K20( the carrier' of p,( the carrier of p *)) is Relation-like set
K19(K20( the carrier' of p,( the carrier of p *))) is set
the Arity of q is Relation-like the carrier' of q -defined the carrier of q * -valued Function-like non empty total V18( the carrier' of q, the carrier of q * ) Element of K19(K20( the carrier' of q,( the carrier of q *)))
K20( the carrier' of q,( the carrier of q *)) is Relation-like set
K19(K20( the carrier' of q,( the carrier of q *))) is set
gg is Element of the carrier' of p
the Arity of p . gg is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
the Arity of q . gg is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
dom ( the carrier' of S,A) is non empty Element of K19( the carrier' of S)
K19( the carrier' of S) is set
FS is set
( the carrier' of S,A) . FS is set
the Arity of p . gg is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of p *
p is Element of the carrier' of S
the_arity_of p is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of S . p is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of p) * ( the carrier of S,S9) is Relation-like K97() -defined Function-like set
dom ( the carrier' of S,A) is non empty Element of K19( the carrier' of S)
K19( the carrier' of S) is set
q is non empty set
K20( the carrier' of S,q) is Relation-like set
K19(K20( the carrier' of S,q)) is set
gg is Relation-like the carrier' of S -defined q -valued Function-like non empty total V18( the carrier' of S,q) Element of K19(K20( the carrier' of S,q))
the Relation-like Function-like (gg) is Relation-like Function-like (gg)
rng the Relation-like Function-like (gg) is set
dom the Relation-like Function-like (gg) is set
rng gg is non empty Element of K19(q)
K19(q) is set
K20(q, the carrier' of S) is Relation-like set
K19(K20(q, the carrier' of S)) is set
dom ( the carrier of S,S9) is non empty Element of K19( the carrier of S)
K19( the carrier of S) is set
p is non empty set
K20( the carrier of S,p) is Relation-like set
K19(K20( the carrier of S,p)) is set
p is Relation-like q -defined the carrier' of S -valued Function-like non empty total V18(q, the carrier' of S) Element of K19(K20(q, the carrier' of S))
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
a is Relation-like the carrier of S -defined p -valued Function-like non empty total V18( the carrier of S,p) Element of K19(K20( the carrier of S,p))
a * the ResultSort of S is Relation-like the carrier' of S -defined p -valued Function-like non empty total V18( the carrier' of S,p) Element of K19(K20( the carrier' of S,p))
K20( the carrier' of S,p) is Relation-like set
K19(K20( the carrier' of S,p)) is set
(a * the ResultSort of S) * p is Relation-like q -defined p -valued Function-like non empty total V18(q,p) Element of K19(K20(q,p))
K20(q,p) is Relation-like set
K19(K20(q,p)) is set
p * is functional non empty FinSequence-membered M11(p)
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
a * is Relation-like the carrier of S * -defined p * -valued Function-like non empty total V18( the carrier of S * ,p * ) Element of K19(K20(( the carrier of S *),(p *)))
K20(( the carrier of S *),(p *)) is Relation-like set
K19(K20(( the carrier of S *),(p *))) is set
(a *) * the Arity of S is Relation-like the carrier' of S -defined p * -valued Function-like non empty total V18( the carrier' of S,p * ) Element of K19(K20( the carrier' of S,(p *)))
K20( the carrier' of S,(p *)) is Relation-like set
K19(K20( the carrier' of S,(p *))) is set
((a *) * the Arity of S) * p is Relation-like q -defined p * -valued Function-like non empty total V18(q,p * ) Element of K19(K20(q,(p *)))
K20(q,(p *)) is Relation-like set
K19(K20(q,(p *))) is set
ManySortedSign(# p,q,(((a *) * the Arity of S) * p),((a * the ResultSort of S) * p) #) is non empty non void feasible strict feasible ManySortedSign
R is non empty non void feasible strict feasible ManySortedSign
the carrier of R is non empty set
the carrier' of R is non empty set
the ResultSort of S * ( the carrier of S,S9) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of R is Relation-like the carrier' of R -defined the carrier of R -valued Function-like non empty total V18( the carrier' of R, the carrier of R) Element of K19(K20( the carrier' of R, the carrier of R))
K20( the carrier' of R, the carrier of R) is Relation-like set
K19(K20( the carrier' of R, the carrier of R)) is set
( the carrier' of S,A) * the ResultSort of R is Relation-like the carrier' of S -defined the carrier of R -valued Function-like set
the Arity of R is Relation-like the carrier' of R -defined the carrier of R * -valued Function-like non empty total V18( the carrier' of R, the carrier of R * ) Element of K19(K20( the carrier' of R,( the carrier of R *)))
the carrier of R * is functional non empty FinSequence-membered M11( the carrier of R)
K20( the carrier' of R,( the carrier of R *)) is Relation-like set
K19(K20( the carrier' of R,( the carrier of R *))) is set
o is Element of the carrier' of S
gg . o is Element of q
p . (gg . o) is Element of the carrier' of S
gg . (p . (gg . o)) is Element of q
((a * the ResultSort of S) * p) * gg is Relation-like the carrier' of S -defined p -valued Function-like non empty total V18( the carrier' of S,p) Element of K19(K20( the carrier' of S,p))
(((a * the ResultSort of S) * p) * gg) . o is Element of p
the ResultSort of R . (gg . o) is set
(a * the ResultSort of S) . (p . (gg . o)) is Element of p
the_result_sort_of (p . (gg . o)) is Element of the carrier of S
the ResultSort of S . (p . (gg . o)) is Element of the carrier of S
a . (the_result_sort_of (p . (gg . o))) is Element of p
the_result_sort_of o is Element of the carrier of S
the ResultSort of S . o is Element of the carrier of S
a . (the_result_sort_of o) is Element of p
(a * the ResultSort of S) . o is Element of p
o is set
the Arity of S . o is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
( the carrier' of S,A) . o is set
the Arity of R . (( the carrier' of S,A) . o) is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
p is Relation-like Function-like set
p * ( the carrier of S,S9) is Relation-like Function-like set
x is Element of the carrier' of S
gg . x is Element of q
p . (gg . x) is Element of the carrier' of S
gg . (p . (gg . x)) is Element of q
the_arity_of x is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . x is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
a * (the_arity_of x) is Relation-like K97() -defined p -valued Function-like V31() FinSequence-like FinSubsequence-like Element of p *
the_arity_of (p . (gg . x)) is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . (p . (gg . x)) is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
a * (the_arity_of (p . (gg . x))) is Relation-like K97() -defined p -valued Function-like V31() FinSequence-like FinSubsequence-like Element of p *
(a *) . (the_arity_of (p . (gg . x))) is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of p *
((a *) * the Arity of S) . (p . (gg . x)) is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of p *
S is non empty non void feasible feasible ManySortedSign
the carrier of S is non empty set
S9 is non empty non void feasible feasible ManySortedSign
the carrier of S9 is non empty set
K20( the carrier of S, the carrier of S9) is Relation-like set
K19(K20( the carrier of S, the carrier of S9)) is set
the carrier' of S is non empty set
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like non empty total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
the carrier' of S9 is non empty set
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set
A is Relation-like the carrier of S -defined the carrier of S9 -valued Function-like non empty total V18( the carrier of S, the carrier of S9) Element of K19(K20( the carrier of S, the carrier of S9))
A * is Relation-like the carrier of S * -defined the carrier of S9 * -valued Function-like non empty total V18( the carrier of S * , the carrier of S9 * ) Element of K19(K20(( the carrier of S *),( the carrier of S9 *)))
K20(( the carrier of S *),( the carrier of S9 *)) is Relation-like set
K19(K20(( the carrier of S *),( the carrier of S9 *))) is set
(A *) * the Arity of S is Relation-like the carrier' of S -defined the carrier of S9 * -valued Function-like non empty total V18( the carrier' of S, the carrier of S9 * ) Element of K19(K20( the carrier' of S,( the carrier of S9 *)))
K20( the carrier' of S,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S9 *))) is set
E is Relation-like Function-like set
E * the Arity of S9 is Relation-like the carrier of S9 * -valued Function-like set
dom the Arity of S9 is non empty Element of K19( the carrier' of S9)
K19( the carrier' of S9) is set
dom ((A *) * the Arity of S) is non empty Element of K19( the carrier' of S)
K19( the carrier' of S) is set
dom E is set
dom the Arity of S is non empty Element of K19( the carrier' of S)
x is set
the Arity of S . x is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
rng the Arity of S is functional non empty FinSequence-membered Element of K19(( the carrier of S *))
K19(( the carrier of S *)) is set
((A *) * the Arity of S) . x is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
o is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the carrier of S
(A *) . o is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
A * o is Relation-like K97() -defined the carrier of S9 -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S9 *
E . x is set
the Arity of S9 . (E . x) is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
(E * the Arity of S9) . x is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
rng E is set
dom (E * the Arity of S9) is set
S is non empty non void feasible feasible ManySortedSign
the carrier of S is non empty set
S9 is Relation-like Function-like set
( the carrier of S,S9) is Relation-like the carrier of S -defined Function-like non empty total set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
S9 | the carrier of S is Relation-like Function-like set
(id the carrier of S) +* (S9 | the carrier of S) is Relation-like Function-like non empty set
A is Relation-like Function-like set
(S,S9,A) is non empty non void feasible strict feasible ManySortedSign
the carrier of (S,S9,A) is non empty set
K20( the carrier of S, the carrier of (S,S9,A)) is Relation-like set
K19(K20( the carrier of S, the carrier of (S,S9,A))) is set
the carrier' of S is non empty set
( the carrier' of S,A) is Relation-like the carrier' of S -defined Function-like non empty total set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
A | the carrier' of S is Relation-like Function-like set
(id the carrier' of S) +* (A | the carrier' of S) is Relation-like Function-like non empty set
S is non empty non void feasible feasible ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
S9 is Relation-like Function-like set
( the carrier of S,S9) is Relation-like the carrier of S -defined Function-like non empty total set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
S9 | the carrier of S is Relation-like Function-like set
(id the carrier of S) +* (S9 | the carrier of S) is Relation-like Function-like non empty set
A is Relation-like Function-like set
(S,S9,A) is non empty non void feasible strict feasible ManySortedSign
the carrier of (S,S9,A) is non empty set
K20( the carrier of S, the carrier of (S,S9,A)) is Relation-like set
K19(K20( the carrier of S, the carrier of (S,S9,A))) is set
( the carrier' of S,A) is Relation-like the carrier' of S -defined Function-like non empty total set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
A | the carrier' of S is Relation-like Function-like set
(id the carrier' of S) +* (A | the carrier' of S) is Relation-like Function-like non empty set
the Arity of (S,S9,A) is Relation-like the carrier' of (S,S9,A) -defined the carrier of (S,S9,A) * -valued Function-like non empty total V18( the carrier' of (S,S9,A), the carrier of (S,S9,A) * ) Element of K19(K20( the carrier' of (S,S9,A),( the carrier of (S,S9,A) *)))
the carrier' of (S,S9,A) is non empty set
the carrier of (S,S9,A) * is functional non empty FinSequence-membered M11( the carrier of (S,S9,A))
K20( the carrier' of (S,S9,A),( the carrier of (S,S9,A) *)) is Relation-like set
K19(K20( the carrier' of (S,S9,A),( the carrier of (S,S9,A) *))) is set
e is Relation-like the carrier of S -defined the carrier of (S,S9,A) -valued Function-like non empty total V18( the carrier of S, the carrier of (S,S9,A)) Element of K19(K20( the carrier of S, the carrier of (S,S9,A)))
e * is Relation-like the carrier of S * -defined the carrier of (S,S9,A) * -valued Function-like non empty total V18( the carrier of S * , the carrier of (S,S9,A) * ) Element of K19(K20(( the carrier of S *),( the carrier of (S,S9,A) *)))
K20(( the carrier of S *),( the carrier of (S,S9,A) *)) is Relation-like set
K19(K20(( the carrier of S *),( the carrier of (S,S9,A) *))) is set
(e *) * the Arity of S is Relation-like the carrier' of S -defined the carrier of (S,S9,A) * -valued Function-like non empty total V18( the carrier' of S, the carrier of (S,S9,A) * ) Element of K19(K20( the carrier' of S,( the carrier of (S,S9,A) *)))
K20( the carrier' of S,( the carrier of (S,S9,A) *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of (S,S9,A) *))) is set
p is Relation-like Function-like (( the carrier' of S,A))
p * ((e *) * the Arity of S) is Relation-like the carrier of (S,S9,A) * -valued Function-like set
rng ( the carrier' of S,A) is non empty set
id (rng ( the carrier' of S,A)) is Relation-like rng ( the carrier' of S,A) -defined rng ( the carrier' of S,A) -valued Function-like one-to-one non empty total V18( rng ( the carrier' of S,A), rng ( the carrier' of S,A)) Element of K19(K20((rng ( the carrier' of S,A)),(rng ( the carrier' of S,A))))
K20((rng ( the carrier' of S,A)),(rng ( the carrier' of S,A))) is Relation-like set
K19(K20((rng ( the carrier' of S,A)),(rng ( the carrier' of S,A)))) is set
the Arity of (S,S9,A) * (id (rng ( the carrier' of S,A))) is Relation-like rng ( the carrier' of S,A) -defined the carrier of (S,S9,A) * -valued Function-like Element of K19(K20((rng ( the carrier' of S,A)),( the carrier of (S,S9,A) *)))
K20((rng ( the carrier' of S,A)),( the carrier of (S,S9,A) *)) is Relation-like set
K19(K20((rng ( the carrier' of S,A)),( the carrier of (S,S9,A) *))) is set
p * ( the carrier' of S,A) is Relation-like Function-like set
(p * ( the carrier' of S,A)) * the Arity of (S,S9,A) is Relation-like the carrier of (S,S9,A) * -valued Function-like set
( the carrier' of S,A) * the Arity of (S,S9,A) is Relation-like the carrier' of S -defined the carrier of (S,S9,A) * -valued Function-like set
p * (( the carrier' of S,A) * the Arity of (S,S9,A)) is Relation-like the carrier of (S,S9,A) * -valued Function-like set
S is non empty non void feasible feasible ManySortedSign
the carrier' of S is non empty set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
the carrier of S is non empty set
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
S9 is Relation-like Function-like set
( the carrier of S,S9) is Relation-like the carrier of S -defined Function-like non empty total set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
S9 | the carrier of S is Relation-like Function-like set
(id the carrier of S) +* (S9 | the carrier of S) is Relation-like Function-like non empty set
the ResultSort of S * ( the carrier of S,S9) is Relation-like the carrier' of S -defined Function-like non empty total set
A is Relation-like Function-like set
( the carrier' of S,A) is Relation-like the carrier' of S -defined Function-like non empty total set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
A | the carrier' of S is Relation-like Function-like set
(id the carrier' of S) +* (A | the carrier' of S) is Relation-like Function-like non empty set
(S,S9,A) is non empty non void feasible strict feasible ManySortedSign
the ResultSort of (S,S9,A) is Relation-like the carrier' of (S,S9,A) -defined the carrier of (S,S9,A) -valued Function-like non empty total V18( the carrier' of (S,S9,A), the carrier of (S,S9,A)) Element of K19(K20( the carrier' of (S,S9,A), the carrier of (S,S9,A)))
the carrier' of (S,S9,A) is non empty set
the carrier of (S,S9,A) is non empty set
K20( the carrier' of (S,S9,A), the carrier of (S,S9,A)) is Relation-like set
K19(K20( the carrier' of (S,S9,A), the carrier of (S,S9,A))) is set
e is Relation-like Function-like (( the carrier' of S,A))
e * ( the ResultSort of S * ( the carrier of S,S9)) is Relation-like Function-like set
rng ( the carrier' of S,A) is non empty set
id (rng ( the carrier' of S,A)) is Relation-like rng ( the carrier' of S,A) -defined rng ( the carrier' of S,A) -valued Function-like one-to-one non empty total V18( rng ( the carrier' of S,A), rng ( the carrier' of S,A)) Element of K19(K20((rng ( the carrier' of S,A)),(rng ( the carrier' of S,A))))
K20((rng ( the carrier' of S,A)),(rng ( the carrier' of S,A))) is Relation-like set
K19(K20((rng ( the carrier' of S,A)),(rng ( the carrier' of S,A)))) is set
the ResultSort of (S,S9,A) * (id (rng ( the carrier' of S,A))) is Relation-like rng ( the carrier' of S,A) -defined the carrier of (S,S9,A) -valued Function-like Element of K19(K20((rng ( the carrier' of S,A)), the carrier of (S,S9,A)))
K20((rng ( the carrier' of S,A)), the carrier of (S,S9,A)) is Relation-like set
K19(K20((rng ( the carrier' of S,A)), the carrier of (S,S9,A))) is set
e * ( the carrier' of S,A) is Relation-like Function-like set
(e * ( the carrier' of S,A)) * the ResultSort of (S,S9,A) is Relation-like the carrier of (S,S9,A) -valued Function-like set
( the carrier' of S,A) * the ResultSort of (S,S9,A) is Relation-like the carrier' of S -defined the carrier of (S,S9,A) -valued Function-like set
e * (( the carrier' of S,A) * the ResultSort of (S,S9,A)) is Relation-like the carrier of (S,S9,A) -valued Function-like set
S is non empty non void feasible feasible ManySortedSign
S9 is non empty non void feasible feasible ManySortedSign
A is Relation-like Function-like set
E is Relation-like Function-like set
(S,A,E) is non empty non void feasible strict feasible ManySortedSign
the carrier of (S,A,E) is non empty set
id the carrier of (S,A,E) is Relation-like the carrier of (S,A,E) -defined the carrier of (S,A,E) -valued Function-like one-to-one non empty total V18( the carrier of (S,A,E), the carrier of (S,A,E)) Element of K19(K20( the carrier of (S,A,E), the carrier of (S,A,E)))
K20( the carrier of (S,A,E), the carrier of (S,A,E)) is Relation-like set
K19(K20( the carrier of (S,A,E), the carrier of (S,A,E))) is set
the carrier' of (S,A,E) is non empty set
id the carrier' of (S,A,E) is Relation-like the carrier' of (S,A,E) -defined the carrier' of (S,A,E) -valued Function-like one-to-one non empty total V18( the carrier' of (S,A,E), the carrier' of (S,A,E)) Element of K19(K20( the carrier' of (S,A,E), the carrier' of (S,A,E)))
K20( the carrier' of (S,A,E), the carrier' of (S,A,E)) is Relation-like set
K19(K20( the carrier' of (S,A,E), the carrier' of (S,A,E))) is set
the carrier of S is non empty set
( the carrier of S,A) is Relation-like the carrier of S -defined Function-like non empty total set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
A | the carrier of S is Relation-like Function-like set
(id the carrier of S) +* (A | the carrier of S) is Relation-like Function-like non empty set
the carrier' of S is non empty set
( the carrier' of S,E) is Relation-like the carrier' of S -defined Function-like non empty total set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
E | the carrier' of S is Relation-like Function-like set
(id the carrier' of S) +* (E | the carrier' of S) is Relation-like Function-like non empty set
the carrier' of S9 is non empty set
the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like non empty total V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
the carrier of S9 is non empty set
K20( the carrier' of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier of S9)) is set
dom the ResultSort of S9 is non empty Element of K19( the carrier' of S9)
K19( the carrier' of S9) is set
the ResultSort of (S,A,E) is Relation-like the carrier' of (S,A,E) -defined the carrier of (S,A,E) -valued Function-like non empty total V18( the carrier' of (S,A,E), the carrier of (S,A,E)) Element of K19(K20( the carrier' of (S,A,E), the carrier of (S,A,E)))
K20( the carrier' of (S,A,E), the carrier of (S,A,E)) is Relation-like set
K19(K20( the carrier' of (S,A,E), the carrier of (S,A,E))) is set
dom the ResultSort of (S,A,E) is non empty Element of K19( the carrier' of (S,A,E))
K19( the carrier' of (S,A,E)) is set
dom A is set
rng ( the carrier' of S,E) is non empty set
dom (id the carrier of (S,A,E)) is non empty Element of K19( the carrier of (S,A,E))
K19( the carrier of (S,A,E)) is set
dom (id the carrier' of (S,A,E)) is non empty Element of K19( the carrier' of (S,A,E))
rng (id the carrier of (S,A,E)) is non empty set
rng (id the carrier' of (S,A,E)) is non empty set
the ResultSort of (S,A,E) * (id the carrier of (S,A,E)) is Relation-like the carrier' of (S,A,E) -defined the carrier of (S,A,E) -valued Function-like non empty total set
(id the carrier' of (S,A,E)) * the ResultSort of S9 is Relation-like the carrier' of (S,A,E) -defined the carrier of S9 -valued Function-like set
the Arity of (S,A,E) is Relation-like the carrier' of (S,A,E) -defined the carrier of (S,A,E) * -valued Function-like non empty total V18( the carrier' of (S,A,E), the carrier of (S,A,E) * ) Element of K19(K20( the carrier' of (S,A,E),( the carrier of (S,A,E) *)))
the carrier of (S,A,E) * is functional non empty FinSequence-membered M11( the carrier of (S,A,E))
K20( the carrier' of (S,A,E),( the carrier of (S,A,E) *)) is Relation-like set
K19(K20( the carrier' of (S,A,E),( the carrier of (S,A,E) *))) is set
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like non empty total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set
dom E is set
gg is set
FS is set
E . FS is set
E * the ResultSort of (S,A,E) is Relation-like the carrier of (S,A,E) -valued Function-like set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S * A is Relation-like the carrier' of S -defined Function-like set
the ResultSort of (S,A,E) . gg is set
p is Element of the carrier' of S
( the ResultSort of S * A) . p is set
E * the ResultSort of S9 is Relation-like the carrier of S9 -valued Function-like set
the ResultSort of S9 . gg is set
the ResultSort of S9 | the carrier' of (S,A,E) is Relation-like the carrier' of (S,A,E) -defined the carrier' of S9 -defined the carrier of S9 -valued Function-like Element of K19(K20( the carrier' of S9, the carrier of S9))
( the ResultSort of S9 | the carrier' of (S,A,E)) . gg is set
rng E is set
dom ( the ResultSort of S9 | the carrier' of (S,A,E)) is Element of K19( the carrier' of S9)
rng ( the carrier of S,A) is non empty set
rng (id the carrier of (S,A,E)) is non empty Element of K19( the carrier of (S,A,E))
rng (id the carrier' of (S,A,E)) is non empty Element of K19( the carrier' of (S,A,E))
rng the ResultSort of (S,A,E) is non empty Element of K19( the carrier of (S,A,E))
(id the carrier of (S,A,E)) * the ResultSort of (S,A,E) is Relation-like the carrier' of (S,A,E) -defined the carrier of (S,A,E) -valued Function-like non empty total V18( the carrier' of (S,A,E), the carrier of (S,A,E)) Element of K19(K20( the carrier' of (S,A,E), the carrier of (S,A,E)))
the ResultSort of S9 * (id the carrier' of (S,A,E)) is Relation-like the carrier' of (S,A,E) -defined the carrier of S9 -valued Function-like Element of K19(K20( the carrier' of (S,A,E), the carrier of S9))
K20( the carrier' of (S,A,E), the carrier of S9) is Relation-like set
K19(K20( the carrier' of (S,A,E), the carrier of S9)) is set
gg is set
the Arity of (S,A,E) . gg is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
(id the carrier' of (S,A,E)) . gg is set
the Arity of S9 . ((id the carrier' of (S,A,E)) . gg) is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
FS is Relation-like Function-like set
FS * (id the carrier of (S,A,E)) is Relation-like the carrier of (S,A,E) -valued Function-like set
p is set
E . p is set
a is Element of the carrier' of S
the_arity_of a is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of S . a is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of a) * A is Relation-like K97() -defined Function-like set
the Arity of S9 . gg is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
rng FS is set
S is non empty non void feasible feasible ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
S9 is Relation-like Function-like set
( the carrier of S,S9) is Relation-like the carrier of S -defined Function-like non empty total set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
S9 | the carrier of S is Relation-like Function-like set
(id the carrier of S) +* (S9 | the carrier of S) is Relation-like Function-like non empty set
A is Relation-like Function-like set
(S,S9,A) is non empty non void feasible strict feasible ManySortedSign
( the carrier' of S,A) is Relation-like the carrier' of S -defined Function-like non empty total set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
A | the carrier' of S is Relation-like Function-like set
(id the carrier' of S) +* (A | the carrier' of S) is Relation-like Function-like non empty set
S is non empty non void feasible feasible ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
S9 is Relation-like Function-like set
dom S9 is set
(id the carrier of S) +* S9 is Relation-like Function-like non empty set
A is Relation-like Function-like set
dom A is set
(S,S9,A) is non empty non void feasible strict feasible ManySortedSign
(id the carrier' of S) +* A is Relation-like Function-like non empty set
( the carrier' of S,A) is Relation-like the carrier' of S -defined Function-like non empty total set
A | the carrier' of S is Relation-like Function-like set
(id the carrier' of S) +* (A | the carrier' of S) is Relation-like Function-like non empty set
( the carrier of S,S9) is Relation-like the carrier of S -defined Function-like non empty total set
S9 | the carrier of S is Relation-like Function-like set
(id the carrier of S) +* (S9 | the carrier of S) is Relation-like Function-like non empty set
S is non empty non void feasible feasible ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
S9 is Relation-like Function-like set
dom S9 is set
A is Relation-like Function-like set
dom A is set
(S,S9,A) is non empty non void feasible strict feasible ManySortedSign
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
dom (id the carrier' of S) is non empty Element of K19( the carrier' of S)
K19( the carrier' of S) is set
(id the carrier' of S) +* A is Relation-like Function-like non empty set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
dom (id the carrier of S) is non empty Element of K19( the carrier of S)
K19( the carrier of S) is set
(id the carrier of S) +* S9 is Relation-like Function-like non empty set
S is non empty non void feasible feasible ManySortedSign
the carrier of S is non empty set
S9 is Relation-like Function-like set
( the carrier of S,S9) is Relation-like the carrier of S -defined Function-like non empty total set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
S9 | the carrier of S is Relation-like Function-like set
(id the carrier of S) +* (S9 | the carrier of S) is Relation-like Function-like non empty set
A is Relation-like Function-like set
(S,( the carrier of S,S9),A) is non empty non void feasible strict feasible ManySortedSign
(S,S9,A) is non empty non void feasible strict feasible ManySortedSign
the carrier' of S is non empty set
( the carrier of S,( the carrier of S,S9)) is Relation-like the carrier of S -defined Function-like non empty total set
( the carrier of S,S9) | the carrier of S is Relation-like the carrier of S -defined the carrier of S -defined Function-like set
(id the carrier of S) +* (( the carrier of S,S9) | the carrier of S) is Relation-like the carrier of S -defined Function-like non empty total set
( the carrier' of S,A) is Relation-like the carrier' of S -defined Function-like non empty total set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
A | the carrier' of S is Relation-like Function-like set
(id the carrier' of S) +* (A | the carrier' of S) is Relation-like Function-like non empty set
the carrier of (S,( the carrier of S,S9),A) is non empty set
rng ( the carrier of S,S9) is non empty set
the carrier' of (S,( the carrier of S,S9),A) is non empty set
rng ( the carrier' of S,A) is non empty set
S is non empty non void feasible feasible ManySortedSign
the carrier' of S is non empty set
S9 is Relation-like Function-like set
A is Relation-like Function-like set
( the carrier' of S,A) is Relation-like the carrier' of S -defined Function-like non empty total set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
A | the carrier' of S is Relation-like Function-like set
(id the carrier' of S) +* (A | the carrier' of S) is Relation-like Function-like non empty set
(S,S9,( the carrier' of S,A)) is non empty non void feasible strict feasible ManySortedSign
(S,S9,A) is non empty non void feasible strict feasible ManySortedSign
the carrier of S is non empty set
( the carrier' of S,( the carrier' of S,A)) is Relation-like the carrier' of S -defined Function-like non empty total set
( the carrier' of S,A) | the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -defined Function-like set
(id the carrier' of S) +* (( the carrier' of S,A) | the carrier' of S) is Relation-like the carrier' of S -defined Function-like non empty total set
( the carrier of S,S9) is Relation-like the carrier of S -defined Function-like non empty total set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
S9 | the carrier of S is Relation-like Function-like set
(id the carrier of S) +* (S9 | the carrier of S) is Relation-like Function-like non empty set
the carrier' of (S,S9,( the carrier' of S,A)) is non empty set
rng ( the carrier' of S,A) is non empty set
the carrier of (S,S9,( the carrier' of S,A)) is non empty set
rng ( the carrier of S,S9) is non empty set
S is feasible ManySortedSign
S is feasible ManySortedSign
S is feasible ManySortedSign
S9 is feasible (S)
A is feasible (S9)
S is non empty feasible feasible ManySortedSign
S9 is non empty feasible feasible ManySortedSign
S +* S9 is non empty feasible strict feasible ManySortedSign
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
the carrier' of S is set
the carrier of S is non empty set
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
the carrier' of S9 is set
the carrier of S9 is non empty set
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like total V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
K20( the carrier' of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier of S9)) is set
the ResultSort of (S +* S9) is Relation-like the carrier' of (S +* S9) -defined the carrier of (S +* S9) -valued Function-like total V18( the carrier' of (S +* S9), the carrier of (S +* S9)) Element of K19(K20( the carrier' of (S +* S9), the carrier of (S +* S9)))
the carrier' of (S +* S9) is set
the carrier of (S +* S9) is non empty set
K20( the carrier' of (S +* S9), the carrier of (S +* S9)) is Relation-like set
K19(K20( the carrier' of (S +* S9), the carrier of (S +* S9))) is set
the ResultSort of S +* the ResultSort of S9 is Relation-like the carrier' of S \/ the carrier' of S9 -defined Function-like total set
the carrier' of S \/ the carrier' of S9 is set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
dom (id the carrier of S) is non empty Element of K19( the carrier of S)
K19( the carrier of S) is set
dom (id the carrier' of S) is Element of K19( the carrier' of S)
K19( the carrier' of S) is set
rng (id the carrier of S) is non empty set
rng (id the carrier' of S) is set
the ResultSort of S * (id the carrier of S) is Relation-like the carrier' of S -defined the carrier of S -valued Function-like total set
(id the carrier' of S) * the ResultSort of (S +* S9) is Relation-like the carrier' of S -defined the carrier of (S +* S9) -valued Function-like set
the Arity of (S +* S9) is Relation-like the carrier' of (S +* S9) -defined the carrier of (S +* S9) * -valued Function-like total V18( the carrier' of (S +* S9), the carrier of (S +* S9) * ) Element of K19(K20( the carrier' of (S +* S9),( the carrier of (S +* S9) *)))
the carrier of (S +* S9) * is functional non empty FinSequence-membered M11( the carrier of (S +* S9))
K20( the carrier' of (S +* S9),( the carrier of (S +* S9) *)) is Relation-like set
K19(K20( the carrier' of (S +* S9),( the carrier of (S +* S9) *))) is set
dom the ResultSort of S is Element of K19( the carrier' of S)
the ResultSort of (S +* S9) | the carrier' of S is Relation-like the carrier' of S -defined the carrier' of (S +* S9) -defined the carrier of (S +* S9) -valued Function-like Element of K19(K20( the carrier' of (S +* S9), the carrier of (S +* S9)))
the ResultSort of (S +* S9) * (id the carrier' of S) is Relation-like the carrier' of S -defined the carrier of (S +* S9) -valued Function-like Element of K19(K20( the carrier' of S, the carrier of (S +* S9)))
K20( the carrier' of S, the carrier of (S +* S9)) is Relation-like set
K19(K20( the carrier' of S, the carrier of (S +* S9))) is set
the carrier of S \/ the carrier of S9 is non empty set
rng (id the carrier of S) is non empty Element of K19( the carrier of S)
rng (id the carrier' of S) is Element of K19( the carrier' of S)
rng the ResultSort of S is Element of K19( the carrier of S)
(id the carrier of S) * the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
o is set
the Arity of S . o is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
(id the carrier' of S) . o is set
the Arity of (S +* S9) . ((id the carrier' of S) . o) is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
e is Relation-like Function-like set
e * (id the carrier of S) is Relation-like the carrier of S -valued Function-like set
dom the Arity of S is Element of K19( the carrier' of S)
rng the Arity of S is functional FinSequence-membered Element of K19(( the carrier of S *))
K19(( the carrier of S *)) is set
rng e is set
the Arity of S +* the Arity of S9 is Relation-like the carrier' of S \/ the carrier' of S9 -defined Function-like total set
( the Arity of S +* the Arity of S9) . o is set
the Arity of (S +* S9) . o is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
S is non empty feasible feasible ManySortedSign
S9 is non empty feasible feasible ManySortedSign
S +* S9 is non empty feasible strict feasible ManySortedSign
the carrier of S9 is non empty set
id the carrier of S9 is Relation-like the carrier of S9 -defined the carrier of S9 -valued Function-like one-to-one non empty total V18( the carrier of S9, the carrier of S9) Element of K19(K20( the carrier of S9, the carrier of S9))
K20( the carrier of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier of S9, the carrier of S9)) is set
the carrier' of S9 is set
id the carrier' of S9 is Relation-like the carrier' of S9 -defined the carrier' of S9 -valued Function-like one-to-one total V18( the carrier' of S9, the carrier' of S9) Element of K19(K20( the carrier' of S9, the carrier' of S9))
K20( the carrier' of S9, the carrier' of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier' of S9)) is set
dom (id the carrier of S9) is non empty Element of K19( the carrier of S9)
K19( the carrier of S9) is set
dom (id the carrier' of S9) is Element of K19( the carrier' of S9)
K19( the carrier' of S9) is set
rng (id the carrier of S9) is non empty set
the carrier of (S +* S9) is non empty set
rng (id the carrier' of S9) is set
the carrier' of (S +* S9) is set
the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like total V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
K20( the carrier' of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier of S9)) is set
the ResultSort of S9 * (id the carrier of S9) is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like total set
the ResultSort of (S +* S9) is Relation-like the carrier' of (S +* S9) -defined the carrier of (S +* S9) -valued Function-like total V18( the carrier' of (S +* S9), the carrier of (S +* S9)) Element of K19(K20( the carrier' of (S +* S9), the carrier of (S +* S9)))
K20( the carrier' of (S +* S9), the carrier of (S +* S9)) is Relation-like set
K19(K20( the carrier' of (S +* S9), the carrier of (S +* S9))) is set
(id the carrier' of S9) * the ResultSort of (S +* S9) is Relation-like the carrier' of S9 -defined the carrier of (S +* S9) -valued Function-like set
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set
the Arity of (S +* S9) is Relation-like the carrier' of (S +* S9) -defined the carrier of (S +* S9) * -valued Function-like total V18( the carrier' of (S +* S9), the carrier of (S +* S9) * ) Element of K19(K20( the carrier' of (S +* S9),( the carrier of (S +* S9) *)))
the carrier of (S +* S9) * is functional non empty FinSequence-membered M11( the carrier of (S +* S9))
K20( the carrier' of (S +* S9),( the carrier of (S +* S9) *)) is Relation-like set
K19(K20( the carrier' of (S +* S9),( the carrier of (S +* S9) *))) is set
the carrier of S is non empty set
the carrier of S \/ the carrier of S9 is non empty set
the carrier' of S is set
the carrier' of S \/ the carrier' of S9 is set
rng (id the carrier of S9) is non empty Element of K19( the carrier of S9)
rng (id the carrier' of S9) is Element of K19( the carrier' of S9)
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S +* the ResultSort of S9 is Relation-like the carrier' of S \/ the carrier' of S9 -defined Function-like total set
dom the ResultSort of S9 is Element of K19( the carrier' of S9)
the ResultSort of (S +* S9) | the carrier' of S9 is Relation-like the carrier' of S9 -defined the carrier' of (S +* S9) -defined the carrier of (S +* S9) -valued Function-like Element of K19(K20( the carrier' of (S +* S9), the carrier of (S +* S9)))
the ResultSort of (S +* S9) * (id the carrier' of S9) is Relation-like the carrier' of S9 -defined the carrier of (S +* S9) -valued Function-like Element of K19(K20( the carrier' of S9, the carrier of (S +* S9)))
K20( the carrier' of S9, the carrier of (S +* S9)) is Relation-like set
K19(K20( the carrier' of S9, the carrier of (S +* S9))) is set
rng the ResultSort of S9 is Element of K19( the carrier of S9)
(id the carrier of S9) * the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like total V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
o is set
the Arity of S9 . o is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
(id the carrier' of S9) . o is set
the Arity of (S +* S9) . ((id the carrier' of S9) . o) is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
e is Relation-like Function-like set
e * (id the carrier of S9) is Relation-like the carrier of S9 -valued Function-like set
dom the Arity of S9 is Element of K19( the carrier' of S9)
rng the Arity of S9 is functional FinSequence-membered Element of K19(( the carrier of S9 *))
K19(( the carrier of S9 *)) is set
rng e is set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of S +* the Arity of S9 is Relation-like the carrier' of S \/ the carrier' of S9 -defined Function-like total set
( the Arity of S +* the Arity of S9) . o is set
the Arity of (S +* S9) . o is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
S is non empty feasible feasible ManySortedSign
A is non empty feasible feasible ManySortedSign
S9 is non empty feasible feasible ManySortedSign
S +* S9 is non empty feasible strict feasible ManySortedSign
E is Relation-like Function-like set
o is Relation-like Function-like set
x is Relation-like Function-like set
e is Relation-like Function-like set
E +* o is Relation-like Function-like set
x +* e is Relation-like Function-like set
dom E is set
the carrier of S is non empty set
dom x is set
the carrier' of S is set
rng E is set
the carrier of A is non empty set
rng x is set
the carrier' of A is set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S * E is Relation-like the carrier' of S -defined Function-like set
the ResultSort of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like total V18( the carrier' of A, the carrier of A) Element of K19(K20( the carrier' of A, the carrier of A))
K20( the carrier' of A, the carrier of A) is Relation-like set
K19(K20( the carrier' of A, the carrier of A)) is set
x * the ResultSort of A is Relation-like the carrier of A -valued Function-like set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of A is Relation-like the carrier' of A -defined the carrier of A * -valued Function-like total V18( the carrier' of A, the carrier of A * ) Element of K19(K20( the carrier' of A,( the carrier of A *)))
the carrier of A * is functional non empty FinSequence-membered M11( the carrier of A)
K20( the carrier' of A,( the carrier of A *)) is Relation-like set
K19(K20( the carrier' of A,( the carrier of A *))) is set
dom o is set
the carrier of S9 is non empty set
dom e is set
the carrier' of S9 is set
rng o is set
rng e is set
the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like total V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
K20( the carrier' of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier of S9)) is set
the ResultSort of S9 * o is Relation-like the carrier' of S9 -defined Function-like set
e * the ResultSort of A is Relation-like the carrier of A -valued Function-like set
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set
the carrier of (S +* S9) is non empty set
the carrier of S \/ the carrier of S9 is non empty set
dom (E +* o) is set
dom (x +* e) is set
the carrier' of (S +* S9) is set
rng (E +* o) is set
rng (x +* e) is set
the ResultSort of (S +* S9) is Relation-like the carrier' of (S +* S9) -defined the carrier of (S +* S9) -valued Function-like total V18( the carrier' of (S +* S9), the carrier of (S +* S9)) Element of K19(K20( the carrier' of (S +* S9), the carrier of (S +* S9)))
K20( the carrier' of (S +* S9), the carrier of (S +* S9)) is Relation-like set
K19(K20( the carrier' of (S +* S9), the carrier of (S +* S9))) is set
the ResultSort of (S +* S9) * (E +* o) is Relation-like the carrier' of (S +* S9) -defined Function-like set
(x +* e) * the ResultSort of A is Relation-like the carrier of A -valued Function-like set
the Arity of (S +* S9) is Relation-like the carrier' of (S +* S9) -defined the carrier of (S +* S9) * -valued Function-like total V18( the carrier' of (S +* S9), the carrier of (S +* S9) * ) Element of K19(K20( the carrier' of (S +* S9),( the carrier of (S +* S9) *)))
the carrier of (S +* S9) * is functional non empty FinSequence-membered M11( the carrier of (S +* S9))
K20( the carrier' of (S +* S9),( the carrier of (S +* S9) *)) is Relation-like set
K19(K20( the carrier' of (S +* S9),( the carrier of (S +* S9) *))) is set
the carrier' of S \/ the carrier' of S9 is set
(rng E) \/ (rng o) is set
(rng x) \/ (rng e) is set
rng the ResultSort of S is Element of K19( the carrier of S)
K19( the carrier of S) is set
rng the ResultSort of S9 is Element of K19( the carrier of S9)
K19( the carrier of S9) is set
dom the ResultSort of A is Element of K19( the carrier' of A)
K19( the carrier' of A) is set
the ResultSort of S +* the ResultSort of S9 is Relation-like the carrier' of S \/ the carrier' of S9 -defined Function-like total set
( the ResultSort of S * E) +* ( the ResultSort of S9 * o) is Relation-like Function-like set
FS is set
the Arity of (S +* S9) . FS is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
(x +* e) . FS is set
the Arity of A . ((x +* e) . FS) is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
p is Relation-like Function-like set
p * (E +* o) is Relation-like Function-like set
the Arity of S +* the Arity of S9 is Relation-like the carrier' of S \/ the carrier' of S9 -defined Function-like total set
dom the Arity of S is Element of K19( the carrier' of S)
K19( the carrier' of S) is set
dom the Arity of S9 is Element of K19( the carrier' of S9)
K19( the carrier' of S9) is set
the Arity of S9 . FS is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
rng the Arity of S9 is functional FinSequence-membered Element of K19(( the carrier of S9 *))
K19(( the carrier of S9 *)) is set
rng p is set
p * o is Relation-like Function-like set
dom (p * o) is set
dom p is set
p * E is Relation-like Function-like set
dom (p * E) is set
(p * E) +* (p * o) is Relation-like Function-like set
e . FS is set
the Arity of A . (e . FS) is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
p * o is Relation-like Function-like set
dom (p * o) is set
dom p is set
the Arity of S . FS is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
rng the Arity of S is functional FinSequence-membered Element of K19(( the carrier of S *))
K19(( the carrier of S *)) is set
rng p is set
p * E is Relation-like Function-like set
dom (p * E) is set
o +* E is Relation-like Function-like set
p * (o +* E) is Relation-like Function-like set
(p * o) +* (p * E) is Relation-like Function-like set
x . FS is set
the Arity of A . (x . FS) is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
A is non empty feasible feasible ManySortedSign
S is non empty feasible feasible ManySortedSign
S9 is non empty feasible feasible ManySortedSign
S +* S9 is non empty feasible strict feasible ManySortedSign
the carrier of S is non empty set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
the carrier' of S is set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
the carrier of S9 is non empty set
id the carrier of S9 is Relation-like the carrier of S9 -defined the carrier of S9 -valued Function-like one-to-one non empty total V18( the carrier of S9, the carrier of S9) Element of K19(K20( the carrier of S9, the carrier of S9))
K20( the carrier of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier of S9, the carrier of S9)) is set
the carrier' of S9 is set
id the carrier' of S9 is Relation-like the carrier' of S9 -defined the carrier' of S9 -valued Function-like one-to-one total V18( the carrier' of S9, the carrier' of S9) Element of K19(K20( the carrier' of S9, the carrier' of S9))
K20( the carrier' of S9, the carrier' of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier' of S9)) is set
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set
the Arity of A is Relation-like the carrier' of A -defined the carrier of A * -valued Function-like total V18( the carrier' of A, the carrier of A * ) Element of K19(K20( the carrier' of A,( the carrier of A *)))
the carrier' of A is set
the carrier of A is non empty set
the carrier of A * is functional non empty FinSequence-membered M11( the carrier of A)
K20( the carrier' of A,( the carrier of A *)) is Relation-like set
K19(K20( the carrier' of A,( the carrier of A *))) is set
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like total V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
K20( the carrier' of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier of S9)) is set
the ResultSort of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like total V18( the carrier' of A, the carrier of A) Element of K19(K20( the carrier' of A, the carrier of A))
K20( the carrier' of A, the carrier of A) is Relation-like set
K19(K20( the carrier' of A, the carrier of A)) is set
the carrier of (S +* S9) is non empty set
the carrier of S \/ the carrier of S9 is non empty set
id ( the carrier of S \/ the carrier of S9) is Relation-like the carrier of S \/ the carrier of S9 -defined the carrier of S \/ the carrier of S9 -valued Function-like one-to-one non empty total V18( the carrier of S \/ the carrier of S9, the carrier of S \/ the carrier of S9) Element of K19(K20(( the carrier of S \/ the carrier of S9),( the carrier of S \/ the carrier of S9)))
K20(( the carrier of S \/ the carrier of S9),( the carrier of S \/ the carrier of S9)) is Relation-like set
K19(K20(( the carrier of S \/ the carrier of S9),( the carrier of S \/ the carrier of S9))) is set
the carrier' of (S +* S9) is set
the carrier' of S \/ the carrier' of S9 is set
(id the carrier of S) +* (id the carrier of S9) is Relation-like the carrier of S \/ the carrier of S9 -defined Function-like non empty total set
(id the carrier' of S) +* (id the carrier' of S9) is Relation-like the carrier' of S \/ the carrier' of S9 -defined Function-like total set
id the carrier of (S +* S9) is Relation-like the carrier of (S +* S9) -defined the carrier of (S +* S9) -valued Function-like one-to-one non empty total V18( the carrier of (S +* S9), the carrier of (S +* S9)) Element of K19(K20( the carrier of (S +* S9), the carrier of (S +* S9)))
K20( the carrier of (S +* S9), the carrier of (S +* S9)) is Relation-like set
K19(K20( the carrier of (S +* S9), the carrier of (S +* S9))) is set
id the carrier' of (S +* S9) is Relation-like the carrier' of (S +* S9) -defined the carrier' of (S +* S9) -valued Function-like one-to-one total V18( the carrier' of (S +* S9), the carrier' of (S +* S9)) Element of K19(K20( the carrier' of (S +* S9), the carrier' of (S +* S9)))
K20( the carrier' of (S +* S9), the carrier' of (S +* S9)) is Relation-like set
K19(K20( the carrier' of (S +* S9), the carrier' of (S +* S9))) is set
S is non empty feasible feasible ManySortedSign
the carrier of S is non empty set
the Element of the carrier of S is Element of the carrier of S
A is feasible (S)
the carrier of A is set
S is non empty non void feasible feasible ManySortedSign
the carrier' of S is non empty set
the Element of the carrier' of S is Element of the carrier' of S
A is non empty feasible feasible (S)
the carrier' of A is set
S is feasible ManySortedSign
S9 is feasible ManySortedSign
the carrier of S is set
the carrier' of S is set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
the carrier' of S9 is set
the carrier of S9 is set
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
K20( the carrier' of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier of S9)) is set
S is feasible ManySortedSign
the non empty non void feasible strict feasible ManySortedSign is non empty non void feasible strict feasible ManySortedSign
A is non empty feasible feasible ManySortedSign
the non empty non void feasible strict feasible ManySortedSign +* A is non empty non void feasible strict feasible ManySortedSign
E is feasible (S)
the carrier of E is set
the carrier' of E is set
S is Relation-like Function-like set
S9 is Relation-like Function-like set
A is non empty non void feasible feasible ManySortedSign
E is non empty non void feasible feasible (A)
the carrier of E is non empty set
( the carrier of E,S) is Relation-like the carrier of E -defined Function-like non empty total set
id the carrier of E is Relation-like the carrier of E -defined the carrier of E -valued Function-like one-to-one non empty total V18( the carrier of E, the carrier of E) Element of K19(K20( the carrier of E, the carrier of E))
K20( the carrier of E, the carrier of E) is Relation-like set
K19(K20( the carrier of E, the carrier of E)) is set
S | the carrier of E is Relation-like Function-like set
(id the carrier of E) +* (S | the carrier of E) is Relation-like Function-like non empty set
the carrier' of E is non empty set
( the carrier' of E,S9) is Relation-like the carrier' of E -defined Function-like non empty total set
id the carrier' of E is Relation-like the carrier' of E -defined the carrier' of E -valued Function-like one-to-one non empty total V18( the carrier' of E, the carrier' of E) Element of K19(K20( the carrier' of E, the carrier' of E))
K20( the carrier' of E, the carrier' of E) is Relation-like set
K19(K20( the carrier' of E, the carrier' of E)) is set
S9 | the carrier' of E is Relation-like Function-like set
(id the carrier' of E) +* (S9 | the carrier' of E) is Relation-like Function-like non empty set
(E,S,S9) is non empty non void feasible strict feasible ManySortedSign
the carrier of A is non empty set
( the carrier of E,S) | the carrier of A is Relation-like the carrier of A -defined the carrier of E -defined Function-like set
( the carrier of A,S) is Relation-like the carrier of A -defined Function-like non empty total set
id the carrier of A is Relation-like the carrier of A -defined the carrier of A -valued Function-like one-to-one non empty total V18( the carrier of A, the carrier of A) Element of K19(K20( the carrier of A, the carrier of A))
K20( the carrier of A, the carrier of A) is Relation-like set
K19(K20( the carrier of A, the carrier of A)) is set
S | the carrier of A is Relation-like Function-like set
(id the carrier of A) +* (S | the carrier of A) is Relation-like Function-like non empty set
the carrier' of A is non empty set
( the carrier' of E,S9) | the carrier' of A is Relation-like the carrier' of A -defined the carrier' of E -defined Function-like set
( the carrier' of A,S9) is Relation-like the carrier' of A -defined Function-like non empty total set
id the carrier' of A is Relation-like the carrier' of A -defined the carrier' of A -valued Function-like one-to-one non empty total V18( the carrier' of A, the carrier' of A) Element of K19(K20( the carrier' of A, the carrier' of A))
K20( the carrier' of A, the carrier' of A) is Relation-like set
K19(K20( the carrier' of A, the carrier' of A)) is set
S9 | the carrier' of A is Relation-like Function-like set
(id the carrier' of A) +* (S9 | the carrier' of A) is Relation-like Function-like non empty set
S is Relation-like Function-like set
S9 is Relation-like Function-like set
A is non empty non void feasible feasible ManySortedSign
(A,S,S9) is non empty non void feasible strict feasible ManySortedSign
E is non empty non void feasible feasible (A)
(E,S,S9) is non empty non void feasible strict feasible ManySortedSign
the carrier of E is non empty set
( the carrier of E,S) is Relation-like the carrier of E -defined Function-like non empty total set
id the carrier of E is Relation-like the carrier of E -defined the carrier of E -valued Function-like one-to-one non empty total V18( the carrier of E, the carrier of E) Element of K19(K20( the carrier of E, the carrier of E))
K20( the carrier of E, the carrier of E) is Relation-like set
K19(K20( the carrier of E, the carrier of E)) is set
S | the carrier of E is Relation-like Function-like set
(id the carrier of E) +* (S | the carrier of E) is Relation-like Function-like non empty set
the carrier' of E is non empty set
( the carrier' of E,S9) is Relation-like the carrier' of E -defined Function-like non empty total set
id the carrier' of E is Relation-like the carrier' of E -defined the carrier' of E -valued Function-like one-to-one non empty total V18( the carrier' of E, the carrier' of E) Element of K19(K20( the carrier' of E, the carrier' of E))
K20( the carrier' of E, the carrier' of E) is Relation-like set
K19(K20( the carrier' of E, the carrier' of E)) is set
S9 | the carrier' of E is Relation-like Function-like set
(id the carrier' of E) +* (S9 | the carrier' of E) is Relation-like Function-like non empty set
the carrier' of A is non empty set
( the carrier' of A,S9) is Relation-like the carrier' of A -defined Function-like non empty total set
id the carrier' of A is Relation-like the carrier' of A -defined the carrier' of A -valued Function-like one-to-one non empty total V18( the carrier' of A, the carrier' of A) Element of K19(K20( the carrier' of A, the carrier' of A))
K20( the carrier' of A, the carrier' of A) is Relation-like set
K19(K20( the carrier' of A, the carrier' of A)) is set
S9 | the carrier' of A is Relation-like Function-like set
(id the carrier' of A) +* (S9 | the carrier' of A) is Relation-like Function-like non empty set
( the carrier' of A,( the carrier' of A,S9)) is Relation-like the carrier' of A -defined Function-like non empty total set
( the carrier' of A,S9) | the carrier' of A is Relation-like the carrier' of A -defined the carrier' of A -defined Function-like set
(id the carrier' of A) +* (( the carrier' of A,S9) | the carrier' of A) is Relation-like the carrier' of A -defined Function-like non empty total set
the carrier of A is non empty set
( the carrier of A,S) is Relation-like the carrier of A -defined Function-like non empty total set
id the carrier of A is Relation-like the carrier of A -defined the carrier of A -valued Function-like one-to-one non empty total V18( the carrier of A, the carrier of A) Element of K19(K20( the carrier of A, the carrier of A))
K20( the carrier of A, the carrier of A) is Relation-like set
K19(K20( the carrier of A, the carrier of A)) is set
S | the carrier of A is Relation-like Function-like set
(id the carrier of A) +* (S | the carrier of A) is Relation-like Function-like non empty set
( the carrier' of E,S9) | the carrier' of A is Relation-like the carrier' of A -defined the carrier' of E -defined Function-like set
( the carrier of E,S) | the carrier of A is Relation-like the carrier of A -defined the carrier of E -defined Function-like set
(A,(( the carrier of E,S) | the carrier of A),(( the carrier' of E,S9) | the carrier' of A)) is non empty non void feasible strict feasible ManySortedSign
(A,S,( the carrier' of A,S9)) is non empty non void feasible strict feasible ManySortedSign
S is non empty non void feasible feasible ManySortedSign
S9 is non empty non void feasible feasible ManySortedSign
S +* S9 is non empty non void feasible strict feasible ManySortedSign
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
the carrier' of S is non empty set
the carrier of S is non empty set
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like non empty total V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
the carrier' of S9 is non empty set
the carrier of S9 is non empty set
K20( the carrier' of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier of S9)) is set
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like non empty total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set
rng the Arity of S9 is functional non empty FinSequence-membered Element of K19(( the carrier of S9 *))
K19(( the carrier of S9 *)) is set
rng the ResultSort of S9 is non empty Element of K19( the carrier of S9)
K19( the carrier of S9) is set
rng the ResultSort of S is non empty Element of K19( the carrier of S)
K19( the carrier of S) is set
E is Relation-like Function-like set
x is Relation-like Function-like set
((S +* S9),E,x) is non empty non void feasible strict feasible ManySortedSign
(S,E,x) is non empty non void feasible strict feasible ManySortedSign
(S9,E,x) is non empty non void feasible strict feasible ManySortedSign
(S,E,x) +* (S9,E,x) is non empty non void feasible strict feasible ManySortedSign
( the carrier of S9,E) is Relation-like the carrier of S9 -defined Function-like non empty total set
id the carrier of S9 is Relation-like the carrier of S9 -defined the carrier of S9 -valued Function-like one-to-one non empty total V18( the carrier of S9, the carrier of S9) Element of K19(K20( the carrier of S9, the carrier of S9))
K20( the carrier of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier of S9, the carrier of S9)) is set
E | the carrier of S9 is Relation-like Function-like set
(id the carrier of S9) +* (E | the carrier of S9) is Relation-like Function-like non empty set
dom H1(S9) is non empty Element of K19( the carrier of S9)
( the carrier of S,E) is Relation-like the carrier of S -defined Function-like non empty total set
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty total V18( the carrier of S, the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is Relation-like set
K19(K20( the carrier of S, the carrier of S)) is set
E | the carrier of S is Relation-like Function-like set
(id the carrier of S) +* (E | the carrier of S) is Relation-like Function-like non empty set
the carrier of H2(S) is non empty set
K20( the carrier of S, the carrier of H2(S)) is Relation-like set
K19(K20( the carrier of S, the carrier of H2(S))) is set
the ResultSort of S * H1(S) is Relation-like the carrier' of S -defined Function-like non empty total set
dom ( the ResultSort of S * H1(S)) is non empty Element of K19( the carrier' of S)
K19( the carrier' of S) is set
dom H1(S) is non empty Element of K19( the carrier of S)
( the carrier' of S,x) is Relation-like the carrier' of S -defined Function-like non empty total set
id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
x | the carrier' of S is Relation-like Function-like set
(id the carrier' of S) +* (x | the carrier' of S) is Relation-like Function-like non empty set
dom H3(S) is non empty Element of K19( the carrier' of S)
the Relation-like Function-like (H3(S)) is Relation-like Function-like (H3(S))
( the carrier' of S9,x) is Relation-like the carrier' of S9 -defined Function-like non empty total set
id the carrier' of S9 is Relation-like the carrier' of S9 -defined the carrier' of S9 -valued Function-like one-to-one non empty total V18( the carrier' of S9, the carrier' of S9) Element of K19(K20( the carrier' of S9, the carrier' of S9))
K20( the carrier' of S9, the carrier' of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier' of S9)) is set
x | the carrier' of S9 is Relation-like Function-like set
(id the carrier' of S9) +* (x | the carrier' of S9) is Relation-like Function-like non empty set
the Relation-like Function-like (H3(S9)) is Relation-like Function-like (H3(S9))
the ResultSort of (S +* S9) is Relation-like the carrier' of (S +* S9) -defined the carrier of (S +* S9) -valued Function-like non empty total V18( the carrier' of (S +* S9), the carrier of (S +* S9)) Element of K19(K20( the carrier' of (S +* S9), the carrier of (S +* S9)))
the carrier' of (S +* S9) is non empty set
the carrier of (S +* S9) is non empty set
K20( the carrier' of (S +* S9), the carrier of (S +* S9)) is Relation-like set
K19(K20( the carrier' of (S +* S9), the carrier of (S +* S9))) is set
the ResultSort of S +* the ResultSort of S9 is Relation-like the carrier' of S \/ the carrier' of S9 -defined Function-like non empty total set
the carrier' of S \/ the carrier' of S9 is non empty set
rng the Relation-like Function-like (H3(S9)) is set
dom H3(S9) is non empty Element of K19( the carrier' of S9)
K19( the carrier' of S9) is set
( the carrier' of (S +* S9),x) is Relation-like the carrier' of (S +* S9) -defined Function-like non empty total set
id the carrier' of (S +* S9) is Relation-like the carrier' of (S +* S9) -defined the carrier' of (S +* S9) -valued Function-like one-to-one non empty total V18( the carrier' of (S +* S9), the carrier' of (S +* S9)) Element of K19(K20( the carrier' of (S +* S9), the carrier' of (S +* S9)))
K20( the carrier' of (S +* S9), the carrier' of (S +* S9)) is Relation-like set
K19(K20( the carrier' of (S +* S9), the carrier' of (S +* S9))) is set
x | the carrier' of (S +* S9) is Relation-like Function-like set
(id the carrier' of (S +* S9)) +* (x | the carrier' of (S +* S9)) is Relation-like Function-like non empty set
H3(S) \/ H3(S9) is Relation-like non empty set
rng H3(S +* S9) is non empty set
rng H3(S) is non empty set
rng H3(S9) is non empty set
(rng H3(S)) \/ (rng H3(S9)) is non empty set
the carrier of H2(S9) is non empty set
K20( the carrier of S9, the carrier of H2(S9)) is Relation-like set
K19(K20( the carrier of S9, the carrier of H2(S9))) is set
the ResultSort of S9 * H1(S9) is Relation-like the carrier' of S9 -defined Function-like non empty total set
dom ( the ResultSort of S9 * H1(S9)) is non empty Element of K19( the carrier' of S9)
the carrier of S \/ the carrier of S9 is non empty set
( the carrier of (S +* S9),E) is Relation-like the carrier of (S +* S9) -defined Function-like non empty total set
id the carrier of (S +* S9) is Relation-like the carrier of (S +* S9) -defined the carrier of (S +* S9) -valued Function-like one-to-one non empty total V18( the carrier of (S +* S9), the carrier of (S +* S9)) Element of K19(K20( the carrier of (S +* S9), the carrier of (S +* S9)))
K20( the carrier of (S +* S9), the carrier of (S +* S9)) is Relation-like set
K19(K20( the carrier of (S +* S9), the carrier of (S +* S9))) is set
E | the carrier of (S +* S9) is Relation-like Function-like set
(id the carrier of (S +* S9)) +* (E | the carrier of (S +* S9)) is Relation-like Function-like non empty set
H1(S) +* H1(S9) is Relation-like the carrier of S \/ the carrier of S9 -defined Function-like non empty total set
H1(S) \/ H1(S9) is Relation-like non empty set
rng H1(S +* S9) is non empty set
rng H1(S) is non empty set
rng H1(S9) is non empty set
(rng H1(S)) \/ (rng H1(S9)) is non empty set
the carrier of H2(S9) * is functional non empty FinSequence-membered M11( the carrier of H2(S9))
q is Relation-like the carrier of S9 -defined the carrier of H2(S9) -valued Function-like non empty total V18( the carrier of S9, the carrier of H2(S9)) Element of K19(K20( the carrier of S9, the carrier of H2(S9)))
q * is Relation-like the carrier of S9 * -defined the carrier of H2(S9) * -valued Function-like non empty total V18( the carrier of S9 * , the carrier of H2(S9) * ) Element of K19(K20(( the carrier of S9 *),( the carrier of H2(S9) *)))
K20(( the carrier of S9 *),( the carrier of H2(S9) *)) is Relation-like set
K19(K20(( the carrier of S9 *),( the carrier of H2(S9) *))) is set
(q *) * the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of H2(S9) * -valued Function-like non empty total V18( the carrier' of S9, the carrier of H2(S9) * ) Element of K19(K20( the carrier' of S9,( the carrier of H2(S9) *)))
K20( the carrier' of S9,( the carrier of H2(S9) *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of H2(S9) *))) is set
dom ((q *) * the Arity of S9) is non empty Element of K19( the carrier' of S9)
dom (q *) is functional non empty FinSequence-membered Element of K19(( the carrier of S9 *))
H3(S) +* H3(S9) is Relation-like the carrier' of S \/ the carrier' of S9 -defined Function-like non empty total set
the Relation-like Function-like (H3(S)) +* the Relation-like Function-like (H3(S9)) is Relation-like Function-like set
rng the Relation-like Function-like (H3(S)) is set
the ResultSort of H2(S +* S9) is Relation-like the carrier' of H2(S +* S9) -defined the carrier of H2(S +* S9) -valued Function-like non empty total V18( the carrier' of H2(S +* S9), the carrier of H2(S +* S9)) Element of K19(K20( the carrier' of H2(S +* S9), the carrier of H2(S +* S9)))
the carrier' of H2(S +* S9) is non empty set
the carrier of H2(S +* S9) is non empty set
K20( the carrier' of H2(S +* S9), the carrier of H2(S +* S9)) is Relation-like set
K19(K20( the carrier' of H2(S +* S9), the carrier of H2(S +* S9))) is set
gg is Relation-like Function-like (H3(S +* S9))
the ResultSort of (S +* S9) * H1(S +* S9) is Relation-like the carrier' of (S +* S9) -defined Function-like non empty total set
gg * ( the ResultSort of (S +* S9) * H1(S +* S9)) is Relation-like Function-like set
( the ResultSort of S * H1(S)) +* ( the ResultSort of S9 * H1(S9)) is Relation-like the carrier' of S \/ the carrier' of S9 -defined Function-like non empty total set
gg * (( the ResultSort of S * H1(S)) +* ( the ResultSort of S9 * H1(S9))) is Relation-like Function-like set
the Relation-like Function-like (H3(S)) * ( the ResultSort of S * H1(S)) is Relation-like Function-like set
the Relation-like Function-like (H3(S9)) * ( the ResultSort of S9 * H1(S9)) is Relation-like Function-like set
( the Relation-like Function-like (H3(S)) * ( the ResultSort of S * H1(S))) +* ( the Relation-like Function-like (H3(S9)) * ( the ResultSort of S9 * H1(S9))) is Relation-like Function-like set
the ResultSort of H2(S) is Relation-like the carrier' of H2(S) -defined the carrier of H2(S) -valued Function-like non empty total V18( the carrier' of H2(S), the carrier of H2(S)) Element of K19(K20( the carrier' of H2(S), the carrier of H2(S)))
the carrier' of H2(S) is non empty set
K20( the carrier' of H2(S), the carrier of H2(S)) is Relation-like set
K19(K20( the carrier' of H2(S), the carrier of H2(S))) is set
the ResultSort of H2(S) +* ( the Relation-like Function-like (H3(S9)) * ( the ResultSort of S9 * H1(S9))) is Relation-like Function-like non empty set
the ResultSort of H2(S9) is Relation-like the carrier' of H2(S9) -defined the carrier of H2(S9) -valued Function-like non empty total V18( the carrier' of H2(S9), the carrier of H2(S9)) Element of K19(K20( the carrier' of H2(S9), the carrier of H2(S9)))
the carrier' of H2(S9) is non empty set
K20( the carrier' of H2(S9), the carrier of H2(S9)) is Relation-like set
K19(K20( the carrier' of H2(S9), the carrier of H2(S9))) is set
the ResultSort of H2(S) +* the ResultSort of H2(S9) is Relation-like the carrier' of H2(S) \/ the carrier' of H2(S9) -defined Function-like non empty total set
the carrier' of H2(S) \/ the carrier' of H2(S9) is non empty set
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the carrier of H2(S) * is functional non empty FinSequence-membered M11( the carrier of H2(S))
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
o is Relation-like the carrier of S -defined the carrier of H2(S) -valued Function-like non empty total V18( the carrier of S, the carrier of H2(S)) Element of K19(K20( the carrier of S, the carrier of H2(S)))
o * is Relation-like the carrier of S * -defined the carrier of H2(S) * -valued Function-like non empty total V18( the carrier of S * , the carrier of H2(S) * ) Element of K19(K20(( the carrier of S *),( the carrier of H2(S) *)))
K20(( the carrier of S *),( the carrier of H2(S) *)) is Relation-like set
K19(K20(( the carrier of S *),( the carrier of H2(S) *))) is set
(o *) * the Arity of S is Relation-like the carrier' of S -defined the carrier of H2(S) * -valued Function-like non empty total V18( the carrier' of S, the carrier of H2(S) * ) Element of K19(K20( the carrier' of S,( the carrier of H2(S) *)))
K20( the carrier' of S,( the carrier of H2(S) *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of H2(S) *))) is set
dom ((o *) * the Arity of S) is non empty Element of K19( the carrier' of S)
K20( the carrier of (S +* S9), the carrier of H2(S +* S9)) is Relation-like set
K19(K20( the carrier of (S +* S9), the carrier of H2(S +* S9))) is set
the carrier of (S +* S9) * is functional non empty FinSequence-membered M11( the carrier of (S +* S9))
the Arity of (S +* S9) is Relation-like the carrier' of (S +* S9) -defined the carrier of (S +* S9) * -valued Function-like non empty total V18( the carrier' of (S +* S9), the carrier of (S +* S9) * ) Element of K19(K20( the carrier' of (S +* S9),( the carrier of (S +* S9) *)))
K20( the carrier' of (S +* S9),( the carrier of (S +* S9) *)) is Relation-like set
K19(K20( the carrier' of (S +* S9),( the carrier of (S +* S9) *))) is set
rng the Arity of (S +* S9) is functional non empty FinSequence-membered Element of K19(( the carrier of (S +* S9) *))
K19(( the carrier of (S +* S9) *)) is set
FS is Relation-like the carrier of (S +* S9) -defined the carrier of H2(S +* S9) -valued Function-like non empty total V18( the carrier of (S +* S9), the carrier of H2(S +* S9)) Element of K19(K20( the carrier of (S +* S9), the carrier of H2(S +* S9)))
FS * is Relation-like the carrier of (S +* S9) * -defined the carrier of H2(S +* S9) * -valued Function-like non empty total V18( the carrier of (S +* S9) * , the carrier of H2(S +* S9) * ) Element of K19(K20(( the carrier of (S +* S9) *),( the carrier of H2(S +* S9) *)))
the carrier of H2(S +* S9) * is functional non empty FinSequence-membered M11( the carrier of H2(S +* S9))
K20(( the carrier of (S +* S9) *),( the carrier of H2(S +* S9) *)) is Relation-like set
K19(K20(( the carrier of (S +* S9) *),( the carrier of H2(S +* S9) *))) is set
dom (FS *) is functional non empty FinSequence-membered Element of K19(( the carrier of (S +* S9) *))
(rng the Arity of (S +* S9)) /\ (dom (FS *)) is functional FinSequence-membered Element of K19(( the carrier of (S +* S9) *))
the Arity of S +* the Arity of S9 is Relation-like the carrier' of S \/ the carrier' of S9 -defined Function-like non empty total set
dom (o *) is functional non empty FinSequence-membered Element of K19(( the carrier of S *))
K19(( the carrier of S *)) is set
the Arity of S \/ the Arity of S9 is Relation-like non empty set
rng the Arity of S is functional non empty FinSequence-membered Element of K19(( the carrier of S *))
(rng the Arity of S) \/ (rng the Arity of S9) is non empty set
( the carrier of S *) \/ ( the carrier of S9 *) is non empty set
(o *) +* (q *) is Relation-like ( the carrier of S *) \/ ( the carrier of S9 *) -defined Function-like non empty total set
dom ((o *) +* (q *)) is non empty Element of K19((( the carrier of S *) \/ ( the carrier of S9 *)))
K19((( the carrier of S *) \/ ( the carrier of S9 *))) is set
(o *) \/ (q *) is Relation-like non empty set
FS | the carrier of S9 is Relation-like the carrier of S9 -defined the carrier of (S +* S9) -defined the carrier of H2(S +* S9) -valued Function-like Element of K19(K20( the carrier of (S +* S9), the carrier of H2(S +* S9)))
FS | the carrier of S is Relation-like the carrier of S -defined the carrier of (S +* S9) -defined the carrier of H2(S +* S9) -valued Function-like Element of K19(K20( the carrier of (S +* S9), the carrier of H2(S +* S9)))
the Arity of H2(S +* S9) is Relation-like the carrier' of H2(S +* S9) -defined the carrier of H2(S +* S9) * -valued Function-like non empty total V18( the carrier' of H2(S +* S9), the carrier of H2(S +* S9) * ) Element of K19(K20( the carrier' of H2(S +* S9),( the carrier of H2(S +* S9) *)))
K20( the carrier' of H2(S +* S9),( the carrier of H2(S +* S9) *)) is Relation-like set
K19(K20( the carrier' of H2(S +* S9),( the carrier of H2(S +* S9) *))) is set
(FS *) * the Arity of (S +* S9) is Relation-like the carrier' of (S +* S9) -defined the carrier of H2(S +* S9) * -valued Function-like non empty total V18( the carrier' of (S +* S9), the carrier of H2(S +* S9) * ) Element of K19(K20( the carrier' of (S +* S9),( the carrier of H2(S +* S9) *)))
K20( the carrier' of (S +* S9),( the carrier of H2(S +* S9) *)) is Relation-like set
K19(K20( the carrier' of (S +* S9),( the carrier of H2(S +* S9) *))) is set
gg * ((FS *) * the Arity of (S +* S9)) is Relation-like the carrier of H2(S +* S9) * -valued Function-like set
the Arity of (S +* S9) * ((o *) +* (q *)) is Relation-like the carrier' of (S +* S9) -defined Function-like set
gg * ( the Arity of (S +* S9) * ((o *) +* (q *))) is Relation-like Function-like set
((o *) * the Arity of S) +* ((q *) * the Arity of S9) is Relation-like the carrier' of S \/ the carrier' of S9 -defined Function-like non empty total set
gg * (((o *) * the Arity of S) +* ((q *) * the Arity of S9)) is Relation-like Function-like set
the Relation-like Function-like (H3(S)) * ((o *) * the Arity of S) is Relation-like the carrier of H2(S) * -valued Function-like set
the Relation-like Function-like (H3(S9)) * ((q *) * the Arity of S9) is Relation-like the carrier of H2(S9) * -valued Function-like set
( the Relation-like Function-like (H3(S)) * ((o *) * the Arity of S)) +* ( the Relation-like Function-like (H3(S9)) * ((q *) * the Arity of S9)) is Relation-like Function-like set
the Arity of H2(S) is Relation-like the carrier' of H2(S) -defined the carrier of H2(S) * -valued Function-like non empty total V18( the carrier' of H2(S), the carrier of H2(S) * ) Element of K19(K20( the carrier' of H2(S),( the carrier of H2(S) *)))
K20( the carrier' of H2(S),( the carrier of H2(S) *)) is Relation-like set
K19(K20( the carrier' of H2(S),( the carrier of H2(S) *))) is set
the Arity of H2(S) +* ( the Relation-like Function-like (H3(S9)) * ((q *) * the Arity of S9)) is Relation-like Function-like non empty set
the Arity of H2(S9) is Relation-like the carrier' of H2(S9) -defined the carrier of H2(S9) * -valued Function-like non empty total V18( the carrier' of H2(S9), the carrier of H2(S9) * ) Element of K19(K20( the carrier' of H2(S9),( the carrier of H2(S9) *)))
K20( the carrier' of H2(S9),( the carrier of H2(S9) *)) is Relation-like set
K19(K20( the carrier' of H2(S9),( the carrier of H2(S9) *))) is set
the Arity of H2(S) +* the Arity of H2(S9) is Relation-like the carrier' of H2(S) \/ the carrier' of H2(S9) -defined Function-like non empty total set
the non empty non void feasible feasible ManySortedSign is non empty non void feasible feasible ManySortedSign
the feasible MSAlgebra over the non empty non void feasible feasible ManySortedSign is feasible MSAlgebra over the non empty non void feasible feasible ManySortedSign
S is feasible ManySortedSign
the non empty non void feasible feasible (S) is non empty non void feasible feasible (S)
the feasible MSAlgebra over the non empty non void feasible feasible (S) is feasible MSAlgebra over the non empty non void feasible feasible (S)
S is non empty non void feasible feasible ManySortedSign
S9 is feasible MSAlgebra over S
S is feasible ManySortedSign
S9 is feasible (S)
A is (S9)
E is non empty non void feasible feasible (S9)
S is feasible ManySortedSign
the carrier of S is set
the carrier' of S is set
S9 is non empty feasible feasible ManySortedSign
the carrier of S9 is non empty set
the carrier' of S9 is set
A is MSAlgebra over S9
the Charact of A is Relation-like the carrier' of S9 -defined Function-like total V53() ManySortedFunction of the Arity of S9 * ( the Sorts of A #), the ResultSort of S9 * the Sorts of A
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set
the Sorts of A is Relation-like the carrier of S9 -defined Function-like non empty total set
the Sorts of A # is Relation-like the carrier of S9 * -defined Function-like non empty total set
the Arity of S9 * ( the Sorts of A #) is Relation-like the carrier' of S9 -defined Function-like total set
the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like total V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
K20( the carrier' of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier of S9)) is set
the ResultSort of S9 * the Sorts of A is Relation-like the carrier' of S9 -defined Function-like total set
dom the Charact of A is Element of K19( the carrier' of S9)
K19( the carrier' of S9) is set
E is non empty non void feasible feasible (S)
dom the Sorts of A is non empty Element of K19( the carrier of S9)
K19( the carrier of S9) is set
the carrier of E is non empty set
x is MSAlgebra over E
the Sorts of x is Relation-like the carrier of E -defined Function-like non empty total set
dom the Sorts of x is non empty Element of K19( the carrier of E)
K19( the carrier of E) is set
the carrier' of E is non empty set
the Charact of x is Relation-like the carrier' of E -defined Function-like non empty total V53() ManySortedFunction of the Arity of E * ( the Sorts of x #), the ResultSort of E * the Sorts of x
the Arity of E is Relation-like the carrier' of E -defined the carrier of E * -valued Function-like non empty total V18( the carrier' of E, the carrier of E * ) Element of K19(K20( the carrier' of E,( the carrier of E *)))
the carrier of E * is functional non empty FinSequence-membered M11( the carrier of E)
K20( the carrier' of E,( the carrier of E *)) is Relation-like set
K19(K20( the carrier' of E,( the carrier of E *))) is set
the Sorts of x # is Relation-like the carrier of E * -defined Function-like non empty total set
the Arity of E * ( the Sorts of x #) is Relation-like the carrier' of E -defined Function-like non empty total set
the ResultSort of E is Relation-like the carrier' of E -defined the carrier of E -valued Function-like non empty total V18( the carrier' of E, the carrier of E) Element of K19(K20( the carrier' of E, the carrier of E))
K20( the carrier' of E, the carrier of E) is Relation-like set
K19(K20( the carrier' of E, the carrier of E)) is set
the ResultSort of E * the Sorts of x is Relation-like the carrier' of E -defined Function-like non empty total set
dom the Charact of x is non empty Element of K19( the carrier' of E)
K19( the carrier' of E) is set
S is non empty non void feasible feasible ManySortedSign
the carrier' of S is non empty set
S9 is non empty feasible feasible ManySortedSign
the carrier of S9 is non empty set
A is MSAlgebra over S9
the Charact of A is Relation-like the carrier' of S9 -defined Function-like total V53() ManySortedFunction of the Arity of S9 * ( the Sorts of A #), the ResultSort of S9 * the Sorts of A
the carrier' of S9 is set
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set
the Sorts of A is Relation-like the carrier of S9 -defined Function-like non empty total set
the Sorts of A # is Relation-like the carrier of S9 * -defined Function-like non empty total set
the Arity of S9 * ( the Sorts of A #) is Relation-like the carrier' of S9 -defined Function-like total set
the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like total V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
K20( the carrier' of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier of S9)) is set
the ResultSort of S9 * the Sorts of A is Relation-like the carrier' of S9 -defined Function-like total set
dom the Sorts of A is non empty Element of K19( the carrier of S9)
K19( the carrier of S9) is set
E is non empty non void feasible feasible (S)
o is Element of the carrier' of S
the Charact of A . o is set
the_arity_of o is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S is non empty set
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of S . o is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
( the Sorts of A #) . (the_arity_of o) is set
the_result_sort_of o is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S . o is Element of the carrier of S
the Sorts of A . (the_result_sort_of o) is set
K20((( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o))) is Relation-like set
K19(K20((( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o)))) is set
the carrier of E is non empty set
x is MSAlgebra over E
the Sorts of x is Relation-like the carrier of E -defined Function-like non empty total set
dom the Sorts of x is non empty Element of K19( the carrier of E)
K19( the carrier of E) is set
the carrier' of E is non empty set
the ResultSort of E is Relation-like the carrier' of E -defined the carrier of E -valued Function-like non empty total V18( the carrier' of E, the carrier of E) Element of K19(K20( the carrier' of E, the carrier of E))
K20( the carrier' of E, the carrier of E) is Relation-like set
K19(K20( the carrier' of E, the carrier of E)) is set
the ResultSort of E | the carrier' of S is Relation-like the carrier' of S -defined the carrier' of E -defined the carrier of E -valued Function-like Element of K19(K20( the carrier' of E, the carrier of E))
the ResultSort of E . o is set
the carrier of E * is functional non empty FinSequence-membered M11( the carrier of E)
the Arity of E is Relation-like the carrier' of E -defined the carrier of E * -valued Function-like non empty total V18( the carrier' of E, the carrier of E * ) Element of K19(K20( the carrier' of E,( the carrier of E *)))
K20( the carrier' of E,( the carrier of E *)) is Relation-like set
K19(K20( the carrier' of E,( the carrier of E *))) is set
the Arity of E | the carrier' of S is Relation-like the carrier' of S -defined the carrier' of E -defined the carrier of E * -valued Function-like Element of K19(K20( the carrier' of E,( the carrier of E *)))
the Arity of E . o is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
the Charact of x is Relation-like the carrier' of E -defined Function-like non empty total V53() ManySortedFunction of the Arity of E * ( the Sorts of x #), the ResultSort of E * the Sorts of x
the Sorts of x # is Relation-like the carrier of E * -defined Function-like non empty total set
the Arity of E * ( the Sorts of x #) is Relation-like the carrier' of E -defined Function-like non empty total set
the ResultSort of E * the Sorts of x is Relation-like the carrier' of E -defined Function-like non empty total set
the Charact of x . o is set
( the Arity of E * ( the Sorts of x #)) . o is set
( the ResultSort of E * the Sorts of x) . o is set
K20((( the Arity of E * ( the Sorts of x #)) . o),(( the ResultSort of E * the Sorts of x) . o)) is Relation-like set
K19(K20((( the Arity of E * ( the Sorts of x #)) . o),(( the ResultSort of E * the Sorts of x) . o))) is set
dom the ResultSort of E is non empty Element of K19( the carrier' of E)
K19( the carrier' of E) is set
dom the Arity of E is non empty Element of K19( the carrier' of E)
S is non empty feasible feasible ManySortedSign
S9 is (S)
A is non empty feasible feasible ManySortedSign
A +* S is non empty feasible strict feasible ManySortedSign
the carrier' of S is set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
the carrier of S is non empty set
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
dom the ResultSort of S is Element of K19( the carrier' of S)
K19( the carrier' of S) is set
the ResultSort of (A +* S) is Relation-like the carrier' of (A +* S) -defined the carrier of (A +* S) -valued Function-like total V18( the carrier' of (A +* S), the carrier of (A +* S)) Element of K19(K20( the carrier' of (A +* S), the carrier of (A +* S)))
the carrier' of (A +* S) is set
the carrier of (A +* S) is non empty set
K20( the carrier' of (A +* S), the carrier of (A +* S)) is Relation-like set
K19(K20( the carrier' of (A +* S), the carrier of (A +* S))) is set
the ResultSort of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like total V18( the carrier' of A, the carrier of A) Element of K19(K20( the carrier' of A, the carrier of A))
the carrier' of A is set
the carrier of A is non empty set
K20( the carrier' of A, the carrier of A) is Relation-like set
K19(K20( the carrier' of A, the carrier of A)) is set
the ResultSort of A +* the ResultSort of S is Relation-like the carrier' of A \/ the carrier' of S -defined Function-like total set
the carrier' of A \/ the carrier' of S is set
the Arity of (A +* S) is Relation-like the carrier' of (A +* S) -defined the carrier of (A +* S) * -valued Function-like total V18( the carrier' of (A +* S), the carrier of (A +* S) * ) Element of K19(K20( the carrier' of (A +* S),( the carrier of (A +* S) *)))
the carrier of (A +* S) * is functional non empty FinSequence-membered M11( the carrier of (A +* S))
K20( the carrier' of (A +* S),( the carrier of (A +* S) *)) is Relation-like set
K19(K20( the carrier' of (A +* S),( the carrier of (A +* S) *))) is set
the Arity of A is Relation-like the carrier' of A -defined the carrier of A * -valued Function-like total V18( the carrier' of A, the carrier of A * ) Element of K19(K20( the carrier' of A,( the carrier of A *)))
the carrier of A * is functional non empty FinSequence-membered M11( the carrier of A)
K20( the carrier' of A,( the carrier of A *)) is Relation-like set
K19(K20( the carrier' of A,( the carrier of A *))) is set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Arity of A +* the Arity of S is Relation-like the carrier' of A \/ the carrier' of S -defined Function-like total set
x is MSAlgebra over A
the carrier of A \/ the carrier of S is non empty set
the Sorts of x is Relation-like the carrier of A -defined Function-like non empty total set
dom the Arity of S is Element of K19( the carrier' of S)
e is set
o is Relation-like the carrier of (A +* S) -defined Function-like non empty total set
the ResultSort of (A +* S) * o is Relation-like the carrier' of (A +* S) -defined Function-like total set
( the ResultSort of (A +* S) * o) . e is set
the ResultSort of (A +* S) . e is set
o . ( the ResultSort of (A +* S) . e) is set
p is non empty non void feasible feasible ManySortedSign
the carrier' of p is non empty set
q is Element of the carrier' of p
the Arity of (A +* S) . q is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
the_arity_of q is Relation-like K97() -defined the carrier of p -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of p *
the carrier of p is non empty set
the carrier of p * is functional non empty FinSequence-membered M11( the carrier of p)
the Arity of p is Relation-like the carrier' of p -defined the carrier of p * -valued Function-like non empty total V18( the carrier' of p, the carrier of p * ) Element of K19(K20( the carrier' of p,( the carrier of p *)))
K20( the carrier' of p,( the carrier of p *)) is Relation-like set
K19(K20( the carrier' of p,( the carrier of p *))) is set
the Arity of p . q is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of p *
the ResultSort of (A +* S) . q is set
the_result_sort_of q is Element of the carrier of p
the ResultSort of p is Relation-like the carrier' of p -defined the carrier of p -valued Function-like non empty total V18( the carrier' of p, the carrier of p) Element of K19(K20( the carrier' of p, the carrier of p))
K20( the carrier' of p, the carrier of p) is Relation-like set
K19(K20( the carrier' of p, the carrier of p)) is set
the ResultSort of p . q is Element of the carrier of p
the Charact of x is Relation-like the carrier' of A -defined Function-like total V53() ManySortedFunction of the Arity of A * ( the Sorts of x #), the ResultSort of A * the Sorts of x
the Sorts of x # is Relation-like the carrier of A * -defined Function-like non empty total set
the Arity of A * ( the Sorts of x #) is Relation-like the carrier' of A -defined Function-like total set
the ResultSort of A * the Sorts of x is Relation-like the carrier' of A -defined Function-like total set
the Charact of x . e is set
the Arity of (A +* S) . e is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
( the Sorts of x #) . ( the Arity of (A +* S) . e) is set
the Sorts of x . ( the ResultSort of (A +* S) . e) is set
K20((( the Sorts of x #) . ( the Arity of (A +* S) . e)),( the Sorts of x . ( the ResultSort of (A +* S) . e))) is Relation-like set
K19(K20((( the Sorts of x #) . ( the Arity of (A +* S) . e)),( the Sorts of x . ( the ResultSort of (A +* S) . e)))) is set
the Arity of A . e is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
the ResultSort of A . e is set
o # is Relation-like the carrier of (A +* S) * -defined Function-like non empty total set
the Arity of A * (o #) is Relation-like the carrier' of A -defined Function-like set
( the Arity of A * (o #)) . e is set
(o #) . ( the Arity of A . e) is set
the Arity of (A +* S) * (o #) is Relation-like the carrier' of (A +* S) -defined Function-like total set
( the Arity of (A +* S) * (o #)) . e is set
(o #) . ( the Arity of (A +* S) . e) is set
the ResultSort of A * o is Relation-like the carrier' of A -defined Function-like set
( the ResultSort of A * o) . e is set
o . ( the ResultSort of A . e) is set
K20((( the Arity of (A +* S) * (o #)) . e),(( the ResultSort of (A +* S) * o) . e)) is Relation-like set
K19(K20((( the Arity of (A +* S) * (o #)) . e),(( the ResultSort of (A +* S) * o) . e))) is set
e is Relation-like the carrier' of (A +* S) -defined Function-like total V53() ManySortedFunction of the Arity of (A +* S) * (o #), the ResultSort of (A +* S) * o
MSAlgebra(# o,e #) is strict MSAlgebra over A +* S
the Sorts of MSAlgebra(# o,e #) is Relation-like the carrier of (A +* S) -defined Function-like non empty total set
S is non empty feasible feasible ManySortedSign
S9 is non empty feasible feasible ManySortedSign
the carrier of S is non empty set
the carrier of S9 is non empty set
the carrier' of S is set
the carrier' of S9 is set
A is MSAlgebra over S
the Sorts of A is Relation-like the carrier of S -defined Function-like non empty total set
E is MSAlgebra over S9
the Sorts of E is Relation-like the carrier of S9 -defined Function-like non empty total set
dom the Sorts of A is non empty Element of K19( the carrier of S)
K19( the carrier of S) is set
the Charact of A is Relation-like the carrier' of S -defined Function-like total V53() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Sorts of A # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ( the Sorts of A #) is Relation-like the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S * the Sorts of A is Relation-like the carrier' of S -defined Function-like total set
the Charact of E is Relation-like the carrier' of S9 -defined Function-like total V53() ManySortedFunction of the Arity of S9 * ( the Sorts of E #), the ResultSort of S9 * the Sorts of E
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set
the Sorts of E # is Relation-like the carrier of S9 * -defined Function-like non empty total set
the Arity of S9 * ( the Sorts of E #) is Relation-like the carrier' of S9 -defined Function-like total set
the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like total V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
K20( the carrier' of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier of S9)) is set
the ResultSort of S9 * the Sorts of E is Relation-like the carrier' of S9 -defined Function-like total set
dom the Charact of A is Element of K19( the carrier' of S)
K19( the carrier' of S) is set
S is non empty non void feasible feasible ManySortedSign
S9 is non-empty disjoint_valued feasible non empty MSAlgebra over S
the Sorts of S9 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the carrier of S is non empty set
A is set
dom the Sorts of S9 is non empty set
E is set
the Sorts of S9 . A is set
the Sorts of S9 . E is set
dom the Sorts of S9 is non empty Element of K19( the carrier of S)
K19( the carrier of S) is set
x is Element of the carrier of S
the Sorts of S9 . x is non empty set
o is Element of the carrier of S
the Sorts of S9 . o is non empty set
S is non empty non void feasible feasible ManySortedSign
S9 is disjoint_valued MSAlgebra over S
the Sorts of S9 is Relation-like the carrier of S -defined Function-like non empty total set
the carrier of S is non empty set
rng the Sorts of S9 is non empty set
A is Element of rng the Sorts of S9
E is Element of rng the Sorts of S9
dom the Sorts of S9 is non empty Element of K19( the carrier of S)
K19( the carrier of S) is set
x is set
the Sorts of S9 . x is set
o is set
the Sorts of S9 . o is set
S is non empty non void feasible feasible ManySortedSign
S9 is non empty non void feasible feasible ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) is non empty non void feasible strict feasible ManySortedSign
the carrier of S9 is non empty set
the carrier' of S9 is non empty set
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like non empty total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set
the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like non empty total V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
K20( the carrier' of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier of S9)) is set
ManySortedSign(# the carrier of S9, the carrier' of S9, the Arity of S9, the ResultSort of S9 #) is non empty non void feasible strict feasible ManySortedSign
A is non-empty disjoint_valued feasible non empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like one-to-one non empty total set
dom the Sorts of A is non empty Element of K19( the carrier of S)
K19( the carrier of S) is set
x is set
o is Element of the carrier' of S
Args (o,A) is non empty Element of rng ( the Sorts of A #)
the Sorts of A # is Relation-like the carrier of S * -defined Function-like non empty total set
rng ( the Sorts of A #) is non empty set
the Arity of S * ( the Sorts of A #) is Relation-like the carrier' of S -defined Function-like non empty total set
( the Arity of S * ( the Sorts of A #)) . o is set
the Element of Args (o,A) is Element of Args (o,A)
e is Element of the carrier' of S9
E is MSAlgebra over S9
Den (e,E) is Relation-like Args (e,E) -defined Result (e,E) -valued Function-like V18( Args (e,E), Result (e,E)) Element of K19(K20((Args (e,E)),(Result (e,E))))
Args (e,E) is Element of rng ( the Sorts of E #)
the Sorts of E is Relation-like the carrier of S9 -defined Function-like non empty total set
the Sorts of E # is Relation-like the carrier of S9 * -defined Function-like non empty total set
rng ( the Sorts of E #) is non empty set
the Arity of S9 * ( the Sorts of E #) is Relation-like the carrier' of S9 -defined Function-like non empty total set
( the Arity of S9 * ( the Sorts of E #)) . e is set
Result (e,E) is Element of rng the Sorts of E
rng the Sorts of E is non empty set
the ResultSort of S9 * the Sorts of E is Relation-like the carrier' of S9 -defined Function-like non empty total set
( the ResultSort of S9 * the Sorts of E) . e is set
K20((Args (e,E)),(Result (e,E))) is Relation-like set
K19(K20((Args (e,E)),(Result (e,E)))) is set
the Charact of E is Relation-like the carrier' of S9 -defined Function-like non empty total V53() ManySortedFunction of the Arity of S9 * ( the Sorts of E #), the ResultSort of S9 * the Sorts of E
the Charact of E . e is set
Result (o,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty V36() set
the ResultSort of S * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of A) . o is non empty set
Den (o,A) is Relation-like Args (o,A) -defined Result (o,A) -valued Function-like non empty total V18( Args (o,A), Result (o,A)) Element of K19(K20((Args (o,A)),(Result (o,A))))
K20((Args (o,A)),(Result (o,A))) is Relation-like set
K19(K20((Args (o,A)),(Result (o,A)))) is set
the Charact of A is Relation-like the carrier' of S -defined Function-like non empty total V53() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A
the Charact of A . o is set
rng (Den (o,A)) is non empty Element of K19((Result (o,A)))
K19((Result (o,A))) is set
(Den (o,A)) . the Element of Args (o,A) is Element of Result (o,A)
( the ResultSort of S9 * the Sorts of E) . x is set
the ResultSort of S9 . e is Element of the carrier of S9
the Sorts of E . ( the ResultSort of S9 . e) is set
the Sorts of A . ( the ResultSort of S9 . e) is set
the ResultSort of S . o is Element of the carrier of S
the Sorts of A . ( the ResultSort of S . o) is non empty set
the ResultSort of S . x is set
the ResultSort of S9 . x is set
x is set
o is Element of the carrier' of S
e is Element of the carrier' of S9
the Arity of S9 . e is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S9 *
the Arity of S . o is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
Den (e,E) is Relation-like Args (e,E) -defined Result (e,E) -valued Function-like V18( Args (e,E), Result (e,E)) Element of K19(K20((Args (e,E)),(Result (e,E))))
Args (e,E) is Element of rng ( the Sorts of E #)
( the Arity of S9 * ( the Sorts of E #)) . e is set
Result (e,E) is Element of rng the Sorts of E
( the ResultSort of S9 * the Sorts of E) . e is set
K20((Args (e,E)),(Result (e,E))) is Relation-like set
K19(K20((Args (e,E)),(Result (e,E)))) is set
the Charact of E . e is set
Args (o,A) is non empty Element of rng ( the Sorts of A #)
( the Arity of S * ( the Sorts of A #)) . o is set
Den (o,A) is Relation-like Args (o,A) -defined Result (o,A) -valued Function-like non empty total V18( Args (o,A), Result (o,A)) Element of K19(K20((Args (o,A)),(Result (o,A))))
Result (o,A) is non empty Element of rng the Sorts of A
( the ResultSort of S * the Sorts of A) . o is non empty set
K20((Args (o,A)),(Result (o,A))) is Relation-like set
K19(K20((Args (o,A)),(Result (o,A)))) is set
the Charact of A . o is set
dom (Den (o,A)) is non empty Element of K19((Args (o,A)))
K19((Args (o,A))) is set
p is Relation-like K97() -defined the carrier of S9 -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S9 *
( the Sorts of E #) . p is set
p * the Sorts of E is Relation-like K97() -defined Function-like set
product (p * the Sorts of E) is set
p * the Sorts of A is Relation-like non-empty K97() -defined Function-like set
product (p * the Sorts of A) is set
q is Relation-like K97() -defined the carrier of S -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of S *
( the Sorts of A #) . q is set
q * the Sorts of A is Relation-like non-empty K97() -defined Function-like set
product (q * the Sorts of A) is set
rng q is Element of K19( the carrier of S)
dom (q * the Sorts of A) is Element of K19(K97())
dom q is Element of K19(K97())
rng p is Element of K19( the carrier of S9)
K19( the carrier of S9) is set
dom (p * the Sorts of E) is Element of K19(K97())
dom p is Element of K19(K97())
the Arity of S . x is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
the Arity of S9 . x is Relation-like K97() -defined Function-like V31() FinSequence-like FinSubsequence-like set
dom the Arity of S9 is non empty Element of K19( the carrier' of S9)
K19( the carrier' of S9) is set
dom the Arity of S is non empty Element of K19( the carrier' of S)
K19( the carrier' of S) is set
dom the ResultSort of S9 is non empty Element of K19( the carrier' of S9)
dom the ResultSort of S is non empty Element of K19( the carrier' of S)
S is non empty non void feasible feasible ManySortedSign
S9 is non empty non void feasible feasible ManySortedSign
A is non-empty disjoint_valued feasible non empty MSAlgebra over S
E is non empty non void feasible feasible (S9)
the carrier of S is non empty set
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) Element of K19(K20( the carrier' of S,( the carrier of S *)))
the carrier of S * is functional non empty FinSequence-membered M11( the carrier of S)
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) is non empty non void feasible strict feasible ManySortedSign
the carrier of E is non empty set
the carrier' of E is non empty set
the Arity of E is Relation-like the carrier' of E -defined the carrier of E * -valued Function-like non empty total V18( the carrier' of E, the carrier of E * ) Element of K19(K20( the carrier' of E,( the carrier of E *)))
the carrier of E * is functional non empty FinSequence-membered M11( the carrier of E)
K20( the carrier' of E,( the carrier of E *)) is Relation-like set
K19(K20( the carrier' of E,( the carrier of E *))) is set
the ResultSort of E is Relation-like the carrier' of E -defined the carrier of E -valued Function-like non empty total V18( the carrier' of E, the carrier of E) Element of K19(K20( the carrier' of E, the carrier of E))
K20( the carrier' of E, the carrier of E) is Relation-like set
K19(K20( the carrier' of E, the carrier of E)) is set
ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #) is non empty non void feasible strict feasible ManySortedSign
the carrier' of S9 is non empty set
the carrier of S9 is non empty set
the ResultSort of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 -valued Function-like non empty total V18( the carrier' of S9, the carrier of S9) Element of K19(K20( the carrier' of S9, the carrier of S9))
K20( the carrier' of S9, the carrier of S9) is Relation-like set
K19(K20( the carrier' of S9, the carrier of S9)) is set
the carrier of S9 * is functional non empty FinSequence-membered M11( the carrier of S9)
the Arity of S9 is Relation-like the carrier' of S9 -defined the carrier of S9 * -valued Function-like non empty total V18( the carrier' of S9, the carrier of S9 * ) Element of K19(K20( the carrier' of S9,( the carrier of S9 *)))
K20( the carrier' of S9,( the carrier of S9 *)) is Relation-like set
K19(K20( the carrier' of S9,( the carrier of S9 *))) is set