:: OSALG_1 semantic presentation

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-