:: MSINST_1 semantic presentation

NAT is Element of bool REAL
REAL is set
bool REAL is non empty set
NAT is set
bool NAT is non empty set
bool NAT is non empty set
K296() is set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V28() Function-yielding V37() V53() V54() V55() set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V28() Function-yielding V37() V53() V54() V55() set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V28() Function-yielding V37() V53() V54() V55() set
{{}} is functional non empty set
{{}} * is functional non empty V55() M8({{}})
[:({{}} *),{{}}:] is Relation-like non empty set
bool [:({{}} *),{{}}:] is non empty set
PFuncs (({{}} *),{{}}) is set
1 is non empty set
2 is non empty set
3 is non empty set
A is non empty set
MSS_set A is non empty MSS-membered set
[:(MSS_set A),(MSS_set A):] is Relation-like non empty set
C is Relation-like [:(MSS_set A),(MSS_set A):] -defined Function-like non empty total set
[:(MSS_set A),(MSS_set A),(MSS_set A):] is non empty set
{|C,C|} is Relation-like [:(MSS_set A),(MSS_set A),(MSS_set A):] -defined Function-like non empty total set
{|C|} is Relation-like [:(MSS_set A),(MSS_set A),(MSS_set A):] -defined Function-like non empty total set
o is set
{|C,C|} . o is set
{|C|} . o is set
GM is set
C is set
i is set
[GM,C,i] is V15() V16() set
[GM,C] is V15() set
{GM,C} is non empty set
{GM} is non empty set
{{GM,C},{GM}} is non empty set
[[GM,C],i] is V15() set
{[GM,C],i} is non empty set
{[GM,C]} is Relation-like Function-like non empty set
{{[GM,C],i},{[GM,C]}} is non empty set
j is set
i9 is non empty non void feasible strict Element of MSS_set A
MS is non empty non void feasible strict Element of MSS_set A
e is non empty non void feasible strict Element of MSS_set A
{|C,C|} . (i9,MS,e) is set
[i9,MS,e] is V15() V16() set
[i9,MS] is V15() set
{i9,MS} is non empty set
{i9} is non empty set
{{i9,MS},{i9}} is non empty set
[[i9,MS],e] is V15() set
{[i9,MS],e} is non empty set
{[i9,MS]} is Relation-like Function-like non empty set
{{[i9,MS],e},{[i9,MS]}} is non empty set
{|C,C|} . [i9,MS,e] is set
C . (MS,e) is set
[MS,e] is V15() set
{MS,e} is non empty set
{MS} is non empty set
{{MS,e},{MS}} is non empty set
C . [MS,e] is set
C . (i9,MS) is set
C . [i9,MS] is set
[:(C . (MS,e)),(C . (i9,MS)):] is Relation-like set
{|C|} . (i9,MS,e) is set
j `1 is set
MSS_morph (MS,e) is set
j9 is Relation-like Function-like set
f is Relation-like Function-like set
[j9,f] is V15() set
{j9,f} is functional non empty set
{j9} is functional non empty set
{{j9,f},{j9}} is non empty set
j `2 is set
MSS_morph (i9,MS) is set
I is Relation-like Function-like set
J is Relation-like Function-like set
[I,J] is V15() set
{I,J} is functional non empty set
{I} is functional non empty set
{{I,J},{I}} is non empty set
I * j9 is Relation-like Function-like set
J * f is Relation-like Function-like set
[(I * j9),(J * f)] is V15() set
{(I * j9),(J * f)} is functional non empty set
{(I * j9)} is functional non empty set
{{(I * j9),(J * f)},{(I * j9)}} is non empty set
M1 is V15() set
C . (i9,e) is set
[i9,e] is V15() set
{i9,e} is non empty set
{{i9,e},{i9}} is non empty set
C . [i9,e] is set
MSS_morph (i9,e) is set
N1 is Relation-like Function-like set
F is Relation-like Function-like set
[N1,F] is V15() set
{N1,F} is functional non empty set
{N1} is functional non empty set
{{N1,F},{N1}} is non empty set
F is Relation-like Function-like set
G is Relation-like Function-like set
[F,G] is V15() set
{F,G} is functional non empty set
{F} is functional non empty set
{{F,G},{F}} is non empty set
[[F,G],[N1,F]] is V15() set
{[F,G],[N1,F]} is Relation-like non empty set
{[F,G]} is Relation-like Function-like non empty set
{{[F,G],[N1,F]},{[F,G]}} is non empty set
N1 * F is Relation-like Function-like set
F * G is Relation-like Function-like set
[(N1 * F),(F * G)] is V15() set
{(N1 * F),(F * G)} is functional non empty set
{(N1 * F)} is functional non empty set
{{(N1 * F),(F * G)},{(N1 * F)}} is non empty set
o is Relation-like [:(MSS_set A),(MSS_set A),(MSS_set A):] -defined Function-like non empty total Function-yielding V37() ManySortedFunction of {|C,C|},{|C|}
AltCatStr(# (MSS_set A),C,o #) is non empty strict AltCatStr
GM is non empty strict AltCatStr
the carrier of GM is non empty set
the Arrows of GM is Relation-like [: the carrier of GM, the carrier of GM:] -defined Function-like non empty total set
[: the carrier of GM, the carrier of GM:] is Relation-like non empty set
the Comp of GM is Relation-like [: the carrier of GM, the carrier of GM, the carrier of GM:] -defined Function-like non empty total Function-yielding V37() ManySortedFunction of {| the Arrows of GM, the Arrows of GM|},{| the Arrows of GM|}
[: the carrier of GM, the carrier of GM, the carrier of GM:] is non empty set
{| the Arrows of GM, the Arrows of GM|} is Relation-like [: the carrier of GM, the carrier of GM, the carrier of GM:] -defined Function-like non empty total set
{| the Arrows of GM|} is Relation-like [: the carrier of GM, the carrier of GM, the carrier of GM:] -defined Function-like non empty total set
C is non empty AltCatStr
the carrier of C is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Comp of C is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V37() ManySortedFunction of {| the Arrows of C, the Arrows of C|},{| the Arrows of C|}
[: the carrier of C, the carrier of C, the carrier of C:] is non empty set
{| the Arrows of C, the Arrows of C|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
{| the Arrows of C|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
i is Element of the carrier of C
i9 is Element of the carrier of C
MS is Element of the carrier of C
the Arrows of C . (i,i9) is set
[i,i9] is V15() set
{i,i9} is non empty set
{i} is non empty set
{{i,i9},{i}} is non empty set
the Arrows of C . [i,i9] is set
the Arrows of C . (i9,MS) is set
[i9,MS] is V15() set
{i9,MS} is non empty set
{i9} is non empty set
{{i9,MS},{i9}} is non empty set
the Arrows of C . [i9,MS] is set
the Comp of C . (i,i9,MS) is Relation-like [:( the Arrows of C . (i9,MS)),( the Arrows of C . (i,i9)):] -defined the Arrows of C . (i,MS) -valued Function-like quasi_total Element of bool [:[:( the Arrows of C . (i9,MS)),( the Arrows of C . (i,i9)):],( the Arrows of C . (i,MS)):]
[:( the Arrows of C . (i9,MS)),( the Arrows of C . (i,i9)):] is Relation-like set
the Arrows of C . (i,MS) is set
[i,MS] is V15() set
{i,MS} is non empty set
{{i,MS},{i}} is non empty set
the Arrows of C . [i,MS] is set
[:[:( the Arrows of C . (i9,MS)),( the Arrows of C . (i,i9)):],( the Arrows of C . (i,MS)):] is Relation-like set
bool [:[:( the Arrows of C . (i9,MS)),( the Arrows of C . (i,i9)):],( the Arrows of C . (i,MS)):] is non empty set
e is Relation-like Function-like set
j is Relation-like Function-like set
[e,j] is V15() set
{e,j} is functional non empty set
{e} is functional non empty set
{{e,j},{e}} is non empty set
j9 is Relation-like Function-like set
f is Relation-like Function-like set
[j9,f] is V15() set
{j9,f} is functional non empty set
{j9} is functional non empty set
{{j9,f},{j9}} is non empty set
( the Comp of C . (i,i9,MS)) . ([j9,f],[e,j]) is set
[[j9,f],[e,j]] is V15() set
{[j9,f],[e,j]} is Relation-like non empty set
{[j9,f]} is Relation-like Function-like non empty set
{{[j9,f],[e,j]},{[j9,f]}} is non empty set
( the Comp of C . (i,i9,MS)) . [[j9,f],[e,j]] is set
e * j9 is Relation-like Function-like set
j * f is Relation-like Function-like set
[(e * j9),(j * f)] is V15() set
{(e * j9),(j * f)} is functional non empty set
{(e * j9)} is functional non empty set
{{(e * j9),(j * f)},{(e * j9)}} is non empty set
[i,i9,MS] is V15() V16() set
[[i,i9],MS] is V15() set
{[i,i9],MS} is non empty set
{[i,i9]} is Relation-like Function-like non empty set
{{[i,i9],MS},{[i,i9]}} is non empty set
{|C,C|} . [i,i9,MS] is set
{|C|} . [i,i9,MS] is set
[:({|C,C|} . [i,i9,MS]),({|C|} . [i,i9,MS]):] is Relation-like set
bool [:({|C,C|} . [i,i9,MS]),({|C|} . [i,i9,MS]):] is non empty set
o . [i,i9,MS] is Relation-like Function-like set
M1 is Relation-like {|C,C|} . [i,i9,MS] -defined {|C|} . [i,i9,MS] -valued Function-like quasi_total Element of bool [:({|C,C|} . [i,i9,MS]),({|C|} . [i,i9,MS]):]
{|C,C|} . (i,i9,MS) is set
C . (i9,MS) is set
C . [i9,MS] is set
C . (i,i9) is set
C . [i,i9] is set
[:(C . (i9,MS)),(C . (i,i9)):] is Relation-like set
M1 . [[j9,f],[e,j]] is set
N1 is non empty non void feasible strict Element of MSS_set A
F is non empty non void feasible strict Element of MSS_set A
F is non empty non void feasible strict Element of MSS_set A
[N1,F,F] is V15() V16() set
[N1,F] is V15() set
{N1,F} is non empty set
{N1} is non empty set
{{N1,F},{N1}} is non empty set
[[N1,F],F] is V15() set
{[N1,F],F} is non empty set
{[N1,F]} is Relation-like Function-like non empty set
{{[N1,F],F},{[N1,F]}} is non empty set
C . (N1,F) is set
C . [N1,F] is set
C . (F,F) is set
[F,F] is V15() set
{F,F} is non empty set
{F} is non empty set
{{F,F},{F}} is non empty set
C . [F,F] is set
i is non empty non void feasible strict Element of MSS_set A
i9 is non empty non void feasible strict Element of MSS_set A
the Arrows of GM . (i,i9) is set
[i,i9] is V15() set
{i,i9} is non empty set
{i} is non empty set
{{i,i9},{i}} is non empty set
the Arrows of GM . [i,i9] is set
MSS_morph (i,i9) is set
MS is Element of the carrier of GM
e is Element of the carrier of GM
j is Element of the carrier of GM
j9 is Relation-like Function-like set
f is Relation-like Function-like set
[j9,f] is V15() set
{j9,f} is functional non empty set
{j9} is functional non empty set
{{j9,f},{j9}} is non empty set
the Arrows of GM . (MS,e) is set
[MS,e] is V15() set
{MS,e} is non empty set
{MS} is non empty set
{{MS,e},{MS}} is non empty set
the Arrows of GM . [MS,e] is set
I is Relation-like Function-like set
J is Relation-like Function-like set
[I,J] is V15() set
{I,J} is functional non empty set
{I} is functional non empty set
{{I,J},{I}} is non empty set
the Arrows of GM . (e,j) is set
[e,j] is V15() set
{e,j} is non empty set
{e} is non empty set
{{e,j},{e}} is non empty set
the Arrows of GM . [e,j] is set
the Comp of GM . (MS,e,j) is Relation-like [:( the Arrows of GM . (e,j)),( the Arrows of GM . (MS,e)):] -defined the Arrows of GM . (MS,j) -valued Function-like quasi_total Element of bool [:[:( the Arrows of GM . (e,j)),( the Arrows of GM . (MS,e)):],( the Arrows of GM . (MS,j)):]
[:( the Arrows of GM . (e,j)),( the Arrows of GM . (MS,e)):] is Relation-like set
the Arrows of GM . (MS,j) is set
[MS,j] is V15() set
{MS,j} is non empty set
{{MS,j},{MS}} is non empty set
the Arrows of GM . [MS,j] is set
[:[:( the Arrows of GM . (e,j)),( the Arrows of GM . (MS,e)):],( the Arrows of GM . (MS,j)):] is Relation-like set
bool [:[:( the Arrows of GM . (e,j)),( the Arrows of GM . (MS,e)):],( the Arrows of GM . (MS,j)):] is non empty set
( the Comp of GM . (MS,e,j)) . ([I,J],[j9,f]) is set
[[I,J],[j9,f]] is V15() set
{[I,J],[j9,f]} is Relation-like non empty set
{[I,J]} is Relation-like Function-like non empty set
{{[I,J],[j9,f]},{[I,J]}} is non empty set
( the Comp of GM . (MS,e,j)) . [[I,J],[j9,f]] is set
j9 * I is Relation-like Function-like set
f * J is Relation-like Function-like set
[(j9 * I),(f * J)] is V15() set
{(j9 * I),(f * J)} is functional non empty set
{(j9 * I)} is functional non empty set
{{(j9 * I),(f * J)},{(j9 * I)}} is non empty set
C is non empty strict AltCatStr
the carrier of C is non empty set
the Arrows of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like non empty total set
[: the carrier of C, the carrier of C:] is Relation-like non empty set
the Comp of C is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total Function-yielding V37() ManySortedFunction of {| the Arrows of C, the Arrows of C|},{| the Arrows of C|}
[: the carrier of C, the carrier of C, the carrier of C:] is non empty set
{| the Arrows of C, the Arrows of C|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
{| the Arrows of C|} is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like non empty total set
o is non empty strict AltCatStr
the carrier of o is non empty set
the Arrows of o is Relation-like [: the carrier of o, the carrier of o:] -defined Function-like non empty total set
[: the carrier of o, the carrier of o:] is Relation-like non empty set
the Comp of o is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like non empty total Function-yielding V37() ManySortedFunction of {| the Arrows of o, the Arrows of o|},{| the Arrows of o|}
[: the carrier of o, the carrier of o, the carrier of o:] is non empty set
{| the Arrows of o, the Arrows of o|} is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like non empty total set
{| the Arrows of o|} is Relation-like [: the carrier of o, the carrier of o, the carrier of o:] -defined Function-like non empty total set
[:(MSS_set A),(MSS_set A):] is Relation-like non empty set
[:(MSS_set A),(MSS_set A),(MSS_set A):] is non empty set
C is Relation-like [:(MSS_set A),(MSS_set A):] -defined Function-like non empty total set
MS is non empty non void feasible strict Element of MSS_set A
e is non empty non void feasible strict Element of MSS_set A
C . (MS,e) is set
[MS,e] is V15() set
{MS,e} is non empty set
{MS} is non empty set
{{MS,e},{MS}} is non empty set
C . [MS,e] is set
MSS_morph (MS,e) is set
GM is Relation-like [:(MSS_set A),(MSS_set A):] -defined Function-like non empty total set
GM . (MS,e) is set
GM . [MS,e] is set
MS is set
e is set
j is set
[MS,e,j] is V15() V16() set
[MS,e] is V15() set
{MS,e} is non empty set
{MS} is non empty set
{{MS,e},{MS}} is non empty set
[[MS,e],j] is V15() set
{[MS,e],j} is non empty set
{[MS,e]} is Relation-like Function-like non empty set
{{[MS,e],j},{[MS,e]}} is non empty set
i is Relation-like [:(MSS_set A),(MSS_set A),(MSS_set A):] -defined Function-like non empty total set
i . (MS,e,j) is set
i . [MS,e,j] is set
i9 is Relation-like [:(MSS_set A),(MSS_set A),(MSS_set A):] -defined Function-like non empty total set
i9 . (MS,e,j) is set
i9 . [MS,e,j] is set
{|GM,GM|} is Relation-like [:(MSS_set A),(MSS_set A),(MSS_set A):] -defined Function-like non empty total set
{|GM,GM|} . [MS,e,j] is set
{|GM|} is Relation-like [:(MSS_set A),(MSS_set A),(MSS_set A):] -defined Function-like non empty total set
{|GM|} . [MS,e,j] is set
[:({|GM,GM|} . [MS,e,j]),({|GM|} . [MS,e,j]):] is Relation-like set
bool [:({|GM,GM|} . [MS,e,j]),({|GM|} . [MS,e,j]):] is non empty set
{|C,C|} is Relation-like [:(MSS_set A),(MSS_set A),(MSS_set A):] -defined Function-like non empty total set
{|C,C|} . [MS,e,j] is set
{|C|} is Relation-like [:(MSS_set A),(MSS_set A),(MSS_set A):] -defined Function-like non empty total set
{|C|} . [MS,e,j] is set
[:({|C,C|} . [MS,e,j]),({|C|} . [MS,e,j]):] is Relation-like set
bool [:({|C,C|} . [MS,e,j]),({|C|} . [MS,e,j]):] is non empty set
H is Relation-like {|C,C|} . [MS,e,j] -defined {|C|} . [MS,e,j] -valued Function-like quasi_total Element of bool [:({|C,C|} . [MS,e,j]),({|C|} . [MS,e,j]):]
N3 is Relation-like {|GM,GM|} . [MS,e,j] -defined {|GM|} . [MS,e,j] -valued Function-like quasi_total Element of bool [:({|GM,GM|} . [MS,e,j]),({|GM|} . [MS,e,j]):]
G9 is set
H . G9 is set
N3 . G9 is set
{|C,C|} . (MS,e,j) is set
C . (e,j) is set
[e,j] is V15() set
{e,j} is non empty set
{e} is non empty set
{{e,j},{e}} is non empty set
C . [e,j] is set
C . (MS,e) is set
C . [MS,e] is set
[:(C . (e,j)),(C . (MS,e)):] is Relation-like set
G9 `1 is set
I is non empty non void feasible strict Element of MSS_set A
J is non empty non void feasible strict Element of MSS_set A
MSS_morph (I,J) is set
HG is Relation-like Function-like set
M1 is Relation-like Function-like set
[HG,M1] is V15() set
{HG,M1} is functional non empty set
{HG} is functional non empty set
{{HG,M1},{HG}} is non empty set
{|GM,GM|} . (MS,e,j) is set
GM . (e,j) is set
GM . [e,j] is set
GM . (MS,e) is set
GM . [MS,e] is set
[:(GM . (e,j)),(GM . (MS,e)):] is Relation-like set
G9 `2 is set
f is non empty non void feasible strict Element of MSS_set A
MSS_morph (f,I) is set
N1 is Relation-like Function-like set
F is Relation-like Function-like set
[N1,F] is V15() set
{N1,F} is functional non empty set
{N1} is functional non empty set
{{N1,F},{N1}} is non empty set
[[HG,M1],[N1,F]] is V15() set
{[HG,M1],[N1,F]} is Relation-like non empty set
{[HG,M1]} is Relation-like Function-like non empty set
{{[HG,M1],[N1,F]},{[HG,M1]}} is non empty set
F is Element of the carrier of C
G is Element of the carrier of C
M3 is Element of the carrier of C
the Comp of C . (F,G,M3) is Relation-like [:( the Arrows of C . (G,M3)),( the Arrows of C . (F,G)):] -defined the Arrows of C . (F,M3) -valued Function-like quasi_total Element of bool [:[:( the Arrows of C . (G,M3)),( the Arrows of C . (F,G)):],( the Arrows of C . (F,M3)):]
the Arrows of C . (G,M3) is set
[G,M3] is V15() set
{G,M3} is non empty set
{G} is non empty set
{{G,M3},{G}} is non empty set
the Arrows of C . [G,M3] is set
the Arrows of C . (F,G) is set
[F,G] is V15() set
{F,G} is non empty set
{F} is non empty set
{{F,G},{F}} is non empty set
the Arrows of C . [F,G] is set
[:( the Arrows of C . (G,M3)),( the Arrows of C . (F,G)):] is Relation-like set
the Arrows of C . (F,M3) is set
[F,M3] is V15() set
{F,M3} is non empty set
{{F,M3},{F}} is non empty set
the Arrows of C . [F,M3] is set
[:[:( the Arrows of C . (G,M3)),( the Arrows of C . (F,G)):],( the Arrows of C . (F,M3)):] is Relation-like set
bool [:[:( the Arrows of C . (G,M3)),( the Arrows of C . (F,G)):],( the Arrows of C . (F,M3)):] is non empty set
( the Comp of C . (F,G,M3)) . ([HG,M1],[N1,F]) is set
( the Comp of C . (F,G,M3)) . [[HG,M1],[N1,F]] is set
N1 * HG is Relation-like Function-like set
F * M1 is Relation-like Function-like set
[(N1 * HG),(F * M1)] is V15() set
{(N1 * HG),(F * M1)} is functional non empty set
{(N1 * HG)} is functional non empty set
{{(N1 * HG),(F * M1)},{(N1 * HG)}} is non empty set
M1 is Element of the carrier of o
N1 is Element of the carrier of o
F is Element of the carrier of o
the Comp of o . (M1,N1,F) is Relation-like [:( the Arrows of o . (N1,F)),( the Arrows of o . (M1,N1)):] -defined the Arrows of o . (M1,F) -valued Function-like quasi_total Element of bool [:[:( the Arrows of o . (N1,F)),( the Arrows of o . (M1,N1)):],( the Arrows of o . (M1,F)):]
the Arrows of o . (N1,F) is set
[N1,F] is V15() set
{N1,F} is non empty set
{N1} is non empty set
{{N1,F},{N1}} is non empty set
the Arrows of o . [N1,F] is set
the Arrows of o . (M1,N1) is set
[M1,N1] is V15() set
{M1,N1} is non empty set
{M1} is non empty set
{{M1,N1},{M1}} is non empty set
the Arrows of o . [M1,N1] is set
[:( the Arrows of o . (N1,F)),( the Arrows of o . (M1,N1)):] is Relation-like set
the Arrows of o . (M1,F) is set
[M1,F] is V15() set
{M1,F} is non empty set
{{M1,F},{M1}} is non empty set
the Arrows of o . [M1,F] is set
[:[:( the Arrows of o . (N1,F)),( the Arrows of o . (M1,N1)):],( the Arrows of o . (M1,F)):] is Relation-like set
bool [:[:( the Arrows of o . (N1,F)),( the Arrows of o . (M1,N1)):],( the Arrows of o . (M1,F)):] is non empty set
( the Comp of o . (M1,N1,F)) . ([HG,M1],[N1,F]) is set
( the Comp of o . (M1,N1,F)) . [[HG,M1],[N1,F]] is set
dom N3 is Element of bool ({|GM,GM|} . [MS,e,j])
bool ({|GM,GM|} . [MS,e,j]) is non empty set
dom H is Element of bool ({|C,C|} . [MS,e,j])
bool ({|C,C|} . [MS,e,j]) is non empty set
H is Relation-like {|C,C|} . [MS,e,j] -defined {|C|} . [MS,e,j] -valued Function-like quasi_total Element of bool [:({|C,C|} . [MS,e,j]),({|C|} . [MS,e,j]):]
N3 is Relation-like {|GM,GM|} . [MS,e,j] -defined {|GM|} . [MS,e,j] -valued Function-like quasi_total Element of bool [:({|GM,GM|} . [MS,e,j]),({|GM|} . [MS,e,j]):]
A is non empty set
(A) is non empty strict AltCatStr
the carrier of (A) is non empty set
o is Element of the carrier of (A)
GM is Element of the carrier of (A)
<^o,GM^> is set
the Arrows of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined Function-like non empty total set
[: the carrier of (A), the carrier of (A):] is Relation-like non empty set
the Arrows of (A) . (o,GM) is set
[o,GM] is V15() set
{o,GM} is non empty set
{o} is non empty set
{{o,GM},{o}} is non empty set
the Arrows of (A) . [o,GM] is set
C is Element of the carrier of (A)
<^GM,C^> is set
the Arrows of (A) . (GM,C) is set
[GM,C] is V15() set
{GM,C} is non empty set
{GM} is non empty set
{{GM,C},{GM}} is non empty set
the Arrows of (A) . [GM,C] is set
<^o,C^> is set
the Arrows of (A) . (o,C) is set
[o,C] is V15() set
{o,C} is non empty set
{{o,C},{o}} is non empty set
the Arrows of (A) . [o,C] is set
MSS_set A is non empty MSS-membered set
i9 is non empty non void feasible strict Element of MSS_set A
MS is non empty non void feasible strict Element of MSS_set A
MSS_morph (i9,MS) is set
the Element of MSS_morph (i9,MS) is Element of MSS_morph (i9,MS)
j is Relation-like Function-like set
j9 is Relation-like Function-like set
[j,j9] is V15() set
{j,j9} is functional non empty set
{j} is functional non empty set
{{j,j9},{j}} is non empty set
i is non empty non void feasible strict Element of MSS_set A
MSS_morph (i,i9) is set
the Element of MSS_morph (i,i9) is Element of MSS_morph (i,i9)
I is Relation-like Function-like set
J is Relation-like Function-like set
[I,J] is V15() set
{I,J} is functional non empty set
{I} is functional non empty set
{{I,J},{I}} is non empty set
I * j is Relation-like Function-like set
J * j9 is Relation-like Function-like set
[(I * j),(J * j9)] is V15() set
{(I * j),(J * j9)} is functional non empty set
{(I * j)} is functional non empty set
{{(I * j),(J * j9)},{(I * j)}} is non empty set
MSS_morph (i,MS) is set
the Arrows of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined Function-like non empty total set
the carrier of (A) is non empty set
[: the carrier of (A), the carrier of (A):] is Relation-like non empty set
the Comp of (A) is Relation-like [: the carrier of (A), the carrier of (A), the carrier of (A):] -defined Function-like non empty total Function-yielding V37() ManySortedFunction of {| the Arrows of (A), the Arrows of (A)|},{| the Arrows of (A)|}
[: the carrier of (A), the carrier of (A), the carrier of (A):] is non empty set
{| the Arrows of (A), the Arrows of (A)|} is Relation-like [: the carrier of (A), the carrier of (A), the carrier of (A):] -defined Function-like non empty total set
{| the Arrows of (A)|} is Relation-like [: the carrier of (A), the carrier of (A), the carrier of (A):] -defined Function-like non empty total set
C is Element of the carrier of (A)
i is Element of the carrier of (A)
the Arrows of (A) . (C,i) is set
[C,i] is V15() set
{C,i} is non empty set
{C} is non empty set
{{C,i},{C}} is non empty set
the Arrows of (A) . [C,i] is set
i9 is Element of the carrier of (A)
the Arrows of (A) . (i,i9) is set
[i,i9] is V15() set
{i,i9} is non empty set
{i} is non empty set
{{i,i9},{i}} is non empty set
the Arrows of (A) . [i,i9] is set
MS is Element of the carrier of (A)
the Arrows of (A) . (i9,MS) is set
[i9,MS] is V15() set
{i9,MS} is non empty set
{i9} is non empty set
{{i9,MS},{i9}} is non empty set
the Arrows of (A) . [i9,MS] is set
the Comp of (A) . (C,i9,MS) is Relation-like [:( the Arrows of (A) . (i9,MS)),( the Arrows of (A) . (C,i9)):] -defined the Arrows of (A) . (C,MS) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (A) . (i9,MS)),( the Arrows of (A) . (C,i9)):],( the Arrows of (A) . (C,MS)):]
the Arrows of (A) . (C,i9) is set
[C,i9] is V15() set
{C,i9} is non empty set
{{C,i9},{C}} is non empty set
the Arrows of (A) . [C,i9] is set
[:( the Arrows of (A) . (i9,MS)),( the Arrows of (A) . (C,i9)):] is Relation-like set
the Arrows of (A) . (C,MS) is set
[C,MS] is V15() set
{C,MS} is non empty set
{{C,MS},{C}} is non empty set
the Arrows of (A) . [C,MS] is set
[:[:( the Arrows of (A) . (i9,MS)),( the Arrows of (A) . (C,i9)):],( the Arrows of (A) . (C,MS)):] is Relation-like set
bool [:[:( the Arrows of (A) . (i9,MS)),( the Arrows of (A) . (C,i9)):],( the Arrows of (A) . (C,MS)):] is non empty set
the Comp of (A) . (C,i,i9) is Relation-like [:( the Arrows of (A) . (i,i9)),( the Arrows of (A) . (C,i)):] -defined the Arrows of (A) . (C,i9) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (A) . (i,i9)),( the Arrows of (A) . (C,i)):],( the Arrows of (A) . (C,i9)):]
[:( the Arrows of (A) . (i,i9)),( the Arrows of (A) . (C,i)):] is Relation-like set
[:[:( the Arrows of (A) . (i,i9)),( the Arrows of (A) . (C,i)):],( the Arrows of (A) . (C,i9)):] is Relation-like set
bool [:[:( the Arrows of (A) . (i,i9)),( the Arrows of (A) . (C,i)):],( the Arrows of (A) . (C,i9)):] is non empty set
the Comp of (A) . (C,i,MS) is Relation-like [:( the Arrows of (A) . (i,MS)),( the Arrows of (A) . (C,i)):] -defined the Arrows of (A) . (C,MS) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (A) . (i,MS)),( the Arrows of (A) . (C,i)):],( the Arrows of (A) . (C,MS)):]
the Arrows of (A) . (i,MS) is set
[i,MS] is V15() set
{i,MS} is non empty set
{{i,MS},{i}} is non empty set
the Arrows of (A) . [i,MS] is set
[:( the Arrows of (A) . (i,MS)),( the Arrows of (A) . (C,i)):] is Relation-like set
[:[:( the Arrows of (A) . (i,MS)),( the Arrows of (A) . (C,i)):],( the Arrows of (A) . (C,MS)):] is Relation-like set
bool [:[:( the Arrows of (A) . (i,MS)),( the Arrows of (A) . (C,i)):],( the Arrows of (A) . (C,MS)):] is non empty set
the Comp of (A) . (i,i9,MS) is Relation-like [:( the Arrows of (A) . (i9,MS)),( the Arrows of (A) . (i,i9)):] -defined the Arrows of (A) . (i,MS) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (A) . (i9,MS)),( the Arrows of (A) . (i,i9)):],( the Arrows of (A) . (i,MS)):]
[:( the Arrows of (A) . (i9,MS)),( the Arrows of (A) . (i,i9)):] is Relation-like set
[:[:( the Arrows of (A) . (i9,MS)),( the Arrows of (A) . (i,i9)):],( the Arrows of (A) . (i,MS)):] is Relation-like set
bool [:[:( the Arrows of (A) . (i9,MS)),( the Arrows of (A) . (i,i9)):],( the Arrows of (A) . (i,MS)):] is non empty set
I is set
J is set
M1 is set
( the Comp of (A) . (C,i,i9)) . (J,I) is set
[J,I] is V15() set
{J,I} is non empty set
{J} is non empty set
{{J,I},{J}} is non empty set
( the Comp of (A) . (C,i,i9)) . [J,I] is set
( the Comp of (A) . (C,i9,MS)) . (M1,(( the Comp of (A) . (C,i,i9)) . (J,I))) is set
[M1,(( the Comp of (A) . (C,i,i9)) . (J,I))] is V15() set
{M1,(( the Comp of (A) . (C,i,i9)) . (J,I))} is non empty set
{M1} is non empty set
{{M1,(( the Comp of (A) . (C,i,i9)) . (J,I))},{M1}} is non empty set
( the Comp of (A) . (C,i9,MS)) . [M1,(( the Comp of (A) . (C,i,i9)) . (J,I))] is set
( the Comp of (A) . (i,i9,MS)) . (M1,J) is set
[M1,J] is V15() set
{M1,J} is non empty set
{{M1,J},{M1}} is non empty set
( the Comp of (A) . (i,i9,MS)) . [M1,J] is set
( the Comp of (A) . (C,i,MS)) . ((( the Comp of (A) . (i,i9,MS)) . (M1,J)),I) is set
[(( the Comp of (A) . (i,i9,MS)) . (M1,J)),I] is V15() set
{(( the Comp of (A) . (i,i9,MS)) . (M1,J)),I} is non empty set
{(( the Comp of (A) . (i,i9,MS)) . (M1,J))} is non empty set
{{(( the Comp of (A) . (i,i9,MS)) . (M1,J)),I},{(( the Comp of (A) . (i,i9,MS)) . (M1,J))}} is non empty set
( the Comp of (A) . (C,i,MS)) . [(( the Comp of (A) . (i,i9,MS)) . (M1,J)),I] is set
MSS_set A is non empty MSS-membered set
F is non empty non void feasible strict Element of MSS_set A
F is non empty non void feasible strict Element of MSS_set A
MSS_morph (F,F) is set
M3 is Relation-like Function-like set
N3 is Relation-like Function-like set
[M3,N3] is V15() set
{M3,N3} is functional non empty set
{M3} is functional non empty set
{{M3,N3},{M3}} is non empty set
N1 is non empty non void feasible strict Element of MSS_set A
MSS_morph (N1,F) is set
H is Relation-like Function-like set
G9 is Relation-like Function-like set
[H,G9] is V15() set
{H,G9} is functional non empty set
{H} is functional non empty set
{{H,G9},{H}} is non empty set
H * M3 is Relation-like Function-like set
G9 * N3 is Relation-like Function-like set
[(H * M3),(G9 * N3)] is V15() set
{(H * M3),(G9 * N3)} is functional non empty set
{(H * M3)} is functional non empty set
{{(H * M3),(G9 * N3)},{(H * M3)}} is non empty set
G is non empty non void feasible strict Element of MSS_set A
MSS_morph (F,G) is set
HG is Relation-like Function-like set
M1 is Relation-like Function-like set
[HG,M1] is V15() set
{HG,M1} is functional non empty set
{HG} is functional non empty set
{{HG,M1},{HG}} is non empty set
M3 * HG is Relation-like Function-like set
N3 * M1 is Relation-like Function-like set
[(M3 * HG),(N3 * M1)] is V15() set
{(M3 * HG),(N3 * M1)} is functional non empty set
{(M3 * HG)} is functional non empty set
{{(M3 * HG),(N3 * M1)},{(M3 * HG)}} is non empty set
MSS_morph (F,G) is set
H * (M3 * HG) is Relation-like Function-like set
(H * M3) * HG is Relation-like Function-like set
G9 * (N3 * M1) is Relation-like Function-like set
(G9 * N3) * M1 is Relation-like Function-like set
j is Element of the carrier of (A)
f is Element of the carrier of (A)
MSS_morph (N1,F) is set
e is Element of the carrier of (A)
j9 is Element of the carrier of (A)
( the Comp of (A) . (C,i9,MS)) . (M1,[(H * M3),(G9 * N3)]) is set
[M1,[(H * M3),(G9 * N3)]] is V15() set
{M1,[(H * M3),(G9 * N3)]} is non empty set
{{M1,[(H * M3),(G9 * N3)]},{M1}} is non empty set
( the Comp of (A) . (C,i9,MS)) . [M1,[(H * M3),(G9 * N3)]] is set
[((H * M3) * HG),((G9 * N3) * M1)] is V15() set
{((H * M3) * HG),((G9 * N3) * M1)} is functional non empty set
{((H * M3) * HG)} is functional non empty set
{{((H * M3) * HG),((G9 * N3) * M1)},{((H * M3) * HG)}} is non empty set
C is Element of the carrier of (A)
the Arrows of (A) . (C,C) is set
[C,C] is V15() set
{C,C} is non empty set
{C} is non empty set
{{C,C},{C}} is non empty set
the Arrows of (A) . [C,C] is set
MSS_set A is non empty MSS-membered set
i is non empty non void feasible strict Element of MSS_set A
the carrier of i is non empty set
id the carrier of i is Relation-like the carrier of i -defined the carrier of i -valued Function-like one-to-one non empty total Element of bool [: the carrier of i, the carrier of i:]
[: the carrier of i, the carrier of i:] is Relation-like non empty set
bool [: the carrier of i, the carrier of i:] is non empty set
the carrier' of i is non empty set
id the carrier' of i is Relation-like the carrier' of i -defined the carrier' of i -valued Function-like one-to-one non empty total Element of bool [: the carrier' of i, the carrier' of i:]
[: the carrier' of i, the carrier' of i:] is Relation-like non empty set
bool [: the carrier' of i, the carrier' of i:] is non empty set
[(id the carrier of i),(id the carrier' of i)] is V15() set
{(id the carrier of i),(id the carrier' of i)} is functional non empty set
{(id the carrier of i)} is functional non empty set
{{(id the carrier of i),(id the carrier' of i)},{(id the carrier of i)}} is non empty set
e is V15() set
MSS_morph (i,i) is set
j is Element of the carrier of (A)
the Arrows of (A) . (j,C) is set
[j,C] is V15() set
{j,C} is non empty set
{j} is non empty set
{{j,C},{j}} is non empty set
the Arrows of (A) . [j,C] is set
the Comp of (A) . (j,C,C) is Relation-like [:( the Arrows of (A) . (C,C)),( the Arrows of (A) . (j,C)):] -defined the Arrows of (A) . (j,C) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (A) . (C,C)),( the Arrows of (A) . (j,C)):],( the Arrows of (A) . (j,C)):]
[:( the Arrows of (A) . (C,C)),( the Arrows of (A) . (j,C)):] is Relation-like set
[:[:( the Arrows of (A) . (C,C)),( the Arrows of (A) . (j,C)):],( the Arrows of (A) . (j,C)):] is Relation-like set
bool [:[:( the Arrows of (A) . (C,C)),( the Arrows of (A) . (j,C)):],( the Arrows of (A) . (j,C)):] is non empty set
f is set
( the Comp of (A) . (j,C,C)) . (e,f) is set
[e,f] is V15() set
{e,f} is non empty set
{e} is non empty set
{{e,f},{e}} is non empty set
( the Comp of (A) . (j,C,C)) . [e,f] is set
j9 is non empty non void feasible strict Element of MSS_set A
MSS_morph (j9,i) is set
M1 is Relation-like Function-like set
N1 is Relation-like Function-like set
[M1,N1] is V15() set
{M1,N1} is functional non empty set
{M1} is functional non empty set
{{M1,N1},{M1}} is non empty set
proj2 N1 is set
proj2 M1 is set
M1 * (id the carrier of i) is Relation-like the carrier of i -valued Function-like set
I is Element of the carrier of (A)
J is Element of the carrier of (A)
the Comp of (A) . (I,J,J) is Relation-like [:( the Arrows of (A) . (J,J)),( the Arrows of (A) . (I,J)):] -defined the Arrows of (A) . (I,J) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (A) . (J,J)),( the Arrows of (A) . (I,J)):],( the Arrows of (A) . (I,J)):]
the Arrows of (A) . (J,J) is set
[J,J] is V15() set
{J,J} is non empty set
{J} is non empty set
{{J,J},{J}} is non empty set
the Arrows of (A) . [J,J] is set
the Arrows of (A) . (I,J) is set
[I,J] is V15() set
{I,J} is non empty set
{I} is non empty set
{{I,J},{I}} is non empty set
the Arrows of (A) . [I,J] is set
[:( the Arrows of (A) . (J,J)),( the Arrows of (A) . (I,J)):] is Relation-like set
[:[:( the Arrows of (A) . (J,J)),( the Arrows of (A) . (I,J)):],( the Arrows of (A) . (I,J)):] is Relation-like set
bool [:[:( the Arrows of (A) . (J,J)),( the Arrows of (A) . (I,J)):],( the Arrows of (A) . (I,J)):] is non empty set
( the Comp of (A) . (I,J,J)) . ([(id the carrier of i),(id the carrier' of i)],[M1,N1]) is set
[[(id the carrier of i),(id the carrier' of i)],[M1,N1]] is V15() set
{[(id the carrier of i),(id the carrier' of i)],[M1,N1]} is Relation-like non empty set
{[(id the carrier of i),(id the carrier' of i)]} is Relation-like Function-like non empty set
{{[(id the carrier of i),(id the carrier' of i)],[M1,N1]},{[(id the carrier of i),(id the carrier' of i)]}} is non empty set
( the Comp of (A) . (I,J,J)) . [[(id the carrier of i),(id the carrier' of i)],[M1,N1]] is set
N1 * (id the carrier' of i) is Relation-like the carrier' of i -valued Function-like set
[(M1 * (id the carrier of i)),(N1 * (id the carrier' of i))] is V15() set
{(M1 * (id the carrier of i)),(N1 * (id the carrier' of i))} is functional non empty set
{(M1 * (id the carrier of i))} is functional non empty set
{{(M1 * (id the carrier of i)),(N1 * (id the carrier' of i))},{(M1 * (id the carrier of i))}} is non empty set
C is Element of the carrier of (A)
the Arrows of (A) . (C,C) is set
[C,C] is V15() set
{C,C} is non empty set
{C} is non empty set
{{C,C},{C}} is non empty set
the Arrows of (A) . [C,C] is set
MSS_set A is non empty MSS-membered set
i is non empty non void feasible strict Element of MSS_set A
the carrier of i is non empty set
id the carrier of i is Relation-like the carrier of i -defined the carrier of i -valued Function-like one-to-one non empty total Element of bool [: the carrier of i, the carrier of i:]
[: the carrier of i, the carrier of i:] is Relation-like non empty set
bool [: the carrier of i, the carrier of i:] is non empty set
the carrier' of i is non empty set
id the carrier' of i is Relation-like the carrier' of i -defined the carrier' of i -valued Function-like one-to-one non empty total Element of bool [: the carrier' of i, the carrier' of i:]
[: the carrier' of i, the carrier' of i:] is Relation-like non empty set
bool [: the carrier' of i, the carrier' of i:] is non empty set
[(id the carrier of i),(id the carrier' of i)] is V15() set
{(id the carrier of i),(id the carrier' of i)} is functional non empty set
{(id the carrier of i)} is functional non empty set
{{(id the carrier of i),(id the carrier' of i)},{(id the carrier of i)}} is non empty set
e is V15() set
MSS_morph (i,i) is set
j is Element of the carrier of (A)
the Arrows of (A) . (C,j) is set
[C,j] is V15() set
{C,j} is non empty set
{{C,j},{C}} is non empty set
the Arrows of (A) . [C,j] is set
the Comp of (A) . (C,C,j) is Relation-like [:( the Arrows of (A) . (C,j)),( the Arrows of (A) . (C,C)):] -defined the Arrows of (A) . (C,j) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (A) . (C,j)),( the Arrows of (A) . (C,C)):],( the Arrows of (A) . (C,j)):]
[:( the Arrows of (A) . (C,j)),( the Arrows of (A) . (C,C)):] is Relation-like set
[:[:( the Arrows of (A) . (C,j)),( the Arrows of (A) . (C,C)):],( the Arrows of (A) . (C,j)):] is Relation-like set
bool [:[:( the Arrows of (A) . (C,j)),( the Arrows of (A) . (C,C)):],( the Arrows of (A) . (C,j)):] is non empty set
f is set
( the Comp of (A) . (C,C,j)) . (f,e) is set
[f,e] is V15() set
{f,e} is non empty set
{f} is non empty set
{{f,e},{f}} is non empty set
( the Comp of (A) . (C,C,j)) . [f,e] is set
j9 is non empty non void feasible strict Element of MSS_set A
MSS_morph (i,j9) is set
M1 is Relation-like Function-like set
N1 is Relation-like Function-like set
[M1,N1] is V15() set
{M1,N1} is functional non empty set
{M1} is functional non empty set
{{M1,N1},{M1}} is non empty set
proj1 N1 is set
proj1 M1 is set
(id the carrier of i) * M1 is Relation-like the carrier of i -defined Function-like set
I is Element of the carrier of (A)
J is Element of the carrier of (A)
the Comp of (A) . (I,I,J) is Relation-like [:( the Arrows of (A) . (I,J)),( the Arrows of (A) . (I,I)):] -defined the Arrows of (A) . (I,J) -valued Function-like quasi_total Element of bool [:[:( the Arrows of (A) . (I,J)),( the Arrows of (A) . (I,I)):],( the Arrows of (A) . (I,J)):]
the Arrows of (A) . (I,J) is set
[I,J] is V15() set
{I,J} is non empty set
{I} is non empty set
{{I,J},{I}} is non empty set
the Arrows of (A) . [I,J] is set
the Arrows of (A) . (I,I) is set
[I,I] is V15() set
{I,I} is non empty set
{{I,I},{I}} is non empty set
the Arrows of (A) . [I,I] is set
[:( the Arrows of (A) . (I,J)),( the Arrows of (A) . (I,I)):] is Relation-like set
[:[:( the Arrows of (A) . (I,J)),( the Arrows of (A) . (I,I)):],( the Arrows of (A) . (I,J)):] is Relation-like set
bool [:[:( the Arrows of (A) . (I,J)),( the Arrows of (A) . (I,I)):],( the Arrows of (A) . (I,J)):] is non empty set
( the Comp of (A) . (I,I,J)) . ([M1,N1],[(id the carrier of i),(id the carrier' of i)]) is set
[[M1,N1],[(id the carrier of i),(id the carrier' of i)]] is V15() set
{[M1,N1],[(id the carrier of i),(id the carrier' of i)]} is Relation-like non empty set
{[M1,N1]} is Relation-like Function-like non empty set
{{[M1,N1],[(id the carrier of i),(id the carrier' of i)]},{[M1,N1]}} is non empty set
( the Comp of (A) . (I,I,J)) . [[M1,N1],[(id the carrier of i),(id the carrier' of i)]] is set
(id the carrier' of i) * N1 is Relation-like the carrier' of i -defined Function-like set
[((id the carrier of i) * M1),((id the carrier' of i) * N1)] is V15() set
{((id the carrier of i) * M1),((id the carrier' of i) * N1)} is functional non empty set
{((id the carrier of i) * M1)} is functional non empty set
{{((id the carrier of i) * M1),((id the carrier' of i) * N1)},{((id the carrier of i) * M1)}} is non empty set
A is non empty set
(A) is non empty transitive strict associative with_units AltCatStr
S is non empty transitive associative with_units AltCatStr
the carrier of S is non empty set
C is Element of the carrier of S
MSS_set A is non empty MSS-membered set
o is non empty non void feasible strict Element of MSS_set A
A is non empty non void feasible ManySortedSign
the feasible MSAlgebra over A is feasible MSAlgebra over A
the Sorts of the feasible MSAlgebra over A is Relation-like the carrier of A -defined Function-like non empty total set
the carrier of A is non empty set
the Charact of the feasible MSAlgebra over A is Relation-like the carrier' of A -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Arity of A * ( the Sorts of the feasible MSAlgebra over A #), the ResultSort of A * the Sorts of the feasible MSAlgebra over A
the carrier' of A is non empty set
the Arity of A is Relation-like the carrier' of A -defined the carrier of A * -valued Function-like quasi_total Function-yielding V37() Element of bool [: the carrier' of A,( the carrier of A *):]
the carrier of A * is functional non empty V55() M8( the carrier of A)
[: the carrier' of A,( the carrier of A *):] is Relation-like non empty set
bool [: the carrier' of A,( the carrier of A *):] is non empty set
the Sorts of the feasible MSAlgebra over A # is Relation-like the carrier of A * -defined Function-like non empty total set
the Arity of A * ( the Sorts of the feasible MSAlgebra over A #) is Relation-like the carrier' of A -defined Function-like non empty total set
the ResultSort of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is Relation-like non empty set
bool [: the carrier' of A, the carrier of A:] is non empty set
the ResultSort of A * the Sorts of the feasible MSAlgebra over A is Relation-like the carrier' of A -defined Function-like non empty total set
MSAlgebra(# the Sorts of the feasible MSAlgebra over A, the Charact of the feasible MSAlgebra over A #) is strict MSAlgebra over A
C is strict MSAlgebra over A
o is Element of the carrier' of A
Args (o, the feasible MSAlgebra over A) is Element of proj2 ( the Sorts of the feasible MSAlgebra over A #)
proj2 ( the Sorts of the feasible MSAlgebra over A #) is non empty set
the Sorts of C is Relation-like the carrier of A -defined Function-like non empty total set
the Sorts of C # is Relation-like the carrier of A * -defined Function-like non empty total set
the Arity of A * ( the Sorts of C #) is Relation-like the carrier' of A -defined Function-like non empty total set
( the Arity of A * ( the Sorts of C #)) . o is set
Args (o,C) is Element of proj2 ( the Sorts of C #)
proj2 ( the Sorts of C #) is non empty set
Result (o, the feasible MSAlgebra over A) is Element of proj2 the Sorts of the feasible MSAlgebra over A
proj2 the Sorts of the feasible MSAlgebra over A is non empty set
the ResultSort of A * the Sorts of C is Relation-like the carrier' of A -defined Function-like non empty total set
( the ResultSort of A * the Sorts of C) . o is set
Result (o,C) is Element of proj2 the Sorts of C
proj2 the Sorts of C is non empty set
A is non empty non void feasible ManySortedSign
S is non empty set
C is set
o is set
GM is set
C is strict feasible MSAlgebra over A
the Sorts of C is Relation-like the carrier of A -defined Function-like non empty total set
the carrier of A is non empty set
the Charact of C is Relation-like the carrier' of A -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Arity of A * ( the Sorts of C #), the ResultSort of A * the Sorts of C
the carrier' of A is non empty set
the Arity of A is Relation-like the carrier' of A -defined the carrier of A * -valued Function-like quasi_total Function-yielding V37() Element of bool [: the carrier' of A,( the carrier of A *):]
the carrier of A * is functional non empty V55() M8( the carrier of A)
[: the carrier' of A,( the carrier of A *):] is Relation-like non empty set
bool [: the carrier' of A,( the carrier of A *):] is non empty set
the Sorts of C # is Relation-like the carrier of A * -defined Function-like non empty total set
the Arity of A * ( the Sorts of C #) is Relation-like the carrier' of A -defined Function-like non empty total set
the ResultSort of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is Relation-like non empty set
bool [: the carrier' of A, the carrier of A:] is non empty set
the ResultSort of A * the Sorts of C is Relation-like the carrier' of A -defined Function-like non empty total set
[ the Sorts of C, the Charact of C] is V15() set
{ the Sorts of C, the Charact of C} is functional non empty set
{ the Sorts of C} is functional non empty set
{{ the Sorts of C, the Charact of C},{ the Sorts of C}} is non empty set
i is strict feasible MSAlgebra over A
the Sorts of i is Relation-like the carrier of A -defined Function-like non empty total set
the Charact of i is Relation-like the carrier' of A -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Arity of A * ( the Sorts of i #), the ResultSort of A * the Sorts of i
the Sorts of i # is Relation-like the carrier of A * -defined Function-like non empty total set
the Arity of A * ( the Sorts of i #) is Relation-like the carrier' of A -defined Function-like non empty total set
the ResultSort of A * the Sorts of i is Relation-like the carrier' of A -defined Function-like non empty total set
[ the Sorts of i, the Charact of i] is V15() set
{ the Sorts of i, the Charact of i} is functional non empty set
{ the Sorts of i} is functional non empty set
{{ the Sorts of i, the Charact of i},{ the Sorts of i}} is non empty set
the carrier of A is non empty set
bool S is non empty set
Funcs ( the carrier of A,(bool S)) is non empty FUNCTION_DOMAIN of the carrier of A, bool S
the carrier' of A is non empty set
PFuncs (NAT,S) is set
PFuncs ((PFuncs (NAT,S)),S) is set
Funcs ( the carrier' of A,(PFuncs ((PFuncs (NAT,S)),S))) is set
[:(Funcs ( the carrier of A,(bool S))),(Funcs ( the carrier' of A,(PFuncs ((PFuncs (NAT,S)),S)))):] is Relation-like set
C is set
o is set
GM is set
C is strict feasible MSAlgebra over A
the Sorts of C is Relation-like the carrier of A -defined Function-like non empty total set
the Charact of C is Relation-like the carrier' of A -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Arity of A * ( the Sorts of C #), the ResultSort of A * the Sorts of C
the Arity of A is Relation-like the carrier' of A -defined the carrier of A * -valued Function-like quasi_total Function-yielding V37() Element of bool [: the carrier' of A,( the carrier of A *):]
the carrier of A * is functional non empty V55() M8( the carrier of A)
[: the carrier' of A,( the carrier of A *):] is Relation-like non empty set
bool [: the carrier' of A,( the carrier of A *):] is non empty set
the Sorts of C # is Relation-like the carrier of A * -defined Function-like non empty total set
the Arity of A * ( the Sorts of C #) is Relation-like the carrier' of A -defined Function-like non empty total set
the ResultSort of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is Relation-like non empty set
bool [: the carrier' of A, the carrier of A:] is non empty set
the ResultSort of A * the Sorts of C is Relation-like the carrier' of A -defined Function-like non empty total set
[ the Sorts of C, the Charact of C] is V15() set
{ the Sorts of C, the Charact of C} is functional non empty set
{ the Sorts of C} is functional non empty set
{{ the Sorts of C, the Charact of C},{ the Sorts of C}} is non empty set
C is strict feasible MSAlgebra over A
the Sorts of C is Relation-like the carrier of A -defined Function-like non empty total set
the Charact of C is Relation-like the carrier' of A -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Arity of A * ( the Sorts of C #), the ResultSort of A * the Sorts of C
the Arity of A is Relation-like the carrier' of A -defined the carrier of A * -valued Function-like quasi_total Function-yielding V37() Element of bool [: the carrier' of A,( the carrier of A *):]
the carrier of A * is functional non empty V55() M8( the carrier of A)
[: the carrier' of A,( the carrier of A *):] is Relation-like non empty set
bool [: the carrier' of A,( the carrier of A *):] is non empty set
the Sorts of C # is Relation-like the carrier of A * -defined Function-like non empty total set
the Arity of A * ( the Sorts of C #) is Relation-like the carrier' of A -defined Function-like non empty total set
the ResultSort of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is Relation-like non empty set
bool [: the carrier' of A, the carrier of A:] is non empty set
the ResultSort of A * the Sorts of C is Relation-like the carrier' of A -defined Function-like non empty total set
[ the Sorts of C, the Charact of C] is V15() set
{ the Sorts of C, the Charact of C} is functional non empty set
{ the Sorts of C} is functional non empty set
{{ the Sorts of C, the Charact of C},{ the Sorts of C}} is non empty set
i is strict feasible MSAlgebra over A
the Sorts of i is Relation-like the carrier of A -defined Function-like non empty total set
proj2 the Sorts of i is non empty set
i9 is Element of proj2 the Sorts of i
dom the Sorts of i is non empty Element of bool the carrier of A
bool the carrier of A is non empty set
MS is set
the Sorts of i . MS is set
e is strict feasible MSAlgebra over A
the Sorts of e is Relation-like the carrier of A -defined Function-like non empty total set
the Charact of e is Relation-like the carrier' of A -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Arity of A * ( the Sorts of e #), the ResultSort of A * the Sorts of e
the Sorts of e # is Relation-like the carrier of A * -defined Function-like non empty total set
the Arity of A * ( the Sorts of e #) is Relation-like the carrier' of A -defined Function-like non empty total set
the ResultSort of A * the Sorts of e is Relation-like the carrier' of A -defined Function-like non empty total set
[ the Sorts of e, the Charact of e] is V15() set
{ the Sorts of e, the Charact of e} is functional non empty set
{ the Sorts of e} is functional non empty set
{{ the Sorts of e, the Charact of e},{ the Sorts of e}} is non empty set
e is Relation-like Function-like set
proj1 e is set
proj2 e is set
e . MS is set
GM is strict feasible MSAlgebra over A
the Sorts of GM is Relation-like the carrier of A -defined Function-like non empty total set
proj2 the Sorts of GM is non empty set
dom the Sorts of GM is non empty Element of bool the carrier of A
bool the carrier of A is non empty set
[: the carrier of A,(proj2 the Sorts of GM):] is Relation-like non empty set
bool [: the carrier of A,(proj2 the Sorts of GM):] is non empty set
i is set
i9 is Element of proj2 the Sorts of GM
[: the carrier of A,(bool S):] is Relation-like non empty set
bool [: the carrier of A,(bool S):] is non empty set
C is Relation-like the carrier of A -defined proj2 the Sorts of GM -valued Function-like quasi_total Element of bool [: the carrier of A,(proj2 the Sorts of GM):]
the Charact of GM is Relation-like the carrier' of A -defined Function-like non empty total Function-yielding V37() ManySortedFunction of the Arity of A * ( the Sorts of GM #), the ResultSort of A * the Sorts of GM
the Sorts of GM # is Relation-like the carrier of A * -defined Function-like non empty total set
the Arity of A * ( the Sorts of GM #) is Relation-like the carrier' of A -defined Function-like non empty total set
the ResultSort of A * the Sorts of GM is Relation-like the carrier' of A -defined Function-like non empty total set
[ the Sorts of GM, the Charact of GM] is V15() set
{ the Sorts of GM, the Charact of GM} is functional non empty set
{ the Sorts of GM} is functional non empty set
{{ the Sorts of GM, the Charact of GM},{ the Sorts of GM}} is non empty set
i9 is set
dom the Charact of GM is non empty Element of bool the carrier' of A
bool the carrier' of A is non empty set
proj2 the Charact of GM is non empty set
j is set
MS is Relation-like the carrier' of A -defined Function-like non empty total set
e is Relation-like the carrier' of A -defined Function-like non empty total set
f is set
the Charact of GM . f is Relation-like Function-like set
MS . f is set
e . f is set
[:(MS . f),(e . f):] is Relation-like set
bool [:(MS . f),(e . f):] is non empty set
j9 is Relation-like the carrier' of A -defined Function-like non empty total Function-yielding V37() ManySortedFunction of MS,e
j9 . f is Relation-like Function-like set
dom MS is non empty Element of bool the carrier' of A
the Arity of A . f is Relation-like NAT -defined Function-like V28() V53() V54() set
M1 is set
( the Sorts of GM #) . ( the Arity of A . f) is set
J is Relation-like NAT -defined the carrier of A -valued Function-like V28() V53() V54() Element of the