:: 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