NAT is non empty non trivial V24() V25() V26() non finite countable denumerable Element of bool REAL
REAL is set
bool REAL is set
NAT is non empty non trivial V24() V25() V26() non finite countable denumerable set
bool NAT is set
bool NAT is set
[:NAT,NAT:] is Relation-like set
[:[:NAT,NAT:],NAT:] is Relation-like set
bool [:[:NAT,NAT:],NAT:] is set
K214() is non empty V65() L9()
the carrier of K214() is non empty set
K217() is countable Element of bool NAT
[:K217(),K217():] is Relation-like set
[:[:K217(),K217():],K217():] is Relation-like set
bool [:[:K217(),K217():],K217():] is set
K284() is set
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() finite finite-yielding V35() Function-yielding Relation-yielding Cardinal-yielding countable set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() finite finite-yielding V35() Function-yielding Relation-yielding Cardinal-yielding countable set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() finite finite-yielding V35() Function-yielding Relation-yielding Cardinal-yielding countable set
{{}} is functional non empty finite V35() with_common_domain countable set
K155({{}}) is M8({{}})
[:K155({{}}),{{}}:] is Relation-like set
bool [:K155({{}}),{{}}:] is set
PFuncs (K155({{}}),{{}}) is set
1 is non empty set
{{},1} is non empty finite countable set
K429() is set
bool K429() is set
K430() is Element of bool K429()
K470() is non empty strict DTConstrStr
the carrier of K470() is non empty set
K433( the carrier of K470()) is non empty M34( the carrier of K470())
K469(K470()) is Element of bool K433( the carrier of K470())
bool K433( the carrier of K470()) is set
[:K469(K470()),NAT:] is Relation-like set
bool [:K469(K470()),NAT:] is set
[:NAT,K469(K470()):] is Relation-like set
bool [:NAT,K469(K470()):] is set
S is set
A is Relation-like S -defined Function-like total set
Bool A is functional non empty with_common_domain V139(S,A) V140(S,A) V141(S,A) V142(S,A) V143(S,A) V144(S,A) Element of bool (Bool A)
Bool A is functional non empty with_common_domain set
bool (Bool A) is set
[[0]] S is Relation-like empty-yielding S -defined Function-like total finite-yielding set
S --> {} is Relation-like S -defined {{}} -valued Function-like constant total V18(S,{{}}) Function-yielding Relation-yielding Element of bool [:S,{{}}:]
[:S,{{}}:] is Relation-like set
bool [:S,{{}}:] is set
B is Relation-like S -defined Function-like total Element of Bool A
S is set
A is Relation-like non-empty S -defined Function-like total set
B is set
A . B is set
the Element of A . B is Element of A . B
{ the Element of A . B} is non empty finite countable set
C1 is non empty finite countable set
B is Relation-like S -defined Function-like total set
F is set
B . F is set
A . F is set
C1 is set
G is Element of A . F
{G} is non empty finite countable set
F is Relation-like S -defined Function-like total ManySortedSubset of A
C1 is set
F . C1 is set
A . C1 is set
G is Element of A . C1
{G} is non empty finite countable set
C1 is set
F . C1 is set
A . C1 is set
G is Element of A . C1
{G} is non empty finite countable set
S is non empty non void V54() ManySortedSign
the carrier' of S is non empty set
B is Element of the carrier' of S
A is non-empty MSAlgebra over S
Args (B,A) is functional non empty Element of rng K158( the carrier of S, the Sorts of A)
the carrier of S is non empty set
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
K155( the carrier of S) is M8( the carrier of S)
rng K158( the carrier of S, the Sorts of A) is set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of A)) . B is set
F is Relation-like Function-like Element of Args (B,A)
dom F is set
the_arity_of B is Relation-like NAT -defined the carrier of S -valued Function-like FinSequence-like M9( the carrier of S,K155( the carrier of S))
the Arity of S . B is Element of K155( the carrier of S)
dom (the_arity_of B) is countable Element of bool NAT
C1 is V24() V25() V26() V30() set
Seg C1 is countable Element of bool NAT
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is set
F is Relation-like A -defined Function-like total MSAlgebra-Family of A,S
SORTS F is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is Element of the carrier of S
(SORTS F) . B is non empty set
C1 is Element of (SORTS F) . B
Carrier (F,B) is Relation-like non-empty A -defined Function-like total set
product (Carrier (F,B)) is functional non empty with_common_domain product-like set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
FreeMSA A is strict non-empty MSAlgebra over S
FreeGen A is Relation-like the carrier of S -defined Function-like non empty total GeneratorSet of FreeMSA A
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
FreeMSA A is strict non-empty MSAlgebra over S
S is non empty non void V54() ManySortedSign
A is non-empty MSAlgebra over S
B is non-empty MSAlgebra over S
[:A,B:] is strict MSAlgebra over S
the carrier of S is non empty set
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
[| the Sorts of A, the Sorts of B|] is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
K155( the carrier of S) is M8( the carrier of S)
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the Charact of A is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of A), the ResultSort of S * the Sorts of A
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
the Charact of B is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of B), the ResultSort of S * the Sorts of B
K158( the carrier of S, the Sorts of B) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S, the Sorts of B) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * the Sorts of B is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
[[: the Charact of A, the Charact of B:]] is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,[| the Sorts of A, the Sorts of B|]), the ResultSort of S * [| the Sorts of A, the Sorts of B|]
K158( the carrier of S,[| the Sorts of A, the Sorts of B|]) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,[| the Sorts of A, the Sorts of B|]) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * [| the Sorts of A, the Sorts of B|] is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# [| the Sorts of A, the Sorts of B|],[[: the Charact of A, the Charact of B:]] #) is strict MSAlgebra over S
the Sorts of [:A,B:] is Relation-like the carrier of S -defined Function-like non empty total set
S is set
A is set
B is set
[:A,B:] is Relation-like set
F is Relation-like Function-like set
dom F is set
F . S is set
pr1 F is Relation-like Function-like set
(pr1 F) . S is set
pr2 F is Relation-like Function-like set
(pr2 F) . S is set
[((pr1 F) . S),((pr2 F) . S)] is V15() set
{((pr1 F) . S),((pr2 F) . S)} is non empty finite countable set
{((pr1 F) . S)} is non empty finite countable set
{{((pr1 F) . S),((pr2 F) . S)},{((pr1 F) . S)}} is non empty finite V35() countable set
(F . S) `1 is set
(F . S) `2 is set
S is non empty set
A is set
{A} is non empty finite countable set
[:S,{A}:] is Relation-like set
bool [:S,{A}:] is set
B is Relation-like S -defined {A} -valued Function-like non empty total V18(S,{A}) Element of bool [:S,{A}:]
rng B is non empty finite countable Element of bool {A}
bool {A} is finite V35() countable set
F is set
C1 is set
dom B is non empty Element of bool S
bool S is set
B . C1 is set
S is set
nabla S is Relation-like S -defined S -valued total V18(S,S) reflexive symmetric transitive Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] is set
Class (nabla S) is with_non-empty_elements a_partition of S
{S} is non empty finite countable set
A is set
B is set
Class ((nabla S),B) is Element of bool S
bool S is set
S is non empty set
nabla S is Relation-like S -defined S -valued total V18(S,S) reflexive symmetric transitive Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] is set
Class (nabla S) is non empty with_non-empty_elements a_partition of S
{S} is non empty finite countable set
A is set
B is set
Class ((nabla S),A) is Element of bool S
bool S is set
S is set
A is set
{A} is non empty finite countable set
S --> {A} is Relation-like non-empty S -defined {{A}} -valued Function-like constant total V18(S,{{A}}) Element of bool [:S,{{A}}:]
{{A}} is non empty finite V35() countable set
[:S,{{A}}:] is Relation-like set
bool [:S,{{A}}:] is set
S --> A is Relation-like S -defined {A} -valued Function-like constant total V18(S,{A}) Element of bool [:S,{A}:]
[:S,{A}:] is Relation-like set
bool [:S,{A}:] is set
B is Relation-like S -defined Function-like total set
{B} is Relation-like non-empty S -defined Function-like total finite-yielding set
F is set
{B} . F is finite countable set
B . F is set
{(B . F)} is non empty finite countable set
(S --> {A}) . F is set
S is set
A is Relation-like S -defined Function-like total set
B is Relation-like S -defined Function-like total set
F is set
B . F is set
A . F is set
{{}} \/ (A . F) is non empty set
F is Relation-like non-empty S -defined Function-like total set
C1 is set
A . C1 is set
F . C1 is set
(A . C1) \/ {{}} is non empty set
S is set
A is Relation-like non-empty S -defined Function-like total set
B is Relation-like S -defined Function-like total finite-yielding ManySortedSubset of A
F is set
A . F is set
the Element of A . F is Element of A . F
{ the Element of A . F} is non empty finite countable set
B . F is finite countable set
{ the Element of A . F} \/ (B . F) is non empty finite countable set
G is non empty finite countable set
F is Relation-like S -defined Function-like total set
C1 is set
F . C1 is set
A . C1 is set
B . C1 is finite countable set
G is Element of A . C1
{G} is non empty finite countable set
{G} \/ (B . C1) is non empty finite countable set
I is set
C1 is set
F . C1 is set
B . C1 is finite countable set
A . C1 is set
I is Element of A . C1
{I} is non empty finite countable set
{I} \/ (B . C1) is non empty finite countable set
C1 is set
F . C1 is set
A . C1 is set
B . C1 is finite countable set
G is Element of A . C1
{G} is non empty finite countable set
{G} \/ (B . C1) is non empty finite countable set
C1 is Relation-like non-empty S -defined Function-like total finite-yielding ManySortedSubset of A
G is set
B . G is finite countable set
C1 . G is finite countable set
A . G is set
I is Element of A . G
{I} is non empty finite countable set
{I} \/ (B . G) is non empty finite countable set
S is set
A is Relation-like S -defined Function-like total set
B is Relation-like S -defined Function-like total set
{B} is Relation-like non-empty S -defined Function-like total finite-yielding set
F is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,{B}
C1 is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,{B}
G is set
{B} . G is finite countable set
B . G is set
{(B . G)} is non empty finite countable set
F . G is Relation-like Function-like set
A . G is set
[:(A . G),({B} . G):] is Relation-like set
bool [:(A . G),({B} . G):] is set
C1 . G is Relation-like Function-like set
S is set
A is Relation-like non-empty S -defined Function-like total set
B is Relation-like S -defined Function-like total set
{B} is Relation-like non-empty S -defined Function-like total finite-yielding set
F is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,{B}
C1 is set
F . C1 is Relation-like Function-like set
rng (F . C1) is set
{B} . C1 is finite countable set
B . C1 is set
{(B . C1)} is non empty finite countable set
A . C1 is set
[:(A . C1),({B} . C1):] is Relation-like set
bool [:(A . C1),({B} . C1):] is set
S is set
A is Relation-like S -defined Function-like total set
{A} is Relation-like non-empty S -defined Function-like total finite-yielding set
B is Relation-like non-empty S -defined Function-like total set
F is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of {A},B
C1 is set
{A} . C1 is finite countable set
A . C1 is set
{(A . C1)} is non empty finite countable set
F . C1 is Relation-like Function-like set
B . C1 is set
[:({A} . C1),(B . C1):] is Relation-like set
bool [:({A} . C1),(B . C1):] is set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
Reverse A is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of FreeGen A,A
FreeGen A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total free GeneratorSet of FreeMSA A
FreeMSA A is strict non-empty free MSAlgebra over S
DTConMSA A is non empty strict V175() V176() V177() DTConstrStr
F is set
(Reverse A) . F is Relation-like Function-like set
C1 is Element of the carrier of S
(Reverse A) . C1 is Relation-like (FreeGen A) . C1 -defined A . C1 -valued Function-like non empty total V18((FreeGen A) . C1,A . C1) Element of bool [:((FreeGen A) . C1),(A . C1):]
(FreeGen A) . C1 is non empty set
A . C1 is non empty set
[:((FreeGen A) . C1),(A . C1):] is Relation-like set
bool [:((FreeGen A) . C1),(A . C1):] is set
I is set
dom ((Reverse A) . F) is set
sQ is set
((Reverse A) . F) . I is set
((Reverse A) . F) . sQ is set
FreeGen (C1,A) is non empty Element of bool ((FreeSort A) . C1)
FreeSort A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
(FreeSort A) . C1 is non empty set
bool ((FreeSort A) . C1) is set
Reverse (C1,A) is Relation-like FreeGen (C1,A) -defined A . C1 -valued Function-like non empty total V18( FreeGen (C1,A),A . C1) Element of bool [:(FreeGen (C1,A)),(A . C1):]
[:(FreeGen (C1,A)),(A . C1):] is Relation-like set
bool [:(FreeGen (C1,A)),(A . C1):] is set
dom ((Reverse A) . C1) is non empty Element of bool ((FreeGen A) . C1)
bool ((FreeGen A) . C1) is set
sF is set
[sF,C1] is V15() set
{sF,C1} is non empty finite countable set
{sF} is non empty finite countable set
{{sF,C1},{sF}} is non empty finite V35() countable set
root-tree [sF,C1] is Relation-like Function-like finite countable V164() set
Terminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
the carrier of (DTConMSA A) is non empty set
bool the carrier of (DTConMSA A) is set
C12 is Element of the carrier of (DTConMSA A)
C12 `2 is set
root-tree C12 is Relation-like Function-like finite countable V164() Element of K433( the carrier of (DTConMSA A))
K433( the carrier of (DTConMSA A)) is non empty M34( the carrier of (DTConMSA A))
{ (root-tree b1) where b1 is Element of the carrier of (DTConMSA A) : ( b1 in Terminals (DTConMSA A) & b1 `2 = C1 ) } is set
((Reverse A) . C1) . sQ is set
[sF,C1] `1 is set
H is set
[H,C1] is V15() set
{H,C1} is non empty finite countable set
{H} is non empty finite countable set
{{H,C1},{H}} is non empty finite V35() countable set
root-tree [H,C1] is Relation-like Function-like finite countable V164() set
i is Element of the carrier of (DTConMSA A)
i `2 is set
root-tree i is Relation-like Function-like finite countable V164() Element of K433( the carrier of (DTConMSA A))
((Reverse A) . C1) . I is set
[H,C1] `1 is set
S is set
S --> NAT is Relation-like non-empty S -defined {NAT} -valued Function-like constant total V18(S,{NAT}) Element of bool [:S,{NAT}:]
{NAT} is non empty finite countable set
[:S,{NAT}:] is Relation-like set
bool [:S,{NAT}:] is set
A is Relation-like non-empty S -defined Function-like total finite-yielding set
B is set
A . B is finite countable set
[:NAT,(A . B):] is Relation-like set
bool [:NAT,(A . B):] is set
F is Relation-like NAT -defined A . B -valued Function-like V18( NAT ,A . B) Element of bool [:NAT,(A . B):]
rng F is finite countable Element of bool (A . B)
bool (A . B) is finite V35() countable set
B is Relation-like S -defined Function-like total set
F is set
B . F is set
(S --> NAT) . F is set
A . F is finite countable set
[:((S --> NAT) . F),(A . F):] is Relation-like set
bool [:((S --> NAT) . F),(A . F):] is set
[:NAT,(A . F):] is Relation-like set
bool [:NAT,(A . F):] is set
C1 is Relation-like NAT -defined A . F -valued Function-like V18( NAT ,A . F) Element of bool [:NAT,(A . F):]
rng C1 is finite countable Element of bool (A . F)
bool (A . F) is finite V35() countable set
F is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of S --> NAT,A
C1 is set
F . C1 is Relation-like Function-like set
rng (F . C1) is set
A . C1 is finite countable set
[:NAT,(A . C1):] is Relation-like set
bool [:NAT,(A . C1):] is set
G is Relation-like NAT -defined A . C1 -valued Function-like V18( NAT ,A . C1) Element of bool [:NAT,(A . C1):]
rng G is finite countable Element of bool (A . C1)
bool (A . C1) is finite V35() countable set
S is non empty V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
product the Sorts of A is functional non empty with_common_domain product-like set
B is Relation-like the carrier of S -defined Function-like the Sorts of A -compatible non empty total Element of product the Sorts of A
F is Relation-like the carrier of S -defined Function-like the Sorts of A -compatible non empty total Element of product the Sorts of A
dom B is non empty Element of bool the carrier of S
bool the carrier of S is set
dom the Sorts of A is non empty Element of bool the carrier of S
dom F is non empty Element of bool the carrier of S
G is set
proj ( the Sorts of A,G) is Relation-like product the Sorts of A -defined Function-like non empty total set
dom (proj ( the Sorts of A,G)) is functional non empty with_common_domain Element of bool (product the Sorts of A)
bool (product the Sorts of A) is set
B . G is set
(proj ( the Sorts of A,G)) . B is set
(proj ( the Sorts of A,G)) . F is set
F . G is set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non empty set
B is Element of the carrier of S
F is Relation-like A -defined Function-like non empty total MSAlgebra-Family of A,S
Carrier (F,B) is Relation-like non-empty non empty-yielding A -defined Function-like non empty total set
product (Carrier (F,B)) is functional non empty with_common_domain product-like set
C1 is Relation-like A -defined Function-like Carrier (F,B) -compatible non empty total Element of product (Carrier (F,B))
G is Relation-like A -defined Function-like Carrier (F,B) -compatible non empty total Element of product (Carrier (F,B))
dom C1 is non empty Element of bool A
bool A is set
dom (Carrier (F,B)) is non empty Element of bool A
dom G is non empty Element of bool A
I is set
proj ((Carrier (F,B)),I) is Relation-like product (Carrier (F,B)) -defined Function-like non empty total set
dom (proj ((Carrier (F,B)),I)) is functional non empty with_common_domain Element of bool (product (Carrier (F,B)))
bool (product (Carrier (F,B))) is set
C1 . I is set
(proj ((Carrier (F,B)),I)) . C1 is set
(proj ((Carrier (F,B)),I)) . G is set
G . I is set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
B is non-empty MSAlgebra over S
the Sorts of B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F is non-empty MSSubAlgebra of A
the Sorts of F is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
C1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of B, the Sorts of F
id the Sorts of F is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of F, the Sorts of F
G is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of F, the Sorts of A
G ** C1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of B, the Sorts of A
I is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of B, the Sorts of A
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is non-empty MSAlgebra over S
the Sorts of B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of B
Image F is strict non-empty MSSubAlgebra of B
the Sorts of (Image F) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
C1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (Image F)
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is non-empty MSAlgebra over S
the Sorts of B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of B
C1 is Element of the carrier' of S
Args (C1,B) is functional non empty Element of rng K158( the carrier of S, the Sorts of B)
K158( the carrier of S, the Sorts of B) is Relation-like K155( the carrier of S) -defined Function-like total set
K155( the carrier of S) is M8( the carrier of S)
rng K158( the carrier of S, the Sorts of B) is set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the Arity of S * K158( the carrier of S, the Sorts of B) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of B)) . C1 is set
Args (C1,A) is functional non empty Element of rng K158( the carrier of S, the Sorts of A)
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
rng K158( the carrier of S, the Sorts of A) is set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of A)) . C1 is set
G is Relation-like Function-like FinSequence-like Element of Args (C1,B)
the_arity_of C1 is Relation-like NAT -defined the carrier of S -valued Function-like FinSequence-like M9( the carrier of S,K155( the carrier of S))
the Arity of S . C1 is Element of K155( the carrier of S)
len (the_arity_of C1) is V24() V25() V26() V30() Element of NAT
Seg (len (the_arity_of C1)) is countable Element of bool NAT
sQ is V24() V25() V26() V30() Element of NAT
(the_arity_of C1) /. sQ is Element of the carrier of S
the Sorts of A . ((the_arity_of C1) /. sQ) is non empty set
the Sorts of B . ((the_arity_of C1) /. sQ) is non empty set
F . ((the_arity_of C1) /. sQ) is Relation-like the Sorts of A . ((the_arity_of C1) /. sQ) -defined the Sorts of B . ((the_arity_of C1) /. sQ) -valued Function-like non empty total V18( the Sorts of A . ((the_arity_of C1) /. sQ), the Sorts of B . ((the_arity_of C1) /. sQ)) Element of bool [:( the Sorts of A . ((the_arity_of C1) /. sQ)),( the Sorts of B . ((the_arity_of C1) /. sQ)):]
[:( the Sorts of A . ((the_arity_of C1) /. sQ)),( the Sorts of B . ((the_arity_of C1) /. sQ)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of C1) /. sQ)),( the Sorts of B . ((the_arity_of C1) /. sQ)):] is set
G . sQ is set
dom (the_arity_of C1) is countable Element of bool NAT
rng (F . ((the_arity_of C1) /. sQ)) is non empty Element of bool ( the Sorts of B . ((the_arity_of C1) /. sQ))
bool ( the Sorts of B . ((the_arity_of C1) /. sQ)) is set
C12 is set
(F . ((the_arity_of C1) /. sQ)) . C12 is set
H is Element of the Sorts of A . ((the_arity_of C1) /. sQ)
(F . ((the_arity_of C1) /. sQ)) . H is Element of the Sorts of B . ((the_arity_of C1) /. sQ)
sQ is Relation-like Function-like FinSequence-like set
dom sQ is countable Element of bool NAT
len sQ is V24() V25() V26() V30() Element of NAT
sF is V24() V25() V26() V30() set
sQ . sF is set
(the_arity_of C1) /. sF is Element of the carrier of S
the Sorts of A . ((the_arity_of C1) /. sF) is non empty set
the Sorts of B . ((the_arity_of C1) /. sF) is non empty set
F . ((the_arity_of C1) /. sF) is Relation-like the Sorts of A . ((the_arity_of C1) /. sF) -defined the Sorts of B . ((the_arity_of C1) /. sF) -valued Function-like non empty total V18( the Sorts of A . ((the_arity_of C1) /. sF), the Sorts of B . ((the_arity_of C1) /. sF)) Element of bool [:( the Sorts of A . ((the_arity_of C1) /. sF)),( the Sorts of B . ((the_arity_of C1) /. sF)):]
[:( the Sorts of A . ((the_arity_of C1) /. sF)),( the Sorts of B . ((the_arity_of C1) /. sF)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of C1) /. sF)),( the Sorts of B . ((the_arity_of C1) /. sF)):] is set
G . sF is set
C12 is Element of the Sorts of A . ((the_arity_of C1) /. sF)
(F . ((the_arity_of C1) /. sF)) . C12 is Element of the Sorts of B . ((the_arity_of C1) /. sF)
sF is Relation-like Function-like FinSequence-like Element of Args (C1,A)
F # sF is Relation-like Function-like FinSequence-like Element of Args (C1,B)
dom (the_arity_of C1) is countable Element of bool NAT
(the_arity_of C1) * the Sorts of B is Relation-like non-empty NAT -defined dom (the_arity_of C1) -defined Function-like total set
H is Relation-like non-empty dom (the_arity_of C1) -defined Function-like total set
product H is functional non empty with_common_domain product-like set
dom ((the_arity_of C1) * the Sorts of B) is countable Element of bool NAT
dom G is countable Element of bool NAT
i is V24() V25() V26() V30() set
(F # sF) . i is set
G . i is set
(the_arity_of C1) /. i is Element of the carrier of S
the Sorts of A . ((the_arity_of C1) /. i) is non empty set
the Sorts of B . ((the_arity_of C1) /. i) is non empty set
F . ((the_arity_of C1) /. i) is Relation-like the Sorts of A . ((the_arity_of C1) /. i) -defined the Sorts of B . ((the_arity_of C1) /. i) -valued Function-like non empty total V18( the Sorts of A . ((the_arity_of C1) /. i), the Sorts of B . ((the_arity_of C1) /. i)) Element of bool [:( the Sorts of A . ((the_arity_of C1) /. i)),( the Sorts of B . ((the_arity_of C1) /. i)):]
[:( the Sorts of A . ((the_arity_of C1) /. i)),( the Sorts of B . ((the_arity_of C1) /. i)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of C1) /. i)),( the Sorts of B . ((the_arity_of C1) /. i)):] is set
sF . i is set
s is Element of the Sorts of A . ((the_arity_of C1) /. i)
(F . ((the_arity_of C1) /. i)) . s is Element of the Sorts of B . ((the_arity_of C1) /. i)
dom (F # sF) is countable Element of bool NAT
S is non empty non void V54() ManySortedSign
the carrier' of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the carrier of S is non empty set
B is Element of the carrier' of S
Args (B,A) is functional non empty Element of rng K158( the carrier of S, the Sorts of A)
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
K155( the carrier of S) is M8( the carrier of S)
rng K158( the carrier of S, the Sorts of A) is set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of A)) . B is set
Result (B,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty with_non-empty_elements set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of A) . B is non empty set
Den (B,A) is Relation-like Args (B,A) -defined Result (B,A) -valued Function-like non empty total V18( Args (B,A), Result (B,A)) Element of bool [:(Args (B,A)),(Result (B,A)):]
[:(Args (B,A)),(Result (B,A)):] is Relation-like set
bool [:(Args (B,A)),(Result (B,A)):] is set
the Charact of A is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of A), the ResultSort of S * the Sorts of A
the Charact of A . B is set
the_result_sort_of B is Element of the carrier of S
the ResultSort of S . B is Element of the carrier of S
the Sorts of A . (the_result_sort_of B) is non empty set
F is Relation-like Function-like FinSequence-like Element of Args (B,A)
(Den (B,A)) . F is Element of Result (B,A)
the Sorts of A . ( the ResultSort of S . B) is non empty set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is non-empty MSAlgebra over S
the Sorts of B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F is non-empty MSAlgebra over S
the Sorts of F is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
C1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of B
G is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of F
I is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of B, the Sorts of F
I ** C1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of F
the carrier' of S is non empty set
sQ is Element of the carrier' of S
Args (sQ,B) is functional non empty Element of rng K158( the carrier of S, the Sorts of B)
K158( the carrier of S, the Sorts of B) is Relation-like K155( the carrier of S) -defined Function-like total set
K155( the carrier of S) is M8( the carrier of S)
rng K158( the carrier of S, the Sorts of B) is set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the Arity of S * K158( the carrier of S, the Sorts of B) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of B)) . sQ is set
the_result_sort_of sQ is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S . sQ is Element of the carrier of S
I . (the_result_sort_of sQ) is Relation-like the Sorts of B . (the_result_sort_of sQ) -defined the Sorts of F . (the_result_sort_of sQ) -valued Function-like non empty total V18( the Sorts of B . (the_result_sort_of sQ), the Sorts of F . (the_result_sort_of sQ)) Element of bool [:( the Sorts of B . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):]
the Sorts of B . (the_result_sort_of sQ) is non empty set
the Sorts of F . (the_result_sort_of sQ) is non empty set
[:( the Sorts of B . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):] is Relation-like set
bool [:( the Sorts of B . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):] is set
Den (sQ,B) is Relation-like Args (sQ,B) -defined Result (sQ,B) -valued Function-like non empty total V18( Args (sQ,B), Result (sQ,B)) Element of bool [:(Args (sQ,B)),(Result (sQ,B)):]
Result (sQ,B) is non empty Element of rng the Sorts of B
rng the Sorts of B is non empty with_non-empty_elements set
the ResultSort of S * the Sorts of B is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of B) . sQ is non empty set
[:(Args (sQ,B)),(Result (sQ,B)):] is Relation-like set
bool [:(Args (sQ,B)),(Result (sQ,B)):] is set
the Charact of B is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of B), the ResultSort of S * the Sorts of B
the Charact of B . sQ is set
Den (sQ,F) is Relation-like Args (sQ,F) -defined Result (sQ,F) -valued Function-like non empty total V18( Args (sQ,F), Result (sQ,F)) Element of bool [:(Args (sQ,F)),(Result (sQ,F)):]
Args (sQ,F) is functional non empty Element of rng K158( the carrier of S, the Sorts of F)
K158( the carrier of S, the Sorts of F) is Relation-like K155( the carrier of S) -defined Function-like total set
rng K158( the carrier of S, the Sorts of F) is set
the Arity of S * K158( the carrier of S, the Sorts of F) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of F)) . sQ is set
Result (sQ,F) is non empty Element of rng the Sorts of F
rng the Sorts of F is non empty with_non-empty_elements set
the ResultSort of S * the Sorts of F is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of F) . sQ is non empty set
[:(Args (sQ,F)),(Result (sQ,F)):] is Relation-like set
bool [:(Args (sQ,F)),(Result (sQ,F)):] is set
the Charact of F is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of F), the ResultSort of S * the Sorts of F
the Charact of F . sQ is set
sF is Relation-like Function-like FinSequence-like Element of Args (sQ,B)
(Den (sQ,B)) . sF is set
(I . (the_result_sort_of sQ)) . ((Den (sQ,B)) . sF) is set
I # sF is Relation-like Function-like FinSequence-like Element of Args (sQ,F)
(Den (sQ,F)) . (I # sF) is set
Args (sQ,A) is functional non empty Element of rng K158( the carrier of S, the Sorts of A)
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
rng K158( the carrier of S, the Sorts of A) is set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of A)) . sQ is set
C12 is Relation-like Function-like FinSequence-like Element of Args (sQ,A)
C1 # C12 is Relation-like Function-like FinSequence-like Element of Args (sQ,B)
C1 . (the_result_sort_of sQ) is Relation-like the Sorts of A . (the_result_sort_of sQ) -defined the Sorts of B . (the_result_sort_of sQ) -valued Function-like non empty total V18( the Sorts of A . (the_result_sort_of sQ), the Sorts of B . (the_result_sort_of sQ)) Element of bool [:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of B . (the_result_sort_of sQ)):]
the Sorts of A . (the_result_sort_of sQ) is non empty set
[:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of B . (the_result_sort_of sQ)):] is Relation-like set
bool [:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of B . (the_result_sort_of sQ)):] is set
Result (sQ,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty with_non-empty_elements set
the ResultSort of S * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of A) . sQ is non empty set
Den (sQ,A) is Relation-like Args (sQ,A) -defined Result (sQ,A) -valued Function-like non empty total V18( Args (sQ,A), Result (sQ,A)) Element of bool [:(Args (sQ,A)),(Result (sQ,A)):]
[:(Args (sQ,A)),(Result (sQ,A)):] is Relation-like set
bool [:(Args (sQ,A)),(Result (sQ,A)):] is set
the Charact of A is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of A), the ResultSort of S * the Sorts of A
the Charact of A . sQ is set
(Den (sQ,A)) . C12 is Element of Result (sQ,A)
(C1 . (the_result_sort_of sQ)) . ((Den (sQ,A)) . C12) is set
(Den (sQ,B)) . sF is Element of Result (sQ,B)
G . (the_result_sort_of sQ) is Relation-like the Sorts of A . (the_result_sort_of sQ) -defined the Sorts of F . (the_result_sort_of sQ) -valued Function-like non empty total V18( the Sorts of A . (the_result_sort_of sQ), the Sorts of F . (the_result_sort_of sQ)) Element of bool [:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):]
[:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):] is Relation-like set
bool [:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):] is set
(G . (the_result_sort_of sQ)) . ((Den (sQ,A)) . C12) is set
(I . (the_result_sort_of sQ)) * (C1 . (the_result_sort_of sQ)) is Relation-like the Sorts of A . (the_result_sort_of sQ) -defined the Sorts of F . (the_result_sort_of sQ) -valued Function-like non empty total V18( the Sorts of A . (the_result_sort_of sQ), the Sorts of F . (the_result_sort_of sQ)) Element of bool [:( the Sorts of A . (the_result_sort_of sQ)),( the Sorts of F . (the_result_sort_of sQ)):]
((I . (the_result_sort_of sQ)) * (C1 . (the_result_sort_of sQ))) . ((Den (sQ,A)) . C12) is set
(I . (the_result_sort_of sQ)) . ((Den (sQ,B)) . sF) is set
(I ** C1) # C12 is Relation-like Function-like FinSequence-like Element of Args (sQ,F)
(Den (sQ,F)) . ((I ** C1) # C12) is Element of Result (sQ,F)
(Den (sQ,F)) . (I # sF) is Element of Result (sQ,F)
S is set
A is Relation-like S -defined Function-like total set
B is Relation-like non-empty S -defined Function-like total set
F is Relation-like non-empty S -defined Function-like total set
[|B,F|] is Relation-like non-empty S -defined Function-like total set
C1 is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,[|B,F|]
G is Relation-like S -defined Function-like total set
I is set
G . I is set
A . I is set
B . I is set
[:(A . I),(B . I):] is Relation-like set
bool [:(A . I),(B . I):] is set
C1 . I is Relation-like Function-like set
pr1 (C1 . I) is Relation-like Function-like set
[|B,F|] . I is set
[:(A . I),([|B,F|] . I):] is Relation-like set
bool [:(A . I),([|B,F|] . I):] is set
sF is Relation-like Function-like set
rng sF is set
sQ is non empty set
C12 is set
dom sF is set
H is set
sF . H is set
dom (C1 . I) is set
(C1 . I) . H is set
((C1 . I) . H) `1 is set
rng (C1 . I) is set
F . I is set
[:(B . I),(F . I):] is Relation-like set
dom (C1 . I) is set
dom sF is set
I is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,B
sQ is set
I . sQ is Relation-like Function-like set
C1 . sQ is Relation-like Function-like set
pr1 (C1 . sQ) is Relation-like Function-like set
G is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,B
I is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,B
sQ is set
G . sQ is Relation-like Function-like set
C1 . sQ is Relation-like Function-like set
pr1 (C1 . sQ) is Relation-like Function-like set
I . sQ is Relation-like Function-like set
G is Relation-like S -defined Function-like total set
I is set
G . I is set
A . I is set
F . I is set
[:(A . I),(F . I):] is Relation-like set
bool [:(A . I),(F . I):] is set
C1 . I is Relation-like Function-like set
pr2 (C1 . I) is Relation-like Function-like set
[|B,F|] . I is set
[:(A . I),([|B,F|] . I):] is Relation-like set
bool [:(A . I),([|B,F|] . I):] is set
sF is Relation-like Function-like set
rng sF is set
sQ is non empty set
C12 is set
dom sF is set
H is set
sF . H is set
dom (C1 . I) is set
(C1 . I) . H is set
((C1 . I) . H) `2 is set
rng (C1 . I) is set
B . I is set
[:(B . I),(F . I):] is Relation-like set
dom (C1 . I) is set
dom sF is set
I is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,F
sQ is set
I . sQ is Relation-like Function-like set
C1 . sQ is Relation-like Function-like set
pr2 (C1 . sQ) is Relation-like Function-like set
G is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,F
I is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,F
sQ is set
G . sQ is Relation-like Function-like set
C1 . sQ is Relation-like Function-like set
pr2 (C1 . sQ) is Relation-like Function-like set
I . sQ is Relation-like Function-like set
S is set
A is set
{A} is non empty finite countable set
S --> {A} is Relation-like non-empty S -defined {{A}} -valued Function-like constant total V18(S,{{A}}) Element of bool [:S,{{A}}:]
{{A}} is non empty finite V35() countable set
[:S,{{A}}:] is Relation-like set
bool [:S,{{A}}:] is set
[|(S --> {A}),(S --> {A})|] is Relation-like non-empty S -defined Function-like total set
B is Relation-like S -defined Function-like total set
F is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of B,[|(S --> {A}),(S --> {A})|]
(S,B,(S --> {A}),(S --> {A}),F) is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of B,S --> {A}
(S,B,(S --> {A}),(S --> {A}),F) is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of B,S --> {A}
C1 is set
F . C1 is Relation-like Function-like set
pr2 (F . C1) is Relation-like Function-like set
dom (pr2 (F . C1)) is set
dom (F . C1) is set
G is set
(F . C1) . G is set
rng (F . C1) is set
B . C1 is set
[|(S --> {A}),(S --> {A})|] . C1 is set
[:(B . C1),([|(S --> {A}),(S --> {A})|] . C1):] is Relation-like set
bool [:(B . C1),([|(S --> {A}),(S --> {A})|] . C1):] is set
(S --> {A}) . C1 is set
[:((S --> {A}) . C1),((S --> {A}) . C1):] is Relation-like set
((F . C1) . G) `1 is set
((F . C1) . G) `2 is set
(pr2 (F . C1)) . G is set
(S,B,(S --> {A}),(S --> {A}),F) . C1 is Relation-like Function-like set
pr1 (F . C1) is Relation-like Function-like set
(S,B,(S --> {A}),(S --> {A}),F) . C1 is Relation-like Function-like set
S is set
A is Relation-like S -defined Function-like total set
B is Relation-like non-empty S -defined Function-like total set
F is Relation-like non-empty S -defined Function-like total set
[|B,F|] is Relation-like non-empty S -defined Function-like total set
C1 is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,[|B,F|]
(S,A,B,F,C1) is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,B
G is set
(S,A,B,F,C1) . G is Relation-like Function-like set
rng ((S,A,B,F,C1) . G) is set
B . G is set
A . G is set
[:(A . G),(B . G):] is Relation-like set
bool [:(A . G),(B . G):] is set
I is Relation-like A . G -defined B . G -valued Function-like V18(A . G,B . G) Element of bool [:(A . G),(B . G):]
rng I is Element of bool (B . G)
bool (B . G) is set
sQ is set
[|B,F|] . G is set
sF is set
sF `2 is set
[sQ,(sF `2)] is V15() set
{sQ,(sF `2)} is non empty finite countable set
{sQ} is non empty finite countable set
{{sQ,(sF `2)},{sQ}} is non empty finite V35() countable set
F . G is set
[:(B . G),(F . G):] is Relation-like set
[sQ,(sF `2)] `2 is set
[sQ,(sF `2)] `1 is set
dom I is Element of bool (A . G)
bool (A . G) is set
C1 . G is Relation-like Function-like set
[:(A . G),([|B,F|] . G):] is Relation-like set
bool [:(A . G),([|B,F|] . G):] is set
dom (C1 . G) is set
rng (C1 . G) is set
H is set
(C1 . G) . H is set
I . H is set
pr1 (C1 . G) is Relation-like Function-like set
(pr1 (C1 . G)) . H is set
S is set
A is Relation-like S -defined Function-like total set
B is Relation-like non-empty S -defined Function-like total set
F is Relation-like non-empty S -defined Function-like total set
[|B,F|] is Relation-like non-empty S -defined Function-like total set
C1 is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,[|B,F|]
(S,A,B,F,C1) is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,F
G is set
(S,A,B,F,C1) . G is Relation-like Function-like set
rng ((S,A,B,F,C1) . G) is set
F . G is set
A . G is set
[:(A . G),(F . G):] is Relation-like set
bool [:(A . G),(F . G):] is set
I is Relation-like A . G -defined F . G -valued Function-like V18(A . G,F . G) Element of bool [:(A . G),(F . G):]
rng I is Element of bool (F . G)
bool (F . G) is set
sQ is set
[|B,F|] . G is set
sF is set
sF `1 is set
[(sF `1),sQ] is V15() set
{(sF `1),sQ} is non empty finite countable set
{(sF `1)} is non empty finite countable set
{{(sF `1),sQ},{(sF `1)}} is non empty finite V35() countable set
B . G is set
[:(B . G),(F . G):] is Relation-like set
[(sF `1),sQ] `1 is set
[(sF `1),sQ] `2 is set
dom I is Element of bool (A . G)
bool (A . G) is set
C1 . G is Relation-like Function-like set
[:(A . G),([|B,F|] . G):] is Relation-like set
bool [:(A . G),([|B,F|] . G):] is set
dom (C1 . G) is set
rng (C1 . G) is set
H is set
(C1 . G) . H is set
I . H is set
pr2 (C1 . G) is Relation-like Function-like set
(pr2 (C1 . G)) . H is set
S is set
A is Relation-like S -defined Function-like total set
B is Relation-like S -defined Function-like total set
F is Relation-like non-empty S -defined Function-like total set
C1 is Relation-like non-empty S -defined Function-like total set
[|F,C1|] is Relation-like non-empty S -defined Function-like total set
G is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,[|F,C1|]
doms G is Relation-like S -defined Function-like total set
G .. B is Relation-like S -defined Function-like total set
(S,A,F,C1,G) is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,F
(S,A,F,C1,G) .. B is Relation-like S -defined Function-like total set
(S,A,F,C1,G) is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,C1
(S,A,F,C1,G) .. B is Relation-like S -defined Function-like total set
I is set
(G .. B) . I is set
((S,A,F,C1,G) .. B) . I is set
((S,A,F,C1,G) .. B) . I is set
[(((S,A,F,C1,G) .. B) . I),(((S,A,F,C1,G) .. B) . I)] is V15() set
{(((S,A,F,C1,G) .. B) . I),(((S,A,F,C1,G) .. B) . I)} is non empty finite countable set
{(((S,A,F,C1,G) .. B) . I)} is non empty finite countable set
{{(((S,A,F,C1,G) .. B) . I),(((S,A,F,C1,G) .. B) . I)},{(((S,A,F,C1,G) .. B) . I)}} is non empty finite V35() countable set
B . I is set
(doms G) . I is set
G . I is Relation-like Function-like set
dom (G . I) is set
sQ is set
[|F,C1|] . sQ is set
A . sQ is set
[|F,C1|] . I is set
F . I is set
C1 . I is set
[:(F . I),(C1 . I):] is Relation-like set
(G . I) . (B . I) is set
(S,A,F,C1,G) . I is Relation-like Function-like set
pr2 (G . I) is Relation-like Function-like set
(pr2 (G . I)) . (B . I) is set
((G . I) . (B . I)) `2 is set
(S,A,F,C1,G) . I is Relation-like Function-like set
pr1 (G . I) is Relation-like Function-like set
(pr1 (G . I)) . (B . I) is set
((G . I) . (B . I)) `1 is set
S is non empty V54() ManySortedSign
Trivial_Algebra S is strict MSAlgebra over S
the Sorts of (Trivial_Algebra S) is Relation-like the carrier of S -defined Function-like non empty total set
the carrier of S is non empty set
0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() finite finite-yielding V35() Function-yielding Relation-yielding Cardinal-yielding countable Element of NAT
{0} is functional non empty finite V35() with_common_domain countable set
the carrier of S --> {0} is Relation-like non-empty non empty-yielding the carrier of S -defined {{0}} -valued Function-like constant non empty total V18( the carrier of S,{{0}}) Element of bool [: the carrier of S,{{0}}:]
{{0}} is non empty finite V35() countable set
[: the carrier of S,{{0}}:] is Relation-like set
bool [: the carrier of S,{{0}}:] is set
A is Relation-like the carrier of S -defined Function-like non empty total set
{A} is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set
S is non empty V54() ManySortedSign
Trivial_Algebra S is strict MSAlgebra over S
the Sorts of (Trivial_Algebra S) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set
the carrier of S is non empty set
A is set
the Sorts of (Trivial_Algebra S) . A is finite countable set
0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() finite finite-yielding V35() Function-yielding Relation-yielding Cardinal-yielding countable Element of NAT
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
Trivial_Algebra S is strict non-empty finite-yielding MSAlgebra over S
the Sorts of (Trivial_Algebra S) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set
the carrier' of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S)
F is Element of the carrier' of S
Args (F,A) is functional non empty Element of rng K158( the carrier of S, the Sorts of A)
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
K155( the carrier of S) is M8( the carrier of S)
rng K158( the carrier of S, the Sorts of A) is set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of A)) . F is set
the_result_sort_of F is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S . F is Element of the carrier of S
B . (the_result_sort_of F) is Relation-like the Sorts of A . (the_result_sort_of F) -defined the Sorts of (Trivial_Algebra S) . (the_result_sort_of F) -valued Function-like non empty total V18( the Sorts of A . (the_result_sort_of F), the Sorts of (Trivial_Algebra S) . (the_result_sort_of F)) Element of bool [:( the Sorts of A . (the_result_sort_of F)),( the Sorts of (Trivial_Algebra S) . (the_result_sort_of F)):]
the Sorts of A . (the_result_sort_of F) is non empty set
the Sorts of (Trivial_Algebra S) . (the_result_sort_of F) is non empty finite countable set
[:( the Sorts of A . (the_result_sort_of F)),( the Sorts of (Trivial_Algebra S) . (the_result_sort_of F)):] is Relation-like set
bool [:( the Sorts of A . (the_result_sort_of F)),( the Sorts of (Trivial_Algebra S) . (the_result_sort_of F)):] is set
Result (F,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty with_non-empty_elements set
the ResultSort of S * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of A) . F is non empty set
Den (F,A) is Relation-like Args (F,A) -defined Result (F,A) -valued Function-like non empty total V18( Args (F,A), Result (F,A)) Element of bool [:(Args (F,A)),(Result (F,A)):]
[:(Args (F,A)),(Result (F,A)):] is Relation-like set
bool [:(Args (F,A)),(Result (F,A)):] is set
the Charact of A is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of A), the ResultSort of S * the Sorts of A
the Charact of A . F is set
Args (F,(Trivial_Algebra S)) is functional non empty Element of rng K158( the carrier of S, the Sorts of (Trivial_Algebra S))
K158( the carrier of S, the Sorts of (Trivial_Algebra S)) is Relation-like K155( the carrier of S) -defined Function-like total set
rng K158( the carrier of S, the Sorts of (Trivial_Algebra S)) is set
the Arity of S * K158( the carrier of S, the Sorts of (Trivial_Algebra S)) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of (Trivial_Algebra S))) . F is set
Result (F,(Trivial_Algebra S)) is non empty finite countable Element of rng the Sorts of (Trivial_Algebra S)
rng the Sorts of (Trivial_Algebra S) is non empty V35() with_non-empty_elements set
the ResultSort of S * the Sorts of (Trivial_Algebra S) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of (Trivial_Algebra S)) . F is non empty set
Den (F,(Trivial_Algebra S)) is Relation-like Args (F,(Trivial_Algebra S)) -defined Result (F,(Trivial_Algebra S)) -valued Function-like non empty total V18( Args (F,(Trivial_Algebra S)), Result (F,(Trivial_Algebra S))) Element of bool [:(Args (F,(Trivial_Algebra S))),(Result (F,(Trivial_Algebra S))):]
[:(Args (F,(Trivial_Algebra S))),(Result (F,(Trivial_Algebra S))):] is Relation-like set
bool [:(Args (F,(Trivial_Algebra S))),(Result (F,(Trivial_Algebra S))):] is set
the Charact of (Trivial_Algebra S) is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of (Trivial_Algebra S)), the ResultSort of S * the Sorts of (Trivial_Algebra S)
the Charact of (Trivial_Algebra S) . F is set
C1 is Relation-like Function-like FinSequence-like Element of Args (F,A)
(Den (F,A)) . C1 is Element of Result (F,A)
(B . (the_result_sort_of F)) . ((Den (F,A)) . C1) is set
B # C1 is Relation-like Function-like FinSequence-like Element of Args (F,(Trivial_Algebra S))
(Den (F,(Trivial_Algebra S))) . (B # C1) is Element of Result (F,(Trivial_Algebra S))
H is set
the Sorts of (Trivial_Algebra S) . H is finite countable set
{0} is functional non empty finite V35() with_common_domain countable set
the carrier of S --> {0} is Relation-like non-empty non empty-yielding the carrier of S -defined {{0}} -valued Function-like constant non empty total V18( the carrier of S,{{0}}) Element of bool [: the carrier of S,{{0}}:]
{{0}} is non empty finite V35() countable set
[: the carrier of S,{{0}}:] is Relation-like set
bool [: the carrier of S,{{0}}:] is set
s is Relation-like the carrier of S -defined Function-like non empty total set
{s} is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set
i is Element of the Sorts of A . (the_result_sort_of F)
(B . (the_result_sort_of F)) . i is Element of the Sorts of (Trivial_Algebra S) . (the_result_sort_of F)
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
Trivial_Algebra S is strict non-empty finite-yielding MSAlgebra over S
the Sorts of (Trivial_Algebra S) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S)
{0} is functional non empty finite V35() with_common_domain countable set
the carrier of S --> {0} is Relation-like non-empty non empty-yielding the carrier of S -defined {{0}} -valued Function-like constant non empty total V18( the carrier of S,{{0}}) Element of bool [: the carrier of S,{{0}}:]
{{0}} is non empty finite V35() countable set
[: the carrier of S,{{0}}:] is Relation-like set
bool [: the carrier of S,{{0}}:] is set
C1 is Relation-like the carrier of S -defined Function-like non empty total set
{C1} is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set
the carrier' of S is non empty set
G is Element of the carrier' of S
Args (G,A) is functional non empty Element of rng K158( the carrier of S, the Sorts of A)
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
K155( the carrier of S) is M8( the carrier of S)
rng K158( the carrier of S, the Sorts of A) is set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of A)) . G is set
the_result_sort_of G is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S . G is Element of the carrier of S
B . (the_result_sort_of G) is Relation-like the Sorts of A . (the_result_sort_of G) -defined the Sorts of (Trivial_Algebra S) . (the_result_sort_of G) -valued Function-like non empty total V18( the Sorts of A . (the_result_sort_of G), the Sorts of (Trivial_Algebra S) . (the_result_sort_of G)) Element of bool [:( the Sorts of A . (the_result_sort_of G)),( the Sorts of (Trivial_Algebra S) . (the_result_sort_of G)):]
the Sorts of A . (the_result_sort_of G) is non empty set
the Sorts of (Trivial_Algebra S) . (the_result_sort_of G) is non empty finite countable set
[:( the Sorts of A . (the_result_sort_of G)),( the Sorts of (Trivial_Algebra S) . (the_result_sort_of G)):] is Relation-like set
bool [:( the Sorts of A . (the_result_sort_of G)),( the Sorts of (Trivial_Algebra S) . (the_result_sort_of G)):] is set
Den (G,A) is Relation-like Args (G,A) -defined Result (G,A) -valued Function-like non empty total V18( Args (G,A), Result (G,A)) Element of bool [:(Args (G,A)),(Result (G,A)):]
Result (G,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty with_non-empty_elements set
the ResultSort of S * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of A) . G is non empty set
[:(Args (G,A)),(Result (G,A)):] is Relation-like set
bool [:(Args (G,A)),(Result (G,A)):] is set
the Charact of A is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of A), the ResultSort of S * the Sorts of A
the Charact of A . G is set
Den (G,(Trivial_Algebra S)) is Relation-like Args (G,(Trivial_Algebra S)) -defined Result (G,(Trivial_Algebra S)) -valued Function-like non empty total V18( Args (G,(Trivial_Algebra S)), Result (G,(Trivial_Algebra S))) Element of bool [:(Args (G,(Trivial_Algebra S))),(Result (G,(Trivial_Algebra S))):]
Args (G,(Trivial_Algebra S)) is functional non empty Element of rng K158( the carrier of S, the Sorts of (Trivial_Algebra S))
K158( the carrier of S, the Sorts of (Trivial_Algebra S)) is Relation-like K155( the carrier of S) -defined Function-like total set
rng K158( the carrier of S, the Sorts of (Trivial_Algebra S)) is set
the Arity of S * K158( the carrier of S, the Sorts of (Trivial_Algebra S)) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of (Trivial_Algebra S))) . G is set
Result (G,(Trivial_Algebra S)) is non empty finite countable Element of rng the Sorts of (Trivial_Algebra S)
rng the Sorts of (Trivial_Algebra S) is non empty V35() with_non-empty_elements set
the ResultSort of S * the Sorts of (Trivial_Algebra S) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of (Trivial_Algebra S)) . G is non empty set
[:(Args (G,(Trivial_Algebra S))),(Result (G,(Trivial_Algebra S))):] is Relation-like set
bool [:(Args (G,(Trivial_Algebra S))),(Result (G,(Trivial_Algebra S))):] is set
the Charact of (Trivial_Algebra S) is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of (Trivial_Algebra S)), the ResultSort of S * the Sorts of (Trivial_Algebra S)
the Charact of (Trivial_Algebra S) . G is set
I is Relation-like Function-like FinSequence-like Element of Args (G,A)
(Den (G,A)) . I is set
(B . (the_result_sort_of G)) . ((Den (G,A)) . I) is set
B # I is Relation-like Function-like FinSequence-like Element of Args (G,(Trivial_Algebra S))
(Den (G,(Trivial_Algebra S))) . (B # I) is set
(Den (G,A)) . I is Element of Result (G,A)
(B . (the_result_sort_of G)) . ((Den (G,A)) . I) is set
(Den (G,(Trivial_Algebra S))) . (B # I) is Element of Result (G,(Trivial_Algebra S))
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
Trivial_Algebra S is strict non-empty finite-yielding MSAlgebra over S
A is MSAlgebra over S
the Sorts of A is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of (Trivial_Algebra S) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set
G is Relation-like the carrier of S -defined Function-like non empty total set
{G} is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set
G is Relation-like the carrier of S -defined Function-like non empty total set
{G} is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set
the Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S)
sQ is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of {G}, the Sorts of (Trivial_Algebra S)
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
[| the Sorts of A, the Sorts of A|] is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is Relation-like the carrier of S -defined Function-like non empty total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
C1 is set
B . C1 is set
[| the Sorts of A, the Sorts of A|] . C1 is set
the Sorts of A . C1 is set
[:( the Sorts of A . C1),( the Sorts of A . C1):] is Relation-like set
bool [:( the Sorts of A . C1),( the Sorts of A . C1):] is set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
CongrLatt A is non empty V65() V72() V77() M15( EqRelLatt the Sorts of A)
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
EqRelLatt the Sorts of A is non empty V65() V72() L9()
the carrier of (CongrLatt A) is non empty set
bool the carrier of (CongrLatt A) is set
[| the Sorts of A, the Sorts of A|] is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
Bool [| the Sorts of A, the Sorts of A|] is functional non empty with_common_domain set
bool (Bool [| the Sorts of A, the Sorts of A|]) is set
B is Element of bool the carrier of (CongrLatt A)
F is functional with_common_domain Element of bool (Bool [| the Sorts of A, the Sorts of A|])
|:F:| is Relation-like the carrier of S -defined Function-like non empty total ManySortedSubset of K261( the carrier of S,[| the Sorts of A, the Sorts of A|])
K261( the carrier of S,[| the Sorts of A, the Sorts of A|]) is Relation-like the carrier of S -defined Function-like non empty total set
meet |:F:| is Relation-like the carrier of S -defined Function-like non empty total ManySortedSubset of [| the Sorts of A, the Sorts of A|]
sQ is functional non empty with_common_domain Element of bool (Bool [| the Sorts of A, the Sorts of A|])
the carrier of (EqRelLatt the Sorts of A) is non empty set
sF is set
sF is Relation-like the carrier of S -defined Function-like non empty total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
C12 is set
the Sorts of A . C12 is set
[:( the Sorts of A . C12),( the Sorts of A . C12):] is Relation-like set
bool [:( the Sorts of A . C12),( the Sorts of A . C12):] is set
sF . C12 is set
H is Relation-like the Sorts of A . C12 -defined the Sorts of A . C12 -valued Element of bool [:( the Sorts of A . C12),( the Sorts of A . C12):]
the carrier' of S is non empty set
H is Element of the carrier' of S
Args (H,A) is functional non empty Element of rng K158( the carrier of S, the Sorts of A)
K158( the carrier of S, the Sorts of A) is Relation-like K155( the carrier of S) -defined Function-like total set
K155( the carrier of S) is M8( the carrier of S)
rng K158( the carrier of S, the Sorts of A) is set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
the Arity of S * K158( the carrier of S, the Sorts of A) is Relation-like the carrier' of S -defined Function-like set
( the Arity of S * K158( the carrier of S, the Sorts of A)) . H is set
i is Relation-like Function-like FinSequence-like Element of Args (H,A)
dom i is countable Element of bool NAT
s is Relation-like Function-like FinSequence-like Element of Args (H,A)
C12 is Relation-like the carrier of S -defined Function-like non empty total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
the_arity_of H is Relation-like NAT -defined the carrier of S -valued Function-like FinSequence-like M9( the carrier of S,K155( the carrier of S))
the Arity of S . H is Element of K155( the carrier of S)
the_result_sort_of H is Element of the carrier of S
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S . H is Element of the carrier of S
[| the Sorts of A, the Sorts of A|] . (the_result_sort_of H) is non empty set
bool ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of H)) is set
bool (bool ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of H))) is set
|:sQ:| is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total ManySortedSubset of K261( the carrier of S,[| the Sorts of A, the Sorts of A|])
|:sQ:| . (the_result_sort_of H) is non empty Element of bool (bool ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of H)))
C12 . (the_result_sort_of H) is Relation-like the Sorts of A . (the_result_sort_of H) -defined the Sorts of A . (the_result_sort_of H) -valued total V18( the Sorts of A . (the_result_sort_of H), the Sorts of A . (the_result_sort_of H)) symmetric transitive Element of bool [:( the Sorts of A . (the_result_sort_of H)),( the Sorts of A . (the_result_sort_of H)):]
the Sorts of A . (the_result_sort_of H) is non empty set
[:( the Sorts of A . (the_result_sort_of H)),( the Sorts of A . (the_result_sort_of H)):] is Relation-like set
bool [:( the Sorts of A . (the_result_sort_of H)),( the Sorts of A . (the_result_sort_of H)):] is set
f is Element of bool (bool ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of H)))
Intersect f is Element of bool ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of H))
Bool [| the Sorts of A, the Sorts of A|] is functional non empty with_common_domain V139( the carrier of S,[| the Sorts of A, the Sorts of A|]) V140( the carrier of S,[| the Sorts of A, the Sorts of A|]) V141( the carrier of S,[| the Sorts of A, the Sorts of A|]) V142( the carrier of S,[| the Sorts of A, the Sorts of A|]) V143( the carrier of S,[| the Sorts of A, the Sorts of A|]) V144( the carrier of S,[| the Sorts of A, the Sorts of A|]) Element of bool (Bool [| the Sorts of A, the Sorts of A|])
{ (b1 . (the_result_sort_of H)) where b1 is Relation-like the carrier of S -defined Function-like non empty total Element of Bool [| the Sorts of A, the Sorts of A|] : b1 in sQ } is set
s is set
x1 is Relation-like the carrier of S -defined Function-like non empty total Element of Bool [| the Sorts of A, the Sorts of A|]
x1 . (the_result_sort_of H) is set
n is V24() V25() V26() V30() set
(the_arity_of H) /. n is Element of the carrier of S
[| the Sorts of A, the Sorts of A|] . ((the_arity_of H) /. n) is non empty set
bool ([| the Sorts of A, the Sorts of A|] . ((the_arity_of H) /. n)) is set
bool (bool ([| the Sorts of A, the Sorts of A|] . ((the_arity_of H) /. n))) is set
|:sQ:| . ((the_arity_of H) /. n) is non empty Element of bool (bool ([| the Sorts of A, the Sorts of A|] . ((the_arity_of H) /. n)))
C12 . ((the_arity_of H) /. n) is Relation-like the Sorts of A . ((the_arity_of H) /. n) -defined the Sorts of A . ((the_arity_of H) /. n) -valued total V18( the Sorts of A . ((the_arity_of H) /. n), the Sorts of A . ((the_arity_of H) /. n)) symmetric transitive Element of bool [:( the Sorts of A . ((the_arity_of H) /. n)),( the Sorts of A . ((the_arity_of H) /. n)):]
the Sorts of A . ((the_arity_of H) /. n) is non empty set
[:( the Sorts of A . ((the_arity_of H) /. n)),( the Sorts of A . ((the_arity_of H) /. n)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of H) /. n)),( the Sorts of A . ((the_arity_of H) /. n)):] is set
G is Element of bool (bool ([| the Sorts of A, the Sorts of A|] . ((the_arity_of H) /. n)))
Intersect G is Element of bool ([| the Sorts of A, the Sorts of A|] . ((the_arity_of H) /. n))
{ (b1 . ((the_arity_of H) /. n)) where b1 is Relation-like the carrier of S -defined Function-like non empty total Element of Bool [| the Sorts of A, the Sorts of A|] : b1 in sQ } is set
s is Relation-like the carrier of S -defined Function-like non empty total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
s . ((the_arity_of H) /. n) is Relation-like the Sorts of A . ((the_arity_of H) /. n) -defined the Sorts of A . ((the_arity_of H) /. n) -valued total V18( the Sorts of A . ((the_arity_of H) /. n), the Sorts of A . ((the_arity_of H) /. n)) symmetric transitive Element of bool [:( the Sorts of A . ((the_arity_of H) /. n)),( the Sorts of A . ((the_arity_of H) /. n)):]
i . n is set
s . n is set
[(i . n),(s . n)] is V15() set
{(i . n),(s . n)} is non empty finite countable set
{(i . n)} is non empty finite countable set
{{(i . n),(s . n)},{(i . n)}} is non empty finite V35() countable set
meet G is Element of bool ([| the Sorts of A, the Sorts of A|] . ((the_arity_of H) /. n))
Result (H,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty with_non-empty_elements set
the ResultSort of S * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
( the ResultSort of S * the Sorts of A) . H is non empty set
Den (H,A) is Relation-like Args (H,A) -defined Result (H,A) -valued Function-like non empty total V18( Args (H,A), Result (H,A)) Element of bool [:(Args (H,A)),(Result (H,A)):]
[:(Args (H,A)),(Result (H,A)):] is Relation-like set
bool [:(Args (H,A)),(Result (H,A)):] is set
the Charact of A is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S, the Sorts of A), the ResultSort of S * the Sorts of A
the Charact of A . H is set
(Den (H,A)) . i is Element of Result (H,A)
(Den (H,A)) . s is Element of Result (H,A)
[((Den (H,A)) . i),((Den (H,A)) . s)] is V15() set
{((Den (H,A)) . i),((Den (H,A)) . s)} is non empty finite countable set
{((Den (H,A)) . i)} is non empty finite countable set
{{((Den (H,A)) . i),((Den (H,A)) . s)},{((Den (H,A)) . i)}} is non empty finite V35() countable set
meet f is Element of bool ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of H))
[[0]] the carrier of S is Relation-like non non-empty empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set
the carrier of S --> {} is Relation-like the carrier of S -defined {{}} -valued Function-like constant non empty total V18( the carrier of S,{{}}) Function-yielding Relation-yielding Element of bool [: the carrier of S,{{}}:]
[: the carrier of S,{{}}:] is Relation-like set
bool [: the carrier of S,{{}}:] is set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
[| the Sorts of A, the Sorts of A|] is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
{ the Sorts of A} is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total finite-yielding set
B is Relation-like the carrier of S -defined Function-like non empty total 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 S
Class B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
QuotCharact B is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,(Class B)), the ResultSort of S * (Class B)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
K155( the carrier of S) is M8( the carrier of S)
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
K158( the carrier of S,(Class B)) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,(Class B)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * (Class B) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (Class B),(QuotCharact B) #) is strict MSAlgebra over S
the Sorts of (QuotMSAlg (A,B)) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F is set
C1 is Element of the carrier of S
B . C1 is Relation-like the Sorts of A . C1 -defined the Sorts of A . C1 -valued total V18( the Sorts of A . C1, the Sorts of A . C1) symmetric transitive Element of bool [:( the Sorts of A . C1),( the Sorts of A . C1):]
the Sorts of A . C1 is non empty set
[:( the Sorts of A . C1),( the Sorts of A . C1):] is Relation-like set
bool [:( the Sorts of A . C1),( the Sorts of A . C1):] is set
nabla ( the Sorts of A . C1) is Relation-like the Sorts of A . C1 -defined the Sorts of A . C1 -valued total V18( the Sorts of A . C1, the Sorts of A . C1) reflexive symmetric transitive Element of bool [:( the Sorts of A . C1),( the Sorts of A . C1):]
the Sorts of (QuotMSAlg (A,B)) . F is set
Class (B . C1) is non empty with_non-empty_elements a_partition of the Sorts of A . C1
{( the Sorts of A . C1)} is non empty finite countable set
{ the Sorts of A} . F is finite countable set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is non-empty MSAlgebra over S
the Sorts of B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of B
MSCng F is Relation-like the carrier of S -defined Function-like non empty total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
QuotMSAlg (A,(MSCng F)) is strict non-empty MSAlgebra over S
Class (MSCng F) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
QuotCharact (MSCng F) is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,(Class (MSCng F))), the ResultSort of S * (Class (MSCng F))
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
K155( the carrier of S) is M8( the carrier of S)
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
K158( the carrier of S,(Class (MSCng F))) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,(Class (MSCng F))) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * (Class (MSCng F)) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (Class (MSCng F)),(QuotCharact (MSCng F)) #) is strict MSAlgebra over S
the Sorts of (QuotMSAlg (A,(MSCng F))) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
MSNat_Hom (A,(MSCng F)) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (QuotMSAlg (A,(MSCng F)))
MSHomQuot F is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (QuotMSAlg (A,(MSCng F))), the Sorts of B
(MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of B
C1 is set
G is Element of the carrier of S
(Class (MSCng F)) . G is non empty set
the Sorts of B . G is non empty set
[:((Class (MSCng F)) . G),( the Sorts of B . G):] is Relation-like set
bool [:((Class (MSCng F)) . G),( the Sorts of B . G):] is set
MSHomQuot (F,G) is Relation-like the Sorts of (QuotMSAlg (A,(MSCng F))) . G -defined the Sorts of B . G -valued Function-like non empty total V18( the Sorts of (QuotMSAlg (A,(MSCng F))) . G, the Sorts of B . G) Element of bool [:( the Sorts of (QuotMSAlg (A,(MSCng F))) . G),( the Sorts of B . G):]
the Sorts of (QuotMSAlg (A,(MSCng F))) . G is non empty set
[:( the Sorts of (QuotMSAlg (A,(MSCng F))) . G),( the Sorts of B . G):] is Relation-like set
bool [:( the Sorts of (QuotMSAlg (A,(MSCng F))) . G),( the Sorts of B . G):] is set
the Sorts of A . G is non empty set
[:( the Sorts of A . G),( the Sorts of B . G):] is Relation-like set
bool [:( the Sorts of A . G),( the Sorts of B . G):] is set
MSNat_Hom (A,(MSCng F),G) is Relation-like the Sorts of A . G -defined (Class (MSCng F)) . G -valued Function-like non empty total V18( the Sorts of A . G,(Class (MSCng F)) . G) Element of bool [:( the Sorts of A . G),((Class (MSCng F)) . G):]
[:( the Sorts of A . G),((Class (MSCng F)) . G):] is Relation-like set
bool [:( the Sorts of A . G),((Class (MSCng F)) . G):] is set
I is Relation-like (Class (MSCng F)) . G -defined the Sorts of B . G -valued Function-like non empty total V18((Class (MSCng F)) . G, the Sorts of B . G) Element of bool [:((Class (MSCng F)) . G),( the Sorts of B . G):]
I * (MSNat_Hom (A,(MSCng F),G)) is Relation-like the Sorts of A . G -defined the Sorts of B . G -valued Function-like non empty total V18( the Sorts of A . G, the Sorts of B . G) Element of bool [:( the Sorts of A . G),( the Sorts of B . G):]
sQ is Relation-like the Sorts of A . G -defined the Sorts of B . G -valued Function-like non empty total V18( the Sorts of A . G, the Sorts of B . G) Element of bool [:( the Sorts of A . G),( the Sorts of B . G):]
F . G is Relation-like the Sorts of A . G -defined the Sorts of B . G -valued Function-like non empty total V18( the Sorts of A . G, the Sorts of B . G) Element of bool [:( the Sorts of A . G),( the Sorts of B . G):]
sF is Element of the Sorts of A . G
sQ . sF is Element of the Sorts of B . G
(F . G) . sF is Element of the Sorts of B . G
(MSNat_Hom (A,(MSCng F),G)) . sF is Element of (Class (MSCng F)) . G
I . ((MSNat_Hom (A,(MSCng F),G)) . sF) is Element of the Sorts of B . G
(MSCng F) . G is Relation-like the Sorts of A . G -defined the Sorts of A . G -valued total V18( the Sorts of A . G, the Sorts of A . G) symmetric transitive Element of bool [:( the Sorts of A . G),( the Sorts of A . G):]
[:( the Sorts of A . G),( the Sorts of A . G):] is Relation-like set
bool [:( the Sorts of A . G),( the Sorts of A . G):] is set
Class (((MSCng F) . G),sF) is Element of bool ( the Sorts of A . G)
bool ( the Sorts of A . G) is set
I . (Class (((MSCng F) . G),sF)) is set
MSCng (F,G) is Relation-like the Sorts of A . G -defined the Sorts of A . G -valued total V18( the Sorts of A . G, the Sorts of A . G) symmetric transitive Element of bool [:( the Sorts of A . G),( the Sorts of A . G):]
Class ((MSCng (F,G)),sF) is Element of bool ( the Sorts of A . G)
I . (Class ((MSCng (F,G)),sF)) is set
((MSHomQuot F) ** (MSNat_Hom (A,(MSCng F)))) . C1 is Relation-like Function-like set
(MSNat_Hom (A,(MSCng F))) . G is Relation-like the Sorts of A . G -defined the Sorts of (QuotMSAlg (A,(MSCng F))) . G -valued Function-like non empty total V18( the Sorts of A . G, the Sorts of (QuotMSAlg (A,(MSCng F))) . G) Element of bool [:( the Sorts of A . G),( the Sorts of (QuotMSAlg (A,(MSCng F))) . G):]
[:( the Sorts of A . G),( the Sorts of (QuotMSAlg (A,(MSCng F))) . G):] is Relation-like set
bool [:( the Sorts of A . G),( the Sorts of (QuotMSAlg (A,(MSCng F))) . G):] is set
(MSHomQuot F) . G is Relation-like the Sorts of (QuotMSAlg (A,(MSCng F))) . G -defined the Sorts of B . G -valued Function-like non empty total V18( the Sorts of (QuotMSAlg (A,(MSCng F))) . G, the Sorts of B . G) Element of bool [:( the Sorts of (QuotMSAlg (A,(MSCng F))) . G),( the Sorts of B . G):]
((MSHomQuot F) . G) * ((MSNat_Hom (A,(MSCng F))) . G) is Relation-like the Sorts of A . G -defined the Sorts of B . G -valued Function-like non empty total V18( the Sorts of A . G, the Sorts of B . G) Element of bool [:( the Sorts of A . G),( the Sorts of B . G):]
(MSHomQuot (F,G)) * ((MSNat_Hom (A,(MSCng F))) . G) is Relation-like the Sorts of A . G -defined the Sorts of B . G -valued Function-like non empty total V18( the Sorts of A . G, the Sorts of B . G) Element of bool [:( the Sorts of A . G),( the Sorts of B . G):]
(MSHomQuot (F,G)) * (MSNat_Hom (A,(MSCng F),G)) is Relation-like the Sorts of A . G -defined the Sorts of B . G -valued Function-like Element of bool [:( the Sorts of A . G),( the Sorts of B . G):]
F . C1 is Relation-like Function-like set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is Relation-like the carrier of S -defined Function-like non empty total 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 S
Class B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
QuotCharact B is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,(Class B)), the ResultSort of S * (Class B)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
K155( the carrier of S) is M8( the carrier of S)
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
K158( the carrier of S,(Class B)) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,(Class B)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * (Class B) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (Class B),(QuotCharact B) #) is strict MSAlgebra over S
the Sorts of (QuotMSAlg (A,B)) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F is Element of the carrier of S
the Sorts of (QuotMSAlg (A,B)) . F is non empty set
the Sorts of A . F is non empty set
C1 is Element of the Sorts of (QuotMSAlg (A,B)) . F
(Class B) . F is non empty set
B . F is Relation-like the Sorts of A . F -defined the Sorts of A . F -valued total V18( the Sorts of A . F, the Sorts of A . F) symmetric transitive Element of bool [:( the Sorts of A . F),( the Sorts of A . F):]
[:( the Sorts of A . F),( the Sorts of A . F):] is Relation-like set
bool [:( the Sorts of A . F),( the Sorts of A . F):] is set
Class (B . F) is non empty with_non-empty_elements a_partition of the Sorts of A . F
G is set
Class ((B . F),G) is Element of bool ( the Sorts of A . F)
bool ( the Sorts of A . F) is set
I is Element of the Sorts of A . F
Class (B,I) is Element of bool ( the Sorts of A . F)
Class ((B . F),I) is Element of bool ( the Sorts of A . F)
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is MSAlgebra over S
the Sorts of A is Relation-like the carrier of S -defined Function-like non empty total set
B is Relation-like the carrier of S -defined Function-like non empty total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
F is Relation-like the carrier of S -defined Function-like non empty total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
C1 is Element of the carrier of S
the Sorts of A . C1 is set
B . C1 is Relation-like the Sorts of A . C1 -defined the Sorts of A . C1 -valued total V18( the Sorts of A . C1, the Sorts of A . C1) symmetric transitive Element of bool [:( the Sorts of A . C1),( the Sorts of A . C1):]
[:( the Sorts of A . C1),( the Sorts of A . C1):] is Relation-like set
bool [:( the Sorts of A . C1),( the Sorts of A . C1):] is set
G is Element of the Sorts of A . C1
I is Element of the Sorts of A . C1
[G,I] is V15() set
{G,I} is non empty finite countable set
{G} is non empty finite countable set
{{G,I},{G}} is non empty finite V35() countable set
Class (B,G) is Element of bool ( the Sorts of A . C1)
bool ( the Sorts of A . C1) is set
Class ((B . C1),G) is Element of bool ( the Sorts of A . C1)
Class (F,I) is Element of bool ( the Sorts of A . C1)
F . C1 is Relation-like the Sorts of A . C1 -defined the Sorts of A . C1 -valued total V18( the Sorts of A . C1, the Sorts of A . C1) symmetric transitive Element of bool [:( the Sorts of A . C1),( the Sorts of A . C1):]
Class ((F . C1),I) is Element of bool ( the Sorts of A . C1)
Class (B,I) is Element of bool ( the Sorts of A . C1)
Class ((B . C1),I) is Element of bool ( the Sorts of A . C1)
Class (F,G) is Element of bool ( the Sorts of A . C1)
Class ((F . C1),G) is Element of bool ( the Sorts of A . C1)
field (B . C1) is set
sQ is set
[sQ,G] is V15() set
{sQ,G} is non empty finite countable set
{sQ} is non empty finite countable set
{{sQ,G},{sQ}} is non empty finite V35() countable set
[sQ,I] is V15() set
{sQ,I} is non empty finite countable set
{{sQ,I},{sQ}} is non empty finite V35() countable set
sQ is non-empty MSAlgebra over S
the Sorts of sQ is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of sQ . C1 is non empty set
[I,G] is V15() set
{I,G} is non empty finite countable set
{I} is non empty finite countable set
{{I,G},{I}} is non empty finite V35() countable set
sF is set
[sF,I] is V15() set
{sF,I} is non empty finite countable set
{sF} is non empty finite countable set
{{sF,I},{sF}} is non empty finite V35() countable set
[sF,G] is V15() set
{sF,G} is non empty finite countable set
{{sF,G},{sF}} is non empty finite V35() countable set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is Relation-like the carrier of S -defined Function-like non empty total 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 S
Class B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
QuotCharact B is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,(Class B)), the ResultSort of S * (Class B)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
K155( the carrier of S) is M8( the carrier of S)
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
K158( the carrier of S,(Class B)) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,(Class B)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * (Class B) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (Class B),(QuotCharact B) #) is strict MSAlgebra over S
the Sorts of (QuotMSAlg (A,B)) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
MSNat_Hom (A,B) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (QuotMSAlg (A,B))
F is Element of the carrier of S
the Sorts of A . F is non empty set
the Sorts of (QuotMSAlg (A,B)) . F is non empty set
(MSNat_Hom (A,B)) . F is Relation-like the Sorts of A . F -defined the Sorts of (QuotMSAlg (A,B)) . F -valued Function-like non empty total V18( the Sorts of A . F, the Sorts of (QuotMSAlg (A,B)) . F) Element of bool [:( the Sorts of A . F),( the Sorts of (QuotMSAlg (A,B)) . F):]
[:( the Sorts of A . F),( the Sorts of (QuotMSAlg (A,B)) . F):] is Relation-like set
bool [:( the Sorts of A . F),( the Sorts of (QuotMSAlg (A,B)) . F):] is set
B . F is Relation-like the Sorts of A . F -defined the Sorts of A . F -valued total V18( the Sorts of A . F, the Sorts of A . F) symmetric transitive Element of bool [:( the Sorts of A . F),( the Sorts of A . F):]
[:( the Sorts of A . F),( the Sorts of A . F):] is Relation-like set
bool [:( the Sorts of A . F),( the Sorts of A . F):] is set
C1 is Element of the Sorts of A . F
((MSNat_Hom (A,B)) . F) . C1 is Element of the Sorts of (QuotMSAlg (A,B)) . F
G is Element of the Sorts of A . F
((MSNat_Hom (A,B)) . F) . G is Element of the Sorts of (QuotMSAlg (A,B)) . F
[C1,G] is V15() set
{C1,G} is non empty finite countable set
{C1} is non empty finite countable set
{{C1,G},{C1}} is non empty finite V35() countable set
MSNat_Hom (A,B,F) is Relation-like the Sorts of A . F -defined (Class B) . F -valued Function-like non empty total V18( the Sorts of A . F,(Class B) . F) Element of bool [:( the Sorts of A . F),((Class B) . F):]
(Class B) . F is non empty set
[:( the Sorts of A . F),((Class B) . F):] is Relation-like set
bool [:( the Sorts of A . F),((Class B) . F):] is set
Class ((B . F),C1) is Element of bool ( the Sorts of A . F)
bool ( the Sorts of A . F) is set
(MSNat_Hom (A,B,F)) . C1 is Element of (Class B) . F
Class ((B . F),G) is Element of bool ( the Sorts of A . F)
S is non empty non void V54() ManySortedSign
A is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is Relation-like the carrier of S -defined Function-like non empty total 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 S
Class B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
QuotCharact B is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,(Class B)), the ResultSort of S * (Class B)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
K155( the carrier of S) is M8( the carrier of S)
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
K158( the carrier of S,(Class B)) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,(Class B)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * (Class B) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (Class B),(QuotCharact B) #) is strict MSAlgebra over S
the Sorts of (QuotMSAlg (A,B)) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F is Relation-like the carrier of S -defined Function-like non empty total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
QuotMSAlg (A,F) is strict non-empty MSAlgebra over S
Class F is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
QuotCharact F is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,(Class F)), the ResultSort of S * (Class F)
K158( the carrier of S,(Class F)) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,(Class F)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (Class F) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (Class F),(QuotCharact F) #) is strict MSAlgebra over S
the Sorts of (QuotMSAlg (A,F)) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
C1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (QuotMSAlg (A,B)), the Sorts of (QuotMSAlg (A,F))
G is set
C1 . G is Relation-like Function-like set
rng (C1 . G) is set
the Sorts of (QuotMSAlg (A,F)) . G is set
sF is Element of the carrier of S
the Sorts of (QuotMSAlg (A,B)) . sF is non empty set
C1 . sF is Relation-like the Sorts of (QuotMSAlg (A,B)) . sF -defined the Sorts of (QuotMSAlg (A,F)) . sF -valued Function-like non empty total V18( the Sorts of (QuotMSAlg (A,B)) . sF, the Sorts of (QuotMSAlg (A,F)) . sF) Element of bool [:( the Sorts of (QuotMSAlg (A,B)) . sF),( the Sorts of (QuotMSAlg (A,F)) . sF):]
the Sorts of (QuotMSAlg (A,F)) . sF is non empty set
[:( the Sorts of (QuotMSAlg (A,B)) . sF),( the Sorts of (QuotMSAlg (A,F)) . sF):] is Relation-like set
bool [:( the Sorts of (QuotMSAlg (A,B)) . sF),( the Sorts of (QuotMSAlg (A,F)) . sF):] is set
dom (C1 . sF) is non empty Element of bool ( the Sorts of (QuotMSAlg (A,B)) . sF)
bool ( the Sorts of (QuotMSAlg (A,B)) . sF) is set
rng (C1 . sF) is non empty Element of bool ( the Sorts of (QuotMSAlg (A,F)) . sF)
bool ( the Sorts of (QuotMSAlg (A,F)) . sF) is set
C12 is set
the Sorts of A . sF is non empty set
F . sF is Relation-like the Sorts of A . sF -defined the Sorts of A . sF -valued total V18( the Sorts of A . sF, the Sorts of A . sF) symmetric transitive Element of bool [:( the Sorts of A . sF),( the Sorts of A . sF):]
[:( the Sorts of A . sF),( the Sorts of A . sF):] is Relation-like set
bool [:( the Sorts of A . sF),( the Sorts of A . sF):] is set
Class (F . sF) is non empty with_non-empty_elements a_partition of the Sorts of A . sF
H is set
Class ((F . sF),H) is Element of bool ( the Sorts of A . sF)
bool ( the Sorts of A . sF) is set
B . sF is Relation-like the Sorts of A . sF -defined the Sorts of A . sF -valued total V18( the Sorts of A . sF, the Sorts of A . sF) symmetric transitive Element of bool [:( the Sorts of A . sF),( the Sorts of A . sF):]
i is Element of the Sorts of A . sF
Class ((B . sF),i) is Element of bool ( the Sorts of A . sF)
Class (B . sF) is non empty with_non-empty_elements a_partition of the Sorts of A . sF
Class (B,i) is Element of bool ( the Sorts of A . sF)
s is Element of the Sorts of (QuotMSAlg (A,B)) . sF
(C1 . sF) . s is Element of the Sorts of (QuotMSAlg (A,F)) . sF
Class (F,i) is Element of bool ( the Sorts of A . sF)
Class ((F . sF),i) is Element of bool ( the Sorts of A . sF)
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is Relation-like the carrier of S -defined Function-like non empty total 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 S
Class B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
QuotCharact B is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,(Class B)), the ResultSort of S * (Class B)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
K155( the carrier of S) is M8( the carrier of S)
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
K158( the carrier of S,(Class B)) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,(Class B)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * (Class B) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (Class B),(QuotCharact B) #) is strict MSAlgebra over S
the Sorts of (QuotMSAlg (A,B)) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F is Relation-like the carrier of S -defined Function-like non empty total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
QuotMSAlg (A,F) is strict non-empty MSAlgebra over S
Class F is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
QuotCharact F is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,(Class F)), the ResultSort of S * (Class F)
K158( the carrier of S,(Class F)) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,(Class F)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (Class F) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (Class F),(QuotCharact F) #) is strict MSAlgebra over S
the Sorts of (QuotMSAlg (A,F)) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
MSNat_Hom (A,B) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (QuotMSAlg (A,B))
MSNat_Hom (A,F) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (QuotMSAlg (A,F))
G is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (QuotMSAlg (A,B)), the Sorts of (QuotMSAlg (A,F))
G ** (MSNat_Hom (A,B)) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (QuotMSAlg (A,F))
I is set
sQ is Element of the carrier of S
the Sorts of A . sQ is non empty set
the Sorts of (QuotMSAlg (A,F)) . sQ is non empty set
the Sorts of (QuotMSAlg (A,B)) . sQ is non empty set
(MSNat_Hom (A,B)) . sQ is Relation-like the Sorts of A . sQ -defined the Sorts of (QuotMSAlg (A,B)) . sQ -valued Function-like non empty total V18( the Sorts of A . sQ, the Sorts of (QuotMSAlg (A,B)) . sQ) Element of bool [:( the Sorts of A . sQ),( the Sorts of (QuotMSAlg (A,B)) . sQ):]
[:( the Sorts of A . sQ),( the Sorts of (QuotMSAlg (A,B)) . sQ):] is Relation-like set
bool [:( the Sorts of A . sQ),( the Sorts of (QuotMSAlg (A,B)) . sQ):] is set
G . sQ is Relation-like the Sorts of (QuotMSAlg (A,B)) . sQ -defined the Sorts of (QuotMSAlg (A,F)) . sQ -valued Function-like non empty total V18( the Sorts of (QuotMSAlg (A,B)) . sQ, the Sorts of (QuotMSAlg (A,F)) . sQ) Element of bool [:( the Sorts of (QuotMSAlg (A,B)) . sQ),( the Sorts of (QuotMSAlg (A,F)) . sQ):]
[:( the Sorts of (QuotMSAlg (A,B)) . sQ),( the Sorts of (QuotMSAlg (A,F)) . sQ):] is Relation-like set
bool [:( the Sorts of (QuotMSAlg (A,B)) . sQ),( the Sorts of (QuotMSAlg (A,F)) . sQ):] is set
(G . sQ) * ((MSNat_Hom (A,B)) . sQ) is Relation-like the Sorts of A . sQ -defined the Sorts of (QuotMSAlg (A,F)) . sQ -valued Function-like non empty total V18( the Sorts of A . sQ, the Sorts of (QuotMSAlg (A,F)) . sQ) Element of bool [:( the Sorts of A . sQ),( the Sorts of (QuotMSAlg (A,F)) . sQ):]
[:( the Sorts of A . sQ),( the Sorts of (QuotMSAlg (A,F)) . sQ):] is Relation-like set
bool [:( the Sorts of A . sQ),( the Sorts of (QuotMSAlg (A,F)) . sQ):] is set
(MSNat_Hom (A,F)) . sQ is Relation-like the Sorts of A . sQ -defined the Sorts of (QuotMSAlg (A,F)) . sQ -valued Function-like non empty total V18( the Sorts of A . sQ, the Sorts of (QuotMSAlg (A,F)) . sQ) Element of bool [:( the Sorts of A . sQ),( the Sorts of (QuotMSAlg (A,F)) . sQ):]
sF is Element of the Sorts of A . sQ
((G . sQ) * ((MSNat_Hom (A,B)) . sQ)) . sF is Element of the Sorts of (QuotMSAlg (A,F)) . sQ
((MSNat_Hom (A,F)) . sQ) . sF is Element of the Sorts of (QuotMSAlg (A,F)) . sQ
B . sQ is Relation-like the Sorts of A . sQ -defined the Sorts of A . sQ -valued total V18( the Sorts of A . sQ, the Sorts of A . sQ) symmetric transitive Element of bool [:( the Sorts of A . sQ),( the Sorts of A . sQ):]
[:( the Sorts of A . sQ),( the Sorts of A . sQ):] is Relation-like set
bool [:( the Sorts of A . sQ),( the Sorts of A . sQ):] is set
Class ((B . sQ),sF) is Element of bool ( the Sorts of A . sQ)
bool ( the Sorts of A . sQ) is set
Class (B . sQ) is non empty with_non-empty_elements a_partition of the Sorts of A . sQ
Class (B,sF) is Element of bool ( the Sorts of A . sQ)
((MSNat_Hom (A,B)) . sQ) . sF is Element of the Sorts of (QuotMSAlg (A,B)) . sQ
(G . sQ) . (((MSNat_Hom (A,B)) . sQ) . sF) is Element of the Sorts of (QuotMSAlg (A,F)) . sQ
(Class B) . sQ is non empty set
MSNat_Hom (A,B,sQ) is Relation-like the Sorts of A . sQ -defined (Class B) . sQ -valued Function-like non empty total V18( the Sorts of A . sQ,(Class B) . sQ) Element of bool [:( the Sorts of A . sQ),((Class B) . sQ):]
[:( the Sorts of A . sQ),((Class B) . sQ):] is Relation-like set
bool [:( the Sorts of A . sQ),((Class B) . sQ):] is set
(MSNat_Hom (A,B,sQ)) . sF is Element of (Class B) . sQ
(G . sQ) . ((MSNat_Hom (A,B,sQ)) . sF) is set
(G . sQ) . (Class (B,sF)) is set
Class (F,sF) is Element of bool ( the Sorts of A . sQ)
F . sQ is Relation-like the Sorts of A . sQ -defined the Sorts of A . sQ -valued total V18( the Sorts of A . sQ, the Sorts of A . sQ) symmetric transitive Element of bool [:( the Sorts of A . sQ),( the Sorts of A . sQ):]
Class ((F . sQ),sF) is Element of bool ( the Sorts of A . sQ)
(Class F) . sQ is non empty set
MSNat_Hom (A,F,sQ) is Relation-like the Sorts of A . sQ -defined (Class F) . sQ -valued Function-like non empty total V18( the Sorts of A . sQ,(Class F) . sQ) Element of bool [:( the Sorts of A . sQ),((Class F) . sQ):]
[:( the Sorts of A . sQ),((Class F) . sQ):] is Relation-like set
bool [:( the Sorts of A . sQ),((Class F) . sQ):] is set
(MSNat_Hom (A,F,sQ)) . sF is Element of (Class F) . sQ
(G ** (MSNat_Hom (A,B))) . I is Relation-like Function-like set
(MSNat_Hom (A,F)) . I is Relation-like Function-like set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is Relation-like the carrier of S -defined Function-like non empty total 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 S
Class B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
QuotCharact B is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,(Class B)), the ResultSort of S * (Class B)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
K155( the carrier of S) is M8( the carrier of S)
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
K158( the carrier of S,(Class B)) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,(Class B)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * (Class B) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (Class B),(QuotCharact B) #) is strict MSAlgebra over S
the Sorts of (QuotMSAlg (A,B)) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F is Relation-like the carrier of S -defined Function-like non empty total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
QuotMSAlg (A,F) is strict non-empty MSAlgebra over S
Class F is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
QuotCharact F is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,(Class F)), the ResultSort of S * (Class F)
K158( the carrier of S,(Class F)) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,(Class F)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (Class F) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (Class F),(QuotCharact F) #) is strict MSAlgebra over S
the Sorts of (QuotMSAlg (A,F)) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
MSNat_Hom (A,F) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (QuotMSAlg (A,F))
C1 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (QuotMSAlg (A,B)), the Sorts of (QuotMSAlg (A,F))
MSNat_Hom (A,B) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (QuotMSAlg (A,B))
C1 ** (MSNat_Hom (A,B)) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (QuotMSAlg (A,F))
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
B is non-empty MSAlgebra over S
the Sorts of B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
F is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of B
MSCng F is Relation-like the carrier of S -defined Function-like non empty total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
QuotMSAlg (A,(MSCng F)) is strict non-empty MSAlgebra over S
Class (MSCng F) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
QuotCharact (MSCng F) is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,(Class (MSCng F))), the ResultSort of S * (Class (MSCng F))
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined K155( the carrier of S) -valued Function-like V18( the carrier' of S,K155( the carrier of S)) Element of bool [: the carrier' of S,K155( the carrier of S):]
K155( the carrier of S) is M8( the carrier of S)
[: the carrier' of S,K155( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K155( the carrier of S):] is set
K158( the carrier of S,(Class (MSCng F))) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,(Class (MSCng F))) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like non empty total V18( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * (Class (MSCng F)) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (Class (MSCng F)),(QuotCharact (MSCng F)) #) is strict MSAlgebra over S
MSHomQuot F is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (QuotMSAlg (A,(MSCng F))), the Sorts of B
the Sorts of (QuotMSAlg (A,(MSCng F))) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
C1 is Relation-like the carrier of S -defined Function-like non empty total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
QuotMSAlg (A,C1) is strict non-empty MSAlgebra over S
Class C1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
QuotCharact C1 is Relation-like the carrier' of S -defined Function-like non empty total ManySortedFunction of the Arity of S * K158( the carrier of S,(Class C1)), the ResultSort of S * (Class C1)
K158( the carrier of S,(Class C1)) is Relation-like K155( the carrier of S) -defined Function-like total set
the Arity of S * K158( the carrier of S,(Class C1)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S * (Class C1) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (Class C1),(QuotCharact C1) #) is strict MSAlgebra over S
the Sorts of (QuotMSAlg (A,C1)) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
MSNat_Hom (A,C1) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (QuotMSAlg (A,C1))
C12 is set
the Sorts of (QuotMSAlg (A,C1)) . C12 is set
the Sorts of (QuotMSAlg (A,(MSCng F))) . C12 is set
i is set
H is Element of the carrier of S
the Sorts of A . H is non empty set
s is Element of the Sorts of A . H
Class (C1,s) is Element of bool ( the Sorts of A . H)
bool ( the Sorts of A . H) is set
C1 . H is Relation-like the Sorts of A . H -defined the Sorts of A . H -valued total V18( the Sorts of A . H, the Sorts of A . H) symmetric transitive Element of bool [:( the Sorts of A . H),( the Sorts of A . H):]
[:( the Sorts of A . H),( the Sorts of A . H):] is Relation-like set
bool [:( the Sorts of A . H),( the Sorts of A . H):] is set
Class ((C1 . H),s) is Element of bool ( the Sorts of A . H)
Class ((MSCng F),s) is Element of bool ( the Sorts of A . H)
(MSCng F) . H is Relation-like the Sorts of A . H -defined the Sorts of A . H -valued total V18( the Sorts of A . H, the Sorts of A . H) symmetric transitive Element of bool [:( the Sorts of A . H),( the Sorts of A . H):]
Class (((MSCng F) . H),s) is Element of bool ( the Sorts of A . H)
x is Element of bool ( the Sorts of A . H)
Class ((MSCng F) . H) is non empty with_non-empty_elements a_partition of the Sorts of A . H
C12 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (QuotMSAlg (A,C1)), the Sorts of (QuotMSAlg (A,(MSCng F)))
(MSHomQuot F) ** C12 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (QuotMSAlg (A,C1)), the Sorts of B
H is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of (QuotMSAlg (A,C1)), the Sorts of B
H ** (MSNat_Hom (A,C1)) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of B
i is Element of the carrier of S
the Sorts of (QuotMSAlg (A,C1)) . i is non empty set
the Sorts of A . i is non empty set
the Sorts of (QuotMSAlg (A,(MSCng F))) . i is non empty set
C12 . i is Relation-like the Sorts of (QuotMSAlg (A,C1)) . i -defined the Sorts of (QuotMSAlg (A,(MSCng F))) . i -valued Function-like non empty total V18( the Sorts of (QuotMSAlg (A,C1)) . i, the Sorts of (QuotMSAlg (A,(MSCng F))) . i) Element of bool [:( the Sorts of (QuotMSAlg (A,C1)) . i),( the Sorts of (QuotMSAlg (A,(MSCng F))) . i):]
[:( the Sorts of (QuotMSAlg (A,C1)) . i),( the Sorts of (QuotMSAlg (A,(MSCng F))) . i):] is Relation-like set
bool [:( the Sorts of (QuotMSAlg (A,C1)) . i),( the Sorts of (QuotMSAlg (A,(MSCng F))) . i):] is set
s is Element of the Sorts of (QuotMSAlg (A,C1)) . i
(C12 . i) . s is Element of the Sorts of (QuotMSAlg (A,(MSCng F))) . i
x is Element of the Sorts of A . i
Class (C1,x) is Element of bool ( the Sorts of A . i)
bool ( the Sorts of A . i) is set
C1 . i is Relation-like the Sorts of A . i -defined the Sorts of A . i -valued total V18( the Sorts of A . i, the Sorts of A . i) symmetric transitive Element of bool [:( the Sorts of A . i),( the Sorts of A . i):]
[:( the Sorts of A . i),( the Sorts of A . i):] is Relation-like set
bool [:( the Sorts of A . i),( the Sorts of A . i):] is set
Class ((C1 . i),x) is Element of bool ( the Sorts of A . i)
Class ((MSCng F),x) is Element of bool ( the Sorts of A . i)
(MSCng F) . i is Relation-like the Sorts of A . i -defined the Sorts of A . i -valued total V18( the Sorts of A . i, the Sorts of A . i) symmetric transitive Element of bool [:( the Sorts of A . i),( the Sorts of A . i):]
Class (((MSCng F) . i),x) is Element of bool ( the Sorts of A . i)
f is Relation-like the Sorts of (QuotMSAlg (A,C1)) . i -defined the Sorts of (QuotMSAlg (A,(MSCng F))) . i -valued Function-like non empty total V18( the Sorts of (QuotMSAlg (A,C1)) . i, the Sorts of (QuotMSAlg (A,(MSCng F))) . i) Element of bool [:( the Sorts of (QuotMSAlg (A,C1)) . i),( the Sorts of (QuotMSAlg (A,(MSCng F))) . i):]
f . s is Element of the Sorts of (QuotMSAlg (A,(MSCng F))) . i
s is Element of the carrier of S
the Sorts of A . s is non empty set
x1 is Element of the Sorts of A . s
Class (C1,x1) is Element of bool ( the Sorts of A . s)
bool ( the Sorts of A . s) is set
C1 . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued total V18( the Sorts of A . s, the Sorts of A . s) symmetric transitive Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
Class ((C1 . s),x1) is Element of bool ( the Sorts of A . s)
Class ((MSCng F),x1) is Element of bool ( the Sorts of A . s)
(MSCng F) . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued total V18( the Sorts of A . s, the Sorts of A . s) symmetric transitive Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
Class (((MSCng F) . s),x1) is Element of bool ( the Sorts of A . s)
[x,x1] is V15() set
{x,x1} is non empty finite countable set
{x} is non empty finite countable set
{{x,x1},{x}} is non empty finite V35() countable set
i is set
s is Element of the carrier of S
the Sorts of A . s is non empty set
the Sorts of (QuotMSAlg (A,(MSCng F))) . s is non empty set
the Sorts of (QuotMSAlg (A,C1)) . s is non empty set
(MSNat_Hom (A,C1)) . s is Relation-like the Sorts of A . s -defined the Sorts of (QuotMSAlg (A,C1)) . s -valued Function-like non empty total V18( the Sorts of A . s, the Sorts of (QuotMSAlg (A,C1)) . s) Element of bool [:( the Sorts of A . s),( the Sorts of (QuotMSAlg (A,C1)) . s):]
[:( the Sorts of A . s),( the Sorts of (QuotMSAlg (A,C1)) . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of (QuotMSAlg (A,C1)) . s):] is set
C12 . s is Relation-like the Sorts of (QuotMSAlg (A,C1)) . s -defined the Sorts of (QuotMSAlg (A,(MSCng F))) . s -valued Function-like non empty total V18( the Sorts of (QuotMSAlg (A,C1)) . s, the Sorts of (QuotMSAlg (A,(MSCng F))) . s) Element of bool [:( the Sorts of (QuotMSAlg (A,C1)) . s),( the Sorts of (QuotMSAlg (A,(MSCng F))) . s):]
[:( the Sorts of (QuotMSAlg (A,C1)) . s),( the Sorts of (QuotMSAlg (A,(MSCng F))) . s):] is Relation-like set
bool [:( the Sorts of (QuotMSAlg (A,C1)) . s),( the Sorts of (QuotMSAlg (A,(MSCng F))) . s):] is set
(C12 . s) * ((MSNat_Hom (A,C1)) . s) is Relation-like the Sorts of A . s -defined the Sorts of (QuotMSAlg (A,(MSCng F))) . s -valued Function-like non empty total V18( the Sorts of A . s, the Sorts of (QuotMSAlg (A,(MSCng F))) . s) Element of bool [:( the Sorts of A . s),( the Sorts of (QuotMSAlg (A,(MSCng F))) . s):]
[:( the Sorts of A . s),( the Sorts of (QuotMSAlg (A,(MSCng F))) . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of (QuotMSAlg (A,(MSCng F))) . s):] is set
MSNat_Hom (A,(MSCng F)) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (QuotMSAlg (A,(MSCng F)))
(MSNat_Hom (A,(MSCng F))) . s is Relation-like the Sorts of A . s -defined the Sorts of (QuotMSAlg (A,(MSCng F))) . s -valued Function-like non empty total V18( the Sorts of A . s, the Sorts of (QuotMSAlg (A,(MSCng F))) . s) Element of bool [:( the Sorts of A . s),( the Sorts of (QuotMSAlg (A,(MSCng F))) . s):]
x is Element of the Sorts of A . s
((C12 . s) * ((MSNat_Hom (A,C1)) . s)) . x is Element of the Sorts of (QuotMSAlg (A,(MSCng F))) . s
((MSNat_Hom (A,(MSCng F))) . s) . x is Element of the Sorts of (QuotMSAlg (A,(MSCng F))) . s
C1 . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued total V18( the Sorts of A . s, the Sorts of A . s) symmetric transitive Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
Class ((C1 . s),x) is Element of bool ( the Sorts of A . s)
bool ( the Sorts of A . s) is set
Class (C1 . s) is non empty with_non-empty_elements a_partition of the Sorts of A . s
Class (C1,x) is Element of bool ( the Sorts of A . s)
(Class C1) . s is non empty set
((MSNat_Hom (A,C1)) . s) . x is Element of the Sorts of (QuotMSAlg (A,C1)) . s
(C12 . s) . (((MSNat_Hom (A,C1)) . s) . x) is Element of the Sorts of (QuotMSAlg (A,(MSCng F))) . s
MSNat_Hom (A,C1,s) is Relation-like the Sorts of A . s -defined (Class C1) . s -valued Function-like non empty total V18( the Sorts of A . s,(Class C1) . s) Element of bool [:( the Sorts of A . s),((Class C1) . s):]
[:( the Sorts of A . s),((Class C1) . s):] is Relation-like set
bool [:( the Sorts of A . s),((Class C1) . s):] is set
(MSNat_Hom (A,C1,s)) . x is Element of (Class C1) . s
(C12 . s) . ((MSNat_Hom (A,C1,s)) . x) is set
(C12 . s) . (Class (C1,x)) is set
Class ((MSCng F),x) is Element of bool ( the Sorts of A . s)
(MSCng F) . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued total V18( the Sorts of A . s, the Sorts of A . s) symmetric transitive Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
Class (((MSCng F) . s),x) is Element of bool ( the Sorts of A . s)
(Class (MSCng F)) . s is non empty set
MSNat_Hom (A,(MSCng F),s) is Relation-like the Sorts of A . s -defined (Class (MSCng F)) . s -valued Function-like non empty total V18( the Sorts of A . s,(Class (MSCng F)) . s) Element of bool [:( the Sorts of A . s),((Class (MSCng F)) . s):]
[:( the Sorts of A . s),((Class (MSCng F)) . s):] is Relation-like set
bool [:( the Sorts of A . s),((Class (MSCng F)) . s):] is set
(MSNat_Hom (A,(MSCng F),s)) . x is Element of (Class (MSCng F)) . s
C12 ** (MSNat_Hom (A,C1)) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of (QuotMSAlg (A,(MSCng F)))
(C12 ** (MSNat_Hom (A,C1))) . i is Relation-like Function-like set
(MSNat_Hom (A,(MSCng F))) . i is Relation-like Function-like set
(MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of B
(MSHomQuot F) ** (C12 ** (MSNat_Hom (A,C1))) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of B