:: BIRKHOFF semantic presentation

NAT is non empty V34() V35() V36() Element of bool REAL
REAL is set
bool REAL is set
NAT is non empty V34() V35() V36() set
bool NAT is set
bool NAT is 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
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] 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
product {} 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 (FreeMSA I) 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
Reverse I 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,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 ** (Reverse I) 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 (FreeMSA I), the Sorts of E
K || (FreeGen I) 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 (FreeMSA I), the Sorts of E
F || (FreeGen I) 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 (FreeMSA E), the Sorts of I
FreeMSA E is non-empty V126(XX) MSAlgebra over XX
the Sorts of (FreeMSA E) 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
Reverse 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,E
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
(FreeGen E) . A is non empty set
(Reverse E) . A is Relation-like (FreeGen E) . A -defined E . A -valued Function-like non empty V14((FreeGen E) . A) V18((FreeGen E) . A,E . A) Element of bool [:((FreeGen E) . A),(E . A):]
E . A is non empty set
[:((FreeGen E) . A),(E . A):] is set
bool [:((FreeGen E) . A),(E . A):] is set
dom ((Reverse E) . A) is Element of bool ((FreeGen E) . A)
bool ((FreeGen E) . A) is set
the Sorts of (FreeMSA E) . 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 (Reverse E) is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) set
rng ((Reverse E) . A) is non empty Element of bool (E . A)
x is set
((Reverse E) . A) . x is set
(XX,E,I,E) . A is Relation-like the Sorts of (FreeMSA E) . A -defined the Sorts of I . A -valued Function-like non empty V14( the Sorts of (FreeMSA E) . A) V18( the Sorts of (FreeMSA E) . A, the Sorts of I . A) Element of bool [:( the Sorts of (FreeMSA E) . A),( the Sorts of I . A):]
[:( the Sorts of (FreeMSA E) . A),( the Sorts of I . A):] is set
bool [:( the Sorts of (FreeMSA E) . A),( the Sorts of I . A):] is set
dom ((XX,E,I,E) . A) is Element of bool ( the Sorts of (FreeMSA E) . A)
bool ( the Sorts of (FreeMSA E) . A) is set
(E . A) * ((Reverse E) . A) is Relation-like (FreeGen E) . A -defined the Sorts of I . A -valued Function-like non empty V14((FreeGen E) . A) V18((FreeGen E) . A, the Sorts of I . A) Element of bool [:((FreeGen E) . A),( the Sorts of I . A):]
[:((FreeGen E) . A),( the Sorts of I . A):] is set
bool [:((FreeGen E) . A),( the Sorts of I . A):] is set
((E . A) * ((Reverse E) . A)) . x is set
E ** (Reverse 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 ** (Reverse E)) . A is Relation-like (FreeGen E) . A -defined the Sorts of I . A -valued Function-like non empty V14((FreeGen E) . A) V18((FreeGen E) . A, the Sorts of I . A) Element of bool [:((FreeGen E) . A),( the Sorts of I . A):]
((E ** (Reverse E)) . A) . x is set
(XX,E,I,E) || (FreeGen 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) || (FreeGen E)) . A is Relation-like (FreeGen E) . A -defined the Sorts of I . A -valued Function-like non empty V14((FreeGen E) . A) V18((FreeGen E) . A, the Sorts of I . A) Element of bool [:((FreeGen E) . A),( the Sorts of I . A):]
(((XX,E,I,E) || (FreeGen E)) . A) . x is set
((XX,E,I,E) . A) | ((FreeGen E) . A) is Relation-like the Sorts of (FreeMSA E) . A -defined the Sorts of I . A -valued Function-like Element of bool [:( the Sorts of (FreeMSA E) . A),( the Sorts of I . A):]
(((XX,E,I,E) . A) | ((FreeGen E) . 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)
F₁() is non empty non void V62() ManySortedSign
the carrier of F₁() is non empty set
F₂() is non-empty MSAlgebra over F₁()
the Sorts of F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁() is Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁()
CongrLatt F₂() is non empty V73() V80() V85() M30( EqRelLatt the Sorts of F₂())
EqRelLatt the Sorts of F₂() is non empty V73() V80() L9()
the carrier of (CongrLatt F₂()) is non empty set
{ b₁ where b₁ is Element of the carrier of (CongrLatt F₂()) : ex b₂ being Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂() st
( b₂ = b₁ & P₁[ QuotMSAlg (F₂(),b₂)] ) } is set
the carrier of F₁() --> {{}} is Relation-like non-empty non empty-yielding the carrier of F₁() -defined {{{}}} -valued Function-like constant non empty V14( the carrier of F₁()) V18( the carrier of F₁(),{{{}}}) Element of bool [: the carrier of F₁(),{{{}}}:]
{{{}}} is non empty set
[: the carrier of F₁(),{{{}}}:] is set
bool [: the carrier of F₁(),{{{}}}:] is set
K is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
{K} is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F is set
product the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁() is non-empty MSAlgebra over F₁()
SORTS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
OPS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁() is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(SORTS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁())), the ResultSort of F₁() * (SORTS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁())
the carrier' of F₁() is non empty set
the Arity of F₁() is Relation-like the carrier' of F₁() -defined K171( the carrier of F₁()) -valued Function-like V18( the carrier' of F₁(),K171( the carrier of F₁())) Element of bool [: the carrier' of F₁(),K171( the carrier of F₁()):]
K171( the carrier of F₁()) is M11( the carrier of F₁())
[: the carrier' of F₁(),K171( the carrier of F₁()):] is set
bool [: the carrier' of F₁(),K171( the carrier of F₁()):] is set
K174( the carrier of F₁(),(SORTS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁())) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(SORTS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁())) is Relation-like set
the ResultSort of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() -valued Function-like non empty V14( the carrier' of F₁()) V18( the carrier' of F₁(), the carrier of F₁()) Element of bool [: the carrier' of F₁(), the carrier of F₁():]
[: the carrier' of F₁(), the carrier of F₁():] is set
bool [: the carrier' of F₁(), the carrier of F₁():] is set
the ResultSort of F₁() * (SORTS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁()) is Relation-like set
MSAlgebra(# (SORTS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁()),(OPS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁()) #) is strict MSAlgebra over F₁()
the Sorts of (product the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁()) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
the Sorts of (product the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁()) . F is set
A is Element of the carrier of F₁()
Carrier ( the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁(),A) is Relation-like {} -defined Function-like V14( {} ) set
product (Carrier ( the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁(),A)) is set
( the carrier of F₁() --> {{}}) . A is non empty Element of {{{}}}
{K} . F is set
[| the Sorts of F₂(), the Sorts of F₂()|] is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
QuotMSAlg (F₂(),F) is strict non-empty MSAlgebra over F₁()
Class F is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact F is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class F)), the ResultSort of F₁() * (Class F)
K174( the carrier of F₁(),(Class F)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class F)) is Relation-like set
the ResultSort of F₁() * (Class F) is Relation-like set
MSAlgebra(# (Class F),(QuotCharact F) #) is strict MSAlgebra over F₁()
the Sorts of (QuotMSAlg (F₂(),F)) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
{ the Sorts of F₂()} is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
Trivial_Algebra F₁() is strict non-empty finitely-generated finite-yielding MSAlgebra over F₁()
A is set
the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F₁() . A is set
A is set
B is Element of the carrier of (CongrLatt F₂())
e is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
QuotMSAlg (F₂(),e) is strict non-empty MSAlgebra over F₁()
Class e is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact e is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class e)), the ResultSort of F₁() * (Class e)
K174( the carrier of F₁(),(Class e)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class e)) is Relation-like set
the ResultSort of F₁() * (Class e) is Relation-like set
MSAlgebra(# (Class e),(QuotCharact e) #) is strict MSAlgebra over F₁()
the carrier of (EqRelLatt the Sorts of F₂()) is non empty set
A is set
Bool [| the Sorts of F₂(), the Sorts of F₂()|] is functional non empty with_common_domain set
bool (Bool [| the Sorts of F₂(), the Sorts of F₂()|]) is set
A is non empty Element of bool (Bool [| the Sorts of F₂(), the Sorts of F₂()|])
|:A:| is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) ManySortedSubset of K109( the carrier of F₁(),[| the Sorts of F₂(), the Sorts of F₂()|])
K109( the carrier of F₁(),[| the Sorts of F₂(), the Sorts of F₂()|]) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
meet |:A:| is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) ManySortedSubset of [| the Sorts of F₂(), the Sorts of F₂()|]
e is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
x is set
the Sorts of F₂() . x is set
[:( the Sorts of F₂() . x),( the Sorts of F₂() . x):] is set
bool [:( the Sorts of F₂() . x),( the Sorts of F₂() . x):] is set
e . x is set
h is Relation-like the Sorts of F₂() . x -defined the Sorts of F₂() . x -valued Element of bool [:( the Sorts of F₂() . x),( the Sorts of F₂() . x):]
{ b₁ where b₁ is Element of the carrier of (CongrLatt F₂()) : S₂[b₁] } is set
bool the carrier of (CongrLatt F₂()) is set
x is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
h is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
QuotMSAlg (F₂(),h) is strict non-empty MSAlgebra over F₁()
Class h is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact h is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class h)), the ResultSort of F₁() * (Class h)
K174( the carrier of F₁(),(Class h)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class h)) is Relation-like set
the ResultSort of F₁() * (Class h) is Relation-like set
MSAlgebra(# (Class h),(QuotCharact h) #) is strict MSAlgebra over F₁()
t2 is strict non-empty MSAlgebra over F₁()
the Sorts of t2 is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
MSNat_Hom (F₂(),h) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of (QuotMSAlg (F₂(),h))
the Sorts of (QuotMSAlg (F₂(),h)) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
e is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of t2
fi is set
x is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
QuotMSAlg (F₂(),x) is strict non-empty MSAlgebra over F₁()
Class x is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact x is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class x)), the ResultSort of F₁() * (Class x)
K174( the carrier of F₁(),(Class x)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class x)) is Relation-like set
the ResultSort of F₁() * (Class x) is Relation-like set
MSAlgebra(# (Class x),(QuotCharact x) #) is strict MSAlgebra over F₁()
FofI1 is set
FofI1 is set
fi is Relation-like A -defined Function-like non empty V14(A) set
x is set
fi . x is set
FofI1 is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
QuotMSAlg (F₂(),FofI1) is strict non-empty MSAlgebra over F₁()
Class FofI1 is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact FofI1 is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class FofI1)), the ResultSort of F₁() * (Class FofI1)
K174( the carrier of F₁(),(Class FofI1)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class FofI1)) is Relation-like set
the ResultSort of F₁() * (Class FofI1) is Relation-like set
MSAlgebra(# (Class FofI1),(QuotCharact FofI1) #) is strict MSAlgebra over F₁()
x is Relation-like A -defined Function-like non empty V14(A) MSAlgebra-Family of A,F₁()
FofI1 is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Element of A
x . FofI1 is non-empty MSAlgebra over F₁()
the Sorts of (x . FofI1) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
FofI1 is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
QuotMSAlg (F₂(),FofI1) is strict non-empty MSAlgebra over F₁()
Class FofI1 is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact FofI1 is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class FofI1)), the ResultSort of F₁() * (Class FofI1)
K174( the carrier of F₁(),(Class FofI1)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class FofI1)) is Relation-like set
the ResultSort of F₁() * (Class FofI1) is Relation-like set
MSAlgebra(# (Class FofI1),(QuotCharact FofI1) #) is strict MSAlgebra over F₁()
MSNat_Hom (F₂(),FofI1) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of (QuotMSAlg (F₂(),FofI1))
the Sorts of (QuotMSAlg (F₂(),FofI1)) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
XX is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), 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 F₁() -defined Function-like non empty V14( the carrier of F₁()) Element of A
x . FofI1 is non-empty MSAlgebra over F₁()
the Sorts of (x . FofI1) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
FofI1 . FofI1 is set
H is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), 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 F₁() -defined Function-like non empty V14( the carrier of F₁()) Element of A
x . H is non-empty MSAlgebra over F₁()
the Sorts of (x . H) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
FofI1 . H is set
XX is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of (x . H)
product x is non-empty MSAlgebra over F₁()
SORTS x is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
OPS x is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(SORTS x)), the ResultSort of F₁() * (SORTS x)
K174( the carrier of F₁(),(SORTS x)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(SORTS x)) is Relation-like set
the ResultSort of F₁() * (SORTS x) is Relation-like set
MSAlgebra(# (SORTS x),(OPS x) #) is strict MSAlgebra over F₁()
the Sorts of (product x) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
FofI1 is Relation-like A -defined Function-like non empty V14(A) Function-yielding Relation-yielding set
H is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of (product x)
XX is set
B is Element of the carrier of F₁()
[| the Sorts of F₂(), the Sorts of F₂()|] . B is set
bool ([| the Sorts of F₂(), the Sorts of F₂()|] . B) is set
bool (bool ([| the Sorts of F₂(), the Sorts of F₂()|] . B)) is set
|:A:| . B is non empty Element of bool (bool ([| the Sorts of F₂(), the Sorts of F₂()|] . B))
(meet |:A:|) . B is set
G is Element of bool (bool ([| the Sorts of F₂(), the Sorts of F₂()|] . B))
Intersect G is Element of bool ([| the Sorts of F₂(), the Sorts of F₂()|] . B)
Bool [| the Sorts of F₂(), the Sorts of F₂()|] is functional non empty with_common_domain V143( the carrier of F₁(),[| the Sorts of F₂(), the Sorts of F₂()|]) V144( the carrier of F₁(),[| the Sorts of F₂(), the Sorts of F₂()|]) V145( the carrier of F₁(),[| the Sorts of F₂(), the Sorts of F₂()|]) V146( the carrier of F₁(),[| the Sorts of F₂(), the Sorts of F₂()|]) V147( the carrier of F₁(),[| the Sorts of F₂(), the Sorts of F₂()|]) V148( the carrier of F₁(),[| the Sorts of F₂(), the Sorts of F₂()|]) Element of bool (Bool [| the Sorts of F₂(), the Sorts of F₂()|])
{ (b₁ . B) where b₁ is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Element of Bool [| the Sorts of F₂(), the Sorts of F₂()|] : b₁ in A } is set
the Sorts of F₂() . B is non empty set
MSCng H is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
(MSCng H) . B is Relation-like the Sorts of F₂() . B -defined the Sorts of F₂() . B -valued V14( the Sorts of F₂() . B) V18( the Sorts of F₂() . B, the Sorts of F₂() . B) V134() V139() Element of bool [:( the Sorts of F₂() . B),( the Sorts of F₂() . B):]
[:( the Sorts of F₂() . B),( the Sorts of F₂() . B):] is set
bool [:( the Sorts of F₂() . B),( the Sorts of F₂() . B):] is set
h . B is Relation-like the Sorts of F₂() . B -defined the Sorts of F₂() . B -valued V14( the Sorts of F₂() . B) V18( the Sorts of F₂() . B, the Sorts of F₂() . B) V134() V139() Element of bool [:( the Sorts of F₂() . B),( the Sorts of F₂() . 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 F₂() . B -defined the Sorts of F₂() . B -valued V14( the Sorts of F₂() . B) V18( the Sorts of F₂() . B, the Sorts of F₂() . B) V134() V139() Element of bool [:( the Sorts of F₂() . B),( the Sorts of F₂() . B):]
K is set
t1 is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Element of Bool [| the Sorts of F₂(), the Sorts of F₂()|]
t1 . B is set
F1 is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Element of A
x . F1 is non-empty MSAlgebra over F₁()
the Sorts of (x . F1) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
FofI1 . F1 is Relation-like Function-like set
F1 is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of (x . F1)
F1 . B is Relation-like the Sorts of F₂() . B -defined the Sorts of (x . F1) . B -valued Function-like non empty V14( the Sorts of F₂() . B) V18( the Sorts of F₂() . B, the Sorts of (x . F1) . B) Element of bool [:( the Sorts of F₂() . B),( the Sorts of (x . F1) . B):]
the Sorts of (x . F1) . B is non empty set
[:( the Sorts of F₂() . B),( the Sorts of (x . F1) . B):] is set
bool [:( the Sorts of F₂() . B),( the Sorts of (x . F1) . B):] is set
(F1 . B) . C is set
proj (x,F1) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (product x), the Sorts of (x . F1)
(proj (x,F1)) ** H is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of (x . F1)
((proj (x,F1)) ** H) . B is Relation-like the Sorts of F₂() . B -defined the Sorts of (x . F1) . B -valued Function-like non empty V14( the Sorts of F₂() . B) V18( the Sorts of F₂() . B, the Sorts of (x . F1) . B) Element of bool [:( the Sorts of F₂() . B),( the Sorts of (x . F1) . B):]
(((proj (x,F1)) ** H) . B) . C is set
the Sorts of (product x) . B is non empty set
H . B is Relation-like the Sorts of F₂() . B -defined the Sorts of (product x) . B -valued Function-like non empty V14( the Sorts of F₂() . B) V18( the Sorts of F₂() . B, the Sorts of (product x) . B) Element of bool [:( the Sorts of F₂() . B),( the Sorts of (product x) . B):]
[:( the Sorts of F₂() . B),( the Sorts of (product x) . B):] is set
bool [:( the Sorts of F₂() . B),( the Sorts of (product x) . B):] is set
(proj (x,F1)) . B is Relation-like the Sorts of (product x) . B -defined the Sorts of (x . F1) . B -valued Function-like non empty V14( the Sorts of (product x) . B) V18( the Sorts of (product x) . B, the Sorts of (x . F1) . B) Element of bool [:( the Sorts of (product x) . B),( the Sorts of (x . F1) . B):]
[:( the Sorts of (product x) . B),( the Sorts of (x . F1) . B):] is set
bool [:( the Sorts of (product x) . B),( the Sorts of (x . F1) . B):] is set
((proj (x,F1)) . B) * (H . B) is Relation-like the Sorts of F₂() . B -defined the Sorts of (x . F1) . B -valued Function-like non empty V14( the Sorts of F₂() . B) V18( the Sorts of F₂() . B, the Sorts of (x . F1) . B) Element of bool [:( the Sorts of F₂() . 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
c₂₈ is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
MSNat_Hom (F₂(),c₂₈) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of (QuotMSAlg (F₂(),c₂₈))
QuotMSAlg (F₂(),c₂₈) is strict non-empty MSAlgebra over F₁()
Class c₂₈ is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact c₂₈ is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class c₂₈)), the ResultSort of F₁() * (Class c₂₈)
K174( the carrier of F₁(),(Class c₂₈)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class c₂₈)) is Relation-like set
the ResultSort of F₁() * (Class c₂₈) is Relation-like set
MSAlgebra(# (Class c₂₈),(QuotCharact c₂₈) #) is strict MSAlgebra over F₁()
the Sorts of (QuotMSAlg (F₂(),c₂₈)) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
Carrier (x,B) is Relation-like A -defined Function-like non empty V14(A) set
H . B is Relation-like the Sorts of F₂() . B -defined the Sorts of (product x) . B -valued Function-like non empty V14( the Sorts of F₂() . B) V18( the Sorts of F₂() . B, the Sorts of (product x) . B) Element of bool [:( the Sorts of F₂() . B),( the Sorts of (product x) . B):]
the Sorts of (product x) . B is non empty set
[:( the Sorts of F₂() . B),( the Sorts of (product x) . B):] is set
bool [:( the Sorts of F₂() . B),( the Sorts of (product x) . B):] is set
(H . B) . C is set
(H . B) . H is set
K is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) 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 F₁()
the Sorts of (x . K) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
FofI1 . K is Relation-like Function-like set
F1 is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of (x . K)
t1 is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
t1 . B is Relation-like the Sorts of F₂() . B -defined the Sorts of F₂() . B -valued V14( the Sorts of F₂() . B) V18( the Sorts of F₂() . B, the Sorts of F₂() . B) V134() V139() Element of bool [:( the Sorts of F₂() . B),( the Sorts of F₂() . B):]
proj (x,K) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (product x), the Sorts of (x . K)
(proj (x,K)) . B is Relation-like the Sorts of (product x) . B -defined the Sorts of (x . K) . B -valued Function-like non empty V14( the Sorts of (product x) . B) V18( the Sorts of (product x) . B, the Sorts of (x . K) . B) Element of bool [:( the Sorts of (product x) . B),( the Sorts of (x . K) . B):]
the Sorts of (x . K) . B is non empty set
[:( the Sorts of (product x) . B),( the Sorts of (x . K) . B):] is set
bool [:( the Sorts of (product x) . 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 F₂() . B -defined the Sorts of (x . K) . B -valued Function-like non empty V14( the Sorts of F₂() . B) V18( the Sorts of F₂() . B, the Sorts of (x . K) . B) Element of bool [:( the Sorts of F₂() . B),( the Sorts of (x . K) . B):]
[:( the Sorts of F₂() . B),( the Sorts of (x . K) . B):] is set
bool [:( the Sorts of F₂() . 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 F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of (x . K)
((proj (x,K)) ** H) . B is Relation-like the Sorts of F₂() . B -defined the Sorts of (x . K) . B -valued Function-like non empty V14( the Sorts of F₂() . B) V18( the Sorts of F₂() . B, the Sorts of (x . K) . B) Element of bool [:( the Sorts of F₂() . B),( the Sorts of (x . K) . B):]
(((proj (x,K)) ** H) . B) . C is set
F1 . B is Relation-like the Sorts of F₂() . B -defined the Sorts of (x . K) . B -valued Function-like non empty V14( the Sorts of F₂() . B) V18( the Sorts of F₂() . B, the Sorts of (x . K) . B) Element of bool [:( the Sorts of F₂() . 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 F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
MSNat_Hom (F₂(),F1) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of (QuotMSAlg (F₂(),F1))
QuotMSAlg (F₂(),F1) is strict non-empty MSAlgebra over F₁()
Class F1 is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact F1 is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class F1)), the ResultSort of F₁() * (Class F1)
K174( the carrier of F₁(),(Class F1)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class F1)) is Relation-like set
the ResultSort of F₁() * (Class F1) is Relation-like set
MSAlgebra(# (Class F1),(QuotCharact F1) #) is strict MSAlgebra over F₁()
the Sorts of (QuotMSAlg (F₂(),F1)) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
product (Carrier (x,B)) is set
(MSCng H) . XX is set
h . XX is set
QuotMSAlg (F₂(),(MSCng H)) is strict non-empty MSAlgebra over F₁()
Class (MSCng H) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact (MSCng H) is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class (MSCng H))), the ResultSort of F₁() * (Class (MSCng H))
K174( the carrier of F₁(),(Class (MSCng H))) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class (MSCng H))) is Relation-like set
the ResultSort of F₁() * (Class (MSCng H)) is Relation-like set
MSAlgebra(# (Class (MSCng H)),(QuotCharact (MSCng H)) #) is strict MSAlgebra over F₁()
MSHomQuot H is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (QuotMSAlg (F₂(),(MSCng H))), the Sorts of (product x)
the Sorts of (QuotMSAlg (F₂(),(MSCng H))) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
Image (MSHomQuot H) is strict non-empty MSSubAlgebra of product x
XX is strict non-empty MSSubAlgebra of product x
B is set
x . B is set
G is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Element of A
x . G is non-empty MSAlgebra over F₁()
C is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
QuotMSAlg (F₂(),C) is strict non-empty MSAlgebra over F₁()
Class C is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact C is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class C)), the ResultSort of F₁() * (Class C)
K174( the carrier of F₁(),(Class C)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class C)) is Relation-like set
the ResultSort of F₁() * (Class C) is Relation-like set
MSAlgebra(# (Class C),(QuotCharact C) #) is strict MSAlgebra over F₁()
H is Element of the carrier of (CongrLatt F₂())
K is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
QuotMSAlg (F₂(),K) is strict non-empty MSAlgebra over F₁()
Class K is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact K is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class K)), the ResultSort of F₁() * (Class K)
K174( the carrier of F₁(),(Class K)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class K)) is Relation-like set
the ResultSort of F₁() * (Class K) is Relation-like set
MSAlgebra(# (Class K),(QuotCharact K) #) is strict MSAlgebra over F₁()
B is non-empty MSAlgebra over F₁()
the Sorts of B is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
G is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of B
MSCng G is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
QuotMSAlg (F₂(),(MSCng G)) is strict non-empty MSAlgebra over F₁()
Class (MSCng G) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact (MSCng G) is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class (MSCng G))), the ResultSort of F₁() * (Class (MSCng G))
K174( the carrier of F₁(),(Class (MSCng G))) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class (MSCng G))) is Relation-like set
the ResultSort of F₁() * (Class (MSCng G)) is Relation-like set
MSAlgebra(# (Class (MSCng G)),(QuotCharact (MSCng G)) #) is strict MSAlgebra over F₁()
MSHomQuot G is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (QuotMSAlg (F₂(),(MSCng G))), the Sorts of B
the Sorts of (QuotMSAlg (F₂(),(MSCng G))) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
Image (MSHomQuot G) is strict non-empty MSSubAlgebra of B
C is strict non-empty MSSubAlgebra of B
H is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of t2, the Sorts of B
H ** e is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of B
K is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of t2, the Sorts of B
K ** e is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of B
F₁() is non empty non void V62() ManySortedSign
the carrier of F₁() is non empty set
F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
XX is non-empty MSAlgebra over F₁()
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,F₁()
product I is non-empty MSAlgebra over F₁()
SORTS I is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
OPS I is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(SORTS I)), the ResultSort of F₁() * (SORTS I)
the carrier' of F₁() is non empty set
the Arity of F₁() is Relation-like the carrier' of F₁() -defined K171( the carrier of F₁()) -valued Function-like V18( the carrier' of F₁(),K171( the carrier of F₁())) Element of bool [: the carrier' of F₁(),K171( the carrier of F₁()):]
K171( the carrier of F₁()) is M11( the carrier of F₁())
[: the carrier' of F₁(),K171( the carrier of F₁()):] is set
bool [: the carrier' of F₁(),K171( the carrier of F₁()):] is set
K174( the carrier of F₁(),(SORTS I)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(SORTS I)) is Relation-like set
the ResultSort of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() -valued Function-like non empty V14( the carrier' of F₁()) V18( the carrier' of F₁(), the carrier of F₁()) Element of bool [: the carrier' of F₁(), the carrier of F₁():]
[: the carrier' of F₁(), the carrier of F₁():] is set
bool [: the carrier' of F₁(), the carrier of F₁():] is set
the ResultSort of F₁() * (SORTS I) is Relation-like set
MSAlgebra(# (SORTS I),(OPS I) #) is strict MSAlgebra over F₁()
FreeMSA F₂() is non-empty V126(F₁()) MSAlgebra over F₁()
Reverse F₂() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(),F₂()
FreeGen F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) V125(F₁(), FreeMSA F₂()) GeneratorSet of FreeMSA F₂()
I is non-empty MSAlgebra over F₁()
E is non-empty MSAlgebra over F₁()
the Sorts of (FreeMSA F₂()) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
I is strict non-empty MSAlgebra over F₁()
the Sorts of I is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA F₂()), the Sorts of I
(Reverse F₂()) "" is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), FreeGen F₂()
E || (FreeGen F₂()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of I
(E || (FreeGen F₂())) ** ((Reverse F₂()) "") is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), the Sorts of I
E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), the Sorts of I
K is non-empty MSAlgebra over F₁()
the Sorts of K is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), the Sorts of K
F ** (Reverse F₂()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
A is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA F₂()), the Sorts of K
A || (FreeGen F₂()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
B is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of I, the Sorts of K
B ** E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA F₂()), the Sorts of K
B ** E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), the Sorts of K
B ** (E || (FreeGen F₂())) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
rngs (Reverse F₂()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
E ** (Reverse F₂()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of I
((Reverse F₂()) "") ** (Reverse F₂()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), FreeGen F₂()
(E || (FreeGen F₂())) ** (((Reverse F₂()) "") ** (Reverse F₂())) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of I
id (FreeGen F₂()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding "1-1" "onto" ManySortedFunction of FreeGen F₂(), FreeGen F₂()
(E || (FreeGen F₂())) ** (id (FreeGen F₂())) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of I
(B ** E) ** (Reverse F₂()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
e is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of I, the Sorts of K
e ** E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), the Sorts of K
((E || (FreeGen F₂())) ** ((Reverse F₂()) "")) ** (Reverse F₂()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of I
e ** (((E || (FreeGen F₂())) ** ((Reverse F₂()) "")) ** (Reverse F₂())) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
B ** ((E || (FreeGen F₂())) ** ((Reverse F₂()) "")) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), the Sorts of K
(B ** ((E || (FreeGen F₂())) ** ((Reverse F₂()) ""))) ** (Reverse F₂()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
B ** (((E || (FreeGen F₂())) ** ((Reverse F₂()) "")) ** (Reverse F₂())) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
e ** ((E || (FreeGen F₂())) ** (((Reverse F₂()) "") ** (Reverse F₂()))) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
B ** ((E || (FreeGen F₂())) ** (((Reverse F₂()) "") ** (Reverse F₂()))) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
e ** ((E || (FreeGen F₂())) ** (id (FreeGen F₂()))) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
B ** ((E || (FreeGen F₂())) ** (id (FreeGen F₂()))) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
e ** (E || (FreeGen F₂())) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
e ** E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA F₂()), the Sorts of K
(e ** E) || (FreeGen F₂()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
(B ** E) || (FreeGen F₂()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen F₂(), the Sorts of K
F₁() is non empty non void V62() ManySortedSign
the carrier of F₁() is non empty set
the carrier of F₁() --> NAT is Relation-like non-empty non empty-yielding the carrier of F₁() -defined {NAT} -valued Function-like constant non empty V14( the carrier of F₁()) V18( the carrier of F₁(),{NAT}) Element of bool [: the carrier of F₁(),{NAT}:]
{NAT} is non empty set
[: the carrier of F₁(),{NAT}:] is set
bool [: the carrier of F₁(),{NAT}:] is set
F₂() is non-empty MSAlgebra over F₁()
the Sorts of F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F₃() is non-empty MSAlgebra over F₁()
the Sorts of F₃() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F₄() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂()
F₅() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₃()
(F₁(),( the carrier of F₁() --> NAT),F₃(),F₅()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)), the Sorts of F₃()
FreeMSA ( the carrier of F₁() --> NAT) is non-empty V126(F₁()) MSAlgebra over F₁()
the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
(F₁(),( the carrier of F₁() --> NAT),F₂(),F₄()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)), the Sorts of F₂()
XX is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of F₃()
XX ** F₄() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₃()
XX ** (F₁(),( the carrier of F₁() --> NAT),F₂(),F₄()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)), the Sorts of F₃()
I is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
FreeMSA I is non-empty V126(F₁()) MSAlgebra over F₁()
E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of I, the Sorts of F₃()
(F₁(),I,F₃(),E) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA I), the Sorts of F₃()
the Sorts of (FreeMSA I) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
FreeGen I is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) V125(F₁(), FreeMSA I) GeneratorSet of FreeMSA I
(F₁(),I,F₃(),E) || (FreeGen I) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of F₃()
Reverse I is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I,I
F₅() ** (Reverse I) is Relation-like Function-like Function-yielding Relation-yielding set
F₄() ** (Reverse I) is Relation-like Function-like Function-yielding Relation-yielding set
XX ** (F₄() ** (Reverse I)) is Relation-like Function-like Function-yielding Relation-yielding set
FreeGen ( the carrier of F₁() --> NAT) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) V125(F₁(), FreeMSA ( the carrier of F₁() --> NAT)) GeneratorSet of FreeMSA ( the carrier of F₁() --> NAT)
(F₁(),( the carrier of F₁() --> NAT),F₂(),F₄()) || (FreeGen ( the carrier of F₁() --> NAT)) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen ( the carrier of F₁() --> NAT), the Sorts of F₂()
XX ** ((F₁(),( the carrier of F₁() --> NAT),F₂(),F₄()) || (FreeGen ( the carrier of F₁() --> NAT))) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen ( the carrier of F₁() --> NAT), the Sorts of F₃()
(XX ** (F₁(),( the carrier of F₁() --> NAT),F₂(),F₄())) || (FreeGen ( the carrier of F₁() --> NAT)) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen ( the carrier of F₁() --> NAT), the Sorts of F₃()
F₁() is non empty non void V62() ManySortedSign
the carrier of F₁() is non empty set
the carrier of F₁() --> NAT is Relation-like non-empty non empty-yielding the carrier of F₁() -defined {NAT} -valued Function-like constant non empty V14( the carrier of F₁()) V18( the carrier of F₁(),{NAT}) Element of bool [: the carrier of F₁(),{NAT}:]
{NAT} is non empty set
[: the carrier of F₁(),{NAT}:] is set
bool [: the carrier of F₁(),{NAT}:] is set
F₂() is non-empty MSAlgebra over F₁()
the Sorts of F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
TermAlg F₁() is strict non-empty V126(F₁()) MSAlgebra over F₁()
the carrier of F₁() --> NAT is Relation-like non-empty non empty-yielding the carrier of F₁() -defined bool REAL -valued Function-like constant non empty V14( the carrier of F₁()) V18( the carrier of F₁(), bool REAL) Element of bool [: the carrier of F₁(),(bool REAL):]
[: the carrier of F₁(),(bool REAL):] is set
bool [: the carrier of F₁(),(bool REAL):] is set
FreeMSA ( the carrier of F₁() --> NAT) is non-empty V126(F₁()) MSAlgebra over F₁()
the Sorts of (TermAlg F₁()) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F₄() is Element of the carrier of F₁()
the Sorts of (TermAlg F₁()) . F₄() is non empty set
FreeMSA ( the carrier of F₁() --> NAT) is non-empty V126(F₁()) MSAlgebra over F₁()
the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F₃() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂()
(F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)), the Sorts of F₂()
(F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F₄() is Relation-like the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F₄() -defined the Sorts of F₂() . F₄() -valued Function-like non empty V14( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F₄()) V18( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F₄(), the Sorts of F₂() . F₄()) Element of bool [:( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F₄()),( the Sorts of F₂() . F₄()):]
the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F₄() is non empty set
the Sorts of F₂() . F₄() is non empty set
[:( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F₄()),( the Sorts of F₂() . F₄()):] is set
bool [:( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F₄()),( the Sorts of F₂() . F₄()):] is set
F₅() is Element of the Sorts of (TermAlg F₁()) . F₄()
((F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F₄()) . F₅() is set
F₆() is Element of the Sorts of (TermAlg F₁()) . F₄()
((F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F₄()) . F₆() is set
F₅() '=' F₆() is V15() Element of (Equations F₁()) . F₄()
Equations F₁() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
[| the Sorts of (TermAlg F₁()), the Sorts of (TermAlg F₁())|] is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
(Equations F₁()) . F₄() is non empty set
{F₅(),F₆()} is non empty set
{F₅()} is non empty set
{{F₅(),F₆()},{F₅()}} is non empty set
E is non-empty MSAlgebra over F₁()
the Sorts of E is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (TermAlg F₁()), the Sorts of E
E . F₄() is Relation-like the Sorts of (TermAlg F₁()) . F₄() -defined the Sorts of E . F₄() -valued Function-like non empty V14( the Sorts of (TermAlg F₁()) . F₄()) V18( the Sorts of (TermAlg F₁()) . F₄(), the Sorts of E . F₄()) Element of bool [:( the Sorts of (TermAlg F₁()) . F₄()),( the Sorts of E . F₄()):]
the Sorts of E . F₄() is non empty set
[:( the Sorts of (TermAlg F₁()) . F₄()),( the Sorts of E . F₄()):] is set
bool [:( the Sorts of (TermAlg F₁()) . F₄()),( the Sorts of E . F₄()):] is set
(F₅() '=' F₆()) `1 is set
(E . F<sub>4</sub>()) . ((F<sub>5</sub>() '=' F<sub>6</sub>()) `1) is set
(F₅() '=' F₆()) `2 is set
(E . F<sub>4</sub>()) . ((F<sub>5</sub>() '=' F<sub>6</sub>()) `2) is set
I is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
FreeMSA I is non-empty V126(F₁()) MSAlgebra over F₁()
the Sorts of (FreeMSA I) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
FreeGen I is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) V125(F₁(), FreeMSA I) GeneratorSet of FreeMSA I
Reverse I is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I,I
(Reverse I) "" is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of I, FreeGen I
K is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA I), the Sorts of E
K || (FreeGen I) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E
(K || (FreeGen I)) ** ((Reverse I) "") is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of I, the Sorts of E
(F₁(),I,E,((K || (FreeGen I)) ** ((Reverse I) ""))) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA I), the Sorts of E
XX is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂()
B is non-empty MSAlgebra over F₁()
the Sorts of B is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
e is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of B
A is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of E
(F₁(),( the carrier of F₁() --> NAT),E,A) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)), the Sorts of E
(F₁(),( the carrier of F₁() --> NAT),F₂(),XX) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)), the Sorts of F₂()
B is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of E
B ** (F₁(),( the carrier of F₁() --> NAT),F₂(),XX) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)), the Sorts of E
(F₁(),I,E,((K || (FreeGen I)) ** ((Reverse I) ""))) . F₄() is Relation-like the Sorts of (FreeMSA I) . F₄() -defined the Sorts of E . F₄() -valued Function-like non empty V14( the Sorts of (FreeMSA I) . F₄()) V18( the Sorts of (FreeMSA I) . F₄(), the Sorts of E . F₄()) Element of bool [:( the Sorts of (FreeMSA I) . F₄()),( the Sorts of E . F₄()):]
the Sorts of (FreeMSA I) . F₄() is non empty set
[:( the Sorts of (FreeMSA I) . F₄()),( the Sorts of E . F₄()):] is set
bool [:( the Sorts of (FreeMSA I) . F₄()),( the Sorts of E . F₄()):] is set
((F₁(),I,E,((K || (FreeGen I)) ** ((Reverse I) ""))) . F₄()) . F₅() is set
B . F₄() is Relation-like the Sorts of F₂() . F₄() -defined the Sorts of E . F₄() -valued Function-like non empty V14( the Sorts of F₂() . F₄()) V18( the Sorts of F₂() . F₄(), the Sorts of E . F₄()) Element of bool [:( the Sorts of F₂() . F₄()),( the Sorts of E . F₄()):]
[:( the Sorts of F₂() . F₄()),( the Sorts of E . F₄()):] is set
bool [:( the Sorts of F₂() . F₄()),( the Sorts of E . F₄()):] is set
(B . F₄()) * ((F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F₄()) is Relation-like the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F₄() -defined the Sorts of E . F₄() -valued Function-like non empty V14( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F₄()) V18( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F₄(), the Sorts of E . F₄()) Element of bool [:( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F₄()),( the Sorts of E . F₄()):]
[:( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F₄()),( the Sorts of E . F₄()):] is set
bool [:( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F₄()),( the Sorts of E . F₄()):] is set
((B . F₄()) * ((F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F₄())) . F₅() is set
(B . F₄()) . (((F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F₄()) . F₆()) is set
((B . F₄()) * ((F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F₄())) . F₆() is set
((F₁(),I,E,((K || (FreeGen I)) ** ((Reverse I) ""))) . F₄()) . F₆() is set
rngs (Reverse I) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
(F₁(),I,E,((K || (FreeGen I)) ** ((Reverse I) ""))) || (FreeGen I) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E
((K || (FreeGen I)) ** ((Reverse I) "")) ** (Reverse I) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E
((Reverse I) "") ** (Reverse I) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, FreeGen I
(K || (FreeGen I)) ** (((Reverse I) "") ** (Reverse I)) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E
id (FreeGen I) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding "1-1" "onto" ManySortedFunction of FreeGen I, FreeGen I
(K || (FreeGen I)) ** (id (FreeGen I)) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E
[F₅(),F₆()] is V15() set
[F₅(),F₆()] `1 is set
(E . F<sub>4</sub>()) . ([F<sub>5</sub>(),F<sub>6</sub>()] `1) is set
(E . F₄()) . F₅() is Element of the Sorts of E . F₄()
[F₅(),F₆()] `2 is set
(E . F<sub>4</sub>()) . ([F<sub>5</sub>(),F<sub>6</sub>()] `2) is set
F₁() is non empty non void V62() ManySortedSign
the carrier of F₁() is non empty set
F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F₃() is strict non-empty MSAlgebra over F₁()
the Sorts of F₃() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F₄() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), the Sorts of F₃()
F₄() .:.: F₂() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
I is set
(F₄() .:.: F₂()) . I is set
F₂() . I is set
the Sorts of F₃() . I is set
[:(F₂() . I),( the Sorts of F₃() . I):] is set
bool [:(F₂() . I),( the Sorts of F₃() . I):] is set
F₄() . I is Relation-like Function-like set
E is Relation-like F₂() . I -defined the Sorts of F₃() . I -valued Function-like V18(F₂() . I, the Sorts of F₃() . I) Element of bool [:(F₂() . I),( the Sorts of F₃() . I):]
E .: (F₂() . I) is Element of bool ( the Sorts of F₃() . I)
bool ( the Sorts of F₃() . I) is set
E is non empty set
dom E is Element of bool (F₂() . I)
bool (F₂() . I) is set
I is set
(F₄() .:.: F₂()) . I is set
the Sorts of F₃() . I is set
F₂() . I is set
[:(F₂() . I),( the Sorts of F₃() . I):] is set
bool [:(F₂() . I),( the Sorts of F₃() . I):] is set
F₄() . I is Relation-like Function-like set
E is Relation-like F₂() . I -defined the Sorts of F₃() . I -valued Function-like V18(F₂() . I, the Sorts of F₃() . I) Element of bool [:(F₂() . I),( the Sorts of F₃() . I):]
E .: (F₂() . I) is Element of bool ( the Sorts of F₃() . I)
bool ( the Sorts of F₃() . I) is set
I is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) ManySortedSubset of the Sorts of F₃()
GenMSAlg I is strict non-empty MSSubAlgebra of F₃()
the Sorts of (GenMSAlg I) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
E is set
the Sorts of (GenMSAlg I) . E is set
F₂() . E is set
E is set
the Sorts of F₃() . E is set
F₂() . E is set
doms F₄() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
rngs F₄() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), the Sorts of (GenMSAlg I)
K is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₃(), the Sorts of (GenMSAlg I)
K ** F₄() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), the Sorts of (GenMSAlg I)
id the Sorts of (GenMSAlg I) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding "1-1" "onto" ManySortedFunction of the Sorts of (GenMSAlg I), the Sorts of (GenMSAlg I)
F is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (GenMSAlg I), the Sorts of F₃()
F ** E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), the Sorts of F₃()
A is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₃(), the Sorts of F₃()
A ** F₄() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), the Sorts of F₃()
F ** K is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₃(), the Sorts of F₃()
(F ** K) ** F₄() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), the Sorts of F₃()
B is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₃(), the Sorts of F₃()
id the Sorts of F₃() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding "1-1" "onto" ManySortedFunction of the Sorts of F₃(), the Sorts of F₃()
(id the Sorts of F₃()) ** F₄() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of F₂(), the Sorts of F₃()
F .:.: the Sorts of (GenMSAlg I) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F₁() is non empty non void V62() ManySortedSign
the carrier of F₁() is non empty set
the carrier of F₁() --> NAT is Relation-like non-empty non empty-yielding the carrier of F₁() -defined {NAT} -valued Function-like constant non empty V14( the carrier of F₁()) V18( the carrier of F₁(),{NAT}) Element of bool [: the carrier of F₁(),{NAT}:]
{NAT} is non empty set
[: the carrier of F₁(),{NAT}:] is set
bool [: the carrier of F₁(),{NAT}:] is set
F₂() is strict non-empty MSAlgebra over F₁()
the Sorts of F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F₃() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂()
FreeMSA ( the carrier of F₁() --> NAT) is non-empty V126(F₁()) MSAlgebra over F₁()
(F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)), the Sorts of F₂()
the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F₃() .:.: ( the carrier of F₁() --> NAT) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
rngs F₃() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
E is set
the Sorts of F₂() . E is set
the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . E is set
doms (F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
(F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) .:.: the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
rngs (F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
I is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) GeneratorSet of FreeMSA ( the carrier of F₁() --> NAT)
(F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) .:.: I is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
E is non-empty MSAlgebra over F₁()
E is strict non-empty MSSubAlgebra of E
E is non-empty MSAlgebra over F₁()
the Sorts of E is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of E
F₁() is non empty non void V62() ManySortedSign
the carrier of F₁() is non empty set
the carrier of F₁() --> NAT is Relation-like non-empty non empty-yielding the carrier of F₁() -defined {NAT} -valued Function-like constant non empty V14( the carrier of F₁()) V18( the carrier of F₁(),{NAT}) Element of bool [: the carrier of F₁(),{NAT}:]
{NAT} is non empty set
[: the carrier of F₁(),{NAT}:] is set
bool [: the carrier of F₁(),{NAT}:] is set
F₃() is non-empty MSAlgebra over F₁()
the Sorts of F₃() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F₂() is strict non-empty finitely-generated MSAlgebra over F₁()
F₄() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₃()
the Sorts of F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) GeneratorSet of F₂()
E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) finite-yielding ManySortedSubset of the Sorts of F₂()
K is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) finite-yielding ManySortedSubset of the Sorts of F₂()
F is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT,K
A is set
K . A is set
( the carrier of F₁() --> NAT) . A is set
A is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂()
B is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₃(), the Sorts of F₂()
B ** F₄() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂()
Image B is strict non-empty MSSubAlgebra of F₂()
the Sorts of (Image B) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
x is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) ManySortedSubset of the Sorts of F₂()
h is set
K . h is set
x . h is set
e is set
t2 is Element of the carrier of F₁()
( the carrier of F₁() --> NAT) . t2 is non empty Element of {NAT}
the Sorts of F₃() . t2 is non empty set
[:NAT,( the Sorts of F₃() . t2):] is set
bool [:NAT,( the Sorts of F₃() . t2):] is set
F₄() . t2 is Relation-like ( the carrier of F₁() --> NAT) . t2 -defined the Sorts of F₃() . t2 -valued Function-like non empty V14(( the carrier of F₁() --> NAT) . t2) V18(( the carrier of F₁() --> NAT) . t2, the Sorts of F₃() . t2) Element of bool [:(( the carrier of F₁() --> NAT) . t2),( the Sorts of F₃() . t2):]
( the carrier of F₁() --> NAT) . t2 is non empty set
[:(( the carrier of F₁() --> NAT) . t2),( the Sorts of F₃() . t2):] is set
bool [:(( the carrier of F₁() --> NAT) . t2),( the Sorts of F₃() . t2):] is set
the Sorts of F₂() . t2 is non empty set
fi is Relation-like NAT -defined the Sorts of F₃() . t2 -valued Function-like non empty V14( NAT ) V18( NAT , the Sorts of F₃() . t2) Element of bool [:NAT,( the Sorts of F₃() . t2):]
B . t2 is Relation-like the Sorts of F₃() . t2 -defined the Sorts of F₂() . t2 -valued Function-like non empty V14( the Sorts of F₃() . t2) V18( the Sorts of F₃() . t2, the Sorts of F₂() . t2) Element of bool [:( the Sorts of F₃() . t2),( the Sorts of F₂() . t2):]
[:( the Sorts of F₃() . t2),( the Sorts of F₂() . t2):] is set
bool [:( the Sorts of F₃() . t2),( the Sorts of F₂() . t2):] is set
(B . t2) * fi is Relation-like NAT -defined the Sorts of F₂() . t2 -valued Function-like non empty V14( NAT ) V18( NAT , the Sorts of F₂() . t2) Element of bool [:NAT,( the Sorts of F₂() . t2):]
[:NAT,( the Sorts of F₂() . t2):] is set
bool [:NAT,( the Sorts of F₂() . t2):] is set
dom ((B . t2) * fi) is Element of bool NAT
dom fi is Element of bool NAT
rng fi is non empty Element of bool ( the Sorts of F₃() . t2)
bool ( the Sorts of F₃() . t2) is set
dom (B . t2) is Element of bool ( the Sorts of F₃() . t2)
K . t2 is non empty set
F . t2 is Relation-like ( the carrier of F₁() --> NAT) . t2 -defined K . t2 -valued Function-like non empty V14(( the carrier of F₁() --> NAT) . t2) V18(( the carrier of F₁() --> NAT) . t2,K . t2) Element of bool [:(( the carrier of F₁() --> NAT) . t2),(K . t2):]
[:(( the carrier of F₁() --> NAT) . t2),(K . t2):] is set
bool [:(( the carrier of F₁() --> NAT) . t2),(K . t2):] is set
rng (F . t2) is non empty Element of bool (K . t2)
bool (K . t2) is set
dom (F . t2) is Element of bool (( the carrier of F₁() --> NAT) . t2)
bool (( the carrier of F₁() --> NAT) . t2) is set
x is set
(F . t2) . x is set
fi . x is set
((B . t2) * fi) . x is set
(B . t2) . (fi . x) is set
(B . t2) .: ( the Sorts of F₃() . t2) is Element of bool ( the Sorts of F₂() . t2)
bool ( the Sorts of F₂() . t2) is set
B .:.: the Sorts of F₃() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
(B .:.: the Sorts of F₃()) . t2 is set
GenMSAlg K is strict non-empty finitely-generated MSSubAlgebra of F₂()
GenMSAlg x is strict MSSubAlgebra of F₂()
e is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) ManySortedSubset of the Sorts of (Image B)
GenMSAlg e is strict MSSubAlgebra of Image B
MSCng B is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₃(), the Sorts of F₃()
QuotMSAlg (F₃(),(MSCng B)) is strict non-empty MSAlgebra over F₁()
Class (MSCng B) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact (MSCng B) is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class (MSCng B))), the ResultSort of F₁() * (Class (MSCng B))
the carrier' of F₁() is non empty set
the Arity of F₁() is Relation-like the carrier' of F₁() -defined K171( the carrier of F₁()) -valued Function-like V18( the carrier' of F₁(),K171( the carrier of F₁())) Element of bool [: the carrier' of F₁(),K171( the carrier of F₁()):]
K171( the carrier of F₁()) is M11( the carrier of F₁())
[: the carrier' of F₁(),K171( the carrier of F₁()):] is set
bool [: the carrier' of F₁(),K171( the carrier of F₁()):] is set
K174( the carrier of F₁(),(Class (MSCng B))) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class (MSCng B))) is Relation-like set
the ResultSort of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() -valued Function-like non empty V14( the carrier' of F₁()) V18( the carrier' of F₁(), the carrier of F₁()) Element of bool [: the carrier' of F₁(), the carrier of F₁():]
[: the carrier' of F₁(), the carrier of F₁():] is set
bool [: the carrier' of F₁(), the carrier of F₁():] is set
the ResultSort of F₁() * (Class (MSCng B)) is Relation-like set
MSAlgebra(# (Class (MSCng B)),(QuotCharact (MSCng B)) #) is strict MSAlgebra over F₁()
F₁() is non empty non void V62() ManySortedSign
the carrier of F₁() is non empty set
F₂() is non-empty MSAlgebra over F₁()
the Sorts of F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F₃() is non-empty MSAlgebra over F₁()
the Sorts of F₃() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
XX is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of F₃()
XX is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of F₃()
MSCng XX is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of F₂(), the Sorts of F₂()
QuotMSAlg (F₂(),(MSCng XX)) is strict non-empty MSAlgebra over F₁()
Class (MSCng XX) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact (MSCng XX) is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class (MSCng XX))), the ResultSort of F₁() * (Class (MSCng XX))
the carrier' of F₁() is non empty set
the Arity of F₁() is Relation-like the carrier' of F₁() -defined K171( the carrier of F₁()) -valued Function-like V18( the carrier' of F₁(),K171( the carrier of F₁())) Element of bool [: the carrier' of F₁(),K171( the carrier of F₁()):]
K171( the carrier of F₁()) is M11( the carrier of F₁())
[: the carrier' of F₁(),K171( the carrier of F₁()):] is set
bool [: the carrier' of F₁(),K171( the carrier of F₁()):] is set
K174( the carrier of F₁(),(Class (MSCng XX))) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class (MSCng XX))) is Relation-like set
the ResultSort of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() -valued Function-like non empty V14( the carrier' of F₁()) V18( the carrier' of F₁(), the carrier of F₁()) Element of bool [: the carrier' of F₁(), the carrier of F₁():]
[: the carrier' of F₁(), the carrier of F₁():] is set
bool [: the carrier' of F₁(), the carrier of F₁():] is set
the ResultSort of F₁() * (Class (MSCng XX)) is Relation-like set
MSAlgebra(# (Class (MSCng XX)),(QuotCharact (MSCng XX)) #) is strict MSAlgebra over F₁()
F₁() is non empty non void V62() ManySortedSign
F₂() is non-empty MSAlgebra over F₁()
the carrier of F₁() is non empty set
XX is non-empty MSAlgebra over F₁()
I is non-empty MSAlgebra over F₁()
the strict non-empty finitely-generated MSSubAlgebra of F₂() is strict non-empty finitely-generated MSSubAlgebra of F₂()
MSSub F₂() is non empty set
{ b₁ where b₁ is Element of MSSub F₂() : ex b₂ being strict non-empty finitely-generated MSSubAlgebra of F₂() st b₂ = b₁ } is set
E is non empty set
E is set
E is Relation-like E -defined Function-like non empty V14(E) set
K is set
E . K is set
F is Element of MSSub F₂()
A is strict non-empty finitely-generated MSSubAlgebra of F₂()
K is Relation-like E -defined Function-like non empty V14(E) MSAlgebra-Family of E,F₁()
product K is non-empty MSAlgebra over F₁()
SORTS K is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
OPS K is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(SORTS K)), the ResultSort of F₁() * (SORTS K)
the carrier' of F₁() is non empty set
the Arity of F₁() is Relation-like the carrier' of F₁() -defined K171( the carrier of F₁()) -valued Function-like V18( the carrier' of F₁(),K171( the carrier of F₁())) Element of bool [: the carrier' of F₁(),K171( the carrier of F₁()):]
K171( the carrier of F₁()) is M11( the carrier of F₁())
[: the carrier' of F₁(),K171( the carrier of F₁()):] is set
bool [: the carrier' of F₁(),K171( the carrier of F₁()):] is set
K174( the carrier of F₁(),(SORTS K)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(SORTS K)) is Relation-like set
the ResultSort of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() -valued Function-like non empty V14( the carrier' of F₁()) V18( the carrier' of F₁(), the carrier of F₁()) Element of bool [: the carrier' of F₁(), the carrier of F₁():]
[: the carrier' of F₁(), the carrier of F₁():] is set
bool [: the carrier' of F₁(), the carrier of F₁():] is set
the ResultSort of F₁() * (SORTS K) is Relation-like set
MSAlgebra(# (SORTS K),(OPS K) #) is strict MSAlgebra over F₁()
the Sorts of F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F is strict non-empty MSSubAlgebra of product K
the Sorts of F is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
A is non-empty MSAlgebra over F₁()
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
B is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
QuotMSAlg (A,B) is strict non-empty MSAlgebra over F₁()
Class B is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact B is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class B)), the ResultSort of F₁() * (Class B)
K174( the carrier of F₁(),(Class B)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class B)) is Relation-like set
the ResultSort of F₁() * (Class B) is Relation-like set
MSAlgebra(# (Class B),(QuotCharact B) #) is strict MSAlgebra over F₁()
A is set
K . A is set
B is Element of MSSub F₂()
e is strict non-empty finitely-generated MSSubAlgebra of F₂()
e is strict non-empty finitely-generated MSSubAlgebra of F₂()
F₁() is non empty non void V62() ManySortedSign
the carrier of F₁() is non empty set
Equations F₁() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
TermAlg F₁() is strict non-empty V126(F₁()) MSAlgebra over F₁()
the carrier of F₁() --> NAT is Relation-like non-empty non empty-yielding the carrier of F₁() -defined bool REAL -valued Function-like constant non empty V14( the carrier of F₁()) V18( the carrier of F₁(), bool REAL) Element of bool [: the carrier of F₁(),(bool REAL):]
[: the carrier of F₁(),(bool REAL):] is set
bool [: the carrier of F₁(),(bool REAL):] is set
{NAT} is non empty set
[: the carrier of F₁(),{NAT}:] is set
FreeMSA ( the carrier of F₁() --> NAT) is non-empty V126(F₁()) MSAlgebra over F₁()
the Sorts of (TermAlg F₁()) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
[| the Sorts of (TermAlg F₁()), the Sorts of (TermAlg F₁())|] is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F₂() is non-empty MSAlgebra over F₁()
XX is Element of the carrier of F₁()
(Equations F₁()) . XX is non empty set
I is Element of (Equations F₁()) . XX
F₁() is non empty non void V62() ManySortedSign
the carrier of F₁() is non empty set
the carrier of F₁() --> NAT is Relation-like non-empty non empty-yielding the carrier of F₁() -defined {NAT} -valued Function-like constant non empty V14( the carrier of F₁()) V18( the carrier of F₁(),{NAT}) Element of bool [: the carrier of F₁(),{NAT}:]
{NAT} is non empty set
[: the carrier of F₁(),{NAT}:] is set
bool [: the carrier of F₁(),{NAT}:] is set
F₂() is strict non-empty MSAlgebra over F₁()
the Sorts of F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
Equations F₁() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
TermAlg F₁() is strict non-empty V126(F₁()) MSAlgebra over F₁()
the carrier of F₁() --> NAT is Relation-like non-empty non empty-yielding the carrier of F₁() -defined bool REAL -valued Function-like constant non empty V14( the carrier of F₁()) V18( the carrier of F₁(), bool REAL) Element of bool [: the carrier of F₁(),(bool REAL):]
[: the carrier of F₁(),(bool REAL):] is set
bool [: the carrier of F₁(),(bool REAL):] is set
FreeMSA ( the carrier of F₁() --> NAT) is non-empty V126(F₁()) MSAlgebra over F₁()
the Sorts of (TermAlg F₁()) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
[| the Sorts of (TermAlg F₁()), the Sorts of (TermAlg F₁())|] is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F₃() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂()
XX is set
I is Relation-like XX -defined Function-like V14(XX) MSAlgebra-Family of XX,F₁()
product I is non-empty MSAlgebra over F₁()
SORTS I is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
OPS I is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(SORTS I)), the ResultSort of F₁() * (SORTS I)
the carrier' of F₁() is non empty set
the Arity of F₁() is Relation-like the carrier' of F₁() -defined K171( the carrier of F₁()) -valued Function-like V18( the carrier' of F₁(),K171( the carrier of F₁())) Element of bool [: the carrier' of F₁(),K171( the carrier of F₁()):]
K171( the carrier of F₁()) is M11( the carrier of F₁())
[: the carrier' of F₁(),K171( the carrier of F₁()):] is set
bool [: the carrier' of F₁(),K171( the carrier of F₁()):] is set
K174( the carrier of F₁(),(SORTS I)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(SORTS I)) is Relation-like set
the ResultSort of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() -valued Function-like non empty V14( the carrier' of F₁()) V18( the carrier' of F₁(), the carrier of F₁()) Element of bool [: the carrier' of F₁(), the carrier of F₁():]
[: the carrier' of F₁(), the carrier of F₁():] is set
bool [: the carrier' of F₁(), the carrier of F₁():] is set
the ResultSort of F₁() * (SORTS I) is Relation-like set
MSAlgebra(# (SORTS I),(OPS I) #) is strict MSAlgebra over F₁()
I is non-empty MSAlgebra over F₁()
E is strict non-empty MSSubAlgebra of I
I is non-empty MSAlgebra over F₁()
E is non-empty MSAlgebra over F₁()
I is strict non-empty MSAlgebra over F₁()
the Sorts of I is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of I
E is non-empty MSAlgebra over F₁()
the Sorts of E is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
K is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of E
E is non-empty MSAlgebra over F₁()
the Sorts of E is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
K is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of E
F is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of E
F ** F₃() is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of E
K is Element of the carrier of F₁()
(Equations F₁()) . K is non empty set
E is non-empty MSAlgebra over F₁()
F is Element of (Equations F₁()) . K
A is non-empty MSAlgebra over F₁()
(F₁(),( the carrier of F₁() --> NAT),I,E) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)), the Sorts of I
FreeMSA ( the carrier of F₁() --> NAT) is non-empty V126(F₁()) MSAlgebra over F₁()
the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
(F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)), the Sorts of F₂()
E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of F₂(), the Sorts of I
E ** (F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)), the Sorts of I
K is set
E . K is Relation-like Function-like set
A is non-empty MSAlgebra over F₁()
B is strict non-empty MSSubAlgebra of A
e is Element of the carrier of F₁()
(Equations F₁()) . e is non empty set
x is Element of (Equations F₁()) . e
A is non-empty MSAlgebra over F₁()
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
B is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of A
e is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of I, the Sorts of A
e ** E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of A
A is set
dom (E . K) is set
B is set
(E . K) . A is set
(E . K) . B is set
F is Element of the carrier of F₁()
the Sorts of F₂() . F is non empty set
E . F is Relation-like the Sorts of F₂() . F -defined the Sorts of I . F -valued Function-like non empty V14( the Sorts of F₂() . F) V18( the Sorts of F₂() . F, the Sorts of I . F) Element of bool [:( the Sorts of F₂() . F),( the Sorts of I . F):]
the Sorts of I . F is non empty set
[:( the Sorts of F₂() . F),( the Sorts of I . F):] is set
bool [:( the Sorts of F₂() . F),( the Sorts of I . F):] is set
dom (E . F) is Element of bool ( the Sorts of F₂() . F)
bool ( the Sorts of F₂() . F) is set
(F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F is Relation-like the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F -defined the Sorts of F₂() . F -valued Function-like non empty V14( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F) V18( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F, the Sorts of F₂() . F) Element of bool [:( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F),( the Sorts of F₂() . F):]
the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F is non empty set
[:( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F),( the Sorts of F₂() . F):] is set
bool [:( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F),( the Sorts of F₂() . F):] is set
rng ((F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F) is non empty Element of bool ( the Sorts of F₂() . F)
dom ((F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F) is Element of bool ( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F)
bool ( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F) is set
e is set
((F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F) . e is set
x is set
((F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F) . x is set
the Sorts of (TermAlg F₁()) . F is non empty set
h is Element of the Sorts of (TermAlg F₁()) . F
t2 is Element of the Sorts of (TermAlg F₁()) . F
h '=' t2 is V15() Element of (Equations F₁()) . F
(Equations F₁()) . F is non empty set
{h,t2} is non empty set
{h} is non empty set
{{h,t2},{h}} is non empty set
(F₁(),( the carrier of F₁() --> NAT),I,E) . F is Relation-like the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F -defined the Sorts of I . F -valued Function-like non empty V14( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F) V18( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F, the Sorts of I . F) Element of bool [:( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F),( the Sorts of I . F):]
[:( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F),( the Sorts of I . F):] is set
bool [:( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F),( the Sorts of I . F):] is set
((F₁(),( the carrier of F₁() --> NAT),I,E) . F) . h is set
(E . F) * ((F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F) is Relation-like the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F -defined the Sorts of I . F -valued Function-like non empty V14( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F) V18( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F, the Sorts of I . F) Element of bool [:( the Sorts of (FreeMSA ( the carrier of F₁() --> NAT)) . F),( the Sorts of I . F):]
((E . F) * ((F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F)) . h is set
(E . F) . A is set
((E . F) * ((F₁(),( the carrier of F₁() --> NAT),F₂(),F₃()) . F)) . t2 is set
((F₁(),( the carrier of F₁() --> NAT),I,E) . F) . t2 is set
(h '=' t2) `1 is set
((F<sub>1</sub>(),( the carrier of F<sub>1</sub>() --> NAT),F<sub>2</sub>(),F<sub>3</sub>()) . F) . ((h '=' t2) `1) is set
(h '=' t2) `2 is set
((F<sub>1</sub>(),( the carrier of F<sub>1</sub>() --> NAT),F<sub>2</sub>(),F<sub>3</sub>()) . F) . ((h '=' t2) `2) is set
Image E is strict non-empty MSSubAlgebra of I
F₁() is non empty non void V62() ManySortedSign
the carrier of F₁() is non empty set
Equations F₁() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
TermAlg F₁() is strict non-empty V126(F₁()) MSAlgebra over F₁()
the carrier of F₁() --> NAT is Relation-like non-empty non empty-yielding the carrier of F₁() -defined bool REAL -valued Function-like constant non empty V14( the carrier of F₁()) V18( the carrier of F₁(), bool REAL) Element of bool [: the carrier of F₁(),(bool REAL):]
[: the carrier of F₁(),(bool REAL):] is set
bool [: the carrier of F₁(),(bool REAL):] is set
{NAT} is non empty set
[: the carrier of F₁(),{NAT}:] is set
FreeMSA ( the carrier of F₁() --> NAT) is non-empty V126(F₁()) MSAlgebra over F₁()
the Sorts of (TermAlg F₁()) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
[| the Sorts of (TermAlg F₁()), the Sorts of (TermAlg F₁())|] is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
XX is non-empty MSAlgebra over F₁()
I is strict non-empty MSSubAlgebra of XX
the carrier of F₁() --> NAT is Relation-like non-empty non empty-yielding the carrier of F₁() -defined {NAT} -valued Function-like constant non empty V14( the carrier of F₁()) V18( the carrier of F₁(),{NAT}) Element of bool [: the carrier of F₁(),{NAT}:]
bool [: the carrier of F₁(),{NAT}:] is set
E is set
E is Element of the carrier of F₁()
(Equations F₁()) . E is non empty set
{ b₁ where b₁ is Element of (Equations F₁()) . E : for b₂ being non-empty MSAlgebra over F₁() holds
( not P₁[b₂] or b₂ |= b₁ ) } is set
K is set
E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
E is set
E . E is set
(Equations F₁()) . E is set
K is Element of the carrier of F₁()
(Equations F₁()) . K is non empty set
{ b₁ where b₁ is Element of (Equations F₁()) . K : for b₂ being non-empty MSAlgebra over F₁() holds
( not P₁[b₂] or b₂ |= b₁ ) } is set
F is set
A is Element of (Equations F₁()) . K
K is non-empty MSAlgebra over F₁()
F is non-empty MSAlgebra over F₁()
E is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) ManySortedSubset of Equations F₁()
K is non-empty MSAlgebra over F₁()
F is Element of the carrier of F₁()
(Equations F₁()) . F is non empty set
A is Element of (Equations F₁()) . F
E . F is set
B is Element of the carrier of F₁()
(Equations F₁()) . B is non empty set
{ b₁ where b₁ is Element of (Equations F₁()) . B : for b₂ being non-empty MSAlgebra over F₁() holds
( not P₁[b₂] or b₂ |= b₁ ) } is set
F is Element of the carrier of F₁()
(Equations F₁()) . F is non empty set
E . F is set
A is Element of (Equations F₁()) . F
B is Element of the carrier of F₁()
(Equations F₁()) . B is non empty set
{ b₁ where b₁ is Element of (Equations F₁()) . B : for b₂ being non-empty MSAlgebra over F₁() holds
( not P₁[b₂] or b₂ |= b₁ ) } is set
B is Element of (Equations F₁()) . F
K is non-empty MSAlgebra over F₁()
F is strict non-empty MSSubAlgebra of K
K is set
F is Relation-like K -defined Function-like V14(K) MSAlgebra-Family of K,F₁()
product F is non-empty MSAlgebra over F₁()
SORTS F is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
OPS F is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(SORTS F)), the ResultSort of F₁() * (SORTS F)
the carrier' of F₁() is non empty set
the Arity of F₁() is Relation-like the carrier' of F₁() -defined K171( the carrier of F₁()) -valued Function-like V18( the carrier' of F₁(),K171( the carrier of F₁())) Element of bool [: the carrier' of F₁(),K171( the carrier of F₁()):]
K171( the carrier of F₁()) is M11( the carrier of F₁())
[: the carrier' of F₁(),K171( the carrier of F₁()):] is set
bool [: the carrier' of F₁(),K171( the carrier of F₁()):] is set
K174( the carrier of F₁(),(SORTS F)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(SORTS F)) is Relation-like set
the ResultSort of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() -valued Function-like non empty V14( the carrier' of F₁()) V18( the carrier' of F₁(), the carrier of F₁()) Element of bool [: the carrier' of F₁(), the carrier of F₁():]
[: the carrier' of F₁(), the carrier of F₁():] is set
bool [: the carrier' of F₁(), the carrier of F₁():] is set
the ResultSort of F₁() * (SORTS F) is Relation-like set
MSAlgebra(# (SORTS F),(OPS F) #) is strict MSAlgebra over F₁()
K is non-empty MSAlgebra over F₁()
F is non-empty MSAlgebra over F₁()
K is strict non-empty MSAlgebra over F₁()
the Sorts of K is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
F is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of K
A is non-empty MSAlgebra over F₁()
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
B is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of A
e is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of K, the Sorts of A
e ** F is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of A
A is set
B is Relation-like A -defined Function-like V14(A) MSAlgebra-Family of A,F₁()
product B is non-empty MSAlgebra over F₁()
SORTS B is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
OPS B is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(SORTS B)), the ResultSort of F₁() * (SORTS B)
the carrier' of F₁() is non empty set
the Arity of F₁() is Relation-like the carrier' of F₁() -defined K171( the carrier of F₁()) -valued Function-like V18( the carrier' of F₁(),K171( the carrier of F₁())) Element of bool [: the carrier' of F₁(),K171( the carrier of F₁()):]
K171( the carrier of F₁()) is M11( the carrier of F₁())
[: the carrier' of F₁(),K171( the carrier of F₁()):] is set
bool [: the carrier' of F₁(),K171( the carrier of F₁()):] is set
K174( the carrier of F₁(),(SORTS B)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(SORTS B)) is Relation-like set
the ResultSort of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() -valued Function-like non empty V14( the carrier' of F₁()) V18( the carrier' of F₁(), the carrier of F₁()) Element of bool [: the carrier' of F₁(), the carrier of F₁():]
[: the carrier' of F₁(), the carrier of F₁():] is set
bool [: the carrier' of F₁(), the carrier of F₁():] is set
the ResultSort of F₁() * (SORTS B) is Relation-like set
MSAlgebra(# (SORTS B),(OPS B) #) is strict MSAlgebra over F₁()
A is non-empty MSAlgebra over F₁()
B is Element of the carrier of F₁()
(Equations F₁()) . B is non empty set
E . B is set
e is Element of (Equations F₁()) . B
x is Element of the carrier of F₁()
(Equations F₁()) . x is non empty set
{ b₁ where b₁ is Element of (Equations F₁()) . x : for b₂ being non-empty MSAlgebra over F₁() holds
( not P₁[b₂] or b₂ |= b₁ ) } is set
x is Element of (Equations F₁()) . B
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
h is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (TermAlg F₁()), the Sorts of A
h . B is Relation-like the Sorts of (TermAlg F₁()) . B -defined the Sorts of A . B -valued Function-like non empty V14( the Sorts of (TermAlg F₁()) . B) V18( the Sorts of (TermAlg F₁()) . B, the Sorts of A . B) Element of bool [:( the Sorts of (TermAlg F₁()) . B),( the Sorts of A . B):]
the Sorts of (TermAlg F₁()) . B is non empty set
the Sorts of A . B is non empty set
[:( the Sorts of (TermAlg F₁()) . B),( the Sorts of A . B):] is set
bool [:( the Sorts of (TermAlg F₁()) . B),( the Sorts of A . B):] is set
e `1 is set
(h . B) . (e `1) is set
e `2 is set
(h . B) . (e `2) is set
B is non-empty MSAlgebra over F₁()
the Sorts of B is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
e is Relation-like the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of B, the Sorts of B
QuotMSAlg (B,e) is strict non-empty MSAlgebra over F₁()
Class e is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty V14( the carrier of F₁()) set
QuotCharact e is Relation-like the carrier' of F₁() -defined Function-like non empty V14( the carrier' of F₁()) ManySortedFunction of the Arity of F₁() * K174( the carrier of F₁(),(Class e)), the ResultSort of F₁() * (Class e)
the carrier' of F₁() is non empty set
the Arity of F₁() is Relation-like the carrier' of F₁() -defined K171( the carrier of F₁()) -valued Function-like V18( the carrier' of F₁(),K171( the carrier of F₁())) Element of bool [: the carrier' of F₁(),K171( the carrier of F₁()):]
K171( the carrier of F₁()) is M11( the carrier of F₁())
[: the carrier' of F₁(),K171( the carrier of F₁()):] is set
bool [: the carrier' of F₁(),K171( the carrier of F₁()):] is set
K174( the carrier of F₁(),(Class e)) is Relation-like K171( the carrier of F₁()) -defined Function-like V14(K171( the carrier of F₁())) set
the Arity of F₁() * K174( the carrier of F₁(),(Class e)) is Relation-like set
the ResultSort of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() -valued Function-like non empty V14( the carrier' of F₁()) V18( the carrier' of F₁(), the carrier of F₁()) Element of bool [: the carrier' of F₁(), the carrier of F₁():]
[: the carrier' of F₁(), the carrier of F₁():] is set
bool [: the carrier' of F₁(), the carrier of F₁():] is set
the ResultSort of F₁() * (Class e) is Relation-like set
MSAlgebra(# (Class e),(QuotCharact e) #) is strict MSAlgebra over F₁()
B is strict non-empty finitely-generated MSSubAlgebra of A