:: 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₇ is set
F2 . c₇ is Relation-like Function-like set
U1 . c₇ is set
id (U1 . c₇) is Relation-like U1 . c₇ -defined U1 . c₇ -valued Function-like one-to-one total V18(U1 . c₇,U1 . c₇) Element of K19(K20((U1 . c₇),(U1 . c₇)))
K20((U1 . c₇),(U1 . c₇)) is Relation-like set
K19(K20((U1 . c₇),(U1 . c₇))) is set
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₇ is set
(F2 ** F1) . c₇ is Relation-like Function-like set
F1 . c₇ is Relation-like Function-like set
F2 . c₇ is Relation-like Function-like set
(F1 . c₇) * (F2 . c₇) 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
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₇ is Relation-like S -defined Function-like total set
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₇ is Relation-like U1 . F2 -defined U2 . F2 -valued Function-like V18(U1 . F2,U2 . F2) Element of K19(K20((U1 . F2),(U2 . F2)))
c₇ * f is Relation-like U1 . F2 -defined U2 . F2 -valued Function-like V18(U1 . F2,U2 . F2) Element of K19(K20((U1 . F2),(U2 . F2)))
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₇ * (id (U1 . F2)) is Relation-like U1 . F2 -defined U2 . F2 -valued Function-like V18(U1 . F2,U2 . F2) Element of K19(K20((U1 . F2),(U2 . F2)))
proj1 c₇ 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
(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₇ is Relation-like U1 . F2 -defined U2 . F2 -valued Function-like V18(U1 . F2,U2 . F2) Element of K19(K20((U1 . F2),(U2 . F2)))
f * c₇ is Relation-like U1 . F2 -defined U2 . F2 -valued Function-like V18(U1 . F2,U2 . F2) Element of K19(K20((U1 . F2),(U2 . F2)))
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₇ is set
F2 . c₇ is set
U1 . c₇ is set
U2 . c₇ is set
K20((U1 . c₇),(U2 . c₇)) is Relation-like set
K19(K20((U1 . c₇),(U2 . c₇))) is set
F . c₇ is Relation-like Function-like set
f is Relation-like U1 . c₇ -defined U2 . c₇ -valued Function-like V18(U1 . c₇,U2 . c₇) Element of K19(K20((U1 . c₇),(U2 . c₇)))
f " is Relation-like Function-like set
c₇ is Relation-like S -defined Function-like total V41() V42() set
f is set
c₇ . f is Relation-like Function-like set
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₇ is set
U1 . c₇ is set
U2 . c₇ is set
K20((U1 . c₇),(U2 . c₇)) is Relation-like set
K19(K20((U1 . c₇),(U2 . c₇))) is set
F . c₇ is Relation-like Function-like set
F1 . c₇ is Relation-like Function-like set
f is Relation-like U1 . c₇ -defined U2 . c₇ -valued Function-like V18(U1 . c₇,U2 . c₇) Element of K19(K20((U1 . c₇),(U2 . c₇)))
f " is Relation-like Function-like set
F2 . c₇ is Relation-like Function-like set
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₇ is Relation-like U1 . F2 -defined U2 . F2 -valued Function-like V18(U1 . F2,U2 . F2) Element of K19(K20((U1 . F2),(U2 . F2)))
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₇ " is Relation-like Function-like set
c₇ * f is Relation-like U2 . F2 -defined U2 . F2 -valued Function-like Element of K19(K20((U2 . F2),(U2 . F2)))
K20((U2 . F2),(U2 . F2)) is Relation-like set
K19(K20((U2 . F2),(U2 . F2))) is set
proj2 c₇ is set
id (proj2 c₇) is Relation-like proj2 c₇ -defined proj2 c₇ -valued Function-like one-to-one total V18( proj2 c₇, proj2 c₇) Element of K19(K20((proj2 c₇),(proj2 c₇)))
K20((proj2 c₇),(proj2 c₇)) is Relation-like set
K19(K20((proj2 c₇),(proj2 c₇))) is set
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₇ is Relation-like U1 . F2 -defined U2 . F2 -valued Function-like V18(U1 . F2,U2 . F2) Element of K19(K20((U1 . F2),(U2 . F2)))
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₇ " is Relation-like Function-like set
proj1 c₇ is set
f * c₇ is Relation-like U1 . F2 -defined U1 . F2 -valued Function-like Element of K19(K20((U1 . F2),(U1 . F2)))
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₇ is set
((the_arity_of F) * F1) . c₇ is Relation-like Function-like set
(the_arity_of F) . c₇ is set
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₇ is set
f is V21() V22() V23() V27() Element of NAT
(the_arity_of F) . f is set
(the_arity_of F) . c₇ 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
c₇ is set
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₇ is set
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₇ is set
the Sorts of U2 . ((the_arity_of F) . c₇) is set
proj2 ((the_arity_of F) * the Sorts of U2) is set
the Sorts of U1 . ((the_arity_of F) . c₇) is set
K20(( the Sorts of U1 . ((the_arity_of F) . c₇)),( the Sorts of U2 . ((the_arity_of F) . c₇))) is Relation-like set
K19(K20(( the Sorts of U1 . ((the_arity_of F) . c₇)),( the Sorts of U2 . ((the_arity_of F) . c₇)))) is set
F1 . ((the_arity_of F) . c₇) is Relation-like Function-like set
((the_arity_of F) * the Sorts of U1) . c₇ is set
h is Relation-like the Sorts of U1 . ((the_arity_of F) . c₇) -defined the Sorts of U2 . ((the_arity_of F) . c₇) -valued Function-like V18( the Sorts of U1 . ((the_arity_of F) . c₇), the Sorts of U2 . ((the_arity_of F) . c₇)) Element of K19(K20(( the Sorts of U1 . ((the_arity_of F) . c₇)),( the Sorts of U2 . ((the_arity_of F) . c₇))))
proj1 h is set
((the_arity_of F) * F1) . c₇ is Relation-like Function-like set
proj1 (((the_arity_of F) * F1) . c₇) is set
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₇ is Relation-like Function-like set
proj1 c₇ is set
((the_arity_of F) * F1) .. c₇ is Relation-like Function-like set
proj1 (((the_arity_of F) * F1) .. c₇) is set
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₇) . f is set
c₇ . f is set
h . (c₇ . f) is set
((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₇ is Relation-like Function-like set
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₇ is set
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₇ is Relation-like Function-like set
(((the_arity_of F) * F1) .. c₇) . h is set
c₇ . h is set
( the carrier of S, the Sorts of U1, the Sorts of U2,F1,((the_arity_of F) /. h)) . (c₇ . h) is set
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₇ . a is set
( the carrier of S, the Sorts of U1, the Sorts of U2,F1,((the_arity_of F) /. a)) . (c₇ . a) is set
(((the_arity_of F) * F1) .. c₇) . a is set
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₇ is Relation-like Function-like Element of Args (F,U2)
f is V21() V22() V23() V27() set
c₇ . f is set
(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₇ is Element of F1
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₇ is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of F, the Sorts of F1
( the carrier of S, the Sorts of U2, the Sorts of F, the Sorts of F1,F2,c₇) is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of U2, the Sorts of F1
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₇),f) is Relation-like Function-like Element of Args (U1,F1)
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₇,(S,U2,F,U1,F2,f)) is Relation-like Function-like Element of Args (U1,F1)
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₇),f) . h is set
(S,F,F1,U1,c₇,(S,U2,F,U1,F2,f)) . h is set
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₇),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 Relation-like the Sorts of U2 . ((the_arity_of U1) /. G1) -defined the Sorts of F1 . ((the_arity_of U1) /. G1) -valued Function-like non empty total V18( the Sorts of U2 . ((the_arity_of U1) /. G1), the Sorts of F1 . ((the_arity_of U1) /. G1)) Element of K19(K20(( the Sorts of U2 . ((the_arity_of U1) /. G1)),( the Sorts of F1 . ((the_arity_of U1) /. G1))))
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)) . (f . G1) is set
(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₇,((the_arity_of U1) /. G1)) is Relation-like the Sorts of F . ((the_arity_of U1) /. G1) -defined the Sorts of F1 . ((the_arity_of U1) /. G1) -valued Function-like non empty total V18( the Sorts of F . ((the_arity_of U1) /. G1), the Sorts of F1 . ((the_arity_of U1) /. G1)) Element of K19(K20(( the Sorts of F . ((the_arity_of U1) /. G1)),( the Sorts of F1 . ((the_arity_of U1) /. G1))))
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₇,((the_arity_of U1) /. G1)) * ( 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 F1 . ((the_arity_of U1) /. G1) -valued Function-like non empty total V18( the Sorts of U2 . ((the_arity_of U1) /. G1), the Sorts of F1 . ((the_arity_of U1) /. G1)) Element of K19(K20(( the Sorts of U2 . ((the_arity_of U1) /. G1)),( the Sorts of F1 . ((the_arity_of U1) /. G1))))
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_arity_of U1) /. G1)) * ( the carrier of S, the Sorts of U2, the Sorts of F,F2,((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)) . (f . G1) is set
( the carrier of S, the Sorts of F, the Sorts of F1,c₇,((the_arity_of U1) /. G1)) . (( the carrier of S, the Sorts of U2, the Sorts of F,F2,((the_arity_of U1) /. G1)) . (f . G1)) is set
(S,U2,F,U1,F2,f) . G1 is set
( the carrier of S, the Sorts of F, the Sorts of F1,c₇,((the_arity_of U1) /. G1)) . ((S,U2,F,U1,F2,f) . G1) is set
proj1 (S,U2,F1,U1,( the carrier of S, the Sorts of U2, the Sorts of F, the Sorts of F1,F2,c₇),f) is set
proj1 (S,F,F1,U1,c₇,(S,U2,F,U1,F2,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 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₇ is Element of the carrier' of S
Args (c₇,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
the_result_sort_of c₇ is Element of the carrier of S
( 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₇)) is Relation-like the Sorts of U1 . (the_result_sort_of c₇) -defined the Sorts of F . (the_result_sort_of c₇) -valued Function-like non empty total V18( the Sorts of U1 . (the_result_sort_of c₇), the Sorts of F . (the_result_sort_of c₇)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of c₇)),( the Sorts of F . (the_result_sort_of c₇))))
the Sorts of U1 . (the_result_sort_of c₇) is non empty set
the Sorts of F . (the_result_sort_of c₇) is non empty set
K20(( the Sorts of U1 . (the_result_sort_of c₇)),( the Sorts of F . (the_result_sort_of c₇))) is Relation-like set
K19(K20(( the Sorts of U1 . (the_result_sort_of c₇)),( the Sorts of F . (the_result_sort_of c₇)))) is set
Den (c₇,U1) is Relation-like Args (c₇,U1) -defined Result (c₇,U1) -valued Function-like non empty total V18( Args (c₇,U1), Result (c₇,U1)) Element of K19(K20((Args (c₇,U1)),(Result (c₇,U1))))
Result (c₇,U1) is non empty Element of proj2 the Sorts of U1
proj2 the Sorts of U1 is non empty set
K20((Args (c₇,U1)),(Result (c₇,U1))) is Relation-like set
K19(K20((Args (c₇,U1)),(Result (c₇,U1)))) is set
Den (c₇,F) is Relation-like Args (c₇,F) -defined Result (c₇,F) -valued Function-like non empty total V18( Args (c₇,F), Result (c₇,F)) Element of K19(K20((Args (c₇,F)),(Result (c₇,F))))
Args (c₇,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
Result (c₇,F) is non empty Element of proj2 the Sorts of F
proj2 the Sorts of F is non empty set
K20((Args (c₇,F)),(Result (c₇,F))) is Relation-like set
K19(K20((Args (c₇,F)),(Result (c₇,F)))) is set
f is Relation-like Function-like Element of Args (c₇,U1)
(Den (c₇,U1)) . f is set
( 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₇,U1)) . f) is set
(S,U1,F,c₇,( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2),f) is Relation-like Function-like Element of Args (c₇,F)
(Den (c₇,F)) . (S,U1,F,c₇,( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2),f) is set
( the carrier of S, the Sorts of U1, the Sorts of U2,F1,(the_result_sort_of c₇)) is Relation-like the Sorts of U1 . (the_result_sort_of c₇) -defined the Sorts of U2 . (the_result_sort_of c₇) -valued Function-like non empty total V18( the Sorts of U1 . (the_result_sort_of c₇), the Sorts of U2 . (the_result_sort_of c₇)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of c₇)),( the Sorts of U2 . (the_result_sort_of c₇))))
the Sorts of U2 . (the_result_sort_of c₇) is non empty set
K20(( the Sorts of U1 . (the_result_sort_of c₇)),( the Sorts of U2 . (the_result_sort_of c₇))) is Relation-like set
K19(K20(( the Sorts of U1 . (the_result_sort_of c₇)),( the Sorts of U2 . (the_result_sort_of c₇)))) is set
(Den (c₇,U1)) . f is Element of Result (c₇,U1)
( the carrier of S, the Sorts of U1, the Sorts of U2,F1,(the_result_sort_of c₇)) . ((Den (c₇,U1)) . f) is set
Args (c₇,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
Result (c₇,U2) is non empty Element of proj2 the Sorts of U2
proj2 the Sorts of U2 is non empty set
Den (c₇,U2) is Relation-like Args (c₇,U2) -defined Result (c₇,U2) -valued Function-like non empty total V18( Args (c₇,U2), Result (c₇,U2)) Element of K19(K20((Args (c₇,U2)),(Result (c₇,U2))))
K20((Args (c₇,U2)),(Result (c₇,U2))) is Relation-like set
K19(K20((Args (c₇,U2)),(Result (c₇,U2)))) is set
(S,U1,U2,c₇,F1,f) is Relation-like Function-like Element of Args (c₇,U2)
(Den (c₇,U2)) . (S,U1,U2,c₇,F1,f) is Element of Result (c₇,U2)
( the carrier of S, the Sorts of U2, the Sorts of F,F2,(the_result_sort_of c₇)) is Relation-like the Sorts of U2 . (the_result_sort_of c₇) -defined the Sorts of F . (the_result_sort_of c₇) -valued Function-like non empty total V18( the Sorts of U2 . (the_result_sort_of c₇), the Sorts of F . (the_result_sort_of c₇)) Element of K19(K20(( the Sorts of U2 . (the_result_sort_of c₇)),( the Sorts of F . (the_result_sort_of c₇))))
K20(( the Sorts of U2 . (the_result_sort_of c₇)),( the Sorts of F . (the_result_sort_of c₇))) is Relation-like set
K19(K20(( the Sorts of U2 . (the_result_sort_of c₇)),( the Sorts of F . (the_result_sort_of c₇)))) is set
( the carrier of S, the Sorts of U2, the Sorts of F,F2,(the_result_sort_of c₇)) . (( the carrier of S, the Sorts of U1, the Sorts of U2,F1,(the_result_sort_of c₇)) . ((Den (c₇,U1)) . f)) is set
(S,U2,F,c₇,F2,(S,U1,U2,c₇,F1,f)) is Relation-like Function-like Element of Args (c₇,F)
(Den (c₇,F)) . (S,U2,F,c₇,F2,(S,U1,U2,c₇,F1,f)) is Element of Result (c₇,F)
( the carrier of S, the Sorts of U2, the Sorts of F,F2,(the_result_sort_of c₇)) * ( the carrier of S, the Sorts of U1, the Sorts of U2,F1,(the_result_sort_of c₇)) is Relation-like the Sorts of U1 . (the_result_sort_of c₇) -defined the Sorts of F . (the_result_sort_of c₇) -valued Function-like non empty total V18( the Sorts of U1 . (the_result_sort_of c₇), the Sorts of F . (the_result_sort_of c₇)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of c₇)),( the Sorts of F . (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₇)) is non empty set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
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₇ is non empty 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 . c₇ is Element of the carrier of S
the Sorts of U1 . ( the ResultSort of S . c₇) is non empty set
( 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₇,U1)) . f) is set
(Den (c₇,F)) . (S,U1,F,c₇,( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2),f) is Element of Result (c₇,F)
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₇ is set
( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2) . c₇ is Relation-like Function-like set
proj2 (( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2) . c₇) is set
the Sorts of F . c₇ is set
the Sorts of U1 . c₇ is set
the Sorts of U2 . c₇ is set
K20(( the Sorts of U1 . c₇),( the Sorts of U2 . c₇)) is Relation-like set
K19(K20(( the Sorts of U1 . c₇),( the Sorts of U2 . c₇))) is set
F1 . c₇ is Relation-like Function-like set
K20(( the Sorts of U2 . c₇),( the Sorts of F . c₇)) is Relation-like set
K19(K20(( the Sorts of U2 . c₇),( the Sorts of F . c₇))) is set
F2 . c₇ is Relation-like Function-like set
f is Relation-like the Sorts of U1 . c₇ -defined the Sorts of U2 . c₇ -valued Function-like V18( the Sorts of U1 . c₇, the Sorts of U2 . c₇) Element of K19(K20(( the Sorts of U1 . c₇),( the Sorts of U2 . c₇)))
proj2 f is set
h is Relation-like the Sorts of U2 . c₇ -defined the Sorts of F . c₇ -valued Function-like V18( the Sorts of U2 . c₇, the Sorts of F . c₇) Element of K19(K20(( the Sorts of U2 . c₇),( the Sorts of F . c₇)))
proj1 h is set
proj2 h is set
h * f is Relation-like the Sorts of U1 . c₇ -defined the Sorts of F . c₇ -valued Function-like Element of K19(K20(( the Sorts of U1 . c₇),( the Sorts of F . c₇)))
K20(( the Sorts of U1 . c₇),( the Sorts of F . c₇)) is Relation-like set
K19(K20(( the Sorts of U1 . c₇),( the Sorts of F . c₇))) is set
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₇ is set
( the carrier of S, the Sorts of U1, the Sorts of U2, the Sorts of F,F1,F2) . c₇ is Relation-like Function-like set
f is Relation-like Function-like set
the Sorts of U2 . c₇ is set
the Sorts of F . c₇ is set
K20(( the Sorts of U2 . c₇),( the Sorts of F . c₇)) is Relation-like set
K19(K20(( the Sorts of U2 . c₇),( the Sorts of F . c₇))) is set
F2 . c₇ is Relation-like Function-like set
the Sorts of U1 . c₇ is set
K20(( the Sorts of U1 . c₇),( the Sorts of U2 . c₇)) is Relation-like set
K19(K20(( the Sorts of U1 . c₇),( the Sorts of U2 . c₇))) is set
F1 . c₇ is Relation-like Function-like set
proj1 F2 is non empty set
h is Relation-like the Sorts of U2 . c₇ -defined the Sorts of F . c₇ -valued Function-like V18( the Sorts of U2 . c₇, the Sorts of F . c₇) Element of K19(K20(( the Sorts of U2 . c₇),( the Sorts of F . c₇)))
proj1 F1 is non empty set
G1 is Relation-like the Sorts of U1 . c₇ -defined the Sorts of U2 . c₇ -valued Function-like V18( the Sorts of U1 . c₇, the Sorts of U2 . c₇) Element of K19(K20(( the Sorts of U1 . c₇),( the Sorts of U2 . c₇)))
h * G1 is Relation-like the Sorts of U1 . c₇ -defined the Sorts of F . c₇ -valued Function-like Element of K19(K20(( the Sorts of U1 . c₇),( the Sorts of F . c₇)))
K20(( the Sorts of U1 . c₇),( the Sorts of F . c₇)) is Relation-like set
K19(K20(( the Sorts of U1 . c₇),( the Sorts of F . c₇))) 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 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₇ is Relation-like Function-like Element of Args (F2,U2)
(Den (F2,U2)) . c₇ is Element of Result (F2,U2)
( 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₇) is set
(S,U2,U1,F2,( the carrier of S, the Sorts of U1, the Sorts of U2,F),c₇) is Relation-like Function-like Element of Args (F2,U1)
(Den (F2,U1)) . (S,U2,U1,F2,( the carrier of S, the Sorts of U1, the Sorts of U2,F),c₇) is Element of Result (F2,U1)
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₇) is set
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₇)) is Relation-like Function-like Element of Args (F2,U2)
(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₇)) is Element of Result (F2,U2)
( 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₇) is Relation-like Function-like Element of Args (F2,U2)
(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₇) is Element of Result (F2,U2)
( 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₇) is Relation-like Function-like Element of Args (F2,U2)
(Den (F2,U2)) . (S,U2,U2,F2,( the carrier of S, the Sorts of U2),c₇) is Element of Result (F2,U2)
(( 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₇)) 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 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₇ is Relation-like Function-like 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-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-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
c₇ 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)))
c₇ " is Relation-like Function-like set
proj2 (c₇ ") is set
proj1 c₇ 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
S is non empty non void V56() ManySortedSign
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
proj1 ( the carrier of S, the Sorts of U1) is non empty set
U2 is set
( the carrier of S, the Sorts of U1) . U2 is Relation-like Function-like set
F is Relation-like Function-like set
the Sorts of U1 . U2 is set
id ( the Sorts of U1 . U2) is Relation-like the Sorts of U1 . U2 -defined the Sorts of U1 . U2 -valued Function-like one-to-one total V18( the Sorts of U1 . U2, the Sorts of U1 . U2) Element of K19(K20(( the Sorts of U1 . U2),( the Sorts of U1 . U2)))
K20(( the Sorts of U1 . U2),( the Sorts of U1 . U2)) is Relation-like set
K19(K20(( the Sorts of U1 . U2),( the Sorts of U1 . U2))) is set
U2 is set
( the carrier of S, the Sorts of U1) . U2 is Relation-like Function-like set
proj2 (( the carrier of S, the Sorts of U1) . U2) is set
the Sorts of U1 . U2 is set
id ( the Sorts of U1 . U2) is Relation-like the Sorts of U1 . U2 -defined the Sorts of U1 . U2 -valued Function-like one-to-one total V18( the Sorts of U1 . U2, the Sorts of U1 . U2) Element of K19(K20(( the Sorts of U1 . U2),( the Sorts of U1 . U2)))
K20(( the Sorts of U1 . U2),( the Sorts of U1 . U2)) is Relation-like set
K19(K20(( the Sorts of U1 . U2),( the Sorts of U1 . U2))) is set
S is non empty non void V56() ManySortedSign
F is MSAlgebra over S
S is non empty non void V56() ManySortedSign
U1 is non-empty MSAlgebra over S
U2 is non-empty MSAlgebra over S
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 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
S is non empty non void V56() ManySortedSign
U1 is non-empty MSAlgebra over S
U2 is non-empty MSAlgebra over S
F is non-empty MSAlgebra over S
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 U2 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
the Sorts of F is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total 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
( 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₇ 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
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
F .:.: the Sorts of U1 is Relation-like the carrier of S -defined Function-like non empty total set
F2 is set
F . F2 is Relation-like Function-like set
(F .:.: the Sorts of U1) . F2 is set
c₇ is Relation-like Function-like set
the Sorts of U1 . F2 is 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 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)))
proj1 f is set
F2 is set
F . F2 is Relation-like Function-like set
(F .:.: the Sorts of U1) . F2 is set
c₇ is Relation-like Function-like set
the Sorts of U1 . F2 is 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 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)))
proj2 f is set
proj1 f is set
F2 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total ManySortedSubset of the Sorts of U2
GenMSAlg F2 is strict non-empty MSSubAlgebra of U2
Opers (U2,F2) is Relation-like the carrier' of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Arity of S * (F2 #), the ResultSort of S * F2
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 non empty total V18( the carrier' of S, the carrier of S * ) V41() V42() Element of K19(K20( the carrier' of S,( the carrier of S *)))
the carrier of S * is functional non empty V60() M8( 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
F2 # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * (F2 #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S * F2 is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# F2,(Opers (U2,F2)) #) is strict MSAlgebra over S
the Sorts of (GenMSAlg F2) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
h is Element of the carrier' of S
Args (h,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
Result (h,U2) is non empty Element of proj2 the Sorts of U2
proj2 the Sorts of U2 is non empty set
Den (h,U2) is Relation-like Args (h,U2) -defined Result (h,U2) -valued Function-like non empty total V18( Args (h,U2), Result (h,U2)) Element of K19(K20((Args (h,U2)),(Result (h,U2))))
K20((Args (h,U2)),(Result (h,U2))) is Relation-like set
K19(K20((Args (h,U2)),(Result (h,U2)))) is set
( the Arity of S * (F2 #)) . h is set
(Den (h,U2)) | (( the Arity of S * (F2 #)) . h) is Relation-like Args (h,U2) -defined ( the Arity of S * (F2 #)) . h -defined Args (h,U2) -defined Result (h,U2) -valued Function-like Element of K19(K20((Args (h,U2)),(Result (h,U2))))
proj2 ((Den (h,U2)) | (( the Arity of S * (F2 #)) . h)) is set
( the ResultSort of S * F2) . h is non empty set
G1 is set
the_arity_of h is Relation-like NAT -defined the carrier of S -valued Function-like V28() countable V58() V59() Element of the carrier of S *
the_result_sort_of h is Element of the carrier of S
(the_arity_of h) * F2 is Relation-like non-empty NAT -defined Function-like set
proj2 (the_arity_of h) is set
proj1 the Arity of S is non empty set
proj1 ( the Arity of S * (F2 #)) is non empty set
the Arity of S . h is Relation-like NAT -defined Function-like V28() countable V58() V59() Element of the carrier of S *
(F2 #) . ( the Arity of S . h) is set
(F2 #) . (the_arity_of h) is set
product ((the_arity_of h) * F2) is functional non empty with_common_domain product-like set
proj1 ((Den (h,U2)) | (( the Arity of S * (F2 #)) . h)) is set
a is set
((Den (h,U2)) | (( the Arity of S * (F2 #)) . h)) . a is set
(Den (h,U2)) . a is set
proj1 (Den (h,U2)) is non empty set
a is Relation-like Function-like Element of Args (h,U2)
proj1 a is set
proj1 ((the_arity_of h) * F2) is set
proj1 F2 is non empty set
f is set
(the_arity_of h) . f is set
a . f is set
((the_arity_of h) * F2) . f is set
dom (the_arity_of h) is countable Element of K19(NAT)
a1 is Element of the carrier of S
( the carrier of S, the Sorts of U1, the Sorts of U2,F,a1) is Relation-like the Sorts of U1 . a1 -defined the Sorts of U2 . a1 -valued Function-like non empty total V18( the Sorts of U1 . a1, the Sorts of U2 . a1) Element of K19(K20(( the Sorts of U1 . a1),( the Sorts of U2 . a1)))
the Sorts of U1 . a1 is non empty set
the Sorts of U2 . a1 is non empty set
K20(( the Sorts of U1 . a1),( the Sorts of U2 . a1)) is Relation-like set
K19(K20(( the Sorts of U1 . a1),( the Sorts of U2 . a1))) is set
proj1 ( the carrier of S, the Sorts of U1, the Sorts of U2,F,a1) is non empty set
F2 . ((the_arity_of h) . f) is set
( the carrier of S, the Sorts of U1, the Sorts of U2,F,a1) .: ( the Sorts of U1 . a1) is set
proj2 ( the carrier of S, the Sorts of U1, the Sorts of U2,F,a1) is non empty set
g is set
( the carrier of S, the Sorts of U1, the Sorts of U2,F,a1) . g is set
n is Element of the carrier of S
the Sorts of U1 . n is non empty set
( the carrier of S, the Sorts of U1, the Sorts of U2,F,n) is Relation-like the Sorts of U1 . n -defined the Sorts of U2 . n -valued Function-like non empty total V18( the Sorts of U1 . n, the Sorts of U2 . n) Element of K19(K20(( the Sorts of U1 . n),( the Sorts of U2 . n)))
the Sorts of U2 . n is non empty set
K20(( the Sorts of U1 . n),( the Sorts of U2 . n)) is Relation-like set
K19(K20(( the Sorts of U1 . n),( the Sorts of U2 . n))) is set
( the carrier of S, the Sorts of U1, the Sorts of U2,F,n) . g is set
f is Relation-like Function-like set
proj1 f is set
proj1 the Sorts of U1 is non empty set
(the_arity_of h) * the Sorts of U1 is Relation-like non-empty NAT -defined Function-like set
proj1 ((the_arity_of h) * the Sorts of U1) is set
dom (the_arity_of h) is countable Element of K19(NAT)
a1 is set
f . a1 is set
((the_arity_of h) * the Sorts of U1) . a1 is set
(the_arity_of h) . a1 is set
g is Element of the carrier of S
the Sorts of U1 . g is non empty set
Args (h,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
product ((the_arity_of h) * the Sorts of U1) is functional non empty with_common_domain product-like set
a1 is Relation-like Function-like Element of Args (h,U1)
proj1 a1 is set
g is set
(the_arity_of h) . g is set
(S,U1,U2,h,F,a1) is Relation-like Function-like Element of Args (h,U2)
n is V21() V22() V23() V27() set
(S,U1,U2,h,F,a1) . n is set
(the_arity_of h) /. n is Element of the carrier of S
( the carrier of S, the Sorts of U1, the Sorts of U2,F,((the_arity_of h) /. n)) is Relation-like the Sorts of U1 . ((the_arity_of h) /. n) -defined the Sorts of U2 . ((the_arity_of h) /. n) -valued Function-like non empty total V18( the Sorts of U1 . ((the_arity_of h) /. n), the Sorts of U2 . ((the_arity_of h) /. n)) Element of K19(K20(( the Sorts of U1 . ((the_arity_of h) /. n)),( the Sorts of U2 . ((the_arity_of h) /. n))))
the Sorts of U1 . ((the_arity_of h) /. n) is non empty set
the Sorts of U2 . ((the_arity_of h) /. n) is non empty set
K20(( the Sorts of U1 . ((the_arity_of h) /. n)),( the Sorts of U2 . ((the_arity_of h) /. n))) is Relation-like set
K19(K20(( the Sorts of U1 . ((the_arity_of h) /. n)),( the Sorts of U2 . ((the_arity_of h) /. n)))) is set
a1 . n is set
( the carrier of S, the Sorts of U1, the Sorts of U2,F,((the_arity_of h) /. n)) . (a1 . n) is set
s is Element of the carrier of S
( the carrier of S, the Sorts of U1, the Sorts of U2,F,s) is Relation-like the Sorts of U1 . s -defined the Sorts of U2 . s -valued Function-like non empty total 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 Relation-like set
K19(K20(( the Sorts of U1 . s),( the Sorts of U2 . s))) is set
( the carrier of S, the Sorts of U1, the Sorts of U2,F,s) . (a1 . n) is set
(S,U1,U2,h,F,a1) . g is set
a . g is set
proj1 (S,U1,U2,h,F,a1) is set
( the carrier of S, the Sorts of U1, the Sorts of U2,F,(the_result_sort_of h)) is Relation-like the Sorts of U1 . (the_result_sort_of h) -defined the Sorts of U2 . (the_result_sort_of h) -valued Function-like non empty total V18( the Sorts of U1 . (the_result_sort_of h), the Sorts of U2 . (the_result_sort_of h)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of h)),( the Sorts of U2 . (the_result_sort_of h))))
the Sorts of U1 . (the_result_sort_of h) is non empty set
the Sorts of U2 . (the_result_sort_of h) is non empty set
K20(( the Sorts of U1 . (the_result_sort_of h)),( the Sorts of U2 . (the_result_sort_of h))) is Relation-like set
K19(K20(( the Sorts of U1 . (the_result_sort_of h)),( the Sorts of U2 . (the_result_sort_of h)))) is set
Result (h,U1) is non empty Element of proj2 the Sorts of U1
proj2 the Sorts of U1 is non empty set
Den (h,U1) is Relation-like Args (h,U1) -defined Result (h,U1) -valued Function-like non empty total V18( Args (h,U1), Result (h,U1)) Element of K19(K20((Args (h,U1)),(Result (h,U1))))
K20((Args (h,U1)),(Result (h,U1))) is Relation-like set
K19(K20((Args (h,U1)),(Result (h,U1)))) is set
(Den (h,U1)) . a1 is Element of Result (h,U1)
( the carrier of S, the Sorts of U1, the Sorts of U2,F,(the_result_sort_of h)) . ((Den (h,U1)) . a1) is set
proj1 ( the carrier of S, the Sorts of U1, the Sorts of U2,F,(the_result_sort_of h)) is non empty 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) . h is non empty set
the ResultSort of S . h is Element of the carrier of S
the Sorts of U1 . ( the ResultSort of S . h) is non empty set
proj1 ( the ResultSort of S * F2) is non empty set
F2 . ( the ResultSort of S . h) is non empty set
F2 . (the_result_sort_of h) is non empty set
g is Relation-like Function-like set
g .: ( the Sorts of U1 . (the_result_sort_of h)) is set
proj2 g is 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
the Charact of f is Relation-like the carrier' of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Arity of S * ( the Sorts of f #), the ResultSort of S * the Sorts of f
the Sorts of f # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ( the Sorts of f #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S * the Sorts of f is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
h is Relation-like the carrier of S -defined Function-like non empty total ManySortedSubset of the Sorts of U2
Opers (U2,h) is Relation-like the carrier' of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Arity of S * (h #), the ResultSort of S * h
h # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * (h #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S * h is Relation-like the carrier' of S -defined Function-like non empty total set
F1 is strict non-empty MSSubAlgebra of U2
the Sorts of F1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F2 is strict non-empty MSSubAlgebra of U2
the Sorts of F2 is Relation-like non-empty non empty-yielding 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
the Charact of U2 is Relation-like the carrier' of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Arity of S * ( the Sorts of U2 #), the ResultSort of S * the Sorts of U2
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 non empty total V18( the carrier' of S, the carrier of S * ) V41() V42() Element of K19(K20( the carrier' of S,( the carrier of S *)))
the carrier of S * is functional non empty V60() M8( the carrier of S)
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Sorts of U2 # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ( the Sorts of U2 #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S * the Sorts of U2 is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# the Sorts of U2, the Charact of U2 #) is strict non-empty MSAlgebra over S
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,U1,U2,F) is strict non-empty MSSubAlgebra of U2
F .:.: the Sorts of U1 is Relation-like the carrier of S -defined Function-like non empty total set
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-like set
K19(K20(( the Sorts of U1 . F2),( the Sorts of U2 . F2))) is set
F . F2 is Relation-like Function-like set
c₇ 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)))
proj2 c₇ is set
(F .:.: the Sorts of U1) . F2 is set
f is Relation-like Function-like set
f .: ( the Sorts of U1 . F2) is set
proj1 f is set
F2 is set
F . F2 is Relation-like Function-like set
proj2 (F . F2) is set
the Sorts of U2 . F2 is set
c₇ is Element of the carrier of S
the Sorts of U1 . c₇ is non empty set
the Sorts of U2 . c₇ is non empty set
K20(( the Sorts of U1 . c₇),( the Sorts of U2 . c₇)) is Relation-like set
K19(K20(( the Sorts of U1 . c₇),( the Sorts of U2 . c₇))) is set
( the carrier of S, the Sorts of U1, the Sorts of U2,F,c₇) is Relation-like the Sorts of U1 . c₇ -defined the Sorts of U2 . c₇ -valued Function-like non empty total V18( the Sorts of U1 . c₇, the Sorts of U2 . c₇) Element of K19(K20(( the Sorts of U1 . c₇),( the Sorts of U2 . c₇)))
f is Relation-like the Sorts of U1 . c₇ -defined the Sorts of U2 . c₇ -valued Function-like non empty total V18( the Sorts of U1 . c₇, the Sorts of U2 . c₇) Element of K19(K20(( the Sorts of U1 . c₇),( the Sorts of U2 . c₇)))
f .: ( the Sorts of U1 . c₇) is set
proj1 f is non empty 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 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) is strict non-empty MSSubAlgebra of U2
the Sorts of (S,U1,U2,F) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F1 is set
F . F1 is Relation-like Function-like set
the Sorts of U1 . F1 is set
the Sorts of (S,U1,U2,F) . F1 is set
K20(( the Sorts of U1 . F1),( the Sorts of (S,U1,U2,F) . F1)) is Relation-like set
K19(K20(( the Sorts of U1 . F1),( the Sorts of (S,U1,U2,F) . F1))) is set
the Sorts of U2 . F1 is set
K20(( the Sorts of U1 . F1),( the Sorts of U2 . F1)) is Relation-like set
K19(K20(( the Sorts of U1 . F1),( the Sorts of U2 . F1))) is set
F2 is Relation-like the Sorts of U1 . F1 -defined the Sorts of U2 . F1 -valued Function-like V18( the Sorts of U1 . F1, the Sorts of U2 . F1) Element of K19(K20(( the Sorts of U1 . F1),( the Sorts of U2 . F1)))
proj1 F2 is set
F .:.: the Sorts of U1 is Relation-like the carrier of S -defined Function-like non empty total set
F2 .: ( the Sorts of U1 . F1) is set
proj2 F2 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 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) is strict non-empty MSSubAlgebra of U2
the Sorts of (S,U1,U2,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 (S,U1,U2,F)
the carrier' of S is non empty set
h is Element of the carrier' of S
Args (h,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
the_result_sort_of h is Element of the carrier of S
( the carrier of S, the Sorts of U1, the Sorts of (S,U1,U2,F),F1,(the_result_sort_of h)) is Relation-like the Sorts of U1 . (the_result_sort_of h) -defined the Sorts of (S,U1,U2,F) . (the_result_sort_of h) -valued Function-like non empty total V18( the Sorts of U1 . (the_result_sort_of h), the Sorts of (S,U1,U2,F) . (the_result_sort_of h)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of h)),( the Sorts of (S,U1,U2,F) . (the_result_sort_of h))))
the Sorts of U1 . (the_result_sort_of h) is non empty set
the Sorts of (S,U1,U2,F) . (the_result_sort_of h) is non empty set
K20(( the Sorts of U1 . (the_result_sort_of h)),( the Sorts of (S,U1,U2,F) . (the_result_sort_of h))) is Relation-like set
K19(K20(( the Sorts of U1 . (the_result_sort_of h)),( the Sorts of (S,U1,U2,F) . (the_result_sort_of h)))) is set
Result (h,U1) is non empty Element of proj2 the Sorts of U1
proj2 the Sorts of U1 is non empty set
Den (h,U1) is Relation-like Args (h,U1) -defined Result (h,U1) -valued Function-like non empty total V18( Args (h,U1), Result (h,U1)) Element of K19(K20((Args (h,U1)),(Result (h,U1))))
K20((Args (h,U1)),(Result (h,U1))) is Relation-like set
K19(K20((Args (h,U1)),(Result (h,U1)))) is set
Args (h,(S,U1,U2,F)) is functional non empty Element of proj2 ( the Sorts of (S,U1,U2,F) #)
the Sorts of (S,U1,U2,F) # is Relation-like the carrier of S * -defined Function-like non empty total set
proj2 ( the Sorts of (S,U1,U2,F) #) is non empty set
Result (h,(S,U1,U2,F)) is non empty Element of proj2 the Sorts of (S,U1,U2,F)
proj2 the Sorts of (S,U1,U2,F) is non empty set
Den (h,(S,U1,U2,F)) is Relation-like Args (h,(S,U1,U2,F)) -defined Result (h,(S,U1,U2,F)) -valued Function-like non empty total V18( Args (h,(S,U1,U2,F)), Result (h,(S,U1,U2,F))) Element of K19(K20((Args (h,(S,U1,U2,F))),(Result (h,(S,U1,U2,F)))))
K20((Args (h,(S,U1,U2,F))),(Result (h,(S,U1,U2,F)))) is Relation-like set
K19(K20((Args (h,(S,U1,U2,F))),(Result (h,(S,U1,U2,F))))) is set
G1 is Relation-like Function-like Element of Args (h,U1)
(Den (h,U1)) . G1 is Element of Result (h,U1)
( the carrier of S, the Sorts of U1, the Sorts of (S,U1,U2,F),F1,(the_result_sort_of h)) . ((Den (h,U1)) . G1) is set
(S,U1,(S,U1,U2,F),h,F1,G1) is Relation-like Function-like Element of Args (h,(S,U1,U2,F))
(Den (h,(S,U1,U2,F))) . (S,U1,(S,U1,U2,F),h,F1,G1) is Element of Result (h,(S,U1,U2,F))
the_arity_of h is Relation-like NAT -defined the carrier of S -valued Function-like V28() countable V58() V59() Element of the carrier of S *
c₇ is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total ManySortedSubset of the Sorts of U2
(the_arity_of h) * c₇ is Relation-like non-empty NAT -defined Function-like set
(the_arity_of h) * the Sorts of U2 is Relation-like non-empty NAT -defined Function-like set
Den (h,U2) is Relation-like Args (h,U2) -defined Result (h,U2) -valued Function-like non empty total V18( Args (h,U2), Result (h,U2)) Element of K19(K20((Args (h,U2)),(Result (h,U2))))
Args (h,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
Result (h,U2) is non empty Element of proj2 the Sorts of U2
proj2 the Sorts of U2 is non empty set
K20((Args (h,U2)),(Result (h,U2))) is Relation-like set
K19(K20((Args (h,U2)),(Result (h,U2)))) is set
proj1 (Den (h,U2)) is non empty set
proj2 (the_arity_of h) is set
proj1 c₇ is non empty set
proj1 ((the_arity_of h) * c₇) is set
dom (the_arity_of h) is countable Element of K19(NAT)
proj1 the Sorts of U2 is non empty set
proj1 ((the_arity_of h) * the Sorts of U2) is set
a is set
((the_arity_of h) * c₇) . a is set
((the_arity_of h) * the Sorts of U2) . a is set
(the_arity_of h) . a is set
n is Element of the carrier of S
( the carrier of S, the Sorts of U1, the Sorts of U2,F,n) is Relation-like the Sorts of U1 . n -defined the Sorts of U2 . n -valued Function-like non empty total V18( the Sorts of U1 . n, the Sorts of U2 . n) Element of K19(K20(( the Sorts of U1 . n),( the Sorts of U2 . n)))
the Sorts of U1 . n is non empty set
the Sorts of U2 . n is non empty set
K20(( the Sorts of U1 . n),( the Sorts of U2 . n)) is Relation-like set
K19(K20(( the Sorts of U1 . n),( the Sorts of U2 . n))) is set
proj1 ( the carrier of S, the Sorts of U1, the Sorts of U2,F,n) is non empty set
proj2 ( the carrier of S, the Sorts of U1, the Sorts of U2,F,n) is non empty set
F .:.: the Sorts of U1 is Relation-like the carrier of S -defined Function-like non empty total set
(F .:.: the Sorts of U1) . n is set
( the carrier of S, the Sorts of U1, the Sorts of U2,F,n) .: ( the Sorts of U1 . n) is set
proj1 G1 is set
a is set
n is V21() V22() V23() V27() set
(S,U1,(S,U1,U2,F),h,F1,G1) . n is set
(the_arity_of h) /. n is Element of the carrier of S
( the carrier of S, the Sorts of U1, the Sorts of (S,U1,U2,F),F1,((the_arity_of h) /. n)) is Relation-like the Sorts of U1 . ((the_arity_of h) /. n) -defined the Sorts of (S,U1,U2,F) . ((the_arity_of h) /. n) -valued Function-like non empty total V18( the Sorts of U1 . ((the_arity_of h) /. n), the Sorts of (S,U1,U2,F) . ((the_arity_of h) /. n)) Element of K19(K20(( the Sorts of U1 . ((the_arity_of h) /. n)),( the Sorts of (S,U1,U2,F) . ((the_arity_of h) /. n))))
the Sorts of U1 . ((the_arity_of h) /. n) is non empty set
the Sorts of (S,U1,U2,F) . ((the_arity_of h) /. n) is non empty set
K20(( the Sorts of U1 . ((the_arity_of h) /. n)),( the Sorts of (S,U1,U2,F) . ((the_arity_of h) /. n))) is Relation-like set
K19(K20(( the Sorts of U1 . ((the_arity_of h) /. n)),( the Sorts of (S,U1,U2,F) . ((the_arity_of h) /. n)))) is set
G1 . n is set
( the carrier of S, the Sorts of U1, the Sorts of (S,U1,U2,F),F1,((the_arity_of h) /. n)) . (G1 . n) is set
(S,U1,(S,U1,U2,F),h,F1,G1) . a is 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,U1,U2,h,f,G1) is Relation-like Function-like Element of Args (h,U2)
(S,U1,U2,h,f,G1) . a is set
proj1 (S,U1,(S,U1,U2,F),h,F1,G1) is set
proj1 (S,U1,U2,h,f,G1) is set
(Den (h,U2)) . (S,U1,(S,U1,U2,F),h,F1,G1) is set
product ((the_arity_of h) * c₇) is functional non empty with_common_domain product-like set
product ((the_arity_of h) * the Sorts of U2) is functional non empty with_common_domain product-like set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) V41() V42() 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
c₇ # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * (c₇ #) is Relation-like the carrier' of S -defined Function-like non empty total set
( the Arity of S * (c₇ #)) . h is set
(proj1 (Den (h,U2))) /\ (Args (h,(S,U1,U2,F))) is set
the Charact of (S,U1,U2,F) is Relation-like the carrier' of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Arity of S * ( the Sorts of (S,U1,U2,F) #), the ResultSort of S * the Sorts of (S,U1,U2,F)
the Arity of S * ( the Sorts of (S,U1,U2,F) #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S * the Sorts of (S,U1,U2,F) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
Opers (U2,c₇) is Relation-like the carrier' of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Arity of S * (c₇ #), the ResultSort of S * c₇
the ResultSort of S * c₇ is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the carrier' of S,( the Arity of S * (c₇ #)),( the ResultSort of S * c₇),(Opers (U2,c₇)),h) is Relation-like ( the Arity of S * (c₇ #)) . h -defined ( the ResultSort of S * c₇) . h -valued Function-like total V18(( the Arity of S * (c₇ #)) . h,( the ResultSort of S * c₇) . h) Element of K19(K20((( the Arity of S * (c₇ #)) . h),(( the ResultSort of S * c₇) . h)))
( the ResultSort of S * c₇) . h is non empty set
K20((( the Arity of S * (c₇ #)) . h),(( the ResultSort of S * c₇) . h)) is Relation-like set
K19(K20((( the Arity of S * (c₇ #)) . h),(( the ResultSort of S * c₇) . h))) is set
h /. c₇ is Relation-like ( the Arity of S * (c₇ #)) . h -defined ( the ResultSort of S * c₇) . h -valued Function-like total V18(( the Arity of S * (c₇ #)) . h,( the ResultSort of S * c₇) . h) Element of K19(K20((( the Arity of S * (c₇ #)) . h),(( the ResultSort of S * c₇) . h)))
(Den (h,U2)) | (( the Arity of S * (c₇ #)) . h) is Relation-like Args (h,U2) -defined ( the Arity of S * (c₇ #)) . h -defined Args (h,U2) -defined Result (h,U2) -valued Function-like Element of K19(K20((Args (h,U2)),(Result (h,U2))))
F2 is set
F1 . F2 is Relation-like Function-like set
proj2 (F1 . F2) is set
the Sorts of (S,U1,U2,F) . F2 is set
c₇ is Element of the carrier of S
( the carrier of S, the Sorts of U1, the Sorts of (S,U1,U2,F),F1,c₇) is Relation-like the Sorts of U1 . c₇ -defined the Sorts of (S,U1,U2,F) . c₇ -valued Function-like non empty total V18( the Sorts of U1 . c₇, the Sorts of (S,U1,U2,F) . c₇) Element of K19(K20(( the Sorts of U1 . c₇),( the Sorts of (S,U1,U2,F) . c₇)))
the Sorts of U1 . c₇ is non empty set
the Sorts of (S,U1,U2,F) . c₇ is non empty set
K20(( the Sorts of U1 . c₇),( the Sorts of (S,U1,U2,F) . c₇)) is Relation-like set
K19(K20(( the Sorts of U1 . c₇),( the Sorts of (S,U1,U2,F) . c₇))) is set
F1 .:.: 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, the Sorts of (S,U1,U2,F),F1,c₇) .: ( the Sorts of U1 . c₇) is set
proj1 ( the carrier of S, the Sorts of U1, the Sorts of (S,U1,U2,F),F1,c₇) is non empty 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 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) is strict non-empty MSSubAlgebra of U2
the Sorts of (S,U1,U2,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 (S,U1,U2,F)
S is non empty non void V56() ManySortedSign
the carrier of S is non empty set
U2 is non-empty MSAlgebra over S
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
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 MSSubAlgebra of U2
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 U1, the Sorts of F
the carrier' of S is non empty 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
the_result_sort_of f is Element of the carrier of S
( the carrier of S, the Sorts of U1, the Sorts of U2,F1,(the_result_sort_of f)) is Relation-like the Sorts of U1 . (the_result_sort_of f) -defined the Sorts of U2 . (the_result_sort_of f) -valued Function-like non empty total V18( the Sorts of U1 . (the_result_sort_of f), the Sorts of U2 . (the_result_sort_of f)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of f)),( the Sorts of U2 . (the_result_sort_of f))))
the Sorts of U1 . (the_result_sort_of f) is non empty set
the Sorts of U2 . (the_result_sort_of f) is non empty set
K20(( the Sorts of U1 . (the_result_sort_of f)),( the Sorts of U2 . (the_result_sort_of f))) is Relation-like set
K19(K20(( the Sorts of U1 . (the_result_sort_of f)),( the Sorts of U2 . (the_result_sort_of f)))) is set
Result (f,U1) is non empty Element of proj2 the Sorts of U1
proj2 the Sorts of U1 is non empty set
Den (f,U1) is Relation-like Args (f,U1) -defined Result (f,U1) -valued Function-like non empty total V18( Args (f,U1), Result (f,U1)) Element of K19(K20((Args (f,U1)),(Result (f,U1))))
K20((Args (f,U1)),(Result (f,U1))) is Relation-like set
K19(K20((Args (f,U1)),(Result (f,U1)))) is 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
Result (f,U2) is non empty Element of proj2 the Sorts of U2
proj2 the Sorts of U2 is non empty set
Den (f,U2) is Relation-like Args (f,U2) -defined Result (f,U2) -valued Function-like non empty total V18( Args (f,U2), Result (f,U2)) Element of K19(K20((Args (f,U2)),(Result (f,U2))))
K20((Args (f,U2)),(Result (f,U2))) is Relation-like set
K19(K20((Args (f,U2)),(Result (f,U2)))) is set
h is Relation-like Function-like Element of Args (f,U1)
(Den (f,U1)) . h is Element of Result (f,U1)
( the carrier of S, the Sorts of U1, the Sorts of U2,F1,(the_result_sort_of f)) . ((Den (f,U1)) . h) is set
(S,U1,U2,f,F1,h) is Relation-like Function-like Element of Args (f,U2)
(Den (f,U2)) . (S,U1,U2,f,F1,h) is Element of Result (f,U2)
a is set
F2 . 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 Relation-like set
K19(K20(( the Sorts of U1 . a),( the Sorts of U2 . a))) is set
the Sorts of F . a is set
K20(( the Sorts of U1 . a),( the Sorts of F . a)) is Relation-like set
K19(K20(( the Sorts of U1 . a),( the Sorts of F . a))) is set
G1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total ManySortedSubset of the Sorts of U2
G1 . a is set
n is Relation-like the Sorts of U1 . a -defined the Sorts of F . a -valued Function-like V18( the Sorts of U1 . a, the Sorts of F . a) Element of K19(K20(( the Sorts of U1 . a),( the Sorts of F . a)))
c₇ is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total ManySortedSubset of the Sorts of U2
the Charact of F is Relation-like the carrier' of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Arity of S * ( the Sorts of F #), the ResultSort of S * the Sorts of F
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like non empty total V18( the carrier' of S, the carrier of S * ) V41() V42() Element of K19(K20( the carrier' of S,( the carrier of S *)))
K20( the carrier' of S,( the carrier of S *)) is Relation-like set
K19(K20( the carrier' of S,( the carrier of S *))) is set
the Sorts of F # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ( the Sorts of F #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of K19(K20( the carrier' of S, the carrier of S))
K20( the carrier' of S, the carrier of S) is Relation-like set
K19(K20( the carrier' of S, the carrier of S)) is set
the ResultSort of S * the Sorts of F is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
Opers (U2,c₇) is Relation-like the carrier' of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Arity of S * (c₇ #), the ResultSort of S * c₇
c₇ # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * (c₇ #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S * c₇ is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
Den (f,F) is Relation-like Args (f,F) -defined Result (f,F) -valued Function-like non empty total V18( Args (f,F), Result (f,F)) Element of K19(K20((Args (f,F)),(Result (f,F))))
Args (f,F) is functional non empty Element of proj2 ( the Sorts of F #)
proj2 ( the Sorts of F #) is non empty set
Result (f,F) is non empty Element of proj2 the Sorts of F
proj2 the Sorts of F is non empty set
K20((Args (f,F)),(Result (f,F))) is Relation-like set
K19(K20((Args (f,F)),(Result (f,F)))) is set
( the carrier' of S,( the Arity of S * (c₇ #)),( the ResultSort of S * c₇),(Opers (U2,c₇)),f) is Relation-like ( the Arity of S * (c₇ #)) . f -defined ( the ResultSort of S * c₇) . f -valued Function-like total V18(( the Arity of S * (c₇ #)) . f,( the ResultSort of S * c₇) . f) Element of K19(K20((( the Arity of S * (c₇ #)) . f),(( the ResultSort of S * c₇) . f)))
( the Arity of S * (c₇ #)) . f is set
( the ResultSort of S * c₇) . f is non empty set
K20((( the Arity of S * (c₇ #)) . f),(( the ResultSort of S * c₇) . f)) is Relation-like set
K19(K20((( the Arity of S * (c₇ #)) . f),(( the ResultSort of S * c₇) . f))) is set
f /. c₇ is Relation-like ( the Arity of S * (c₇ #)) . f -defined ( the ResultSort of S * c₇) . f -valued Function-like total V18(( the Arity of S * (c₇ #)) . f,( the ResultSort of S * c₇) . f) Element of K19(K20((( the Arity of S * (c₇ #)) . f),(( the ResultSort of S * c₇) . f)))
(Den (f,U2)) | (( the Arity of S * (c₇ #)) . f) is Relation-like Args (f,U2) -defined ( the Arity of S * (c₇ #)) . f -defined Args (f,U2) -defined Result (f,U2) -valued Function-like Element of K19(K20((Args (f,U2)),(Result (f,U2))))
proj1 h 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 *
dom (the_arity_of f) is countable Element of K19(NAT)
a is set
(S,U1,F,f,F2,h) is Relation-like Function-like Element of Args (f,F)
n is V21() V22() V23() V27() set
(S,U1,F,f,F2,h) . n is set
(the_arity_of f) /. n is Element of the carrier of S
( the carrier of S, the Sorts of U1, the Sorts of F,F2,((the_arity_of f) /. n)) is Relation-like the Sorts of U1 . ((the_arity_of f) /. n) -defined the Sorts of F . ((the_arity_of f) /. n) -valued Function-like non empty total V18( the Sorts of U1 . ((the_arity_of f) /. n), the Sorts of F . ((the_arity_of f) /. n)) Element of K19(K20(( the Sorts of U1 . ((the_arity_of f) /. n)),( the Sorts of F . ((the_arity_of f) /. n))))
the Sorts of U1 . ((the_arity_of f) /. n) is non empty set
the Sorts of F . ((the_arity_of f) /. n) is non empty set
K20(( the Sorts of U1 . ((the_arity_of f) /. n)),( the Sorts of F . ((the_arity_of f) /. n))) is Relation-like set
K19(K20(( the Sorts of U1 . ((the_arity_of f) /. n)),( the Sorts of F . ((the_arity_of f) /. n)))) is set
h . n is set
( the carrier of S, the Sorts of U1, the Sorts of F,F2,((the_arity_of f) /. n)) . (h . n) is set
(S,U1,F,f,F2,h) . a is set
G1 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,G1,h) is Relation-like Function-like Element of Args (f,U2)
(S,U1,U2,f,G1,h) . a is set
proj1 (S,U1,F,f,F2,h) is set
proj1 (S,U1,U2,f,G1,h) is set
proj1 (Den (f,U2)) is non empty set
(proj1 (Den (f,U2))) /\ (Args (f,F)) is set
(Den (f,F)) . (S,U1,U2,f,F1,h) 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 MSSubAlgebra of U1
the Sorts of U2 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total 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
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
F2 is set
F . F2 is Relation-like Function-like set
the Sorts of U2 . F2 is set
K20(( the Sorts of U2 . F2),( the Sorts of U2 . F2)) is Relation-like set
K19(K20(( the Sorts of U2 . F2),( the Sorts of U2 . F2))) is set
( the carrier of S, the Sorts of U2) . F2 is Relation-like Function-like set
c₇ is Relation-like the Sorts of U2 . F2 -defined the Sorts of U2 . F2 -valued Function-like total V18( the Sorts of U2 . F2, the Sorts of U2 . F2) Element of K19(K20(( the Sorts of U2 . F2),( the Sorts of U2 . F2)))
id ( the Sorts of U2 . F2) is Relation-like the Sorts of U2 . F2 -defined the Sorts of U2 . F2 -valued Function-like one-to-one total V18( the Sorts of U2 . F2, the Sorts of U2 . F2) Element of K19(K20(( the Sorts of U2 . F2),( the Sorts of U2 . F2)))
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
(S,U1,U2,F) is strict non-empty MSSubAlgebra of U2
the Sorts of (S,U1,U2,F) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F2 is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of (S,U1,U2,F), the Sorts of (S,U1,U2,F)
c₇ is set
F2 . c₇ is Relation-like Function-like set
the Sorts of (S,U1,U2,F) . c₇ is set
the Sorts of U2 . c₇ is set
K20(( the Sorts of (S,U1,U2,F) . c₇),( the Sorts of U2 . c₇)) is Relation-like set
K19(K20(( the Sorts of (S,U1,U2,F) . c₇),( the Sorts of U2 . c₇))) is set
the Sorts of U1 . c₇ is set
K20(( the Sorts of U1 . c₇),( the Sorts of U2 . c₇)) is Relation-like set
K19(K20(( the Sorts of U1 . c₇),( the Sorts of U2 . c₇))) is set
F . c₇ is Relation-like Function-like set
f is Relation-like the Sorts of U1 . c₇ -defined the Sorts of U2 . c₇ -valued Function-like V18( the Sorts of U1 . c₇, the Sorts of U2 . c₇) Element of K19(K20(( the Sorts of U1 . c₇),( the Sorts of U2 . c₇)))
proj1 f is set
K20(( the Sorts of (S,U1,U2,F) . c₇),( the Sorts of (S,U1,U2,F) . c₇)) is Relation-like set
K19(K20(( the Sorts of (S,U1,U2,F) . c₇),( the Sorts of (S,U1,U2,F) . c₇))) is set
proj2 f is set
F .:.: the Sorts of U1 is Relation-like the carrier of S -defined Function-like non empty total set
f .: ( the Sorts of U1 . c₇) is set
h is Relation-like the Sorts of (S,U1,U2,F) . c₇ -defined the Sorts of (S,U1,U2,F) . c₇ -valued Function-like total V18( the Sorts of (S,U1,U2,F) . c₇, the Sorts of (S,U1,U2,F) . c₇) Element of K19(K20(( the Sorts of (S,U1,U2,F) . c₇),( the Sorts of (S,U1,U2,F) . c₇)))
( the carrier of S, the Sorts of (S,U1,U2,F)) is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of (S,U1,U2,F), the Sorts of (S,U1,U2,F)
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 (S,U1,U2,F)
F2 is Relation-like the carrier of S -defined Function-like non empty total V41() V42() ManySortedFunction of the Sorts of (S,U1,U2,F), the Sorts of U2
( the carrier of S, the Sorts of U1, the Sorts of (S,U1,U2,F), the Sorts of U2,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 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 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₇ is Relation-like Function-like set
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
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)
h is V21() V22() V23() V27() set
proj1 c₇ is set
f . h 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 *
(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
c₇ . h is set
( the carrier of S, the Sorts of U1, the Sorts of U2,F1,((the_arity_of F) /. h)) . (c₇ . h) is set