:: OSALG_3 semantic presentation

K125() is Element of K19(K121())

K121() is set

K19(K121()) is set

K87() is set

K19(K87()) is set

K19(K125()) is set

{} is Relation-like non-empty empty-yielding K125() -defined Function-like one-to-one constant functional empty V28() V36() V37() FinSequence-like FinSubsequence-like FinSequence-membered set

1 is non empty set

{{},1} is non empty set

2 is non empty set

3 is non empty set

S1 is non empty V98() V99() V100() RelStr

the carrier of S1 is non empty set

S1 is non empty V98() V99() V100() RelStr

the carrier of S1 is non empty set

U1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() set

U2 is Element of the carrier of S1

F is Element of the carrier of S1

U1 . U2 is Relation-like Function-like set

dom (U1 . U2) is set

U1 . F is Relation-like Function-like set

dom (U1 . F) is set

O1 is set

O1 is set

O2 is set

[O1,O2] is set

{O1,O2} is non empty set

{O1} is non empty set

{{O1,O2},{O1}} is non empty set

(U1 . U2) . O1 is set

(U1 . F) . O1 is set

S1 is non empty V98() V99() V100() RelStr

the carrier of S1 is non empty set

U1 is Relation-like the carrier of S1 -defined Function-like non empty total order-sorted set

U2 is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total order-sorted set

F is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of U1,U2

O1 is Element of the carrier of S1

O2 is Element of the carrier of S1

F1 is set

U1 . O1 is set

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

U2 . O1 is non empty set

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

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

dom (F . O1) is Element of K19((U1 . O1))

K19((U1 . O1)) is set

(F . O1) . F1 is set

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

U1 . O2 is set

U2 . O2 is non empty set

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

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

(F . O2) . F1 is set

O1 is Element of the carrier of S1

O2 is Element of the carrier of S1

F . O1 is Relation-like Function-like set

dom (F . O1) is set

F . O2 is Relation-like Function-like set

dom (F . O2) is set

U1 . O1 is set

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

U2 . O1 is non empty set

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

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

dom (F . O1) is Element of K19((U1 . O1))

K19((U1 . O1)) is set

U1 . O2 is set

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

U2 . O2 is non empty set

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

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

dom (F . O2) is Element of K19((U1 . O2))

K19((U1 . O2)) is set

F1 is set

(F . O1) . F1 is set

(F . O2) . F1 is set

(F . O1) . F1 is set

(F . O2) . F1 is set

S1 is non empty V98() V99() V100() RelStr

the carrier of S1 is non empty set

the carrier of S1 * is functional non empty FinSequence-membered M8( the carrier of S1)

U1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() set

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

U2 is Relation-like K125() -defined the carrier of S1 -valued Function-like V28() FinSequence-like FinSubsequence-like Element of the carrier of S1 *

F is Relation-like K125() -defined the carrier of S1 -valued Function-like V28() FinSequence-like FinSubsequence-like Element of the carrier of S1 *

(U1 #) . U2 is set

(U1 #) . F is set

len U2 is Element of K125()

len F is Element of K125()

dom U2 is Element of K19(K125())

dom F is Element of K19(K125())

U2 * U1 is Relation-like K125() -defined Function-like V28() V36() V37() FinSequence-like FinSubsequence-like set

product (U2 * U1) is set

F1 is set

dom (U2 * U1) is Element of K19(K125())

F2 is Relation-like Function-like set

dom F2 is set

dom U1 is non empty Element of K19( the carrier of S1)

K19( the carrier of S1) is set

rng F is Element of K19( the carrier of S1)

F * U1 is Relation-like K125() -defined Function-like V28() V36() V37() FinSequence-like FinSubsequence-like set

dom (F * U1) is Element of K19(K125())

rng U2 is Element of K19( the carrier of S1)

o2 is set

F2 . o2 is set

(F * U1) . o2 is Relation-like Function-like set

F . o2 is set

U1 . (F . o2) is Relation-like Function-like set

U2 . o2 is set

s1 is Element of the carrier of S1

s2 is Element of the carrier of S1

U1 . s1 is Relation-like Function-like set

U1 . s2 is Relation-like Function-like set

(U2 * U1) . o2 is Relation-like Function-like set

U1 . (U2 . o2) is Relation-like Function-like set

product (F * U1) is set

S1 is non empty V98() V99() V100() RelStr

the carrier of S1 is non empty set

U1 is Relation-like the carrier of S1 -defined Function-like non empty total order-sorted set

id U1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of U1,U1

F is Element of the carrier of S1

O1 is Element of the carrier of S1

(id U1) . F is Relation-like Function-like set

dom ((id U1) . F) is set

(id U1) . O1 is Relation-like Function-like set

dom ((id U1) . O1) is set

U1 . F is set

U1 . O1 is set

O2 is set

((id U1) . F) . O2 is set

((id U1) . O1) . O2 is set

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

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

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

dom ((id U1) . F) is Element of K19((U1 . F))

K19((U1 . F)) is set

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

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

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

dom ((id U1) . O1) is Element of K19((U1 . O1))

K19((U1 . O1)) is set

((id U1) . F) . O2 is set

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

(id (U1 . F)) . O2 is set

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

(id (U1 . O1)) . O2 is set

((id U1) . O1) . O2 is set

S1 is non empty V98() V99() V100() RelStr

the carrier of S1 is non empty set

U1 is Relation-like the carrier of S1 -defined Function-like non empty total order-sorted set

id U1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of U1,U1

S1 is non empty V98() V99() V100() RelStr

the carrier of S1 is non empty set

U1 is Relation-like the carrier of S1 -defined Function-like non empty total order-sorted set

U2 is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total order-sorted set

F is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total order-sorted set

O1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of U1,U2

O2 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of U2,F

O2 ** O1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of U1,F

F1 is Element of the carrier of S1

F2 is Element of the carrier of S1

U1 . F1 is set

(O2 ** O1) . F1 is Relation-like U1 . F1 -defined F . F1 -valued Function-like V18(U1 . F1,F . F1) Element of K19(K20((U1 . F1),(F . F1)))

F . F1 is non empty set

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

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

(O2 ** O1) . F2 is Relation-like U1 . F2 -defined F . F2 -valued Function-like V18(U1 . F2,F . F2) Element of K19(K20((U1 . F2),(F . F2)))

U1 . F2 is set

F . F2 is non empty set

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

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

o2 is set

((O2 ** O1) . F1) . o2 is set

((O2 ** O1) . F2) . o2 is set

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

U2 . F1 is non empty set

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

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

(O1 . F1) . o2 is set

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

U2 . F2 is non empty set

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

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

(O1 . F2) . o2 is set

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

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

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

(O2 . F1) . ((O1 . F2) . o2) is set

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

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

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

(O2 . F2) . ((O1 . F2) . o2) is set

(O2 . F1) * (O1 . F1) is Relation-like U1 . F1 -defined F . F1 -valued Function-like Element of K19(K20((U1 . F1),(F . F1)))

((O2 . F1) * (O1 . F1)) . o2 is set

(O2 . F2) * (O1 . F2) is Relation-like U1 . F2 -defined F . F2 -valued Function-like Element of K19(K20((U1 . F2),(F . F2)))

((O2 . F2) * (O1 . F2)) . o2 is set

S1 is non empty V98() V99() V100() RelStr

the carrier of S1 is non empty set

U1 is Relation-like the carrier of S1 -defined Function-like non empty total order-sorted set

U2 is Relation-like the carrier of S1 -defined Function-like non empty total order-sorted set

F is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of U1,U2

F "" is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of U2,U1

O1 is Element of the carrier of S1

O2 is Element of the carrier of S1

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

dom ((F "") . O1) is set

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

dom ((F "") . O2) is set

U2 . O1 is set

U2 . O2 is set

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

U1 . O2 is set

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

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

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

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

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

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

U1 . O1 is set

dom F is non empty Element of K19( the carrier of S1)

K19( the carrier of S1) is set

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

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

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

F1 is set

((F "") . O1) . F1 is set

((F "") . O2) . F1 is set

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

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

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

dom ((F "") . O1) is Element of K19((U2 . O1))

K19((U2 . O1)) is set

dom (F . O2) is Element of K19((U1 . O2))

K19((U1 . O2)) is set

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

((F . O1) ") . F1 is set

((F . O2) ") . F1 is set

dom (F . O1) is Element of K19((U1 . O1))

K19((U1 . O1)) is set

rng ((F . O1) ") is set

rng (F . O1) is Element of K19((U2 . O1))

rng (F . O2) is Element of K19((U2 . O2))

K19((U2 . O2)) is set

(F . O2) . (((F . O2) ") . F1) is set

(F . O1) . (((F . O1) ") . F1) is set

(F . O2) . (((F . O1) ") . F1) is set

dom ((F "") . O2) is Element of K19((U2 . O2))

S1 is non empty V98() V99() V100() RelStr

the carrier of S1 is non empty set

U1 is Relation-like the carrier of S1 -defined Function-like non empty total order-sorted set

U2 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() set

U2 .:.: U1 is Relation-like the carrier of S1 -defined Function-like non empty total set

F is Relation-like the carrier of S1 -defined Function-like non empty total set

O1 is Element of the carrier of S1

O2 is Element of the carrier of S1

F . O1 is set

F . O2 is set

U1 . O1 is set

U1 . O2 is set

U2 . O1 is Relation-like Function-like set

U2 . O2 is Relation-like Function-like set

(U2 . O1) .: (U1 . O1) is set

(U2 . O2) .: (U1 . O2) is set

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

U1 is order-sorted MSAlgebra over S1

the carrier of S1 is non empty set

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

id the Sorts of U1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of U1

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

U1 is non-empty order-sorted MSAlgebra over S1

U2 is non-empty order-sorted MSAlgebra over S1

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

the carrier of S1 is non empty set

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

F is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of U2

F "" is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U2, the Sorts of U1

O1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U2, the Sorts of U1

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

F is order-sorted MSAlgebra over S1

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

F is non-empty order-sorted MSAlgebra over S1

O1 is non-empty order-sorted MSAlgebra over S1

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

U1 is non-empty order-sorted MSAlgebra over S1

U2 is non-empty order-sorted MSAlgebra over S1

F is non-empty order-sorted MSAlgebra over S1

the carrier of S1 is non empty set

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

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

O1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() 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 S1 -defined Function-like non empty total set

O2 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U2, the Sorts of F

O2 ** O1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of F

F1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of F

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U1 is non-empty order-sorted MSAlgebra over S1

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

U2 is non-empty order-sorted MSAlgebra over S1

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

F is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of U2

Image F is strict non-empty MSSubAlgebra of U2

O1 is Relation-like the carrier of S1 -defined Function-like non empty total order-sorted set

F .:.: O1 is Relation-like the carrier of S1 -defined Function-like non empty total set

the Sorts of (Image F) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

the carrier' of S1 is non empty set

U1 is non-empty order-sorted MSAlgebra over S1

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

U2 is non-empty order-sorted MSAlgebra over S1

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

F is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of U2

O1 is Element of the carrier' of S1

O2 is Element of the carrier' of S1

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

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

the carrier of S1 * is functional non empty FinSequence-membered M8( the carrier of S1)

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

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

F1 is Relation-like K125() -defined Function-like V28() FinSequence-like FinSubsequence-like Element of Args (O1,U1)

F # F1 is Relation-like K125() -defined Function-like V28() FinSequence-like FinSubsequence-like Element of Args (O1,U2)

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

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

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

F2 is Relation-like K125() -defined Function-like V28() FinSequence-like FinSubsequence-like Element of Args (O2,U1)

F # F2 is Relation-like K125() -defined Function-like V28() FinSequence-like FinSubsequence-like Element of Args (O2,U2)

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

dom F1 is Element of K19(K125())

the_arity_of O1 is Relation-like K125() -defined the carrier of S1 -valued Function-like V28() FinSequence-like FinSubsequence-like Element of the carrier of S1 *

dom (the_arity_of O1) is Element of K19(K125())

o2 is set

(F # F1) . o2 is set

(F # F2) . o2 is set

s1 is V27() set

(the_arity_of O1) /. s1 is Element of the carrier of S1

the_arity_of O2 is Relation-like K125() -defined the carrier of S1 -valued Function-like V28() FinSequence-like FinSubsequence-like Element of the carrier of S1 *

(the_arity_of O2) /. s1 is Element of the carrier of S1

(the_arity_of O1) . s1 is set

len (the_arity_of O1) is Element of K125()

len (the_arity_of O2) is Element of K125()

dom (the_arity_of O2) is Element of K19(K125())

(the_arity_of O2) . s1 is set

s2 is Element of the carrier of S1

a is Element of the carrier of S1

rng (the_arity_of O1) is Element of K19( the carrier of S1)

K19( the carrier of S1) is set

dom the Sorts of U1 is non empty Element of K19( the carrier of S1)

(the_arity_of O1) * the Sorts of U1 is Relation-like non-empty K125() -defined Function-like V28() FinSequence-like FinSubsequence-like set

dom ((the_arity_of O1) * the Sorts of U1) is Element of K19(K125())

the Sorts of U1 . s2 is non empty set

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

the Sorts of U2 . s2 is non empty set

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

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

dom (F . s2) is Element of K19(( the Sorts of U1 . s2))

K19(( the Sorts of U1 . s2)) is set

the Sorts of U1 . ((the_arity_of O1) . s1) is set

((the_arity_of O1) * the Sorts of U1) . s1 is set

F2 . s1 is set

(F # F1) . s1 is set

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

the Sorts of U1 . ((the_arity_of O1) /. s1) is non empty set

the Sorts of U2 . ((the_arity_of O1) /. s1) is non empty set

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

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

(F . ((the_arity_of O1) /. s1)) . (F2 . s1) is set

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

the Sorts of U1 . a is non empty set

the Sorts of U2 . a is non empty 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

(F . a) . (F2 . s1) is set

(F # F2) . s1 is set

dom F2 is Element of K19(K125())

the_arity_of O2 is Relation-like K125() -defined the carrier of S1 -valued Function-like V28() FinSequence-like FinSubsequence-like Element of the carrier of S1 *

dom (the_arity_of O2) is Element of K19(K125())

dom (F # F2) is Element of K19(K125())

dom (F # F1) is Element of K19(K125())

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U1 is non-empty order-sorted monotone MSAlgebra over S1

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

U2 is non-empty order-sorted MSAlgebra over S1

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

F is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of U2

Image F is strict non-empty MSSubAlgebra of U2

O1 is Relation-like the carrier of S1 -defined Function-like non empty total order-sorted set

F .:.: O1 is Relation-like the carrier of S1 -defined Function-like non empty total set

the Sorts of (Image F) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

O2 is non-empty order-sorted MSAlgebra over S1

the Sorts of O2 is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

F1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of O2

the carrier' of S1 is non empty set

F2 is Element of the carrier' of S1

o2 is Element of the carrier' of S1

Args (F2,O2) is functional non empty Element of rng ( the Sorts of O2 #)

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

the carrier of S1 * is functional non empty FinSequence-membered M8( the carrier of S1)

rng ( the Sorts of O2 #) is non empty set

Result (F2,O2) is non empty Element of rng the Sorts of O2

rng the Sorts of O2 is non empty set

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

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

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

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

Args (o2,O2) is functional non empty Element of rng ( the Sorts of O2 #)

Result (o2,O2) is non empty Element of rng the Sorts of O2

K20((Args (o2,O2)),(Result (o2,O2))) is Relation-like set

K19(K20((Args (o2,O2)),(Result (o2,O2)))) is set

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

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

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

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

dom (Den (o2,O2)) is functional Element of K19((Args (o2,O2)))

K19((Args (o2,O2))) is set

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

rng the Sorts of U1 is non empty set

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

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

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

(Den (o2,U1)) | (Args (F2,U1)) is Relation-like Args (F2,U1) -defined Args (o2,U1) -defined Result (o2,U1) -valued Function-like Element of K19(K20((Args (o2,U1)),(Result (o2,U1))))

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

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

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

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

the_result_sort_of F2 is Element of the carrier of S1

the_result_sort_of o2 is Element of the carrier of S1

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

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

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

dom the ResultSort of S1 is Element of K19( the carrier' of S1)

K19( the carrier' of S1) is set

a is set

b is set

[a,b] is set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

y is Relation-like K125() -defined Function-like V28() FinSequence-like FinSubsequence-like Element of Args (F2,U1)

F1 # y is Relation-like K125() -defined Function-like V28() FinSequence-like FinSubsequence-like Element of Args (F2,O2)

y1 is Relation-like K125() -defined Function-like V28() FinSequence-like FinSubsequence-like Element of Args (o2,U1)

F1 # y1 is Relation-like K125() -defined Function-like V28() FinSequence-like FinSubsequence-like Element of Args (o2,O2)

(Den (o2,U1)) . y is set

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

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

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

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

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

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

(F1 . (the_result_sort_of F2)) . ((Den (F2,U1)) . y) is set

(Den (F2,O2)) . a is set

the ResultSort of S1 * O1 is Relation-like the carrier' of S1 -defined Function-like set

( the ResultSort of S1 * O1) . F2 is set

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

O1 . ( the ResultSort of S1 . F2) is set

O1 . (the_result_sort_of F2) is set

dom (F1 . (the_result_sort_of F2)) is Element of K19(( the Sorts of U1 . (the_result_sort_of F2)))

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

F1 . (the_result_sort_of o2) is Relation-like the Sorts of U1 . (the_result_sort_of o2) -defined the Sorts of O2 . (the_result_sort_of o2) -valued Function-like V18( the Sorts of U1 . (the_result_sort_of o2), the Sorts of O2 . (the_result_sort_of o2)) Element of K19(K20(( the Sorts of U1 . (the_result_sort_of o2)),( the Sorts of O2 . (the_result_sort_of o2))))

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

the Sorts of O2 . (the_result_sort_of o2) is non empty set

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

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

(F1 . (the_result_sort_of o2)) . ((Den (F2,U1)) . y) is set

(Den (o2,O2)) . a is set

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

U1 is order-sorted monotone MSAlgebra over S1

U2 is order-sorted MSSubAlgebra of U1

the carrier' of S1 is non empty set

F is Element of the carrier' of S1

O1 is Element of the carrier' of S1

Args (O1,U2) is Element of rng ( the Sorts of U2 #)

the carrier of S1 is non empty set

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

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

the carrier of S1 * is functional non empty FinSequence-membered M8( the carrier of S1)

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

Result (O1,U2) is Element of rng the Sorts of U2

rng the Sorts of U2 is non empty set

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

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

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

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

(Den (O1,U2)) | (Args (F,U2)) is Relation-like Args (O1,U2) -defined Args (F,U2) -defined Args (O1,U2) -defined Result (O1,U2) -valued Function-like Element of K19(K20((Args (O1,U2)),(Result (O1,U2))))

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

Result (F,U2) is Element of rng the Sorts of U2

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

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

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

O2 is Relation-like the carrier of S1 -defined Function-like non empty total OSSubset of U1

the Charact of U2 is Relation-like the carrier' of S1 -defined Function-like non empty total ManySortedFunction of the Arity of S1 * ( the Sorts of U2 #), the ResultSort of S1 * the Sorts of U2

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

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

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

the Arity of S1 * ( the Sorts of U2 #) is Relation-like the carrier' of S1 -defined Function-like set

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

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

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

the ResultSort of S1 * the Sorts of U2 is Relation-like the carrier' of S1 -defined Function-like set

the Charact of U2 . O1 is set

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

O2 # is Relation-like the carrier of S1 * -defined Function-like non empty total set

the Arity of S1 * (O2 #) is Relation-like the carrier' of S1 -defined Function-like set

the ResultSort of S1 * O2 is Relation-like the carrier' of S1 -defined Function-like set

(Opers (U1,O2)) . O1 is set

O1 /. O2 is Relation-like ( the Arity of S1 * (O2 #)) . O1 -defined ( the ResultSort of S1 * O2) . O1 -valued Function-like V18(( the Arity of S1 * (O2 #)) . O1,( the ResultSort of S1 * O2) . O1) Element of K19(K20((( the Arity of S1 * (O2 #)) . O1),(( the ResultSort of S1 * O2) . O1)))

( the Arity of S1 * (O2 #)) . O1 is set

( the ResultSort of S1 * O2) . O1 is set

K20((( the Arity of S1 * (O2 #)) . O1),(( the ResultSort of S1 * O2) . O1)) is Relation-like set

K19(K20((( the Arity of S1 * (O2 #)) . O1),(( the ResultSort of S1 * O2) . O1))) is set

Args (O1,U1) is Element of rng ( the Sorts of U1 #)

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

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

Result (O1,U1) is Element of rng the Sorts of U1

rng the Sorts of U1 is non empty set

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

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

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

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

(Den (O1,U1)) | (Args (O1,U2)) is Relation-like Args (O1,U2) -defined Args (O1,U1) -defined Result (O1,U1) -valued Function-like Element of K19(K20((Args (O1,U1)),(Result (O1,U1))))

the Charact of U2 . F is set

(Opers (U1,O2)) . F is set

F /. O2 is Relation-like ( the Arity of S1 * (O2 #)) . F -defined ( the ResultSort of S1 * O2) . F -valued Function-like V18(( the Arity of S1 * (O2 #)) . F,( the ResultSort of S1 * O2) . F) Element of K19(K20((( the Arity of S1 * (O2 #)) . F),(( the ResultSort of S1 * O2) . F)))

( the Arity of S1 * (O2 #)) . F is set

( the ResultSort of S1 * O2) . F is set

K20((( the Arity of S1 * (O2 #)) . F),(( the ResultSort of S1 * O2) . F)) is Relation-like set

K19(K20((( the Arity of S1 * (O2 #)) . F),(( the ResultSort of S1 * O2) . F))) is set

Args (F,U1) is Element of rng ( the Sorts of U1 #)

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

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

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

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

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

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

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

(Args (F,U1)) /\ (Args (F,U2)) is set

(Den (O1,U1)) | ((Args (F,U1)) /\ (Args (F,U2))) is Relation-like Args (O1,U1) -defined (Args (F,U1)) /\ (Args (F,U2)) -defined Args (O1,U1) -defined Result (O1,U1) -valued Function-like Element of K19(K20((Args (O1,U1)),(Result (O1,U1))))

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

(Args (O1,U2)) /\ (Args (F,U2)) is set

(Den (O1,U1)) | ((Args (O1,U2)) /\ (Args (F,U2))) is Relation-like Args (O1,U1) -defined (Args (O1,U2)) /\ (Args (F,U2)) -defined Args (O1,U1) -defined Result (O1,U1) -valued Function-like Element of K19(K20((Args (O1,U1)),(Result (O1,U1))))

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

U1 is order-sorted monotone MSAlgebra over S1

the order-sorted MSSubAlgebra of U1 is order-sorted MSSubAlgebra of U1

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

U1 is order-sorted monotone MSAlgebra over S1

U2 is order-sorted MSSubAlgebra of U1

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U1 is non-empty order-sorted MSAlgebra over S1

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

U2 is non-empty order-sorted MSAlgebra over S1

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

F is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of U2

Image F is strict non-empty MSSubAlgebra of U2

the Sorts of (Image F) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

O1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of (Image F)

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U1 is non-empty order-sorted MSAlgebra over S1

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

U2 is non-empty order-sorted MSAlgebra over S1

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

F is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of U2

Image F is strict non-empty MSSubAlgebra of U2

the Sorts of (Image F) is Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like non empty total set

O1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of (Image F), the Sorts of (Image F)

O2 is set

O1 . O2 is Relation-like Function-like set

the Sorts of (Image F) . O2 is set

the Sorts of U2 . O2 is set

K20(( the Sorts of (Image F) . O2),( the Sorts of U2 . O2)) is Relation-like set

K19(K20(( the Sorts of (Image F) . O2),( the Sorts of U2 . O2))) is set

the Sorts of U1 . O2 is set

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

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

F . O2 is Relation-like Function-like set

K20(( the Sorts of (Image F) . O2),( the Sorts of (Image F) . O2)) is Relation-like set

K19(K20(( the Sorts of (Image F) . O2),( the Sorts of (Image F) . O2))) is set

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

dom F1 is Element of K19(( the Sorts of U1 . O2))

K19(( the Sorts of U1 . O2)) is set

F .:.: the Sorts of U1 is Relation-like the carrier of S1 -defined Function-like non empty total set

F1 .: ( the Sorts of U1 . O2) is Element of K19(( the Sorts of U2 . O2))

K19(( the Sorts of U2 . O2)) is set

rng F1 is Element of K19(( the Sorts of U2 . O2))

F2 is Relation-like the Sorts of (Image F) . O2 -defined the Sorts of (Image F) . O2 -valued Function-like V18( the Sorts of (Image F) . O2, the Sorts of (Image F) . O2) Element of K19(K20(( the Sorts of (Image F) . O2),( the Sorts of (Image F) . O2)))

id the Sorts of (Image F) is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of (Image F), the Sorts of (Image F)

O2 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of (Image F)

O1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of (Image F), the Sorts of U2

O1 ** O2 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of U2

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

U1 is order-sorted MSAlgebra over S1

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

the carrier of S1 is non empty set

the Charact of U1 is Relation-like the carrier' of S1 -defined Function-like non empty total ManySortedFunction of the Arity of S1 * ( the Sorts of U1 #), the ResultSort of S1 * the Sorts of U1

the carrier' of S1 is non empty set

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

the carrier of S1 * is functional non empty FinSequence-membered M8( the carrier of S1)

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

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

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

the Arity of S1 * ( the Sorts of U1 #) is Relation-like the carrier' of S1 -defined Function-like set

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

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

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

the ResultSort of S1 * the Sorts of U1 is Relation-like the carrier' of S1 -defined Function-like set

MSAlgebra(# the Sorts of U1, the Charact of U1 #) is strict MSAlgebra over S1

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

U1 is order-sorted MSAlgebra over S1

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

the carrier of S1 is non empty set

the Charact of U1 is Relation-like the carrier' of S1 -defined Function-like non empty total ManySortedFunction of the Arity of S1 * ( the Sorts of U1 #), the ResultSort of S1 * the Sorts of U1

the carrier' of S1 is non empty set

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

the carrier of S1 * is functional non empty FinSequence-membered M8( the carrier of S1)

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

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

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

the Arity of S1 * ( the Sorts of U1 #) is Relation-like the carrier' of S1 -defined Function-like set

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

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

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

the ResultSort of S1 * the Sorts of U1 is Relation-like the carrier' of S1 -defined Function-like set

MSAlgebra(# the Sorts of U1, the Charact of U1 #) is strict order-sorted MSAlgebra over S1

F is Element of the carrier' of S1

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

Args (F,U1) is Element of rng ( the Sorts of U1 #)

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

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

rng 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

the Charact of MSAlgebra(# the Sorts of U1, the Charact of U1 #) is Relation-like the carrier' of S1 -defined Function-like non empty total ManySortedFunction of the Arity of S1 * ( the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) #), the ResultSort of S1 * the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #)

the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) is Relation-like the carrier of S1 -defined Function-like non empty total set

the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) # is Relation-like the carrier of S1 * -defined Function-like non empty total set

the Arity of S1 * ( the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) #) is Relation-like the carrier' of S1 -defined Function-like set

the ResultSort of S1 * the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) is Relation-like the carrier' of S1 -defined Function-like set

the Charact of MSAlgebra(# the Sorts of U1, the Charact of U1 #) . F is set

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

Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) is Element of rng ( the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) #)

rng ( the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) #) is non empty set

Result (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) is Element of rng the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #)

rng the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) is non empty set

K20((Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #)))) is Relation-like set

K19(K20((Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #))))) is set

( the Arity of S1 * ( the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) #)) . F is set

F is Element of the carrier' of S1

O1 is Element of the carrier' of S1

Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) is Element of rng ( the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) #)

Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) is Element of rng the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #)

Den (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) is Relation-like Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -defined Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -valued Function-like V18( Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)), Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) Element of K19(K20((Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)))))

K20((Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)))) is Relation-like set

K19(K20((Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))))) is set

Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) is Element of rng ( the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) #)

(Den (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) is Relation-like Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -defined Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -defined Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -defined Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -valued Function-like Element of K19(K20((Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)))))

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

Result (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) is Element of rng the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #)

K20((Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #)))) is Relation-like set

K19(K20((Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #))))) is set

Args (O1,U1) is Element of rng ( the Sorts of U1 #)

Result (O1,U1) is Element of rng the Sorts of U1

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

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

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

Args (F,U1) is Element of rng ( the Sorts of U1 #)

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

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 rng the Sorts of U1

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

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

(Den (O1,U1)) | (Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) is Relation-like Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -defined Args (O1,U1) -defined Result (O1,U1) -valued Function-like Element of K19(K20((Args (O1,U1)),(Result (O1,U1))))

F is Element of the carrier' of S1

O1 is Element of the carrier' of S1

Args (O1,U1) is Element of rng ( the Sorts of U1 #)

Result (O1,U1) is Element of rng the Sorts of U1

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

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

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

Args (F,U1) is Element of rng ( the Sorts of U1 #)

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

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 rng the Sorts of U1

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

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

Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) is Element of rng ( the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) #)

Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) is Element of rng the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #)

Den (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) is Relation-like Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -defined Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -valued Function-like V18( Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)), Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) Element of K19(K20((Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)))))

K20((Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)))) is Relation-like set

K19(K20((Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))))) is set

Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) is Element of rng ( the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) #)

(Den (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) is Relation-like Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -defined Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -defined Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -defined Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -valued Function-like Element of K19(K20((Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)))))

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

Result (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) is Element of rng the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #)

K20((Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #)))) is Relation-like set

K19(K20((Args (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (F,MSAlgebra(# the Sorts of U1, the Charact of U1 #))))) is set

(Den (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (F,U1)) is Relation-like Args (F,U1) -defined Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -defined Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) -valued Function-like Element of K19(K20((Args (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))),(Result (O1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)))))

S1 is non empty non void V51() V98() V99() V100() order-sorted discernable OverloadedRSSign

U1 is strict non-empty order-sorted MSAlgebra over S1

U2 is strict non-empty order-sorted MSAlgebra over S1

the carrier of S1 is non empty set

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

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

F is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U1, the Sorts of U2

O1 is Relation-like the carrier of S1 -defined Function-like non empty total order-sorted set

O2 is Relation-like the carrier of S1 -defined Function-like non empty total order-sorted set

F1 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of O1,O2

F1 "" is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of O2,O1

Image F is strict non-empty MSSubAlgebra of U2

F "" is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U2, the Sorts of U1

F2 is Relation-like the carrier of S1 -defined Function-like non empty total V36() V37() ManySortedFunction of the Sorts of U2, the Sorts of U1

Image F2 is strict non-empty MSSubAlgebra of U1