K162() is non empty V36() V37() V38() Element of K10(K158())
K158() is set
K10(K158()) is non empty set
K110() is non empty V36() V37() V38() set
K10(K110()) is non empty set
{} is empty Relation-like non-empty empty-yielding K162() -defined Function-like one-to-one constant functional V36() V37() V38() V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty set
{{},1} is non empty set
K10(K162()) is non empty set
K333() is set
K10(K333()) is non empty set
K334() is Element of K10(K333())
K381() is non empty V145() L11()
the carrier of K381() is non empty set
K337( the carrier of K381()) is non empty M32( the carrier of K381())
K380(K381()) is Element of K10(K337( the carrier of K381()))
K10(K337( the carrier of K381())) is non empty set
K11(K380(K381()),K162()) is Relation-like set
K10(K11(K380(K381()),K162())) is non empty set
K11(K162(),K380(K381())) is Relation-like set
K10(K11(K162(),K380(K381()))) is non empty set
2 is non empty set
3 is non empty set
S is set
w1 is Relation-like K162() -defined S -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of S
o is Relation-like S -defined Function-like V25(S) set
w1 * o is Relation-like K162() -defined Function-like set
rng w1 is Element of K10(S)
K10(S) is non empty set
dom o is Element of K10(S)
dom (w1 * o) is Element of K10(K162())
dom w1 is Element of K10(K162())
len w1 is V36() V37() V38() V42() Element of K162()
Seg (len w1) is V43() V50( len w1) Element of K10(K162())
S is set
o is Relation-like S -defined Function-like V25(S) set
w1 is Relation-like K162() -defined S -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of S
w1 * o is Relation-like K162() -defined Function-like V43() FinSequence-like FinSubsequence-like set
dom (w1 * o) is Element of K10(K162())
dom w1 is Element of K10(K162())
len (w1 * o) is V36() V37() V38() V42() Element of K162()
len w1 is V36() V37() V38() V42() Element of K162()
rng w1 is Element of K10(S)
K10(S) is non empty set
dom o is Element of K10(S)
lo is Relation-like K162() -defined Function-like V43() FinSequence-like FinSubsequence-like set
len lo is V36() V37() V38() V42() Element of K162()
S is non empty set
K11(S,S) is non empty Relation-like set
K10(K11(S,S)) is non empty set
S * is non empty functional FinSequence-membered M37(S)
o is non empty set
K11(o,o) is non empty Relation-like set
K10(K11(o,o)) is non empty set
K11(o,(S *)) is non empty Relation-like set
K10(K11(o,(S *))) is non empty set
K11(o,S) is non empty Relation-like set
K10(K11(o,S)) is non empty set
w1 is Relation-like S -defined S -valued reflexive antisymmetric transitive V25(S) Element of K10(K11(S,S))
lo is Relation-like o -defined o -valued reflexive symmetric transitive V25(o) Element of K10(K11(o,o))
op2 is Relation-like o -defined S * -valued Function-like V29(o,S * ) Element of K10(K11(o,(S *)))
op is Relation-like o -defined S -valued Function-like V29(o,S) Element of K10(K11(o,S))
(S,w1,o,lo,op2,op) is () ()
the InternalRel of (S,w1,o,lo,op2,op) is Relation-like the carrier of (S,w1,o,lo,op2,op) -defined the carrier of (S,w1,o,lo,op2,op) -valued Element of K10(K11( the carrier of (S,w1,o,lo,op2,op), the carrier of (S,w1,o,lo,op2,op)))
the carrier of (S,w1,o,lo,op2,op) is set
K11( the carrier of (S,w1,o,lo,op2,op), the carrier of (S,w1,o,lo,op2,op)) is Relation-like set
K10(K11( the carrier of (S,w1,o,lo,op2,op), the carrier of (S,w1,o,lo,op2,op))) is non empty set
field the InternalRel of (S,w1,o,lo,op2,op) is set
S is non empty set
K11(S,S) is non empty Relation-like set
K10(K11(S,S)) is non empty set
w1 is non empty set
K11(w1,w1) is non empty Relation-like set
K10(K11(w1,w1)) is non empty set
S * is non empty functional FinSequence-membered M37(S)
K11(w1,(S *)) is non empty Relation-like set
K10(K11(w1,(S *))) is non empty set
K11(w1,S) is non empty Relation-like set
K10(K11(w1,S)) is non empty set
o is Relation-like S -defined S -valued reflexive antisymmetric transitive V25(S) Element of K10(K11(S,S))
lo is Relation-like w1 -defined w1 -valued reflexive symmetric transitive V25(w1) Element of K10(K11(w1,w1))
op2 is Relation-like w1 -defined S * -valued Function-like V29(w1,S * ) Element of K10(K11(w1,(S *)))
op is Relation-like w1 -defined S -valued Function-like V29(w1,S) Element of K10(K11(w1,S))
(S,o,w1,lo,op2,op) is () ()
S is ()
the non empty set is non empty set
K11( the non empty set , the non empty set ) is non empty Relation-like set
K10(K11( the non empty set , the non empty set )) is non empty set
the Relation-like the non empty set -defined the non empty set -valued reflexive antisymmetric transitive V25( the non empty set ) Element of K10(K11( the non empty set , the non empty set )) is Relation-like the non empty set -defined the non empty set -valued reflexive antisymmetric transitive V25( the non empty set ) Element of K10(K11( the non empty set , the non empty set ))
the Relation-like the non empty set -defined the non empty set -valued reflexive symmetric transitive V25( the non empty set ) Element of K10(K11( the non empty set , the non empty set )) is Relation-like the non empty set -defined the non empty set -valued reflexive symmetric transitive V25( the non empty set ) Element of K10(K11( the non empty set , the non empty set ))
the non empty set * is non empty functional FinSequence-membered M37( the non empty set )
K11( the non empty set ,( the non empty set *)) is non empty Relation-like set
K10(K11( the non empty set ,( the non empty set *))) is non empty set
the Relation-like the non empty set -defined the non empty set * -valued Function-like V29( the non empty set , the non empty set * ) Element of K10(K11( the non empty set ,( the non empty set *))) is Relation-like the non empty set -defined the non empty set * -valued Function-like V29( the non empty set , the non empty set * ) Element of K10(K11( the non empty set ,( the non empty set *)))
the Relation-like the non empty set -defined the non empty set -valued Function-like V29( the non empty set , the non empty set ) Element of K10(K11( the non empty set , the non empty set )) is Relation-like the non empty set -defined the non empty set -valued Function-like V29( the non empty set , the non empty set ) Element of K10(K11( the non empty set , the non empty set ))
( the non empty set , the Relation-like the non empty set -defined the non empty set -valued reflexive antisymmetric transitive V25( the non empty set ) Element of K10(K11( the non empty set , the non empty set )), the non empty set , the Relation-like the non empty set -defined the non empty set -valued reflexive symmetric transitive V25( the non empty set ) Element of K10(K11( the non empty set , the non empty set )), the Relation-like the non empty set -defined the non empty set * -valued Function-like V29( the non empty set , the non empty set * ) Element of K10(K11( the non empty set ,( the non empty set *))), the Relation-like the non empty set -defined the non empty set -valued Function-like V29( the non empty set , the non empty set ) Element of K10(K11( the non empty set , the non empty set ))) is non empty V64() reflexive transitive antisymmetric () ()
the non empty non void V64() () is non empty non void V64() ()
S is non empty non void V64() ()
the carrier' of S is non empty set
the of S is Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric transitive V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
lo is Element of the carrier' of S
op2 is Element of the carrier' of S
[lo,op2] is set
{lo,op2} is non empty set
{lo} is non empty set
{{lo,op2},{lo}} is non empty set
[op2,lo] is set
{op2,lo} is non empty set
{op2} is non empty set
{{op2,lo},{op2}} is non empty set
field the of S is set
lo is Element of the carrier' of S
[lo,lo] is set
{lo,lo} is non empty set
{lo} is non empty set
{{lo,lo},{lo}} is non empty set
field the of S is set
S is non empty non void V64() ()
the carrier' of S is non empty set
o is Element of the carrier' of S
w1 is Element of the carrier' of S
lo is Element of the carrier' of S
the of S is Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric transitive V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
field the of S is set
[o,w1] is set
{o,w1} is non empty set
{o} is non empty set
{{o,w1},{o}} is non empty set
[w1,lo] is set
{w1,lo} is non empty set
{w1} is non empty set
{{w1,lo},{w1}} is non empty set
[o,lo] is set
{o,lo} is non empty set
{{o,lo},{o}} is non empty set
S is non empty non void V64() ()
the carrier' of S is non empty set
id the carrier' of S is non empty Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric antisymmetric transitive Function-like one-to-one V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
the of S is Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric transitive V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
op2 is Element of the carrier' of S
op is Element of the carrier' of S
[op2,op] is set
{op2,op} is non empty set
{op2} is non empty set
{{op2,op},{op2}} is non empty set
op2 is set
op is set
[op2,op] is set
{op2,op} is non empty set
{op2} is non empty set
{{op2,op},{op2}} is non empty set
o is set
s2 is set
[o,s2] is set
{o,s2} is non empty set
{o} is non empty set
{{o,s2},{o}} is non empty set
op1 is Element of the carrier' of S
T is Element of the carrier' of S
S is non empty non void V64() ()
the carrier' of S is non empty set
o is Element of the carrier' of S
w1 is Element of the carrier' of S
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
the_arity_of w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of o is Element of the carrier of S
the_result_sort_of w1 is Element of the carrier of S
S is non empty non void V64() ManySortedSign
the carrier of S is non empty set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued reflexive symmetric antisymmetric transitive Function-like one-to-one V25( the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty Relation-like set
K10(K11( the carrier of S, the carrier of S)) is non empty set
the carrier' of S is non empty set
id the carrier' of S is non empty Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric antisymmetric transitive Function-like one-to-one V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Element of K10(K11( the carrier' of S,( the carrier of S *)))
K11( the carrier' of S,( the carrier of S *)) is non empty Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is non empty set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is non empty set
( the carrier of S,(id the carrier of S), the carrier' of S,(id the carrier' of S), the Arity of S, the ResultSort of S) is non empty V64() reflexive transitive antisymmetric () ()
w1 is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier of w1 is non empty set
the InternalRel of w1 is Relation-like the carrier of w1 -defined the carrier of w1 -valued Element of K10(K11( the carrier of w1, the carrier of w1))
K11( the carrier of w1, the carrier of w1) is non empty Relation-like set
K10(K11( the carrier of w1, the carrier of w1)) is non empty set
the carrier' of w1 is non empty set
the of w1 is Relation-like the carrier' of w1 -defined the carrier' of w1 -valued reflexive symmetric transitive V25( the carrier' of w1) Element of K10(K11( the carrier' of w1, the carrier' of w1))
K11( the carrier' of w1, the carrier' of w1) is non empty Relation-like set
K10(K11( the carrier' of w1, the carrier' of w1)) is non empty set
the carrier of w1 * is non empty functional FinSequence-membered M37( the carrier of w1)
the Arity of w1 is Relation-like the carrier' of w1 -defined the carrier of w1 * -valued Function-like V29( the carrier' of w1, the carrier of w1 * ) Element of K10(K11( the carrier' of w1,( the carrier of w1 *)))
K11( the carrier' of w1,( the carrier of w1 *)) is non empty Relation-like set
K10(K11( the carrier' of w1,( the carrier of w1 *))) is non empty set
the ResultSort of w1 is Relation-like the carrier' of w1 -defined the carrier of w1 -valued Function-like V29( the carrier' of w1, the carrier of w1) Element of K10(K11( the carrier' of w1, the carrier of w1))
K11( the carrier' of w1, the carrier of w1) is non empty Relation-like set
K10(K11( the carrier' of w1, the carrier of w1)) is non empty set
o is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier of o is non empty set
the InternalRel of o is Relation-like the carrier of o -defined the carrier of o -valued Element of K10(K11( the carrier of o, the carrier of o))
K11( the carrier of o, the carrier of o) is non empty Relation-like set
K10(K11( the carrier of o, the carrier of o)) is non empty set
the carrier' of o is non empty set
the of o is Relation-like the carrier' of o -defined the carrier' of o -valued reflexive symmetric transitive V25( the carrier' of o) Element of K10(K11( the carrier' of o, the carrier' of o))
K11( the carrier' of o, the carrier' of o) is non empty Relation-like set
K10(K11( the carrier' of o, the carrier' of o)) is non empty set
the carrier of o * is non empty functional FinSequence-membered M37( the carrier of o)
the Arity of o is Relation-like the carrier' of o -defined the carrier of o * -valued Function-like V29( the carrier' of o, the carrier of o * ) Element of K10(K11( the carrier' of o,( the carrier of o *)))
K11( the carrier' of o,( the carrier of o *)) is non empty Relation-like set
K10(K11( the carrier' of o,( the carrier of o *))) is non empty set
the ResultSort of o is Relation-like the carrier' of o -defined the carrier of o -valued Function-like V29( the carrier' of o, the carrier of o) Element of K10(K11( the carrier' of o, the carrier of o))
K11( the carrier' of o, the carrier of o) is non empty Relation-like set
K10(K11( the carrier' of o, the carrier of o)) is non empty set
w1 is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier of w1 is non empty set
the InternalRel of w1 is Relation-like the carrier of w1 -defined the carrier of w1 -valued Element of K10(K11( the carrier of w1, the carrier of w1))
K11( the carrier of w1, the carrier of w1) is non empty Relation-like set
K10(K11( the carrier of w1, the carrier of w1)) is non empty set
the carrier' of w1 is non empty set
the of w1 is Relation-like the carrier' of w1 -defined the carrier' of w1 -valued reflexive symmetric transitive V25( the carrier' of w1) Element of K10(K11( the carrier' of w1, the carrier' of w1))
K11( the carrier' of w1, the carrier' of w1) is non empty Relation-like set
K10(K11( the carrier' of w1, the carrier' of w1)) is non empty set
the carrier of w1 * is non empty functional FinSequence-membered M37( the carrier of w1)
the Arity of w1 is Relation-like the carrier' of w1 -defined the carrier of w1 * -valued Function-like V29( the carrier' of w1, the carrier of w1 * ) Element of K10(K11( the carrier' of w1,( the carrier of w1 *)))
K11( the carrier' of w1,( the carrier of w1 *)) is non empty Relation-like set
K10(K11( the carrier' of w1,( the carrier of w1 *))) is non empty set
the ResultSort of w1 is Relation-like the carrier' of w1 -defined the carrier of w1 -valued Function-like V29( the carrier' of w1, the carrier of w1) Element of K10(K11( the carrier' of w1, the carrier of w1))
K11( the carrier' of w1, the carrier of w1) is non empty Relation-like set
K10(K11( the carrier' of w1, the carrier of w1)) is non empty set
S is non empty non void V64() ManySortedSign
(S) is non empty non void V64() reflexive transitive antisymmetric () () ()
the of (S) is Relation-like the carrier' of (S) -defined the carrier' of (S) -valued reflexive symmetric transitive V25( the carrier' of (S)) Element of K10(K11( the carrier' of (S), the carrier' of (S)))
the carrier' of (S) is non empty set
K11( the carrier' of (S), the carrier' of (S)) is non empty Relation-like set
K10(K11( the carrier' of (S), the carrier' of (S))) is non empty set
the carrier of S is non empty set
the carrier of (S) is non empty set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued reflexive symmetric antisymmetric transitive Function-like one-to-one V25( the carrier of S) Element of K10(K11( the carrier of S, the carrier of S))
K11( the carrier of S, the carrier of S) is non empty Relation-like set
K10(K11( the carrier of S, the carrier of S)) is non empty set
the InternalRel of (S) is Relation-like the carrier of (S) -defined the carrier of (S) -valued Element of K10(K11( the carrier of (S), the carrier of (S)))
K11( the carrier of (S), the carrier of (S)) is non empty Relation-like set
K10(K11( the carrier of (S), the carrier of (S))) is non empty set
the carrier' of S is non empty set
id the carrier' of S is non empty Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric antisymmetric transitive Function-like one-to-one V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
lo is Element of the carrier' of (S)
op2 is Element of the carrier' of (S)
[lo,op2] is set
{lo,op2} is non empty set
{lo} is non empty set
{{lo,op2},{lo}} is non empty set
the non empty non void V64() ManySortedSign is non empty non void V64() ManySortedSign
( the non empty non void V64() ManySortedSign ) is non empty non void V64() reflexive transitive antisymmetric () () ()
o is non empty non void V64() reflexive transitive antisymmetric () () ()
S is non empty non void V64() ()
S is non empty non void V64() ManySortedSign
(S) is non empty non void V64() reflexive transitive antisymmetric () () ()
S is non empty reflexive transitive antisymmetric RelStr
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
lo is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
len lo is V36() V37() V38() V42() Element of K162()
op is set
op2 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
dom op2 is Element of K10(K162())
op1 is Element of the carrier of S
op2 . op is set
T is Element of the carrier of S
S is non empty reflexive transitive antisymmetric RelStr
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
len o is V36() V37() V38() V42() Element of K162()
len w1 is V36() V37() V38() V42() Element of K162()
dom o is Element of K10(K162())
dom w1 is Element of K10(K162())
lo is set
o . lo is set
w1 . lo is set
op2 is Element of the carrier of S
op is Element of the carrier of S
S is non empty reflexive transitive antisymmetric RelStr
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
len o is V36() V37() V38() V42() Element of K162()
len w1 is V36() V37() V38() V42() Element of K162()
dom o is Element of K10(K162())
dom w1 is Element of K10(K162())
op2 is set
o . op2 is set
w1 . op2 is set
lo is non empty reflexive transitive antisymmetric discrete RelStr
the carrier of lo is non empty set
op is Element of the carrier of S
op1 is Element of the carrier of S
T is Element of the carrier of lo
o is Element of the carrier of lo
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
o is Element of the carrier' of S
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
the_result_sort_of o is Element of the carrier of S
w1 is Element of the carrier' of S
the_arity_of w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of w1 is Element of the carrier of S
lo is non empty non void V64() reflexive transitive antisymmetric discrete () () ()
the carrier of lo is non empty set
op2 is Element of the carrier of lo
op is Element of the carrier of lo
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the of S is Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric transitive V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
the carrier' of S is non empty set
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
id the carrier' of S is non empty Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric antisymmetric transitive Function-like one-to-one V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
w1 is Element of the carrier' of S
lo is Element of the carrier' of S
the_arity_of w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
the_arity_of lo is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of w1 is Element of the carrier of S
the_result_sort_of lo is Element of the carrier of S
[w1,lo] is set
{w1,lo} is non empty set
{w1} is non empty set
{{w1,lo},{w1}} is non empty set
the non empty non void V64() reflexive transitive antisymmetric () () () () is non empty non void V64() reflexive transitive antisymmetric () () () ()
S is non empty non void V64() reflexive transitive antisymmetric () () () ()
the carrier' of S is non empty set
the Element of the carrier' of S is Element of the carrier' of S
S is non empty non void V64() reflexive transitive antisymmetric () () () ()
the carrier' of S is non empty set
o is Element of the carrier' of S
S is non empty non void V64() reflexive transitive antisymmetric () () ()
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
o is Element of the carrier' of S
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
w1 is Element of the carrier' of S
the_arity_of w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of o is Element of the carrier of S
the_result_sort_of w1 is Element of the carrier of S
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
S is non empty non void V64() reflexive transitive antisymmetric () () () ()
the carrier' of S is non empty set
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
o is (S) Element of the carrier' of S
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
lo is (S) Element of the carrier' of S
op2 is (S) Element of the carrier' of S
the_arity_of op2 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of op2 is Element of the carrier of S
op is (S) Element of the carrier' of S
the_arity_of op is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of op is Element of the carrier of S
o is (S) Element of the carrier' of S
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
lo is (S) Element of the carrier' of S
S is non empty non void V64() reflexive transitive antisymmetric () () () ()
the carrier' of S is non empty set
o is (S) Element of the carrier' of S
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
lo is (S) Element of the carrier' of S
the_arity_of lo is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the non empty non void V64() reflexive transitive antisymmetric () () () () () is non empty non void V64() reflexive transitive antisymmetric () () () () ()
S is non empty non void V64() reflexive transitive antisymmetric () () () ()
S is non empty non void V64() reflexive transitive antisymmetric () () () () ()
the carrier' of S is non empty set
o is (S) Element of the carrier' of S
S is non empty non void V64() reflexive transitive antisymmetric () () () () ()
the carrier' of S is non empty set
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
o is (S) (S) Element of the carrier' of S
w1 is (S) (S) Element of the carrier' of S
lo is (S) (S) Element of the carrier' of S
op2 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_arity_of lo is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of lo is Element of the carrier of S
the_result_sort_of o is Element of the carrier of S
S is non empty non void V64() reflexive transitive antisymmetric () () () () ()
the carrier' of S is non empty set
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
o is (S) (S) Element of the carrier' of S
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
lo is (S) (S) Element of the carrier' of S
op2 is (S) (S) Element of the carrier' of S
S is non empty non void V64() reflexive transitive antisymmetric () () () () ()
the carrier' of S is non empty set
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
o is (S) (S) Element of the carrier' of S
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
(S,o,w1) is (S) (S) Element of the carrier' of S
lo is (S) (S) Element of the carrier' of S
S is non empty reflexive transitive antisymmetric RelStr
the carrier of S is non empty set
o is non empty set
the carrier of S --> o is Relation-like the carrier of S -defined {o} -valued Function-like V29( the carrier of S,{o}) Element of K10(K11( the carrier of S,{o}))
{o} is non empty set
K11( the carrier of S,{o}) is non empty Relation-like set
K10(K11( the carrier of S,{o})) is non empty set
dom ( the carrier of S --> o) is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
S is non empty reflexive transitive antisymmetric RelStr
the carrier of S is non empty set
o is non empty set
(S,o) is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
the carrier of S --> o is Relation-like the carrier of S -defined {o} -valued Function-like V29( the carrier of S,{o}) Element of K10(K11( the carrier of S,{o}))
{o} is non empty set
K11( the carrier of S,{o}) is non empty Relation-like set
K10(K11( the carrier of S,{o})) is non empty set
op2 is set
(S,o) . op2 is set
op2 is Element of the carrier of S
op is Element of the carrier of S
(S,o) . op2 is set
(S,o) . op is set
( the carrier of S --> o) . op2 is Element of {o}
( the carrier of S --> o) . op is Element of {o}
S is non empty reflexive transitive antisymmetric RelStr
the carrier of S is non empty set
S is non empty reflexive transitive antisymmetric RelStr
o is non empty set
(S,o) is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
the carrier of S is non empty set
the carrier of S --> o is Relation-like the carrier of S -defined {o} -valued Function-like V29( the carrier of S,{o}) Element of K10(K11( the carrier of S,{o}))
{o} is non empty set
K11( the carrier of S,{o}) is non empty Relation-like set
K10(K11( the carrier of S,{o})) is non empty set
lo is Element of the carrier of S
op2 is Element of the carrier of S
(S,o) . lo is set
(S,o) . op2 is set
S is non empty reflexive transitive antisymmetric RelStr
the carrier of S is non empty set
the non empty set is non empty set
(S, the non empty set ) is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
the carrier of S --> the non empty set is Relation-like the carrier of S -defined { the non empty set } -valued Function-like V29( the carrier of S,{ the non empty set }) Element of K10(K11( the carrier of S,{ the non empty set }))
{ the non empty set } is non empty set
K11( the carrier of S,{ the non empty set }) is non empty Relation-like set
K10(K11( the carrier of S,{ the non empty set })) is non empty set
S is non empty reflexive transitive antisymmetric RelStr
o is non empty set
(S,o) is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
the carrier of S is non empty set
the carrier of S --> o is Relation-like the carrier of S -defined {o} -valued Function-like V29( the carrier of S,{o}) Element of K10(K11( the carrier of S,{o}))
{o} is non empty set
K11( the carrier of S,{o}) is non empty Relation-like set
K10(K11( the carrier of S,{o})) is non empty set
S is non empty reflexive transitive antisymmetric RelStr
the carrier of S is non empty set
(S,1) is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) (S) set
the carrier of S --> 1 is Relation-like the carrier of S -defined {1} -valued Function-like V29( the carrier of S,{1}) Element of K10(K11( the carrier of S,{1}))
{1} is non empty set
K11( the carrier of S,{1}) is non empty Relation-like set
K10(K11( the carrier of S,{1})) is non empty set
S is non empty non void V64() reflexive transitive antisymmetric () () ()
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier of S is non empty set
o is MSAlgebra over S
the Sorts of o is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
lo is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
op2 is Element of the carrier of S
lo . op2 is set
op is Element of the carrier of S
lo . op is set
op2 is Element of the carrier of S
the Sorts of o . op2 is set
op is Element of the carrier of S
the Sorts of o . op is set
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is non empty Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is non empty set
o is non empty set
(S,o) is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) (S) set
the carrier of S --> o is Relation-like the carrier of S -defined {o} -valued Function-like V29( the carrier of S,{o}) Element of K10(K11( the carrier of S,{o}))
{o} is non empty set
K11( the carrier of S,{o}) is non empty Relation-like set
K10(K11( the carrier of S,{o})) is non empty set
(S,o) # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the Arity of S * ((S,o) #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is non empty set
the ResultSort of S * (S,o) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
w1 is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ((S,o) #), the ResultSort of S * (S,o)
lo is set
(S,o) . lo is set
MSAlgebra(# (S,o),w1 #) is strict MSAlgebra over S
lo is strict non-empty MSAlgebra over S
the Sorts of lo is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V25( the carrier of S) set
the Charact of lo is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ( the Sorts of lo #), the ResultSort of S * the Sorts of lo
the Sorts of lo # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the Arity of S * ( the Sorts of lo #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the ResultSort of S * the Sorts of lo is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V25( the carrier' of S) set
lo is strict non-empty MSAlgebra over S
the Sorts of lo is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V25( the carrier of S) set
the Charact of lo is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ( the Sorts of lo #), the ResultSort of S * the Sorts of lo
the Sorts of lo # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the Arity of S * ( the Sorts of lo #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the ResultSort of S * the Sorts of lo is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V25( the carrier' of S) set
op2 is strict non-empty MSAlgebra over S
the Sorts of op2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V25( the carrier of S) set
the Charact of op2 is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ( the Sorts of op2 #), the ResultSort of S * the Sorts of op2
the Sorts of op2 # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the Arity of S * ( the Sorts of op2 #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the ResultSort of S * the Sorts of op2 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V25( the carrier' of S) set
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is non empty Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is non empty set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is non empty set
o is non empty set
(S,o) is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) (S) set
the carrier of S --> o is Relation-like the carrier of S -defined {o} -valued Function-like V29( the carrier of S,{o}) Element of K10(K11( the carrier of S,{o}))
{o} is non empty set
K11( the carrier of S,{o}) is non empty Relation-like set
K10(K11( the carrier of S,{o})) is non empty set
(S,o) # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the Arity of S * ((S,o) #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the ResultSort of S * (S,o) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
w1 is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ((S,o) #), the ResultSort of S * (S,o)
(S,o,w1) is strict non-empty MSAlgebra over S
the Sorts of (S,o,w1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V25( the carrier of S) set
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the non empty set is non empty set
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is non empty Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is non empty set
(S, the non empty set ) is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) (S) set
the carrier of S --> the non empty set is Relation-like the carrier of S -defined { the non empty set } -valued Function-like V29( the carrier of S,{ the non empty set }) Element of K10(K11( the carrier of S,{ the non empty set }))
{ the non empty set } is non empty set
K11( the carrier of S,{ the non empty set }) is non empty Relation-like set
K10(K11( the carrier of S,{ the non empty set })) is non empty set
(S, the non empty set ) # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the Arity of S * ((S, the non empty set ) #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is non empty set
the ResultSort of S * (S, the non empty set ) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ((S, the non empty set ) #), the ResultSort of S * (S, the non empty set ) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ((S, the non empty set ) #), the ResultSort of S * (S, the non empty set )
(S, the non empty set , the non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ((S, the non empty set ) #), the ResultSort of S * (S, the non empty set )) is strict non-empty MSAlgebra over S
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is non empty Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is non empty set
o is non empty set
(S,o) is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) (S) set
the carrier of S --> o is Relation-like the carrier of S -defined {o} -valued Function-like V29( the carrier of S,{o}) Element of K10(K11( the carrier of S,{o}))
{o} is non empty set
K11( the carrier of S,{o}) is non empty Relation-like set
K10(K11( the carrier of S,{o})) is non empty set
(S,o) # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the Arity of S * ((S,o) #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is non empty set
the ResultSort of S * (S,o) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
w1 is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ((S,o) #), the ResultSort of S * (S,o)
(S,o,w1) is strict non-empty MSAlgebra over S
S is non empty non void V64() reflexive transitive antisymmetric discrete () () ()
o is MSAlgebra over S
the carrier of S is non empty set
w1 is Element of the carrier of S
lo is Element of the carrier of S
the Sorts of o is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
the Sorts of o . w1 is set
the Sorts of o . lo is set
S is non empty non void V64() reflexive transitive antisymmetric discrete () () ()
o is MSAlgebra over S
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
lo is (S) MSAlgebra over S
the Sorts of lo is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
the Sorts of lo # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
( the Sorts of lo #) . o is set
( the Sorts of lo #) . w1 is set
o * the Sorts of lo is Relation-like K162() -defined Function-like V43() FinSequence-like FinSubsequence-like set
w1 * the Sorts of lo is Relation-like K162() -defined Function-like V43() FinSequence-like FinSubsequence-like set
len o is V36() V37() V38() V42() Element of K162()
len w1 is V36() V37() V38() V42() Element of K162()
op1 is set
product (o * the Sorts of lo) is set
dom (o * the Sorts of lo) is Element of K10(K162())
T is Relation-like Function-like set
dom T is set
dom o is Element of K10(K162())
dom w1 is Element of K10(K162())
dom (w1 * the Sorts of lo) is Element of K10(K162())
o is set
T . o is set
(w1 * the Sorts of lo) . o is set
(o * the Sorts of lo) . o is set
o . o is set
the Sorts of lo . (o . o) is set
w1 . o is set
the Sorts of lo . (w1 . o) is set
s2 is Element of the carrier of S
s2 is Element of the carrier of S
product (w1 * the Sorts of lo) is set
S is non empty non void V64() ManySortedSign
(S) is non empty non void V64() reflexive transitive antisymmetric discrete () () () () () () ()
o is MSAlgebra over S
the Sorts of o is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
the carrier of S is non empty set
the Charact of o is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ( the Sorts of o #), the ResultSort of S * the Sorts of o
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is non empty Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is non empty set
the Sorts of o # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the Arity of S * ( the Sorts of o #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is non empty set
the ResultSort of S * the Sorts of o is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
w1 is strict ((S)) MSAlgebra over (S)
the Sorts of w1 is non empty Relation-like the carrier of (S) -defined Function-like V25( the carrier of (S)) set
the carrier of (S) is non empty set
the Charact of w1 is non empty Relation-like the carrier' of (S) -defined Function-like V25( the carrier' of (S)) Function-yielding ManySortedFunction of the Arity of (S) * ( the Sorts of w1 #), the ResultSort of (S) * the Sorts of w1
the carrier' of (S) is non empty set
the Arity of (S) is Relation-like the carrier' of (S) -defined the carrier of (S) * -valued Function-like V29( the carrier' of (S), the carrier of (S) * ) Element of K10(K11( the carrier' of (S),( the carrier of (S) *)))
the carrier of (S) * is non empty functional FinSequence-membered M37( the carrier of (S))
K11( the carrier' of (S),( the carrier of (S) *)) is non empty Relation-like set
K10(K11( the carrier' of (S),( the carrier of (S) *))) is non empty set
the Sorts of w1 # is non empty Relation-like the carrier of (S) * -defined Function-like V25( the carrier of (S) * ) set
the Arity of (S) * ( the Sorts of w1 #) is non empty Relation-like the carrier' of (S) -defined Function-like V25( the carrier' of (S)) set
the ResultSort of (S) is Relation-like the carrier' of (S) -defined the carrier of (S) -valued Function-like V29( the carrier' of (S), the carrier of (S)) Element of K10(K11( the carrier' of (S), the carrier of (S)))
K11( the carrier' of (S), the carrier of (S)) is non empty Relation-like set
K10(K11( the carrier' of (S), the carrier of (S))) is non empty set
the ResultSort of (S) * the Sorts of w1 is non empty Relation-like the carrier' of (S) -defined Function-like V25( the carrier' of (S)) set
lo is strict ((S)) MSAlgebra over (S)
the Sorts of lo is non empty Relation-like the carrier of (S) -defined Function-like V25( the carrier of (S)) set
the Charact of lo is non empty Relation-like the carrier' of (S) -defined Function-like V25( the carrier' of (S)) Function-yielding ManySortedFunction of the Arity of (S) * ( the Sorts of lo #), the ResultSort of (S) * the Sorts of lo
the Sorts of lo # is non empty Relation-like the carrier of (S) * -defined Function-like V25( the carrier of (S) * ) set
the Arity of (S) * ( the Sorts of lo #) is non empty Relation-like the carrier' of (S) -defined Function-like V25( the carrier' of (S)) set
the ResultSort of (S) * the Sorts of lo is non empty Relation-like the carrier' of (S) -defined Function-like V25( the carrier' of (S)) set
the carrier of (S) is non empty set
the carrier' of (S) is non empty set
the carrier of (S) * is non empty functional FinSequence-membered M37( the carrier of (S))
the Arity of (S) is Relation-like the carrier' of (S) -defined the carrier of (S) * -valued Function-like V29( the carrier' of (S), the carrier of (S) * ) Element of K10(K11( the carrier' of (S),( the carrier of (S) *)))
K11( the carrier' of (S),( the carrier of (S) *)) is non empty Relation-like set
K10(K11( the carrier' of (S),( the carrier of (S) *))) is non empty set
the ResultSort of (S) is Relation-like the carrier' of (S) -defined the carrier of (S) -valued Function-like V29( the carrier' of (S), the carrier of (S)) Element of K10(K11( the carrier' of (S), the carrier of (S)))
K11( the carrier' of (S), the carrier of (S)) is non empty Relation-like set
K10(K11( the carrier' of (S), the carrier of (S))) is non empty set
op is non empty Relation-like the carrier of (S) -defined Function-like V25( the carrier of (S)) set
op # is non empty Relation-like the carrier of (S) * -defined Function-like V25( the carrier of (S) * ) set
the Arity of (S) * (op #) is non empty Relation-like the carrier' of (S) -defined Function-like V25( the carrier' of (S)) set
the ResultSort of (S) * op is non empty Relation-like the carrier' of (S) -defined Function-like V25( the carrier' of (S)) set
op1 is non empty Relation-like the carrier' of (S) -defined Function-like V25( the carrier' of (S)) Function-yielding ManySortedFunction of the Arity of (S) * (op #), the ResultSort of (S) * op
MSAlgebra(# op,op1 #) is strict ((S)) MSAlgebra over (S)
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
lo is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
len o is V36() V37() V38() V42() Element of K162()
len w1 is V36() V37() V38() V42() Element of K162()
dom o is Element of K10(K162())
dom w1 is Element of K10(K162())
len lo is V36() V37() V38() V42() Element of K162()
dom lo is Element of K10(K162())
op2 is set
o . op2 is set
lo . op2 is set
w1 . op2 is set
op is Element of the carrier of S
op1 is Element of the carrier of S
T is Element of the carrier of S
o is Element of the carrier of S
s2 is Element of the carrier of S
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
lo is Element of the carrier' of S
op2 is Element of the carrier' of S
the_arity_of op2 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
op is Element of the carrier' of S
the_result_sort_of op is Element of the carrier of S
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
o is Element of the carrier' of S
w1 is Element of the carrier' of S
the_result_sort_of o is Element of the carrier of S
the carrier of S is non empty set
the_result_sort_of w1 is Element of the carrier of S
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
the_arity_of w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
o is Element of the carrier' of S
w1 is Element of the carrier' of S
lo is Element of the carrier' of S
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
the_arity_of lo is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of o is Element of the carrier of S
the_result_sort_of lo is Element of the carrier of S
the_arity_of w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of w1 is Element of the carrier of S
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
o is Element of the carrier' of S
the_result_sort_of o is Element of the carrier of S
the carrier of S is non empty set
w1 is Element of the carrier' of S
the_result_sort_of w1 is Element of the carrier of S
lo is (S) MSAlgebra over S
Result (o,lo) is Element of rng the Sorts of lo
the Sorts of lo is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
rng the Sorts of lo is non empty set
Result (w1,lo) is Element of rng the Sorts of lo
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is non empty set
the ResultSort of S * the Sorts of lo is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
( the ResultSort of S * the Sorts of lo) . w1 is set
the ResultSort of S . w1 is Element of the carrier of S
the Sorts of lo . ( the ResultSort of S . w1) is set
the Sorts of lo . (the_result_sort_of w1) is set
op2 is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) (S) set
op2 . (the_result_sort_of o) is set
op2 . (the_result_sort_of w1) is set
( the ResultSort of S * the Sorts of lo) . o is set
the ResultSort of S . o is Element of the carrier of S
the Sorts of lo . ( the ResultSort of S . o) is set
the Sorts of lo . (the_result_sort_of o) is set
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
o is Element of the carrier' of S
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
w1 is Element of the carrier' of S
the_arity_of w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
lo is (S) MSAlgebra over S
Args (o,lo) is Element of rng ( the Sorts of lo #)
the Sorts of lo is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
the Sorts of lo # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
rng ( the Sorts of lo #) is non empty set
Args (w1,lo) is Element of rng ( the Sorts of lo #)
op2 is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) (S) set
op2 # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
(op2 #) . (the_arity_of o) is set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Element of K10(K11( the carrier' of S,( the carrier of S *)))
K11( the carrier' of S,( the carrier of S *)) is non empty Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is non empty set
the Arity of S . o is Relation-like K162() -defined Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
(op2 #) . ( the Arity of S . o) is set
the Arity of S * (op2 #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
( the Arity of S * (op2 #)) . o is set
(op2 #) . (the_arity_of w1) is set
the Arity of S . w1 is Relation-like K162() -defined Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
(op2 #) . ( the Arity of S . w1) is set
( the Arity of S * (op2 #)) . w1 is set
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
o is Element of the carrier' of S
w1 is Element of the carrier' of S
lo is (S) MSAlgebra over S
Args (o,lo) is Element of rng ( the Sorts of lo #)
the carrier of S is non empty set
the Sorts of lo is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
the Sorts of lo # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
rng ( the Sorts of lo #) is non empty set
Args (w1,lo) is Element of rng ( the Sorts of lo #)
Result (o,lo) is Element of rng the Sorts of lo
rng the Sorts of lo is non empty set
Result (w1,lo) is Element of rng the Sorts of lo
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_arity_of w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of o is Element of the carrier of S
the_result_sort_of w1 is Element of the carrier of S
S is non empty non void V64() reflexive transitive antisymmetric () () ()
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
o is non-empty (S) MSAlgebra over S
w1 is Element of the carrier' of S
lo is Element of the carrier' of S
Args (lo,o) is non empty Element of rng ( the Sorts of o #)
the carrier of S is non empty set
the Sorts of o is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V25( the carrier of S) set
the Sorts of o # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
rng ( the Sorts of o #) is non empty set
Result (lo,o) is non empty Element of rng the Sorts of o
rng the Sorts of o is non empty with_non-empty_elements set
Den (lo,o) is Relation-like Args (lo,o) -defined Result (lo,o) -valued Function-like V29( Args (lo,o), Result (lo,o)) Element of K10(K11((Args (lo,o)),(Result (lo,o))))
K11((Args (lo,o)),(Result (lo,o))) is non empty Relation-like set
K10(K11((Args (lo,o)),(Result (lo,o)))) is non empty set
Args (w1,o) is non empty Element of rng ( the Sorts of o #)
(Den (lo,o)) | (Args (w1,o)) is Relation-like Args (lo,o) -defined Args (w1,o) -defined Args (lo,o) -defined Result (lo,o) -valued Function-like Element of K10(K11((Args (lo,o)),(Result (lo,o))))
Den (w1,o) is Relation-like Args (w1,o) -defined Result (w1,o) -valued Function-like V29( Args (w1,o), Result (w1,o)) Element of K10(K11((Args (w1,o)),(Result (w1,o))))
Result (w1,o) is non empty Element of rng the Sorts of o
K11((Args (w1,o)),(Result (w1,o))) is non empty Relation-like set
K10(K11((Args (w1,o)),(Result (w1,o)))) is non empty set
w1 is Element of the carrier' of S
Args (w1,o) is non empty Element of rng ( the Sorts of o #)
Den (w1,o) is Relation-like Args (w1,o) -defined Result (w1,o) -valued Function-like V29( Args (w1,o), Result (w1,o)) Element of K10(K11((Args (w1,o)),(Result (w1,o))))
Result (w1,o) is non empty Element of rng the Sorts of o
K11((Args (w1,o)),(Result (w1,o))) is non empty Relation-like set
K10(K11((Args (w1,o)),(Result (w1,o)))) is non empty set
lo is Element of the carrier' of S
Args (lo,o) is non empty Element of rng ( the Sorts of o #)
Result (lo,o) is non empty Element of rng the Sorts of o
Den (lo,o) is Relation-like Args (lo,o) -defined Result (lo,o) -valued Function-like V29( Args (lo,o), Result (lo,o)) Element of K10(K11((Args (lo,o)),(Result (lo,o))))
K11((Args (lo,o)),(Result (lo,o))) is non empty Relation-like set
K10(K11((Args (lo,o)),(Result (lo,o)))) is non empty set
(Den (lo,o)) | (Args (w1,o)) is Relation-like Args (w1,o) -defined Args (lo,o) -defined Result (lo,o) -valued Function-like Element of K10(K11((Args (lo,o)),(Result (lo,o))))
dom (Den (w1,o)) is Element of K10((Args (w1,o)))
K10((Args (w1,o))) is non empty set
(Den (w1,o)) | (Args (w1,o)) is Relation-like Args (w1,o) -defined Args (w1,o) -defined Result (w1,o) -valued Function-like Element of K10(K11((Args (w1,o)),(Result (w1,o))))
S is non empty non void V64() reflexive transitive antisymmetric () () ()
o is (S) MSAlgebra over S
the carrier' of S is non empty set
w1 is Element of the carrier' of S
Args (w1,o) is Element of rng ( the Sorts of o #)
the carrier of S is non empty set
the Sorts of o is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
the Sorts of o # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
rng ( the Sorts of o #) is non empty set
Den (w1,o) is Relation-like Args (w1,o) -defined Result (w1,o) -valued Function-like V29( Args (w1,o), Result (w1,o)) Element of K10(K11((Args (w1,o)),(Result (w1,o))))
Result (w1,o) is Element of rng the Sorts of o
rng the Sorts of o is non empty set
K11((Args (w1,o)),(Result (w1,o))) is Relation-like set
K10(K11((Args (w1,o)),(Result (w1,o)))) is non empty set
lo is Element of the carrier' of S
Args (lo,o) is Element of rng ( the Sorts of o #)
Result (lo,o) is Element of rng the Sorts of o
Den (lo,o) is Relation-like Args (lo,o) -defined Result (lo,o) -valued Function-like V29( Args (lo,o), Result (lo,o)) Element of K10(K11((Args (lo,o)),(Result (lo,o))))
K11((Args (lo,o)),(Result (lo,o))) is Relation-like set
K10(K11((Args (lo,o)),(Result (lo,o)))) is non empty set
(Den (lo,o)) | (Args (w1,o)) is Relation-like Args (w1,o) -defined Args (lo,o) -defined Result (lo,o) -valued Function-like Element of K10(K11((Args (lo,o)),(Result (lo,o))))
the_arity_of w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_arity_of lo is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of w1 is Element of the carrier of S
the_result_sort_of lo is Element of the carrier of S
o is non empty set
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier of S is non empty set
(S,o) is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) (S) set
the carrier of S --> o is Relation-like the carrier of S -defined {o} -valued Function-like V29( the carrier of S,{o}) Element of K10(K11( the carrier of S,{o}))
{o} is non empty set
K11( the carrier of S,{o}) is non empty Relation-like set
K10(K11( the carrier of S,{o})) is non empty set
the carrier' of S is non empty set
w1 is Element of o
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is non empty Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is non empty set
(S,o) # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the Arity of S * ((S,o) #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
{w1} is non empty set
op2 is Relation-like Function-like set
dom op2 is set
op is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is non empty set
the ResultSort of S * (S,o) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
op1 is set
op . op1 is set
( the Arity of S * ((S,o) #)) . op1 is set
( the ResultSort of S * (S,o)) . op1 is set
K11((( the Arity of S * ((S,o) #)) . op1),(( the ResultSort of S * (S,o)) . op1)) is Relation-like set
K10(K11((( the Arity of S * ((S,o) #)) . op1),(( the ResultSort of S * (S,o)) . op1))) is non empty set
T is Element of the carrier' of S
the ResultSort of S . T is Element of the carrier of S
the ResultSort of S " the carrier of S is Element of K10( the carrier' of S)
K10( the carrier' of S) is non empty set
( the ResultSort of S * (S,o)) . T is set
( the ResultSort of S " the carrier of S) --> o is Relation-like the ResultSort of S " the carrier of S -defined {o} -valued Function-like V29( the ResultSort of S " the carrier of S,{o}) Element of K10(K11(( the ResultSort of S " the carrier of S),{o}))
K11(( the ResultSort of S " the carrier of S),{o}) is Relation-like set
K10(K11(( the ResultSort of S " the carrier of S),{o})) is non empty set
(( the ResultSort of S " the carrier of S) --> o) . T is set
( the Arity of S * ((S,o) #)) . T is set
(( the Arity of S * ((S,o) #)) . T) --> w1 is Relation-like ( the Arity of S * ((S,o) #)) . T -defined {w1} -valued Function-like V29(( the Arity of S * ((S,o) #)) . T,{w1}) Element of K10(K11((( the Arity of S * ((S,o) #)) . T),{w1}))
K11((( the Arity of S * ((S,o) #)) . T),{w1}) is Relation-like set
K10(K11((( the Arity of S * ((S,o) #)) . T),{w1})) is non empty set
op1 is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ((S,o) #), the ResultSort of S * (S,o)
(S,o,op1) is strict non-empty (S) MSAlgebra over S
T is strict non-empty (S) MSAlgebra over S
the Sorts of T is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V25( the carrier of S) set
o is Element of the carrier' of S
Den (o,T) is Relation-like Args (o,T) -defined Result (o,T) -valued Function-like V29( Args (o,T), Result (o,T)) Element of K10(K11((Args (o,T)),(Result (o,T))))
Args (o,T) is non empty Element of rng ( the Sorts of T #)
the Sorts of T # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
rng ( the Sorts of T #) is non empty set
Result (o,T) is non empty Element of rng the Sorts of T
rng the Sorts of T is non empty with_non-empty_elements set
K11((Args (o,T)),(Result (o,T))) is non empty Relation-like set
K10(K11((Args (o,T)),(Result (o,T)))) is non empty set
(Args (o,T)) --> w1 is Relation-like Args (o,T) -defined o -valued Function-like V29( Args (o,T),o) Element of K10(K11((Args (o,T)),o))
K11((Args (o,T)),o) is non empty Relation-like set
K10(K11((Args (o,T)),o)) is non empty set
the Charact of T is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ( the Sorts of T #), the ResultSort of S * the Sorts of T
the Arity of S * ( the Sorts of T #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the ResultSort of S * the Sorts of T is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V25( the carrier' of S) set
the Charact of T . o is set
op1 . o is set
( the Arity of S * ((S,o) #)) . o is set
(( the Arity of S * ((S,o) #)) . o) --> w1 is Relation-like ( the Arity of S * ((S,o) #)) . o -defined o -valued Function-like V29(( the Arity of S * ((S,o) #)) . o,o) Element of K10(K11((( the Arity of S * ((S,o) #)) . o),o))
K11((( the Arity of S * ((S,o) #)) . o),o) is Relation-like set
K10(K11((( the Arity of S * ((S,o) #)) . o),o)) is non empty set
lo is strict (S) MSAlgebra over S
the Sorts of lo is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
op2 is strict (S) MSAlgebra over S
the Sorts of op2 is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
op is set
the Charact of lo is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ( the Sorts of lo #), the ResultSort of S * the Sorts of lo
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Element of K10(K11( the carrier' of S,( the carrier of S *)))
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
K11( the carrier' of S,( the carrier of S *)) is non empty Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is non empty set
the Sorts of lo # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the Arity of S * ( the Sorts of lo #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of K10(K11( the carrier' of S, the carrier of S))
K11( the carrier' of S, the carrier of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier of S)) is non empty set
the ResultSort of S * the Sorts of lo is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the Charact of lo . op is set
op1 is Element of the carrier' of S
Den (op1,lo) is Relation-like Args (op1,lo) -defined Result (op1,lo) -valued Function-like V29( Args (op1,lo), Result (op1,lo)) Element of K10(K11((Args (op1,lo)),(Result (op1,lo))))
Args (op1,lo) is Element of rng ( the Sorts of lo #)
rng ( the Sorts of lo #) is non empty set
Result (op1,lo) is Element of rng the Sorts of lo
rng the Sorts of lo is non empty set
K11((Args (op1,lo)),(Result (op1,lo))) is Relation-like set
K10(K11((Args (op1,lo)),(Result (op1,lo)))) is non empty set
(Args (op1,lo)) --> w1 is Relation-like Args (op1,lo) -defined o -valued Function-like V29( Args (op1,lo),o) Element of K10(K11((Args (op1,lo)),o))
K11((Args (op1,lo)),o) is Relation-like set
K10(K11((Args (op1,lo)),o)) is non empty set
(S,o) # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the Arity of S * ((S,o) #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
( the Arity of S * ((S,o) #)) . op1 is set
(( the Arity of S * ((S,o) #)) . op1) --> w1 is Relation-like ( the Arity of S * ((S,o) #)) . op1 -defined o -valued Function-like V29(( the Arity of S * ((S,o) #)) . op1,o) Element of K10(K11((( the Arity of S * ((S,o) #)) . op1),o))
K11((( the Arity of S * ((S,o) #)) . op1),o) is Relation-like set
K10(K11((( the Arity of S * ((S,o) #)) . op1),o)) is non empty set
Args (op1,op2) is Element of rng ( the Sorts of op2 #)
the Sorts of op2 # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
rng ( the Sorts of op2 #) is non empty set
(Args (op1,op2)) --> w1 is Relation-like Args (op1,op2) -defined o -valued Function-like V29( Args (op1,op2),o) Element of K10(K11((Args (op1,op2)),o))
K11((Args (op1,op2)),o) is Relation-like set
K10(K11((Args (op1,op2)),o)) is non empty set
Den (op1,op2) is Relation-like Args (op1,op2) -defined Result (op1,op2) -valued Function-like V29( Args (op1,op2), Result (op1,op2)) Element of K10(K11((Args (op1,op2)),(Result (op1,op2))))
Result (op1,op2) is Element of rng the Sorts of op2
rng the Sorts of op2 is non empty set
K11((Args (op1,op2)),(Result (op1,op2))) is Relation-like set
K10(K11((Args (op1,op2)),(Result (op1,op2)))) is non empty set
the Charact of op2 is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) Function-yielding ManySortedFunction of the Arity of S * ( the Sorts of op2 #), the ResultSort of S * the Sorts of op2
the Arity of S * ( the Sorts of op2 #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the ResultSort of S * the Sorts of op2 is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
the Charact of op2 . op is set
S is non empty non void V64() reflexive transitive antisymmetric () () ()
o is non empty set
w1 is Element of o
(S,o,w1) is strict (S) MSAlgebra over S
the carrier of S is non empty set
the Sorts of (S,o,w1) is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) set
(S,o) is non empty Relation-like the carrier of S -defined Function-like V25( the carrier of S) (S) set
the carrier of S --> o is Relation-like the carrier of S -defined {o} -valued Function-like V29( the carrier of S,{o}) Element of K10(K11( the carrier of S,{o}))
{o} is non empty set
K11( the carrier of S,{o}) is non empty Relation-like set
K10(K11( the carrier of S,{o})) is non empty set
the carrier' of S is non empty set
op2 is non-empty (S) MSAlgebra over S
op is Element of the carrier' of S
Args (op,op2) is non empty Element of rng ( the Sorts of op2 #)
the Sorts of op2 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V25( the carrier of S) set
the Sorts of op2 # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
rng ( the Sorts of op2 #) is non empty set
Result (op,op2) is non empty Element of rng the Sorts of op2
rng the Sorts of op2 is non empty with_non-empty_elements set
Den (op,op2) is Relation-like Args (op,op2) -defined Result (op,op2) -valued Function-like V29( Args (op,op2), Result (op,op2)) Element of K10(K11((Args (op,op2)),(Result (op,op2))))
K11((Args (op,op2)),(Result (op,op2))) is non empty Relation-like set
K10(K11((Args (op,op2)),(Result (op,op2)))) is non empty set
op1 is Element of the carrier' of S
Den (op1,op2) is Relation-like Args (op1,op2) -defined Result (op1,op2) -valued Function-like V29( Args (op1,op2), Result (op1,op2)) Element of K10(K11((Args (op1,op2)),(Result (op1,op2))))
Args (op1,op2) is non empty Element of rng ( the Sorts of op2 #)
Result (op1,op2) is non empty Element of rng the Sorts of op2
K11((Args (op1,op2)),(Result (op1,op2))) is non empty Relation-like set
K10(K11((Args (op1,op2)),(Result (op1,op2)))) is non empty set
Args (op,(S,o,w1)) is Element of rng ( the Sorts of (S,o,w1) #)
the Sorts of (S,o,w1) # is non empty Relation-like the carrier of S * -defined Function-like V25( the carrier of S * ) set
rng ( the Sorts of (S,o,w1) #) is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Element of K10(K11( the carrier' of S,( the carrier of S *)))
K11( the carrier' of S,( the carrier of S *)) is non empty Relation-like set
K10(K11( the carrier' of S,( the carrier of S *))) is non empty set
the Arity of S * ( the Sorts of (S,o,w1) #) is non empty Relation-like the carrier' of S -defined Function-like V25( the carrier' of S) set
( the Arity of S * ( the Sorts of (S,o,w1) #)) . op is set
the Arity of S . op is Relation-like K162() -defined Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
( the Sorts of (S,o,w1) #) . ( the Arity of S . op) is set
the_arity_of op is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
( the Sorts of (S,o,w1) #) . (the_arity_of op) is set
Args (op1,(S,o,w1)) is Element of rng ( the Sorts of (S,o,w1) #)
( the Arity of S * ( the Sorts of (S,o,w1) #)) . op1 is set
the Arity of S . op1 is Relation-like K162() -defined Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
( the Sorts of (S,o,w1) #) . ( the Arity of S . op1) is set
the_arity_of op1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
( the Sorts of (S,o,w1) #) . (the_arity_of op1) is set
Den (op,(S,o,w1)) is Relation-like Args (op,(S,o,w1)) -defined Result (op,(S,o,w1)) -valued Function-like V29( Args (op,(S,o,w1)), Result (op,(S,o,w1))) Element of K10(K11((Args (op,(S,o,w1))),(Result (op,(S,o,w1)))))
Result (op,(S,o,w1)) is Element of rng the Sorts of (S,o,w1)
rng the Sorts of (S,o,w1) is non empty set
K11((Args (op,(S,o,w1))),(Result (op,(S,o,w1)))) is Relation-like set
K10(K11((Args (op,(S,o,w1))),(Result (op,(S,o,w1))))) is non empty set
(Args (op,(S,o,w1))) --> w1 is Relation-like Args (op,(S,o,w1)) -defined o -valued Function-like V29( Args (op,(S,o,w1)),o) Element of K10(K11((Args (op,(S,o,w1))),o))
K11((Args (op,(S,o,w1))),o) is Relation-like set
K10(K11((Args (op,(S,o,w1))),o)) is non empty set
Den (op1,(S,o,w1)) is Relation-like Args (op1,(S,o,w1)) -defined Result (op1,(S,o,w1)) -valued Function-like V29( Args (op1,(S,o,w1)), Result (op1,(S,o,w1))) Element of K10(K11((Args (op1,(S,o,w1))),(Result (op1,(S,o,w1)))))
Result (op1,(S,o,w1)) is Element of rng the Sorts of (S,o,w1)
K11((Args (op1,(S,o,w1))),(Result (op1,(S,o,w1)))) is Relation-like set
K10(K11((Args (op1,(S,o,w1))),(Result (op1,(S,o,w1))))) is non empty set
(Args (op1,(S,o,w1))) --> w1 is Relation-like Args (op1,(S,o,w1)) -defined o -valued Function-like V29( Args (op1,(S,o,w1)),o) Element of K10(K11((Args (op1,(S,o,w1))),o))
K11((Args (op1,(S,o,w1))),o) is Relation-like set
K10(K11((Args (op1,(S,o,w1))),o)) is non empty set
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the non empty set is non empty set
the Element of the non empty set is Element of the non empty set
(S, the non empty set , the Element of the non empty set ) is strict (S) MSAlgebra over S
o is non empty set
S is non empty non void V64() reflexive transitive antisymmetric () () ()
w1 is Element of o
(S,o,w1) is strict (S) MSAlgebra over S
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
the of S is Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric transitive V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
Class the of S is non empty with_non-empty_elements a_partition of the carrier' of S
K10( the carrier' of S) is non empty set
K10(K10( the carrier' of S)) is non empty set
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
K10( the carrier' of S) is non empty set
(S) is non empty Element of K10(K10( the carrier' of S))
K10(K10( the carrier' of S)) is non empty set
the of S is Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric transitive V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
Class the of S is non empty with_non-empty_elements a_partition of the carrier' of S
o is Element of (S)
w1 is set
Class ( the of S,w1) is Element of K10( the carrier' of S)
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
the of S is Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric transitive V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
o is Element of the carrier' of S
Class ( the of S,o) is Element of K10( the carrier' of S)
K10( the carrier' of S) is non empty set
(S) is non empty Element of K10(K10( the carrier' of S))
K10(K10( the carrier' of S)) is non empty set
Class the of S is non empty with_non-empty_elements a_partition of the carrier' of S
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
the of S is Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric transitive V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
o is Element of the carrier' of S
Class ( the of S,o) is Element of K10( the carrier' of S)
K10( the carrier' of S) is non empty set
w1 is Element of the carrier' of S
[w1,o] is set
{w1,o} is non empty set
{w1} is non empty set
{{w1,o},{w1}} is non empty set
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
o is Element of the carrier' of S
(S,o) is non empty Element of (S)
K10( the carrier' of S) is non empty set
(S) is non empty Element of K10(K10( the carrier' of S))
K10(K10( the carrier' of S)) is non empty set
the of S is Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric transitive V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
Class the of S is non empty with_non-empty_elements a_partition of the carrier' of S
Class ( the of S,o) is Element of K10( the carrier' of S)
w1 is Element of the carrier' of S
(S,w1) is non empty Element of (S)
Class ( the of S,w1) is Element of K10( the carrier' of S)
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
K10( the carrier' of S) is non empty set
(S) is non empty Element of K10(K10( the carrier' of S))
K10(K10( the carrier' of S)) is non empty set
the of S is Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric transitive V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
Class the of S is non empty with_non-empty_elements a_partition of the carrier' of S
o is set
w1 is set
Class ( the of S,w1) is Element of K10( the carrier' of S)
lo is Element of the carrier' of S
op2 is Element of the carrier' of S
(S,op2) is non empty Element of (S)
Class ( the of S,op2) is Element of K10( the carrier' of S)
w1 is Element of the carrier' of S
(S,w1) is non empty Element of (S)
Class ( the of S,w1) is Element of K10( the carrier' of S)
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
K10( the carrier' of S) is non empty set
(S) is non empty Element of K10(K10( the carrier' of S))
K10(K10( the carrier' of S)) is non empty set
the of S is Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric transitive V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
Class the of S is non empty with_non-empty_elements a_partition of the carrier' of S
o is non empty Element of (S)
w1 is Element of o
S is non empty non void V64() reflexive transitive antisymmetric () () ()
the carrier' of S is non empty set
K10( the carrier' of S) is non empty set
(S) is non empty Element of K10(K10( the carrier' of S))
K10(K10( the carrier' of S)) is non empty set
the of S is Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric transitive V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
Class the of S is non empty with_non-empty_elements a_partition of the carrier' of S
o is non empty Element of (S)
w1 is Element of the carrier' of S
(S,w1) is non empty Element of (S)
Class ( the of S,w1) is Element of K10( the carrier' of S)
lo is (S,o)
(S,lo) is non empty Element of (S)
Class ( the of S,lo) is Element of K10( the carrier' of S)
op2 is set
Class ( the of S,op2) is Element of K10( the carrier' of S)
S is non empty non void V64() reflexive transitive antisymmetric () () () () ()
the carrier' of S is non empty set
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
o is (S) (S) Element of the carrier' of S
w1 is (S) (S) Element of the carrier' of S
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_arity_of w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
lo is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
(S,o,lo) is (S) (S) Element of the carrier' of S
(S,w1,lo) is (S) (S) Element of the carrier' of S
the_arity_of (S,w1,lo) is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
op1 is (S) (S) Element of the carrier' of S
the_arity_of op1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_arity_of (S,o,lo) is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of (S,w1,lo) is Element of the carrier of S
the_result_sort_of (S,o,lo) is Element of the carrier of S
S is non empty non void V64() reflexive transitive antisymmetric () () () () ()
the carrier' of S is non empty set
K10( the carrier' of S) is non empty set
(S) is non empty Element of K10(K10( the carrier' of S))
K10(K10( the carrier' of S)) is non empty set
the of S is Relation-like the carrier' of S -defined the carrier' of S -valued reflexive symmetric transitive V25( the carrier' of S) Element of K10(K11( the carrier' of S, the carrier' of S))
K11( the carrier' of S, the carrier' of S) is non empty Relation-like set
K10(K11( the carrier' of S, the carrier' of S)) is non empty set
Class the of S is non empty with_non-empty_elements a_partition of the carrier' of S
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
o is non empty Element of (S)
w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
lo is (S,o)
the_arity_of lo is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
lo is (S,o)
the_arity_of lo is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
(S,lo,w1) is (S) (S) Element of the carrier' of S
(S,lo) is non empty Element of (S)
Class ( the of S,lo) is Element of K10( the carrier' of S)
(S,(S,lo,w1)) is non empty Element of (S)
Class ( the of S,(S,lo,w1)) is Element of K10( the carrier' of S)
op is (S,o)
op1 is (S,o)
the_arity_of op1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
(S,op1,w1) is (S) (S) Element of the carrier' of S
(S,op1) is non empty Element of (S)
Class ( the of S,op1) is Element of K10( the carrier' of S)
lo is (S,o)
op2 is (S,o)
op is (S,o)
the_arity_of op is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
op is (S,o)
the_arity_of op is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
(S,op,w1) is (S) (S) Element of the carrier' of S
S is non empty non void V64() reflexive transitive antisymmetric () () () () ()
the carrier' of S is non empty set
the carrier of S is non empty set
the carrier of S * is non empty functional FinSequence-membered M37( the carrier of S)
o is (S) (S) Element of the carrier' of S
the_arity_of o is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
w1 is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *
(S,o,w1) is (S) (S) Element of the carrier' of S
the_result_sort_of (S,o,w1) is Element of the carrier of S
the_result_sort_of o is Element of the carrier of S
the_arity_of (S,o,w1) is Relation-like K162() -defined the carrier of S -valued Function-like V43() FinSequence-like FinSubsequence-like Element of the carrier of S *