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