:: AUTALG_1 semantic presentation

K119() is non empty V24() V25() V26() Element of bool K115()
K115() is set
bool K115() is non empty set
K92() is non empty V24() V25() V26() set
bool K92() is non empty set
bool K119() is non empty set
K285() 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
K263() is M12()

[:K119(),K263():] is set
bool [:K119(),K263():] is non empty set
UA is non empty V144() 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 non empty set
bool [: the carrier of UA, the carrier of UA:] is non empty set
rng (id the carrier of UA) is set
UA is non empty V144() quasi_total non-empty UAStr
the carrier of UA is non empty set
[: the carrier of UA, the carrier of UA:] is non empty set
bool [: 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
{ 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_isomorphism 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
c4 is set
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)
c4 is functional non empty set

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 Funcs ( the carrier of UA, the carrier of UA)
b is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier 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 bool [: the carrier of UA, the carrier of UA:]
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)
h 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
c4 is set
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 bool [: the carrier of UA, the carrier of UA:]
c4 is set
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 bool [: the carrier of UA, the carrier of UA:]
UA is non empty V144() 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
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)
UA is non empty V144() 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 non empty set
bool [: the carrier of UA, the carrier of UA:] is non empty set
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
UA is non empty V144() quasi_total non-empty UAStr
the carrier of UA is non empty set
[: the carrier of UA, the carrier of UA:] is non empty set
bool [: the carrier of UA, 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 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:]
UA is non empty V144() quasi_total non-empty UAStr
the carrier of UA is non empty set
[: the carrier of UA, the carrier of UA:] is non empty set
bool [: the carrier of UA, the carrier of UA:] is 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 bool [: the carrier of UA, the carrier of UA:]

rng h is set
UA is non empty V144() 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)

[: the carrier of UA, the carrier of UA:] is non empty set
bool [: the carrier of UA, the carrier of UA:] is 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 bool [: the carrier of UA, the carrier of UA:]
UA is non empty V144() 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)
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 * 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 non empty set
bool [: the carrier of UA, the carrier of UA:] is non empty set
UA is non empty V144() 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 non empty set
[:[:(UA),(UA):],(UA):] is non empty set
bool [:[:(UA),(UA):],(UA):] is 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 (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 * 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 non empty set
bool [: the carrier of UA, the carrier of UA:] is non empty set
c4 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:]
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 bool [: the carrier of UA, the carrier of UA:]
b * c4 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 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 [:(UA),(UA):] -defined (UA) -valued Function-like non empty V14([:(UA),(UA):]) quasi_total Function-yielding V118() Element of bool [:[:(UA),(UA):],(UA):]
h is Relation-like [:(UA),(UA):] -defined (UA) -valued Function-like non empty V14([:(UA),(UA):]) quasi_total Function-yielding V118() Element of bool [:[:(UA),(UA):],(UA):]
c4 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)
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 (UA)
h . (c4,b) is Relation-like Function-like Element of (UA)
h . (c4,b) is Relation-like Function-like Element of (UA)
b * c4 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 non empty set
bool [: the carrier of UA, the carrier of UA:] is non empty set
UA is non empty V144() 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 non empty V14([:(UA),(UA):]) quasi_total Function-yielding V118() Element of bool [:[:(UA),(UA):],(UA):]
[:(UA),(UA):] is non empty set
[:[:(UA),(UA):],(UA):] is non empty set
bool [:[:(UA),(UA):],(UA):] is non empty set
multMagma(# (UA),(UA) #) is strict multMagma
the carrier of multMagma(# (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 non empty set
bool [: the carrier of UA, the carrier of UA:] is non empty set
h is Element of the carrier of multMagma(# (UA),(UA) #)
c4 is Element of the carrier of multMagma(# (UA),(UA) #)
c4 * h is Element of the carrier of multMagma(# (UA),(UA) #)
the multF of multMagma(# (UA),(UA) #) is Relation-like [: the carrier of multMagma(# (UA),(UA) #), the carrier of multMagma(# (UA),(UA) #):] -defined the carrier of multMagma(# (UA),(UA) #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# (UA),(UA) #), the carrier of multMagma(# (UA),(UA) #):], the carrier of multMagma(# (UA),(UA) #):]
[: the carrier of multMagma(# (UA),(UA) #), the carrier of multMagma(# (UA),(UA) #):] is set
[:[: the carrier of multMagma(# (UA),(UA) #), the carrier of multMagma(# (UA),(UA) #):], the carrier of multMagma(# (UA),(UA) #):] is set
bool [:[: the carrier of multMagma(# (UA),(UA) #), the carrier of multMagma(# (UA),(UA) #):], the carrier of multMagma(# (UA),(UA) #):] is non empty set
the multF of multMagma(# (UA),(UA) #) . (c4,h) is Element of the carrier of multMagma(# (UA),(UA) #)
h * c4 is Element of the carrier of multMagma(# (UA),(UA) #)
the multF of multMagma(# (UA),(UA) #) . (h,c4) is Element of the carrier of multMagma(# (UA),(UA) #)
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 (UA)
(id the carrier of UA) * 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 bool [: the carrier of UA, the carrier of UA:]
b * (id the carrier of UA) 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 is Element of the carrier of multMagma(# (UA),(UA) #)
c4 * a is Element of the carrier of multMagma(# (UA),(UA) #)
the multF of multMagma(# (UA),(UA) #) . (c4,a) is Element of the carrier of multMagma(# (UA),(UA) #)
a * c4 is Element of the carrier of multMagma(# (UA),(UA) #)
the multF of multMagma(# (UA),(UA) #) . (a,c4) is Element of the carrier of multMagma(# (UA),(UA) #)
rng b is set

h is Element of the carrier of multMagma(# (UA),(UA) #)
c4 is Element of the carrier of multMagma(# (UA),(UA) #)
h * c4 is Element of the carrier of multMagma(# (UA),(UA) #)
the multF of multMagma(# (UA),(UA) #) is Relation-like [: the carrier of multMagma(# (UA),(UA) #), the carrier of multMagma(# (UA),(UA) #):] -defined the carrier of multMagma(# (UA),(UA) #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# (UA),(UA) #), the carrier of multMagma(# (UA),(UA) #):], the carrier of multMagma(# (UA),(UA) #):]
[: the carrier of multMagma(# (UA),(UA) #), the carrier of multMagma(# (UA),(UA) #):] is set
[:[: the carrier of multMagma(# (UA),(UA) #), the carrier of multMagma(# (UA),(UA) #):], the carrier of multMagma(# (UA),(UA) #):] is set
bool [:[: the carrier of multMagma(# (UA),(UA) #), the carrier of multMagma(# (UA),(UA) #):], the carrier of multMagma(# (UA),(UA) #):] is non empty set
the multF of multMagma(# (UA),(UA) #) . (h,c4) is Element of the carrier of multMagma(# (UA),(UA) #)
b is Element of the carrier of multMagma(# (UA),(UA) #)
(h * c4) * b is Element of the carrier of multMagma(# (UA),(UA) #)
the multF of multMagma(# (UA),(UA) #) . ((h * c4),b) is Element of the carrier of multMagma(# (UA),(UA) #)
c4 * b is Element of the carrier of multMagma(# (UA),(UA) #)
the multF of multMagma(# (UA),(UA) #) . (c4,b) is Element of the carrier of multMagma(# (UA),(UA) #)
h * (c4 * b) is Element of the carrier of multMagma(# (UA),(UA) #)
the multF of multMagma(# (UA),(UA) #) . (h,(c4 * b)) is Element of the carrier of multMagma(# (UA),(UA) #)
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 (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)
a9 * 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 bool [: the carrier of UA, the carrier of UA:]
[: the carrier of UA, the carrier of UA:] is non empty set
bool [: the carrier of UA, the carrier of UA:] is non empty set
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)
b * 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 bool [: the carrier of UA, the carrier of UA:]
a9 * (b * 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 bool [: the carrier of UA, the carrier of UA:]
(a9 * b) * 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 bool [: the carrier of UA, the carrier of UA:]
h is Element of the carrier of multMagma(# (UA),(UA) #)
UA is non empty V144() quasi_total non-empty UAStr
(UA) is non empty Group-like associative multMagma
(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 non empty V14([:(UA),(UA):]) quasi_total Function-yielding V118() Element of bool [:[:(UA),(UA):],(UA):]
[:(UA),(UA):] is non empty set
[:[:(UA),(UA):],(UA):] is non empty set
bool [:[:(UA),(UA):],(UA):] is non empty set
multMagma(# (UA),(UA) #) is strict multMagma
UA is non empty V144() 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)
dom h is set
rng h is set
UA is non empty V144() quasi_total non-empty UAStr
(UA) is non empty strict Group-like associative multMagma
(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 non empty V14([:(UA),(UA):]) quasi_total Function-yielding V118() Element of bool [:[:(UA),(UA):],(UA):]
[:(UA),(UA):] is non empty set
[:[:(UA),(UA):],(UA):] is non empty set
bool [:[:(UA),(UA):],(UA):] is non empty set
multMagma(# (UA),(UA) #) is strict multMagma
the carrier of (UA) is non empty set
h is Element of the carrier of (UA)
c4 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 Element of the carrier of (UA)
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 (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 non empty 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 non empty set
[:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is non empty set
bool [:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is non empty set
the multF of (UA) . (h,h) is Element of the carrier of (UA)
b * c4 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 non empty set
bool [: the carrier of UA, the carrier of UA:] is non empty set
UA is non empty V144() 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 non empty set
bool [: the carrier of UA, the carrier of UA:] is non empty set
(UA) is non empty strict Group-like associative multMagma
(UA) is functional non empty FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
(UA) is Relation-like [:(UA),(UA):] -defined (UA) -valued Function-like non empty V14([:(UA),(UA):]) quasi_total Function-yielding V118() Element of bool [:[:(UA),(UA):],(UA):]
[:(UA),(UA):] is non empty set
[:[:(UA),(UA):],(UA):] is non empty set
bool [:[:(UA),(UA):],(UA):] is non empty set
multMagma(# (UA),(UA) #) is strict multMagma
1_ (UA) is Element of the carrier of (UA)
the carrier of (UA) is non empty set
the Element of the carrier of (UA) is Element of the carrier of (UA)
h is Element of the carrier of (UA)
c4 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:]
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 bool [: the carrier of UA, the carrier of UA:]
h * the Element of the carrier of (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 non empty 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 non empty set
[:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is non empty set
bool [:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is non empty set
the multF of (UA) . (h, the Element of the carrier of (UA)) is Element of the carrier of (UA)
b * c4 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 V144() 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
(UA) is non empty strict Group-like associative multMagma
(UA) is Relation-like [:(UA),(UA):] -defined (UA) -valued Function-like non empty V14([:(UA),(UA):]) quasi_total Function-yielding V118() Element of bool [:[:(UA),(UA):],(UA):]
[:(UA),(UA):] is non empty set
[:[:(UA),(UA):],(UA):] is non empty set
bool [:[:(UA),(UA):],(UA):] is non empty set
multMagma(# (UA),(UA) #) is strict multMagma
the carrier of (UA) is 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 (UA)

h is Element of the carrier of (UA)
h " is Element of the carrier of (UA)
c4 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)
c4 * 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 non empty set
bool [: the carrier of UA, the carrier of UA:] is non empty set
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 non empty 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 non empty set
[:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is non empty set
bool [:[: the carrier of (UA), the carrier of (UA):], the carrier of (UA):] is non empty set
the multF of (UA) . (h,(h ")) is Element of the carrier of (UA)
1_ (UA) 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:]
rng h is set
dom h is set
UA is set

c4 is Relation-like UA -defined Function-like V14(UA) set
b is set
c4 . b is set
h . b is set
h . b is set
UA is set
{UA} is non empty set

h . UA is set

{UA} --> (h . UA) is Relation-like {UA} -defined {(h . UA)} -valued Function-like constant non empty V14({UA}) quasi_total Element of bool [:{UA},{(h . UA)}:]
{(h . UA)} is non empty set
[:{UA},{(h . UA)}:] is non empty set
bool [:{UA},{(h . UA)}:] is non empty set
dom h is set
rng h is set
UA is set

b is set
h . b is set
h . b is set
[:(h . b),(h . b):] is set
bool [:(h . b),(h . b):] is non empty set

a is Relation-like h . b -defined h . b -valued Function-like quasi_total Element of bool [:(h . b),(h . b):]

(c4 "") . b is Relation-like Function-like set
b is set
(c4 "") . b is Relation-like Function-like set
rng ((c4 "") . b) is set
h . b is set
h . b is set
[:(h . b),(h . b):] is set
bool [:(h . b),(h . b):] is non empty set

a is Relation-like h . b -defined h . b -valued Function-like quasi_total Element of bool [:(h . b),(h . b):]
dom a is set

rng (a ") is set
UA is set

(c4 "") "" is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
b is set
h . b is set
h . b is set
[:(h . b),(h . b):] is set
bool [:(h . b),(h . b):] is non empty set

[:(h . b),(h . b):] is set
bool [:(h . b),(h . b):] is non empty set
(c4 "") . b is Relation-like Function-like set
a is Relation-like h . b -defined h . b -valued Function-like quasi_total Element of bool [:(h . b),(h . b):]

((c4 "") "") . b is Relation-like Function-like set
b is Relation-like h . b -defined h . b -valued Function-like quasi_total Element of bool [:(h . b),(h . b):]

h is set
dom (h ** UA) is set
(h ** UA) . h is Relation-like Function-like set

dom h is set
dom UA is set
(dom h) /\ (dom UA) is set

(UA . h) * (h . h) is Relation-like Function-like set
UA is set

b is set
h . b is set
h . b is set
[:(h . b),(h . b):] is set
bool [:(h . b),(h . b):] is non empty set

c4 . b is set
[:(h . b),(c4 . b):] is set
bool [:(h . b),(c4 . b):] is non empty set

a9 is Relation-like h . b -defined h . b -valued Function-like quasi_total Element of bool [:(h . b),(h . b):]
rng a9 is set
b9 is Relation-like h . b -defined c4 . b -valued Function-like quasi_total Element of bool [:(h . b),(c4 . b):]
rng b9 is set
b9 * a9 is Relation-like h . b -defined c4 . b -valued Function-like Element of bool [:(h . b),(c4 . b):]
[:(h . b),(c4 . b):] is set
bool [:(h . b),(c4 . b):] is non empty set
rng (b9 * a9) is set
(a ** b) . b is Relation-like Function-like set
rng ((a ** b) . b) is set
UA is set

(a ** b) "" is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of c4,h

(b "") ** (a "") is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of c4,h
b is set
h . b is set
h . b is set
[:(h . b),(h . b):] is set
bool [:(h . b),(h . b):] is non empty set

a9 is Relation-like h . b -defined h . b -valued Function-like quasi_total Element of bool [:(h . b),(h . b):]
c4 . b is set
[:(h . b),(c4 . b):] is set
bool [:(h . b),(c4 . b):] is non empty set

b9 is Relation-like h . b -defined c4 . b -valued Function-like quasi_total Element of bool [:(h . b),(c4 . b):]

rng a9 is set
[:(h . b),(h . b):] is set
bool [:(h . b),(h . b):] is non empty set
(a ** b) . b is Relation-like Function-like set
b9 * a9 is Relation-like h . b -defined c4 . b -valued Function-like Element of bool [:(h . b),(c4 . b):]
[:(h . b),(c4 . b):] is set
bool [:(h . b),(c4 . b):] is non empty set
((a ** b) "") . b is Relation-like Function-like set
(b9 * a9) " is Relation-like Function-like set

rng b9 is set
[:(c4 . b),(h . b):] is set
bool [:(c4 . b),(h . b):] is non empty set
((b "") ** (a "")) . b is Relation-like Function-like set
B is Relation-like c4 . b -defined h . b -valued Function-like quasi_total Element of bool [:(c4 . b),(h . b):]
A is Relation-like h . b -defined h . b -valued Function-like quasi_total Element of bool [:(h . b),(h . b):]
A * B is Relation-like c4 . b -defined h . b -valued Function-like Element of bool [:(c4 . b),(h . b):]
[:(c4 . b),(h . b):] is set
bool [:(c4 . b),(h . b):] is non empty set
(b9 ") * A is Relation-like Function-like set
(b9 ") * (a9 ") is Relation-like Function-like set
UA is set

a is set
h . a is set
h . a is set
[:(h . a),(h . a):] is set
bool [:(h . a),(h . a):] is non empty set

b is Relation-like h . a -defined h . a -valued Function-like quasi_total Element of bool [:(h . a),(h . a):]
[:(h . a),(h . a):] is set
bool [:(h . a),(h . a):] is non empty set

(b ** c4) . a is Relation-like Function-like set
id (h . a) is Relation-like h . a -defined h . a -valued Function-like one-to-one V14(h . a) quasi_total Element of bool [:(h . a),(h . a):]
[:(h . a),(h . a):] is set
bool [:(h . a),(h . a):] is non empty set
a9 is Relation-like h . a -defined h . a -valued Function-like quasi_total Element of bool [:(h . a),(h . a):]
a9 * b is Relation-like h . a -defined h . a -valued Function-like Element of bool [:(h . a),(h . a):]
(c4 "") . a is Relation-like Function-like set

rng b is set
UA is set

(Funcs) (h,h) is Relation-like UA -defined Function-like V14(UA) set
c4 is set
h . c4 is set
h . c4 is set
Funcs ((h . c4),(h . c4)) is functional set
c4 is set
((Funcs) (h,h)) . c4 is set
h . c4 is set
h . c4 is set
Funcs ((h . c4),(h . c4)) is functional set
c4 is set
((Funcs) (h,h)) . c4 is set
UA is set

(Funcs) (h,h) is Relation-like UA -defined Function-like V14(UA) set
product ((Funcs) (h,h)) is set
rng ((Funcs) (h,h)) is set
UA is set

(UA,h,h) is non empty set
(Funcs) (h,h) is Relation-like UA -defined Function-like V14(UA) set
b is set
product ((Funcs) (h,h)) is set
dom ((Funcs) (h,h)) is set

dom a is set
b is set
a . b is set
h . b is set
h . b is set
Funcs ((h . b),(h . b)) is functional set
((Funcs) (h,h)) . b is set
b is set
a . b is set
h . b is set
h . b is set
Funcs ((h . b),(h . b)) is functional set
b is set
a . b is set
h . b is set
h . b is set
[:(h . b),(h . b):] is set
bool [:(h . b),(h . b):] is non empty set

dom a9 is set
rng a9 is set
UA is set

(UA,h,h) is non empty set
(Funcs) (h,h) is Relation-like UA -defined Function-like V14(UA) set

dom ((Funcs) (h,h)) is set
a is set
b is Element of UA

h . b is set
h . b is set
[:(h . b),(h . b):] is set
bool [:(h . b),(h . b):] is non empty set
Funcs ((h . b),(h . b)) is functional set

((Funcs) (h,h)) . a is set
dom b is set
product ((Funcs) (h,h)) is set
UA is set

(Funcs) (h,h) is Relation-like UA -defined Function-like V14(UA) set
h is set
((Funcs) (h,h)) . h is set

h . h is set
[:(h . h),(h . h):] is set
bool [:(h . h),(h . h):] is non empty set
Funcs ((h . h),(h . h)) is functional non empty set
UA is set

(UA,h,h) is non empty set
bool (UA,h,h) is non empty set
h is non empty Element of bool (UA,h,h)
c4 is Element of h
UA is set

h is set

rng ((id h) . h) is set
h . h is set
id (h . h) is Relation-like h . h -defined h . h -valued Function-like one-to-one V14(h . h) quasi_total Element of bool [:(h . h),(h . h):]
[:(h . h),(h . h):] is set
bool [:(h . h),(h . h):] is non empty set
h is set

h . h is set
id (h . h) is Relation-like h . h -defined h . h -valued Function-like one-to-one V14(h . h) quasi_total Element of bool [:(h . h),(h . h):]
[:(h . h),(h . h):] is set
bool [:(h . h),(h . h):] is non empty set
UA is non empty non void V59() ManySortedSign
UA is non empty non void V59() ManySortedSign
the carrier of UA is non empty set
h is non-empty MSAlgebra over UA
the Sorts of h 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 h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() "1-1" "onto" ManySortedFunction of the Sorts of h, the Sorts of h
( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
UA is non empty non void V59() ManySortedSign
h is non-empty MSAlgebra over UA
the Sorts of h 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
( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
bool ( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
c4 is set
b is set
id the Sorts of h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() "1-1" "onto" ManySortedFunction of the Sorts of h, the Sorts of h
a is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
b is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
a is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
c4 is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
b is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
a is set
b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
a is set
b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
UA is non empty non void V59() ManySortedSign
the carrier of UA is non empty set
h is non-empty MSAlgebra over UA
the Sorts of h is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
(UA,h) is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
bool ( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
UA is non empty non void V59() ManySortedSign
h is non-empty MSAlgebra over UA
(UA,h) is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
the carrier of UA is non empty set
the Sorts of h 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, the Sorts of h, the Sorts of h) is non empty set
bool ( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
UA is non empty non void V59() ManySortedSign
the carrier of UA is non empty set
h is non-empty MSAlgebra over UA
the Sorts of h is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
(UA,h) is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
bool ( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
UA is non empty non void V59() ManySortedSign
the carrier of UA is non empty set
h is non-empty MSAlgebra over UA
the Sorts of h 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 h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() "1-1" "onto" ManySortedFunction of the Sorts of h, the Sorts of h
(UA,h) is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
bool ( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
UA is non empty non void V59() ManySortedSign
the carrier of UA is non empty set
h is non-empty MSAlgebra over UA
the Sorts of h is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
(UA,h) is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
bool ( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
h "" is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
UA is non empty non void V59() ManySortedSign
the carrier of UA is non empty set
h is non-empty MSAlgebra over UA
the Sorts of h is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
(UA,h) is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
bool ( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
c4 is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
h ** c4 is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
UA is non empty V144() 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 ( the carrier of (MSSign UA), the Sorts of (MSAlg UA), the Sorts of (MSAlg UA))
( the carrier of (MSSign UA), the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)) is non empty set
bool ( the carrier of (MSSign UA), the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)) is non empty set
h is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding V118() 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)

{h} is functional non empty set
is non empty set
bool is non empty set
MSAlg h is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding V118() 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
h is non-empty MSAlgebra over UA
(UA,h) is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
the carrier of UA is non empty set
the Sorts of h 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, the Sorts of h, the Sorts of h) is non empty set
bool ( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
[:(UA,h),(UA,h):] is non empty set
[:[:(UA,h),(UA,h):],(UA,h):] is non empty set
bool [:[:(UA,h),(UA,h):],(UA,h):] is non empty set
h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
c4 is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
c4 ** h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
a is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
a ** b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
h is Relation-like [:(UA,h),(UA,h):] -defined (UA,h) -valued Function-like non empty V14([:(UA,h),(UA,h):]) quasi_total Element of bool [:[:(UA,h),(UA,h):],(UA,h):]
c4 is Relation-like [:(UA,h),(UA,h):] -defined (UA,h) -valued Function-like non empty V14([:(UA,h),(UA,h):]) quasi_total Element of bool [:[:(UA,h),(UA,h):],(UA,h):]
b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
a is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
h . (b,a) is Element of (UA,h)
c4 . (b,a) is Element of (UA,h)
a ** b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
UA is non empty non void V59() ManySortedSign
h is non-empty MSAlgebra over UA
(UA,h) is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
the carrier of UA is non empty set
the Sorts of h 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, the Sorts of h, the Sorts of h) is non empty set
bool ( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
(UA,h) is Relation-like [:(UA,h),(UA,h):] -defined (UA,h) -valued Function-like non empty V14([:(UA,h),(UA,h):]) quasi_total Element of bool [:[:(UA,h),(UA,h):],(UA,h):]
[:(UA,h),(UA,h):] is non empty set
[:[:(UA,h),(UA,h):],(UA,h):] is non empty set
bool [:[:(UA,h),(UA,h):],(UA,h):] is non empty set
multMagma(# (UA,h),(UA,h) #) is strict multMagma
the carrier of multMagma(# (UA,h),(UA,h) #) is set
id the Sorts of h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() "1-1" "onto" ManySortedFunction of the Sorts of h, the Sorts of h
b is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
a is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
a * b is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
the multF of multMagma(# (UA,h),(UA,h) #) is Relation-like [: the carrier of multMagma(# (UA,h),(UA,h) #), the carrier of multMagma(# (UA,h),(UA,h) #):] -defined the carrier of multMagma(# (UA,h),(UA,h) #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# (UA,h),(UA,h) #), the carrier of multMagma(# (UA,h),(UA,h) #):], the carrier of multMagma(# (UA,h),(UA,h) #):]
[: the carrier of multMagma(# (UA,h),(UA,h) #), the carrier of multMagma(# (UA,h),(UA,h) #):] is set
[:[: the carrier of multMagma(# (UA,h),(UA,h) #), the carrier of multMagma(# (UA,h),(UA,h) #):], the carrier of multMagma(# (UA,h),(UA,h) #):] is set
bool [:[: the carrier of multMagma(# (UA,h),(UA,h) #), the carrier of multMagma(# (UA,h),(UA,h) #):], the carrier of multMagma(# (UA,h),(UA,h) #):] is non empty set
the multF of multMagma(# (UA,h),(UA,h) #) . (a,b) is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
b * a is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
the multF of multMagma(# (UA,h),(UA,h) #) . (b,a) is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
(id the Sorts of h) ** b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
b ** (id the Sorts of h) is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
b "" is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
a9 is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
a * a9 is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
the multF of multMagma(# (UA,h),(UA,h) #) . (a,a9) is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
a9 * a is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
the multF of multMagma(# (UA,h),(UA,h) #) . (a9,a) is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
(b "") ** b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
b ** (b "") is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
b is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
a is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
b * a is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
the multF of multMagma(# (UA,h),(UA,h) #) is Relation-like [: the carrier of multMagma(# (UA,h),(UA,h) #), the carrier of multMagma(# (UA,h),(UA,h) #):] -defined the carrier of multMagma(# (UA,h),(UA,h) #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# (UA,h),(UA,h) #), the carrier of multMagma(# (UA,h),(UA,h) #):], the carrier of multMagma(# (UA,h),(UA,h) #):]
[: the carrier of multMagma(# (UA,h),(UA,h) #), the carrier of multMagma(# (UA,h),(UA,h) #):] is set
[:[: the carrier of multMagma(# (UA,h),(UA,h) #), the carrier of multMagma(# (UA,h),(UA,h) #):], the carrier of multMagma(# (UA,h),(UA,h) #):] is set
bool [:[: the carrier of multMagma(# (UA,h),(UA,h) #), the carrier of multMagma(# (UA,h),(UA,h) #):], the carrier of multMagma(# (UA,h),(UA,h) #):] is non empty set
the multF of multMagma(# (UA,h),(UA,h) #) . (b,a) is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
b is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
(b * a) * b is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
the multF of multMagma(# (UA,h),(UA,h) #) . ((b * a),b) is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
a * b is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
the multF of multMagma(# (UA,h),(UA,h) #) . (a,b) is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
b * (a * b) is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
the multF of multMagma(# (UA,h),(UA,h) #) . (b,(a * b)) is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
b9 is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
A is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
A ** b9 is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
a9 is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
b9 ** a9 is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
A ** (b9 ** a9) is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
(A ** b9) ** a9 is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
b is Element of the carrier of multMagma(# (UA,h),(UA,h) #)
UA is non empty non void V59() ManySortedSign
h is non-empty MSAlgebra over UA
(UA,h) is non empty Group-like associative multMagma
(UA,h) is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
the carrier of UA is non empty set
the Sorts of h 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, the Sorts of h, the Sorts of h) is non empty set
bool ( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
(UA,h) is Relation-like [:(UA,h),(UA,h):] -defined (UA,h) -valued Function-like non empty V14([:(UA,h),(UA,h):]) quasi_total Element of bool [:[:(UA,h),(UA,h):],(UA,h):]
[:(UA,h),(UA,h):] is non empty set
[:[:(UA,h),(UA,h):],(UA,h):] is non empty set
bool [:[:(UA,h),(UA,h):],(UA,h):] is non empty set
multMagma(# (UA,h),(UA,h) #) is strict multMagma
UA is non empty non void V59() ManySortedSign
h is non-empty MSAlgebra over UA
(UA,h) is non empty strict Group-like associative multMagma
(UA,h) is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
the carrier of UA is non empty set
the Sorts of h 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, the Sorts of h, the Sorts of h) is non empty set
bool ( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
(UA,h) is Relation-like [:(UA,h),(UA,h):] -defined (UA,h) -valued Function-like non empty V14([:(UA,h),(UA,h):]) quasi_total Element of bool [:[:(UA,h),(UA,h):],(UA,h):]
[:(UA,h),(UA,h):] is non empty set
[:[:(UA,h),(UA,h):],(UA,h):] is non empty set
bool [:[:(UA,h),(UA,h):],(UA,h):] is non empty set
multMagma(# (UA,h),(UA,h) #) is strict multMagma
the carrier of (UA,h) is non empty set
h is Element of the carrier of (UA,h)
b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
c4 is Element of the carrier of (UA,h)
a is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
h * c4 is Element of the carrier of (UA,h)
the multF of (UA,h) is Relation-like [: the carrier of (UA,h), the carrier of (UA,h):] -defined the carrier of (UA,h) -valued Function-like non empty V14([: the carrier of (UA,h), the carrier of (UA,h):]) quasi_total Element of bool [:[: the carrier of (UA,h), the carrier of (UA,h):], the carrier of (UA,h):]
[: the carrier of (UA,h), the carrier of (UA,h):] is non empty set
[:[: the carrier of (UA,h), the carrier of (UA,h):], the carrier of (UA,h):] is non empty set
bool [:[: the carrier of (UA,h), the carrier of (UA,h):], the carrier of (UA,h):] is non empty set
the multF of (UA,h) . (h,c4) is Element of the carrier of (UA,h)
a ** b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
UA is non empty non void V59() ManySortedSign
the carrier of UA is non empty set
h is non-empty MSAlgebra over UA
the Sorts of h 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 h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() "1-1" "onto" ManySortedFunction of the Sorts of h, the Sorts of h
(UA,h) is non empty strict Group-like associative multMagma
(UA,h) is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
bool ( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
(UA,h) is Relation-like [:(UA,h),(UA,h):] -defined (UA,h) -valued Function-like non empty V14([:(UA,h),(UA,h):]) quasi_total Element of bool [:[:(UA,h),(UA,h):],(UA,h):]
[:(UA,h),(UA,h):] is non empty set
[:[:(UA,h),(UA,h):],(UA,h):] is non empty set
bool [:[:(UA,h),(UA,h):],(UA,h):] is non empty set
multMagma(# (UA,h),(UA,h) #) is strict multMagma
1_ (UA,h) is Element of the carrier of (UA,h)
the carrier of (UA,h) is non empty set
the Element of the carrier of (UA,h) is Element of the carrier of (UA,h)
b is Element of the carrier of (UA,h)
a is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
b * the Element of the carrier of (UA,h) is Element of the carrier of (UA,h)
the multF of (UA,h) is Relation-like [: the carrier of (UA,h), the carrier of (UA,h):] -defined the carrier of (UA,h) -valued Function-like non empty V14([: the carrier of (UA,h), the carrier of (UA,h):]) quasi_total Element of bool [:[: the carrier of (UA,h), the carrier of (UA,h):], the carrier of (UA,h):]
[: the carrier of (UA,h), the carrier of (UA,h):] is non empty set
[:[: the carrier of (UA,h), the carrier of (UA,h):], the carrier of (UA,h):] is non empty set
bool [:[: the carrier of (UA,h), the carrier of (UA,h):], the carrier of (UA,h):] is non empty set
the multF of (UA,h) . (b, the Element of the carrier of (UA,h)) is Element of the carrier of (UA,h)
b ** a is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
UA is non empty non void V59() ManySortedSign
the carrier of UA is non empty set
h is non-empty MSAlgebra over UA
the Sorts of h is Relation-like non-empty non empty-yielding the carrier of UA -defined Function-like non empty V14( the carrier of UA) set
(UA,h) is non empty Element of bool ( the carrier of UA, the Sorts of h, the Sorts of h)
( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
bool ( the carrier of UA, the Sorts of h, the Sorts of h) is non empty set
(UA,h) is non empty strict Group-like associative multMagma
(UA,h) is Relation-like [:(UA,h),(UA,h):] -defined (UA,h) -valued Function-like non empty V14([:(UA,h),(UA,h):]) quasi_total Element of bool [:[:(UA,h),(UA,h):],(UA,h):]
[:(UA,h),(UA,h):] is non empty set
[:[:(UA,h),(UA,h):],(UA,h):] is non empty set
bool [:[:(UA,h),(UA,h):],(UA,h):] is non empty set
multMagma(# (UA,h),(UA,h) #) is strict multMagma
the carrier of (UA,h) is non empty set
h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
h "" is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
c4 is Element of the carrier of (UA,h)
c4 " is Element of the carrier of (UA,h)
b is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ( the carrier of UA, the Sorts of h,(UA,h))
b ** h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() ManySortedFunction of the Sorts of h, the Sorts of h
c4 * (c4 ") is Element of the carrier of (UA,h)
the multF of (UA,h) is Relation-like [: the carrier of (UA,h), the carrier of (UA,h):] -defined the carrier of (UA,h) -valued Function-like non empty V14([: the carrier of (UA,h), the carrier of (UA,h):]) quasi_total Element of bool [:[: the carrier of (UA,h), the carrier of (UA,h):], the carrier of (UA,h):]
[: the carrier of (UA,h), the carrier of (UA,h):] is non empty set
[:[: the carrier of (UA,h), the carrier of (UA,h):], the carrier of (UA,h):] is non empty set
bool [:[: the carrier of (UA,h), the carrier of (UA,h):], the carrier of (UA,h):] is non empty set
the multF of (UA,h) . (c4,(c4 ")) is Element of the carrier of (UA,h)
1_ (UA,h) is Element of the carrier of (UA,h)
id the Sorts of h is Relation-like the carrier of UA -defined Function-like non empty V14( the carrier of UA) Function-yielding V118() "1-1" "onto" ManySortedFunction of the Sorts of h, the Sorts of h
UA is non empty V144() quasi_total non-empty UAStr
h is non empty V144() 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
MSSign h is non empty trivial V53() non void 1 -element V59() strict segmental ManySortedSign

() Over (MSSign UA) is strict non-empty MSAlgebra over MSSign UA
the Sorts of (() 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 is non empty set
the carrier of h is non empty set
[: the carrier of UA, the carrier of h:] is non empty set
bool [: the carrier of UA, the carrier of h:] is non empty set
MSSorts h is Relation-like non-empty non empty-yielding the carrier of () -defined Function-like non empty V14( the carrier of ()) set
the carrier of () is non empty trivial V31() set
MSCharact h is Relation-like the carrier' of () -defined Function-like non empty V14( the carrier' of ()) ManySortedFunction of the Arity of () * K266( the carrier of (),()), the ResultSort of () * ()
the carrier' of () is non empty set
the Arity of () is Relation-like the carrier' of () -defined K263( the carrier of ()) -valued Function-like quasi_total Element of bool [: the carrier' of (),K263( the carrier of ()):]
K263( the carrier of ()) is M12( the carrier of ())
[: the carrier' of (),K263( the carrier of ()):] is set
bool [: the carrier' of (),K263( the carrier of ()):] is non empty set
K266( the carrier of (),()) is Relation-like K263( the carrier of ()) -defined Function-like V14(K263( the carrier of ())) set
the Arity of () * K266( the carrier of (),()) is Relation-like Function-like set
the ResultSort of () is Relation-like the carrier' of () -defined the carrier of () -valued Function-like non empty V14( the carrier' of ()) quasi_total Element of bool [: the carrier' of (), the carrier of ():]
[: the carrier' of (), the carrier of ():] is non empty set
bool [: the carrier' of (), the carrier of ():] is non empty set
the ResultSort of () * () is Relation-like Function-like set
MSAlgebra(# (),() #) is strict MSAlgebra over MSSign h
h is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding V118() ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of (() Over (MSSign UA))

MSSorts 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
MSCharact UA is Relation-like the carrier' of (MSSign UA) -defined Function-like non empty V14( the carrier' of (MSSign UA)) ManySortedFunction of the Arity of (MSSign UA) * K266( the carrier of (MSSign UA),(MSSorts UA)), the ResultSort of (MSSign UA) * (MSSorts UA)
the carrier' of (MSSign UA) is non empty set
the Arity of (MSSign UA) is Relation-like the carrier' of (MSSign UA) -defined K263( the carrier of (MSSign UA)) -valued Function-like quasi_total Element of bool [: the carrier' of (MSSign UA),K263( the carrier of (MSSign UA)):]
K263( the carrier of (MSSign UA)) is M12( the carrier of (MSSign UA))
[: the carrier' of (MSSign UA),K263( the carrier of (MSSign UA)):] is set
bool [: the carrier' of (MSSign UA),K263( the carrier of (MSSign UA)):] is non empty set
K266( the carrier of (MSSign UA),(MSSorts UA)) is Relation-like K263( the carrier of (MSSign UA)) -defined Function-like V14(K263( the carrier of (MSSign UA))) set
the Arity of (MSSign UA) * K266( the carrier of (MSSign UA),(MSSorts UA)) is Relation-like Function-like set
the ResultSort of (MSSign UA) is Relation-like the carrier' of (MSSign UA) -defined the carrier of (MSSign UA) -valued Function-like non empty V14( the carrier' of (MSSign UA)) quasi_total Element of bool [: the carrier' of (MSSign UA), the carrier of (MSSign UA):]
[: the carrier' of (MSSign UA), the carrier of (MSSign UA):] is non empty set
bool [: the carrier' of (MSSign UA), the carrier of (MSSign UA):] is non empty set
the ResultSort of (MSSign UA) * (MSSorts UA) is Relation-like Function-like set
MSAlgebra(# (MSSorts UA),() #) is strict MSAlgebra over MSSign UA
() . 0 is set

--> the carrier of h is Relation-like non-empty non empty-yielding -defined { the carrier of h} -valued Function-like constant non empty V14() quasi_total Element of bool [:,{ the carrier of h}:]
{ the carrier of h} is non empty set
[:,{ the carrier of h}:] is non empty set
bool [:,{ the carrier of h}:] is non empty set
(0 .--> the carrier of h) . 0 is set
(MSSorts UA) . 0 is set

--> the carrier of UA is Relation-like non-empty non empty-yielding -defined { the carrier of UA} -valued Function-like constant non empty V14() quasi_total Element of bool [:,{ the carrier of UA}:]
{ the carrier of UA} is non empty set
[:,{ the carrier of UA}:] is non empty set
bool [:,{ the carrier of UA}:] is non empty set
(0 .--> the carrier of UA) . 0 is set
UA is non empty V144() 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
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 functional non empty set
is non empty set
bool is non empty set
MSAlg h is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding V118() 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 V144() 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 ( the carrier of (MSSign UA), 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
( the carrier of (MSSign UA), the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)) is non empty set
bool ( the carrier of (MSSign UA), the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)) is non empty set

dom h is set
rng h is set
h is set
c4 is set
h . c4 is set
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 (UA)

{c4} is non empty set
[:,{c4}:] is non empty set
bool [:,{c4}:] is non empty set
a is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding V118() 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 b is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding V118() 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
h is set
c4 is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding V118() ManySortedFunction of the Sorts of (MSAlg UA), the Sorts of (MSAlg UA)

--> (c4 . 0) is Relation-like -defined {(c4 . 0)} -valued