:: EXTENS_1 semantic presentation

K127() is Element of K19(K123())

K123() is set

K19(K123()) is set

K89() is set

K19(K89()) is set

K19(K127()) is set

{} is set

the Function-like functional empty V55() set is Function-like functional empty V55() set

1 is non empty set

{{},1} is set

K262() is set

K19(K262()) is set

K263() is Element of K19(K262())

K303() is non empty strict DTConstrStr

the carrier of K303() is non empty set

K266( the carrier of K303()) is non empty M20( the carrier of K303())

K302(K303()) is Element of K19(K266( the carrier of K303()))

K19(K266( the carrier of K303())) is set

K20(K302(K303()),K127()) is set

K19(K20(K302(K303()),K127())) is set

K20(K127(),K302(K303())) is set

K19(K20(K127(),K302(K303()))) is set

2 is non empty set

3 is non empty set

S is set

U1 is Relation-like S -defined Function-like total set

U2 is Relation-like S -defined Function-like total set

Gen is Relation-like S -defined Function-like total set

h1 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,U2

h2 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U2,Gen

h2 ** h1 is Relation-like Function-like Function-yielding V37() set

dom (h2 ** h1) is set

dom h1 is Element of K19(S)

K19(S) is set

dom h2 is Element of K19(S)

(dom h1) /\ (dom h2) is Element of K19(S)

S /\ (dom h2) is Element of K19(S)

S /\ S is set

S is set

U1 is Relation-like S -defined Function-like total set

U2 is Relation-like non-empty S -defined Function-like total set

Gen is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,U2

h1 is Relation-like S -defined Function-like total ManySortedSubset of U1

Gen || h1 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of h1,U2

h2 is set

U1 . h2 is set

U2 . h2 is set

K20((U1 . h2),(U2 . h2)) is set

K19(K20((U1 . h2),(U2 . h2))) is set

Gen . h2 is Relation-like Function-like set

h1 . h2 is set

(Gen || h1) . h2 is Relation-like Function-like set

I is Relation-like U1 . h2 -defined U2 . h2 -valued Function-like V18(U1 . h2,U2 . h2) Element of K19(K20((U1 . h2),(U2 . h2)))

I | (h1 . h2) is Relation-like U1 . h2 -defined U2 . h2 -valued Function-like Element of K19(K20((U1 . h2),(U2 . h2)))

S is set

U1 is Relation-like S -defined Function-like total set

U2 is Relation-like S -defined Function-like total set

Gen is Relation-like S -defined Function-like total ManySortedSubset of U1

h1 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,U2

h1 .:.: Gen is Relation-like S -defined Function-like total set

h1 .:.: U1 is Relation-like S -defined Function-like total set

h2 is set

(h1 .:.: Gen) . h2 is set

(h1 .:.: U1) . h2 is set

U1 . h2 is set

U2 . h2 is set

K20((U1 . h2),(U2 . h2)) is set

K19(K20((U1 . h2),(U2 . h2))) is set

h1 . h2 is Relation-like Function-like set

I is Relation-like U1 . h2 -defined U2 . h2 -valued Function-like V18(U1 . h2,U2 . h2) Element of K19(K20((U1 . h2),(U2 . h2)))

Gen . h2 is set

I .: (Gen . h2) is set

I .: (U1 . h2) is set

A is set

S is set

U1 is Relation-like S -defined Function-like total set

U2 is Relation-like non-empty S -defined Function-like total set

Gen is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,U2

h1 is Relation-like S -defined Function-like total ManySortedSubset of U1

h2 is Relation-like S -defined Function-like total ManySortedSubset of U1

Gen || h2 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of h2,U2

(Gen || h2) .:.: h1 is Relation-like S -defined Function-like total set

Gen .:.: h1 is Relation-like S -defined Function-like total set

I is set

U1 . I is set

U2 . I is set

K20((U1 . I),(U2 . I)) is set

K19(K20((U1 . I),(U2 . I))) is set

Gen . I is Relation-like Function-like set

h2 . I is set

K20((h2 . I),(U2 . I)) is set

K19(K20((h2 . I),(U2 . I))) is set

(Gen || h2) . I is Relation-like Function-like set

h1 . I is set

A is Relation-like h2 . I -defined U2 . I -valued Function-like V18(h2 . I,U2 . I) Element of K19(K20((h2 . I),(U2 . I)))

A is Relation-like U1 . I -defined U2 . I -valued Function-like V18(U1 . I,U2 . I) Element of K19(K20((U1 . I),(U2 . I)))

A | (h2 . I) is Relation-like U1 . I -defined U2 . I -valued Function-like Element of K19(K20((U1 . I),(U2 . I)))

((Gen || h2) .:.: h1) . I is set

(A | (h2 . I)) .: (h1 . I) is set

A .: (h1 . I) is set

(Gen .:.: h1) . I is set

S is set

U1 is Relation-like S -defined Function-like total set

U2 is Relation-like non-empty S -defined Function-like total set

Gen is Relation-like non-empty S -defined Function-like total set

h1 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,U2

h2 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U2,Gen

h2 ** h1 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,Gen

I is Relation-like S -defined Function-like total ManySortedSubset of U1

(h2 ** h1) || I is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of I,Gen

h1 || I is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of I,U2

h2 ** (h1 || I) is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of I,Gen

A is set

U1 . A is set

Gen . A is set

K20((U1 . A),(Gen . A)) is set

K19(K20((U1 . A),(Gen . A))) is set

(h2 ** h1) . A is Relation-like Function-like set

I . A is set

U2 . A is set

K20((I . A),(U2 . A)) is set

K19(K20((I . A),(U2 . A))) is set

(h1 || I) . A is Relation-like Function-like set

K20((U2 . A),(Gen . A)) is set

K19(K20((U2 . A),(Gen . A))) is set

h2 . A is Relation-like Function-like set

K20((U1 . A),(U2 . A)) is set

K19(K20((U1 . A),(U2 . A))) is set

h1 . A is Relation-like Function-like set

((h2 ** h1) || I) . A is Relation-like Function-like set

A is Relation-like U1 . A -defined Gen . A -valued Function-like V18(U1 . A,Gen . A) Element of K19(K20((U1 . A),(Gen . A)))

A | (I . A) is Relation-like U1 . A -defined Gen . A -valued Function-like Element of K19(K20((U1 . A),(Gen . A)))

x is Relation-like U1 . A -defined U2 . A -valued Function-like V18(U1 . A,U2 . A) Element of K19(K20((U1 . A),(U2 . A)))

s is Relation-like U2 . A -defined Gen . A -valued Function-like V18(U2 . A,Gen . A) Element of K19(K20((U2 . A),(Gen . A)))

s * x is Relation-like U1 . A -defined Gen . A -valued Function-like Element of K19(K20((U1 . A),(Gen . A)))

(s * x) | (I . A) is Relation-like U1 . A -defined Gen . A -valued Function-like Element of K19(K20((U1 . A),(Gen . A)))

x | (I . A) is Relation-like U1 . A -defined U2 . A -valued Function-like Element of K19(K20((U1 . A),(U2 . A)))

s * (x | (I . A)) is Relation-like U1 . A -defined Gen . A -valued Function-like Element of K19(K20((U1 . A),(Gen . A)))

i is Relation-like I . A -defined U2 . A -valued Function-like V18(I . A,U2 . A) Element of K19(K20((I . A),(U2 . A)))

s * i is Relation-like I . A -defined Gen . A -valued Function-like Element of K19(K20((I . A),(Gen . A)))

K20((I . A),(Gen . A)) is set

K19(K20((I . A),(Gen . A))) is set

(h2 ** (h1 || I)) . A is Relation-like Function-like set

S is set

U1 is Relation-like S -defined Function-like total set

U2 is Relation-like S -defined Function-like total set

Gen is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,U2

h1 is Relation-like S -defined Function-like total set

h2 is set

Gen . h2 is Relation-like Function-like set

U1 . h2 is set

h1 . h2 is set

K20((U1 . h2),(h1 . h2)) is set

K19(K20((U1 . h2),(h1 . h2))) is set

U2 . h2 is set

K20((U1 . h2),(U2 . h2)) is set

K19(K20((U1 . h2),(U2 . h2))) is set

S is set

U1 is Relation-like S -defined Function-like total set

U2 is Relation-like non-empty S -defined Function-like total set

Gen is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,U2

h1 is Relation-like S -defined Function-like total ManySortedSubset of U1

Gen || h1 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of h1,U2

h2 is set

U1 . h2 is set

U2 . h2 is set

K20((U1 . h2),(U2 . h2)) is set

K19(K20((U1 . h2),(U2 . h2))) is set

Gen . h2 is Relation-like Function-like set

I is Relation-like U1 . h2 -defined U2 . h2 -valued Function-like V18(U1 . h2,U2 . h2) Element of K19(K20((U1 . h2),(U2 . h2)))

h1 . h2 is set

I | (h1 . h2) is Relation-like U1 . h2 -defined U2 . h2 -valued Function-like Element of K19(K20((U1 . h2),(U2 . h2)))

(Gen || h1) . h2 is Relation-like Function-like set

S is set

U1 is Relation-like S -defined Function-like total set

U2 is Relation-like non-empty S -defined Function-like total set

Gen is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,U2

doms Gen is Relation-like S -defined Function-like total set

h1 is Relation-like S -defined Function-like total ManySortedSubset of U1

Gen || h1 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of h1,U2

doms (Gen || h1) is Relation-like S -defined Function-like total set

h2 is set

(doms (Gen || h1)) . h2 is set

(doms Gen) . h2 is set

dom (Gen || h1) is Element of K19(S)

K19(S) is set

U1 . h2 is set

U2 . h2 is set

K20((U1 . h2),(U2 . h2)) is set

K19(K20((U1 . h2),(U2 . h2))) is set

Gen . h2 is Relation-like Function-like set

dom Gen is Element of K19(S)

I is Relation-like U1 . h2 -defined U2 . h2 -valued Function-like V18(U1 . h2,U2 . h2) Element of K19(K20((U1 . h2),(U2 . h2)))

dom I is Element of K19((U1 . h2))

K19((U1 . h2)) is set

(Gen || h1) . h2 is Relation-like Function-like set

h1 . h2 is set

I | (h1 . h2) is Relation-like U1 . h2 -defined U2 . h2 -valued Function-like Element of K19(K20((U1 . h2),(U2 . h2)))

dom (I | (h1 . h2)) is Element of K19((U1 . h2))

S is set

U1 is Relation-like S -defined Function-like total set

U2 is Relation-like non-empty S -defined Function-like total set

Gen is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,U2

rngs Gen is Relation-like S -defined Function-like total set

h1 is Relation-like S -defined Function-like total ManySortedSubset of U1

Gen || h1 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of h1,U2

rngs (Gen || h1) is Relation-like S -defined Function-like total set

h2 is set

(rngs (Gen || h1)) . h2 is set

(rngs Gen) . h2 is set

dom (Gen || h1) is Element of K19(S)

K19(S) is set

U1 . h2 is set

U2 . h2 is set

K20((U1 . h2),(U2 . h2)) is set

K19(K20((U1 . h2),(U2 . h2))) is set

Gen . h2 is Relation-like Function-like set

dom Gen is Element of K19(S)

I is Relation-like U1 . h2 -defined U2 . h2 -valued Function-like V18(U1 . h2,U2 . h2) Element of K19(K20((U1 . h2),(U2 . h2)))

rng I is set

(Gen || h1) . h2 is Relation-like Function-like set

h1 . h2 is set

I | (h1 . h2) is Relation-like U1 . h2 -defined U2 . h2 -valued Function-like Element of K19(K20((U1 . h2),(U2 . h2)))

rng (I | (h1 . h2)) is set

S is set

U1 is Relation-like S -defined Function-like total set

U2 is Relation-like S -defined Function-like total set

Gen is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,U2

rngs Gen is Relation-like S -defined Function-like total set

dom Gen is Element of K19(S)

K19(S) is set

h1 is set

U1 . h1 is set

U2 . h1 is set

K20((U1 . h1),(U2 . h1)) is set

K19(K20((U1 . h1),(U2 . h1))) is set

Gen . h1 is Relation-like Function-like set

h2 is Relation-like U1 . h1 -defined U2 . h1 -valued Function-like V18(U1 . h1,U2 . h1) Element of K19(K20((U1 . h1),(U2 . h1)))

rng h2 is set

(rngs Gen) . h1 is set

h1 is set

Gen . h1 is Relation-like Function-like set

rng (Gen . h1) is set

U2 . h1 is set

S is non empty non void V51() ManySortedSign

the carrier of S is non empty set

U1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

Reverse U1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of FreeGen U1,U1

FreeGen U1 is Relation-like the carrier of S -defined Function-like non empty total GeneratorSet of FreeMSA U1

FreeMSA U1 is strict non-empty MSAlgebra over S

rngs (Reverse U1) is Relation-like the carrier of S -defined Function-like non empty total set

h1 is set

(FreeGen U1) . h1 is set

U1 . h1 is set

K20(((FreeGen U1) . h1),(U1 . h1)) is set

K19(K20(((FreeGen U1) . h1),(U1 . h1))) is set

(Reverse U1) . h1 is Relation-like Function-like set

dom (Reverse U1) is Element of K19( the carrier of S)

K19( the carrier of S) is set

(rngs (Reverse U1)) . h1 is set

DTConMSA U1 is non empty strict V113() V114() V115() DTConstrStr

A is set

h2 is Relation-like (FreeGen U1) . h1 -defined U1 . h1 -valued Function-like V18((FreeGen U1) . h1,U1 . h1) Element of K19(K20(((FreeGen U1) . h1),(U1 . h1)))

rng h2 is set

A is set

I is Element of the carrier of S

[A,I] is V15() set

{A,I} is set

{A} is set

{{A,I},{A}} is set

Terminals (DTConMSA U1) is non empty Element of K19( the carrier of (DTConMSA U1))

the carrier of (DTConMSA U1) is non empty set

K19( the carrier of (DTConMSA U1)) is set

i is Element of the carrier of (DTConMSA U1)

i `2 is set

root-tree i is Element of K266( the carrier of (DTConMSA U1))

K266( the carrier of (DTConMSA U1)) is non empty M20( the carrier of (DTConMSA U1))

{ (root-tree b

FreeGen (I,U1) is non empty Element of K19(((FreeSort U1) . I))

FreeSort U1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

(FreeSort U1) . I is non empty set

K19(((FreeSort U1) . I)) is set

(FreeGen U1) . I is set

U1 . I is non empty set

(Reverse U1) . I is Relation-like (FreeGen U1) . I -defined U1 . I -valued Function-like V18((FreeGen U1) . I,U1 . I) Element of K19(K20(((FreeGen U1) . I),(U1 . I)))

K20(((FreeGen U1) . I),(U1 . I)) is set

K19(K20(((FreeGen U1) . I),(U1 . I))) is set

Reverse (I,U1) is Relation-like FreeGen (I,U1) -defined U1 . I -valued Function-like V18( FreeGen (I,U1),U1 . I) Element of K19(K20((FreeGen (I,U1)),(U1 . I)))

K20((FreeGen (I,U1)),(U1 . I)) is set

K19(K20((FreeGen (I,U1)),(U1 . I))) is set

((Reverse U1) . I) . (root-tree i) is set

i `1 is set

dom ((Reverse U1) . I) is Element of K19(((FreeGen U1) . I))

K19(((FreeGen U1) . I)) is set

rng ((Reverse U1) . I) is set

S is set

U1 is Relation-like S -defined Function-like total set

U2 is Relation-like non-empty S -defined Function-like total set

Gen is Relation-like non-empty S -defined Function-like total set

h1 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,U2

rngs h1 is Relation-like S -defined Function-like total set

h2 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U2,Gen

h2 ** h1 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,Gen

I is Relation-like non-empty S -defined Function-like total ManySortedSubset of U2

h2 || I is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of I,Gen

(h2 || I) ** h1 is Relation-like Function-like Function-yielding V37() set

dom h1 is Element of K19(S)

K19(S) is set

A is set

h1 . A is Relation-like Function-like set

U1 . A is set

I . A is set

K20((U1 . A),(I . A)) is set

K19(K20((U1 . A),(I . A))) is set

U2 . A is set

K20((U1 . A),(U2 . A)) is set

K19(K20((U1 . A),(U2 . A))) is set

(rngs h1) . A is set

A is Relation-like U1 . A -defined U2 . A -valued Function-like V18(U1 . A,U2 . A) Element of K19(K20((U1 . A),(U2 . A)))

dom A is Element of K19((U1 . A))

K19((U1 . A)) is set

rng A is set

A is set

U1 . A is set

U2 . A is set

K20((U1 . A),(U2 . A)) is set

K19(K20((U1 . A),(U2 . A))) is set

h1 . A is Relation-like Function-like set

(rngs h1) . A is set

A is Relation-like U1 . A -defined U2 . A -valued Function-like V18(U1 . A,U2 . A) Element of K19(K20((U1 . A),(U2 . A)))

rng A is set

I . A is set

dom A is Element of K19((U1 . A))

K19((U1 . A)) is set

K20((U1 . A),(I . A)) is set

K19(K20((U1 . A),(I . A))) is set

Gen . A is set

K20((U2 . A),(Gen . A)) is set

K19(K20((U2 . A),(Gen . A))) is set

h2 . A is Relation-like Function-like set

i is Relation-like U1 . A -defined I . A -valued Function-like V18(U1 . A,I . A) Element of K19(K20((U1 . A),(I . A)))

rng i is set

K20((I . A),(Gen . A)) is set

K19(K20((I . A),(Gen . A))) is set

(h2 || I) . A is Relation-like Function-like set

((h2 || I) ** h1) . A is Relation-like Function-like set

x is Relation-like I . A -defined Gen . A -valued Function-like V18(I . A,Gen . A) Element of K19(K20((I . A),(Gen . A)))

x * i is Relation-like U1 . A -defined Gen . A -valued Function-like Element of K19(K20((U1 . A),(Gen . A)))

K20((U1 . A),(Gen . A)) is set

K19(K20((U1 . A),(Gen . A))) is set

s is Relation-like U2 . A -defined Gen . A -valued Function-like V18(U2 . A,Gen . A) Element of K19(K20((U2 . A),(Gen . A)))

s | (I . A) is Relation-like U2 . A -defined Gen . A -valued Function-like Element of K19(K20((U2 . A),(Gen . A)))

(s | (I . A)) * A is Relation-like U1 . A -defined Gen . A -valued Function-like Element of K19(K20((U1 . A),(Gen . A)))

s * i is Relation-like U1 . A -defined Gen . A -valued Function-like Element of K19(K20((U1 . A),(Gen . A)))

(h2 ** h1) . A is Relation-like Function-like set

S is set

U1 is Relation-like S -defined Function-like total set

U2 is Relation-like non-empty S -defined Function-like total set

Gen is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,U2

h1 is Relation-like non-empty S -defined Function-like total set

h2 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U2,h1

h2 ** Gen is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,h1

I is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U2,h1

I ** Gen is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,h1

A is set

U1 . A is set

U2 . A is set

K20((U1 . A),(U2 . A)) is set

K19(K20((U1 . A),(U2 . A))) is set

Gen . A is Relation-like Function-like set

h1 . A is set

K20((U2 . A),(h1 . A)) is set

K19(K20((U2 . A),(h1 . A))) is set

I . A is Relation-like Function-like set

h2 . A is Relation-like Function-like set

A is Relation-like U1 . A -defined U2 . A -valued Function-like V18(U1 . A,U2 . A) Element of K19(K20((U1 . A),(U2 . A)))

rng A is set

s is Relation-like U2 . A -defined h1 . A -valued Function-like V18(U2 . A,h1 . A) Element of K19(K20((U2 . A),(h1 . A)))

s * A is Relation-like U1 . A -defined h1 . A -valued Function-like Element of K19(K20((U1 . A),(h1 . A)))

K20((U1 . A),(h1 . A)) is set

K19(K20((U1 . A),(h1 . A))) is set

(I ** Gen) . A is Relation-like Function-like set

i is Relation-like U2 . A -defined h1 . A -valued Function-like V18(U2 . A,h1 . A) Element of K19(K20((U2 . A),(h1 . A)))

i * A is Relation-like U1 . A -defined h1 . A -valued Function-like Element of K19(K20((U1 . A),(h1 . A)))

h1 is set

Gen . h1 is Relation-like Function-like set

rng (Gen . h1) is set

U2 . h1 is set

h2 is non empty set

A is Relation-like h2 -defined Function-like non empty total set

A is Relation-like h2 -defined Function-like non empty total set

I is Element of h2

A . I is set

A . I is set

K20((A . I),(A . I)) is set

K19(K20((A . I),(A . I))) is set

i is Relation-like h2 -defined Function-like non empty total Function-yielding V37() ManySortedFunction of A,A

i . I is Relation-like A . I -defined A . I -valued Function-like V18(A . I,A . I) Element of K19(K20((A . I),(A . I)))

s is Relation-like A . I -defined A . I -valued Function-like V18(A . I,A . I) Element of K19(K20((A . I),(A . I)))

x is set

K20((A . I),x) is set

K19(K20((A . I),x)) is set

ar is Relation-like A . I -defined x -valued Function-like V18(A . I,x) Element of K19(K20((A . I),x))

ar * s is Relation-like A . I -defined x -valued Function-like Element of K19(K20((A . I),x))

K20((A . I),x) is set

K19(K20((A . I),x)) is set

x is Relation-like A . I -defined x -valued Function-like V18(A . I,x) Element of K19(K20((A . I),x))

x * s is Relation-like A . I -defined x -valued Function-like Element of K19(K20((A . I),x))

ar is Relation-like A . I -defined x -valued Function-like V18(A . I,x) Element of K19(K20((A . I),x))

ar * (i . I) is Relation-like A . I -defined x -valued Function-like Element of K19(K20((A . I),x))

K20((A . I),x) is set

K19(K20((A . I),x)) is set

x is Relation-like A . I -defined x -valued Function-like V18(A . I,x) Element of K19(K20((A . I),x))

x * (i . I) is Relation-like A . I -defined x -valued Function-like Element of K19(K20((A . I),x))

x is Relation-like h2 -defined Function-like non empty total set

n is set

x . n is set

A . n is set

IFEQ (n,I,x,(A . n)) is set

A . n is set

IFEQ (n,I,x,(A . n)) is set

id A is Relation-like h2 -defined Function-like non empty total Function-yielding V37() ManySortedFunction of A,A

n is Relation-like h2 -defined Function-like non empty total set

n9 is Relation-like h2 -defined Function-like non empty total set

G is Relation-like A . I -defined x -valued Function-like V18(A . I,x) Element of K19(K20((A . I),x))

G * (i . I) is Relation-like A . I -defined x -valued Function-like Element of K19(K20((A . I),x))

H is Relation-like A . I -defined x -valued Function-like V18(A . I,x) Element of K19(K20((A . I),x))

H * (i . I) is Relation-like A . I -defined x -valued Function-like Element of K19(K20((A . I),x))

r is Relation-like h2 -defined Function-like non empty total set

G is set

dom r is set

r . G is set

dom r is Element of K19(h2)

K19(h2) is set

(id A) . G is Relation-like Function-like set

IFEQ (G,I,G,((id A) . G)) is set

(id A) . G is Relation-like Function-like set

IFEQ (G,I,G,((id A) . G)) is set

G is Relation-like A . I -defined x -valued Function-like V18(A . I,x) Element of K19(K20((A . I),x))

G * (i . I) is Relation-like A . I -defined x -valued Function-like Element of K19(K20((A . I),x))

H is Relation-like A . I -defined x -valued Function-like V18(A . I,x) Element of K19(K20((A . I),x))

H * (i . I) is Relation-like A . I -defined x -valued Function-like Element of K19(K20((A . I),x))

H is Relation-like h2 -defined Function-like non empty total Function-yielding V37() set

G is set

H . G is Relation-like Function-like set

A . G is set

x . G is set

K20((A . G),(x . G)) is set

K19(K20((A . G),(x . G))) is set

IFEQ (G,I,x,(A . G)) is set

(id A) . G is Relation-like Function-like set

IFEQ (G,I,G,((id A) . G)) is set

IFEQ (G,I,x,(A . G)) is set

(id A) . G is Relation-like Function-like set

IFEQ (G,I,G,((id A) . G)) is set

r is Relation-like h2 -defined Function-like non empty total Function-yielding V37() set

G is Relation-like h2 -defined Function-like non empty total Function-yielding V37() set

H is set

(id A) . H is Relation-like Function-like set

IFEQ (H,I,x,((id A) . H)) is set

G is Relation-like h2 -defined Function-like non empty total Function-yielding V37() ManySortedFunction of A,x

G . H is Relation-like Function-like set

IFEQ (H,I,ar,((id A) . H)) is set

H is Relation-like h2 -defined Function-like non empty total Function-yielding V37() ManySortedFunction of A,x

H . H is Relation-like Function-like set

H ** i is Relation-like Function-like Function-yielding V37() set

(H ** i) . H is Relation-like Function-like set

G ** i is Relation-like Function-like Function-yielding V37() set

(G ** i) . H is Relation-like Function-like set

A . H is set

x . H is set

K20((A . H),(x . H)) is set

K19(K20((A . H),(x . H))) is set

H is Relation-like h2 -defined Function-like non empty total Function-yielding V37() ManySortedFunction of A,x

H . H is Relation-like Function-like set

A . H is set

K20((A . H),(A . H)) is set

K19(K20((A . H),(A . H))) is set

i . H is Relation-like Function-like set

G is Relation-like h2 -defined Function-like non empty total Function-yielding V37() ManySortedFunction of A,x

G . H is Relation-like Function-like set

(id A) . H is Relation-like Function-like set

IFEQ (H,I,x,((id A) . H)) is set

IFEQ (H,I,ar,((id A) . H)) is set

G is Relation-like A . H -defined x . H -valued Function-like V18(A . H,x . H) Element of K19(K20((A . H),(x . H)))

h1 is Relation-like A . H -defined x . H -valued Function-like V18(A . H,x . H) Element of K19(K20((A . H),(x . H)))

H ** i is Relation-like Function-like Function-yielding V37() set

(H ** i) . H is Relation-like Function-like set

H is Relation-like A . H -defined A . H -valued Function-like V18(A . H,A . H) Element of K19(K20((A . H),(A . H)))

h1 * H is Relation-like A . H -defined x . H -valued Function-like Element of K19(K20((A . H),(x . H)))

K20((A . H),(x . H)) is set

K19(K20((A . H),(x . H))) is set

G ** i is Relation-like Function-like Function-yielding V37() set

(G ** i) . H is Relation-like Function-like set

H is Relation-like h2 -defined Function-like non empty total Function-yielding V37() ManySortedFunction of A,x

H ** i is Relation-like Function-like Function-yielding V37() set

(H ** i) . H is Relation-like Function-like set

G is Relation-like h2 -defined Function-like non empty total Function-yielding V37() ManySortedFunction of A,x

G ** i is Relation-like Function-like Function-yielding V37() set

(G ** i) . H is Relation-like Function-like set

H is Relation-like h2 -defined Function-like non empty total Function-yielding V37() ManySortedFunction of A,x

H ** i is Relation-like Function-like Function-yielding V37() set

(H ** i) . H is Relation-like Function-like set

G is Relation-like h2 -defined Function-like non empty total Function-yielding V37() ManySortedFunction of A,x

G ** i is Relation-like Function-like Function-yielding V37() set

(G ** i) . H is Relation-like Function-like set

H is Element of h2

H . H is Relation-like Function-like set

G . H is Relation-like Function-like set

(id A) . H is Relation-like A . H -defined A . H -valued Function-like V18(A . H,A . H) Element of K19(K20((A . H),(A . H)))

A . H is set

K20((A . H),(A . H)) is set

K19(K20((A . H),(A . H))) is set

IFEQ (H,I,x,((id A) . H)) is set

G . H is Relation-like A . H -defined x . H -valued Function-like V18(A . H,x . H) Element of K19(K20((A . H),(x . H)))

x . H is set

K20((A . H),(x . H)) is set

K19(K20((A . H),(x . H))) is set

IFEQ (H,I,ar,((id A) . H)) is set

H . H is Relation-like A . H -defined x . H -valued Function-like V18(A . H,x . H) Element of K19(K20((A . H),(x . H)))

H is set

H . H is Relation-like Function-like set

G . H is Relation-like Function-like set

x is Relation-like h2 -defined Function-like non empty total set

n is Relation-like h2 -defined Function-like non empty total Function-yielding V37() ManySortedFunction of A,x

n ** i is Relation-like Function-like Function-yielding V37() set

n9 is Relation-like h2 -defined Function-like non empty total Function-yielding V37() ManySortedFunction of A,x

n9 ** i is Relation-like Function-like Function-yielding V37() set

S is set

U1 is Relation-like S -defined Function-like total set

U2 is Relation-like non-empty S -defined Function-like total set

Gen is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of U1,U2

h1 is Relation-like S -defined Function-like total set

h2 is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of h1,U1

Gen ** h2 is Relation-like Function-like Function-yielding V37() set

I is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of h1,U1

Gen ** I is Relation-like Function-like Function-yielding V37() set

A is set

U1 . A is set

U2 . A is set

K20((U1 . A),(U2 . A)) is set

K19(K20((U1 . A),(U2 . A))) is set

Gen . A is Relation-like Function-like set

h1 . A is set

K20((h1 . A),(U1 . A)) is set

K19(K20((h1 . A),(U1 . A))) is set

I . A is Relation-like Function-like set

h2 . A is Relation-like Function-like set

A is Relation-like U1 . A -defined U2 . A -valued Function-like V18(U1 . A,U2 . A) Element of K19(K20((U1 . A),(U2 . A)))

s is Relation-like h1 . A -defined U1 . A -valued Function-like V18(h1 . A,U1 . A) Element of K19(K20((h1 . A),(U1 . A)))

A * s is Relation-like h1 . A -defined U2 . A -valued Function-like Element of K19(K20((h1 . A),(U2 . A)))

K20((h1 . A),(U2 . A)) is set

K19(K20((h1 . A),(U2 . A))) is set

(Gen ** I) . A is Relation-like Function-like set

i is Relation-like h1 . A -defined U1 . A -valued Function-like V18(h1 . A,U1 . A) Element of K19(K20((h1 . A),(U1 . A)))

A * i is Relation-like h1 . A -defined U2 . A -valued Function-like Element of K19(K20((h1 . A),(U2 . A)))

h1 is set

Gen . h1 is Relation-like Function-like set

U1 . h1 is set

U2 . h1 is set

K20((U1 . h1),(U2 . h1)) is set

K19(K20((U1 . h1),(U2 . h1))) is set

h2 is set

K20(h2,(U1 . h1)) is set

K19(K20(h2,(U1 . h1))) is set

I is Relation-like h2 -defined U1 . h1 -valued Function-like V18(h2,U1 . h1) Element of K19(K20(h2,(U1 . h1)))

I * (Gen . h1) is Relation-like Function-like set

A is Relation-like h2 -defined U1 . h1 -valued Function-like V18(h2,U1 . h1) Element of K19(K20(h2,(U1 . h1)))

A * (Gen . h1) is Relation-like Function-like set

I is Relation-like h2 -defined U1 . h1 -valued Function-like V18(h2,U1 . h1) Element of K19(K20(h2,(U1 . h1)))

I * (Gen . h1) is Relation-like Function-like set

A is Relation-like h2 -defined U1 . h1 -valued Function-like V18(h2,U1 . h1) Element of K19(K20(h2,(U1 . h1)))

A * (Gen . h1) is Relation-like Function-like set

A is Relation-like S -defined Function-like total set

id A is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of A,A

i is Relation-like S -defined Function-like total set

s is Relation-like S -defined Function-like total set

ar is Relation-like h2 -defined U1 . h1 -valued Function-like V18(h2,U1 . h1) Element of K19(K20(h2,(U1 . h1)))

ar * (Gen . h1) is Relation-like Function-like set

x is Relation-like h2 -defined U1 . h1 -valued Function-like V18(h2,U1 . h1) Element of K19(K20(h2,(U1 . h1)))

x * (Gen . h1) is Relation-like Function-like set

x is Relation-like S -defined Function-like total set

x is set

dom x is set

x . x is set

dom x is Element of K19(S)

K19(S) is set

(id A) . x is Relation-like Function-like set

IFEQ (x,h1,ar,((id A) . x)) is set

(id A) . x is Relation-like Function-like set

IFEQ (x,h1,ar,((id A) . x)) is set

x is Relation-like h2 -defined U1 . h1 -valued Function-like V18(h2,U1 . h1) Element of K19(K20(h2,(U1 . h1)))

x * (Gen . h1) is Relation-like Function-like set

n is Relation-like h2 -defined U1 . h1 -valued Function-like V18(h2,U1 . h1) Element of K19(K20(h2,(U1 . h1)))

n * (Gen . h1) is Relation-like Function-like set

x is Relation-like S -defined Function-like total Function-yielding V37() set

n9 is set

x . n9 is Relation-like Function-like set

A . n9 is set

U1 . n9 is set

K20((A . n9),(U1 . n9)) is set

K19(K20((A . n9),(U1 . n9))) is set

(id A) . n9 is Relation-like Function-like set

IFEQ (n9,h1,x,((id A) . n9)) is set

IFEQ (n9,h1,h2,(U1 . n9)) is set

IFEQ (n9,h1,h2,(U1 . n9)) is set

(id A) . n9 is Relation-like Function-like set

IFEQ (n9,h1,x,((id A) . n9)) is set

x is Relation-like S -defined Function-like total Function-yielding V37() set

ar is Relation-like S -defined Function-like total Function-yielding V37() set

n is set

(id A) . n is Relation-like Function-like set

IFEQ (n,h1,A,((id A) . n)) is set

x is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of A,U1

x . n is Relation-like Function-like set

IFEQ (n,h1,I,((id A) . n)) is set

x is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of A,U1

x . n is Relation-like Function-like set

Gen ** x is Relation-like Function-like Function-yielding V37() set

(Gen ** x) . n is Relation-like Function-like set

Gen ** x is Relation-like Function-like Function-yielding V37() set

(Gen ** x) . n is Relation-like Function-like set

A . n is set

U1 . n is set

K20((A . n),(U1 . n)) is set

K19(K20((A . n),(U1 . n))) is set

x is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of A,U1

x . n is Relation-like Function-like set

U2 . n is set

K20((U1 . n),(U2 . n)) is set

K19(K20((U1 . n),(U2 . n))) is set

Gen . n is Relation-like Function-like set

x is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of A,U1

x . n is Relation-like Function-like set

(id A) . n is Relation-like Function-like set

IFEQ (n,h1,A,((id A) . n)) is set

IFEQ (n,h1,I,((id A) . n)) is set

n9 is Relation-like A . n -defined U1 . n -valued Function-like V18(A . n,U1 . n) Element of K19(K20((A . n),(U1 . n)))

G is Relation-like A . n -defined U1 . n -valued Function-like V18(A . n,U1 . n) Element of K19(K20((A . n),(U1 . n)))

Gen ** x is Relation-like Function-like Function-yielding V37() set

(Gen ** x) . n is Relation-like Function-like set

r is Relation-like U1 . n -defined U2 . n -valued Function-like V18(U1 . n,U2 . n) Element of K19(K20((U1 . n),(U2 . n)))

r * G is Relation-like A . n -defined U2 . n -valued Function-like Element of K19(K20((A . n),(U2 . n)))

K20((A . n),(U2 . n)) is set

K19(K20((A . n),(U2 . n))) is set

Gen ** x is Relation-like Function-like Function-yielding V37() set

(Gen ** x) . n is Relation-like Function-like set

x is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of A,U1

Gen ** x is Relation-like Function-like Function-yielding V37() set

(Gen ** x) . n is Relation-like Function-like set

x is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of A,U1

Gen ** x is Relation-like Function-like Function-yielding V37() set

(Gen ** x) . n is Relation-like Function-like set

x is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of A,U1

Gen ** x is Relation-like Function-like Function-yielding V37() set

(Gen ** x) . n is Relation-like Function-like set

x is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of A,U1

Gen ** x is Relation-like Function-like Function-yielding V37() set

(Gen ** x) . n is Relation-like Function-like set

n is set

x . n is Relation-like Function-like set

x . n is Relation-like Function-like set

(id A) . n is Relation-like Function-like set

IFEQ (n,h1,A,((id A) . n)) is set

IFEQ (n,h1,I,((id A) . n)) is set

n is set

x . n is Relation-like Function-like set

x . n is Relation-like Function-like set

A is Relation-like S -defined Function-like total set

i is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of A,U1

Gen ** i is Relation-like Function-like Function-yielding V37() set

s is Relation-like S -defined Function-like total Function-yielding V37() ManySortedFunction of A,U1

Gen ** s is Relation-like Function-like Function-yielding V37() set

S is non empty non void V51() ManySortedSign

the carrier of S is non empty set

U1 is non-empty MSAlgebra over S

the Sorts of U1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

U2 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

FreeMSA U2 is strict non-empty MSAlgebra over S

the Sorts of (FreeMSA U2) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

FreeGen U2 is Relation-like the carrier of S -defined Function-like non empty total GeneratorSet of FreeMSA U2

Gen is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of (FreeMSA U2), the Sorts of U1

h1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of (FreeMSA U2), the Sorts of U1

Gen || (FreeGen U2) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of FreeGen U2, the Sorts of U1

h1 || (FreeGen U2) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of FreeGen U2, the Sorts of U1

I is Element of the carrier of S

FreeGen (I,U2) is non empty Element of K19(((FreeSort U2) . I))

FreeSort U2 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

(FreeSort U2) . I is non empty set

K19(((FreeSort U2) . I)) is set

h1 . I is Relation-like the Sorts of (FreeMSA U2) . I -defined the Sorts of U1 . I -valued Function-like V18( the Sorts of (FreeMSA U2) . I, the Sorts of U1 . I) Element of K19(K20(( the Sorts of (FreeMSA U2) . I),( the Sorts of U1 . I)))

the Sorts of (FreeMSA U2) . I is non empty set

the Sorts of U1 . I is non empty set

K20(( the Sorts of (FreeMSA U2) . I),( the Sorts of U1 . I)) is set

K19(K20(( the Sorts of (FreeMSA U2) . I),( the Sorts of U1 . I))) is set

Gen . I is Relation-like the Sorts of (FreeMSA U2) . I -defined the Sorts of U1 . I -valued Function-like V18( the Sorts of (FreeMSA U2) . I, the Sorts of U1 . I) Element of K19(K20(( the Sorts of (FreeMSA U2) . I),( the Sorts of U1 . I)))

A is set

(h1 . I) . A is set

A is set

(Gen . I) . A is set

(FreeGen U2) . I is set

(Gen || (FreeGen U2)) . I is Relation-like (FreeGen U2) . I -defined the Sorts of U1 . I -valued Function-like V18((FreeGen U2) . I, the Sorts of U1 . I) Element of K19(K20(((FreeGen U2) . I),( the Sorts of U1 . I)))

K20(((FreeGen U2) . I),( the Sorts of U1 . I)) is set

K19(K20(((FreeGen U2) . I),( the Sorts of U1 . I))) is set

(Gen . I) | ((FreeGen U2) . I) is Relation-like the Sorts of (FreeMSA U2) . I -defined the Sorts of U1 . I -valued Function-like Element of K19(K20(( the Sorts of (FreeMSA U2) . I),( the Sorts of U1 . I)))

(h1 || (FreeGen U2)) . I is Relation-like (FreeGen U2) . I -defined the Sorts of U1 . I -valued Function-like V18((FreeGen U2) . I, the Sorts of U1 . I) Element of K19(K20(((FreeGen U2) . I),( the Sorts of U1 . I)))

(h1 . I) | ((FreeGen U2) . I) is Relation-like the Sorts of (FreeMSA U2) . I -defined the Sorts of U1 . I -valued Function-like Element of K19(K20(( the Sorts of (FreeMSA U2) . I),( the Sorts of U1 . I)))

((Gen . I) | ((FreeGen U2) . I)) . A is set

A is set

h2 is Element of the carrier of S

FreeGen (h2,U2) is non empty Element of K19(((FreeSort U2) . h2))

FreeSort U2 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

(FreeSort U2) . h2 is non empty set

K19(((FreeSort U2) . h2)) is set

Gen . h2 is Relation-like the Sorts of (FreeMSA U2) . h2 -defined the Sorts of U1 . h2 -valued Function-like V18( the Sorts of (FreeMSA U2) . h2, the Sorts of U1 . h2) Element of K19(K20(( the Sorts of (FreeMSA U2) . h2),( the Sorts of U1 . h2)))

the Sorts of (FreeMSA U2) . h2 is non empty set

the Sorts of U1 . h2 is non empty set

K20(( the Sorts of (FreeMSA U2) . h2),( the Sorts of U1 . h2)) is set

K19(K20(( the Sorts of (FreeMSA U2) . h2),( the Sorts of U1 . h2))) is set

(Gen . h2) . A is set

I is set

S is non empty non void V51() ManySortedSign

the carrier of S is non empty set

U1 is non-empty MSAlgebra over S

the Sorts of U1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

U2 is non-empty MSAlgebra over S

the Sorts of U2 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

Gen is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of U1, the Sorts of U2

h1 is non-empty MSAlgebra over S

the Sorts of h1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

h2 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of U2, the Sorts of h1

h2 ** Gen is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of U1, the Sorts of h1

I is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of U2, the Sorts of h1

I ** Gen is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of U1, the Sorts of h1

S is non empty non void V51() ManySortedSign

the carrier of S is non empty set

U1 is non-empty MSAlgebra over S

the Sorts of U1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

U2 is non-empty MSAlgebra over S

the Sorts of U2 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

Gen is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of U1, the Sorts of U2

I is non-empty MSAlgebra over S

the Sorts of I is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

A is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of I, the Sorts of U1

A is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of I, the Sorts of U1

Gen ** A is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of I, the Sorts of U2

Gen ** A is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of I, the Sorts of U2

A is set

Gen . A is Relation-like Function-like set

the Sorts of U1 . A is set

the Sorts of U2 . A is set

K20(( the Sorts of U1 . A),( the Sorts of U2 . A)) is set

K19(K20(( the Sorts of U1 . A),( the Sorts of U2 . A))) is set

i is set

s is set

(Gen . A) . i is set

(Gen . A) . s is set

FreeMSA the Sorts of U1 is strict non-empty MSAlgebra over S

x is strict non-empty MSAlgebra over S

the Sorts of x is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

FreeGen the Sorts of U1 is Relation-like the carrier of S -defined Function-like non empty total GeneratorSet of FreeMSA the Sorts of U1

ar is Relation-like the carrier of S -defined Function-like non empty total GeneratorSet of x

ar . A is set

x is non empty set

x is non empty set

K20(x,x) is set

K19(K20(x,x)) is set

x --> s is Relation-like x -defined {s} -valued Function-like constant non empty total V18(x,{s}) Element of K19(K20(x,{s}))

{s} is set

K20(x,{s}) is set

K19(K20(x,{s})) is set

x --> i is Relation-like x -defined {i} -valued Function-like constant non empty total V18(x,{i}) Element of K19(K20(x,{i}))

{i} is set

K20(x,{i}) is set

K19(K20(x,{i})) is set

Reverse the Sorts of U1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of FreeGen the Sorts of U1, the Sorts of U1

n9 is Relation-like x -defined x -valued Function-like V18(x,x) Element of K19(K20(x,x))

G is Relation-like the carrier of S -defined Function-like non empty total set

n is Relation-like x -defined x -valued Function-like V18(x,x) Element of K19(K20(x,x))

H is Relation-like the carrier of S -defined Function-like non empty total set

G is Relation-like the carrier of S -defined Function-like non empty total set

H is Relation-like x -defined x -valued Function-like V18(x,x) Element of K19(K20(x,x))

H is set

dom G is set

G . H is set

dom G is Element of K19( the carrier of S)

K19( the carrier of S) is set

(Reverse the Sorts of U1) . H is Relation-like Function-like set

IFEQ (H,A,H,((Reverse the Sorts of U1) . H)) is set

(Reverse the Sorts of U1) . H is Relation-like Function-like set

IFEQ (H,A,H,((Reverse the Sorts of U1) . H)) is set

G is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() set

H is Relation-like x -defined x -valued Function-like V18(x,x) Element of K19(K20(x,x))

h2 is set

G . h2 is Relation-like Function-like set

ar . h2 is set

the Sorts of U1 . h2 is set

K20((ar . h2),( the Sorts of U1 . h2)) is set

K19(K20((ar . h2),( the Sorts of U1 . h2))) is set

(Reverse the Sorts of U1) . h2 is Relation-like Function-like set

IFEQ (h2,A,H,((Reverse the Sorts of U1) . h2)) is set

(Reverse the Sorts of U1) . h2 is Relation-like Function-like set

IFEQ (h2,A,H,((Reverse the Sorts of U1) . h2)) is set

G is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() set

H is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() set

G is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U1

h1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of x, the Sorts of U1

h1 || ar is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U1

H is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U1

h2 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of x, the Sorts of U1

h2 || ar is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U1

Gen ** h1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of x, the Sorts of U2

Gen ** h2 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of x, the Sorts of U2

Fh1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of x, the Sorts of U2

i is set

the Sorts of U1 . i is set

the Sorts of U2 . i is set

K20(( the Sorts of U1 . i),( the Sorts of U2 . i)) is set

K19(K20(( the Sorts of U1 . i),( the Sorts of U2 . i))) is set

K20(x,( the Sorts of U2 . i)) is set

K19(K20(x,( the Sorts of U2 . i))) is set

n9 * (Gen . A) is Relation-like Function-like set

n * (Gen . A) is Relation-like Function-like set

x is set

x is Relation-like x -defined the Sorts of U2 . i -valued Function-like V18(x, the Sorts of U2 . i) Element of K19(K20(x,( the Sorts of U2 . i)))

x . x is set

n9 . x is set

(Gen . A) . (n9 . x) is set

n . x is set

(Gen . A) . (n . x) is set

h29 is Relation-like x -defined the Sorts of U2 . i -valued Function-like V18(x, the Sorts of U2 . i) Element of K19(K20(x,( the Sorts of U2 . i)))

h29 . x is set

(Reverse the Sorts of U1) . i is Relation-like Function-like set

IFEQ (i,A,n9,((Reverse the Sorts of U1) . i)) is set

(h1 || ar) . i is Relation-like Function-like set

Gen ** (h1 || ar) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U2

(Gen ** (h1 || ar)) . i is Relation-like Function-like set

IFEQ (i,A,n,((Reverse the Sorts of U1) . i)) is set

(h2 || ar) . i is Relation-like Function-like set

Gen ** (h2 || ar) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U2

(Gen ** (h2 || ar)) . i is Relation-like Function-like set

the Sorts of U1 . i is set

the Sorts of U2 . i is set

K20(( the Sorts of U1 . i),( the Sorts of U2 . i)) is set

K19(K20(( the Sorts of U1 . i),( the Sorts of U2 . i))) is set

Gen . i is Relation-like Function-like set

ar . i is set

K20((ar . i),( the Sorts of U1 . i)) is set

K19(K20((ar . i),( the Sorts of U1 . i))) is set

(h2 || ar) . i is Relation-like Function-like set

(Reverse the Sorts of U1) . i is Relation-like Function-like set

IFEQ (i,A,n,((Reverse the Sorts of U1) . i)) is set

IFEQ (i,A,n9,((Reverse the Sorts of U1) . i)) is set

(h1 || ar) . i is Relation-like Function-like set

Gen ** (h1 || ar) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U2

(Gen ** (h1 || ar)) . i is Relation-like Function-like set

h29 is Relation-like ar . i -defined the Sorts of U1 . i -valued Function-like V18(ar . i, the Sorts of U1 . i) Element of K19(K20((ar . i),( the Sorts of U1 . i)))

x is Relation-like the Sorts of U1 . i -defined the Sorts of U2 . i -valued Function-like V18( the Sorts of U1 . i, the Sorts of U2 . i) Element of K19(K20(( the Sorts of U1 . i),( the Sorts of U2 . i)))

x * h29 is Relation-like ar . i -defined the Sorts of U2 . i -valued Function-like Element of K19(K20((ar . i),( the Sorts of U2 . i)))

K20((ar . i),( the Sorts of U2 . i)) is set

K19(K20((ar . i),( the Sorts of U2 . i))) is set

Gen ** (h2 || ar) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U2

(Gen ** (h2 || ar)) . i is Relation-like Function-like set

Gen ** (h1 || ar) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U2

(Gen ** (h1 || ar)) . i is Relation-like Function-like set

Gen ** (h2 || ar) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U2

(Gen ** (h2 || ar)) . i is Relation-like Function-like set

Gen ** (h1 || ar) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U2

(Gen ** (h1 || ar)) . i is Relation-like Function-like set

Gen ** (h2 || ar) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U2

(Gen ** (h2 || ar)) . i is Relation-like Function-like set

Fh2 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of x, the Sorts of U2

(Gen ** h1) || ar is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U2

(Gen ** h2) || ar is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of ar, the Sorts of U2

i is set

x is Element of x

n9 . x is Element of x

(Reverse the Sorts of U1) . i is Relation-like Function-like set

IFEQ (i,A,n,((Reverse the Sorts of U1) . i)) is set

H . i is Relation-like Function-like set

IFEQ (i,A,n9,((Reverse the Sorts of U1) . i)) is set

G . i is Relation-like Function-like set

i is set

x is non-empty MSAlgebra over S

the Sorts of x is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

ar is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of x, the Sorts of U1

x is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of x, the Sorts of U1

Gen ** ar is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of x, the Sorts of U2

Gen ** x is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of x, the Sorts of U2

S is non empty non void V51() ManySortedSign

the carrier of S is non empty set

U1 is non-empty MSAlgebra over S

the Sorts of U1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

U2 is Relation-like the carrier of S -defined Function-like non empty total GeneratorSet of U1

S is non empty non void V51() ManySortedSign

the carrier of S is non empty set

U1 is MSAlgebra over S

the Sorts of U1 is Relation-like the carrier of S -defined Function-like non empty total set

U2 is Relation-like the carrier of S -defined Function-like non empty total ManySortedSubset of the Sorts of U1

Gen is Relation-like the carrier of S -defined Function-like non empty total ManySortedSubset of the Sorts of U1

GenMSAlg U2 is strict MSSubAlgebra of U1

GenMSAlg Gen is strict MSSubAlgebra of U1

the Sorts of (GenMSAlg Gen) is Relation-like the carrier of S -defined Function-like non empty total set

S is non empty non void V51() ManySortedSign

the carrier of S is non empty set

U1 is MSAlgebra over S

the Sorts of U1 is Relation-like the carrier of S -defined Function-like non empty total set

U2 is MSSubAlgebra of U1

the Sorts of U2 is Relation-like the carrier of S -defined Function-like non empty total set

Gen is Relation-like the carrier of S -defined Function-like non empty total ManySortedSubset of the Sorts of U1

GenMSAlg Gen is strict MSSubAlgebra of U1

h1 is Relation-like the carrier of S -defined Function-like non empty total ManySortedSubset of the Sorts of U2

GenMSAlg h1 is strict MSSubAlgebra of U2

I is MSSubAlgebra of U1

the Sorts of I is Relation-like the carrier of S -defined Function-like non empty total set

h2 is MSSubAlgebra of U2

the Sorts of h2 is Relation-like the carrier of S -defined Function-like non empty total set

S is non empty non void V51() ManySortedSign

the carrier of S is non empty set

U1 is non-empty MSAlgebra over S

the Sorts of U1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

U2 is non-empty MSAlgebra over S

the Sorts of U2 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

Gen is Relation-like the carrier of S -defined Function-like non empty total GeneratorSet of U1

h1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of U1, the Sorts of U2

h2 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Sorts of U1, the Sorts of U2

h1 || Gen is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of Gen, the Sorts of U2

h2 || Gen is Relation-like the carrier of S -defined Function-like non empty total Function-yielding V37() ManySortedFunction of Gen, the Sorts of U2

A is Relation-like the carrier of S -defined Function-like non empty total set

A is set

A . A is set

the Sorts of U1 . A is set

i is set

A is Relation-like the carrier of S -defined Function-like non empty total ManySortedSubset of the Sorts of U1

the carrier' of S is non empty set

i is Element of the carrier' of S

s is set

Den (i,U1) is Relation-like Args (i,U1) -defined Result (i,U1) -valued Function-like V18( Args (i,U1), Result (i,U1)) Element of K19(K20((Args (i,U1)),(Result (i,U1))))

Args (i,U1) is functional non empty Element of rng ( the Sorts of U1 #)

the Sorts of U1 # is Relation-like the carrier of S * -defined Function-like non empty total set

the carrier of S * is functional non empty V55() M8( the carrier of S)

rng ( the Sorts of U1 #) is set

Result (i,U1) is non empty Element of rng the Sorts of U1

rng the Sorts of U1 is set

K20((Args (i,U1)),(Result (i,U1))) is set

K19(K20((Args (i,U1)),(Result (i,U1)))) is set

the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V18( the carrier' of S, the carrier of S * ) Function-yielding V37() Element of K19(K20( the carrier' of S,( the carrier of S *)))

K20( the carrier' of S,( the carrier of S *)) is set

K19(K20( the carrier' of S,( the carrier of S *))) is set

A # is Relation-like the carrier of S * -defined Function-like non empty total set

the Arity of S * (A #) is Relation-like Function-like set

( the Arity of S * (A #)) . i is set

(Den (i,U1)) | (( the Arity of S * (A #)) . i) is Relation-like Function-like set

rng ((Den (i,U1)) | (( the Arity of S * (A #)) . i)) is set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))

K20( the carrier' of S, the carrier of S) is set

K19(K20( the carrier' of S, the carrier of S)) is set

the ResultSort of S * A is Relation-like Function-like set

( the ResultSort of S * A) . i is set

the_result_sort_of i is Element of the carrier of S

the_arity_of i is Relation-like K127() -defined the carrier of S -valued Function-like V28() V53() V54() Element of the carrier of S *

(Den (i,U1)) | (( the Arity of S * (A #)) . i) is Relation-like Args (i,U1) -defined Result (i,U1) -valued Function-like Element of K19(K20((Args (i,U1)),(Result (i,U1))))

rng ((Den (i,U1)) | (( the Arity of S * (A #)) . i)) is set

dom ((Den (i,U1)) | (( the Arity of S * (A #)) . i)) is functional Element of K19((Args (i,U1)))

K19((Args (i,U1))) is set

x is set

((Den (i,U1)) | (( the Arity of S * (A #)) . i)) . x is set

the Arity of S . i is Relation-like K127() -defined Function-like V28() V53() V54() Element of the carrier of S *

(A #) . ( the Arity of S . i) is set

(A #) . (the_arity_of i) is set

(the_arity_of i) * A is Relation-like Function-like set

product ((the_arity_of i) * A) is set

x is Relation-like Function-like Element of Args (i,U1)

(Den (i,U1)) . x is Element of Result (i,U1)

h1 # x is Relation-like Function-like Element of Args (i,U2)

Args (i,U2) is functional non empty Element of rng ( the Sorts of U2 #)

the Sorts of U2 # is Relation-like the carrier of S * -defined Function-like non empty total set

rng ( the Sorts of U2 #) is set

dom (h1 # x) is set

dom (the_arity_of i) is Element of K19(K127())

h2 # x is Relation-like Function-like Element of Args (i,U2)

n is set

(h1 # x) . n is set

(h2 # x) . n is set

dom x is set

dom ((the_arity_of i) * A) is set

x . n is set

((the_arity_of i) * A) . n is set

(the_arity_of i) . n is set

A . ((the_arity_of i) . n) is set

(the_arity_of i) /. n is Element of the carrier of S

A . ((the_arity_of i) /. n) is set

h2 . ((the_arity_of i) /. n) is Relation-like the Sorts of U1 . ((the_arity_of i) /. n) -defined the Sorts of U2 . ((the_arity_of i) /. n) -valued Function-like V18( the Sorts of U1 . ((the_arity_of i) /. n), the Sorts of U2 . ((the_arity_of i) /. n)) Element of K19(K20(( the Sorts of U1 . ((the_arity_of i) /. n)),( the Sorts of U2 . ((the_arity_of i) /. n))))

the Sorts of U1 . ((the_arity_of i) /. n) is non empty set

the Sorts of U2 . ((the_arity_of i) /. n) is non empty set

K20(( the Sorts of U1 . ((the_arity_of i) /. n)),( the Sorts of U2 . ((the_arity_of i) /. n))) is set

K19(K20(( the Sorts of U1 . ((the_arity_of i) /. n)),( the Sorts of U2 . ((the_arity_of i) /. n)))) is set

n9 is V27() set

x . n9 is set

(h2 . ((the_arity_of i) /. n)) . (x . n9) is set

r is Element of the carrier of S

h1 . r is Relation-like the Sorts of U1 . r -defined the Sorts of U2 . r -valued Function-like V18( the Sorts of U1 . r, the Sorts of U2 . r) Element of K19(K20(( the Sorts of U1 . r),( the Sorts of U2 . r)))

the Sorts of U1 . r is non empty set

the Sorts of U2 . r is non empty set

K20(( the Sorts of U1 . r),( the Sorts of U2 . r)) is set

K19(K20(( the Sorts of U1 . r),( the Sorts of U2 . r))) is set

(h1 . r) . (x . n) is set

h2 . r is Relation-like the Sorts of U1 . r -defined the Sorts of U2 . r -valued Function-like V18( the Sorts of U1 . r, the Sorts of U2 . r) Element of K19(K20(( the Sorts of U1 . r),( the Sorts of U2 . r)))

(h2 . r) . (x . n) is set

the ResultSort of S * the Sorts of U1 is Relation-like Function-like set

( the ResultSort of S * the Sorts of U1) . i is set

the ResultSort of S . i is Element of the carrier of S

the Sorts of U1 . ( the ResultSort of S . i) is non empty set

the Sorts of U1 . (the_result_sort_of i) is non empty set

dom (h2 # x) is set

h1 . (the_result_sort_of i) is Relation-like the Sorts of U1 . (the_result_sort_of i) -defined the Sorts of U2 . (the_result_sort_of i) -valued Function-like V18( the Sorts of U1 . (the_result_sort_of i), the Sorts of U2 . (the_result_sort_of i)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of i)),( the Sorts of U2 . (the_result_sort_of i))))

the Sorts of U2 . (the_result_sort_of i) is non empty set

K20(( the Sorts of U1 . (the_result_sort_of i)),( the Sorts of U2 . (the_result_sort_of i))) is set

K19(K20(( the Sorts of U1 . (the_result_sort_of i)),( the Sorts of U2 . (the_result_sort_of i)))) is set

(h1 . (the_result_sort_of i)) . s is set

(h1 . (the_result_sort_of i)) . ((Den (i,U1)) . x) is set

Result (i,U2) is non empty Element of rng the Sorts of U2

rng the Sorts of U2 is set

Den (i,U2) is Relation-like Args (i,U2) -defined Result (i,U2) -valued Function-like V18( Args (i,U2), Result (i,U2)) Element of K19(K20((Args (i,U2)),(Result (i,U2))))

K20((Args (i,U2)),(Result (i,U2))) is set

K19(K20((Args (i,U2)),(Result (i,U2)))) is set

(Den (i,U2)) . (h1 # x) is Element of Result (i,U2)

(Den (i,U2)) . (h2 # x) is Element of Result (i,U2)

h2 . (the_result_sort_of i) is Relation-like the Sorts of U1 . (the_result_sort_of i) -defined the Sorts of U2 . (the_result_sort_of i) -valued Function-like V18( the Sorts of U1 . (the_result_sort_of i), the Sorts of U2 . (the_result_sort_of i)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of i)),( the Sorts of U2 . (the_result_sort_of i))))

(h2 . (the_result_sort_of i)) . ((Den (i,U1)) . x) is set

(h2 . (the_result_sort_of i)) . s is set

A . (the_result_sort_of i) is set

A . ( the ResultSort of S . i) is set

U1 | A is strict MSSubAlgebra of U1

Opers (U1,A) is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * (A #), the ResultSort of S * A

the carrier' of S is non empty set

the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V18( the carrier' of S, the carrier of S * ) Function-yielding V37() Element of K19(K20( the carrier' of S,( the carrier of S *)))

the carrier of S * is functional non empty V55() M8( the carrier of S)

K20( the carrier' of S,( the carrier of S *)) is set

K19(K20( the carrier' of S,( the carrier of S *))) is set

A # is Relation-like the carrier of S * -defined Function-like non empty total set

the Arity of S * (A #) is Relation-like Function-like set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))

K20( the carrier' of S, the carrier of S) is set

K19(K20( the carrier' of S, the carrier of S)) is set

the ResultSort of S * A is Relation-like Function-like set

MSAlgebra(# A,(Opers (U1,A)) #) is strict MSAlgebra over S

the Sorts of (U1 | A) is Relation-like the carrier of S -defined Function-like non empty total set

i is set

Gen . i is set

the Sorts of (U1 | A) . i is set

the Sorts of U1 . i is set

x is set

s is Element of the carrier of S

h1 . s is Relation-like the Sorts of U1 . s -defined the Sorts of U2 . s -valued Function-like V18( the Sorts of U1 . s, the Sorts of U2 . s) Element of K19(K20(( the Sorts of U1 . s),( the Sorts of U2 . s)))

the Sorts of U1 . s is non empty set

the Sorts of U2 . s is non empty set

K20(( the Sorts of U1 . s),( the Sorts of U2 . s)) is set

K19(K20(( the Sorts of U1 . s),( the Sorts of U2 . s))) is set

(h1 . s) . x is set

Gen . s is set

(h1 . s) | (Gen . s) is Relation-like the Sorts of U1 . s -defined the Sorts of U2 . s -valued Function-like Element of K19(K20(( the Sorts of U1 . s),( the Sorts of U2 . s)))

((h1 . s) | (Gen . s)) . x is set

(h1 || Gen) . s is Relation-like Gen . s -defined the Sorts of U2 . s -valued Function-like V18(Gen . s, the Sorts of U2 . s) Element of K19(K20((Gen . s),( the Sorts of U2 . s)))

K20((Gen . s),( the Sorts of U2 . s)) is set

K19(K20((Gen . s),( the Sorts of U2 . s))) is set

((h1 || Gen) . s) . x is set

h2 . s is Relation-like the Sorts of U1 . s -defined the Sorts of U2 . s -valued Function-like V18( the Sorts of U1 . s, the Sorts of U2 . s) Element of K19(K20(( the Sorts of U1 . s),( the Sorts of U2 . s)))

(h2 . s) | (Gen . s) is Relation-like the Sorts of U1 . s -defined the Sorts of U2 . s -valued Function-like Element of K19(K20(( the Sorts of U1 . s),( the Sorts of U2 . s)))

((h2 . s) | (Gen . s)) . x is set

(h2 . s) . x is set

GenMSAlg Gen is strict MSSubAlgebra of U1

the Sorts of (GenMSAlg Gen) is Relation-like the carrier of S -defined Function-like non empty total set

i is set

s is Element of the carrier of S

the Sorts of U1 . s is non empty set

h1 . s is Relation-like the Sorts of U1 . s -defined the Sorts of U2 . s -valued Function-like V18( the Sorts of U1 . s, the Sorts of U2 . s) Element of K19(K20(( the Sorts of U1 . s),( the Sorts of U2 . s)))

the Sorts of U2 . s is non empty set

K20(( the Sorts of U1 . s),( the Sorts of U2 . s)) is set

K19(K20(( the Sorts of U1 . s),( the Sorts of U2 . s))) is set