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