:: MSINST_1 semantic presentation

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 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
[:(),():] is Relation-like non empty set

[:(),(),():] is non empty set
{|C,C|} is Relation-like [:(),(),():] -defined Function-like non empty total set
{|C|} is Relation-like [:(),(),():] -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],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,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,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),(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,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,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],[N1,F]},{[F,G]}} is non empty 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 [:(),(),():] -defined Function-like non empty total Function-yielding V37() ManySortedFunction of {|C,C|},{|C|}
AltCatStr(# (),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,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,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],[e,j]},{[j9,f]}} is non empty set
( the Comp of C . (i,i9,MS)) . [[j9,f],[e,j]] is 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],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],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,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,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],[j9,f]},{[I,J]}} is non empty set
( the Comp of GM . (MS,e,j)) . [[I,J],[j9,f]] is 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
[:(),():] is Relation-like non empty set
[:(),(),():] is non empty 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 . (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],j},{[MS,e]}} is non empty set
i is Relation-like [:(),(),():] -defined Function-like non empty total set
i . (MS,e,j) is set
i . [MS,e,j] is set
i9 is Relation-like [:(),(),():] -defined Function-like non empty total set
i9 . (MS,e,j) is set
i9 . [MS,e,j] is set
{|GM,GM|} is Relation-like [:(),(),():] -defined Function-like non empty total set
{|GM,GM|} . [MS,e,j] is set
{|GM|} is Relation-like [:(),(),():] -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 [:(),(),():] -defined Function-like non empty total set
{|C,C|} . [MS,e,j] is set
{|C|} is Relation-like [:(),(),():] -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,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,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),(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,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,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),(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,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,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),(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,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),(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,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,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

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

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

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

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