:: MSUALG_3 semantic presentation

NAT is non empty V21() V22() V23() V28() countable denumerable Element of K19(REAL)

REAL is set

K19(REAL) is set

NAT is non empty V21() V22() V23() V28() countable denumerable set

K19(NAT) is set

K19(NAT) is set

K183() is set

{} is set

the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable V41() V42() V58() V59() V60() set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() V28() Cardinal-yielding countable V41() V42() V58() V59() V60() set

{{}} is set

{{}} * is functional non empty V60() M8({{}})

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

K19(K20(({{}} *),{{}})) is set

PFuncs (({{}} *),{{}}) is set

1 is non empty set

2 is non empty set

3 is non empty set

S is non empty set

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

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

F is Relation-like S -defined Function-like non empty total V41() V42() ManySortedFunction of U1,U2

F1 is Element of S

F . F1 is Relation-like Function-like set

U1 . F1 is set

U2 . F1 is set

K20((U1 . F1),(U2 . F1)) is Relation-like set

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

S is non empty V56() ManySortedSign

S is set

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

U2 is Relation-like Function-like set

proj1 U2 is set

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

proj1 F is set

F1 is set

F . F1 is set

U1 . F1 is set

id (U1 . F1) is Relation-like U1 . F1 -defined U1 . F1 -valued Function-like one-to-one total V18(U1 . F1,U1 . F1) Element of K19(K20((U1 . F1),(U1 . F1)))

K20((U1 . F1),(U1 . F1)) is Relation-like set

K19(K20((U1 . F1),(U1 . F1))) is set

F1 is Relation-like S -defined Function-like total V41() V42() set

F2 is set

F1 . F2 is Relation-like Function-like set

U1 . F2 is set

K20((U1 . F2),(U1 . F2)) is Relation-like set

K19(K20((U1 . F2),(U1 . F2))) is set

id (U1 . F2) is Relation-like U1 . F2 -defined U1 . F2 -valued Function-like one-to-one total V18(U1 . F2,U1 . F2) Element of K19(K20((U1 . F2),(U1 . F2)))

F2 is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U1,U1

c

F2 . c

U1 . c

id (U1 . c

K20((U1 . c

K19(K20((U1 . c

U2 is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U1,U1

F is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U1,U1

F1 is set

U2 . F1 is Relation-like Function-like set

U1 . F1 is set

id (U1 . F1) is Relation-like U1 . F1 -defined U1 . F1 -valued Function-like one-to-one total V18(U1 . F1,U1 . F1) Element of K19(K20((U1 . F1),(U1 . F1)))

K20((U1 . F1),(U1 . F1)) is Relation-like set

K19(K20((U1 . F1),(U1 . F1))) is set

F . F1 is Relation-like Function-like set

proj1 U2 is set

proj1 F is set

S is set

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

(S, the Relation-like S -defined Function-like total set ) is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of the Relation-like S -defined Function-like total set , the Relation-like S -defined Function-like total set

U2 is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of the Relation-like S -defined Function-like total set , the Relation-like S -defined Function-like total set

F is set

proj1 U2 is set

U2 . F is Relation-like Function-like set

F1 is Relation-like Function-like set

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

the Relation-like S -defined Function-like total set . F is set

id ( the Relation-like S -defined Function-like total set . F) is Relation-like the Relation-like S -defined Function-like total set . F -defined the Relation-like S -defined Function-like total set . F -valued Function-like one-to-one total V18( the Relation-like S -defined Function-like total set . F, the Relation-like S -defined Function-like total set . F) Element of K19(K20(( the Relation-like S -defined Function-like total set . F),( the Relation-like S -defined Function-like total set . F)))

K20(( the Relation-like S -defined Function-like total set . F),( the Relation-like S -defined Function-like total set . F)) is Relation-like set

K19(K20(( the Relation-like S -defined Function-like total set . F),( the Relation-like S -defined Function-like total set . F))) is set

S is set

U1 is Relation-like S -defined Function-like total V41() V42() set

proj1 U1 is set

U2 is set

U1 . U2 is Relation-like Function-like set

U2 is set

F is Relation-like Function-like set

U1 . U2 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

S is set

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

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

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

F1 is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U1,U2

F2 is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U2,F

F2 ** F1 is Relation-like Function-like V41() V42() set

proj1 (F2 ** F1) is set

proj1 F1 is set

proj1 F2 is set

(proj1 F1) /\ (proj1 F2) is set

c

(F2 ** F1) . c

F1 . c

F2 . c

(F1 . c

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

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

F1 is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U1,U2

F2 is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U2,F

F2 ** F1 is Relation-like Function-like V41() V42() set

proj1 (F2 ** F1) is set

c

f is Relation-like S -defined Function-like total V41() V42() set

h is set

f . h is Relation-like Function-like set

U1 . h is set

F . h is set

K20((U1 . h),(F . h)) is Relation-like set

K19(K20((U1 . h),(F . h))) is set

U2 . h is set

K20((U1 . h),(U2 . h)) is Relation-like set

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

F1 . h is Relation-like Function-like set

K20((U2 . h),(F . h)) is Relation-like set

K19(K20((U2 . h),(F . h))) is set

F2 . h is Relation-like Function-like set

(F2 ** F1) . h is Relation-like Function-like set

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

a is Relation-like U2 . h -defined F . h -valued Function-like V18(U2 . h,F . h) Element of K19(K20((U2 . h),(F . h)))

a * G1 is Relation-like U1 . h -defined F . h -valued Function-like Element of K19(K20((U1 . h),(F . h)))

S is set

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

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

(S,U1) is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U1,U1

F is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U1,U2

F ** (S,U1) is Relation-like Function-like V41() V42() set

proj1 (F ** (S,U1)) is set

proj1 F is set

proj1 (S,U1) is set

(proj1 F) /\ (proj1 (S,U1)) is set

S /\ (proj1 (S,U1)) is set

S /\ S is set

F2 is set

U1 . F2 is set

U2 . F2 is set

K20((U1 . F2),(U2 . F2)) is Relation-like set

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

F . F2 is Relation-like Function-like set

K20((U1 . F2),(U1 . F2)) is Relation-like set

K19(K20((U1 . F2),(U1 . F2))) is set

(S,U1) . F2 is Relation-like Function-like set

F1 is Relation-like S -defined Function-like total V41() V42() set

F1 . F2 is Relation-like Function-like set

f is Relation-like U1 . F2 -defined U1 . F2 -valued Function-like total V18(U1 . F2,U1 . F2) Element of K19(K20((U1 . F2),(U1 . F2)))

c

c

id (U1 . F2) is Relation-like U1 . F2 -defined U1 . F2 -valued Function-like one-to-one total V18(U1 . F2,U1 . F2) Element of K19(K20((U1 . F2),(U1 . F2)))

c

proj1 c

S is set

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

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

(S,U2) is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U2,U2

F is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U1,U2

(S,U2) ** F is Relation-like Function-like V41() V42() set

proj1 ((S,U2) ** F) is set

proj1 (S,U2) is set

proj1 F is set

(proj1 (S,U2)) /\ (proj1 F) is set

S /\ (proj1 F) is set

S /\ S is set

F2 is set

U1 . F2 is set

U2 . F2 is set

K20((U1 . F2),(U2 . F2)) is Relation-like set

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

F . F2 is Relation-like Function-like set

K20((U2 . F2),(U2 . F2)) is Relation-like set

K19(K20((U2 . F2),(U2 . F2))) is set

(S,U2) . F2 is Relation-like Function-like set

f is Relation-like U2 . F2 -defined U2 . F2 -valued Function-like total V18(U2 . F2,U2 . F2) Element of K19(K20((U2 . F2),(U2 . F2)))

id (U2 . F2) is Relation-like U2 . F2 -defined U2 . F2 -valued Function-like one-to-one total V18(U2 . F2,U2 . F2) Element of K19(K20((U2 . F2),(U2 . F2)))

F1 is Relation-like S -defined Function-like total V41() V42() set

F1 . F2 is Relation-like Function-like set

c

f * c

S is set

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

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

F is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U1,U2

F1 is set

F . F1 is Relation-like Function-like set

(F . F1) " is Relation-like Function-like set

F1 is Relation-like Function-like set

proj1 F1 is set

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

proj1 F2 is set

c

F2 . c

U1 . c

U2 . c

K20((U1 . c

K19(K20((U1 . c

F . c

f is Relation-like U1 . c

f " is Relation-like Function-like set

c

f is set

c

U2 . f is set

U1 . f is set

K20((U2 . f),(U1 . f)) is Relation-like set

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

K20((U1 . f),(U2 . f)) is Relation-like set

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

F . f is Relation-like Function-like set

proj1 F is set

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

proj2 h is set

h " is Relation-like Function-like set

f is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U2,U1

h is set

f . h is Relation-like Function-like set

F . h is Relation-like Function-like set

(F . h) " is Relation-like Function-like set

F1 is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U2,U1

F2 is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U2,U1

c

U1 . c

U2 . c

K20((U1 . c

K19(K20((U1 . c

F . c

F1 . c

f is Relation-like U1 . c

f " is Relation-like Function-like set

F2 . c

S is set

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

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

(S,U2) is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U2,U2

(S,U1) is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U1,U1

F is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U1,U2

(S,U1,U2,F) is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U2,U1

F1 is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U2,U1

(S,U2,U1,U2,F1,F) is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U2,U2

(S,U1,U2,U1,F,F1) is Relation-like S -defined Function-like total V41() V42() ManySortedFunction of U1,U1

F2 is set

U1 . F2 is set

U2 . F2 is set

K20((U1 . F2),(U2 . F2)) is Relation-like set

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

F . F2 is Relation-like Function-like set

K20((U2 . F2),(U1 . F2)) is Relation-like set

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

F1 . F2 is Relation-like Function-like set

proj1 F is set

c

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

c

c

K20((U2 . F2),(U2 . F2)) is Relation-like set

K19(K20((U2 . F2),(U2 . F2))) is set

proj2 c

id (proj2 c

K20((proj2 c

K19(K20((proj2 c

id (U2 . F2) is Relation-like U2 . F2 -defined U2 . F2 -valued Function-like one-to-one total V18(U2 . F2,U2 . F2) Element of K19(K20((U2 . F2),(U2 . F2)))

(S,U2,U1,U2,F1,F) . F2 is Relation-like Function-like set

F2 is set

(S,U1,U2,U1,F,F1) . F2 is Relation-like Function-like set

U1 . F2 is set

id (U1 . F2) is Relation-like U1 . F2 -defined U1 . F2 -valued Function-like one-to-one total V18(U1 . F2,U1 . F2) Element of K19(K20((U1 . F2),(U1 . F2)))

K20((U1 . F2),(U1 . F2)) is Relation-like set

K19(K20((U1 . F2),(U1 . F2))) is set

U2 . F2 is set

K20((U1 . F2),(U2 . F2)) is Relation-like set

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

F . F2 is Relation-like Function-like set

K20((U2 . F2),(U1 . F2)) is Relation-like set

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

F1 . F2 is Relation-like Function-like set

c

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

c

proj1 c

f * c

S is non empty non void V56() ManySortedSign

the carrier' of S is non empty set

U2 is Element of the carrier' of S

U1 is non-empty MSAlgebra over S

Args (U2,U1) is non empty Element of proj2 ( the Sorts of U1 #)

the carrier of S is non empty set

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

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 V60() M8( the carrier of S)

proj2 ( the Sorts of U1 #) is non empty set

the_arity_of U2 is Relation-like NAT -defined the carrier of S -valued Function-like V28() countable V58() V59() Element of the carrier of S *

(the_arity_of U2) * the Sorts of U1 is Relation-like non-empty NAT -defined Function-like set

product ((the_arity_of U2) * the Sorts of U1) is functional non empty with_common_domain product-like set

S is non empty non void V56() ManySortedSign

the carrier' of S is non empty set

U1 is Element of the carrier' of S

the_arity_of U1 is Relation-like NAT -defined the carrier of S -valued Function-like V28() countable V58() V59() Element of the carrier of S *

the carrier of S is non empty set

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

dom (the_arity_of U1) is countable Element of K19(NAT)

U2 is MSAlgebra over S

Args (U1,U2) is Element of proj2 ( the Sorts of U2 #)

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

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

proj2 ( the Sorts of U2 #) is non empty set

(the_arity_of U1) * the Sorts of U2 is Relation-like NAT -defined Function-like set

proj1 ((the_arity_of U1) * the Sorts of U2) is set

F is Relation-like Function-like set

proj1 F is set

product ((the_arity_of U1) * the Sorts of U2) is functional with_common_domain product-like set

proj1 the Sorts of U2 is non empty set

proj2 (the_arity_of U1) is set

F1 is set

F . F1 is set

((the_arity_of U1) * the Sorts of U2) . F1 is set

S is non empty non void V56() ManySortedSign

the carrier' of S is non empty set

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 MSAlgebra over S

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

F is Element of the carrier' of S

Args (F,U1) is Element of proj2 ( 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 V60() M8( the carrier of S)

proj2 ( the Sorts of U1 #) is non empty set

Args (F,U2) is Element of proj2 ( the Sorts of U2 #)

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

proj2 ( the Sorts of U2 #) is non empty set

the_arity_of F is Relation-like NAT -defined the carrier of S -valued Function-like V28() countable V58() V59() Element of the carrier of S *

F1 is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U1, the Sorts of U2

(the_arity_of F) * F1 is Relation-like NAT -defined Function-like V41() V42() set

Frege ((the_arity_of F) * F1) is Relation-like product (doms ((the_arity_of F) * F1)) -defined Function-like total V41() V42() set

doms ((the_arity_of F) * F1) is Relation-like Function-like set

product (doms ((the_arity_of F) * F1)) is functional with_common_domain product-like set

F2 is Element of Args (F,U1)

(Frege ((the_arity_of F) * F1)) . F2 is Relation-like Function-like set

(the_arity_of F) * the Sorts of U1 is Relation-like NAT -defined Function-like set

proj1 ((the_arity_of F) * the Sorts of U1) is set

proj2 ((the_arity_of F) * F1) is set

SubFuncs (proj2 ((the_arity_of F) * F1)) is set

((the_arity_of F) * F1) " (SubFuncs (proj2 ((the_arity_of F) * F1))) is set

c

((the_arity_of F) * F1) . c

(the_arity_of F) . c

proj1 the Sorts of U1 is non empty set

proj1 F1 is non empty set

dom (the_arity_of F) is countable Element of K19(NAT)

proj1 ((the_arity_of F) * F1) is set

c

f is V21() V22() V23() V27() Element of NAT

(the_arity_of F) . f is set

(the_arity_of F) . c

(the_arity_of F) * the Sorts of U2 is Relation-like NAT -defined Function-like set

product ((the_arity_of F) * the Sorts of U2) is functional with_common_domain product-like set

c

proj1 ((the_arity_of F) * F1) is set

dom (the_arity_of F) is countable Element of K19(NAT)

f is V21() V22() V23() V27() Element of NAT

(the_arity_of F) . f is set

(the_arity_of F) . c

proj1 the Sorts of U2 is non empty set

proj1 ((the_arity_of F) * the Sorts of U2) is set

((the_arity_of F) * the Sorts of U2) . c

the Sorts of U2 . ((the_arity_of F) . c

proj2 ((the_arity_of F) * the Sorts of U2) is set

the Sorts of U1 . ((the_arity_of F) . c

K20(( the Sorts of U1 . ((the_arity_of F) . c

K19(K20(( the Sorts of U1 . ((the_arity_of F) . c

F1 . ((the_arity_of F) . c

((the_arity_of F) * the Sorts of U1) . c

h is Relation-like the Sorts of U1 . ((the_arity_of F) . c

proj1 h is set

((the_arity_of F) * F1) . c

proj1 (((the_arity_of F) * F1) . c

product ((the_arity_of F) * the Sorts of U1) is functional with_common_domain product-like set

proj1 (doms ((the_arity_of F) * F1)) is set

c

proj1 c

((the_arity_of F) * F1) .. c

proj1 (((the_arity_of F) * F1) .. c

proj2 (the_arity_of F) is set

proj1 F1 is non empty set

f is set

(the_arity_of F) . f is set

the Sorts of U1 . ((the_arity_of F) . f) is set

the Sorts of U2 . ((the_arity_of F) . f) is set

K20(( the Sorts of U1 . ((the_arity_of F) . f)),( the Sorts of U2 . ((the_arity_of F) . f))) is Relation-like set

K19(K20(( the Sorts of U1 . ((the_arity_of F) . f)),( the Sorts of U2 . ((the_arity_of F) . f)))) is set

F1 . ((the_arity_of F) . f) is Relation-like Function-like set

h is Relation-like the Sorts of U1 . ((the_arity_of F) . f) -defined the Sorts of U2 . ((the_arity_of F) . f) -valued Function-like V18( the Sorts of U1 . ((the_arity_of F) . f), the Sorts of U2 . ((the_arity_of F) . f)) Element of K19(K20(( the Sorts of U1 . ((the_arity_of F) . f)),( the Sorts of U2 . ((the_arity_of F) . f))))

((the_arity_of F) * F1) . f is Relation-like Function-like set

(((the_arity_of F) * F1) .. c

c

h . (c

((the_arity_of F) * the Sorts of U2) . f is set

G1 is V21() V22() V23() V27() Element of NAT

(the_arity_of F) . G1 is set

proj1 the Sorts of U1 is non empty set

(doms ((the_arity_of F) * F1)) . f is set

S is non empty non void V56() ManySortedSign

the carrier' of S is non empty set

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 MSAlgebra over S

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

F is Element of the carrier' of S

Args (F,U1) is Element of proj2 ( 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 V60() M8( the carrier of S)

proj2 ( the Sorts of U1 #) is non empty set

F2 is Element of Args (F,U1)

c

f is Relation-like Function-like set

Args (F,U2) is Element of proj2 ( the Sorts of U2 #)

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

proj2 ( the Sorts of U2 #) is non empty set

the_arity_of F is Relation-like NAT -defined the carrier of S -valued Function-like V28() countable V58() V59() Element of the carrier of S *

proj2 (the_arity_of F) is set

proj1 the Sorts of U1 is non empty set

F1 is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U1, the Sorts of U2

(S,U1,U2,F,F1,F2) is Element of Args (F,U2)

(the_arity_of F) * F1 is Relation-like NAT -defined Function-like V41() V42() set

Frege ((the_arity_of F) * F1) is Relation-like product (doms ((the_arity_of F) * F1)) -defined Function-like total V41() V42() set

doms ((the_arity_of F) * F1) is Relation-like Function-like set

product (doms ((the_arity_of F) * F1)) is functional with_common_domain product-like set

(Frege ((the_arity_of F) * F1)) . F2 is Relation-like Function-like set

(the_arity_of F) * the Sorts of U1 is Relation-like NAT -defined Function-like set

proj1 ((the_arity_of F) * the Sorts of U1) is set

proj2 ((the_arity_of F) * F1) is set

SubFuncs (proj2 ((the_arity_of F) * F1)) is set

((the_arity_of F) * F1) " (SubFuncs (proj2 ((the_arity_of F) * F1))) is set

h is set

((the_arity_of F) * F1) . h is Relation-like Function-like set

(the_arity_of F) . h is set

proj1 F1 is non empty set

dom (the_arity_of F) is countable Element of K19(NAT)

proj1 ((the_arity_of F) * F1) is set

h is set

G1 is V21() V22() V23() V27() Element of NAT

(the_arity_of F) . G1 is set

(the_arity_of F) . h is set

(the_arity_of F) * the Sorts of U2 is Relation-like NAT -defined Function-like set

product ((the_arity_of F) * the Sorts of U2) is functional with_common_domain product-like set

proj1 f is set

proj1 ((the_arity_of F) * the Sorts of U2) is set

product ((the_arity_of F) * the Sorts of U1) is functional with_common_domain product-like set

proj1 c

dom (the_arity_of F) is countable Element of K19(NAT)

proj1 the Sorts of U2 is non empty set

h is set

proj1 ((the_arity_of F) * F1) is set

(the_arity_of F) . h is set

the Sorts of U1 . ((the_arity_of F) . h) is set

the Sorts of U2 . ((the_arity_of F) . h) is set

K20(( the Sorts of U1 . ((the_arity_of F) . h)),( the Sorts of U2 . ((the_arity_of F) . h))) is Relation-like set

K19(K20(( the Sorts of U1 . ((the_arity_of F) . h)),( the Sorts of U2 . ((the_arity_of F) . h)))) is set

F1 . ((the_arity_of F) . h) is Relation-like Function-like set

((the_arity_of F) * the Sorts of U2) . h is set

proj2 ((the_arity_of F) * the Sorts of U2) is set

((the_arity_of F) * the Sorts of U1) . h is set

G1 is Relation-like the Sorts of U1 . ((the_arity_of F) . h) -defined the Sorts of U2 . ((the_arity_of F) . h) -valued Function-like V18( the Sorts of U1 . ((the_arity_of F) . h), the Sorts of U2 . ((the_arity_of F) . h)) Element of K19(K20(( the Sorts of U1 . ((the_arity_of F) . h)),( the Sorts of U2 . ((the_arity_of F) . h))))

proj1 G1 is set

((the_arity_of F) * F1) . h is Relation-like Function-like set

proj1 (((the_arity_of F) * F1) . h) is set

h is V21() V22() V23() V27() set

(the_arity_of F) . h is set

proj1 F1 is non empty set

((the_arity_of F) * F1) . h is Relation-like Function-like set

F1 . ((the_arity_of F) . h) is Relation-like Function-like set

(the_arity_of F) /. h is Element of the carrier of S

( the carrier of S, the Sorts of U1, the Sorts of U2,F1,((the_arity_of F) /. h)) is Relation-like the Sorts of U1 . ((the_arity_of F) /. h) -defined the Sorts of U2 . ((the_arity_of F) /. h) -valued Function-like V18( the Sorts of U1 . ((the_arity_of F) /. h), the Sorts of U2 . ((the_arity_of F) /. h)) Element of K19(K20(( the Sorts of U1 . ((the_arity_of F) /. h)),( the Sorts of U2 . ((the_arity_of F) /. h))))

the Sorts of U1 . ((the_arity_of F) /. h) is set

the Sorts of U2 . ((the_arity_of F) /. h) is set

K20(( the Sorts of U1 . ((the_arity_of F) /. h)),( the Sorts of U2 . ((the_arity_of F) /. h))) is Relation-like set

K19(K20(( the Sorts of U1 . ((the_arity_of F) /. h)),( the Sorts of U2 . ((the_arity_of F) /. h)))) is set

f . h is set

((the_arity_of F) * F1) .. c

(((the_arity_of F) * F1) .. c

c

( the carrier of S, the Sorts of U1, the Sorts of U2,F1,((the_arity_of F) /. h)) . (c

G1 is set

a is V21() V22() V23() V27() set

(the_arity_of F) . a is set

((the_arity_of F) * F1) . a is Relation-like Function-like set

F1 . ((the_arity_of F) . a) is Relation-like Function-like set

(the_arity_of F) /. a is Element of the carrier of S

( the carrier of S, the Sorts of U1, the Sorts of U2,F1,((the_arity_of F) /. a)) is Relation-like the Sorts of U1 . ((the_arity_of F) /. a) -defined the Sorts of U2 . ((the_arity_of F) /. a) -valued Function-like V18( the Sorts of U1 . ((the_arity_of F) /. a), the Sorts of U2 . ((the_arity_of F) /. a)) Element of K19(K20(( the Sorts of U1 . ((the_arity_of F) /. a)),( the Sorts of U2 . ((the_arity_of F) /. a))))

the Sorts of U1 . ((the_arity_of F) /. a) is set

the Sorts of U2 . ((the_arity_of F) /. a) is set

K20(( the Sorts of U1 . ((the_arity_of F) /. a)),( the Sorts of U2 . ((the_arity_of F) /. a))) is Relation-like set

K19(K20(( the Sorts of U1 . ((the_arity_of F) /. a)),( the Sorts of U2 . ((the_arity_of F) /. a)))) is set

f . G1 is set

c

( the carrier of S, the Sorts of U1, the Sorts of U2,F1,((the_arity_of F) /. a)) . (c

(((the_arity_of F) * F1) .. c

h is Relation-like Function-like set

h . G1 is set

proj1 h is set

S is non empty non void V56() ManySortedSign

the carrier' of S is non empty set

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

F is Element of the carrier' of S

Args (F,U1) is functional non empty Element of proj2 ( 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 V60() M8( the carrier of S)

proj2 ( the Sorts of U1 #) is non empty set

Args (F,U2) is functional non empty Element of proj2 ( the Sorts of U2 #)

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

proj2 ( the Sorts of U2 #) is non empty set

F1 is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U1, the Sorts of U2

F2 is Relation-like Function-like Element of Args (F,U1)

(S,U1,U2,F,F1,F2) is Relation-like Function-like Element of Args (F,U2)

proj1 F2 is set

the_arity_of F is Relation-like NAT -defined the carrier of S -valued Function-like V28() countable V58() V59() Element of the carrier of S *

c

f is V21() V22() V23() V27() set

c

(the_arity_of F) /. f is Element of the carrier of S

( the carrier of S, the Sorts of U1, the Sorts of U2,F1,((the_arity_of F) /. f)) is Relation-like the Sorts of U1 . ((the_arity_of F) /. f) -defined the Sorts of U2 . ((the_arity_of F) /. f) -valued Function-like non empty total V18( the Sorts of U1 . ((the_arity_of F) /. f), the Sorts of U2 . ((the_arity_of F) /. f)) Element of K19(K20(( the Sorts of U1 . ((the_arity_of F) /. f)),( the Sorts of U2 . ((the_arity_of F) /. f))))

the Sorts of U1 . ((the_arity_of F) /. f) is non empty set

the Sorts of U2 . ((the_arity_of F) /. f) is non empty set

K20(( the Sorts of U1 . ((the_arity_of F) /. f)),( the Sorts of U2 . ((the_arity_of F) /. f))) is Relation-like set

K19(K20(( the Sorts of U1 . ((the_arity_of F) /. f)),( the Sorts of U2 . ((the_arity_of F) /. f)))) is set

F2 . f is set

( the carrier of S, the Sorts of U1, the Sorts of U2,F1,((the_arity_of F) /. f)) . (F2 . f) is set

h is Relation-like Function-like Element of Args (F,U2)

S is non empty non void V56() ManySortedSign

the carrier' of S is non empty set

the carrier of S is non empty set

U1 is Element of the carrier' of S

U2 is MSAlgebra over S

Args (U1,U2) is Element of proj2 ( the Sorts of U2 #)

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

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

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

proj2 ( the Sorts of U2 #) is non empty set

( the carrier of S, the Sorts of U2) is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U2, the Sorts of U2

F2 is Element of Args (U1,U2)

(S,U2,U2,U1,( the carrier of S, the Sorts of U2),F2) is Element of Args (U1,U2)

F1 is non empty set

the_arity_of U1 is Relation-like NAT -defined the carrier of S -valued Function-like V28() countable V58() V59() Element of the carrier of S *

(the_arity_of U1) * the Sorts of U2 is Relation-like NAT -defined Function-like set

product ((the_arity_of U1) * the Sorts of U2) is functional with_common_domain product-like set

c

proj1 ((the_arity_of U1) * the Sorts of U2) is set

f is Relation-like Function-like set

proj1 f is set

h is Relation-like Function-like set

proj1 h is set

dom (the_arity_of U1) is countable Element of K19(NAT)

G1 is set

h . G1 is set

f . G1 is set

a is V21() V22() V23() V27() set

(the_arity_of U1) /. a is Element of the carrier of S

proj1 the Sorts of U2 is non empty set

proj2 (the_arity_of U1) is set

h . a is set

((the_arity_of U1) * the Sorts of U2) . a is set

(the_arity_of U1) . a is set

the Sorts of U2 . ((the_arity_of U1) . a) is set

the Sorts of U2 . ((the_arity_of U1) /. a) is set

( the carrier of S, the Sorts of U2, the Sorts of U2,( the carrier of S, the Sorts of U2),((the_arity_of U1) /. a)) is Relation-like the Sorts of U2 . ((the_arity_of U1) /. a) -defined the Sorts of U2 . ((the_arity_of U1) /. a) -valued Function-like total V18( the Sorts of U2 . ((the_arity_of U1) /. a), the Sorts of U2 . ((the_arity_of U1) /. a)) Element of K19(K20(( the Sorts of U2 . ((the_arity_of U1) /. a)),( the Sorts of U2 . ((the_arity_of U1) /. a))))

K20(( the Sorts of U2 . ((the_arity_of U1) /. a)),( the Sorts of U2 . ((the_arity_of U1) /. a))) is Relation-like set

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

id ( the Sorts of U2 . ((the_arity_of U1) /. a)) is Relation-like the Sorts of U2 . ((the_arity_of U1) /. a) -defined the Sorts of U2 . ((the_arity_of U1) /. a) -valued Function-like one-to-one total V18( the Sorts of U2 . ((the_arity_of U1) /. a), the Sorts of U2 . ((the_arity_of U1) /. a)) Element of K19(K20(( the Sorts of U2 . ((the_arity_of U1) /. a)),( the Sorts of U2 . ((the_arity_of U1) /. a))))

f . a is set

( the carrier of S, the Sorts of U2, the Sorts of U2,( the carrier of S, the Sorts of U2),((the_arity_of U1) /. a)) . (h . a) is set

S is non empty non void V56() ManySortedSign

the carrier' of S is non empty set

the carrier of S is non empty set

U1 is Element of the carrier' of S

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

F is non-empty MSAlgebra over S

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

F1 is non-empty MSAlgebra over S

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

Args (U1,U2) is functional non empty Element of proj2 ( the Sorts of U2 #)

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

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

proj2 ( the Sorts of U2 #) is non empty set

F2 is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U2, the Sorts of F

c

( the carrier of S, the Sorts of U2, the Sorts of F, the Sorts of F1,F2,c

f is Relation-like Function-like Element of Args (U1,U2)

(S,U2,F1,U1,( the carrier of S, the Sorts of U2, the Sorts of F, the Sorts of F1,F2,c

Args (U1,F1) is functional non empty Element of proj2 ( the Sorts of F1 #)

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

proj2 ( the Sorts of F1 #) is non empty set

(S,U2,F,U1,F2,f) is Relation-like Function-like Element of Args (U1,F)

Args (U1,F) is functional non empty Element of proj2 ( the Sorts of F #)

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

proj2 ( the Sorts of F #) is non empty set

(S,F,F1,U1,c

proj1 f is set

the_arity_of U1 is Relation-like NAT -defined the carrier of S -valued Function-like V28() countable V58() V59() Element of the carrier of S *

dom (the_arity_of U1) is countable Element of K19(NAT)

proj1 (S,U2,F,U1,F2,f) is set

proj2 (the_arity_of U1) is set

proj1 the Sorts of U2 is non empty set

(the_arity_of U1) * the Sorts of U2 is Relation-like non-empty NAT -defined Function-like set

proj1 ((the_arity_of U1) * the Sorts of U2) is set

h is set

(S,U2,F1,U1,( the carrier of S, the Sorts of U2, the Sorts of F, the Sorts of F1,F2,c

(S,F,F1,U1,c

G1 is V21() V22() V23() V27() set

(the_arity_of U1) /. G1 is Element of the carrier of S

(S,U2,F1,U1,( the carrier of S, the Sorts of U2, the Sorts of F, the Sorts of F1,F2,c

( the carrier of S, the Sorts of U2, the Sorts of F1,( the carrier of S, the Sorts of U2, the Sorts of F, the Sorts of F1,F2,c

the Sorts of U2 . ((the_arity_of U1) /. G1) is non empty set

the Sorts of F1 . ((the_arity_of U1) /. G1) is non empty set

K20(( the Sorts of U2 . ((the_arity_of U1) /. G1)),( the Sorts of F1 . ((the_arity_of U1) /. G1))) is Relation-like set

K19(K20(( the Sorts of U2 . ((the_arity_of U1) /. G1)),( the Sorts of F1 . ((the_arity_of U1) /. G1)))) is set

f . G1 is set

( the carrier of S, the Sorts of U2, the Sorts of F1,( the carrier of S, the Sorts of U2, the Sorts of F, the Sorts of F1,F2,c

(the_arity_of U1) . G1 is set

((the_arity_of U1) * the Sorts of U2) . G1 is set

the Sorts of F . ((the_arity_of U1) /. G1) is non empty set

( the carrier of S, the Sorts of U2, the Sorts of F,F2,((the_arity_of U1) /. G1)) is Relation-like the Sorts of U2 . ((the_arity_of U1) /. G1) -defined the Sorts of F . ((the_arity_of U1) /. G1) -valued Function-like non empty total V18( the Sorts of U2 . ((the_arity_of U1) /. G1), the Sorts of F . ((the_arity_of U1) /. G1)) Element of K19(K20(( the Sorts of U2 . ((the_arity_of U1) /. G1)),( the Sorts of F . ((the_arity_of U1) /. G1))))

K20(( the Sorts of U2 . ((the_arity_of U1) /. G1)),( the Sorts of F . ((the_arity_of U1) /. G1))) is Relation-like set

K19(K20(( the Sorts of U2 . ((the_arity_of U1) /. G1)),( the Sorts of F . ((the_arity_of U1) /. G1)))) is set

( the carrier of S, the Sorts of F, the Sorts of F1,c

K20(( the Sorts of F . ((the_arity_of U1) /. G1)),( the Sorts of F1 . ((the_arity_of U1) /. G1))) is Relation-like set

K19(K20(( the Sorts of F . ((the_arity_of U1) /. G1)),( the Sorts of F1 . ((the_arity_of U1) /. G1)))) is set

( the carrier of S, the Sorts of F, the Sorts of F1,c

proj1 ( the carrier of S, the Sorts of U2, the Sorts of F,F2,((the_arity_of U1) /. G1)) is non empty set

proj1 (( the carrier of S, the Sorts of F, the Sorts of F1,c

( the carrier of S, the Sorts of U2, the Sorts of F,F2,((the_arity_of U1) /. G1)) . (f . G1) is set

( the carrier of S, the Sorts of F, the Sorts of F1,c

(S,U2,F,U1,F2,f) . G1 is set

( the carrier of S, the Sorts of F, the Sorts of F1,c

proj1 (S,U2,F1,U1,( the carrier of S, the Sorts of U2, the Sorts of F, the Sorts of F1,F2,c

proj1 (S,F,F1,U1,c

S is non empty non void V56() 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 MSAlgebra over S

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

S is non empty non void V56() 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

( the carrier of S, the Sorts of U1) is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U1, the Sorts of U1

the carrier' of S is non empty set

F is Element of the carrier' of S

Args (F,U1) is Element of proj2 ( 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 V60() M8( the carrier of S)

proj2 ( the Sorts of U1 #) is non empty set

the_result_sort_of F is Element of the carrier of S

( the carrier of S, the Sorts of U1, the Sorts of U1,( the carrier of S, the Sorts of U1),(the_result_sort_of F)) is Relation-like the Sorts of U1 . (the_result_sort_of F) -defined the Sorts of U1 . (the_result_sort_of F) -valued Function-like total V18( the Sorts of U1 . (the_result_sort_of F), the Sorts of U1 . (the_result_sort_of F)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of F)),( the Sorts of U1 . (the_result_sort_of F))))

the Sorts of U1 . (the_result_sort_of F) is set

K20(( the Sorts of U1 . (the_result_sort_of F)),( the Sorts of U1 . (the_result_sort_of F))) is Relation-like set

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

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

Result (F,U1) is Element of proj2 the Sorts of U1

proj2 the Sorts of U1 is non empty set

K20((Args (F,U1)),(Result (F,U1))) is Relation-like set

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

F1 is Element of Args (F,U1)

(Den (F,U1)) . F1 is set

( the carrier of S, the Sorts of U1, the Sorts of U1,( the carrier of S, the Sorts of U1),(the_result_sort_of F)) . ((Den (F,U1)) . F1) is set

(S,U1,U1,F,( the carrier of S, the Sorts of U1),F1) is Element of Args (F,U1)

(Den (F,U1)) . (S,U1,U1,F,( the carrier of S, the Sorts of U1),F1) is set

id ( the Sorts of U1 . (the_result_sort_of F)) is Relation-like the Sorts of U1 . (the_result_sort_of F) -defined the Sorts of U1 . (the_result_sort_of F) -valued Function-like one-to-one total V18( the Sorts of U1 . (the_result_sort_of F), the Sorts of U1 . (the_result_sort_of F)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of F)),( the Sorts of U1 . (the_result_sort_of F))))

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

K20( the carrier' of S, the carrier of S) is Relation-like set

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

proj2 the ResultSort of S is non empty set

proj1 the Sorts of U1 is non empty set

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

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

proj1 ( the ResultSort of S * the Sorts of U1) is non empty set

proj1 the ResultSort of S is non empty set

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

the Sorts of U1 . ( the ResultSort of S . F) is set

proj1 (Den (F,U1)) is set

proj2 (Den (F,U1)) is set

proj1 (Den (F,U1)) is set

proj1 ( the carrier of S, the Sorts of U1, the Sorts of U1,( the carrier of S, the Sorts of U1),(the_result_sort_of F)) is set

( the carrier of S, the Sorts of U1, the Sorts of U1,( the carrier of S, the Sorts of U1),(the_result_sort_of F)) . {} is set

S is non empty non void V56() 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

F is non-empty MSAlgebra over S

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

F1 is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U1, the Sorts of U2

F2 is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U2, the Sorts of F

( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2) is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U1, the Sorts of F

the carrier' of S is non empty set

c

Args (c

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 V60() M8( the carrier of S)

proj2 ( the Sorts of U1 #) is non empty set

the_result_sort_of c

( the carrier of S, the Sorts of U1, the Sorts of F,( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2),(the_result_sort_of c

the Sorts of U1 . (the_result_sort_of c

the Sorts of F . (the_result_sort_of c

K20(( the Sorts of U1 . (the_result_sort_of c

K19(K20(( the Sorts of U1 . (the_result_sort_of c

Den (c

Result (c

proj2 the Sorts of U1 is non empty set

K20((Args (c

K19(K20((Args (c

Den (c

Args (c

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

proj2 ( the Sorts of F #) is non empty set

Result (c

proj2 the Sorts of F is non empty set

K20((Args (c

K19(K20((Args (c

f is Relation-like Function-like Element of Args (c

(Den (c

( the carrier of S, the Sorts of U1, the Sorts of F,( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2),(the_result_sort_of c

(S,U1,F,c

(Den (c

( the carrier of S, the Sorts of U1, the Sorts of U2,F1,(the_result_sort_of c

the Sorts of U2 . (the_result_sort_of c

K20(( the Sorts of U1 . (the_result_sort_of c

K19(K20(( the Sorts of U1 . (the_result_sort_of c

(Den (c

( the carrier of S, the Sorts of U1, the Sorts of U2,F1,(the_result_sort_of c

Args (c

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

proj2 ( the Sorts of U2 #) is non empty set

Result (c

proj2 the Sorts of U2 is non empty set

Den (c

K20((Args (c

K19(K20((Args (c

(S,U1,U2,c

(Den (c

( the carrier of S, the Sorts of U2, the Sorts of F,F2,(the_result_sort_of c

K20(( the Sorts of U2 . (the_result_sort_of c

K19(K20(( the Sorts of U2 . (the_result_sort_of c

( the carrier of S, the Sorts of U2, the Sorts of F,F2,(the_result_sort_of c

(S,U2,F,c

(Den (c

( the carrier of S, the Sorts of U2, the Sorts of F,F2,(the_result_sort_of c

proj1 ( the carrier of S, the Sorts of U1, the Sorts of F,( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2),(the_result_sort_of c

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

K20( the carrier' of S, the carrier of S) is Relation-like set

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

proj2 the ResultSort of S is non empty set

proj1 the Sorts of U1 is non empty set

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

( the ResultSort of S * the Sorts of U1) . c

proj1 ( the ResultSort of S * the Sorts of U1) is non empty set

proj1 the ResultSort of S is non empty set

the ResultSort of S . c

the Sorts of U1 . ( the ResultSort of S . c

( the carrier of S, the Sorts of U1, the Sorts of F,( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2),(the_result_sort_of c

(Den (c

S is non empty non void V56() 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 MSAlgebra over S

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

S is non empty non void V56() 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

F is non-empty MSAlgebra over S

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

F1 is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U1, the Sorts of U2

F2 is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U2, the Sorts of F

( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2) is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U1, the Sorts of F

c

( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2) . c

proj2 (( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2) . c

the Sorts of F . c

the Sorts of U1 . c

the Sorts of U2 . c

K20(( the Sorts of U1 . c

K19(K20(( the Sorts of U1 . c

F1 . c

K20(( the Sorts of U2 . c

K19(K20(( the Sorts of U2 . c

F2 . c

f is Relation-like the Sorts of U1 . c

proj2 f is set

h is Relation-like the Sorts of U2 . c

proj1 h is set

proj2 h is set

h * f is Relation-like the Sorts of U1 . c

K20(( the Sorts of U1 . c

K19(K20(( the Sorts of U1 . c

proj2 (h * f) is set

S is non empty non void V56() 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 MSAlgebra over S

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

S is non empty non void V56() 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

F is non-empty MSAlgebra over S

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

F1 is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U1, the Sorts of U2

F2 is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U2, the Sorts of F

( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2) is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U1, the Sorts of F

proj1 ( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2) is non empty set

c

( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2) . c

f is Relation-like Function-like set

the Sorts of U2 . c

the Sorts of F . c

K20(( the Sorts of U2 . c

K19(K20(( the Sorts of U2 . c

F2 . c

the Sorts of U1 . c

K20(( the Sorts of U1 . c

K19(K20(( the Sorts of U1 . c

F1 . c

proj1 F2 is non empty set

h is Relation-like the Sorts of U2 . c

proj1 F1 is non empty set

G1 is Relation-like the Sorts of U1 . c

h * G1 is Relation-like the Sorts of U1 . c

K20(( the Sorts of U1 . c

K19(K20(( the Sorts of U1 . c

S is non empty non void V56() 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 MSAlgebra over S

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

S is non empty non void V56() 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 MSAlgebra over S

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

F is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U1, the Sorts of U2

S is non empty non void V56() 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

F is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U1, the Sorts of U2

( the carrier of S, the Sorts of U1, the Sorts of U2,F) is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U2, the Sorts of U1

the carrier' of S is non empty set

F2 is Element of the carrier' of S

Args (F2,U2) is functional non empty Element of proj2 ( the Sorts of U2 #)

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

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

proj2 ( the Sorts of U2 #) is non empty set

the_result_sort_of F2 is Element of the carrier of S

( the carrier of S, the Sorts of U2, the Sorts of U1,( the carrier of S, the Sorts of U1, the Sorts of U2,F),(the_result_sort_of F2)) is Relation-like the Sorts of U2 . (the_result_sort_of F2) -defined the Sorts of U1 . (the_result_sort_of F2) -valued Function-like non empty total V18( the Sorts of U2 . (the_result_sort_of F2), the Sorts of U1 . (the_result_sort_of F2)) Element of K19(K20(( the Sorts of U2 . (the_result_sort_of F2)),( the Sorts of U1 . (the_result_sort_of F2))))

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

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

K20(( the Sorts of U2 . (the_result_sort_of F2)),( the Sorts of U1 . (the_result_sort_of F2))) is Relation-like set

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

Result (F2,U2) is non empty Element of proj2 the Sorts of U2

proj2 the Sorts of U2 is non empty set

Den (F2,U2) is Relation-like Args (F2,U2) -defined Result (F2,U2) -valued Function-like non empty total V18( Args (F2,U2), Result (F2,U2)) Element of K19(K20((Args (F2,U2)),(Result (F2,U2))))

K20((Args (F2,U2)),(Result (F2,U2))) is Relation-like set

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

Args (F2,U1) is functional non empty Element of proj2 ( the Sorts of U1 #)

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

proj2 ( the Sorts of U1 #) is non empty set

Result (F2,U1) is non empty Element of proj2 the Sorts of U1

proj2 the Sorts of U1 is non empty set

Den (F2,U1) is Relation-like Args (F2,U1) -defined Result (F2,U1) -valued Function-like non empty total V18( Args (F2,U1), Result (F2,U1)) Element of K19(K20((Args (F2,U1)),(Result (F2,U1))))

K20((Args (F2,U1)),(Result (F2,U1))) is Relation-like set

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

c

(Den (F2,U2)) . c

( the carrier of S, the Sorts of U2, the Sorts of U1,( the carrier of S, the Sorts of U1, the Sorts of U2,F),(the_result_sort_of F2)) . ((Den (F2,U2)) . c

(S,U2,U1,F2,( the carrier of S, the Sorts of U1, the Sorts of U2,F),c

(Den (F2,U1)) . (S,U2,U1,F2,( the carrier of S, the Sorts of U1, the Sorts of U2,F),c

the_arity_of F2 is Relation-like NAT -defined the carrier of S -valued Function-like V28() countable V58() V59() Element of the carrier of S *

dom (the_arity_of F2) is countable Element of K19(NAT)

h is Relation-like Function-like set

proj1 h is set

proj1 (S,U2,U1,F2,( the carrier of S, the Sorts of U1, the Sorts of U2,F),c

proj1 F is non empty set

( the carrier of S, the Sorts of U1, the Sorts of U2,F,(the_result_sort_of F2)) is Relation-like the Sorts of U1 . (the_result_sort_of F2) -defined the Sorts of U2 . (the_result_sort_of F2) -valued Function-like non empty total V18( the Sorts of U1 . (the_result_sort_of F2), the Sorts of U2 . (the_result_sort_of F2)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of F2)),( the Sorts of U2 . (the_result_sort_of F2))))

K20(( the Sorts of U1 . (the_result_sort_of F2)),( the Sorts of U2 . (the_result_sort_of F2))) is Relation-like set

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

proj1 ( the carrier of S, the Sorts of U1, the Sorts of U2,F,(the_result_sort_of F2)) is non empty set

( the carrier of S, the Sorts of U1, the Sorts of U2,F,(the_result_sort_of F2)) " is Relation-like Function-like set

( the carrier of S, the Sorts of U2, the Sorts of U1,( the carrier of S, the Sorts of U1, the Sorts of U2,F),(the_result_sort_of F2)) * ( the carrier of S, the Sorts of U1, the Sorts of U2,F,(the_result_sort_of F2)) is Relation-like the Sorts of U1 . (the_result_sort_of F2) -defined the Sorts of U1 . (the_result_sort_of F2) -valued Function-like non empty total V18( the Sorts of U1 . (the_result_sort_of F2), the Sorts of U1 . (the_result_sort_of F2)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of F2)),( the Sorts of U1 . (the_result_sort_of F2))))

K20(( the Sorts of U1 . (the_result_sort_of F2)),( the Sorts of U1 . (the_result_sort_of F2))) is Relation-like set

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

id ( the Sorts of U1 . (the_result_sort_of F2)) is Relation-like the Sorts of U1 . (the_result_sort_of F2) -defined the Sorts of U1 . (the_result_sort_of F2) -valued Function-like one-to-one non empty total V18( the Sorts of U1 . (the_result_sort_of F2), the Sorts of U1 . (the_result_sort_of F2)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of F2)),( the Sorts of U1 . (the_result_sort_of F2))))

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

K20( the carrier' of S, the carrier of S) is Relation-like set

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

proj1 the ResultSort of S is non empty set

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

proj1 ( the ResultSort of S * the Sorts of U1) is non empty set

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

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

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

proj1 (( the carrier of S, the Sorts of U2, the Sorts of U1,( the carrier of S, the Sorts of U1, the Sorts of U2,F),(the_result_sort_of F2)) * ( the carrier of S, the Sorts of U1, the Sorts of U2,F,(the_result_sort_of F2))) is non empty set

G1 is Relation-like Function-like Element of Args (F2,U1)

(Den (F2,U1)) . G1 is Element of Result (F2,U1)

( the carrier of S, the Sorts of U1, the Sorts of U2,F,(the_result_sort_of F2)) . ((Den (F2,U1)) . G1) is set

(S,U1,U2,F2,F,(S,U2,U1,F2,( the carrier of S, the Sorts of U1, the Sorts of U2,F),c

(Den (F2,U2)) . (S,U1,U2,F2,F,(S,U2,U1,F2,( the carrier of S, the Sorts of U1, the Sorts of U2,F),c

( the carrier of S, the Sorts of U2, the Sorts of U1, the Sorts of U2,( the carrier of S, the Sorts of U1, the Sorts of U2,F),F) is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U2, the Sorts of U2

(S,U2,U2,F2,( the carrier of S, the Sorts of U2, the Sorts of U1, the Sorts of U2,( the carrier of S, the Sorts of U1, the Sorts of U2,F),F),c

(Den (F2,U2)) . (S,U2,U2,F2,( the carrier of S, the Sorts of U2, the Sorts of U1, the Sorts of U2,( the carrier of S, the Sorts of U1, the Sorts of U2,F),F),c

( the carrier of S, the Sorts of U2) is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U2, the Sorts of U2

(S,U2,U2,F2,( the carrier of S, the Sorts of U2),c

(Den (F2,U2)) . (S,U2,U2,F2,( the carrier of S, the Sorts of U2),c

(( the carrier of S, the Sorts of U2, the Sorts of U1,( the carrier of S, the Sorts of U1, the Sorts of U2,F),(the_result_sort_of F2)) * ( the carrier of S, the Sorts of U1, the Sorts of U2,F,(the_result_sort_of F2))) . ((Den (F2,U1)) . (S,U2,U1,F2,( the carrier of S, the Sorts of U1, the Sorts of U2,F),c

S is non empty non void V56() 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

F is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U1, the Sorts of U2

( the carrier of S, the Sorts of U1, the Sorts of U2,F) is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U2, the Sorts of U1

F1 is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U2, the Sorts of U1

proj1 F1 is non empty set

F2 is set

F1 . F2 is Relation-like Function-like set

c

the Sorts of U1 . F2 is set

the Sorts of U2 . F2 is set

K20(( the Sorts of U1 . F2),( the Sorts of U2 . F2)) is Relation-like set

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

F . F2 is Relation-like Function-like set

proj1 F is non empty set

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

f " is Relation-like Function-like set

F2 is set

F1 . F2 is Relation-like Function-like set

proj2 (F1 . F2) is set

the Sorts of U1 . F2 is set

the Sorts of U2 . F2 is set

K20(( the Sorts of U1 . F2),( the Sorts of U2 . F2)) is Relation