:: 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()
is non empty set
K268() is M12()

[:K119(),K268():] is set
bool [:K119(),K268():] 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
{ b1 where b1 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) : b1 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 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 #)

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

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

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

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

{H} is functional non empty set
is set
bool 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

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

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

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

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

{G} is functional non empty set
is set
bool 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

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
--> (h . 0) is Relation-like -defined {(h . 0)} -valued Function-like non empty V14() quasi_total Element of bool [:,{(h . 0)}:]
{(h . 0)} is non empty set
[:,{(h . 0)}:] is set
bool [:,{(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

{h} is non empty set
is set
bool 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

the Element of is Element of

the carrier of multLoopStr(# , the Relation-like -defined -valued Function-like V14() quasi_total Element of bool , the Element of #) is non empty set

H is Element of the carrier of multLoopStr(# , the Relation-like -defined -valued Function-like V14() quasi_total Element of bool , the Element of #)
() * H is Element of the carrier of multLoopStr(# , the Relation-like -defined -valued Function-like V14() quasi_total Element of bool , the Element of #)
the multF of multLoopStr(# , the Relation-like -defined -valued Function-like V14() quasi_total Element of bool , the Element of #) is Relation-like [::] -defined the carrier of multLoopStr(# , the Relation-like -defined -valued Function-like V14() quasi_total Element of bool , the Element of #) -valued Function-like V14([::]) quasi_total Element of bool [:[::], the carrier of multLoopStr(# , the Relation-like -defined -valued Function-like V14() quasi_total Element of bool , the Element of #):]
[::] is set
[:[::], the carrier of multLoopStr(# , the Relation-like -defined -valued Function-like V14() quasi_total Element of bool , the Element of #):] is set
bool [:[::], the carrier of multLoopStr(# , the Relation-like -defined -valued Function-like V14() quasi_total Element of bool , the Element of #):] is set
the multF of multLoopStr(# , the Relation-like -defined -valued Function-like V14() quasi_total Element of bool , the Element of #) . ((),H) is Element of the carrier of multLoopStr(# , the Relation-like -defined -valued Function-like V14() quasi_total Element of bool , the Element of #)

the carrier of UA is non empty set

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

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

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

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

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

{G} is functional non empty set
is set
bool 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