:: ALGSPEC1 semantic presentation

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