:: ALTCAT_1 semantic presentation

K124() is set

K128() is non empty V28() V29() V30() V36() cardinal limit_cardinal Element of bool K124()

bool K124() is non empty set

K123() is non empty V28() V29() V30() V36() cardinal limit_cardinal set

bool K123() is non empty V36() set

bool K128() is non empty V36() set

2 is non empty V28() V29() V30() V34() V36() cardinal Element of K128()

[:2,2:] is Relation-like non empty set

[:[:2,2:],2:] is Relation-like non empty set

bool [:[:2,2:],2:] is non empty set

{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() V28() V29() V30() V32() V33() V34() V36() cardinal {} -element set

the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() V28() V29() V30() V32() V33() V34() V36() cardinal {} -element set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() V28() V29() V30() V32() V33() V34() V36() cardinal {} -element set

1 is non empty V28() V29() V30() V34() V36() cardinal Element of K128()

proj1 {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() V28() V29() V30() V32() V33() V34() V36() cardinal {} -element set

proj2 {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() V28() V29() V30() V32() V33() V34() V36() cardinal {} -element set

{{}} is functional non empty trivial 1 -element set

A is set

id A is Relation-like A -defined A -valued Function-like one-to-one V14(A) set

Funcs (A,A) is functional non empty set

proj1 (id A) is set

proj2 (id A) is set

Funcs ({},{}) is functional non empty set

id {} is Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional empty trivial V14( {} ) Function-yielding V25() V28() V29() V30() V32() V33() V34() V36() cardinal {} -element set

{(id {})} is functional non empty trivial 1 -element set

A is set

[:{},{}:] is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() V28() V29() V30() V32() V33() V34() V36() cardinal {} -element set

bool [:{},{}:] is non empty set

C is Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional empty trivial non proper V14( {} ) quasi_total Function-yielding V25() V28() V29() V30() V32() V33() V34() V36() cardinal {} -element Element of bool [:{},{}:]

A is set

C is set

Funcs (A,C) is functional set

i is set

Funcs (C,i) is functional set

Funcs (A,i) is functional set

j is Relation-like Function-like set

k is Relation-like Function-like set

j * k is Relation-like Function-like set

proj2 (j * k) is set

proj2 k is set

l is Relation-like Function-like set

proj1 l is set

proj2 l is set

proj1 (j * k) is set

l is Relation-like Function-like set

proj1 l is set

proj2 l is set

G is Relation-like Function-like set

proj1 G is set

proj2 G is set

A is set

C is set

Funcs (A,C) is functional set

i is set

Funcs (C,i) is functional set

Funcs (A,i) is functional set

j is set

k is set

C is set

A is set

[:C,A:] is Relation-like set

bool A is non empty set

bool C is non empty set

i is Relation-like [:C,A:] -defined Function-like V14([:C,A:]) set

j is Element of bool A

k is Element of bool C

[:k,j:] is Relation-like C -defined A -valued Element of bool [:C,A:]

bool [:C,A:] is non empty set

i | [:k,j:] is Relation-like [:k,j:] -defined [:C,A:] -defined Function-like set

l is set

G is set

i . (G,l) is set

[G,l] is non empty V15() set

{G,l} is non empty set

{G} is non empty trivial 1 -element set

{{G,l},{G}} is non empty set

i . [G,l] is set

(i | [:k,j:]) . (G,l) is set

(i | [:k,j:]) . [G,l] is set

F

F

[:F

A is Relation-like Function-like set

proj1 A is set

C is Relation-like [:F

i is set

j is set

C . (i,j) is set

[i,j] is non empty V15() set

{i,j} is non empty set

{i} is non empty trivial 1 -element set

{{i,j},{i}} is non empty set

C . [i,j] is set

F

[i,j] `1 is set

[i,j] `2 is set

F

F

[:F

A is Relation-like [:F

C is Element of F

i is Element of F

A . (C,i) is set

[C,i] is non empty V15() set

{C,i} is non empty set

{C} is non empty trivial 1 -element set

{{C,i},{C}} is non empty set

A . [C,i] is set

F

F

F

F

[:F

A is Relation-like Function-like set

proj1 A is set

C is Relation-like [:F

i is set

j is set

k is set

C . (i,j,k) is set

F

[i,j] is non empty V15() set

{i,j} is non empty set

{i} is non empty trivial 1 -element set

{{i,j},{i}} is non empty set

[[i,j],k] is non empty V15() set

{[i,j],k} is non empty set

{[i,j]} is Relation-like Function-like constant non empty trivial 1 -element set

{{[i,j],k},{[i,j]}} is non empty set

[[i,j],k] `2 is set

[i,j,k] is V15() V16() set

[[i,j],k] `1 is set

([[i,j],k] `1) `2 is set

([[i,j],k] `1) `1 is set

C . [i,j,k] is set

F

F

F

[:F

A is Relation-like [:F

C is Element of F

i is Element of F

j is Element of F

A . (C,i,j) is set

F

A is set

C is set

[:A,C:] is Relation-like set

i is Relation-like [:A,C:] -defined Function-like V14([:A,C:]) set

j is Relation-like [:A,C:] -defined Function-like V14([:A,C:]) set

k is set

l is non empty set

G is non empty set

c is Element of l

i9 is Element of G

[c,i9] is non empty V15() Element of [:l,G:]

[:l,G:] is Relation-like non empty set

{c,i9} is non empty set

{c} is non empty trivial 1 -element set

{{c,i9},{c}} is non empty set

i . k is set

i . (c,i9) is set

[c,i9] is non empty V15() set

i . [c,i9] is set

j . (c,i9) is set

j . [c,i9] is set

j . k is set

proj1 j is set

proj1 i is set

A is non empty set

C is non empty set

[:A,C:] is Relation-like non empty set

i is Relation-like [:A,C:] -defined Function-like V14([:A,C:]) set

j is Relation-like [:A,C:] -defined Function-like V14([:A,C:]) set

k is set

l is set

i . (k,l) is set

[k,l] is non empty V15() set

{k,l} is non empty set

{k} is non empty trivial 1 -element set

{{k,l},{k}} is non empty set

i . [k,l] is set

j . (k,l) is set

j . [k,l] is set

A is set

[:A,A,A:] is set

C is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

i is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

j is set

k is non empty set

l is Element of k

G is Element of k

c is Element of k

[l,G,c] is V15() V16() Element of [:k,k,k:]

[:k,k,k:] is non empty set

[l,G] is non empty V15() set

{l,G} is non empty set

{l} is non empty trivial 1 -element set

{{l,G},{l}} is non empty set

[[l,G],c] is non empty V15() set

{[l,G],c} is non empty set

{[l,G]} is Relation-like Function-like constant non empty trivial 1 -element set

{{[l,G],c},{[l,G]}} is non empty set

i . j is set

i . (l,G,c) is set

C . (l,G,c) is set

C . j is set

proj1 i is set

proj1 C is set

A is set

C is set

i is set

(A,C) :-> i is Relation-like [:{A},{C}:] -defined {i} -valued Function-like non empty V14([:{A},{C}:]) quasi_total Element of bool [:[:{A},{C}:],{i}:]

{A} is non empty trivial 1 -element set

{C} is non empty trivial 1 -element set

[:{A},{C}:] is Relation-like non empty set

{i} is non empty trivial 1 -element set

[:[:{A},{C}:],{i}:] is Relation-like non empty set

bool [:[:{A},{C}:],{i}:] is non empty set

[A,C] is non empty V15() set

{A,C} is non empty set

{{A,C},{A}} is non empty set

{[A,C]} is Relation-like Function-like constant non empty trivial 1 -element set

{[A,C]} --> i is Relation-like {[A,C]} -defined {i} -valued Function-like constant non empty V14({[A,C]}) quasi_total Element of bool [:{[A,C]},{i}:]

[:{[A,C]},{i}:] is Relation-like non empty set

bool [:{[A,C]},{i}:] is non empty set

[A,C] .--> i is Relation-like {[A,C]} -defined Function-like one-to-one set

A is set

C is set

i is set

(A,C) :-> i is Relation-like [:{A},{C}:] -defined {i} -valued Function-like non empty V14([:{A},{C}:]) quasi_total Element of bool [:[:{A},{C}:],{i}:]

{A} is non empty trivial 1 -element set

{C} is non empty trivial 1 -element set

[:{A},{C}:] is Relation-like non empty set

{i} is non empty trivial 1 -element set

[:[:{A},{C}:],{i}:] is Relation-like non empty set

bool [:[:{A},{C}:],{i}:] is non empty set

[A,C] is non empty V15() set

{A,C} is non empty set

{{A,C},{A}} is non empty set

{[A,C]} is Relation-like Function-like constant non empty trivial 1 -element set

{[A,C]} --> i is Relation-like {[A,C]} -defined {i} -valued Function-like constant non empty V14({[A,C]}) quasi_total Element of bool [:{[A,C]},{i}:]

[:{[A,C]},{i}:] is Relation-like non empty set

bool [:{[A,C]},{i}:] is non empty set

((A,C) :-> i) . (A,C) is set

((A,C) :-> i) . [A,C] is set

[A,C] .--> i is Relation-like {[A,C]} -defined Function-like one-to-one set

([A,C] .--> i) . [A,C] is set

A is ()

the carrier of A is set

the of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A:]) set

[: the carrier of A, the carrier of A:] is Relation-like set

C is Element of the carrier of A

i is Element of the carrier of A

the of A . (C,i) is set

[C,i] is non empty V15() set

{C,i} is non empty set

{C} is non empty trivial 1 -element set

{{C,i},{C}} is non empty set

the of A . [C,i] is set

A is ()

the carrier of A is set

A is set

[:A,A:] is Relation-like set

[:A,A,A:] is set

C is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) set

i is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

i is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

j is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

k is set

l is set

G is set

i . (k,l,G) is set

C . (k,G) is set

[k,G] is non empty V15() set

{k,G} is non empty set

{k} is non empty trivial 1 -element set

{{k,G},{k}} is non empty set

C . [k,G] is set

j . (k,l,G) is set

i is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) set

j is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

j is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

k is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

l is set

G is set

c is set

j . (l,G,c) is set

i . (G,c) is set

[G,c] is non empty V15() set

{G,c} is non empty set

{G} is non empty trivial 1 -element set

{{G,c},{G}} is non empty set

i . [G,c] is set

C . (l,G) is set

[l,G] is non empty V15() set

{l,G} is non empty set

{l} is non empty trivial 1 -element set

{{l,G},{l}} is non empty set

C . [l,G] is set

[:(i . (G,c)),(C . (l,G)):] is Relation-like set

k . (l,G,c) is set

A is set

[:A,A:] is Relation-like set

A is non empty set

[:A,A:] is Relation-like non empty set

[:A,A,A:] is non empty set

C is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) set

(A,C,C) is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

(A,C) is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

i is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) ManySortedFunction of (A,C,C),(A,C)

j is Element of A

k is Element of A

l is Element of A

i . (j,k,l) is set

C . (k,l) is set

[k,l] is non empty V15() set

{k,l} is non empty set

{k} is non empty trivial 1 -element set

{{k,l},{k}} is non empty set

C . [k,l] is set

C . (j,k) is set

[j,k] is non empty V15() set

{j,k} is non empty set

{j} is non empty trivial 1 -element set

{{j,k},{j}} is non empty set

C . [j,k] is set

[:(C . (k,l)),(C . (j,k)):] is Relation-like set

C . (j,l) is set

[j,l] is non empty V15() set

{j,l} is non empty set

{{j,l},{j}} is non empty set

C . [j,l] is set

[:[:(C . (k,l)),(C . (j,k)):],(C . (j,l)):] is Relation-like set

bool [:[:(C . (k,l)),(C . (j,k)):],(C . (j,l)):] is non empty set

[j,k,l] is V15() V16() Element of [:A,A,A:]

[[j,k],l] is non empty V15() set

{[j,k],l} is non empty set

{[j,k]} is Relation-like Function-like constant non empty trivial 1 -element set

{{[j,k],l},{[j,k]}} is non empty set

(A,C) . [j,k,l] is set

(A,C) . (j,k,l) is set

i . [j,k,l] is set

(A,C,C) . [j,k,l] is set

(A,C,C) . (j,k,l) is set

A is non empty set

[:A,A:] is Relation-like non empty set

[:A,A,A:] is non empty set

C is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) set

(A,C,C) is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

(A,C) is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

the non empty set is non empty set

[: the non empty set , the non empty set :] is Relation-like non empty set

the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set is Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set

[: the non empty set , the non empty set , the non empty set :] is non empty set

( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set ) is Relation-like [: the non empty set , the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set , the non empty set :]) set

( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set ) is Relation-like [: the non empty set , the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set , the non empty set :]) set

the Relation-like [: the non empty set , the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set , the non empty set :]) ManySortedFunction of ( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set ),( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set ) is Relation-like [: the non empty set , the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set , the non empty set :]) ManySortedFunction of ( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set ),( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set )

( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set , the Relation-like [: the non empty set , the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set , the non empty set :]) ManySortedFunction of ( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set ),( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set )) is () ()

the carrier of ( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set , the Relation-like [: the non empty set , the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set , the non empty set :]) ManySortedFunction of ( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set ),( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined Function-like V14([: the non empty set , the non empty set :]) set )) is set

A is non empty ()

the carrier of A is non empty set

C is Element of the carrier of A

i is Element of the carrier of A

(A,C,i) is set

the of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A:]) set

[: the carrier of A, the carrier of A:] is Relation-like non empty set

the of A . (C,i) is set

[C,i] is non empty V15() set

{C,i} is non empty set

{C} is non empty trivial 1 -element set

{{C,i},{C}} is non empty set

the of A . [C,i] is set

j is Element of the carrier of A

(A,i,j) is set

the of A . (i,j) is set

[i,j] is non empty V15() set

{i,j} is non empty set

{i} is non empty trivial 1 -element set

{{i,j},{i}} is non empty set

the of A . [i,j] is set

the of A is Relation-like [: the carrier of A, the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A, the carrier of A:]) ManySortedFunction of ( the carrier of A, the of A, the of A),( the carrier of A, the of A)

[: the carrier of A, the carrier of A, the carrier of A:] is non empty set

( the carrier of A, the of A, the of A) is Relation-like [: the carrier of A, the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A, the carrier of A:]) set

( the carrier of A, the of A) is Relation-like [: the carrier of A, the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A, the carrier of A:]) set

( the carrier of A, the of A, the of A,C,i,j) is Relation-like [:( the of A . (i,j)),( the of A . (C,i)):] -defined the of A . (C,j) -valued Function-like quasi_total Element of bool [:[:( the of A . (i,j)),( the of A . (C,i)):],( the of A . (C,j)):]

[:( the of A . (i,j)),( the of A . (C,i)):] is Relation-like set

the of A . (C,j) is set

[C,j] is non empty V15() set

{C,j} is non empty set

{{C,j},{C}} is non empty set

the of A . [C,j] is set

[:[:( the of A . (i,j)),( the of A . (C,i)):],( the of A . (C,j)):] is Relation-like set

bool [:[:( the of A . (i,j)),( the of A . (C,i)):],( the of A . (C,j)):] is non empty set

l is Element of (A,i,j)

k is Element of (A,C,i)

( the carrier of A, the of A, the of A,C,i,j) . (l,k) is set

[l,k] is non empty V15() set

{l,k} is non empty set

{l} is non empty trivial 1 -element set

{{l,k},{l}} is non empty set

( the carrier of A, the of A, the of A,C,i,j) . [l,k] is set

(A,C,j) is set

c is non empty set

G is non empty set

[:c,G:] is Relation-like non empty set

[:[:c,G:],(A,C,j):] is Relation-like set

bool [:[:c,G:],(A,C,j):] is non empty set

i9 is Relation-like [:c,G:] -defined (A,C,j) -valued Function-like quasi_total Element of bool [:[:c,G:],(A,C,j):]

j9 is Element of c

k9 is Element of G

i9 . (j9,k9) is Element of (A,C,j)

[j9,k9] is non empty V15() set

{j9,k9} is non empty set

{j9} is non empty trivial 1 -element set

{{j9,k9},{j9}} is non empty set

i9 . [j9,k9] is set

A is functional set

C is functional set

[:A,C:] is Relation-like set

[[0]] [:A,C:] is Relation-like [:A,C:] -defined Function-like V14([:A,C:]) set

j is Relation-like [:A,C:] -defined Function-like V14([:A,C:]) Function-yielding V25() set

k is set

proj1 j is set

j . k is Relation-like Function-like set

i is functional non empty set

j is functional non empty set

[:i,j:] is Relation-like non empty set

k is Relation-like [:i,j:] -defined Function-like V14([:i,j:]) set

l is set

proj1 k is set

k . l is set

l `1 is set

l `2 is set

G is Relation-like Function-like set

c is Relation-like Function-like set

k . (G,c) is set

[G,c] is non empty V15() set

{G,c} is functional non empty set

{G} is functional non empty trivial 1 -element set

{{G,c},{G}} is non empty set

k . [G,c] is set

c * G is Relation-like Function-like set

l is Relation-like [:A,C:] -defined Function-like V14([:A,C:]) Function-yielding V25() set

G is set

proj1 l is set

l . G is Relation-like Function-like set

G `1 is set

G `2 is set

i9 is Relation-like Function-like set

c is Relation-like Function-like set

[c,i9] is non empty V15() set

{c,i9} is functional non empty set

{c} is functional non empty trivial 1 -element set

{{c,i9},{c}} is non empty set

i9 * c is Relation-like Function-like set

l . (c,i9) is set

l . [c,i9] is Relation-like Function-like set

A is functional set

C is functional set

[:A,C:] is Relation-like set

i is Relation-like [:A,C:] -defined Function-like V14([:A,C:]) () set

j is Relation-like Function-like set

k is Relation-like Function-like set

i . (j,k) is set

[j,k] is non empty V15() set

{j,k} is functional non empty set

{j} is functional non empty trivial 1 -element set

{{j,k},{j}} is non empty set

i . [j,k] is set

k * j is Relation-like Function-like set

proj1 i is set

G is Relation-like Function-like set

l is Relation-like Function-like set

[G,l] is non empty V15() set

{G,l} is functional non empty set

{G} is functional non empty trivial 1 -element set

{{G,l},{G}} is non empty set

l * G is Relation-like Function-like set

C is functional set

A is functional set

[:C,A:] is Relation-like set

i is Relation-like [:C,A:] -defined Function-like V14([:C,A:]) Function-yielding V25() () set

j is Relation-like [:C,A:] -defined Function-like V14([:C,A:]) Function-yielding V25() () set

k is set

l is set

[k,l] is non empty V15() set

{k,l} is non empty set

{k} is non empty trivial 1 -element set

{{k,l},{k}} is non empty set

proj1 i is set

i . [k,l] is Relation-like Function-like set

c is Relation-like Function-like set

G is Relation-like Function-like set

[c,G] is non empty V15() set

{c,G} is functional non empty set

{c} is functional non empty trivial 1 -element set

{{c,G},{c}} is non empty set

G * c is Relation-like Function-like set

proj1 j is set

j . [k,l] is Relation-like Function-like set

j9 is Relation-like Function-like set

i9 is Relation-like Function-like set

[j9,i9] is non empty V15() set

{j9,i9} is functional non empty set

{j9} is functional non empty trivial 1 -element set

{{j9,i9},{j9}} is non empty set

i9 * j9 is Relation-like Function-like set

i . (k,l) is set

j . (k,l) is set

A is set

C is set

Funcs (A,C) is functional set

i is set

Funcs (C,i) is functional set

((Funcs (A,C)),(Funcs (C,i))) is Relation-like [:(Funcs (C,i)),(Funcs (A,C)):] -defined Function-like V14([:(Funcs (C,i)),(Funcs (A,C)):]) Function-yielding V25() () set

[:(Funcs (C,i)),(Funcs (A,C)):] is Relation-like set

proj2 ((Funcs (A,C)),(Funcs (C,i))) is set

Funcs (A,i) is functional set

j is set

proj1 ((Funcs (A,C)),(Funcs (C,i))) is set

l is set

((Funcs (A,C)),(Funcs (C,i))) . l is Relation-like Function-like set

c is Relation-like Function-like set

G is Relation-like Function-like set

[c,G] is non empty V15() set

{c,G} is functional non empty set

{c} is functional non empty trivial 1 -element set

{{c,G},{c}} is non empty set

G * c is Relation-like Function-like set

A is set

id A is Relation-like A -defined A -valued Function-like one-to-one V14(A) set

{(id A)} is functional non empty trivial 1 -element set

[:{(id A)},{(id A)}:] is Relation-like non empty set

({(id A)},{(id A)}) is Relation-like [:{(id A)},{(id A)}:] -defined Function-like V14([:{(id A)},{(id A)}:]) Function-yielding V25() () set

((id A),(id A)) :-> (id A) is Relation-like [:{(id A)},{(id A)}:] -defined {(id A)} -valued Function-like non empty V14([:{(id A)},{(id A)}:]) quasi_total Function-yielding V25() Element of bool [:[:{(id A)},{(id A)}:],{(id A)}:]

[:[:{(id A)},{(id A)}:],{(id A)}:] is Relation-like non empty set

bool [:[:{(id A)},{(id A)}:],{(id A)}:] is non empty set

[(id A),(id A)] is non empty V15() set

{(id A),(id A)} is functional non empty set

{{(id A),(id A)},{(id A)}} is non empty set

{[(id A),(id A)]} is Relation-like Function-like constant non empty trivial 1 -element set

{[(id A),(id A)]} --> (id A) is Relation-like {[(id A),(id A)]} -defined {(id A)} -valued Function-like constant non empty V14({[(id A),(id A)]}) quasi_total Function-yielding V25() Element of bool [:{[(id A),(id A)]},{(id A)}:]

[:{[(id A),(id A)]},{(id A)}:] is Relation-like non empty set

bool [:{[(id A),(id A)]},{(id A)}:] is non empty set

proj1 ({(id A)},{(id A)}) is set

proj2 ({(id A)},{(id A)}) is set

C is set

i is set

({(id A)},{(id A)}) . i is Relation-like Function-like set

k is Relation-like Function-like set

j is Relation-like Function-like set

[k,j] is non empty V15() set

{k,j} is functional non empty set

{k} is functional non empty trivial 1 -element set

{{k,j},{k}} is non empty set

j * k is Relation-like Function-like set

A /\ A is set

A is functional set

bool A is non empty set

C is functional set

bool C is non empty set

(A,C) is Relation-like [:C,A:] -defined Function-like V14([:C,A:]) Function-yielding V25() () set

[:C,A:] is Relation-like set

i is functional Element of bool A

j is functional Element of bool C

(i,j) is Relation-like [:j,i:] -defined Function-like V14([:j,i:]) Function-yielding V25() () set

[:j,i:] is Relation-like set

[:j,i:] is Relation-like C -defined A -valued Element of bool [:C,A:]

bool [:C,A:] is non empty set

(A,C) | [:j,i:] is Relation-like [:j,i:] -defined [:C,A:] -defined Function-like Function-yielding V25() set

proj1 (A,C) is set

proj1 ((A,C) | [:j,i:]) is set

l is Relation-like [:j,i:] -defined Function-like V14([:j,i:]) Function-yielding V25() set

G is set

proj1 l is set

l . G is Relation-like Function-like set

(A,C) . G is Relation-like Function-like set

A is non empty set

[:A,A:] is Relation-like non empty set

[:A,A,A:] is non empty set

C is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) set

(A,C,C) is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

(A,C) is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

i is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) ManySortedFunction of (A,C,C),(A,C)

(A,C,i) is () ()

[:K128(),K128(),K128():] is non empty set

0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() V28() V29() V30() V32() V33() V34() V36() cardinal {} -element Element of K128()

[0,0,0] is V15() V16() Element of [:K128(),K128(),K128():]

[0,0] is non empty V15() set

{0,0} is functional non empty set

{0} is functional non empty trivial 1 -element set

{{0,0},{0}} is non empty set

[[0,0],0] is non empty V15() set

{[0,0],0} is non empty set

{[0,0]} is Relation-like Function-like constant non empty trivial 1 -element set

{{[0,0],0},{[0,0]}} is non empty set

{[0,0,0]} is non empty trivial 1 -element Element of bool [:K128(),K128(),K128():]

bool [:K128(),K128(),K128():] is non empty set

[:1,1,1:] is non empty set

Funcs (0,0) is functional non empty set

((Funcs (0,0)),(Funcs (0,0))) is Relation-like [:(Funcs (0,0)),(Funcs (0,0)):] -defined Function-like V14([:(Funcs (0,0)),(Funcs (0,0)):]) Function-yielding V25() () set

[:(Funcs (0,0)),(Funcs (0,0)):] is Relation-like non empty set

[0,0,0] .--> ((Funcs (0,0)),(Funcs (0,0))) is Relation-like [:K128(),K128(),K128():] -defined {[0,0,0]} -defined Function-like one-to-one Function-yielding V25() set

{[0,0,0]} is non empty trivial 1 -element set

{[0,0,0]} --> ((Funcs (0,0)),(Funcs (0,0))) is Relation-like {[0,0,0]} -defined {((Funcs (0,0)),(Funcs (0,0)))} -valued Function-like constant non empty V14({[0,0,0]}) quasi_total Function-yielding V25() Element of bool [:{[0,0,0]},{((Funcs (0,0)),(Funcs (0,0)))}:]

{((Funcs (0,0)),(Funcs (0,0)))} is functional non empty trivial 1 -element set

[:{[0,0,0]},{((Funcs (0,0)),(Funcs (0,0)))}:] is Relation-like non empty set

bool [:{[0,0,0]},{((Funcs (0,0)),(Funcs (0,0)))}:] is non empty set

A is Relation-like [:1,1,1:] -defined Function-like V14([:1,1,1:]) set

[0,0] is non empty V15() Element of [:K128(),K128():]

[:K128(),K128():] is Relation-like non empty V36() set

[0,0] .--> (Funcs (0,0)) is Relation-like [:K128(),K128():] -defined {[0,0]} -defined Function-like one-to-one set

{[0,0]} is Relation-like Function-like constant non empty trivial 1 -element set

{[0,0]} --> (Funcs (0,0)) is Relation-like non-empty {[0,0]} -defined {(Funcs (0,0))} -valued Function-like constant non empty V14({[0,0]}) quasi_total Element of bool [:{[0,0]},{(Funcs (0,0))}:]

{(Funcs (0,0))} is non empty trivial 1 -element set

[:{[0,0]},{(Funcs (0,0))}:] is Relation-like non empty set

bool [:{[0,0]},{(Funcs (0,0))}:] is non empty set

proj1 ([0,0] .--> (Funcs (0,0))) is set

{[0,0]} is Relation-like K128() -defined K128() -valued Function-like constant non empty trivial 1 -element Element of bool [:K128(),K128():]

bool [:K128(),K128():] is non empty V36() set

[:1,1:] is Relation-like non empty set

i is Relation-like [:1,1:] -defined Function-like V14([:1,1:]) set

i . (0,0) is set

i . [0,0] is set

C is Relation-like [:1,1,1:] -defined Function-like V14([:1,1,1:]) Function-yielding V25() set

j is set

C . j is Relation-like Function-like set

k is Relation-like Function-like set

proj1 k is set

[:(i . (0,0)),(i . (0,0)):] is Relation-like set

(1,i,i) is Relation-like [:1,1,1:] -defined Function-like V14([:1,1,1:]) set

(1,i,i) . (0,0,0) is set

(1,i,i) . j is set

(1,i) is Relation-like [:1,1,1:] -defined Function-like V14([:1,1,1:]) set

(1,i) . j is set

(1,i) . (0,0,0) is set

proj2 k is set

[:((1,i,i) . j),((1,i) . j):] is Relation-like set

bool [:((1,i,i) . j),((1,i) . j):] is non empty set

j is Relation-like [:1,1,1:] -defined Function-like V14([:1,1,1:]) ManySortedFunction of (1,i,i),(1,i)

(1,i,j) is non empty () ()

k is non empty () ()

the carrier of k is non empty set

the of k is Relation-like [: the carrier of k, the carrier of k:] -defined Function-like V14([: the carrier of k, the carrier of k:]) set

[: the carrier of k, the carrier of k:] is Relation-like non empty set

the of k is Relation-like [: the carrier of k, the carrier of k, the carrier of k:] -defined Function-like V14([: the carrier of k, the carrier of k, the carrier of k:]) ManySortedFunction of ( the carrier of k, the of k, the of k),( the carrier of k, the of k)

[: the carrier of k, the carrier of k, the carrier of k:] is non empty set

( the carrier of k, the of k, the of k) is Relation-like [: the carrier of k, the carrier of k, the carrier of k:] -defined Function-like V14([: the carrier of k, the carrier of k, the carrier of k:]) set

( the carrier of k, the of k) is Relation-like [: the carrier of k, the carrier of k, the carrier of k:] -defined Function-like V14([: the carrier of k, the carrier of k, the carrier of k:]) set

l is Element of the carrier of k

G is Element of the carrier of k

c is Element of the carrier of k

( the carrier of k, the of k, the of k,l,G,c) is Relation-like [:( the of k . (G,c)),( the of k . (l,G)):] -defined the of k . (l,c) -valued Function-like quasi_total Element of bool [:[:( the of k . (G,c)),( the of k . (l,G)):],( the of k . (l,c)):]

the of k . (G,c) is set

[G,c] is non empty V15() set

{G,c} is non empty set

{G} is non empty trivial 1 -element set

{{G,c},{G}} is non empty set

the of k . [G,c] is set

the of k . (l,G) is set

[l,G] is non empty V15() set

{l,G} is non empty set

{l} is non empty trivial 1 -element set

{{l,G},{l}} is non empty set

the of k . [l,G] is set

[:( the of k . (G,c)),( the of k . (l,G)):] is Relation-like set

the of k . (l,c) is set

[l,c] is non empty V15() set

{l,c} is non empty set

{{l,c},{l}} is non empty set

the of k . [l,c] is set

[:[:( the of k . (G,c)),( the of k . (l,G)):],( the of k . (l,c)):] is Relation-like set

bool [:[:( the of k . (G,c)),( the of k . (l,G)):],( the of k . (l,c)):] is non empty set

Funcs (l,G) is functional set

Funcs (G,c) is functional set

((Funcs (l,G)),(Funcs (G,c))) is Relation-like [:(Funcs (G,c)),(Funcs (l,G)):] -defined Function-like V14([:(Funcs (G,c)),(Funcs (l,G)):]) Function-yielding V25() () set

[:(Funcs (G,c)),(Funcs (l,G)):] is Relation-like set

(k,G,c) is set

(k,l,G) is set

[:(k,G,c),(k,l,G):] is Relation-like set

((Funcs (l,G)),(Funcs (G,c))) | [:(k,G,c),(k,l,G):] is Relation-like [:(k,G,c),(k,l,G):] -defined [:(Funcs (G,c)),(Funcs (l,G)):] -defined Function-like Function-yielding V25() set

proj1 ((Funcs (0,0)),(Funcs (0,0))) is set

[l,G,c] is V15() V16() Element of [: the carrier of k, the carrier of k, the carrier of k:]

[[l,G],c] is non empty V15() set

{[l,G],c} is non empty set

{[l,G]} is Relation-like Function-like constant non empty trivial 1 -element set

{{[l,G],c},{[l,G]}} is non empty set

j . [l,G,c] is set

A is non empty ()

the carrier of A is non empty set

the of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A:]) set

[: the carrier of A, the carrier of A:] is Relation-like non empty set

the of A is Relation-like [: the carrier of A, the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A, the carrier of A:]) ManySortedFunction of ( the carrier of A, the of A, the of A),( the carrier of A, the of A)

[: the carrier of A, the carrier of A, the carrier of A:] is non empty set

( the carrier of A, the of A, the of A) is Relation-like [: the carrier of A, the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A, the carrier of A:]) set

( the carrier of A, the of A) is Relation-like [: the carrier of A, the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A, the carrier of A:]) set

C is Element of the carrier of A

i is Element of the carrier of A

j is Element of the carrier of A

( the carrier of A, the of A, the of A,C,i,j) is Relation-like [:( the of A . (i,j)),( the of A . (C,i)):] -defined the of A . (C,j) -valued Function-like quasi_total Element of bool [:[:( the of A . (i,j)),( the of A . (C,i)):],( the of A . (C,j)):]

the of A . (i,j) is set

[i,j] is non empty V15() set

{i,j} is non empty set

{i} is non empty trivial 1 -element set

{{i,j},{i}} is non empty set

the of A . [i,j] is set

the of A . (C,i) is set

[C,i] is non empty V15() set

{C,i} is non empty set

{C} is non empty trivial 1 -element set

{{C,i},{C}} is non empty set

the of A . [C,i] is set

[:( the of A . (i,j)),( the of A . (C,i)):] is Relation-like set

the of A . (C,j) is set

[C,j] is non empty V15() set

{C,j} is non empty set

{{C,j},{C}} is non empty set

the of A . [C,j] is set

[:[:( the of A . (i,j)),( the of A . (C,i)):],( the of A . (C,j)):] is Relation-like set

bool [:[:( the of A . (i,j)),( the of A . (C,i)):],( the of A . (C,j)):] is non empty set

(A,i,j) is set

(A,C,i) is set

[:(A,i,j),(A,C,i):] is Relation-like set

(A,C,j) is set

[:[:(A,i,j),(A,C,i):],(A,C,j):] is Relation-like set

bool [:[:(A,i,j),(A,C,i):],(A,C,j):] is non empty set

A is non empty () ()

the carrier of A is non empty set

C is Element of the carrier of A

i is Element of the carrier of A

(A,C,i) is set

the of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A:]) set

[: the carrier of A, the carrier of A:] is Relation-like non empty set

the of A . (C,i) is set

[C,i] is non empty V15() set

{C,i} is non empty set

{C} is non empty trivial 1 -element set

{{C,i},{C}} is non empty set

the of A . [C,i] is set

j is Element of the carrier of A

(A,i,j) is set

the of A . (i,j) is set

[i,j] is non empty V15() set

{i,j} is non empty set

{i} is non empty trivial 1 -element set

{{i,j},{i}} is non empty set

the of A . [i,j] is set

(A,C,j) is set

the of A . (C,j) is set

[C,j] is non empty V15() set

{C,j} is non empty set

{{C,j},{C}} is non empty set

the of A . [C,j] is set

k is Element of (A,C,i)

l is Element of (A,i,j)

(A,C,i,j,k,l) is Element of (A,C,j)

G is Relation-like Function-like set

c is Relation-like Function-like set

G * c is Relation-like Function-like set

[l,k] is non empty V15() set

{l,k} is non empty set

{l} is non empty trivial 1 -element set

{{l,k},{l}} is non empty set

[:(A,i,j),(A,C,i):] is Relation-like set

the of A is Relation-like [: the carrier of A, the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A, the carrier of A:]) ManySortedFunction of ( the carrier of A, the of A, the of A),( the carrier of A, the of A)

[: the carrier of A, the carrier of A, the carrier of A:] is non empty set

( the carrier of A, the of A, the of A) is Relation-like [: the carrier of A, the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A, the carrier of A:]) set

( the carrier of A, the of A) is Relation-like [: the carrier of A, the carrier of A, the carrier of A:] -defined Function-like V14([: the carrier of A, the carrier of A, the carrier of A:]) set

( the carrier of A, the of A, the of A,C,i,j) is Relation-like [:( the of A . (i,j)),( the of A . (C,i)):] -defined the of A . (C,j) -valued Function-like quasi_total Element of bool [:[:( the of A . (i,j)),( the of A . (C,i)):],( the of A . (C,j)):]

[:( the of A . (i,j)),( the of A . (C,i)):] is Relation-like set

[:[:( the of A . (i,j)),( the of A . (C,i)):],( the of A . (C,j)):] is Relation-like set

bool [:[:( the of A . (i,j)),( the of A . (C,i)):],( the of A . (C,j)):] is non empty set

Funcs (C,i) is functional set

Funcs (i,j) is functional set

((Funcs (C,i)),(Funcs (i,j))) is Relation-like [:(Funcs (i,j)),(Funcs (C,i)):] -defined Function-like V14([:(Funcs (i,j)),(Funcs (C,i)):]) Function-yielding V25() () set

[:(Funcs (i,j)),(Funcs (C,i)):] is Relation-like set

((Funcs (C,i)),(Funcs (i,j))) | [:(A,i,j),(A,C,i):] is Relation-like [:(A,i,j),(A,C,i):] -defined [:(Funcs (i,j)),(Funcs (C,i)):] -defined Function-like Function-yielding V25() set

proj1 (((Funcs (C,i)),(Funcs (i,j))) | [:(A,i,j),(A,C,i):]) is set

proj1 ((Funcs (C,i)),(Funcs (i,j))) is set

proj1 ( the carrier of A, the of A, the of A,C,i,j) is Relation-like set

((Funcs (C,i)),(Funcs (i,j))) . [l,k] is Relation-like Function-like set

j9 is Relation-like Function-like set

i9 is Relation-like Function-like set

[j9,i9] is non empty V15() set

{j9,i9} is functional non empty set

{j9} is functional non empty trivial 1 -element set

{{j9,i9},{j9}} is non empty set

i9 * j9 is Relation-like Function-like set

( the carrier of A, the of A, the of A,C,i,j) . (l,k) is set

( the carrier of A, the of A, the of A,C,i,j) . [l,k] is set

A is non empty set

[:A,A:] is Relation-like non empty set

C is Relation-like [:A,A:] -defined Function-like V14([:A,A:]) set

[:A,A,A:] is non empty set

i is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

j is set

proj1 i is set

i . j is set

k is set

l is set

G is set

[k,l,G] is V15() V16() set

[k,l] is non empty V15() set

{k,l} is non empty set

{k} is non empty trivial 1 -element set

{{k,l},{k}} is non empty set

[[k,l],G] is non empty V15() set

{[k,l],G} is non empty set

{[k,l]} is Relation-like Function-like constant non empty trivial 1 -element set

{{[k,l],G},{[k,l]}} is non empty set

i . (k,l,G) is set

Funcs (k,l) is functional set

Funcs (l,G) is functional set

((Funcs (k,l)),(Funcs (l,G))) is Relation-like [:(Funcs (l,G)),(Funcs (k,l)):] -defined Function-like V14([:(Funcs (l,G)),(Funcs (k,l)):]) Function-yielding V25() () set

[:(Funcs (l,G)),(Funcs (k,l)):] is Relation-like set

j is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) Function-yielding V25() set

k is set

j . k is Relation-like Function-like set

G is set

c is set

i9 is set

[G,c,i9] is V15() V16() set

[G,c] is non empty V15() set

{G,c} is non empty set

{G} is non empty trivial 1 -element set

{{G,c},{G}} is non empty set

[[G,c],i9] is non empty V15() set

{[G,c],i9} is non empty set

{[G,c]} is Relation-like Function-like constant non empty trivial 1 -element set

{{[G,c],i9},{[G,c]}} is non empty set

(A,C) is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

(A,C) . k is set

(A,C) . (G,c,i9) is set

C . (G,i9) is set

[G,i9] is non empty V15() set

{G,i9} is non empty set

{{G,i9},{G}} is non empty set

C . [G,i9] is set

j . (G,c,i9) is set

Funcs (G,c) is functional set

Funcs (c,i9) is functional set

((Funcs (G,c)),(Funcs (c,i9))) is Relation-like [:(Funcs (c,i9)),(Funcs (G,c)):] -defined Function-like V14([:(Funcs (c,i9)),(Funcs (G,c)):]) Function-yielding V25() () set

[:(Funcs (c,i9)),(Funcs (G,c)):] is Relation-like set

C . (G,c) is set

C . [G,c] is set

C . (c,i9) is set

[c,i9] is non empty V15() set

{c,i9} is non empty set

{c} is non empty trivial 1 -element set

{{c,i9},{c}} is non empty set

C . [c,i9] is set

(A,C,C) is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set

(A,C,C) . (G,c,i9) is set

(A,C,C) . k is set

Funcs (G,i9) is functional set

l is Relation-like Function-like set

proj2 l is set

proj1 l is set

[:((A,C,C) . k),((A,C) . k):] is Relation-like set

bool [:((A,C,C) . k),((A,C) . k):] is non empty set

k is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) ManySortedFunction of (A,C,C),(A,C)

(A,C,k) is non empty () ()

the carrier of (A,C,k) is non empty set

the of (A,C,k) is Relation-like [: the carrier of (A,C,k), the carrier of (A,C,k):] -defined Function-like V14([: the carrier of (A,C,k), the carrier of (A,C,k):]) set

[: the carrier of (A,C,k), the carrier of (A,C,k):] is Relation-like non empty set

the of (A,C,k) is Relation-like [: the carrier of (A,C,k), the carrier of (A,C,k), the carrier of (A,C,k):] -defined Function-like V14([: the carrier of (A,C,k), the carrier of (A,C,k), the carrier of (A,C,k):]) ManySortedFunction of ( the carrier of (A,C,k), the of (A,C,k), the of (A,C,k)),( the carrier of (A,C,k), the of (A,C,k))

[: the carrier of (A,C,k), the carrier of (A,C,k), the carrier of (A,C,k):] is non empty set

( the carrier of (A,C,k), the of (A,C,k), the of (A,C,k)) is Relation-like [: the carrier of (A,C,k), the carrier of (A,C,k), the carrier of (A,C,k):] -defined Function-like V14([: the carrier of (A,C,k), the carrier of (A,C,k), the carrier of (A,C,k):]) set

( the carrier of (A,C,k), the of (A,C,k)) is Relation-like [: the carrier of (A,C,k), the carrier of (A,C,k), the carrier of (A,C,k):] -defined Function-like V14([: the carrier of (A,C,k), the carrier of (A,C,k), the carrier of (A,C,k):]) set

G is Element of the carrier of (A,C,k)

c is Element of the carrier of (A,C,k)

i9 is Element of the carrier of (A,C,k)

( the carrier of (A,C,k), the of (A,C,k), the of (A,C,k),G,c,i9) is Relation-like [:( the of (A,C,k) . (c,i9)),( the of (A,C,k) . (G,c)):] -defined the of (A,C,k) . (G,i9) -valued Function-like quasi_total Element of bool [:[:( the of (A,C,k) . (c,i9)),( the of (A,C,k) . (G,c)):],( the of (A,C,k) . (G,i9)):]

the of (A,C,k) . (c,i9) is set

[c,i9] is non empty V15() set

{c,i9} is non empty set

{c} is non empty trivial 1 -element set

{{c,i9},{c}} is non empty set

the of (A,C,k) . [c,i9] is set

the of (A,C,k) . (G,c) is set

[G,c] is non empty V15() set

{G,c} is non empty set

{G} is non empty trivial 1 -element set

{{G,c},{G}} is non empty set

the of (A,C,k) . [G,c] is set

[:( the of (A,C,k) . (c,i9)),( the of (A,C,k) . (G,c)):] is Relation-like set

the of (A,C,k) . (G,i9) is set

[G,i9] is non empty V15() set

{G,i9} is non empty set

{{G,i9},{G}} is non empty set

the of (A,C,k) . [G,i9] is set

[:[:( the of (A,C,k) . (c,i9)),( the of (A,C,k) . (G,c)):],( the of (A,C,k) . (G,i9)):] is Relation-like set

bool [:[:( the of (A,C,k) . (c,i9)),( the of (A,C,k) . (G,c)):],( the of (A,C,k) . (G,i9)):] is non empty set

Funcs (G,c) is functional set

Funcs (c,i9) is functional set

((Funcs (G,c)),(Funcs (c,i9))) is Relation-like [:(Funcs (c,i9)),(Funcs (G,c)):] -defined Function-like V14([:(Funcs (c,i9)),(Funcs (G,c)):]) Function-yielding V25() () set

[:(Funcs (c,i9)),(Funcs (G,c)):] is Relation-like set

((A,C,k),c,i9) is set

((A,C,k),G,c) is set

[:((A,C,k),c,i9),((A,C,k),G,c):] is Relation-like set

((Funcs (G,c)),(Funcs (c,i9))) | [:((A,C,k),c,i9),((A,C,k),G,c):] is Relation-like [:((A,C,k),c,i9),((A,C,k),G,c):] -defined [:(Funcs (c,i9)),(Funcs (G,c)):] -defined Function-like Function-yielding V25() set

proj1 ((Funcs (G,c)),(Funcs (c,i9))) is set

G is non empty () () ()

the carrier of G is non empty set

c is Element of the carrier of G

i9 is Element of the carrier of G

(G,c,i9) is set

the of G is Relation-like [: the carrier of G, the carrier of G:] -defined Function-like V14([: the carrier of G, the carrier of G:]) set

[: the carrier of G, the carrier of G:] is Relation-like non empty set

the of G . (c,i9) is set

[c,i9] is non empty V15() set

{c,i9} is non empty set

{c} is non empty trivial 1 -element set

{{c,i9},{c}} is non empty set

the of G . [c,i9] is set

Funcs (c,i9) is functional set

C is non empty () () ()

the carrier of C is non empty set

i is non empty () () ()

the carrier of i is non empty set

j is set

k is set

the of C is Relation-like [: the carrier of C, the carrier of C:] -defined Function-like V14([: the carrier of C, the carrier of C:]) set

[: the carrier of C, the carrier of C:] is Relation-like non empty set

the of C . (j,k) is set

[j,k] is non empty V15() set

{j,k} is non empty set

{j} is non empty trivial 1 -element set

{{j,k},{j}} is non empty set

the of C . [j,k] is set

l is Element of the carrier of C

G is Element of the carrier of C

(C,l,G) is set

the of C . (l,G) is set

[l,G] is non empty V15() set

{l,G} is non empty set

{l} is non empty trivial 1 -element set

{{l,G},{l}} is non empty set

the of C . [l,G] is set

Funcs (l,G) is functional set

c is Element of the carrier of i

i9 is Element of the carrier of i

(i,c,i9) is set

the of i is Relation-like [: the carrier of i, the carrier of i:] -defined Function-like V14([: the carrier of i, the carrier of i:]) set

[: the carrier of i, the carrier of i:] is Relation-like non empty set

the of i . (c,i9) is set

[c,i9] is non empty V15() set

{c,i9} is non empty set

{c} is non empty trivial 1 -element set

{{c,i9},{c}} is non empty set

the of i . [c,i9] is set

the of i . (j,k) is set

the of i . [j,k] is set

j is set

k is set

l is set

c is Element of the carrier of C

i9 is Element of the carrier of C

(C,c,i9) is set

the of C . (c,i9) is set

[c,i9] is non empty V15() set

{c,i9} is non empty set

{c} is non empty trivial 1 -element set

{{c,i9},{c}} is non empty set

the of C . [c,i9] is set

k9 is Element of the carrier of i

l9 is Element of the carrier of i

(i,k9,l9) is set

the of i . (k9,l9) is set

[k9,l9] is non empty V15() set

{k9,l9} is non empty set

{k9} is non empty trivial 1 -element set

{{k9,l9},{k9}} is non empty set

the of i . [k9,l9] is set

G is Element of the carrier of C

(C,G,c) is set

the of C . (G,c) is set

[G,c] is non empty V15() set

{G,c} is non empty set

{G} is non empty trivial 1 -element set

{{G,c},{G}} is non empty set

the of C . [G,c] is set

j9 is Element of the carrier of i

(i,j9,k9) is set

the of i . (j9,k9) is set

[j9,k9] is non empty V15() set

{j9,k9} is non empty set

{j9} is non empty trivial 1 -element set

{{j9,k9},{j9}} is non empty set

the of i . [j9,k9] is set

the of C is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like V14([: the carrier of C, the carrier of C, the carrier of C:]) ManySortedFunction of ( the carrier of C, the of C, the of C),( the carrier of C, the of C)

[: the carrier of C, the carrier of C, the carrier of C:] is non empty set

( the carrier of C, the of C, the of C) is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like V14([: the carrier of C, the carrier of C, the carrier of C:]) set

( the carrier of C, the of C) is Relation-like [: the carrier of C, the carrier of C, the carrier of C:] -defined Function-like V14([: the carrier of C, the carrier of C, the carrier of C:]) set

the of C . (j,k,l) is set

Funcs (j9,k9) is functional set

Funcs (k9,l9) is functional set

((Funcs (j9,k9)),(Funcs (k9,l9))) is Relation-like [:(Funcs (k9,l9)),(Funcs (j9,k9)):] -defined Function-like V14([:(Funcs (k9,l9)),(Funcs (j9,k9)):]) Function-yielding V25() () set

[:(Funcs (k9,l9)),(Funcs (j9,k9)):] is Relation-like set

[:(i,k9,l9),(i,j9,k9):] is Relation-like set

((Funcs (j9,k9)),(Funcs (k9,l9))) | [:(i,k9,l9),(i,j9,k9):] is Relation-like [:(i,k9,l9),(i,j9,k9):] -defined [:(Funcs (k9,l9)),(Funcs (j9,k9)):] -defined Function-like Function-yielding V25() set

the of i is Relation-like [: the carrier of i, the carrier of i, the carrier of i:] -defined Function-like V14([: the carrier of i, the carrier of i, the carrier of i:]) ManySortedFunction of ( the carrier of i, the of i, the of i),( the carrier of i, the of i)

[: the carrier of i, the carrier of i, the carrier of i:] is non empty set

( the carrier of i, the of i, the of i) is Relation-like [: the carrier of i, the carrier of i, the carrier of i:] -defined Function-like V14([: the carrier of i, the carrier of i, the carrier of i:]) set

( the carrier of i, the of i) is Relation-like [: the carrier of i, the carrier of i, the carrier of i:] -defined Function-like V14([: the carrier of i, the carrier of i, the carrier of i:]) set

the of i . (j,k,l) is set

A is non empty set

(A) is non empty () () ()

the of (A) is Relation-like [: the carrier of (A), the carrier of (A):] -defined Function-like V14([: the carrier of (A), the carrier of (A):]) set

the carrier of (A) is non empty set

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

the of (A) is Relation-like [: the carrier of (A), the carrier of (A), the carrier of (A):] -defined Function-like V14([: the carrier of (A), the carrier of (A), the carrier of (A):]) ManySortedFunction of ( the carrier of (A), the of (A), the of (A)),( the carrier of (A), the of (A))

[: the carrier of (A), the carrier of (A), the carrier of (A):] is non empty set

( the carrier of (A), the of (A), the of (A)) is Relation-like [: the carrier of (A), the carrier of (A), the carrier of (A):] -defined Function-like V14([: the carrier of (A), the carrier of (A), the carrier of (A):]) set

( the carrier of (A), the of (A)) is Relation-like [: the carrier of (A), the carrier of (A), the carrier of (A):] -defined Function-like V14([: the carrier of (A), the carrier of (A), the carrier of (A):]) set

j is Element of the carrier of (A)

k is Element of the carrier of (A)

((A),j,k) is set

the of (A) . (j,k) is set

[j,k] is non empty V15() set

{j,k} is non empty set

{j} is non empty trivial 1 -element set

{{j,k},{j}} is non empty set

the of (A) . [j,k] is set

l is Element of the carrier of (A)

((A),k,l) is set

the of (A) . (k,l) is set

[k,l] is non empty V15() set

{k,l} is non empty set

{k} is non empty trivial 1 -element set

{{k,l},{k}} is non empty set

the of (A) . [k,l] is set

((A),j,l) is set

the of (A) . (j,l) is set

[j,l] is non empty V15() set

{j,l} is non