:: 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

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

dom S is set

dom S9 is set
(dom S) /\ (dom S9) is set

dom A is set

(S +* S9) +* A 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

rng A is set
dom S9 is set
(rng A) /\ (dom S9) is set
dom S is 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

dom S is set

rng A is set

dom A is set
S9 .: (dom A) is set

(S9 +* A) * 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

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

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)

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

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

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 *)))

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)

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

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 *))

gg is set

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) . 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

(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

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

(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

(S,S9) is Relation-like S -defined Function-like non empty total 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

dom A 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

(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) . S9 is set
S is set

dom S9 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

(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

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

(id S) +* (S9 | S) is Relation-like Function-like set
(S,(S,S9)) is Relation-like S -defined Function-like total 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

(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

(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

(id S) +* (S9 | S) is Relation-like Function-like set

(S,(id S)) is Relation-like S -defined Function-like total set

(id S) +* ((id S) | S) is Relation-like S -defined S -valued Function-like total 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

(id S) +* ({} | S) is Relation-like Function-like set
S is set

dom S9 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

(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

K20({},{}) is Relation-like set
K19(K20({},{})) is set

S is set
S9 is 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

(id S9) +* (A | S9) is Relation-like Function-like set
(S9,A) | S is Relation-like S -defined S9 -defined Function-like 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

(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

((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

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

(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

(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

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

(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

(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

((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

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

(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

(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

rng A is set

(S,S9) is Relation-like S -defined Function-like non empty total 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

dom S is set

dom S9 is set
rng S9 is set
A is 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

(id A) +* (S9 | A) is Relation-like Function-like set
(A,S9) * S is Relation-like A -defined 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

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

dom S9 is set
rng S9 is set
A is 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

rng S9 is set
dom S is set
dom S9 is 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 (S9 * S) is 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) . 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

dom (S ") is 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

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 \/ S9 is Relation-like set

E is Relation-like Function-like (S9)

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) +* (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

the Relation-like Function-like (S9) is Relation-like Function-like (S9)

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

( 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

(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 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

rng () is Element of K19( the carrier of S)
K19( the carrier of S) is set
x is Element of the carrier' of S

rng () 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
() * ((id the carrier of S) +* S9) is Relation-like K97() -defined Function-like set
() * ((id the carrier of S) +* S9) is Relation-like K97() -defined Function-like set
() * ( the carrier of S,S9) is Relation-like K97() -defined Function-like set
() * ( 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) . is set
((id the carrier of S) +* S9) . 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) . is set
( the carrier of S,S9) . 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

() * ((id the carrier of S) +* S9) is Relation-like K97() -defined Function-like set

() * ((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) . 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) . is set
rng () is Element of K19( the carrier of S)
rng () 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 carrier of S,S9) is Relation-like K97() -defined Function-like set
() * ( the carrier of S,S9) is Relation-like K97() -defined Function-like set
( the carrier of S,S9) . is set
( the carrier of S,S9) . 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

( 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

(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 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 carrier of S,S9) is Relation-like K97() -defined Function-like set

() * ( 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) . 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) . 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 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 carrier of S,S9) is Relation-like K97() -defined Function-like set

() * ( 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) . 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) . is set
S is non empty non void feasible feasible ManySortedSign
S9 is non empty non void feasible feasible ManySortedSign

the carrier of S is non empty set
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 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

(id the carrier of S) +* A is Relation-like Function-like non empty set
() * ((id the carrier of S) +* A) is Relation-like K97() -defined Function-like set

() * ((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) . 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) . 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

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

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 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

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
() * ((id the carrier of S) +* S9) is Relation-like K97() -defined Function-like set

() * ((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) . 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) . 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

rng S9 is set
the carrier' of S /\ (rng S9) is set
dom S9 is set

id the carrier' of S is Relation-like the carrier' of S -defined the carrier' of S -valued Function-like one-to-one non empty total V18( the carrier' of S, the carrier' of S) Element of K19(K20( the carrier' of S, the carrier' of S))
K20( the carrier' of S, the carrier' of S) is Relation-like set
K19(K20( the carrier' of S, the carrier' of S)) is set
(id the carrier' of S) +* 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 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

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
() * ((id the carrier of S) +* A) is Relation-like K97() -defined Function-like set

() * ((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) . 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) . 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

rng S9 is set

the carrier' of S /\ (rng S9) is set
dom S9 is set
S9 is non empty set
S is set

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

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

(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) . 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) . 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

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 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 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

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 . is Element of p
(a * the ResultSort of S) . o is Element of p
o is 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 * ( 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 (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 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