:: ENDALG semantic presentation

K119() is non empty V24() V25() V26() Element of bool K115()
K115() is set
bool K115() is set
K92() is non empty V24() V25() V26() set
bool K92() is set
bool K119() is set
K290() is set
{} is Function-like functional empty V24() V25() V26() V28() V29() V30() set
the Function-like functional empty V24() V25() V26() V28() V29() V30() set is Function-like functional empty V24() V25() V26() V28() V29() V30() set
1 is non empty set
0 is Function-like functional empty V24() V25() V26() V28() V29() V30() Element of K119()
{0} is non empty set
K268({0}) is M12({0})
K272(0) is Relation-like K119() -defined K268({0}) -valued Function-like quasi_total Element of bool [:K119(),K268({0}):]
[:K119(),K268({0}):] is set
bool [:K119(),K268({0}):] is set
UA is non empty V157() quasi_total non-empty UAStr
the carrier of UA is non empty set
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
Funcs ( the carrier of UA, the carrier of UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
{ b₁ where b₁ is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of Funcs ( the carrier of UA, the carrier of UA) : b₁ is_homomorphism UA,UA } is set
id the carrier of UA is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like one-to-one non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
H is set
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of Funcs ( the carrier of UA, the carrier of UA)
H is functional non empty set
h is Relation-like Function-like Element of H
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of Funcs ( the carrier of UA, the carrier of UA)
h is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of Funcs ( the carrier of UA, the carrier of UA)
G is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
H is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of H
h is set
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of G
h is set
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
UA is non empty V157() quasi_total non-empty UAStr
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
the carrier of UA is non empty set
Funcs ( the carrier of UA, the carrier of UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
G is set
UA is non empty V157() quasi_total non-empty UAStr
the carrier of UA is non empty set
id the carrier of UA is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like one-to-one non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
UA is non empty V157() quasi_total non-empty UAStr
the carrier of UA is non empty set
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
H is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
G * H is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
UA is non empty V157() quasi_total non-empty UAStr
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
the carrier of UA is non empty set
[:(UA),(UA):] is set
[:[:(UA),(UA):],(UA):] is set
bool [:[:(UA),(UA):],(UA):] is set
G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
H is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
H * G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
h * h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
G is Relation-like [:(UA),(UA):] -defined (UA) -valued Function-like V14([:(UA),(UA):]) quasi_total Element of bool [:[:(UA),(UA):],(UA):]
G is Relation-like [:(UA),(UA):] -defined (UA) -valued Function-like V14([:(UA),(UA):]) quasi_total Element of bool [:[:(UA),(UA):],(UA):]
H is Relation-like [:(UA),(UA):] -defined (UA) -valued Function-like V14([:(UA),(UA):]) quasi_total Element of bool [:[:(UA),(UA):],(UA):]
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
G . (h,h) is Relation-like Function-like Element of (UA)
H . (h,h) is Relation-like Function-like Element of (UA)
h * h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
UA is non empty V157() quasi_total non-empty UAStr
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
the carrier of UA is non empty set
(UA) is Relation-like [:(UA),(UA):] -defined (UA) -valued Function-like V14([:(UA),(UA):]) quasi_total Element of bool [:[:(UA),(UA):],(UA):]
[:(UA),(UA):] is set
[:[:(UA),(UA):],(UA):] is set
bool [:[:(UA),(UA):],(UA):] is set
id the carrier of UA is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like one-to-one non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
multLoopStr(# (UA),(UA),G #) is non empty strict multLoopStr
the carrier of multLoopStr(# (UA),(UA),G #) is non empty set
the multF of multLoopStr(# (UA),(UA),G #) is Relation-like [: the carrier of multLoopStr(# (UA),(UA),G #), the carrier of multLoopStr(# (UA),(UA),G #):] -defined the carrier of multLoopStr(# (UA),(UA),G #) -valued Function-like V14([: the carrier of multLoopStr(# (UA),(UA),G #), the carrier of multLoopStr(# (UA),(UA),G #):]) quasi_total Element of bool [:[: the carrier of multLoopStr(# (UA),(UA),G #), the carrier of multLoopStr(# (UA),(UA),G #):], the carrier of multLoopStr(# (UA),(UA),G #):]
[: the carrier of multLoopStr(# (UA),(UA),G #), the carrier of multLoopStr(# (UA),(UA),G #):] is set
[:[: the carrier of multLoopStr(# (UA),(UA),G #), the carrier of multLoopStr(# (UA),(UA),G #):], the carrier of multLoopStr(# (UA),(UA),G #):] is set
bool [:[: the carrier of multLoopStr(# (UA),(UA),G #), the carrier of multLoopStr(# (UA),(UA),G #):], the carrier of multLoopStr(# (UA),(UA),G #):] is set
1. multLoopStr(# (UA),(UA),G #) is Element of the carrier of multLoopStr(# (UA),(UA),G #)
the OneF of multLoopStr(# (UA),(UA),G #) is Element of the carrier of multLoopStr(# (UA),(UA),G #)
G is strict multLoopStr
the carrier of G is set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
1. G is Element of the carrier of G
the OneF of G is Element of the carrier of G
H is strict multLoopStr
the carrier of H is set
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
1. H is Element of the carrier of H
the OneF of H is Element of the carrier of H
UA is non empty V157() quasi_total non-empty UAStr
(UA) is strict multLoopStr
the carrier of UA is non empty set
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
id the carrier of UA is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like one-to-one non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
(UA) is Relation-like [:(UA),(UA):] -defined (UA) -valued Function-like V14([:(UA),(UA):]) quasi_total Element of bool [:[:(UA),(UA):],(UA):]
[:(UA),(UA):] is set
[:[:(UA),(UA):],(UA):] is set
bool [:[:(UA),(UA):],(UA):] is set
G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
multLoopStr(# (UA),(UA),G #) is non empty strict multLoopStr
1. multLoopStr(# (UA),(UA),G #) is Element of the carrier of multLoopStr(# (UA),(UA),G #)
the carrier of multLoopStr(# (UA),(UA),G #) is non empty set
the OneF of multLoopStr(# (UA),(UA),G #) is Element of the carrier of multLoopStr(# (UA),(UA),G #)
UA is non empty V157() quasi_total non-empty UAStr
(UA) is non empty strict multLoopStr
the carrier of (UA) is non empty set
the carrier of UA is non empty set
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
H is Element of the carrier of (UA)
G is Element of the carrier of (UA)
id the carrier of UA is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like one-to-one non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
G * H is Element of the carrier of (UA)
the multF of (UA) is Relation-like [: the carrier of (UA), the carrier of (UA):] -defined the carrier of (UA) -valued Function-like V14([: the carrier of (UA), the carrier of (UA):]) quasi_total Element of bool [:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):]
[: the carrier of (UA), the carrier of (UA):] is set
[:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is set
bool [:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is set
the multF of (UA) . (G,H) is Element of the carrier of (UA)
(UA) is Relation-like [:(UA),(UA):] -defined (UA) -valued Function-like V14([:(UA),(UA):]) quasi_total Element of bool [:[:(UA),(UA):],(UA):]
[:(UA),(UA):] is set
[:[:(UA),(UA):],(UA):] is set
bool [:[:(UA),(UA):],(UA):] is set
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
(UA) . (h,h) is Relation-like Function-like Element of (UA)
h * h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
H * G is Element of the carrier of (UA)
the multF of (UA) . (H,G) is Element of the carrier of (UA)
(UA) . (h,h) is Relation-like Function-like Element of (UA)
h * h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
UA is non empty V157() quasi_total non-empty UAStr
(UA) is non empty strict multLoopStr
the carrier of UA is non empty set
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
id the carrier of UA is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like one-to-one non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
(UA) is Relation-like [:(UA),(UA):] -defined (UA) -valued Function-like V14([:(UA),(UA):]) quasi_total Element of bool [:[:(UA),(UA):],(UA):]
[:(UA),(UA):] is set
[:[:(UA),(UA):],(UA):] is set
bool [:[:(UA),(UA):],(UA):] is set
G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
multLoopStr(# (UA),(UA),G #) is non empty strict multLoopStr
the carrier of (UA) is non empty set
h is Element of the carrier of (UA)
1. (UA) is Element of the carrier of (UA)
the OneF of (UA) is Element of the carrier of (UA)
h * (1. (UA)) is Element of the carrier of (UA)
the multF of (UA) is Relation-like [: the carrier of (UA), the carrier of (UA):] -defined the carrier of (UA) -valued Function-like V14([: the carrier of (UA), the carrier of (UA):]) quasi_total Element of bool [:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):]
[: the carrier of (UA), the carrier of (UA):] is set
[:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is set
bool [:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is set
the multF of (UA) . (h,(1. (UA))) is Element of the carrier of (UA)
(1. (UA)) * h is Element of the carrier of (UA)
the multF of (UA) . ((1. (UA)),h) is Element of the carrier of (UA)
the carrier of multLoopStr(# (UA),(UA),G #) is non empty set
h is Element of the carrier of multLoopStr(# (UA),(UA),G #)
h is Element of the carrier of multLoopStr(# (UA),(UA),G #)
h * h is Element of the carrier of multLoopStr(# (UA),(UA),G #)
the multF of multLoopStr(# (UA),(UA),G #) is Relation-like [: the carrier of multLoopStr(# (UA),(UA),G #), the carrier of multLoopStr(# (UA),(UA),G #):] -defined the carrier of multLoopStr(# (UA),(UA),G #) -valued Function-like V14([: the carrier of multLoopStr(# (UA),(UA),G #), the carrier of multLoopStr(# (UA),(UA),G #):]) quasi_total Element of bool [:[: the carrier of multLoopStr(# (UA),(UA),G #), the carrier of multLoopStr(# (UA),(UA),G #):], the carrier of multLoopStr(# (UA),(UA),G #):]
[: the carrier of multLoopStr(# (UA),(UA),G #), the carrier of multLoopStr(# (UA),(UA),G #):] is set
[:[: the carrier of multLoopStr(# (UA),(UA),G #), the carrier of multLoopStr(# (UA),(UA),G #):], the carrier of multLoopStr(# (UA),(UA),G #):] is set
bool [:[: the carrier of multLoopStr(# (UA),(UA),G #), the carrier of multLoopStr(# (UA),(UA),G #):], the carrier of multLoopStr(# (UA),(UA),G #):] is set
the multF of multLoopStr(# (UA),(UA),G #) . (h,h) is Element of the carrier of multLoopStr(# (UA),(UA),G #)
G is Element of the carrier of multLoopStr(# (UA),(UA),G #)
(h * h) * G is Element of the carrier of multLoopStr(# (UA),(UA),G #)
the multF of multLoopStr(# (UA),(UA),G #) . ((h * h),G) is Element of the carrier of multLoopStr(# (UA),(UA),G #)
h * G is Element of the carrier of multLoopStr(# (UA),(UA),G #)
the multF of multLoopStr(# (UA),(UA),G #) . (h,G) is Element of the carrier of multLoopStr(# (UA),(UA),G #)
h * (h * G) is Element of the carrier of multLoopStr(# (UA),(UA),G #)
the multF of multLoopStr(# (UA),(UA),G #) . (h,(h * G)) is Element of the carrier of multLoopStr(# (UA),(UA),G #)
M is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
a is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
a * M is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
H is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
M * H is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
a * (M * H) is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
(a * M) * H is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
1. multLoopStr(# (UA),(UA),G #) is Element of the carrier of multLoopStr(# (UA),(UA),G #)
the OneF of multLoopStr(# (UA),(UA),G #) is Element of the carrier of multLoopStr(# (UA),(UA),G #)
UA is non empty V157() quasi_total non-empty UAStr
(UA) is non empty strict unital associative right_unital well-unital left_unital multLoopStr
the carrier of (UA) is non empty set
the carrier of UA is non empty set
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
id the carrier of UA is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like one-to-one non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
H is Element of the carrier of (UA)
h is Element of the carrier of (UA)
H * h is Element of the carrier of (UA)
the multF of (UA) is Relation-like [: the carrier of (UA), the carrier of (UA):] -defined the carrier of (UA) -valued Function-like V14([: the carrier of (UA), the carrier of (UA):]) quasi_total Element of bool [:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):]
[: the carrier of (UA), the carrier of (UA):] is set
[:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is set
bool [:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is set
the multF of (UA) . (H,h) is Element of the carrier of (UA)
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
G * h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
(UA) is Relation-like [:(UA),(UA):] -defined (UA) -valued Function-like V14([:(UA),(UA):]) quasi_total Element of bool [:[:(UA),(UA):],(UA):]
[:(UA),(UA):] is set
[:[:(UA),(UA):],(UA):] is set
bool [:[:(UA),(UA):],(UA):] is set
G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
multLoopStr(# (UA),(UA),G #) is non empty strict multLoopStr
1. multLoopStr(# (UA),(UA),G #) is Element of the carrier of multLoopStr(# (UA),(UA),G #)
the carrier of multLoopStr(# (UA),(UA),G #) is non empty set
the OneF of multLoopStr(# (UA),(UA),G #) is Element of the carrier of multLoopStr(# (UA),(UA),G #)
UA is non empty V157() quasi_total non-empty UAStr
the carrier of UA is non empty set
id the carrier of UA is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like one-to-one non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
(UA) is non empty strict unital associative right_unital well-unital left_unital multLoopStr
1_ (UA) is Element of the carrier of (UA)
the carrier of (UA) is non empty set
1. (UA) is Element of the carrier of (UA)
the OneF of (UA) is Element of the carrier of (UA)
UA is non empty non void V59() ManySortedSign
G is non-empty MSAlgebra over UA
the Sorts of G is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
the carrier of UA is non empty set
MSFuncs ( the Sorts of G, the Sorts of G) is non empty set
bool (MSFuncs ( the Sorts of G, the Sorts of G)) is set
h is set
id the Sorts of G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding "1-1" "onto" ManySortedFunction of the Sorts of G, the Sorts of G
G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
h is non empty set
G is set
G is non empty Element of bool (MSFuncs ( the Sorts of G, the Sorts of G))
H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of G
H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
M is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
h is non empty Element of bool (MSFuncs ( the Sorts of G, the Sorts of G))
h is non empty Element of bool (MSFuncs ( the Sorts of G, the Sorts of G))
G is set
H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
G is set
H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
UA is non empty non void V59() ManySortedSign
G is non-empty MSAlgebra over UA
(UA,G) is non empty Element of bool (MSFuncs ( the Sorts of G, the Sorts of G))
the carrier of UA is non empty set
the Sorts of G is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
MSFuncs ( the Sorts of G, the Sorts of G) is non empty set
bool (MSFuncs ( the Sorts of G, the Sorts of G)) is set
UA is non empty non void V59() ManySortedSign
the carrier of UA is non empty set
G is non-empty MSAlgebra over UA
the Sorts of G is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
id the Sorts of G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding "1-1" "onto" ManySortedFunction of the Sorts of G, the Sorts of G
(UA,G) is non empty Element of bool (MSFuncs ( the Sorts of G, the Sorts of G))
MSFuncs ( the Sorts of G, the Sorts of G) is non empty set
bool (MSFuncs ( the Sorts of G, the Sorts of G)) is set
UA is non empty non void V59() ManySortedSign
the carrier of UA is non empty set
G is non-empty MSAlgebra over UA
the Sorts of G is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
(UA,G) is non empty Element of bool (MSFuncs ( the Sorts of G, the Sorts of G))
MSFuncs ( the Sorts of G, the Sorts of G) is non empty set
bool (MSFuncs ( the Sorts of G, the Sorts of G)) is set
h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
H ** h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
UA is non empty V157() quasi_total non-empty UAStr
MSSign UA is non empty trivial V53() non void 1 -element V59() strict segmental ManySortedSign
the carrier of (MSSign UA) is non empty trivial V31() set
MSAlg UA is strict non-empty MSAlgebra over MSSign UA
the Sorts of (MSAlg UA) is Relation-like non-empty non empty-yielding the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) set
the carrier of UA is non empty set
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
((MSSign UA),(MSAlg UA)) is non empty Element of bool (MSFuncs ( the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)))
MSFuncs ( the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)) is non empty set
bool (MSFuncs ( the Sorts of (MSAlg UA), the Sorts of (MSAlg UA))) is set
G is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)
H is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
0 .--> H is set
{0} --> H is Relation-like {0} -defined {H} -valued Function-like non empty V14({0}) quasi_total Element of bool [:{0},{H}:]
{H} is functional non empty set
[:{0},{H}:] is set
bool [:{0},{H}:] is set
MSAlg H is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of ((MSAlg UA) Over (MSSign UA))
(MSAlg UA) Over (MSSign UA) is strict non-empty MSAlgebra over MSSign UA
the Sorts of ((MSAlg UA) Over (MSSign UA)) is Relation-like non-empty non empty-yielding the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) set
UA is non empty non void V59() ManySortedSign
G is non-empty MSAlgebra over UA
(UA,G) is non empty Element of bool (MSFuncs ( the Sorts of G, the Sorts of G))
the carrier of UA is non empty set
the Sorts of G is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
MSFuncs ( the Sorts of G, the Sorts of G) is non empty set
bool (MSFuncs ( the Sorts of G, the Sorts of G)) is set
[:(UA,G),(UA,G):] is set
[:[:(UA,G),(UA,G):],(UA,G):] is set
bool [:[:(UA,G),(UA,G):],(UA,G):] is set
H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
h ** H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
G ** h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
H is Relation-like [:(UA,G),(UA,G):] -defined (UA,G) -valued Function-like V14([:(UA,G),(UA,G):]) quasi_total Element of bool [:[:(UA,G),(UA,G):],(UA,G):]
H is Relation-like [:(UA,G),(UA,G):] -defined (UA,G) -valued Function-like V14([:(UA,G),(UA,G):]) quasi_total Element of bool [:[:(UA,G),(UA,G):],(UA,G):]
h is Relation-like [:(UA,G),(UA,G):] -defined (UA,G) -valued Function-like V14([:(UA,G),(UA,G):]) quasi_total Element of bool [:[:(UA,G),(UA,G):],(UA,G):]
h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
H . (h,G) is Element of (UA,G)
h . (h,G) is Element of (UA,G)
G ** h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
UA is non empty non void V59() ManySortedSign
G is non-empty MSAlgebra over UA
(UA,G) is non empty Element of bool (MSFuncs ( the Sorts of G, the Sorts of G))
the carrier of UA is non empty set
the Sorts of G is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
MSFuncs ( the Sorts of G, the Sorts of G) is non empty set
bool (MSFuncs ( the Sorts of G, the Sorts of G)) is set
(UA,G) is Relation-like [:(UA,G),(UA,G):] -defined (UA,G) -valued Function-like V14([:(UA,G),(UA,G):]) quasi_total Element of bool [:[:(UA,G),(UA,G):],(UA,G):]
[:(UA,G),(UA,G):] is set
[:[:(UA,G),(UA,G):],(UA,G):] is set
bool [:[:(UA,G),(UA,G):],(UA,G):] is set
id the Sorts of G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding "1-1" "onto" ManySortedFunction of the Sorts of G, the Sorts of G
H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
multLoopStr(# (UA,G),(UA,G),H #) is non empty strict multLoopStr
h is non empty strict multLoopStr
the carrier of h is non empty set
the multF of h is Relation-like [: the carrier of h, the carrier of h:] -defined the carrier of h -valued Function-like V14([: the carrier of h, the carrier of h:]) quasi_total Element of bool [:[: the carrier of h, the carrier of h:], the carrier of h:]
[: the carrier of h, the carrier of h:] is set
[:[: the carrier of h, the carrier of h:], the carrier of h:] is set
bool [:[: the carrier of h, the carrier of h:], the carrier of h:] is set
1. h is Element of the carrier of h
the OneF of h is Element of the carrier of h
H is strict multLoopStr
the carrier of H is set
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
1. H is Element of the carrier of H
the OneF of H is Element of the carrier of H
h is strict multLoopStr
the carrier of h is set
the multF of h is Relation-like [: the carrier of h, the carrier of h:] -defined the carrier of h -valued Function-like quasi_total Element of bool [:[: the carrier of h, the carrier of h:], the carrier of h:]
[: the carrier of h, the carrier of h:] is set
[:[: the carrier of h, the carrier of h:], the carrier of h:] is set
bool [:[: the carrier of h, the carrier of h:], the carrier of h:] is set
1. h is Element of the carrier of h
the OneF of h is Element of the carrier of h
UA is non empty non void V59() ManySortedSign
G is non-empty MSAlgebra over UA
(UA,G) is strict multLoopStr
the carrier of UA is non empty set
the Sorts of G is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
(UA,G) is non empty Element of bool (MSFuncs ( the Sorts of G, the Sorts of G))
MSFuncs ( the Sorts of G, the Sorts of G) is non empty set
bool (MSFuncs ( the Sorts of G, the Sorts of G)) is set
id the Sorts of G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding "1-1" "onto" ManySortedFunction of the Sorts of G, the Sorts of G
(UA,G) is Relation-like [:(UA,G),(UA,G):] -defined (UA,G) -valued Function-like V14([:(UA,G),(UA,G):]) quasi_total Element of bool [:[:(UA,G),(UA,G):],(UA,G):]
[:(UA,G),(UA,G):] is set
[:[:(UA,G),(UA,G):],(UA,G):] is set
bool [:[:(UA,G),(UA,G):],(UA,G):] is set
H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
multLoopStr(# (UA,G),(UA,G),H #) is non empty strict multLoopStr
1. multLoopStr(# (UA,G),(UA,G),H #) is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
the carrier of multLoopStr(# (UA,G),(UA,G),H #) is non empty set
the OneF of multLoopStr(# (UA,G),(UA,G),H #) is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
UA is non empty non void V59() ManySortedSign
G is non-empty MSAlgebra over UA
(UA,G) is non empty strict multLoopStr
the carrier of (UA,G) is non empty set
the carrier of UA is non empty set
the Sorts of G is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
(UA,G) is non empty Element of bool (MSFuncs ( the Sorts of G, the Sorts of G))
MSFuncs ( the Sorts of G, the Sorts of G) is non empty set
bool (MSFuncs ( the Sorts of G, the Sorts of G)) is set
h is Element of the carrier of (UA,G)
h is Element of the carrier of (UA,G)
id the Sorts of G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding "1-1" "onto" ManySortedFunction of the Sorts of G, the Sorts of G
h * h is Element of the carrier of (UA,G)
the multF of (UA,G) is Relation-like [: the carrier of (UA,G), the carrier of (UA,G):] -defined the carrier of (UA,G) -valued Function-like V14([: the carrier of (UA,G), the carrier of (UA,G):]) quasi_total Element of bool [:[: the carrier of (UA,G), the carrier of (UA,G):], the carrier of (UA,G):]
[: the carrier of (UA,G), the carrier of (UA,G):] is set
[:[: the carrier of (UA,G), the carrier of (UA,G):], the carrier of (UA,G):] is set
bool [:[: the carrier of (UA,G), the carrier of (UA,G):], the carrier of (UA,G):] is set
the multF of (UA,G) . (h,h) is Element of the carrier of (UA,G)
(UA,G) is Relation-like [:(UA,G),(UA,G):] -defined (UA,G) -valued Function-like V14([:(UA,G),(UA,G):]) quasi_total Element of bool [:[:(UA,G),(UA,G):],(UA,G):]
[:(UA,G),(UA,G):] is set
[:[:(UA,G),(UA,G):],(UA,G):] is set
bool [:[:(UA,G),(UA,G):],(UA,G):] is set
H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
(UA,G) . (H,G) is Element of (UA,G)
G ** H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
h * h is Element of the carrier of (UA,G)
the multF of (UA,G) . (h,h) is Element of the carrier of (UA,G)
(UA,G) . (G,H) is Element of (UA,G)
H ** G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
UA is non empty non void V59() ManySortedSign
G is non-empty MSAlgebra over UA
(UA,G) is non empty strict multLoopStr
the carrier of UA is non empty set
the Sorts of G is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
(UA,G) is non empty Element of bool (MSFuncs ( the Sorts of G, the Sorts of G))
MSFuncs ( the Sorts of G, the Sorts of G) is non empty set
bool (MSFuncs ( the Sorts of G, the Sorts of G)) is set
id the Sorts of G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding "1-1" "onto" ManySortedFunction of the Sorts of G, the Sorts of G
(UA,G) is Relation-like [:(UA,G),(UA,G):] -defined (UA,G) -valued Function-like V14([:(UA,G),(UA,G):]) quasi_total Element of bool [:[:(UA,G),(UA,G):],(UA,G):]
[:(UA,G),(UA,G):] is set
[:[:(UA,G),(UA,G):],(UA,G):] is set
bool [:[:(UA,G),(UA,G):],(UA,G):] is set
H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
multLoopStr(# (UA,G),(UA,G),H #) is non empty strict multLoopStr
the carrier of (UA,G) is non empty set
h is Element of the carrier of (UA,G)
1. (UA,G) is Element of the carrier of (UA,G)
the OneF of (UA,G) is Element of the carrier of (UA,G)
h * (1. (UA,G)) is Element of the carrier of (UA,G)
the multF of (UA,G) is Relation-like [: the carrier of (UA,G), the carrier of (UA,G):] -defined the carrier of (UA,G) -valued Function-like V14([: the carrier of (UA,G), the carrier of (UA,G):]) quasi_total Element of bool [:[: the carrier of (UA,G), the carrier of (UA,G):], the carrier of (UA,G):]
[: the carrier of (UA,G), the carrier of (UA,G):] is set
[:[: the carrier of (UA,G), the carrier of (UA,G):], the carrier of (UA,G):] is set
bool [:[: the carrier of (UA,G), the carrier of (UA,G):], the carrier of (UA,G):] is set
the multF of (UA,G) . (h,(1. (UA,G))) is Element of the carrier of (UA,G)
(1. (UA,G)) * h is Element of the carrier of (UA,G)
the multF of (UA,G) . ((1. (UA,G)),h) is Element of the carrier of (UA,G)
the carrier of multLoopStr(# (UA,G),(UA,G),H #) is non empty set
h is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
G is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
h * G is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
the multF of multLoopStr(# (UA,G),(UA,G),H #) is Relation-like [: the carrier of multLoopStr(# (UA,G),(UA,G),H #), the carrier of multLoopStr(# (UA,G),(UA,G),H #):] -defined the carrier of multLoopStr(# (UA,G),(UA,G),H #) -valued Function-like V14([: the carrier of multLoopStr(# (UA,G),(UA,G),H #), the carrier of multLoopStr(# (UA,G),(UA,G),H #):]) quasi_total Element of bool [:[: the carrier of multLoopStr(# (UA,G),(UA,G),H #), the carrier of multLoopStr(# (UA,G),(UA,G),H #):], the carrier of multLoopStr(# (UA,G),(UA,G),H #):]
[: the carrier of multLoopStr(# (UA,G),(UA,G),H #), the carrier of multLoopStr(# (UA,G),(UA,G),H #):] is set
[:[: the carrier of multLoopStr(# (UA,G),(UA,G),H #), the carrier of multLoopStr(# (UA,G),(UA,G),H #):], the carrier of multLoopStr(# (UA,G),(UA,G),H #):] is set
bool [:[: the carrier of multLoopStr(# (UA,G),(UA,G),H #), the carrier of multLoopStr(# (UA,G),(UA,G),H #):], the carrier of multLoopStr(# (UA,G),(UA,G),H #):] is set
the multF of multLoopStr(# (UA,G),(UA,G),H #) . (h,G) is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
H is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
(h * G) * H is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
the multF of multLoopStr(# (UA,G),(UA,G),H #) . ((h * G),H) is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
G * H is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
the multF of multLoopStr(# (UA,G),(UA,G),H #) . (G,H) is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
h * (G * H) is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
the multF of multLoopStr(# (UA,G),(UA,G),H #) . (h,(G * H)) is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
a is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
b ** a is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
M is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
a ** M is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
b ** (a ** M) is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
(b ** a) ** M is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
1. multLoopStr(# (UA,G),(UA,G),H #) is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
the OneF of multLoopStr(# (UA,G),(UA,G),H #) is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
UA is non empty non void V59() ManySortedSign
the carrier of UA is non empty set
G is non-empty MSAlgebra over UA
(UA,G) is non empty strict unital associative right_unital well-unital left_unital multLoopStr
the carrier of (UA,G) is non empty set
the Sorts of G is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
(UA,G) is non empty Element of bool (MSFuncs ( the Sorts of G, the Sorts of G))
MSFuncs ( the Sorts of G, the Sorts of G) is non empty set
bool (MSFuncs ( the Sorts of G, the Sorts of G)) is set
id the Sorts of G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding "1-1" "onto" ManySortedFunction of the Sorts of G, the Sorts of G
h is Element of the carrier of (UA,G)
h is Element of the carrier of (UA,G)
h * h is Element of the carrier of (UA,G)
the multF of (UA,G) is Relation-like [: the carrier of (UA,G), the carrier of (UA,G):] -defined the carrier of (UA,G) -valued Function-like V14([: the carrier of (UA,G), the carrier of (UA,G):]) quasi_total Element of bool [:[: the carrier of (UA,G), the carrier of (UA,G):], the carrier of (UA,G):]
[: the carrier of (UA,G), the carrier of (UA,G):] is set
[:[: the carrier of (UA,G), the carrier of (UA,G):], the carrier of (UA,G):] is set
bool [:[: the carrier of (UA,G), the carrier of (UA,G):], the carrier of (UA,G):] is set
the multF of (UA,G) . (h,h) is Element of the carrier of (UA,G)
G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
H ** G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding ManySortedFunction of the Sorts of G, the Sorts of G
(UA,G) is Relation-like [:(UA,G),(UA,G):] -defined (UA,G) -valued Function-like V14([:(UA,G),(UA,G):]) quasi_total Element of bool [:[:(UA,G),(UA,G):],(UA,G):]
[:(UA,G),(UA,G):] is set
[:[:(UA,G),(UA,G):],(UA,G):] is set
bool [:[:(UA,G),(UA,G):],(UA,G):] is set
H is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding Element of (UA,G)
multLoopStr(# (UA,G),(UA,G),H #) is non empty strict multLoopStr
1. multLoopStr(# (UA,G),(UA,G),H #) is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
the carrier of multLoopStr(# (UA,G),(UA,G),H #) is non empty set
the OneF of multLoopStr(# (UA,G),(UA,G),H #) is Element of the carrier of multLoopStr(# (UA,G),(UA,G),H #)
UA is non empty non void V59() ManySortedSign
the carrier of UA is non empty set
G is non-empty MSAlgebra over UA
the Sorts of G is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
id the Sorts of G is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding "1-1" "onto" ManySortedFunction of the Sorts of G, the Sorts of G
(UA,G) is non empty strict unital associative right_unital well-unital left_unital multLoopStr
1_ (UA,G) is Element of the carrier of (UA,G)
the carrier of (UA,G) is non empty set
1. (UA,G) is Element of the carrier of (UA,G)
the OneF of (UA,G) is Element of the carrier of (UA,G)
UA is non empty V157() quasi_total non-empty UAStr
the carrier of UA is non empty set
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
MSSign UA is non empty trivial V53() non void 1 -element V59() strict segmental ManySortedSign
the carrier of (MSSign UA) is non empty trivial V31() set
MSAlg UA is strict non-empty MSAlgebra over MSSign UA
the Sorts of (MSAlg UA) is Relation-like non-empty non empty-yielding the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) set
G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
0 .--> G is set
{0} --> G is Relation-like {0} -defined {G} -valued Function-like non empty V14({0}) quasi_total Element of bool [:{0},{G}:]
{G} is functional non empty set
[:{0},{G}:] is set
bool [:{0},{G}:] is set
MSAlg G is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of ((MSAlg UA) Over (MSSign UA))
(MSAlg UA) Over (MSSign UA) is strict non-empty MSAlgebra over MSSign UA
the Sorts of ((MSAlg UA) Over (MSSign UA)) is Relation-like non-empty non empty-yielding the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) set
UA is non empty V157() quasi_total non-empty UAStr
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
the carrier of UA is non empty set
MSSign UA is non empty trivial V53() non void 1 -element V59() strict segmental ManySortedSign
MSAlg UA is strict non-empty MSAlgebra over MSSign UA
((MSSign UA),(MSAlg UA)) is non empty Element of bool (MSFuncs ( the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)))
the carrier of (MSSign UA) is non empty trivial V31() set
the Sorts of (MSAlg UA) is Relation-like non-empty non empty-yielding the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) set
MSFuncs ( the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)) is non empty set
bool (MSFuncs ( the Sorts of (MSAlg UA), the Sorts of (MSAlg UA))) is set
G is Relation-like Function-like set
dom G is set
rng G is set
H is set
h is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)
h . 0 is set
0 .--> (h . 0) is set
{0} --> (h . 0) is Relation-like {0} -defined {(h . 0)} -valued Function-like non empty V14({0}) quasi_total Element of bool [:{0},{(h . 0)}:]
{(h . 0)} is non empty set
[:{0},{(h . 0)}:] is set
bool [:{0},{(h . 0)}:] is set
h is set
G . h is set
(MSAlg UA) Over (MSSign UA) is strict non-empty MSAlgebra over MSSign UA
the Sorts of ((MSAlg UA) Over (MSSign UA)) is Relation-like non-empty non empty-yielding the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) set
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
MSAlg G is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of ((MSAlg UA) Over (MSSign UA))
h is set
G . h is set
H is set
h is set
G . h is set
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
0 .--> h is set
{0} --> h is Relation-like {0} -defined {h} -valued Function-like non empty V14({0}) quasi_total Element of bool [:{0},{h}:]
{h} is non empty set
[:{0},{h}:] is set
bool [:{0},{h}:] is set
G is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)
(MSAlg UA) Over (MSSign UA) is strict non-empty MSAlgebra over MSSign UA
MSAlg h is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of ((MSAlg UA) Over (MSSign UA))
the Sorts of ((MSAlg UA) Over (MSSign UA)) is Relation-like non-empty non empty-yielding the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) set
[:{0},{0}:] is set
[:[:{0},{0}:],{0}:] is set
bool [:[:{0},{0}:],{0}:] is set
the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:] is Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:]
the Element of {0} is Element of {0}
multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #) is non empty strict multLoopStr
the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #) is non empty set
1. multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #) is Element of the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #)
the OneF of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #) is Element of the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #)
H is Element of the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #)
(1. multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #)) * H is Element of the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #)
the multF of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #) is Relation-like [: the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #), the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #):] -defined the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #) -valued Function-like V14([: the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #), the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #):]) quasi_total Element of bool [:[: the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #), the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #):], the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #):]
[: the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #), the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #):] is set
[:[: the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #), the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #):], the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #):] is set
bool [:[: the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #), the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #):], the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #):] is set
the multF of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #) . ((1. multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #)),H) is Element of the carrier of multLoopStr(# {0}, the Relation-like [:{0},{0}:] -defined {0} -valued Function-like V14([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the Element of {0} #)
UA is non empty unital right_unital well-unital left_unital multLoopStr
the carrier of UA is non empty set
G is non empty unital right_unital well-unital left_unital multLoopStr
the carrier of G is non empty set
[: the carrier of UA, the carrier of G:] is set
bool [: the carrier of UA, the carrier of G:] is set
1. G is Element of the carrier of G
the OneF of G is Element of the carrier of G
the carrier of UA --> (1. G) is Relation-like the carrier of UA -defined the carrier of G -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of G:]
{(1. G)} is non empty set
[: the carrier of UA,{(1. G)}:] is set
H is Relation-like the carrier of UA -defined the carrier of G -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of G:]
h is Relation-like the carrier of UA -defined the carrier of G -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of G:]
h is Element of the carrier of UA
G is Element of the carrier of UA
h * G is Element of the carrier of UA
the multF of UA is Relation-like [: the carrier of UA, the carrier of UA:] -defined the carrier of UA -valued Function-like V14([: the carrier of UA, the carrier of UA:]) quasi_total Element of bool [:[: the carrier of UA, the carrier of UA:], the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
[:[: the carrier of UA, the carrier of UA:], the carrier of UA:] is set
bool [:[: the carrier of UA, the carrier of UA:], the carrier of UA:] is set
the multF of UA . (h,G) is Element of the carrier of UA
h . (h * G) is Element of the carrier of G
h . h is Element of the carrier of G
h . G is Element of the carrier of G
(h . h) * (h . G) is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V14([: the carrier of G, the carrier of G:]) quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((h . h),(h . G)) is Element of the carrier of G
(1. G) * (1. G) is Element of the carrier of G
the multF of G . ((1. G),(1. G)) is Element of the carrier of G
(h . h) * (1. G) is Element of the carrier of G
the multF of G . ((h . h),(1. G)) is Element of the carrier of G
1_ UA is Element of the carrier of UA
1. UA is Element of the carrier of UA
the OneF of UA is Element of the carrier of UA
h . (1_ UA) is Element of the carrier of G
1_ G is Element of the carrier of G
UA is non empty unital right_unital well-unital left_unital multLoopStr
the carrier of UA is non empty set
id the carrier of UA is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like one-to-one non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
H is Element of the carrier of UA
h is Element of the carrier of UA
H * h is Element of the carrier of UA
the multF of UA is Relation-like [: the carrier of UA, the carrier of UA:] -defined the carrier of UA -valued Function-like V14([: the carrier of UA, the carrier of UA:]) quasi_total Element of bool [:[: the carrier of UA, the carrier of UA:], the carrier of UA:]
[:[: the carrier of UA, the carrier of UA:], the carrier of UA:] is set
bool [:[: the carrier of UA, the carrier of UA:], the carrier of UA:] is set
the multF of UA . (H,h) is Element of the carrier of UA
G . (H * h) is Element of the carrier of UA
G . H is Element of the carrier of UA
G . h is Element of the carrier of UA
(G . H) * (G . h) is Element of the carrier of UA
the multF of UA . ((G . H),(G . h)) is Element of the carrier of UA
(G . H) * h is Element of the carrier of UA
the multF of UA . ((G . H),h) is Element of the carrier of UA
1_ UA is Element of the carrier of UA
1. UA is Element of the carrier of UA
the OneF of UA is Element of the carrier of UA
G . (1_ UA) is Element of the carrier of UA
H is non empty unital right_unital well-unital left_unital multLoopStr
the carrier of H is non empty set
[: the carrier of H, the carrier of H:] is set
bool [: the carrier of H, the carrier of H:] is set
id the carrier of H is Relation-like the carrier of H -defined the carrier of H -valued Function-like one-to-one non empty V14( the carrier of H) quasi_total Element of bool [: the carrier of H, the carrier of H:]
h is Relation-like the carrier of H -defined the carrier of H -valued Function-like non empty V14( the carrier of H) quasi_total unity-preserving multiplicative Element of bool [: the carrier of H, the carrier of H:]
rng h is set
h is set
dom h is set
h . h is set
G is set
h . G is set
UA is non empty V157() quasi_total non-empty UAStr
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
the carrier of UA is non empty set
(UA) is non empty strict unital associative right_unital well-unital left_unital multLoopStr
the carrier of (UA) is non empty set
MSSign UA is non empty trivial V53() non void 1 -element V59() strict segmental ManySortedSign
MSAlg UA is strict non-empty MSAlgebra over MSSign UA
((MSSign UA),(MSAlg UA)) is non empty strict unital associative right_unital well-unital left_unital multLoopStr
the carrier of ((MSSign UA),(MSAlg UA)) is non empty set
[: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):] is set
bool [: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):] is set
the carrier of (MSSign UA) is non empty trivial V31() set
the Sorts of (MSAlg UA) is Relation-like non-empty non empty-yielding the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) set
((MSSign UA),(MSAlg UA)) is non empty Element of bool (MSFuncs ( the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)))
MSFuncs ( the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)) is non empty set
bool (MSFuncs ( the Sorts of (MSAlg UA), the Sorts of (MSAlg UA))) is set
id the Sorts of (MSAlg UA) is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding "1-1" "onto" ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)
((MSSign UA),(MSAlg UA)) is Relation-like [:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):] -defined ((MSSign UA),(MSAlg UA)) -valued Function-like V14([:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):]) quasi_total Element of bool [:[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):],((MSSign UA),(MSAlg UA)):]
[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):] is set
[:[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):],((MSSign UA),(MSAlg UA)):] is set
bool [:[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):],((MSSign UA),(MSAlg UA)):] is set
G is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding Element of ((MSSign UA),(MSAlg UA))
multLoopStr(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)),G #) is non empty strict multLoopStr
id the carrier of UA is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like one-to-one non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
H is Relation-like Function-like set
dom H is set
1. multLoopStr(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)),G #) is Element of the carrier of multLoopStr(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)),G #)
the carrier of multLoopStr(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)),G #) is non empty set
the OneF of multLoopStr(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)),G #) is Element of the carrier of multLoopStr(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)),G #)
rng H is set
M is Relation-like the carrier of (UA) -defined the carrier of ((MSSign UA),(MSAlg UA)) -valued Function-like non empty V14( the carrier of (UA)) quasi_total Element of bool [: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):]
G is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
M . G is set
0 .--> G is set
{0} --> G is Relation-like {0} -defined {G} -valued Function-like non empty V14({0}) quasi_total Element of bool [:{0},{G}:]
{G} is functional non empty set
[:{0},{G}:] is set
bool [:{0},{G}:] is set
a is Element of the carrier of (UA)
b is Element of the carrier of (UA)
a * b is Element of the carrier of (UA)
the multF of (UA) is Relation-like [: the carrier of (UA), the carrier of (UA):] -defined the carrier of (UA) -valued Function-like V14([: the carrier of (UA), the carrier of (UA):]) quasi_total Element of bool [:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):]
[: the carrier of (UA), the carrier of (UA):] is set
[:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is set
bool [:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is set
the multF of (UA) . (a,b) is Element of the carrier of (UA)
M . (a * b) is Element of the carrier of ((MSSign UA),(MSAlg UA))
M . a is Element of the carrier of ((MSSign UA),(MSAlg UA))
M . b is Element of the carrier of ((MSSign UA),(MSAlg UA))
(M . a) * (M . b) is Element of the carrier of ((MSSign UA),(MSAlg UA))
the multF of ((MSSign UA),(MSAlg UA)) is Relation-like [: the carrier of ((MSSign UA),(MSAlg UA)), the carrier of ((MSSign UA),(MSAlg UA)):] -defined the carrier of ((MSSign UA),(MSAlg UA)) -valued Function-like V14([: the carrier of ((MSSign UA),(MSAlg UA)), the carrier of ((MSSign UA),(MSAlg UA)):]) quasi_total Element of bool [:[: the carrier of ((MSSign UA),(MSAlg UA)), the carrier of ((MSSign UA),(MSAlg UA)):], the carrier of ((MSSign UA),(MSAlg UA)):]
[: the carrier of ((MSSign UA),(MSAlg UA)), the carrier of ((MSSign UA),(MSAlg UA)):] is set
[:[: the carrier of ((MSSign UA),(MSAlg UA)), the carrier of ((MSSign UA),(MSAlg UA)):], the carrier of ((MSSign UA),(MSAlg UA)):] is set
bool [:[: the carrier of ((MSSign UA),(MSAlg UA)), the carrier of ((MSSign UA),(MSAlg UA)):], the carrier of ((MSSign UA),(MSAlg UA)):] is set
the multF of ((MSSign UA),(MSAlg UA)) . ((M . a),(M . b)) is Element of the carrier of ((MSSign UA),(MSAlg UA))
a9 is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
0 .--> a9 is set
{0} --> a9 is Relation-like {0} -defined {a9} -valued Function-like non empty V14({0}) quasi_total Element of bool [:{0},{a9}:]
{a9} is functional non empty set
[:{0},{a9}:] is set
bool [:{0},{a9}:] is set
b9 is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
0 .--> b9 is set
{0} --> b9 is Relation-like {0} -defined {b9} -valued Function-like non empty V14({0}) quasi_total Element of bool [:{0},{b9}:]
{b9} is functional non empty set
[:{0},{b9}:] is set
bool [:{0},{b9}:] is set
b9 * a9 is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
M . (b9 * a9) is set
0 .--> (b9 * a9) is set
{0} --> (b9 * a9) is Relation-like {0} -defined {(b9 * a9)} -valued Function-like non empty V14({0}) quasi_total Element of bool [:{0},{(b9 * a9)}:]
{(b9 * a9)} is functional non empty set
[:{0},{(b9 * a9)}:] is set
bool [:{0},{(b9 * a9)}:] is set
A is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)
B is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)
ha is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding Element of ((MSSign UA),(MSAlg UA))
A9 is Element of the carrier of ((MSSign UA),(MSAlg UA))
hb is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding Element of ((MSSign UA),(MSAlg UA))
B9 is Element of the carrier of ((MSSign UA),(MSAlg UA))
MSAlg (b9 * a9) is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of ((MSAlg UA) Over (MSSign UA))
(MSAlg UA) Over (MSSign UA) is strict non-empty MSAlgebra over MSSign UA
the Sorts of ((MSAlg UA) Over (MSSign UA)) is Relation-like non-empty non empty-yielding the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) set
MSAlg a9 is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of ((MSAlg UA) Over (MSSign UA))
MSAlg b9 is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of ((MSAlg UA) Over (MSSign UA))
(MSAlg b9) ** (MSAlg a9) is Relation-like Function-like Function-yielding set
B ** (MSAlg a9) is Relation-like Function-like Function-yielding set
B ** A is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)
1. (UA) is Element of the carrier of (UA)
the OneF of (UA) is Element of the carrier of (UA)
M . (1. (UA)) is Element of the carrier of ((MSSign UA),(MSAlg UA))
MSAlg G is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of ((MSAlg UA) Over (MSSign UA))
(MSAlg UA) Over (MSSign UA) is strict non-empty MSAlgebra over MSSign UA
the Sorts of ((MSAlg UA) Over (MSSign UA)) is Relation-like non-empty non empty-yielding the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) set
1_ ((MSSign UA),(MSAlg UA)) is Element of the carrier of ((MSSign UA),(MSAlg UA))
1. ((MSSign UA),(MSAlg UA)) is Element of the carrier of ((MSSign UA),(MSAlg UA))
the OneF of ((MSSign UA),(MSAlg UA)) is Element of the carrier of ((MSSign UA),(MSAlg UA))
1_ (UA) is Element of the carrier of (UA)
M . (1_ (UA)) is Element of the carrier of ((MSSign UA),(MSAlg UA))
UA is non empty V157() quasi_total non-empty UAStr
(UA) is non empty strict unital associative right_unital well-unital left_unital multLoopStr
the carrier of (UA) is non empty set
MSSign UA is non empty trivial V53() non void 1 -element V59() strict segmental ManySortedSign
MSAlg UA is strict non-empty MSAlgebra over MSSign UA
((MSSign UA),(MSAlg UA)) is non empty strict unital associative right_unital well-unital left_unital multLoopStr
the carrier of ((MSSign UA),(MSAlg UA)) is non empty set
[: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):] is set
bool [: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):] is set
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
the carrier of UA is non empty set
the carrier of (MSSign UA) is non empty trivial V31() set
the Sorts of (MSAlg UA) is Relation-like non-empty non empty-yielding the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) set
((MSSign UA),(MSAlg UA)) is non empty Element of bool (MSFuncs ( the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)))
MSFuncs ( the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)) is non empty set
bool (MSFuncs ( the Sorts of (MSAlg UA), the Sorts of (MSAlg UA))) is set
id the Sorts of (MSAlg UA) is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding "1-1" "onto" ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)
((MSSign UA),(MSAlg UA)) is Relation-like [:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):] -defined ((MSSign UA),(MSAlg UA)) -valued Function-like V14([:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):]) quasi_total Element of bool [:[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):],((MSSign UA),(MSAlg UA)):]
[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):] is set
[:[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):],((MSSign UA),(MSAlg UA)):] is set
bool [:[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):],((MSSign UA),(MSAlg UA)):] is set
G is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding Element of ((MSSign UA),(MSAlg UA))
multLoopStr(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)),G #) is non empty strict multLoopStr
id the carrier of UA is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like one-to-one non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is set
bool [: the carrier of UA, the carrier of UA:] is set
h is Relation-like the carrier of (UA) -defined the carrier of ((MSSign UA),(MSAlg UA)) -valued Function-like non empty V14( the carrier of (UA)) quasi_total unity-preserving multiplicative Element of bool [: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):]
(UA) is Relation-like [:(UA),(UA):] -defined (UA) -valued Function-like V14([:(UA),(UA):]) quasi_total Element of bool [:[:(UA),(UA):],(UA):]
[:(UA),(UA):] is set
[:[:(UA),(UA):],(UA):] is set
bool [:[:(UA),(UA):],(UA):] is set
h is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
multLoopStr(# (UA),(UA),h #) is non empty strict multLoopStr
1. multLoopStr(# (UA),(UA),h #) is Element of the carrier of multLoopStr(# (UA),(UA),h #)
the carrier of multLoopStr(# (UA),(UA),h #) is non empty set
the OneF of multLoopStr(# (UA),(UA),h #) is Element of the carrier of multLoopStr(# (UA),(UA),h #)
a is Element of the carrier of (UA)
h . a is Element of the carrier of ((MSSign UA),(MSAlg UA))
b is Element of the carrier of (UA)
h . b is Element of the carrier of ((MSSign UA),(MSAlg UA))
0 .--> b is set
{0} --> b is Relation-like {0} -defined {b} -valued Function-like non empty V14({0}) quasi_total Element of bool [:{0},{b}:]
{b} is non empty set
[:{0},{b}:] is set
bool [:{0},{b}:] is set
0 .--> a is set
{0} --> a is Relation-like {0} -defined {a} -valued Function-like non empty V14({0}) quasi_total Element of bool [:{0},{a}:]
{a} is non empty set
[:{0},{a}:] is set
bool [:{0},{a}:] is set
1. multLoopStr(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)),G #) is Element of the carrier of multLoopStr(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)),G #)
the carrier of multLoopStr(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)),G #) is non empty set
the OneF of multLoopStr(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)),G #) is Element of the carrier of multLoopStr(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)),G #)
dom h is set
rng h is set
UA is non empty V157() quasi_total non-empty UAStr
(UA) is non empty strict unital associative right_unital well-unital left_unital multLoopStr
MSSign UA is non empty trivial V53() non void 1 -element V59() strict segmental ManySortedSign
MSAlg UA is strict non-empty MSAlgebra over MSSign UA
((MSSign UA),(MSAlg UA)) is non empty strict unital associative right_unital well-unital left_unital multLoopStr
the carrier of (UA) is non empty set
the carrier of ((MSSign UA),(MSAlg UA)) is non empty set
[: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):] is set
bool [: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):] is set
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
the carrier of UA is non empty set
h is Relation-like Function-like set
dom h is set
h is Relation-like the carrier of (UA) -defined the carrier of ((MSSign UA),(MSAlg UA)) -valued Function-like non empty V14( the carrier of (UA)) quasi_total unity-preserving multiplicative Element of bool [: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):]
h is Relation-like the carrier of (UA) -defined the carrier of ((MSSign UA),(MSAlg UA)) -valued Function-like non empty V14( the carrier of (UA)) quasi_total unity-preserving multiplicative Element of bool [: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):]