:: CATALG_1 semantic presentation

REAL is set
NAT is V6() V7() V8() non empty Element of bool REAL
bool REAL is non empty set
NAT is V6() V7() V8() non empty set
bool NAT is non empty set
bool NAT is non empty set

bool is non empty set
bool () is non empty set

1 is V6() V7() V8() V12() non empty Element of NAT
{{},1} is non empty set
K387() is set
bool K387() is non empty set
K388() is Element of bool K387()
K428() is non empty V161() L15()
the carrier of K428() is non empty set
K391( the carrier of K428()) is non empty M36( the carrier of K428())
K427(K428()) is Element of bool K391( the carrier of K428())
bool K391( the carrier of K428()) is non empty set

bool [:K427(K428()),NAT:] is non empty set

bool [:NAT,K427(K428()):] is non empty set
2 is V6() V7() V8() V12() non empty Element of NAT
3 is V6() V7() V8() V12() non empty Element of NAT

Seg 1 is non empty V24() V31(1) Element of bool NAT
{1} is non empty set
Seg 2 is non empty V24() V31(2) Element of bool NAT
{1,2} is non empty set
Seg 3 is non empty V24() V31(3) Element of bool NAT
{1,2,3} is non empty set

C1 is set

S2 is set
proj1 S1 is set
S1 . S2 is set
dom S1 is Element of bool C1
bool C1 is non empty set
C2 . S2 is set
F | (C2 . S2) is Relation-like Function-like set

A1 is set

C2 . A1 is set
F | (C2 . A1) is Relation-like Function-like set

C1 is set

Union C2 is set
id (Union C2) is Relation-like Union C2 -defined Union C2 -valued Function-like one-to-one total V36( Union C2, Union C2) Element of bool [:(Union C2),(Union C2):]
[:(Union C2),(Union C2):] is Relation-like set
bool [:(Union C2),(Union C2):] is non empty set
(C1,C2,(id (Union C2))) is Relation-like C1 -defined Function-like total Function-yielding V78() set

proj2 C2 is set
union (proj2 C2) is set
S2 is set
dom C2 is Element of bool C1
bool C1 is non empty set
C2 . S2 is set
(C1,C2,(id (Union C2))) . S2 is Relation-like Function-like set
(id (Union C2)) | (C2 . S2) is Relation-like Union C2 -defined C2 . S2 -defined Union C2 -defined Union C2 -valued Function-like Element of bool [:(Union C2),(Union C2):]
(id C2) . S2 is Relation-like Function-like set
id (C2 . S2) is Relation-like C2 . S2 -defined C2 . S2 -valued Function-like one-to-one total V36(C2 . S2,C2 . S2) Element of bool [:(C2 . S2),(C2 . S2):]
[:(C2 . S2),(C2 . S2):] is Relation-like set
bool [:(C2 . S2),(C2 . S2):] is non empty set
C1 is set

(C1,C2,S1) is Relation-like C1 -defined Function-like total Function-yielding V78() set
rngs (C1,C2,S1) is Relation-like C1 -defined Function-like total set

(C1,C2,(S1 * S2)) is Relation-like C1 -defined Function-like total Function-yielding V78() set
(C1,F,S2) is Relation-like C1 -defined Function-like total Function-yielding V78() set
(C1,F,S2) ** (C1,C2,S1) is Relation-like Function-like Function-yielding V78() set
C1 /\ C1 is set
dom (C1,F,S2) is Element of bool C1
bool C1 is non empty set
dom (C1,C2,S1) is Element of bool C1
proj1 ((C1,F,S2) ** (C1,C2,S1)) is set
A1 is set
(C1,C2,S1) . A1 is Relation-like Function-like set
C2 . A1 is set
S1 | (C2 . A1) is Relation-like Function-like set
(rngs (C1,C2,S1)) . A1 is set
proj2 (S1 | (C2 . A1)) is set
F . A1 is set
(S1 * S2) | (C2 . A1) is Relation-like Function-like set
(S1 | (C2 . A1)) * S2 is Relation-like Function-like set
(F . A1) |` (S1 | (C2 . A1)) is Relation-like Function-like set
S2 | (F . A1) is Relation-like Function-like set
(S1 | (C2 . A1)) * (S2 | (F . A1)) is Relation-like Function-like set
(C1,C2,(S1 * S2)) . A1 is Relation-like Function-like set
(C1,F,S2) . A1 is Relation-like Function-like set
((C1,F,S2) ** (C1,C2,S1)) . A1 is Relation-like Function-like set
dom (C1,C2,(S1 * S2)) is Element of bool C1

proj1 C1 is set
C2 is set

(C2,F,C1) is Relation-like C2 -defined Function-like total Function-yielding V78() set
S2 is set
(C2,F,C1) . S2 is Relation-like Function-like set
F . S2 is set
S1 . S2 is set
[:(F . S2),(S1 . S2):] is Relation-like set
bool [:(F . S2),(S1 . S2):] is non empty set
C1 | (F . S2) is Relation-like Function-like set
C1 .: (F . S2) is set
proj2 ((C2,F,C1) . S2) is set
proj1 ((C2,F,C1) . S2) is set
C1 is set

C2 is set

<*C1*> . 1 is set
C1 is non empty feasible feasible ManySortedSign
C1 is non empty feasible feasible ManySortedSign
C2 is MSAlgebra over C1
the Sorts of C2 is Relation-like the carrier of C1 -defined Function-like non empty total set
the carrier of C1 is non empty set
C1 is non empty non void feasible feasible ManySortedSign
the carrier of C1 is non empty set

C1 is non empty non void feasible feasible ManySortedSign
C2 is (C1) MSAlgebra over C1
the Sorts of C2 is Relation-like the carrier of C1 -defined Function-like non empty total set
the carrier of C1 is non empty set
the non empty non void feasible feasible ManySortedSign is non empty non void feasible feasible ManySortedSign
the ( the non empty non void feasible feasible ManySortedSign ) MSAlgebra over the non empty non void feasible feasible ManySortedSign is ( the non empty non void feasible feasible ManySortedSign ) MSAlgebra over the non empty non void feasible feasible ManySortedSign
the Sorts of the ( the non empty non void feasible feasible ManySortedSign ) MSAlgebra over the non empty non void feasible feasible ManySortedSign is Relation-like non empty-yielding the carrier of the non empty non void feasible feasible ManySortedSign -defined Function-like non empty total set
the carrier of the non empty non void feasible feasible ManySortedSign is non empty set

C1 is set

[:,(2 -tuples_on C1):] is Relation-like set

[:{1},(1 -tuples_on C1):] is Relation-like set
{2} is non empty set

[:{2},(3 -tuples_on C1):] is Relation-like set
[:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] is Relation-like set
[:,(2 -tuples_on C1):] * is functional non empty FinSequence-membered FinSequenceSet of [:,(2 -tuples_on C1):]
C2 is set
C2 `2 is set

{ } is set

len S1 is V6() V7() V8() V12() Element of NAT
S1 . 1 is set
S2 is set

[1,<*S2*>] is V21() set
{1,<*S2*>} is non empty set
{{1,<*S2*>},{1}} is non empty set
A1 is set

[0,<*S2,A1*>] is V21() set
{0,<*S2,A1*>} is functional non empty set
{{0,<*S2,A1*>},} is non empty set
A2 is set

[2,<*S2,A1,A2*>] is V21() set
{2,<*S2,A1,A2*>} is non empty set
{{2,<*S2,A1,A2*>},{2}} is non empty set

[0,<*A1,A2*>] is V21() set
{0,<*A1,A2*>} is functional non empty set
{{0,<*A1,A2*>},} is non empty set

{S2} is non empty set
rng S1 is Element of bool C1
bool C1 is non empty set
C2 `1 is set
C2 `2 is set

{ } is set

len F is V6() V7() V8() V12() Element of NAT
F . 1 is set
F . 2 is set
F . 3 is set
<*(F . 1),(F . 2),(F . 3)*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set
rng F is Element of bool C1
bool C1 is non empty set
{(F . 1),(F . 2),(F . 3)} is non empty set
<*(F . 2),(F . 3)*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set
[0,<*(F . 2),(F . 3)*>] is V21() set
{0,<*(F . 2),(F . 3)*>} is functional non empty set
{{0,<*(F . 2),(F . 3)*>},} is non empty set
<*(F . 1),(F . 2)*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set
[0,<*(F . 1),(F . 2)*>] is V21() set
{0,<*(F . 1),(F . 2)*>} is functional non empty set
{{0,<*(F . 1),(F . 2)*>},} is non empty set
<*[0,<*(F . 2),(F . 3)*>],[0,<*(F . 1),(F . 2)*>]*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set

A2 is non empty set

[:,(2 -tuples_on A2):] is Relation-like non empty set
G is Element of [:,(2 -tuples_on A2):]

B1 is Element of [:,(2 -tuples_on A2):]

[1,<*(F . 1)*>] is V21() set
{1,<*(F . 1)*>} is non empty set
{{1,<*(F . 1)*>},{1}} is non empty set
[2,<*(F . 1),(F . 2),(F . 3)*>] is V21() set
{2,<*(F . 1),(F . 2),(F . 3)*>} is non empty set
{{2,<*(F . 1),(F . 2),(F . 3)*>},{2}} is non empty set
C2 `1 is set

proj1 C2 is set
proj2 C2 is set
[:([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),([:,(2 -tuples_on C1):] *):] is Relation-like set
bool [:([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),([:,(2 -tuples_on C1):] *):] is non empty set
S1 is set
S1 `2 is set

{ } is set

len S2 is V6() V7() V8() V12() Element of NAT
S2 . 1 is set

{(S2 . 1)} is non empty set
rng S2 is Element of bool C1
bool C1 is non empty set
<*(S2 . 1),(S2 . 1)*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set
[0,<*(S2 . 1),(S2 . 1)*>] is V21() set
{0,<*(S2 . 1),(S2 . 1)*>} is functional non empty set
{{0,<*(S2 . 1),(S2 . 1)*>},} is non empty set
G is V21() set
B1 is non empty set
H is Element of B1

[1,<*H*>] is V21() set
{1,<*H*>} is non empty set
{{1,<*H*>},{1}} is non empty set

[0,<*H,H*>] is V21() set
{0,<*H,H*>} is functional non empty set
{{0,<*H,H*>},} is non empty set
<*H,(S2 . 1),(S2 . 1)*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set
[2,<*H,(S2 . 1),(S2 . 1)*>] is V21() set
{2,<*H,(S2 . 1),(S2 . 1)*>} is non empty set
{{2,<*H,(S2 . 1),(S2 . 1)*>},{2}} is non empty set

[0,<*H,(S2 . 1)*>] is V21() set
{0,<*H,(S2 . 1)*>} is functional non empty set
{{0,<*H,(S2 . 1)*>},} is non empty set
S1 `1 is set

[1,<*H*>] is V21() set
{1,<*H*>} is non empty set
{{1,<*H*>},{1}} is non empty set
[0,<*H,H*>] is V21() set
{0,<*H,H*>} is functional non empty set
{{0,<*H,H*>},} is non empty set
S1 `2 is set

{ } is set

len S2 is V6() V7() V8() V12() Element of NAT
S2 . 1 is set
S2 . 2 is set
S2 . 3 is set
<*(S2 . 1),(S2 . 2),(S2 . 3)*> is Relation-like NAT -defined Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like set
rng S2 is Element of bool C1
bool C1 is non empty set
{(S2 . 1),(S2 . 2),(S2 . 3)} is non empty set
<*(S2 . 1),(S2 . 3)*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set
[0,<*(S2 . 1),(S2 . 3)*>] is V21() set
{0,<*(S2 . 1),(S2 . 3)*>} is functional non empty set
{{0,<*(S2 . 1),(S2 . 3)*>},} is non empty set
B1 is V21() set
G is non empty set

[1,<*(S2 . 1)*>] is V21() set
{1,<*(S2 . 1)*>} is non empty set
{{1,<*(S2 . 1)*>},{1}} is non empty set
<*(S2 . 1),(S2 . 1)*> is Relation-like NAT -defined Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like set
[0,<*(S2 . 1),(S2 . 1)*>] is V21() set
{0,<*(S2 . 1),(S2 . 1)*>} is functional non empty set
{{0,<*(S2 . 1),(S2 . 1)*>},} is non empty set
[2,<*(S2 . 1),(S2 . 2),(S2 . 3)*>] is V21() set
{2,<*(S2 . 1),(S2 . 2),(S2 . 3)*>} is non empty set
{{2,<*(S2 . 1),(S2 . 2),(S2 . 3)*>},{2}} is non empty set
S1 `1 is set

proj1 S1 is set
proj2 S1 is set
[:([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),[:,(2 -tuples_on C1):]:] is Relation-like set
bool [:([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),[:,(2 -tuples_on C1):]:] is non empty set
F is Relation-like [:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] -defined [:,(2 -tuples_on C1):] * -valued Function-like total V36([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):],[:,(2 -tuples_on C1):] * ) Function-yielding V78() Element of bool [:([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),([:,(2 -tuples_on C1):] *):]
S2 is Relation-like [:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] -defined [:,(2 -tuples_on C1):] -valued Function-like V36([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):],[:,(2 -tuples_on C1):]) Element of bool [:([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),[:,(2 -tuples_on C1):]:]
ManySortedSign(# [:,(2 -tuples_on C1):],([:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):]),F,S2 #) is strict ManySortedSign

the carrier of A1 is set
the carrier' of A1 is set
the Arity of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 * -valued Function-like total V36( the carrier' of A1, the carrier of A1 * ) Function-yielding V78() Element of bool [: the carrier' of A1,( the carrier of A1 *):]
the carrier of A1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of A1
[: the carrier' of A1,( the carrier of A1 *):] is Relation-like set
bool [: the carrier' of A1,( the carrier of A1 *):] is non empty set
the ResultSort of A1 is Relation-like the carrier' of A1 -defined the carrier of A1 -valued Function-like V36( the carrier' of A1, the carrier of A1) Element of bool [: the carrier' of A1, the carrier of A1:]
[: the carrier' of A1, the carrier of A1:] is Relation-like set
bool [: the carrier' of A1, the carrier of A1:] is non empty set
A2 is set
f is non empty set
G is Element of f

[1,<*A2*>] is V21() set
{1,<*A2*>} is non empty set
{{1,<*A2*>},{1}} is non empty set
S2 . [1,<*A2*>] is set
B1 is set
H is set
o is set

[1,<*B1*>] is V21() set
{1,<*B1*>} is non empty set
{{1,<*B1*>},{1}} is non empty set

[0,<*B1,B1*>] is V21() set
{0,<*B1,B1*>} is functional non empty set
{{0,<*B1,B1*>},} is non empty set

[2,<*B1,H,o*>] is V21() set
{2,<*B1,H,o*>} is non empty set
{{2,<*B1,H,o*>},{2}} is non empty set

[0,<*B1,o*>] is V21() set
{0,<*B1,o*>} is functional non empty set
{{0,<*B1,o*>},} is non empty set

x is set
a is set
b is set

[1,<*x*>] is V21() set
{1,<*x*>} is non empty set
{{1,<*x*>},{1}} is non empty set

[2,<*x,a,b*>] is V21() set
{2,<*x,a,b*>} is non empty set
{{2,<*x,a,b*>},{2}} is non empty set

[0,<*a,b*>] is V21() set
{0,<*a,b*>} is functional non empty set
{{0,<*a,b*>},} is non empty set

[0,<*x,a*>] is V21() set
{0,<*x,a*>} is functional non empty set
{{0,<*x,a*>},} is non empty set

<*A2*> . 1 is set
<*B1*> . 1 is set
the ResultSort of A1 . [1,<*A2*>] is set

[0,<*A2,A2*>] is V21() set
{0,<*A2,A2*>} is functional non empty set
{{0,<*A2,A2*>},} is non empty set
A2 is set
f is set
G is set

[2,<*A2,f,G*>] is V21() set
{2,<*A2,f,G*>} is non empty set
{{2,<*A2,f,G*>},{2}} is non empty set

[0,<*f,G*>] is V21() set
{0,<*f,G*>} is functional non empty set
{{0,<*f,G*>},} is non empty set

[0,<*A2,f*>] is V21() set
{0,<*A2,f*>} is functional non empty set
{{0,<*A2,f*>},} is non empty set

the ResultSort of A1 . [2,<*A2,f,G*>] is set

[0,<*A2,G*>] is V21() set
{0,<*A2,G*>} is functional non empty set
{{0,<*A2,G*>},} is non empty set
B1 is non empty set
H is Element of B1
o is Element of B1
x is Element of B1

a is set
b is set
c is set

[1,<*a*>] is V21() set
{1,<*a*>} is non empty set
{{1,<*a*>},{1}} is non empty set

[2,<*a,b,c*>] is V21() set
{2,<*a,b,c*>} is non empty set
{{2,<*a,b,c*>},{2}} is non empty set

[0,<*b,c*>] is V21() set
{0,<*b,c*>} is functional non empty set
{{0,<*b,c*>},} is non empty set

[0,<*a,b*>] is V21() set
{0,<*a,b*>} is functional non empty set
{{0,<*a,b*>},} is non empty set

S2 . [2,<*A2,f,G*>] is set
g is set
h is set
gh is set

[1,<*g*>] is V21() set
{1,<*g*>} is non empty set
{{1,<*g*>},{1}} is non empty set

[0,<*g,g*>] is V21() set
{0,<*g,g*>} is functional non empty set
{{0,<*g,g*>},} is non empty set

[2,<*g,h,gh*>] is V21() set
{2,<*g,h,gh*>} is non empty set
{{2,<*g,h,gh*>},{2}} is non empty set

[0,<*g,gh*>] is V21() set
{0,<*g,gh*>} is functional non empty set
{{0,<*g,gh*>},} is non empty set
<*A2,f,G*> . 1 is set
<*g,h,gh*> . 1 is set
<*A2,f,G*> . 3 is set

the carrier of C2 is set
the carrier' of C2 is set
the Arity of C2 is Relation-like the carrier' of C2 -defined the carrier of C2 * -valued Function-like total V36( the carrier' of C2, the carrier of C2 * ) Function-yielding V78() Element of bool [: the carrier' of C2,( the carrier of C2 *):]
the carrier of C2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of C2
[: the carrier' of C2,( the carrier of C2 *):] is Relation-like set
bool [: the carrier' of C2,( the carrier of C2 *):] is non empty set
the ResultSort of C2 is Relation-like the carrier' of C2 -defined the carrier of C2 -valued Function-like V36( the carrier' of C2, the carrier of C2) Element of bool [: the carrier' of C2, the carrier of C2:]
[: the carrier' of C2, the carrier of C2:] is Relation-like set
bool [: the carrier' of C2, the carrier of C2:] is non empty set

the carrier of F is set
the carrier' of F is set
the Arity of F is Relation-like the carrier' of F -defined the carrier of F * -valued Function-like total V36( the carrier' of F, the carrier of F * ) Function-yielding V78() Element of bool [: the carrier' of F,( the carrier of F *):]
the carrier of F * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F
[: the carrier' of F,( the carrier of F *):] is Relation-like set
bool [: the carrier' of F,( the carrier of F *):] is non empty set
the ResultSort of F is Relation-like the carrier' of F -defined the carrier of F -valued Function-like V36( the carrier' of F, the carrier of F) Element of bool [: the carrier' of F, the carrier of F:]
[: the carrier' of F, the carrier of F:] is Relation-like set
bool [: the carrier' of F, the carrier of F:] is non empty set
S1 is set
S1 `1 is set
S1 `2 is set
S2 is set
A1 is set
A2 is set

[2,(S1 `2)] is V21() set
{2,(S1 `2)} is non empty set
{{2,(S1 `2)},{2}} is non empty set

[0,<*A1,A2*>] is V21() set
{0,<*A1,A2*>} is functional non empty set
{{0,<*A1,A2*>},} is non empty set

[0,<*S2,A1*>] is V21() set
{0,<*S2,A1*>} is functional non empty set
{{0,<*S2,A1*>},} is non empty set

[1,(S1 `2)] is V21() set
{1,(S1 `2)} is non empty set
{{1,(S1 `2)},{1}} is non empty set

S2 is set

S2 is set

[(S1 `1),(S1 `2)] is V21() set
{(S1 `1),(S1 `2)} is non empty set
{(S1 `1)} is non empty set
{{(S1 `1),(S1 `2)},{(S1 `1)}} is non empty set

S1 is set
S1 `1 is set
S1 `2 is set
S2 is set
A1 is set
A2 is set

[2,(S1 `2)] is V21() set
{2,(S1 `2)} is non empty set
{{2,(S1 `2)},{2}} is non empty set
the ResultSort of C2 . [2,(S1 `2)] is set

[0,<*S2,A2*>] is V21() set
{0,<*S2,A2*>} is functional non empty set
{{0,<*S2,A2*>},} is non empty set
the ResultSort of F . [2,(S1 `2)] is set
S2 is set

[1,(S1 `2)] is V21() set
{1,(S1 `2)} is non empty set
{{1,(S1 `2)},{1}} is non empty set
the ResultSort of C2 . [1,(S1 `2)] is set

[0,<*S2,S2*>] is V21() set
{0,<*S2,S2*>} is functional non empty set
{{0,<*S2,S2*>},} is non empty set
the ResultSort of F . [1,(S1 `2)] is set
[(S1 `1),(S1 `2)] is V21() set
{(S1 `1),(S1 `2)} is non empty set
{(S1 `1)} is non empty set
{{(S1 `1),(S1 `2)},{(S1 `1)}} is non empty set
the ResultSort of C2 . S1 is set
the ResultSort of F . S1 is set
dom the Arity of C2 is Element of bool the carrier' of C2
bool the carrier' of C2 is non empty set
dom the Arity of F is Element of bool the carrier' of F
bool the carrier' of F is non empty set
dom the ResultSort of C2 is Element of bool the carrier' of C2
dom the ResultSort of F is Element of bool the carrier' of F
C1 is set
(C1) is strict ManySortedSign
the carrier of (C1) is set
the carrier' of (C1) is set

[:,(2 -tuples_on C1):] is Relation-like set

[:{1},(1 -tuples_on C1):] is Relation-like set
[:{2},(3 -tuples_on C1):] is Relation-like set
[:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] is Relation-like set
C1 is non empty set
(C1) is strict feasible ManySortedSign
the carrier of (C1) is set

[:,(2 -tuples_on C1):] is Relation-like non empty set
the carrier' of (C1) is set

[:{1},(1 -tuples_on C1):] is Relation-like non empty set

[:{2},(3 -tuples_on C1):] is Relation-like non empty set
[:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] is Relation-like non empty set
C1 is non empty feasible feasible ManySortedSign
the carrier of C1 is non empty set
C2 is set
(C2) is strict feasible ManySortedSign

[:,(2 -tuples_on C2):] is Relation-like set
the Element of the carrier of C1 is Element of the carrier of C1
S1 is set
S2 is set
[S1,S2] is V21() set
{S1,S2} is non empty set
{S1} is non empty set
{{S1,S2},{S1}} is non empty set

{ } is set

len A1 is V6() V7() V8() V12() Element of NAT
dom A1 is Element of bool NAT
A1 . 1 is set
rng A1 is Element of bool C2
bool C2 is non empty set
A2 is non empty set
the carrier' of (C2) is set

[:{1},(1 -tuples_on C2):] is Relation-like set

[:{2},(3 -tuples_on C2):] is Relation-like set
[:{1},(1 -tuples_on C2):] \/ [:{2},(3 -tuples_on C2):] is Relation-like set
f is Element of A2

the carrier' of C1 is set
() is non empty non void feasible strict feasible ManySortedSign
C1 is non empty non void feasible strict feasible ManySortedSign
the carrier of C1 is non empty set

[:,():] is Relation-like non empty set
C1 is set
(C1) is strict feasible ManySortedSign

[:,(2 -tuples_on C1):] is Relation-like set
the carrier of (C1) is set

the carrier of F is set
C1 is set
C2 is set
F is feasible (C1)
(C2) is strict feasible ManySortedSign
the carrier of F is set

[:,(2 -tuples_on C2):] is Relation-like set

[:,(2 -tuples_on C1):] is Relation-like set
S1 is set

S1 is set

C1 is set
C2 is feasible (C1)
(C1) is strict feasible ManySortedSign
the carrier of C2 is set

[:,(2 -tuples_on C1):] is Relation-like set
C1 is non empty set
C2 is feasible () (C1)
(C1) is non empty non void feasible strict feasible ManySortedSign
the carrier of (C1) is non empty set
the carrier of C2 is set
C1 is set
(C1) is strict feasible ManySortedSign
the carrier of (C1) is set

[:,(2 -tuples_on C1):] is Relation-like set
C1 is set
(C1) is strict feasible ManySortedSign
the carrier of (C1) is set

[:,(2 -tuples_on C1):] is Relation-like set
C1 is ManySortedSign
the carrier of C1 is set
the carrier' of C1 is set
the carrier of C1 \/ the carrier' of C1 is set
proj2 ( the carrier of C1 \/ the carrier' of C1) is set
SubFuncs (proj2 ( the carrier of C1 \/ the carrier' of C1)) is set
union (SubFuncs (proj2 ( the carrier of C1 \/ the carrier' of C1))) is set
proj2 (union (SubFuncs (proj2 ( the carrier of C1 \/ the carrier' of C1)))) is set
F is set
S1 is set
S2 is set
[S2,S1] is V21() set
{S2,S1} is non empty set
{S2} is non empty set
{{S2,S1},{S2}} is non empty set
A1 is set

f is set
[f,A2] is V21() set
{f,A2} is non empty set
{f} is non empty set
{{f,A2},{f}} is non empty set
G is set

[G,B1] is V21() set
{G,B1} is non empty set
{G} is non empty set
{{G,B1},{G}} is non empty set
proj2 B1 is set
S2 is set

[S2,A1] is V21() set
{S2,A1} is non empty set
{S2} is non empty set
{{S2,A1},{S2}} is non empty set
proj2 A1 is set
A2 is set
[A2,S1] is V21() set
{A2,S1} is non empty set
{A2} is non empty set
{{A2,S1},{A2}} is non empty set
C1 is set
(C1) is strict feasible () (C1)
((C1)) is set
the carrier' of (C1) is set

[:{1},(1 -tuples_on C1):] is Relation-like set

[:{2},(3 -tuples_on C1):] is Relation-like set
[:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] is Relation-like set
F is set
the carrier of (C1) is set
the carrier of (C1) \/ the carrier' of (C1) is set
S1 is set

[S1,S2] is V21() set
{S1,S2} is non empty set
{S1} is non empty set
{{S1,S2},{S1}} is non empty set
proj2 S2 is set

[:,(2 -tuples_on C1):] is Relation-like set
F is set

[0,<*F,F*>] is V21() set
{0,<*F,F*>} is functional non empty set
{{0,<*F,F*>},} is non empty set
proj2 <*F,F*> is non empty set
{F,F} is non empty set

bool is non empty set
C1 is set
(C1) is strict feasible () (C1)
A1 is set
F is set
S1 is set
S2 is set
F is set

proj1 F is set
proj2 F is set

the carrier of (C1) is set
((C1)) is set
the carrier' of (C1) is set

[:,(2 -tuples_on C1):] is Relation-like set
S2 is set
A1 is set
A2 is set
[A1,A2] is V21() set
{A1,A2} is non empty set
{A1} is non empty set
{{A1,A2},{A1}} is non empty set

S1 . G is V6() V7() V8() V12() Element of NAT

[G,B1] is V21() set
{G,B1} is functional non empty set
{G} is functional non empty set
{{G,B1},{G}} is non empty set
len B1 is V6() V7() V8() V12() Element of NAT
(S1 . G) -tuples_on ((C1)) is functional FinSequence-membered FinSequenceSet of ((C1))
[:{G},((S1 . G) -tuples_on ((C1))):] is Relation-like set
S2 is set

[:{1},(1 -tuples_on C1):] is Relation-like set

[:{2},(3 -tuples_on C1):] is Relation-like set
[:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] is Relation-like set
A1 is set
A2 is set
[A1,A2] is V21() set
{A1,A2} is non empty set
{A1} is non empty set
{{A1,A2},{A1}} is non empty set
G is V6() V7() V8() V12() non empty Element of NAT
S1 . G is V6() V7() V8() V12() Element of NAT
{G} is non empty set
(S1 . G) -tuples_on ((C1)) is functional FinSequence-membered FinSequenceSet of ((C1))
[:{G},((S1 . G) -tuples_on ((C1))):] is Relation-like set

[G,f] is V21() set
{G,f} is non empty set
{{G,f},{G}} is non empty set
len f is V6() V7() V8() V12() Element of NAT
A1 is set
A2 is set
[A1,A2] is V21() set
{A1,A2} is non empty set
{A1} is non empty set
{{A1,A2},{A1}} is non empty set
G is V6() V7() V8() V12() non empty Element of NAT
S1 . G is V6() V7() V8() V12() Element of NAT
{G} is non empty set
(S1 . G) -tuples_on ((C1)) is functional FinSequence-membered FinSequenceSet of ((C1))
[:{G},((S1 . G) -tuples_on ((C1))):] is Relation-like set

[G,f] is V21() set
{G,f} is non empty set
{{G,f},{G}} is non empty set
len f is V6() V7() V8() V12() Element of NAT
() is non empty non void feasible strict feasible () () ()
C1 is set
(C1) is strict feasible () () (C1)
C1 is () ManySortedSign
the carrier of C1 is set
the carrier' of C1 is set
(C1) is set
C2 is set
the carrier of C1 \/ the carrier' of C1 is set

S1 is V6() V7() V8() V12() Element of NAT

[S1,S2] is V21() set
{S1,S2} is non empty set
{S1} is non empty set
{{S1,S2},{S1}} is non empty set
len S2 is V6() V7() V8() V12() Element of NAT
F . S1 is V6() V7() V8() V12() Element of NAT
(F . S1) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)
[:{S1},((F . S1) -tuples_on (C1)):] is Relation-like set
proj2 S2 is set
A1 is set
S1 is V6() V7() V8() V12() Element of NAT

[S1,S2] is V21() set
{S1,S2} is non empty set
{S1} is non empty set
{{S1,S2},{S1}} is non empty set
len S2 is V6() V7() V8() V12() Element of NAT
F . S1 is V6() V7() V8() V12() Element of NAT
(F . S1) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)
[:{S1},((F . S1) -tuples_on (C1)):] is Relation-like set
proj2 S2 is set
A1 is set
C1 is () ManySortedSign
the carrier of C1 is set
the carrier' of C1 is set
C2 is set

[C2,F] is V21() set
{C2,F} is non empty set
{C2} is non empty set
{{C2,F},{C2}} is non empty set

[C2,S1] is V21() set
{C2,S1} is non empty set
{{C2,S1},{C2}} is non empty set
len F is V6() V7() V8() V12() Element of NAT
len S1 is V6() V7() V8() V12() Element of NAT
(C1) is set

A1 is V6() V7() V8() V12() Element of NAT

[A1,A2] is V21() set
{A1,A2} is non empty set
{A1} is non empty set
{{A1,A2},{A1}} is non empty set
len A2 is V6() V7() V8() V12() Element of NAT
S2 . A1 is V6() V7() V8() V12() Element of NAT
(S2 . A1) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)
[:{A1},((S2 . A1) -tuples_on (C1)):] is Relation-like set
f is V6() V7() V8() V12() Element of NAT

[f,G] is V21() set
{f,G} is non empty set
{f} is non empty set
{{f,G},{f}} is non empty set
len G is V6() V7() V8() V12() Element of NAT
S2 . f is V6() V7() V8() V12() Element of NAT
(S2 . f) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)
[:{f},((S2 . f) -tuples_on (C1)):] is Relation-like set
A1 is V6() V7() V8() V12() Element of NAT

[A1,A2] is V21() set
{A1,A2} is non empty set
{A1} is non empty set
{{A1,A2},{A1}} is non empty set
len A2 is V6() V7() V8() V12() Element of NAT
S2 . A1 is V6() V7() V8() V12() Element of NAT
(S2 . A1) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)
[:{A1},((S2 . A1) -tuples_on (C1)):] is Relation-like set
f is V6() V7() V8() V12() Element of NAT

[f,G] is V21() set
{f,G} is non empty set
{f} is non empty set
{{f,G},{f}} is non empty set
len G is V6() V7() V8() V12() Element of NAT
S2 . f is V6() V7() V8() V12() Element of NAT
(S2 . f) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)
[:{f},((S2 . f) -tuples_on (C1)):] is Relation-like set
C1 is () ManySortedSign
(C1) is set
the carrier of C1 is set
the carrier' of C1 is set
C2 is set

len S1 is V6() V7() V8() V12() Element of NAT

len F is V6() V7() V8() V12() Element of NAT
proj2 S1 is set
[C2,F] is V21() set
{C2,F} is non empty set
{C2} is non empty set
{{C2,F},{C2}} is non empty set
[C2,S1] is V21() set
{C2,S1} is non empty set
{{C2,S1},{C2}} is non empty set

A1 is V6() V7() V8() V12() Element of NAT

[A1,A2] is V21() set
{A1,A2} is non empty set
{A1} is non empty set
{{A1,A2},{A1}} is non empty set
len A2 is V6() V7() V8() V12() Element of NAT
S2 . A1 is V6() V7() V8() V12() Element of NAT
(S2 . A1) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)
[:{A1},((S2 . A1) -tuples_on (C1)):] is Relation-like set
A1 is V6() V7() V8() V12() Element of NAT

[A1,A2] is V21() set
{A1,A2} is non empty set
{A1} is non empty set
{{A1,A2},{A1}} is non empty set
len A2 is V6() V7() V8() V12() Element of NAT
S2 . A1 is V6() V7() V8() V12() Element of NAT
(S2 . A1) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)
[:{A1},((S2 . A1) -tuples_on (C1)):] is Relation-like set
C1 is non empty non void feasible feasible () () ManySortedSign
(C1) is set
the carrier of C1 is non empty set
the Element of the carrier of C1 is Element of the carrier of C1
F is set
(F) is strict feasible () () (F)

[:,():] is Relation-like set
the carrier' of C1 is non empty set

S2 is V6() V7() V8() V12() Element of NAT

[S2,A1] is V21() set
{S2,A1} is non empty set
{S2} is non empty set
{{S2,A1},{S2}} is non empty set
len A1 is V6() V7() V8() V12() Element of NAT
S1 . S2 is V6() V7() V8() V12() Element of NAT
(S1 . S2) -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)
[:{S2},((S1 . S2) -tuples_on (C1)):] is Relation-like set
A2 is set

[0,<*A2,A2*>] is V21() set
{0,<*A2,A2*>} is functional non empty set
{{0,<*A2,A2*>},} is non empty set
the carrier of C1 \/ the carrier' of C1 is non empty set
proj2 <*A2,A2*> is non empty set
{A2,A2} is non empty set
2 -tuples_on (C1) is functional FinSequence-membered FinSequenceSet of (C1)
A2 is set

C1 is non empty non void feasible feasible () ManySortedSign
the carrier of C1 is non empty set
C2 is Element of the carrier of C1
C2 `2 is set
F is set
(F) is strict feasible () () (F)

[:,():] is Relation-like set
C1 is non empty feasible feasible () ManySortedSign
the carrier of C1 is non empty set
C2 is Element of the carrier of C1
C2 `2 is set
(C1) is set
F is V6() V7() V8() V12() Element of NAT

[F,S1] is V21() set
{F,S1} is non empty set
{F} is non empty set
{{F,S1},{F}} is non empty set
proj2 S1 is set
C1 is non void () ManySortedSign
the carrier' of C1 is non empty set
C2 is Element of the carrier' of C1
C2 `2 is set
(C1) is set
F is V6() V7() V8() V12() Element of NAT

[F,S1] is V21() set
{F,S1} is non empty set
{F} is non empty set
{{F,S1},{F}} is non empty set
proj2 S1 is set
C1 is non empty non void feasible feasible () ManySortedSign
the carrier of C1 is non empty set
C2 is Element of the carrier of C1

F is set
(F) is strict feasible () () (F)

[:,():] is Relation-like set
S1 is set
S2 is set

C1 is non empty feasible feasible () ManySortedSign
the carrier of C1 is non empty set
C2 is Element of the carrier of C1

(C1) is set
F is V6() V7() V8() V12() Element of NAT

[F,S1] is V21() set
{F,S1} is non empty set
{F} is non empty set
{{F,S1},{F}} is non empty set
proj2 S1 is set
C1 is non void () ManySortedSign
the carrier' of C1 is non empty set
C2 is Element of the carrier' of C1

(C1) is set
F is V6() V7() V8() V12() Element of NAT

[F,S1] is V21() set
{F,S1} is non empty set
{F} is non empty set
{{F,S1},{F}} is non empty set
proj2 S1 is set
C1 is set

[1,<*C1*>] is V21() set
{1,<*C1*>} is non empty set
{{1,<*C1*>},{1}} is non empty set
C2 is set

[0,<*C1,C2*>] is V21() set
{0,<*C1,C2*>} is functional non empty set
{{0,<*C1,C2*>},} is non empty set
F is set

[2,<*C1,C2,F*>] is V21() set
{2,<*C1,C2,F*>} is non empty set
{{2,<*C1,C2,F*>},{2}} is non empty set
C1 is non empty set
C2 is non empty non void feasible feasible () (C1)
the carrier' of C2 is non empty set
the carrier of C2 is non empty set
F is Element of C1
(F) is set

[1,<*F*>] is V21() set
{1,<*F*>} is non empty set
{{1,<*F*>},{1}} is non empty set
(C1) is non empty non void feasible strict feasible () () (C1)
the carrier' of (C1) is non empty set

[:{1},(1 -tuples_on C1):] is Relation-like non empty set

[:{2},(3 -tuples_on C1):] is Relation-like non empty set
[:{1},(1 -tuples_on C1):] \/ [:{2},(3 -tuples_on C1):] is Relation-like non empty set
the carrier of (C1) is non empty set

[1,<*F*>] is V21() set
{1,<*F*>} is non empty set
{{1,<*F*>},{1}} is non empty set
S1 is Element of C1
(F,S1) is set

[0,<*F,S1*>] is V21() set
{0,<*F,S1*>} is functional non empty set
{{0,<*F,S1*>},} is non empty set

[:,(2 -tuples_on C1):] is Relation-like non empty set

[0,<*F,S1*>] is V21() set
{0,<*F,S1*>} is functional non empty set
{{0,<*F,S1*>},} is non empty