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
F1() is set
F2() is set
[:F1(),F2():] is Relation-like set
A is Relation-like Function-like set
proj1 A is set
C is Relation-like [:F1(),F2():] -defined Function-like V14([:F1(),F2():]) set
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
F3(i,j) is set
[i,j] `1 is set
[i,j] `2 is set
F1() is non empty set
F2() is non empty set
[:F1(),F2():] is Relation-like non empty set
A is Relation-like [:F1(),F2():] -defined Function-like V14([:F1(),F2():]) set
C is Element of F1()
i is Element of F2()
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
F3(C,i) is set
F1() is set
F2() is set
F3() is set
[:F1(),F2(),F3():] is set
A is Relation-like Function-like set
proj1 A is set
C is Relation-like [:F1(),F2(),F3():] -defined Function-like V14([:F1(),F2(),F3():]) set
i is set
j is set
k is set
C . (i,j,k) is set
F4(i,j,k) 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
[[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
F1() is non empty set
F2() is non empty set
F3() is non empty set
[:F1(),F2(),F3():] is non empty set
A is Relation-like [:F1(),F2(),F3():] -defined Function-like V14([:F1(),F2(),F3():]) set
C is Element of F1()
i is Element of F2()
j is Element of F3()
A . (C,i,j) is set
F4(C,i,j) is set
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