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()
{0} is non empty set
K263({0}) is M12({0})
K267(0) is Relation-like K119() -defined K263({0}) -valued Function-like quasi_total Element of bool [:K119(),K263({0}):]
[:K119(),K263({0}):] is set
bool [:K119(),K263({0}):] 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
b is Relation-like Function-like Element of c4
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 Function-like 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
[: 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:]
h " is Relation-like Function-like set
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)
h " is Relation-like Function-like 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:]
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:]
b " is Relation-like Function-like set
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
b * (b ") is Relation-like Function-like set
(b ") * b is Relation-like Function-like 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 Relation-like Function-like set
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
h is Relation-like UA -defined Function-like V14(UA) set
h is Relation-like UA -defined Function-like V14(UA) 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 is Relation-like {UA} -defined Function-like non empty V14({UA}) set
h . UA is set
UA .--> (h . UA) is Relation-like {UA} -defined Function-like one-to-one 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
h is Relation-like non-empty UA -defined Function-like V14(UA) set
h is Relation-like non-empty UA -defined Function-like V14(UA) set
c4 is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
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
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):]
a " is Relation-like Function-like set
(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
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):]
dom a is set
a " is Relation-like Function-like set
rng (a ") is set
UA is set
h is Relation-like non-empty UA -defined Function-like V14(UA) set
h is Relation-like non-empty UA -defined Function-like V14(UA) set
c4 is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
c4 "" is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
(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
c4 . b is Relation-like Function-like 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):]
a " is Relation-like Function-like set
(a ") " is Relation-like Function-like set
((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):]
b " is Relation-like Function-like set
UA is Relation-like Function-like Function-yielding V118() set
h is Relation-like Function-like Function-yielding V118() set
h ** UA is Relation-like Function-like Function-yielding V118() set
h is set
dom (h ** UA) is set
(h ** UA) . h is Relation-like Function-like set
c4 is Relation-like Function-like set
dom h is set
dom UA is set
(dom h) /\ (dom UA) is set
UA . h is Relation-like Function-like set
h . h is Relation-like Function-like set
(UA . h) * (h . h) is Relation-like Function-like set
UA is set
h is Relation-like UA -defined Function-like V14(UA) set
h is Relation-like non-empty UA -defined Function-like V14(UA) set
c4 is Relation-like non-empty UA -defined Function-like V14(UA) set
b is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
a is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,c4
a ** b is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,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
b . b is Relation-like Function-like set
c4 . b is set
[:(h . b),(c4 . b):] is set
bool [:(h . b),(c4 . b):] is non empty set
a . b is Relation-like Function-like 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
h is Relation-like non-empty UA -defined Function-like V14(UA) set
h is Relation-like non-empty UA -defined Function-like V14(UA) set
c4 is Relation-like non-empty UA -defined Function-like V14(UA) set
b is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
b "" is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
a is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,c4
a ** b is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,c4
(a ** b) "" is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of c4,h
a "" 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
b . b is Relation-like Function-like 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
a . b is Relation-like Function-like set
b9 is Relation-like h . b -defined c4 . b -valued Function-like quasi_total Element of bool [:(h . b),(c4 . b):]
(b "") . b is Relation-like Function-like set
a9 " is Relation-like Function-like set
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
(a "") . b is Relation-like Function-like set
b9 " 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
h is Relation-like non-empty UA -defined Function-like V14(UA) set
h is Relation-like non-empty UA -defined Function-like V14(UA) set
id h is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
c4 is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
c4 "" is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
b is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
b ** c4 is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
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
c4 . a is Relation-like Function-like 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 . a is Relation-like Function-like 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
b " is Relation-like Function-like set
rng b is set
UA is set
h is Relation-like UA -defined Function-like V14(UA) set
h is Relation-like UA -defined Function-like V14(UA) 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
h is Relation-like UA -defined Function-like V14(UA) set
h is Relation-like UA -defined Function-like V14(UA) 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
h is Relation-like UA -defined Function-like V14(UA) set
h is Relation-like UA -defined Function-like V14(UA) 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
a is Relation-like Function-like 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
a9 is Relation-like Function-like set
dom a9 is set
rng a9 is set
UA is set
h is Relation-like UA -defined Function-like V14(UA) set
h is Relation-like UA -defined Function-like V14(UA) set
(UA,h,h) is non empty set
(Funcs) (h,h) is Relation-like UA -defined Function-like V14(UA) set
b is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
dom ((Funcs) (h,h)) is set
a is set
b is Element of UA
b . b is Relation-like Function-like set
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
b . a is Relation-like Function-like set
((Funcs) (h,h)) . a is set
dom b is set
product ((Funcs) (h,h)) is set
UA is set
h is Relation-like UA -defined Function-like V14(UA) set
(Funcs) (h,h) is Relation-like UA -defined Function-like V14(UA) set
h is set
((Funcs) (h,h)) . h is set
id h is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
(id h) . h is Relation-like Function-like 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
h is Relation-like UA -defined Function-like V14(UA) 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 Relation-like UA -defined Function-like V14(UA) set
id h is Relation-like UA -defined Function-like V14(UA) Function-yielding V118() ManySortedFunction of h,h
h is set
(id h) . h is Relation-like Function-like 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
(id h) . h is Relation-like Function-like 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)
0 .--> h is Relation-like K119() -defined {0} -defined (UA) -valued Function-like one-to-one Function-yielding V118() set
{0} --> h is Relation-like non-empty non empty-yielding {0} -defined (UA) -valued {h} -valued Function-like constant non empty V14({0}) quasi_total Function-yielding V118() Element of bool [:{0},{h}:]
{h} is functional non empty set
[:{0},{h}:] is non empty set
bool [:{0},{h}:] 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
MSAlg h is strict non-empty MSAlgebra over MSSign h
(MSAlg h) Over (MSSign UA) is strict non-empty MSAlgebra over MSSign UA
the Sorts of ((MSAlg h) 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 (MSSign h) -defined Function-like non empty V14( the carrier of (MSSign h)) set
the carrier of (MSSign h) is non empty trivial V31() set
MSCharact h is Relation-like the carrier' of (MSSign h) -defined Function-like non empty V14( the carrier' of (MSSign h)) ManySortedFunction of the Arity of (MSSign h) * K266( the carrier of (MSSign h),(MSSorts h)), the ResultSort of (MSSign h) * (MSSorts h)
the carrier' of (MSSign h) is non empty set
the Arity of (MSSign h) is Relation-like the carrier' of (MSSign h) -defined K263( the carrier of (MSSign h)) -valued Function-like quasi_total Element of bool [: the carrier' of (MSSign h),K263( the carrier of (MSSign h)):]
K263( the carrier of (MSSign h)) is M12( the carrier of (MSSign h))
[: the carrier' of (MSSign h),K263( the carrier of (MSSign h)):] is set
bool [: the carrier' of (MSSign h),K263( the carrier of (MSSign h)):] is non empty set
K266( the carrier of (MSSign h),(MSSorts h)) is Relation-like K263( the carrier of (MSSign h)) -defined Function-like V14(K263( the carrier of (MSSign h))) set
the Arity of (MSSign h) * K266( the carrier of (MSSign h),(MSSorts h)) is Relation-like Function-like set
the ResultSort of (MSSign h) is Relation-like the carrier' of (MSSign h) -defined the carrier of (MSSign h) -valued Function-like non empty V14( the carrier' of (MSSign h)) quasi_total Element of bool [: the carrier' of (MSSign h), the carrier of (MSSign h):]
[: the carrier' of (MSSign h), the carrier of (MSSign h):] is non empty set
bool [: the carrier' of (MSSign h), the carrier of (MSSign h):] is non empty set
the ResultSort of (MSSign h) * (MSSorts h) is Relation-like Function-like set
MSAlgebra(# (MSSorts h),(MSCharact h) #) 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 ((MSAlg h) Over (MSSign UA))
h . 0 is Relation-like Function-like set
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),(MSCharact UA) #) is strict MSAlgebra over MSSign UA
(MSSorts h) . 0 is set
0 .--> the carrier of h is Relation-like K119() -defined {0} -defined Function-like one-to-one set
{0} --> the carrier of h is Relation-like non-empty non empty-yielding {0} -defined { the carrier of h} -valued Function-like constant non empty V14({0}) quasi_total Element of bool [:{0},{ the carrier of h}:]
{ the carrier of h} is non empty set
[:{0},{ the carrier of h}:] is non empty set
bool [:{0},{ the carrier of h}:] is non empty set
(0 .--> the carrier of h) . 0 is set
(MSSorts UA) . 0 is set
0 .--> the carrier of UA is Relation-like K119() -defined {0} -defined Function-like one-to-one set
{0} --> the carrier of UA is Relation-like non-empty non empty-yielding {0} -defined { the carrier of UA} -valued Function-like constant non empty V14({0}) quasi_total Element of bool [:{0},{ the carrier of UA}:]
{ the carrier of UA} is non empty set
[:{0},{ the carrier of UA}:] is non empty set
bool [:{0},{ 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)
0 .--> h is Relation-like K119() -defined {0} -defined (UA) -valued Function-like one-to-one Function-yielding V118() set
{0} --> h is Relation-like non-empty non empty-yielding {0} -defined (UA) -valued {h} -valued Function-like constant non empty V14({0}) quasi_total Function-yielding V118() Element of bool [:{0},{h}:]
{h} is functional non empty set
[:{0},{h}:] is non empty set
bool [:{0},{h}:] 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
h is Relation-like Function-like 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)
0 .--> c4 is Relation-like K119() -defined {0} -defined Function-like one-to-one set
{0} --> c4 is Relation-like {0} -defined {c4} -valued Function-like constant non empty V14({0}) quasi_total Element of bool [:{0},{c4}:]
{c4} is non empty set
[:{0},{c4}:] is non empty set
bool [:{0},{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 Function-like set
0 .--> (c4 . 0) is Relation-like K119() -defined {0} -defined Function-like one-to-one Function-yielding V118() set
{0} --> (c4 . 0) is Relation-like {0} -defined {(c4 . 0)} -valued Function-like constant non empty V14({0}) quasi_total Function-yielding V118() Element of bool [:{0},{(c4 . 0)}:]
{(c4 . 0)} is functional non empty set
[:{0},{(c4 . 0)}:] is non empty set
bool [:{0},{(c4 . 0)}:] is non empty set
b is Relation-like Function-like set
h . b 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 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 bool [: the carrier of UA, the carrier of UA:]
MSAlg 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) Over (MSSign UA))
b is set
h . b is 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 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
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 Group-like associative multMagma
((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
((MSSign UA),(MSAlg UA)) is Relation-like [:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):] -defined ((MSSign UA),(MSAlg UA)) -valued Function-like non empty 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 non empty set
[:[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):],((MSSign UA),(MSAlg UA)):] is non empty set
bool [:[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):],((MSSign UA),(MSAlg UA)):] is non empty set
multMagma(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)) #) is strict multMagma
the carrier of ((MSSign UA),(MSAlg UA)) is non empty set
[: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):] is non empty set
bool [: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):] is non empty set
h is Relation-like Function-like set
dom h is set
rng h is set
b 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)):]
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 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) . (a,b) is Element of the carrier of (UA)
b . (a * b) is Element of the carrier of ((MSSign UA),(MSAlg UA))
b . a is Element of the carrier of ((MSSign UA),(MSAlg UA))
b . b is Element of the carrier of ((MSSign UA),(MSAlg UA))
(b . a) * (b . b) is Element of the carrier of ((MSSign UA),(MSAlg UA))
the multF of ((MSSign UA),(MSAlg UA)) is Relation-like [: the carrier of ((MSSign UA),(MSAlg UA)), the carrier of ((MSSign UA),(MSAlg UA)):] -defined the carrier of ((MSSign UA),(MSAlg UA)) -valued Function-like non empty V14([: the carrier of ((MSSign UA),(MSAlg UA)), the carrier of ((MSSign UA),(MSAlg UA)):]) quasi_total Element of bool [:[: the carrier of ((MSSign UA),(MSAlg UA)), the carrier of ((MSSign UA),(MSAlg UA)):], the carrier of ((MSSign UA),(MSAlg UA)):]
[: the carrier of ((MSSign UA),(MSAlg UA)), the carrier of ((MSSign UA),(MSAlg UA)):] is non empty set
[:[: the carrier of ((MSSign UA),(MSAlg UA)), the carrier of ((MSSign UA),(MSAlg UA)):], the carrier of ((MSSign UA),(MSAlg UA)):] is non empty set
bool [:[: the carrier of ((MSSign UA),(MSAlg UA)), the carrier of ((MSSign UA),(MSAlg UA)):], the carrier of ((MSSign UA),(MSAlg UA)):] is non empty set
the multF of ((MSSign UA),(MSAlg UA)) . ((b . a),(b . b)) is Element of the carrier of ((MSSign UA),(MSAlg UA))
a9 is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
b9 is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of (UA)
b9 * a9 is Relation-like the carrier of UA -defined the carrier of UA -valued Function-like non empty V14( the carrier of UA) quasi_total Element of bool [: the carrier of UA, the carrier of UA:]
[: 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
b . (b9 * a9) is set
0 .--> (b9 * a9) is Relation-like K119() -defined {0} -defined bool [: the carrier of UA, the carrier of UA:] -valued Function-like one-to-one Function-yielding V118() set
{0} --> (b9 * a9) is Relation-like non-empty non empty-yielding {0} -defined bool [: the carrier of UA, the carrier of UA:] -valued {(b9 * a9)} -valued Function-like constant non empty V14({0}) quasi_total Function-yielding V118() Element of bool [:{0},{(b9 * a9)}:]
{(b9 * a9)} is functional non empty set
[:{0},{(b9 * a9)}:] is non empty set
bool [:{0},{(b9 * a9)}:] is non empty set
0 .--> a9 is Relation-like K119() -defined {0} -defined (UA) -valued Function-like one-to-one Function-yielding V118() set
{0} --> a9 is Relation-like non-empty non empty-yielding {0} -defined (UA) -valued {a9} -valued Function-like constant non empty V14({0}) quasi_total Function-yielding V118() Element of bool [:{0},{a9}:]
{a9} is functional non empty set
[:{0},{a9}:] is non empty set
bool [:{0},{a9}:] is non empty set
0 .--> b9 is Relation-like K119() -defined {0} -defined (UA) -valued Function-like one-to-one Function-yielding V118() set
{0} --> b9 is Relation-like non-empty non empty-yielding {0} -defined (UA) -valued {b9} -valued Function-like constant non empty V14({0}) quasi_total Function-yielding V118() Element of bool [:{0},{b9}:]
{b9} is functional non empty set
[:{0},{b9}:] is non empty set
bool [:{0},{b9}:] 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)
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)
ha is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding V118() ( the carrier of (MSSign UA), the Sorts of (MSAlg UA),((MSSign UA),(MSAlg UA)))
A9 is Element of the carrier of ((MSSign UA),(MSAlg UA))
hb is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding V118() ( the carrier of (MSSign UA), the Sorts of (MSAlg UA),((MSSign UA),(MSAlg UA)))
B9 is Element of the carrier of ((MSSign UA),(MSAlg UA))
MSAlg (b9 * a9) is Relation-like the carrier of (MSSign UA) -defined Function-like non empty V14( the carrier of (MSSign UA)) Function-yielding 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
MSAlg a9 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 b9 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 b9) ** (MSAlg a9) is Relation-like Function-like Function-yielding V118() set
B ** (MSAlg a9) is Relation-like Function-like Function-yielding V118() set
B ** 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)
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
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 Group-like associative multMagma
((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
((MSSign UA),(MSAlg UA)) is Relation-like [:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):] -defined ((MSSign UA),(MSAlg UA)) -valued Function-like non empty 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 non empty set
[:[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):],((MSSign UA),(MSAlg UA)):] is non empty set
bool [:[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):],((MSSign UA),(MSAlg UA)):] is non empty set
multMagma(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)) #) is strict multMagma
the carrier of ((MSSign UA),(MSAlg UA)) is non empty set
[: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):] is non empty set
bool [: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):] is non empty set
h is Relation-like the carrier of (UA) -defined the carrier of ((MSSign UA),(MSAlg UA)) -valued Function-like non empty V14( the carrier of (UA)) quasi_total V104((UA),((MSSign UA),(MSAlg UA))) Element of bool [: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):]
c4 is Element of the carrier of (UA)
h . c4 is Element of the carrier of ((MSSign UA),(MSAlg UA))
b is Element of the carrier of (UA)
h . b is Element of the carrier of ((MSSign UA),(MSAlg UA))
0 .--> b is Relation-like K119() -defined {0} -defined the carrier of (UA) -valued Function-like one-to-one set
{0} --> b is Relation-like {0} -defined the carrier of (UA) -valued {b} -valued Function-like constant non empty V14({0}) quasi_total Element of bool [:{0},{b}:]
{b} is non empty set
[:{0},{b}:] is non empty set
bool [:{0},{b}:] is non empty set
0 .--> c4 is Relation-like K119() -defined {0} -defined the carrier of (UA) -valued Function-like one-to-one set
{0} --> c4 is Relation-like {0} -defined the carrier of (UA) -valued {c4} -valued Function-like constant non empty V14({0}) quasi_total Element of bool [:{0},{c4}:]
{c4} is non empty set
[:{0},{c4}:] is non empty set
bool [:{0},{c4}:] is non empty set
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
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 Group-like associative multMagma
((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
((MSSign UA),(MSAlg UA)) is Relation-like [:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):] -defined ((MSSign UA),(MSAlg UA)) -valued Function-like non empty 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 non empty set
[:[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):],((MSSign UA),(MSAlg UA)):] is non empty set
bool [:[:((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)):],((MSSign UA),(MSAlg UA)):] is non empty set
multMagma(# ((MSSign UA),(MSAlg UA)),((MSSign UA),(MSAlg UA)) #) is strict multMagma
h is Relation-like Function-like set
dom h is set
the carrier of (UA) is non empty set
the carrier of ((MSSign UA),(MSAlg UA)) is non empty set
[: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):] is non empty set
bool [: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):] is non empty set
h is Relation-like the carrier of (UA) -defined the carrier of ((MSSign UA),(MSAlg UA)) -valued Function-like non empty V14( the carrier of (UA)) quasi_total V104((UA),((MSSign UA),(MSAlg UA))) Element of bool [: the carrier of (UA), the carrier of ((MSSign UA),(MSAlg UA)):]