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 b1) where b1 is Element of the carrier of (DTConMSA U1) : ( b1 in Terminals (DTConMSA U1) & b1 `2 = I ) } is set
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
dom (h1 . s) is Element of K19(( the Sorts of U1 . s))
K19(( the Sorts of U1 . s)) is set
the Sorts of U1 . i is set
A . i is set
x is set
(h1 . 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) . x is set
ar is Element of the carrier of S
h1 . ar is Relation-like the Sorts of U1 . ar -defined the Sorts of U2 . ar -valued Function-like V18( the Sorts of U1 . ar, the Sorts of U2 . ar) Element of K19(K20(( the Sorts of U1 . ar),( the Sorts of U2 . ar)))
the Sorts of U1 . ar is non empty set
the Sorts of U2 . ar is non empty set
K20(( the Sorts of U1 . ar),( the Sorts of U2 . ar)) is set
K19(K20(( the Sorts of U1 . ar),( the Sorts of U2 . ar))) is set
(h1 . ar) . x is set
h2 . ar is Relation-like the Sorts of U1 . ar -defined the Sorts of U2 . ar -valued Function-like V18( the Sorts of U1 . ar, the Sorts of U2 . ar) Element of K19(K20(( the Sorts of U1 . ar),( the Sorts of U2 . ar)))
(h2 . ar) . x is set
dom (h2 . s) is Element of K19(( the Sorts of U1 . s))
h1 . i is Relation-like Function-like set
h2 . i is Relation-like Function-like set