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