:: BIRKHOFF semantic presentation

NAT is non empty V34() V35() V36() Element of bool REAL
REAL is set

NAT is non empty V34() V35() V36() set

{} is empty V34() V35() V36() V38() V39() V40() set
1 is non empty set
{{},1} is non empty set
K274() is set
bool K274() is set
K275() is Element of bool K274()
K315() is non empty V118() L13()
the carrier of K315() is non empty set
K278( the carrier of K315()) is non empty M20( the carrier of K315())
K314(K315()) is Element of bool K278( the carrier of K315())
bool K278( the carrier of K315()) is set
[:K314(K315()),NAT:] is set
bool [:K314(K315()),NAT:] is set
[:NAT,K314(K315()):] is set
bool [:NAT,K314(K315()):] is set

K359() is non empty V73() L9()
the carrier of K359() is non empty set
K362() is Element of bool NAT
[:K362(),K362():] is set
[:[:K362(),K362():],K362():] is set
bool [:[:K362(),K362():],K362():] is set

is non empty set
XX is non empty non void V62() ManySortedSign
the carrier of XX is non empty set
I is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) set
E is non-empty MSAlgebra over XX
the Sorts of E is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) set
FreeMSA I is non-empty V126(XX) MSAlgebra over XX
the Sorts of () is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) set
FreeGen I is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) V125(XX, FreeMSA I) GeneratorSet of FreeMSA I

E is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of I, the Sorts of E
E ** () is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E
K is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (), the Sorts of E
K || () is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E
F is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (), the Sorts of E
F || () is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E
XX is non empty non void V62() ManySortedSign
the carrier of XX is non empty set
I is non-empty MSAlgebra over XX
the Sorts of I is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) set
E is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) set
E is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of E, the Sorts of I
rngs E is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) set
(XX,E,I,E) is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (), the Sorts of I
FreeMSA E is non-empty V126(XX) MSAlgebra over XX
the Sorts of () is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) set
rngs (XX,E,I,E) is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) set

FreeGen E is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) V125(XX, FreeMSA E) GeneratorSet of FreeMSA E
F is set
(rngs E) . F is set
(rngs (XX,E,I,E)) . F is set
B is set
A is Element of the carrier of XX
() . A is non empty set
() . A is Relation-like () . A -defined E . A -valued Function-like non empty V14(() . A) V18(() . A,E . A) Element of bool [:(() . A),(E . A):]
E . A is non empty set
[:(() . A),(E . A):] is set
bool [:(() . A),(E . A):] is set
dom (() . A) is Element of bool (() . A)
bool (() . A) is set
the Sorts of () . A is non empty set
the Sorts of I . A is non empty set
E . A is Relation-like E . A -defined the Sorts of I . A -valued Function-like non empty V14(E . A) V18(E . A, the Sorts of I . A) Element of bool [:(E . A),( the Sorts of I . A):]
[:(E . A),( the Sorts of I . A):] is set
bool [:(E . A),( the Sorts of I . A):] is set
rng (E . A) is non empty Element of bool ( the Sorts of I . A)
bool ( the Sorts of I . A) is set
dom (E . A) is Element of bool (E . A)
bool (E . A) is set
e is set
(E . A) . e is set
rngs () is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) set
rng (() . A) is non empty Element of bool (E . A)
x is set
(() . A) . x is set
(XX,E,I,E) . A is Relation-like the Sorts of () . A -defined the Sorts of I . A -valued Function-like non empty V14( the Sorts of () . A) V18( the Sorts of () . A, the Sorts of I . A) Element of bool [:( the Sorts of () . A),( the Sorts of I . A):]
[:( the Sorts of () . A),( the Sorts of I . A):] is set
bool [:( the Sorts of () . A),( the Sorts of I . A):] is set
dom ((XX,E,I,E) . A) is Element of bool ( the Sorts of () . A)
bool ( the Sorts of () . A) is set
(E . A) * (() . A) is Relation-like () . A -defined the Sorts of I . A -valued Function-like non empty V14(() . A) V18(() . A, the Sorts of I . A) Element of bool [:(() . A),( the Sorts of I . A):]
[:(() . A),( the Sorts of I . A):] is set
bool [:(() . A),( the Sorts of I . A):] is set
((E . A) * (() . A)) . x is set
E ** () is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of FreeGen E, the Sorts of I
(E ** ()) . A is Relation-like () . A -defined the Sorts of I . A -valued Function-like non empty V14(() . A) V18(() . A, the Sorts of I . A) Element of bool [:(() . A),( the Sorts of I . A):]
((E ** ()) . A) . x is set
(XX,E,I,E) || () is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of FreeGen E, the Sorts of I
((XX,E,I,E) || ()) . A is Relation-like () . A -defined the Sorts of I . A -valued Function-like non empty V14(() . A) V18(() . A, the Sorts of I . A) Element of bool [:(() . A),( the Sorts of I . A):]
(((XX,E,I,E) || ()) . A) . x is set
((XX,E,I,E) . A) | (() . A) is Relation-like the Sorts of () . A -defined the Sorts of I . A -valued Function-like Element of bool [:( the Sorts of () . A),( the Sorts of I . A):]
(((XX,E,I,E) . A) | (() . A)) . x is set
((XX,E,I,E) . A) . x is set
rng ((XX,E,I,E) . A) is non empty Element of bool ( the Sorts of I . A)
F1() is non empty non void V62() ManySortedSign
the carrier of F1() is non empty set
F2() is non-empty MSAlgebra over F1()
the Sorts of F2() is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set

CongrLatt F2() is non empty V73() V80() V85() M30( EqRelLatt the Sorts of F2())
EqRelLatt the Sorts of F2() is non empty V73() V80() L9()
the carrier of (CongrLatt F2()) is non empty set
{ b1 where b1 is Element of the carrier of (CongrLatt F2()) : ex b2 being Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2() st
( b2 = b1 & P1[ QuotMSAlg (F2(),b2)] )
}
is set

the carrier of F1() --> is Relation-like non-empty non empty-yielding the carrier of F1() -defined -valued Function-like constant non empty V14( the carrier of F1()) V18( the carrier of F1(),) Element of bool [: the carrier of F1(),:]
is non empty set
[: the carrier of F1(),:] is set
bool [: the carrier of F1(),:] is set
K is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
{K} is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
F is set
product the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F1() is non-empty MSAlgebra over F1()
SORTS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F1() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
OPS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F1() is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),()), the ResultSort of F1() * ()
the carrier' of F1() is non empty set
the Arity of F1() is Relation-like the carrier' of F1() -defined K171( the carrier of F1()) -valued Function-like V18( the carrier' of F1(),K171( the carrier of F1())) Element of bool [: the carrier' of F1(),K171( the carrier of F1()):]
K171( the carrier of F1()) is M11( the carrier of F1())
[: the carrier' of F1(),K171( the carrier of F1()):] is set
bool [: the carrier' of F1(),K171( the carrier of F1()):] is set
K174( the carrier of F1(),()) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),()) is Relation-like set
the ResultSort of F1() is Relation-like the carrier' of F1() -defined the carrier of F1() -valued Function-like non empty V14( the carrier' of F1()) V18( the carrier' of F1(), the carrier of F1()) Element of bool [: the carrier' of F1(), the carrier of F1():]
[: the carrier' of F1(), the carrier of F1():] is set
bool [: the carrier' of F1(), the carrier of F1():] is set
the ResultSort of F1() * () is Relation-like set
MSAlgebra(# (),() #) is strict MSAlgebra over F1()
the Sorts of () is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
the Sorts of () . F is set
A is Element of the carrier of F1()

product (Carrier ( the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F1(),A)) is set
( the carrier of F1() --> ) . A is non empty Element of
{K} . F is set
[| the Sorts of F2(), the Sorts of F2()|] is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
F is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
QuotMSAlg (F2(),F) is strict non-empty MSAlgebra over F1()
Class F is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
QuotCharact F is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),()), the ResultSort of F1() * ()
K174( the carrier of F1(),()) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),()) is Relation-like set
the ResultSort of F1() * () is Relation-like set
MSAlgebra(# (),() #) is strict MSAlgebra over F1()
the Sorts of (QuotMSAlg (F2(),F)) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
{ the Sorts of F2()} is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set

A is set

A is set
B is Element of the carrier of (CongrLatt F2())
e is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
QuotMSAlg (F2(),e) is strict non-empty MSAlgebra over F1()
Class e is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
QuotCharact e is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),()), the ResultSort of F1() * ()
K174( the carrier of F1(),()) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),()) is Relation-like set
the ResultSort of F1() * () is Relation-like set
MSAlgebra(# (),() #) is strict MSAlgebra over F1()
the carrier of (EqRelLatt the Sorts of F2()) is non empty set
A is set
Bool [| the Sorts of F2(), the Sorts of F2()|] is functional non empty with_common_domain set
bool (Bool [| the Sorts of F2(), the Sorts of F2()|]) is set
A is non empty Element of bool (Bool [| the Sorts of F2(), the Sorts of F2()|])
|:A:| is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) ManySortedSubset of K109( the carrier of F1(),[| the Sorts of F2(), the Sorts of F2()|])
K109( the carrier of F1(),[| the Sorts of F2(), the Sorts of F2()|]) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
meet |:A:| is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) ManySortedSubset of [| the Sorts of F2(), the Sorts of F2()|]
e is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding ManySortedRelation of the Sorts of F2(), the Sorts of F2()
x is set
the Sorts of F2() . x is set
[:( the Sorts of F2() . x),( the Sorts of F2() . x):] is set
bool [:( the Sorts of F2() . x),( the Sorts of F2() . x):] is set
e . x is set
h is Relation-like the Sorts of F2() . x -defined the Sorts of F2() . x -valued Element of bool [:( the Sorts of F2() . x),( the Sorts of F2() . x):]
{ b1 where b1 is Element of the carrier of (CongrLatt F2()) : S2[b1] } is set
bool the carrier of (CongrLatt F2()) is set
x is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
h is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
QuotMSAlg (F2(),h) is strict non-empty MSAlgebra over F1()
Class h is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
QuotCharact h is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),()), the ResultSort of F1() * ()
K174( the carrier of F1(),()) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),()) is Relation-like set
the ResultSort of F1() * () is Relation-like set
MSAlgebra(# (),() #) is strict MSAlgebra over F1()
t2 is strict non-empty MSAlgebra over F1()
the Sorts of t2 is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
MSNat_Hom (F2(),h) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of (QuotMSAlg (F2(),h))
the Sorts of (QuotMSAlg (F2(),h)) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
e is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of t2
fi is set
x is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
QuotMSAlg (F2(),x) is strict non-empty MSAlgebra over F1()
Class x is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
QuotCharact x is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),()), the ResultSort of F1() * ()
K174( the carrier of F1(),()) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),()) is Relation-like set
the ResultSort of F1() * () is Relation-like set
MSAlgebra(# (),() #) is strict MSAlgebra over F1()
FofI1 is set
FofI1 is set

x is set
fi . x is set
FofI1 is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
QuotMSAlg (F2(),FofI1) is strict non-empty MSAlgebra over F1()
Class FofI1 is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
QuotCharact FofI1 is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),(Class FofI1)), the ResultSort of F1() * (Class FofI1)
K174( the carrier of F1(),(Class FofI1)) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),(Class FofI1)) is Relation-like set
the ResultSort of F1() * (Class FofI1) is Relation-like set
MSAlgebra(# (Class FofI1),(QuotCharact FofI1) #) is strict MSAlgebra over F1()
x is Relation-like A -defined Function-like non empty V14(A) MSAlgebra-Family of A,F1()
FofI1 is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Element of A
x . FofI1 is non-empty MSAlgebra over F1()
the Sorts of (x . FofI1) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
FofI1 is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
QuotMSAlg (F2(),FofI1) is strict non-empty MSAlgebra over F1()
Class FofI1 is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
QuotCharact FofI1 is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),(Class FofI1)), the ResultSort of F1() * (Class FofI1)
K174( the carrier of F1(),(Class FofI1)) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),(Class FofI1)) is Relation-like set
the ResultSort of F1() * (Class FofI1) is Relation-like set
MSAlgebra(# (Class FofI1),(QuotCharact FofI1) #) is strict MSAlgebra over F1()
MSNat_Hom (F2(),FofI1) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of (QuotMSAlg (F2(),FofI1))
the Sorts of (QuotMSAlg (F2(),FofI1)) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
XX is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of (x . FofI1)
FofI1 is Relation-like A -defined Function-like non empty V14(A) set
FofI1 is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Element of A
x . FofI1 is non-empty MSAlgebra over F1()
the Sorts of (x . FofI1) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
FofI1 . FofI1 is set
H is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of (x . FofI1)
FofI1 is set
dom FofI1 is set
FofI1 . FofI1 is set
dom FofI1 is Element of bool A
bool A is set
H is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Element of A
x . H is non-empty MSAlgebra over F1()
the Sorts of (x . H) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
FofI1 . H is set
XX is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of (x . H)
product x is non-empty MSAlgebra over F1()
SORTS x is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
OPS x is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),()), the ResultSort of F1() * ()
K174( the carrier of F1(),()) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),()) is Relation-like set
the ResultSort of F1() * () is Relation-like set
MSAlgebra(# (),(OPS x) #) is strict MSAlgebra over F1()
the Sorts of () is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set

H is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of ()
XX is set
B is Element of the carrier of F1()
[| the Sorts of F2(), the Sorts of F2()|] . B is set
bool ([| the Sorts of F2(), the Sorts of F2()|] . B) is set
bool (bool ([| the Sorts of F2(), the Sorts of F2()|] . B)) is set
|:A:| . B is non empty Element of bool (bool ([| the Sorts of F2(), the Sorts of F2()|] . B))
() . B is set
G is Element of bool (bool ([| the Sorts of F2(), the Sorts of F2()|] . B))
Intersect G is Element of bool ([| the Sorts of F2(), the Sorts of F2()|] . B)
Bool [| the Sorts of F2(), the Sorts of F2()|] is functional non empty with_common_domain V143( the carrier of F1(),[| the Sorts of F2(), the Sorts of F2()|]) V144( the carrier of F1(),[| the Sorts of F2(), the Sorts of F2()|]) V145( the carrier of F1(),[| the Sorts of F2(), the Sorts of F2()|]) V146( the carrier of F1(),[| the Sorts of F2(), the Sorts of F2()|]) V147( the carrier of F1(),[| the Sorts of F2(), the Sorts of F2()|]) V148( the carrier of F1(),[| the Sorts of F2(), the Sorts of F2()|]) Element of bool (Bool [| the Sorts of F2(), the Sorts of F2()|])
{ (b1 . B) where b1 is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Element of Bool [| the Sorts of F2(), the Sorts of F2()|] : b1 in A } is set
the Sorts of F2() . B is non empty set
MSCng H is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
() . B is Relation-like the Sorts of F2() . B -defined the Sorts of F2() . B -valued V14( the Sorts of F2() . B) V18( the Sorts of F2() . B, the Sorts of F2() . B) V134() V139() Element of bool [:( the Sorts of F2() . B),( the Sorts of F2() . B):]
[:( the Sorts of F2() . B),( the Sorts of F2() . B):] is set
bool [:( the Sorts of F2() . B),( the Sorts of F2() . B):] is set
h . B is Relation-like the Sorts of F2() . B -defined the Sorts of F2() . B -valued V14( the Sorts of F2() . B) V18( the Sorts of F2() . B, the Sorts of F2() . B) V134() V139() Element of bool [:( the Sorts of F2() . B),( the Sorts of F2() . B):]
C is set
H is set
[C,H] is V15() set
{C,H} is non empty set
{C} is non empty set
{{C,H},{C}} is non empty set
MSCng (H,B) is Relation-like the Sorts of F2() . B -defined the Sorts of F2() . B -valued V14( the Sorts of F2() . B) V18( the Sorts of F2() . B, the Sorts of F2() . B) V134() V139() Element of bool [:( the Sorts of F2() . B),( the Sorts of F2() . B):]
K is set
t1 is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Element of Bool [| the Sorts of F2(), the Sorts of F2()|]
t1 . B is set
F1 is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Element of A
x . F1 is non-empty MSAlgebra over F1()
the Sorts of (x . F1) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
FofI1 . F1 is Relation-like Function-like set
F1 is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of (x . F1)
F1 . B is Relation-like the Sorts of F2() . B -defined the Sorts of (x . F1) . B -valued Function-like non empty V14( the Sorts of F2() . B) V18( the Sorts of F2() . B, the Sorts of (x . F1) . B) Element of bool [:( the Sorts of F2() . B),( the Sorts of (x . F1) . B):]
the Sorts of (x . F1) . B is non empty set
[:( the Sorts of F2() . B),( the Sorts of (x . F1) . B):] is set
bool [:( the Sorts of F2() . B),( the Sorts of (x . F1) . B):] is set
(F1 . B) . C is set
proj (x,F1) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (), the Sorts of (x . F1)
(proj (x,F1)) ** H is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of (x . F1)
((proj (x,F1)) ** H) . B is Relation-like the Sorts of F2() . B -defined the Sorts of (x . F1) . B -valued Function-like non empty V14( the Sorts of F2() . B) V18( the Sorts of F2() . B, the Sorts of (x . F1) . B) Element of bool [:( the Sorts of F2() . B),( the Sorts of (x . F1) . B):]
(((proj (x,F1)) ** H) . B) . C is set
the Sorts of () . B is non empty set
H . B is Relation-like the Sorts of F2() . B -defined the Sorts of () . B -valued Function-like non empty V14( the Sorts of F2() . B) V18( the Sorts of F2() . B, the Sorts of () . B) Element of bool [:( the Sorts of F2() . B),( the Sorts of () . B):]
[:( the Sorts of F2() . B),( the Sorts of () . B):] is set
bool [:( the Sorts of F2() . B),( the Sorts of () . B):] is set
(proj (x,F1)) . B is Relation-like the Sorts of () . B -defined the Sorts of (x . F1) . B -valued Function-like non empty V14( the Sorts of () . B) V18( the Sorts of () . B, the Sorts of (x . F1) . B) Element of bool [:( the Sorts of () . B),( the Sorts of (x . F1) . B):]
[:( the Sorts of () . B),( the Sorts of (x . F1) . B):] is set
bool [:( the Sorts of () . B),( the Sorts of (x . F1) . B):] is set
((proj (x,F1)) . B) * (H . B) is Relation-like the Sorts of F2() . B -defined the Sorts of (x . F1) . B -valued Function-like non empty V14( the Sorts of F2() . B) V18( the Sorts of F2() . B, the Sorts of (x . F1) . B) Element of bool [:( the Sorts of F2() . B),( the Sorts of (x . F1) . B):]
(((proj (x,F1)) . B) * (H . B)) . C is set
(H . B) . C is set
((proj (x,F1)) . B) . ((H . B) . C) is set
(H . B) . H is set
((proj (x,F1)) . B) . ((H . B) . H) is set
(((proj (x,F1)) . B) * (H . B)) . H is set
(((proj (x,F1)) ** H) . B) . H is set
(F1 . B) . H is set
c28 is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
MSNat_Hom (F2(),c28) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of (QuotMSAlg (F2(),c28))
QuotMSAlg (F2(),c28) is strict non-empty MSAlgebra over F1()
Class c28 is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
QuotCharact c28 is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),(Class c28)), the ResultSort of F1() * (Class c28)
K174( the carrier of F1(),(Class c28)) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),(Class c28)) is Relation-like set
the ResultSort of F1() * (Class c28) is Relation-like set
MSAlgebra(# (Class c28),(QuotCharact c28) #) is strict MSAlgebra over F1()
the Sorts of (QuotMSAlg (F2(),c28)) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
Carrier (x,B) is Relation-like A -defined Function-like non empty V14(A) set
H . B is Relation-like the Sorts of F2() . B -defined the Sorts of () . B -valued Function-like non empty V14( the Sorts of F2() . B) V18( the Sorts of F2() . B, the Sorts of () . B) Element of bool [:( the Sorts of F2() . B),( the Sorts of () . B):]
the Sorts of () . B is non empty set
[:( the Sorts of F2() . B),( the Sorts of () . B):] is set
bool [:( the Sorts of F2() . B),( the Sorts of () . B):] is set
(H . B) . C is set
(H . B) . H is set
K is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Element of A
proj ((Carrier (x,B)),K) is Relation-like Function-like set
(proj ((Carrier (x,B)),K)) . ((H . B) . C) is set
(proj ((Carrier (x,B)),K)) . ((H . B) . H) is set
x . K is non-empty MSAlgebra over F1()
the Sorts of (x . K) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
FofI1 . K is Relation-like Function-like set
F1 is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of (x . K)
t1 is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
t1 . B is Relation-like the Sorts of F2() . B -defined the Sorts of F2() . B -valued V14( the Sorts of F2() . B) V18( the Sorts of F2() . B, the Sorts of F2() . B) V134() V139() Element of bool [:( the Sorts of F2() . B),( the Sorts of F2() . B):]
proj (x,K) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (), the Sorts of (x . K)
(proj (x,K)) . B is Relation-like the Sorts of () . B -defined the Sorts of (x . K) . B -valued Function-like non empty V14( the Sorts of () . B) V18( the Sorts of () . B, the Sorts of (x . K) . B) Element of bool [:( the Sorts of () . B),( the Sorts of (x . K) . B):]
the Sorts of (x . K) . B is non empty set
[:( the Sorts of () . B),( the Sorts of (x . K) . B):] is set
bool [:( the Sorts of () . B),( the Sorts of (x . K) . B):] is set
((proj (x,K)) . B) . ((H . B) . C) is set
((proj (x,K)) . B) * (H . B) is Relation-like the Sorts of F2() . B -defined the Sorts of (x . K) . B -valued Function-like non empty V14( the Sorts of F2() . B) V18( the Sorts of F2() . B, the Sorts of (x . K) . B) Element of bool [:( the Sorts of F2() . B),( the Sorts of (x . K) . B):]
[:( the Sorts of F2() . B),( the Sorts of (x . K) . B):] is set
bool [:( the Sorts of F2() . B),( the Sorts of (x . K) . B):] is set
(((proj (x,K)) . B) * (H . B)) . C is set
(proj (x,K)) ** H is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of (x . K)
((proj (x,K)) ** H) . B is Relation-like the Sorts of F2() . B -defined the Sorts of (x . K) . B -valued Function-like non empty V14( the Sorts of F2() . B) V18( the Sorts of F2() . B, the Sorts of (x . K) . B) Element of bool [:( the Sorts of F2() . B),( the Sorts of (x . K) . B):]
(((proj (x,K)) ** H) . B) . C is set
F1 . B is Relation-like the Sorts of F2() . B -defined the Sorts of (x . K) . B -valued Function-like non empty V14( the Sorts of F2() . B) V18( the Sorts of F2() . B, the Sorts of (x . K) . B) Element of bool [:( the Sorts of F2() . B),( the Sorts of (x . K) . B):]
(F1 . B) . C is set
(F1 . B) . H is set
(((proj (x,K)) ** H) . B) . H is set
(((proj (x,K)) . B) * (H . B)) . H is set
((proj (x,K)) . B) . ((H . B) . H) is set
F1 is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
MSNat_Hom (F2(),F1) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of (QuotMSAlg (F2(),F1))
QuotMSAlg (F2(),F1) is strict non-empty MSAlgebra over F1()
Class F1 is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
QuotCharact F1 is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),(Class F1)), the ResultSort of F1() * (Class F1)
K174( the carrier of F1(),(Class F1)) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),(Class F1)) is Relation-like set
the ResultSort of F1() * (Class F1) is Relation-like set
MSAlgebra(# (Class F1),() #) is strict MSAlgebra over F1()
the Sorts of (QuotMSAlg (F2(),F1)) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
product (Carrier (x,B)) is set
() . XX is set
h . XX is set
QuotMSAlg (F2(),()) is strict non-empty MSAlgebra over F1()
Class () is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
QuotCharact () is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),(Class ())), the ResultSort of F1() * (Class ())
K174( the carrier of F1(),(Class ())) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),(Class ())) is Relation-like set
the ResultSort of F1() * (Class ()) is Relation-like set
MSAlgebra(# (Class ()),(QuotCharact ()) #) is strict MSAlgebra over F1()
MSHomQuot H is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (QuotMSAlg (F2(),())), the Sorts of ()
the Sorts of (QuotMSAlg (F2(),())) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set

B is set
x . B is set
G is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Element of A
x . G is non-empty MSAlgebra over F1()
C is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
QuotMSAlg (F2(),C) is strict non-empty MSAlgebra over F1()
Class C is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
QuotCharact C is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),()), the ResultSort of F1() * ()
K174( the carrier of F1(),()) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),()) is Relation-like set
the ResultSort of F1() * () is Relation-like set
MSAlgebra(# (),() #) is strict MSAlgebra over F1()
H is Element of the carrier of (CongrLatt F2())
K is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
QuotMSAlg (F2(),K) is strict non-empty MSAlgebra over F1()
Class K is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
QuotCharact K is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),()), the ResultSort of F1() * ()
K174( the carrier of F1(),()) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),()) is Relation-like set
the ResultSort of F1() * () is Relation-like set
MSAlgebra(# (),() #) is strict MSAlgebra over F1()
B is non-empty MSAlgebra over F1()
the Sorts of B is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
G is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of B
MSCng G is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F2(), the Sorts of F2()
QuotMSAlg (F2(),()) is strict non-empty MSAlgebra over F1()
Class () is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
QuotCharact () is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),(Class ())), the ResultSort of F1() * (Class ())
K174( the carrier of F1(),(Class ())) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),(Class ())) is Relation-like set
the ResultSort of F1() * (Class ()) is Relation-like set
MSAlgebra(# (Class ()),(QuotCharact ()) #) is strict MSAlgebra over F1()
MSHomQuot G is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (QuotMSAlg (F2(),())), the Sorts of B
the Sorts of (QuotMSAlg (F2(),())) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set

H is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of t2, the Sorts of B
H ** e is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of B
K is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of t2, the Sorts of B
K ** e is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of B
F1() is non empty non void V62() ManySortedSign
the carrier of F1() is non empty set
F2() is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
XX is non-empty MSAlgebra over F1()
I is strict non-empty MSSubAlgebra of XX
XX is set
I is Relation-like XX -defined Function-like V14(XX) MSAlgebra-Family of XX,F1()
product I is non-empty MSAlgebra over F1()
SORTS I is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
OPS I is Relation-like the carrier' of F1() -defined Function-like non empty V14( the carrier' of F1()) ManySortedFunction of the Arity of F1() * K174( the carrier of F1(),()), the ResultSort of F1() * ()
the carrier' of F1() is non empty set
the Arity of F1() is Relation-like the carrier' of F1() -defined K171( the carrier of F1()) -valued Function-like V18( the carrier' of F1(),K171( the carrier of F1())) Element of bool [: the carrier' of F1(),K171( the carrier of F1()):]
K171( the carrier of F1()) is M11( the carrier of F1())
[: the carrier' of F1(),K171( the carrier of F1()):] is set
bool [: the carrier' of F1(),K171( the carrier of F1()):] is set
K174( the carrier of F1(),()) is Relation-like K171( the carrier of F1()) -defined Function-like V14(K171( the carrier of F1())) set
the Arity of F1() * K174( the carrier of F1(),()) is Relation-like set
the ResultSort of F1() is Relation-like the carrier' of F1() -defined the carrier of F1() -valued Function-like non empty V14( the carrier' of F1()) V18( the carrier' of F1(), the carrier of F1()) Element of bool [: the carrier' of F1(), the carrier of F1():]
[: the carrier' of F1(), the carrier of F1():] is set
bool [: the carrier' of F1(), the carrier of F1():] is set
the ResultSort of F1() * () is Relation-like set
MSAlgebra(# (),(OPS I) #) is strict MSAlgebra over F1()
FreeMSA F2() is non-empty V126(F1()) MSAlgebra over F1()
Reverse F2() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(),F2()
FreeGen F2() is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) V125(F1(), FreeMSA F2()) GeneratorSet of FreeMSA F2()
I is non-empty MSAlgebra over F1()
E is non-empty MSAlgebra over F1()
the Sorts of (FreeMSA F2()) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
I is strict non-empty MSAlgebra over F1()
the Sorts of I is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
E is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA F2()), the Sorts of I
(Reverse F2()) "" is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), FreeGen F2()
E || (FreeGen F2()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of I
(E || (FreeGen F2())) ** ((Reverse F2()) "") is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), the Sorts of I
E is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), the Sorts of I
K is non-empty MSAlgebra over F1()
the Sorts of K is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
F is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), the Sorts of K
F ** (Reverse F2()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
A is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA F2()), the Sorts of K
A || (FreeGen F2()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
B is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of I, the Sorts of K
B ** E is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA F2()), the Sorts of K
B ** E is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), the Sorts of K
B ** (E || (FreeGen F2())) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
rngs (Reverse F2()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
E ** (Reverse F2()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of I
((Reverse F2()) "") ** (Reverse F2()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), FreeGen F2()
(E || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2())) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of I
id (FreeGen F2()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding "1-1" "onto" ManySortedFunction of FreeGen F2(), FreeGen F2()
(E || (FreeGen F2())) ** (id (FreeGen F2())) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of I
(B ** E) ** (Reverse F2()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
e is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of I, the Sorts of K
e ** E is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), the Sorts of K
((E || (FreeGen F2())) ** ((Reverse F2()) "")) ** (Reverse F2()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of I
e ** (((E || (FreeGen F2())) ** ((Reverse F2()) "")) ** (Reverse F2())) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
B ** ((E || (FreeGen F2())) ** ((Reverse F2()) "")) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), the Sorts of K
(B ** ((E || (FreeGen F2())) ** ((Reverse F2()) ""))) ** (Reverse F2()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
B ** (((E || (FreeGen F2())) ** ((Reverse F2()) "")) ** (Reverse F2())) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
e ** ((E || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
B ** ((E || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
e ** ((E || (FreeGen F2())) ** (id (FreeGen F2()))) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
B ** ((E || (FreeGen F2())) ** (id (FreeGen F2()))) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
e ** (E || (FreeGen F2())) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
e ** E is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA F2()), the Sorts of K
(e ** E) || (FreeGen F2()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
(B ** E) || (FreeGen F2()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F2(), the Sorts of K
F1() is non empty non void V62() ManySortedSign
the carrier of F1() is non empty set
the carrier of F1() --> NAT is Relation-like non-empty non empty-yielding the carrier of F1() -defined -valued Function-like constant non empty V14( the carrier of F1()) V18( the carrier of F1(),) Element of bool [: the carrier of F1(),:]
is non empty set
[: the carrier of F1(),:] is set
bool [: the carrier of F1(),:] is set
F2() is non-empty MSAlgebra over F1()
the Sorts of F2() is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
F3() is non-empty MSAlgebra over F1()
the Sorts of F3() is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
F4() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2()
F5() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F3()
(F1(),( the carrier of F1() --> NAT),F3(),F5()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F1() --> NAT)), the Sorts of F3()
FreeMSA ( the carrier of F1() --> NAT) is non-empty V126(F1()) MSAlgebra over F1()
the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
(F1(),( the carrier of F1() --> NAT),F2(),F4()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F1() --> NAT)), the Sorts of F2()
XX is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of F3()
XX ** F4() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F3()
XX ** (F1(),( the carrier of F1() --> NAT),F2(),F4()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F1() --> NAT)), the Sorts of F3()
I is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
FreeMSA I is non-empty V126(F1()) MSAlgebra over F1()
E is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of I, the Sorts of F3()
(F1(),I,F3(),E) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (), the Sorts of F3()
the Sorts of () is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
FreeGen I is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) V125(F1(), FreeMSA I) GeneratorSet of FreeMSA I
(F1(),I,F3(),E) || () is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of F3()
Reverse I is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I,I

FreeGen ( the carrier of F1() --> NAT) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) V125(F1(), FreeMSA ( the carrier of F1() --> NAT)) GeneratorSet of FreeMSA ( the carrier of F1() --> NAT)
(F1(),( the carrier of F1() --> NAT),F2(),F4()) || (FreeGen ( the carrier of F1() --> NAT)) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen ( the carrier of F1() --> NAT), the Sorts of F2()
XX ** ((F1(),( the carrier of F1() --> NAT),F2(),F4()) || (FreeGen ( the carrier of F1() --> NAT))) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen ( the carrier of F1() --> NAT), the Sorts of F3()
(XX ** (F1(),( the carrier of F1() --> NAT),F2(),F4())) || (FreeGen ( the carrier of F1() --> NAT)) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen ( the carrier of F1() --> NAT), the Sorts of F3()
F1() is non empty non void V62() ManySortedSign
the carrier of F1() is non empty set
the carrier of F1() --> NAT is Relation-like non-empty non empty-yielding the carrier of F1() -defined -valued Function-like constant non empty V14( the carrier of F1()) V18( the carrier of F1(),) Element of bool [: the carrier of F1(),:]
is non empty set
[: the carrier of F1(),:] is set
bool [: the carrier of F1(),:] is set
F2() is non-empty MSAlgebra over F1()
the Sorts of F2() is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
TermAlg F1() is strict non-empty V126(F1()) MSAlgebra over F1()
the carrier of F1() --> NAT is Relation-like non-empty non empty-yielding the carrier of F1() -defined bool REAL -valued Function-like constant non empty V14( the carrier of F1()) V18( the carrier of F1(), bool REAL) Element of bool [: the carrier of F1(),():]
[: the carrier of F1(),():] is set
bool [: the carrier of F1(),():] is set
FreeMSA ( the carrier of F1() --> NAT) is non-empty V126(F1()) MSAlgebra over F1()
the Sorts of (TermAlg F1()) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
F4() is Element of the carrier of F1()
the Sorts of (TermAlg F1()) . F4() is non empty set
FreeMSA ( the carrier of F1() --> NAT) is non-empty V126(F1()) MSAlgebra over F1()
the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
F3() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2()
(F1(),( the carrier of F1() --> NAT),F2(),F3()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F1() --> NAT)), the Sorts of F2()
(F1(),( the carrier of F1() --> NAT),F2(),F3()) . F4() is Relation-like the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . F4() -defined the Sorts of F2() . F4() -valued Function-like non empty V14( the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . F4()) V18( the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . F4(), the Sorts of F2() . F4()) Element of bool [:( the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . F4()),( the Sorts of F2() . F4()):]
the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . F4() is non empty set
the Sorts of F2() . F4() is non empty set
[:( the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . F4()),( the Sorts of F2() . F4()):] is set
bool [:( the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . F4()),( the Sorts of F2() . F4()):] is set
F5() is Element of the Sorts of (TermAlg F1()) . F4()
((F1(),( the carrier of F1() --> NAT),F2(),F3()) . F4()) . F5() is set
F6() is Element of the Sorts of (TermAlg F1()) . F4()
((F1(),( the carrier of F1() --> NAT),F2(),F3()) . F4()) . F6() is set
F5() '=' F6() is V15() Element of (Equations F1()) . F4()
Equations F1() is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
[| the Sorts of (TermAlg F1()), the Sorts of (TermAlg F1())|] is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
(Equations F1()) . F4() is non empty set
{F5(),F6()} is non empty set
{F5()} is non empty set
{{F5(),F6()},{F5()}} is non empty set
E is non-empty MSAlgebra over F1()
the Sorts of E is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
E is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (TermAlg F1()), the Sorts of E
E . F4() is Relation-like the Sorts of (TermAlg F1()) . F4() -defined the Sorts of E . F4() -valued Function-like non empty V14( the Sorts of (TermAlg F1()) . F4()) V18( the Sorts of (TermAlg F1()) . F4(), the Sorts of E . F4()) Element of bool [:( the Sorts of (TermAlg F1()) . F4()),( the Sorts of E . F4()):]
the Sorts of E . F4() is non empty set
[:( the Sorts of (TermAlg F1()) . F4()),( the Sorts of E . F4()):] is set
bool [:( the Sorts of (TermAlg F1()) . F4()),( the Sorts of E . F4()):] is set
(F5() '=' F6()) `1 is set
(E . F4()) . ((F5() '=' F6()) `1) is set
(F5() '=' F6()) `2 is set
(E . F4()) . ((F5() '=' F6()) `2) is set
I is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
FreeMSA I is non-empty V126(F1()) MSAlgebra over F1()
the Sorts of () is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
FreeGen I is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) V125(F1(), FreeMSA I) GeneratorSet of FreeMSA I
Reverse I is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I,I
() "" is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of I, FreeGen I
K is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (), the Sorts of E
K || () is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E
(K || ()) ** (() "") is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of I, the Sorts of E
(F1(),I,E,((K || ()) ** (() ""))) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (), the Sorts of E
XX is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2()
B is non-empty MSAlgebra over F1()
the Sorts of B is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
e is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F1() --> NAT, the Sorts of B
A is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F1() --> NAT, the Sorts of E
(F1(),( the carrier of F1() --> NAT),E,A) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F1() --> NAT)), the Sorts of E
(F1(),( the carrier of F1() --> NAT),F2(),XX) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F1() --> NAT)), the Sorts of F2()
B is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F2(), the Sorts of E
B ** (F1(),( the carrier of F1() --> NAT),F2(),XX) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F1() --> NAT)), the Sorts of E
(F1(),I,E,((K || ()) ** (() ""))) . F4() is Relation-like the Sorts of () . F4() -defined the Sorts of E . F4() -valued Function-like non empty V14( the Sorts of () . F4()) V18( the Sorts of () . F4(), the Sorts of E . F4()) Element of bool [:( the Sorts of () . F4()),( the Sorts of E . F4()):]
the Sorts of () . F4() is non empty set
[:( the Sorts of () . F4()),( the Sorts of E . F4()):] is set
bool [:( the Sorts of () . F4()),( the Sorts of E . F4()):] is set
((F1(),I,E,((K || ()) ** (() ""))) . F4()) . F5() is set
B . F4() is Relation-like the Sorts of F2() . F4() -defined the Sorts of E . F4() -valued Function-like non empty V14( the Sorts of F2() . F4()) V18( the Sorts of F2() . F4(), the Sorts of E . F4()) Element of bool [:( the Sorts of F2() . F4()),( the Sorts of E . F4()):]
[:( the Sorts of F2() . F4()),( the Sorts of E . F4()):] is set
bool [:( the Sorts of F2() . F4()),( the Sorts of E . F4()):] is set
(B . F4()) * ((F1(),( the carrier of F1() --> NAT),F2(),F3()) . F4()) is Relation-like the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . F4() -defined the Sorts of E . F4() -valued Function-like non empty V14( the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . F4()) V18( the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . F4(), the Sorts of E . F4()) Element of bool [:( the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . F4()),( the Sorts of E . F4()):]
[:( the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . F4()),( the Sorts of E . F4()):] is set
bool [:( the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . F4()),( the Sorts of E . F4()):] is set
((B . F4()) * ((F1(),( the carrier of F1() --> NAT),F2(),F3()) . F4())) . F5() is set
(B . F4()) . (((F1(),( the carrier of F1() --> NAT),F2(),F3()) . F4()) . F6()) is set
((B . F4()) * ((F1(),( the carrier of F1() --> NAT),F2(),F3()) . F4())) . F6() is set
((F1(),I,E,((K || ()) ** (() ""))) . F4()) . F6() is set
rngs () is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
(F1(),I,E,((K || ()) ** (() ""))) || () is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E
((K || ()) ** (() "")) ** () is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E
(() "") ** () is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, FreeGen I
(K || ()) ** ((() "") ** ()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E

(K || ()) ** (id ()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E
[F5(),F6()] is V15() set
[F5(),F6()] `1 is set
(E . F4()) . ([F5(),F6()] `1) is set
(E . F4()) . F5() is Element of the Sorts of E . F4()
[F5(),F6()] `2 is set
(E . F4()) . ([F5(),F6()] `2) is set
F1() is non empty non void V62() ManySortedSign
the carrier of F1() is non empty set
F2() is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
F3() is strict non-empty MSAlgebra over F1()
the Sorts of F3() is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
F4() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), the Sorts of F3()
F4() .:.: F2() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
I is set
(F4() .:.: F2()) . I is set
F2() . I is set
the Sorts of F3() . I is set
[:(F2() . I),( the Sorts of F3() . I):] is set
bool [:(F2() . I),( the Sorts of F3() . I):] is set

E is Relation-like F2() . I -defined the Sorts of F3() . I -valued Function-like V18(F2() . I, the Sorts of F3() . I) Element of bool [:(F2() . I),( the Sorts of F3() . I):]
E .: (F2() . I) is Element of bool ( the Sorts of F3() . I)
bool ( the Sorts of F3() . I) is set
E is non empty set
dom E is Element of bool (F2() . I)
bool (F2() . I) is set
I is set
(F4() .:.: F2()) . I is set
the Sorts of F3() . I is set
F2() . I is set
[:(F2() . I),( the Sorts of F3() . I):] is set
bool [:(F2() . I),( the Sorts of F3() . I):] is set

E is Relation-like F2() . I -defined the Sorts of F3() . I -valued Function-like V18(F2() . I, the Sorts of F3() . I) Element of bool [:(F2() . I),( the Sorts of F3() . I):]
E .: (F2() . I) is Element of bool ( the Sorts of F3() . I)
bool ( the Sorts of F3() . I) is set
I is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) ManySortedSubset of the Sorts of F3()
GenMSAlg I is strict non-empty MSSubAlgebra of F3()
the Sorts of () is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
E is set
the Sorts of () . E is set
F2() . E is set
E is set
the Sorts of F3() . E is set
F2() . E is set
doms F4() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
rngs F4() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
E is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), the Sorts of ()
K is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F3(), the Sorts of ()
K ** F4() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), the Sorts of ()
id the Sorts of () is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding "1-1" "onto" ManySortedFunction of the Sorts of (), the Sorts of ()
F is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (), the Sorts of F3()
F ** E is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), the Sorts of F3()
A is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F3(), the Sorts of F3()
A ** F4() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), the Sorts of F3()
F ** K is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F3(), the Sorts of F3()
(F ** K) ** F4() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), the Sorts of F3()
B is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F3(), the Sorts of F3()
id the Sorts of F3() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding "1-1" "onto" ManySortedFunction of the Sorts of F3(), the Sorts of F3()
(id the Sorts of F3()) ** F4() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of F2(), the Sorts of F3()
F .:.: the Sorts of () is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
F1() is non empty non void V62() ManySortedSign
the carrier of F1() is non empty set
the carrier of F1() --> NAT is Relation-like non-empty non empty-yielding the carrier of F1() -defined -valued Function-like constant non empty V14( the carrier of F1()) V18( the carrier of F1(),) Element of bool [: the carrier of F1(),:]
is non empty set
[: the carrier of F1(),:] is set
bool [: the carrier of F1(),:] is set
F2() is strict non-empty MSAlgebra over F1()
the Sorts of F2() is Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) set
F3() is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2()
FreeMSA ( the carrier of F1() --> NAT) is non-empty V126(F1()) MSAlgebra over F1()
(F1(),( the carrier of F1() --> NAT),F2(),F3()) is Relation-like the carrier of F1() -defined Function-like non empty V14( the carrier of F1()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F1() --> NAT)), the Sorts of F2()
the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) is Relation-like non-empty non empty-yielding the carrier of F1() -defined