:: 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₁() is set
F₂() is set
[:F₁(),F₂():] is Relation-like set
A is Relation-like Function-like set
proj1 A is set
C is Relation-like [:F₁(),F₂():] -defined Function-like V14([:F₁(),F₂():]) 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
F₃(i,j) is set
[i,j] `1 is set
[i,j] `2 is set
F₁() is non empty set
F₂() is non empty set
[:F₁(),F₂():] is Relation-like non empty set
A is Relation-like [:F₁(),F₂():] -defined Function-like V14([:F₁(),F₂():]) set
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₃(C,i) is set
F₁() is set
F₂() is set
F₃() is set
[:F₁(),F₂(),F₃():] is set
A is Relation-like Function-like set
proj1 A is set
C is Relation-like [:F₁(),F₂(),F₃():] -defined Function-like V14([:F₁(),F₂(),F₃():]) set
i is set
j is set
k is set
C . (i,j,k) is set
F₄(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
F₁() is non empty set
F₂() is non empty set
F₃() is non empty set
[:F₁(),F₂(),F₃():] is non empty set
A is Relation-like [:F₁(),F₂(),F₃():] -defined Function-like V14([:F₁(),F₂(),F₃():]) set
C is Element of F₁()
i is Element of F₂()
j is Element of F₃()
A . (C,i,j) is set
F₄(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 empty set
{{j,l},{j}} is non empty set
the of (A) . [j,l] is set
Funcs (j,k) is functional set
Funcs (k,l) is functional set
Funcs (j,l) is functional set
j is Element of the carrier of (A)
k is Element of the carrier of (A)
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)
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
G is Element of the carrier of (A)
the of (A) . (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 (A) . [l,G] is set
( the carrier of (A), the of (A), the of (A),j,l,G) is Relation-like [:( the of (A) . (l,G)),( the of (A) . (j,l)):] -defined the of (A) . (j,G) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (l,G)),( the of (A) . (j,l)):],( the of (A) . (j,G)):]
the of (A) . (j,l) is set
[j,l] is non empty V15() set
{j,l} is non empty set
{{j,l},{j}} is non empty set
the of (A) . [j,l] is set
[:( the of (A) . (l,G)),( the of (A) . (j,l)):] is Relation-like set
the of (A) . (j,G) is set
[j,G] is non empty V15() set
{j,G} is non empty set
{{j,G},{j}} is non empty set
the of (A) . [j,G] is set
[:[:( the of (A) . (l,G)),( the of (A) . (j,l)):],( the of (A) . (j,G)):] is Relation-like set
bool [:[:( the of (A) . (l,G)),( the of (A) . (j,l)):],( the of (A) . (j,G)):] is non empty set
( the carrier of (A), the of (A), the of (A),j,k,l) is Relation-like [:( the of (A) . (k,l)),( the of (A) . (j,k)):] -defined the of (A) . (j,l) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (k,l)),( the of (A) . (j,k)):],( the of (A) . (j,l)):]
[:( the of (A) . (k,l)),( the of (A) . (j,k)):] is Relation-like set
[:[:( the of (A) . (k,l)),( the of (A) . (j,k)):],( the of (A) . (j,l)):] is Relation-like set
bool [:[:( the of (A) . (k,l)),( the of (A) . (j,k)):],( the of (A) . (j,l)):] is non empty set
( the carrier of (A), the of (A), the of (A),j,k,G) is Relation-like [:( the of (A) . (k,G)),( the of (A) . (j,k)):] -defined the of (A) . (j,G) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (k,G)),( the of (A) . (j,k)):],( the of (A) . (j,G)):]
the of (A) . (k,G) is set
[k,G] is non empty V15() set
{k,G} is non empty set
{{k,G},{k}} is non empty set
the of (A) . [k,G] is set
[:( the of (A) . (k,G)),( the of (A) . (j,k)):] is Relation-like set
[:[:( the of (A) . (k,G)),( the of (A) . (j,k)):],( the of (A) . (j,G)):] is Relation-like set
bool [:[:( the of (A) . (k,G)),( the of (A) . (j,k)):],( the of (A) . (j,G)):] is non empty set
( the carrier of (A), the of (A), the of (A),k,l,G) is Relation-like [:( the of (A) . (l,G)),( the of (A) . (k,l)):] -defined the of (A) . (k,G) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (l,G)),( the of (A) . (k,l)):],( the of (A) . (k,G)):]
[:( the of (A) . (l,G)),( the of (A) . (k,l)):] is Relation-like set
[:[:( the of (A) . (l,G)),( the of (A) . (k,l)):],( the of (A) . (k,G)):] is Relation-like set
bool [:[:( the of (A) . (l,G)),( the of (A) . (k,l)):],( the of (A) . (k,G)):] is non empty set
l9 is set
f is set
g is set
( the carrier of (A), the of (A), the of (A),j,k,l) . (f,l9) is set
[f,l9] is non empty V15() set
{f,l9} is non empty set
{f} is non empty trivial 1 -element set
{{f,l9},{f}} is non empty set
( the carrier of (A), the of (A), the of (A),j,k,l) . [f,l9] is set
( the carrier of (A), the of (A), the of (A),j,l,G) . (g,(( the carrier of (A), the of (A), the of (A),j,k,l) . (f,l9))) is set
[g,(( the carrier of (A), the of (A), the of (A),j,k,l) . (f,l9))] is non empty V15() set
{g,(( the carrier of (A), the of (A), the of (A),j,k,l) . (f,l9))} is non empty set
{g} is non empty trivial 1 -element set
{{g,(( the carrier of (A), the of (A), the of (A),j,k,l) . (f,l9))},{g}} is non empty set
( the carrier of (A), the of (A), the of (A),j,l,G) . [g,(( the carrier of (A), the of (A), the of (A),j,k,l) . (f,l9))] is set
( the carrier of (A), the of (A), the of (A),k,l,G) . (g,f) is set
[g,f] is non empty V15() set
{g,f} is non empty set
{{g,f},{g}} is non empty set
( the carrier of (A), the of (A), the of (A),k,l,G) . [g,f] is set
( the carrier of (A), the of (A), the of (A),j,k,G) . ((( the carrier of (A), the of (A), the of (A),k,l,G) . (g,f)),l9) is set
[(( the carrier of (A), the of (A), the of (A),k,l,G) . (g,f)),l9] is non empty V15() set
{(( the carrier of (A), the of (A), the of (A),k,l,G) . (g,f)),l9} is non empty set
{(( the carrier of (A), the of (A), the of (A),k,l,G) . (g,f))} is non empty trivial 1 -element set
{{(( the carrier of (A), the of (A), the of (A),k,l,G) . (g,f)),l9},{(( the carrier of (A), the of (A), the of (A),k,l,G) . (g,f))}} is non empty set
( the carrier of (A), the of (A), the of (A),j,k,G) . [(( the carrier of (A), the of (A), the of (A),k,l,G) . (g,f)),l9] is set
j9 is Element of the carrier of (A)
k9 is Element of the carrier of (A)
((A),j9,k9) is set
the of (A) . (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 (A) . [j9,k9] is set
i9 is Element of the carrier of (A)
((A),i9,j9) is set
the of (A) . (i9,j9) is set
[i9,j9] is non empty V15() set
{i9,j9} is non empty set
{i9} is non empty trivial 1 -element set
{{i9,j9},{i9}} is non empty set
the of (A) . [i9,j9] is set
Funcs (l,G) is functional set
c is Element of the carrier of (A)
((A),c,i9) is set
the of (A) . (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,i9] is set
Funcs (j,k) is functional set
Funcs (k,l) is functional set
((A),i9,k9) is set
the of (A) . (i9,k9) is set
[i9,k9] is non empty V15() set
{i9,k9} is non empty set
{{i9,k9},{i9}} is non empty set
the of (A) . [i9,k9] is set
g99 is Element of ((A),i9,j9)
h is Element of ((A),j9,k9)
((A),i9,j9,k9,g99,h) is Element of ((A),i9,k9)
g9 is Relation-like Function-like set
h9 is Relation-like Function-like set
g9 * h9 is Relation-like Function-like set
((A),c,j9) is set
the of (A) . (c,j9) is set
[c,j9] is non empty V15() set
{c,j9} is non empty set
{{c,j9},{c}} is non empty set
the of (A) . [c,j9] is set
f99 is Element of ((A),c,i9)
((A),c,i9,j9,f99,g99) is Element of ((A),c,j9)
f9 is Relation-like Function-like set
f9 * g9 is Relation-like Function-like set
((A),c,k9) is set
the of (A) . (c,k9) is set
[c,k9] is non empty V15() set
{c,k9} is non empty set
{{c,k9},{c}} is non empty set
the of (A) . [c,k9] is set
((A),c,j9,k9,((A),c,i9,j9,f99,g99),h) is Element of ((A),c,k9)
(f9 * g9) * h9 is Relation-like Function-like set
f9 * (g9 * h9) is Relation-like Function-like set
((A),c,i9,k9,f99,((A),i9,j9,k9,g99,h)) is Element of ((A),c,k9)
j is Element of the carrier of (A)
the of (A) . (j,j) is set
[j,j] is non empty V15() set
{j,j} is non empty set
{j} is non empty trivial 1 -element set
{{j,j},{j}} is non empty set
the of (A) . [j,j] is set
id j is Relation-like j -defined j -valued Function-like one-to-one V14(j) set
k is Element of the carrier of (A)
((A),k,k) is set
the of (A) . (k,k) is set
[k,k] is non empty V15() set
{k,k} is non empty set
{k} is non empty trivial 1 -element set
{{k,k},{k}} is non empty set
the of (A) . [k,k] is set
Funcs (j,j) is functional non empty set
G is Element of the carrier of (A)
the of (A) . (G,j) is set
[G,j] is non empty V15() set
{G,j} is non empty set
{G} is non empty trivial 1 -element set
{{G,j},{G}} is non empty set
the of (A) . [G,j] is set
( the carrier of (A), the of (A), the of (A),G,j,j) is Relation-like [:( the of (A) . (j,j)),( the of (A) . (G,j)):] -defined the of (A) . (G,j) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (j,j)),( the of (A) . (G,j)):],( the of (A) . (G,j)):]
[:( the of (A) . (j,j)),( the of (A) . (G,j)):] is Relation-like set
[:[:( the of (A) . (j,j)),( the of (A) . (G,j)):],( the of (A) . (G,j)):] is Relation-like set
bool [:[:( the of (A) . (j,j)),( the of (A) . (G,j)):],( the of (A) . (G,j)):] is non empty set
c is set
( the carrier of (A), the of (A), the of (A),G,j,j) . ((id j),c) is set
[(id j),c] is non empty V15() set
{(id j),c} is non empty set
{(id j)} is functional non empty trivial 1 -element set
{{(id j),c},{(id j)}} is non empty set
( the carrier of (A), the of (A), the of (A),G,j,j) . [(id j),c] is set
i9 is Element of the carrier of (A)
((A),i9,k) is set
the of (A) . (i9,k) is set
[i9,k] is non empty V15() set
{i9,k} is non empty set
{i9} is non empty trivial 1 -element set
{{i9,k},{i9}} is non empty set
the of (A) . [i9,k] is set
Funcs (G,j) is functional set
[:G,j:] is Relation-like set
bool [:G,j:] is non empty set
j9 is Element of ((A),i9,k)
l is Element of ((A),k,k)
((A),i9,k,k,j9,l) is Element of ((A),i9,k)
k9 is Relation-like G -defined j -valued Function-like quasi_total Element of bool [:G,j:]
k9 * (id j) is Relation-like G -defined j -valued Function-like set
j is Element of the carrier of (A)
the of (A) . (j,j) is set
[j,j] is non empty V15() set
{j,j} is non empty set
{j} is non empty trivial 1 -element set
{{j,j},{j}} is non empty set
the of (A) . [j,j] is set
id j is Relation-like j -defined j -valued Function-like one-to-one V14(j) set
k is Element of the carrier of (A)
((A),k,k) is set
the of (A) . (k,k) is set
[k,k] is non empty V15() set
{k,k} is non empty set
{k} is non empty trivial 1 -element set
{{k,k},{k}} is non empty set
the of (A) . [k,k] is set
Funcs (j,j) is functional non empty set
G is Element of the carrier of (A)
the of (A) . (j,G) is set
[j,G] is non empty V15() set
{j,G} is non empty set
{{j,G},{j}} is non empty set
the of (A) . [j,G] is set
( the carrier of (A), the of (A), the of (A),j,j,G) is Relation-like [:( the of (A) . (j,G)),( the of (A) . (j,j)):] -defined the of (A) . (j,G) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (j,G)),( the of (A) . (j,j)):],( the of (A) . (j,G)):]
[:( the of (A) . (j,G)),( the of (A) . (j,j)):] is Relation-like set
[:[:( the of (A) . (j,G)),( the of (A) . (j,j)):],( the of (A) . (j,G)):] is Relation-like set
bool [:[:( the of (A) . (j,G)),( the of (A) . (j,j)):],( the of (A) . (j,G)):] is non empty set
c is set
( the carrier of (A), the of (A), the of (A),j,j,G) . (c,(id j)) is set
[c,(id j)] is non empty V15() set
{c,(id j)} is non empty set
{c} is non empty trivial 1 -element set
{{c,(id j)},{c}} is non empty set
( the carrier of (A), the of (A), the of (A),j,j,G) . [c,(id j)] is set
i9 is Element of the carrier of (A)
((A),k,i9) is set
the of (A) . (k,i9) is set
[k,i9] is non empty V15() set
{k,i9} is non empty set
{{k,i9},{k}} is non empty set
the of (A) . [k,i9] is set
Funcs (j,G) is functional set
[:j,G:] is Relation-like set
bool [:j,G:] is non empty set
l is Element of ((A),k,k)
j9 is Element of ((A),k,i9)
((A),k,k,i9,l,j9) is Element of ((A),k,i9)
k9 is Relation-like j -defined G -valued Function-like quasi_total Element of bool [:j,G:]
(id j) * k9 is Relation-like j -defined G -valued Function-like set
({{}}) is non empty () () ()
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
proj1 ( the carrier of A, the of A, the of A,C,i,j) is Relation-like set
(A,i,j) is set
(A,C,i) is set
[:(A,i,j),(A,C,i):] is Relation-like set
proj2 ( the carrier of A, the of A, the of A,C,i,j) is set
(A,C,j) is set
A is non empty () ()
the carrier of A is non empty set
C is Element of the carrier of A
(A,C,C) 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,C) is set
[C,C] is non empty V15() set
{C,C} is non empty set
{C} is non empty trivial 1 -element set
{{C,C},{C}} is non empty set
the of A . [C,C] 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
i is set
A is non empty set
(A) is non empty () () ()
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
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
(A,i,j) is set
(A,C,i) is set
[:(A,i,j),(A,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
(A,C,j) is set
proj1 ( the carrier of A, the of A, the of A,C,i,j) is Relation-like set
proj1 ((Funcs (C,i)),(Funcs (i,j))) is set
proj1 (((Funcs (C,i)),(Funcs (i,j))) | [:(A,i,j),(A,C,i):]) is set
[:(Funcs (i,j)),(Funcs (C,i)):] /\ [:(A,i,j),(A,C,i):] is Relation-like set
G is set
c is set
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 carrier of A, the of A, the of A,C,i,j) . G is set
k9 is Element of (A,i,j)
j9 is Element of (A,C,i)
( the carrier of A, the of A, the of A,C,i,j) . (k9,j9) is set
[k9,j9] is non empty V15() set
{k9,j9} is non empty set
{k9} is non empty trivial 1 -element set
{{k9,j9},{k9}} is non empty set
( the carrier of A, the of A, the of A,C,i,j) . [k9,j9] is set
(A,C,i,j,j9,k9) is Element of (A,C,j)
f is Relation-like Function-like set
l9 is Relation-like Function-like set
f * l9 is Relation-like Function-like set
((Funcs (C,i)),(Funcs (i,j))) . (l9,f) is set
[l9,f] is non empty V15() set
{l9,f} is functional non empty set
{l9} is functional non empty trivial 1 -element set
{{l9,f},{l9}} is non empty set
((Funcs (C,i)),(Funcs (i,j))) . [l9,f] is Relation-like Function-like set
(((Funcs (C,i)),(Funcs (i,j))) | [:(A,i,j),(A,C,i):]) . G is Relation-like Function-like 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
Funcs (C,i) is functional 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,C,i) is Relation-like [:( the of A . (C,i)),( the of A . (C,C)):] -defined the of A . (C,i) -valued Function-like quasi_total Element of bool [:[:( the of A . (C,i)),( the of A . (C,C)):],( the of A . (C,i)):]
the of A . (C,C) is set
[C,C] is non empty V15() set
{C,C} is non empty set
{{C,C},{C}} is non empty set
the of A . [C,C] is set
[:( the of A . (C,i)),( the of A . (C,C)):] is Relation-like set
[:[:( the of A . (C,i)),( the of A . (C,C)):],( the of A . (C,i)):] is Relation-like set
bool [:[:( the of A . (C,i)),( the of A . (C,C)):],( the of A . (C,i)):] is non empty set
Funcs (C,C) is functional non empty set
((Funcs (C,C)),(Funcs (C,i))) is Relation-like [:(Funcs (C,i)),(Funcs (C,C)):] -defined Function-like V14([:(Funcs (C,i)),(Funcs (C,C)):]) Function-yielding V25() () set
[:(Funcs (C,i)),(Funcs (C,C)):] is Relation-like set
proj1 ( the carrier of A, the of A, the of A,C,C,i) is Relation-like set
(A,C,C) is set
[:(A,C,i),(A,C,C):] is Relation-like set
proj1 ((Funcs (C,C)),(Funcs (C,i))) is set
((Funcs (C,C)),(Funcs (C,i))) | [:(A,C,i),(A,C,C):] is Relation-like [:(A,C,i),(A,C,C):] -defined [:(Funcs (C,i)),(Funcs (C,C)):] -defined Function-like Function-yielding V25() set
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)
G is Relation-like Function-like set
l is Element of (A,i,j)
c is Relation-like Function-like set
(A,C,i,j,k,l) is Element of (A,C,j)
G * c is Relation-like Function-like set
A is non empty () ()
the carrier of A is non empty set
C is Element of the carrier of A
(A,C,C) 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,C) is set
[C,C] is non empty V15() set
{C,C} is non empty set
{C} is non empty trivial 1 -element set
{{C,C},{C}} is non empty set
the of A . [C,C] 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
i is set
j is Element of (A,C,C)
k is Element of the carrier of A
(A,C,k) is set
the of A . (C,k) is set
[C,k] is non empty V15() set
{C,k} is non empty set
{{C,k},{C}} is non empty set
the of A . [C,k] is set
l is Element of (A,C,k)
(A,C,C,k,j,l) is Element of (A,C,k)
( the carrier of A, the of A, the of A,C,C,k) is Relation-like [:( the of A . (C,k)),( the of A . (C,C)):] -defined the of A . (C,k) -valued Function-like quasi_total Element of bool [:[:( the of A . (C,k)),( the of A . (C,C)):],( the of A . (C,k)):]
[:( the of A . (C,k)),( the of A . (C,C)):] is Relation-like set
[:[:( the of A . (C,k)),( the of A . (C,C)):],( the of A . (C,k)):] is Relation-like set
bool [:[:( the of A . (C,k)),( the of A . (C,C)):],( the of A . (C,k)):] is non empty set
( the carrier of A, the of A, the of A,C,C,k) . (l,j) is set
[l,j] is non empty V15() set
{l,j} is non empty set
{l} is non empty trivial 1 -element set
{{l,j},{l}} is non empty set
( the carrier of A, the of A, the of A,C,C,k) . [l,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
i is set
k is Element of (A,C,C)
l is Element of (A,C,C)
( the carrier of A, the of A, the of A,C,C,C) is Relation-like [:( the of A . (C,C)),( the of A . (C,C)):] -defined the of A . (C,C) -valued Function-like quasi_total Element of bool [:[:( the of A . (C,C)),( the of A . (C,C)):],( the of A . (C,C)):]
[:( the of A . (C,C)),( the of A . (C,C)):] is Relation-like set
[:[:( the of A . (C,C)),( the of A . (C,C)):],( the of A . (C,C)):] is Relation-like set
bool [:[:( the of A . (C,C)),( the of A . (C,C)):],( the of A . (C,C)):] is non empty set
j is Element of (A,C,C)
( the carrier of A, the of A, the of A,C,C,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 carrier of A, the of A, the of A,C,C,C) . [j,k] is set
(A,C,C,C,k,j) is Element of (A,C,C)
(A,C,C,C,l,j) is Element of (A,C,C)
( the carrier of A, the of A, the of A,C,C,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
( the carrier of A, the of A, the of A,C,C,C) . [j,l] is set
A is non empty () ()
the carrier of A is non empty set
C is Element of the carrier of A
(A,C) is Element of (A,C,C)
(A,C,C) 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,C) is set
[C,C] is non empty V15() set
{C,C} is non empty set
{C} is non empty trivial 1 -element set
{{C,C},{C}} is non empty set
the of A . [C,C] 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
(A,i) is Element of (A,i,i)
(A,i,i) is set
the of A . (i,i) is set
[i,i] is non empty V15() set
{i,i} is non empty set
{i} is non empty trivial 1 -element set
{{i,i},{i}} is non empty set
the of A . [i,i] is set
j is Element of (A,C,i)
(A,C,i,i,j,(A,i)) is Element of (A,C,i)
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
k is set
l is Element of (A,i,i)
(A,i,i,i,(A,i),l) is Element of (A,i,i)
( the carrier of A, the of A, the of A,i,i,i) is Relation-like [:( the of A . (i,i)),( the of A . (i,i)):] -defined the of A . (i,i) -valued Function-like quasi_total Element of bool [:[:( the of A . (i,i)),( the of A . (i,i)):],( the of A . (i,i)):]
[:( the of A . (i,i)),( the of A . (i,i)):] is Relation-like set
[:[:( the of A . (i,i)),( the of A . (i,i)):],( the of A . (i,i)):] is Relation-like set
bool [:[:( the of A . (i,i)),( the of A . (i,i)):],( the of A . (i,i)):] is non empty set
( the carrier of A, the of A, the of A,i,i,i) . (l,(A,i)) is set
[l,(A,i)] is non empty V15() set
{l,(A,i)} is non empty set
{l} is non empty trivial 1 -element set
{{l,(A,i)},{l}} is non empty set
( the carrier of A, the of A, the of A,i,i,i) . [l,(A,i)] is set
( the carrier of A, the of A, the of A,C,i,i) is Relation-like [:( the of A . (i,i)),( the of A . (C,i)):] -defined the of A . (C,i) -valued Function-like quasi_total Element of bool [:[:( the of A . (i,i)),( the of A . (C,i)):],( the of A . (C,i)):]
[:( the of A . (i,i)),( the of A . (C,i)):] is Relation-like set
[:[:( the of A . (i,i)),( the of A . (C,i)):],( the of A . (C,i)):] is Relation-like set
bool [:[:( the of A . (i,i)),( the of A . (C,i)):],( the of A . (C,i)):] is non empty set
( the carrier of A, the of A, the of A,C,i,i) . (l,j) is set
[l,j] is non empty V15() set
{l,j} is non empty set
{{l,j},{l}} is non empty set
( the carrier of A, the of A, the of A,C,i,i) . [l,j] 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
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 (A,C,i)
G is Element of (A,i,j)
(A,C,i,j,l,G) is Element of (A,C,j)
(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
c is Element of (A,j,k)
(A,C,j,k,(A,C,i,j,l,G),c) is Element of (A,C,k)
(A,C,k) is set
the of A . (C,k) is set
[C,k] is non empty V15() set
{C,k} is non empty set
{{C,k},{C}} is non empty set
the of A . [C,k] is set
(A,i,j,k,G,c) is Element of (A,i,k)
(A,i,k) is set
the of A . (i,k) is set
[i,k] is non empty V15() set
{i,k} is non empty set
{{i,k},{i}} is non empty set
the of A . [i,k] is set
(A,C,i,k,l,(A,i,j,k,G,c)) is Element of (A,C,k)
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,i,j,k) is Relation-like [:( the of A . (j,k)),( the of A . (i,j)):] -defined the of A . (i,k) -valued Function-like quasi_total Element of bool [:[:( the of A . (j,k)),( the of A . (i,j)):],( the of A . (i,k)):]
[:( the of A . (j,k)),( the of A . (i,j)):] is Relation-like set
[:[:( the of A . (j,k)),( the of A . (i,j)):],( the of A . (i,k)):] is Relation-like set
bool [:[:( the of A . (j,k)),( the of A . (i,j)):],( the of A . (i,k)):] is non empty set
( the carrier of A, the of A, the of A,i,j,k) . (c,G) is set
[c,G] is non empty V15() set
{c,G} is non empty set
{c} is non empty trivial 1 -element set
{{c,G},{c}} is non empty set
( the carrier of A, the of A, the of A,i,j,k) . [c,G] is 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
( the carrier of A, the of A, the of A,C,i,j) . (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
( the carrier of A, the of A, the of A,C,i,j) . [G,l] is set
( the carrier of A, the of A, the of A,C,j,k) is Relation-like [:( the of A . (j,k)),( the of A . (C,j)):] -defined the of A . (C,k) -valued Function-like quasi_total Element of bool [:[:( the of A . (j,k)),( the of A . (C,j)):],( the of A . (C,k)):]
[:( the of A . (j,k)),( the of A . (C,j)):] is Relation-like set
[:[:( the of A . (j,k)),( the of A . (C,j)):],( the of A . (C,k)):] is Relation-like set
bool [:[:( the of A . (j,k)),( the of A . (C,j)):],( the of A . (C,k)):] is non empty set
( the carrier of A, the of A, the of A,C,j,k) . (c,(( the carrier of A, the of A, the of A,C,i,j) . (G,l))) is set
[c,(( the carrier of A, the of A, the of A,C,i,j) . (G,l))] is non empty V15() set
{c,(( the carrier of A, the of A, the of A,C,i,j) . (G,l))} is non empty set
{{c,(( the carrier of A, the of A, the of A,C,i,j) . (G,l))},{c}} is non empty set
( the carrier of A, the of A, the of A,C,j,k) . [c,(( the carrier of A, the of A, the of A,C,i,j) . (G,l))] is set
( the carrier of A, the of A, the of A,C,i,k) is Relation-like [:( the of A . (i,k)),( the of A . (C,i)):] -defined the of A . (C,k) -valued Function-like quasi_total Element of bool [:[:( the of A . (i,k)),( the of A . (C,i)):],( the of A . (C,k)):]
[:( the of A . (i,k)),( the of A . (C,i)):] is Relation-like set
[:[:( the of A . (i,k)),( the of A . (C,i)):],( the of A . (C,k)):] is Relation-like set
bool [:[:( the of A . (i,k)),( the of A . (C,i)):],( the of A . (C,k)):] is non empty set
( the carrier of A, the of A, the of A,C,i,k) . ((( the carrier of A, the of A, the of A,i,j,k) . (c,G)),l) is set
[(( the carrier of A, the of A, the of A,i,j,k) . (c,G)),l] is non empty V15() set
{(( the carrier of A, the of A, the of A,i,j,k) . (c,G)),l} is non empty set
{(( the carrier of A, the of A, the of A,i,j,k) . (c,G))} is non empty trivial 1 -element set
{{(( the carrier of A, the of A, the of A,i,j,k) . (c,G)),l},{(( the carrier of A, the of A, the of A,i,j,k) . (c,G))}} is non empty set
( the carrier of A, the of A, the of A,C,i,k) . [(( the carrier of A, the of A, the of A,i,j,k) . (c,G)),l] is set
A is non empty () ()
the carrier of A is non empty set
C is Element of the carrier of A
(A,C) is Element of (A,C,C)
(A,C,C) 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,C) is set
[C,C] is non empty V15() set
{C,C} is non empty set
{C} is non empty trivial 1 -element set
{{C,C},{C}} is non empty set
the of A . [C,C] is set
j is set
{j} is non empty trivial 1 -element set
i is set
{(A,C)} is non empty trivial 1 -element set
C is Element of the carrier of A
(A,C,C) is set
the of A . (C,C) is set
[C,C] is non empty V15() set
{C,C} is non empty set
{C} is non empty trivial 1 -element set
{{C,C},{C}} is non empty set
the of A . [C,C] is set
(A,C) is Element of (A,C,C)
{(A,C)} is non empty trivial 1 -element set
A is ()
the carrier of A is 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 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
(1) is non empty () () () () () () () ()
the carrier of (1) is non empty set
A is Element of the carrier of (1)
((1),A,A) is set
the of (1) is Relation-like [: the carrier of (1), the carrier of (1):] -defined Function-like V14([: the carrier of (1), the carrier of (1):]) set
[: the carrier of (1), the carrier of (1):] is Relation-like non empty set
the of (1) . (A,A) is set
[A,A] is non empty V15() set
{A,A} is non empty set
{A} is non empty trivial 1 -element set
{{A,A},{A}} is non empty set
the of (1) . [A,A] 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
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
c is Element of A
i9 is Element of A
j9 is Element of A
C . (c,c) is set
[c,c] is non empty V15() set
{c,c} is non empty set
{c} is non empty trivial 1 -element set
{{c,c},{c}} is non empty set
C . [c,c] is set
id c is Relation-like c -defined c -valued Function-like one-to-one V14(c) set
{(id c)} is functional non empty trivial 1 -element set
IFEQ (c,c,{(id c)},{}) is set
i . j is set
i . (c,i9,j9) is set
[(id c),(id c)] is non empty V15() set
{(id c),(id c)} is functional non empty set
{{(id c),(id c)},{(id c)}} is non empty set
[(id c),(id c)] .--> (id c) is Relation-like {[(id c),(id c)]} -defined Function-like one-to-one Function-yielding V25() set
{[(id c),(id c)]} is Relation-like Function-like constant non empty trivial 1 -element set
{[(id c),(id c)]} --> (id c) is Relation-like {[(id c),(id c)]} -defined {(id c)} -valued Function-like constant non empty V14({[(id c),(id c)]}) quasi_total Function-yielding V25() Element of bool [:{[(id c),(id c)]},{(id c)}:]
[:{[(id c),(id c)]},{(id c)}:] is Relation-like non empty set
bool [:{[(id c),(id c)]},{(id c)}:] is non empty set
IFEQ (i9,j9,([(id c),(id c)] .--> (id c)),{}) is set
IFEQ (c,i9,(IFEQ (i9,j9,([(id c),(id c)] .--> (id c)),{})),{}) is set
(A,C) is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set
(A,C) . j is set
(A,C) . (c,c,c) is set
(A,C,C) is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set
(A,C,C) . j is set
(A,C,C) . (c,c,c) is set
[:{(id c)},{(id c)}:] is Relation-like non empty set
proj1 ([(id c),(id c)] .--> (id c)) is set
[:((A,C,C) . j),((A,C) . j):] is Relation-like set
bool [:((A,C,C) . j),((A,C) . j):] is non empty set
c is Element of A
i9 is Element of A
j9 is Element of A
i . j is set
i . (c,i9,j9) is set
id c is Relation-like c -defined c -valued Function-like one-to-one V14(c) set
[(id c),(id c)] is non empty V15() set
{(id c),(id c)} is functional non empty set
{(id c)} is functional non empty trivial 1 -element set
{{(id c),(id c)},{(id c)}} is non empty set
[(id c),(id c)] .--> (id c) is Relation-like {[(id c),(id c)]} -defined Function-like one-to-one Function-yielding V25() set
{[(id c),(id c)]} is Relation-like Function-like constant non empty trivial 1 -element set
{[(id c),(id c)]} --> (id c) is Relation-like {[(id c),(id c)]} -defined {(id c)} -valued Function-like constant non empty V14({[(id c),(id c)]}) quasi_total Function-yielding V25() Element of bool [:{[(id c),(id c)]},{(id c)}:]
[:{[(id c),(id c)]},{(id c)}:] is Relation-like non empty set
bool [:{[(id c),(id c)]},{(id c)}:] is non empty set
IFEQ (i9,j9,([(id c),(id c)] .--> (id c)),{}) is set
IFEQ (c,i9,(IFEQ (i9,j9,([(id c),(id c)] .--> (id c)),{})),{}) is set
i . j is set
i . (c,i9,j9) is set
id c is Relation-like c -defined c -valued Function-like one-to-one V14(c) set
[(id c),(id c)] is non empty V15() set
{(id c),(id c)} is functional non empty set
{(id c)} is functional non empty trivial 1 -element set
{{(id c),(id c)},{(id c)}} is non empty set
[(id c),(id c)] .--> (id c) is Relation-like {[(id c),(id c)]} -defined Function-like one-to-one Function-yielding V25() set
{[(id c),(id c)]} is Relation-like Function-like constant non empty trivial 1 -element set
{[(id c),(id c)]} --> (id c) is Relation-like {[(id c),(id c)]} -defined {(id c)} -valued Function-like constant non empty V14({[(id c),(id c)]}) quasi_total Function-yielding V25() Element of bool [:{[(id c),(id c)]},{(id c)}:]
[:{[(id c),(id c)]},{(id c)}:] is Relation-like non empty set
bool [:{[(id c),(id c)]},{(id c)}:] is non empty set
IFEQ (i9,j9,([(id c),(id c)] .--> (id c)),{}) is set
IFEQ (c,i9,(IFEQ (i9,j9,([(id c),(id c)] .--> (id c)),{})),{}) is set
i . j is set
i . j 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
id c is Relation-like c -defined c -valued Function-like one-to-one V14(c) set
{(id c)} is functional non empty trivial 1 -element set
IFEQ (c,i9,{(id c)},{}) is set
C . (i9,j9) is set
[i9,j9] is non empty V15() set
{i9,j9} is non empty set
{i9} is non empty trivial 1 -element set
{{i9,j9},{i9}} is non empty set
C . [i9,j9] is set
id i9 is Relation-like i9 -defined i9 -valued Function-like one-to-one V14(i9) set
{(id i9)} is functional non empty trivial 1 -element set
IFEQ (i9,j9,{(id i9)},{}) is set
(A,C,C) is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set
(A,C,C) . j is set
(A,C,C) . (c,i9,j9) is set
[:(C . (i9,j9)),(C . (c,i9)):] is Relation-like set
(A,C) is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) set
(A,C) . j is set
[:((A,C,C) . j),((A,C) . j):] is Relation-like set
bool [:((A,C,C) . j),((A,C) . j):] is non empty set
c is Element of A
i9 is Element of A
j9 is Element of A
(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
(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
j is set
proj1 i is set
i . j is set
j is Relation-like [:A,A,A:] -defined Function-like V14([:A,A,A:]) Function-yielding V25() 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
G is Element of the carrier of (A,C,k)
c is Element of the carrier of (A,C,k)
((A,C,k),G,c) is 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) . (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
id G is Relation-like G -defined G -valued Function-like one-to-one V14(G) set
{(id G)} is functional non empty trivial 1 -element set
IFEQ (G,c,{(id G)},{}) is set
G is non empty () () ()
the carrier of G is non empty set
c is Element of the carrier of G
(G,c,c) 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,c) is set
[c,c] is non empty V15() set
{c,c} is non empty set
{c} is non empty trivial 1 -element set
{{c,c},{c}} is non empty set
the of G . [c,c] is set
id c is Relation-like c -defined c -valued Function-like one-to-one V14(c) set
{(id c)} is functional non empty trivial 1 -element set
IFEQ (c,c,{(id c)},{}) is 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
l is set
G is Element of the carrier of i
(i,G,G) 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 . (G,G) is set
[G,G] is non empty V15() set
{G,G} is non empty set
{G} is non empty trivial 1 -element set
{{G,G},{G}} is non empty set
the of i . [G,G] is set
id G is Relation-like G -defined G -valued Function-like one-to-one V14(G) set
{(id G)} is functional non empty trivial 1 -element 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 carrier of i, the of i, the of i,G,G,G) is Relation-like [:( the of i . (G,G)),( the of i . (G,G)):] -defined the of i . (G,G) -valued Function-like quasi_total Element of bool [:[:( the of i . (G,G)),( the of i . (G,G)):],( the of i . (G,G)):]
[:( the of i . (G,G)),( the of i . (G,G)):] is Relation-like set
[:[:( the of i . (G,G)),( the of i . (G,G)):],( the of i . (G,G)):] is Relation-like set
bool [:[:( the of i . (G,G)),( the of i . (G,G)):],( the of i . (G,G)):] is non empty set
[:(i,G,G),(i,G,G):] is Relation-like set
[:[:(i,G,G),(i,G,G):],(i,G,G):] is Relation-like set
bool [:[:(i,G,G),(i,G,G):],(i,G,G):] is non empty set
c is Element of the carrier of C
(C,c,c) 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 . (c,c) is set
[c,c] is non empty V15() set
{c,c} is non empty set
{c} is non empty trivial 1 -element set
{{c,c},{c}} is non empty set
the of C . [c,c] is set
id c is Relation-like c -defined c -valued Function-like one-to-one V14(c) set
{(id c)} is functional non empty trivial 1 -element 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 carrier of C, the of C, the of C,c,c,c) is Relation-like [:( the of C . (c,c)),( the of C . (c,c)):] -defined the of C . (c,c) -valued Function-like quasi_total Element of bool [:[:( the of C . (c,c)),( the of C . (c,c)):],( the of C . (c,c)):]
[:( the of C . (c,c)),( the of C . (c,c)):] is Relation-like set
[:[:( the of C . (c,c)),( the of C . (c,c)):],( the of C . (c,c)):] is Relation-like set
bool [:[:( the of C . (c,c)),( the of C . (c,c)):],( the of C . (c,c)):] is non empty set
[:(C,c,c),(C,c,c):] is Relation-like set
[:[:(C,c,c),(C,c,c):],(C,c,c):] is Relation-like set
bool [:[:(C,c,c),(C,c,c):],(C,c,c):] is non empty set
the of C . (j,k,l) is set
id j is Relation-like j -defined j -valued Function-like one-to-one V14(j) set
((id j),(id j)) :-> (id j) is Relation-like [:{(id j)},{(id j)}:] -defined {(id j)} -valued Function-like non empty V14([:{(id j)},{(id j)}:]) quasi_total Function-yielding V25() Element of bool [:[:{(id j)},{(id j)}:],{(id j)}:]
{(id j)} is functional non empty trivial 1 -element set
[:{(id j)},{(id j)}:] is Relation-like non empty set
[:[:{(id j)},{(id j)}:],{(id j)}:] is Relation-like non empty set
bool [:[:{(id j)},{(id j)}:],{(id j)}:] is non empty set
[(id j),(id j)] is non empty V15() set
{(id j),(id j)} is functional non empty set
{{(id j),(id j)},{(id j)}} is non empty set
{[(id j),(id j)]} is Relation-like Function-like constant non empty trivial 1 -element set
{[(id j),(id j)]} --> (id j) is Relation-like {[(id j),(id j)]} -defined {(id j)} -valued Function-like constant non empty V14({[(id j),(id j)]}) quasi_total Function-yielding V25() Element of bool [:{[(id j),(id j)]},{(id j)}:]
[:{[(id j),(id j)]},{(id j)}:] is Relation-like non empty set
bool [:{[(id j),(id j)]},{(id j)}:] is non empty set
the of i . (j,k,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 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 . (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
j9 is Element of the carrier of C
(C,i9,j9) is set
the of C . (i9,j9) is set
[i9,j9] is non empty V15() set
{i9,j9} is non empty set
{i9} is non empty trivial 1 -element set
{{i9,j9},{i9}} is non empty set
the of C . [i9,j9] 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 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
G is Element of the carrier of i
k9 is Element of the carrier of i
l9 is Element of the carrier of i
( the carrier of i, the of i, the of i,G,k9,l9) is Relation-like [:( the of i . (k9,l9)),( the of i . (G,k9)):] -defined the of i . (G,l9) -valued Function-like quasi_total Element of bool [:[:( the of i . (k9,l9)),( the of i . (G,k9)):],( the of i . (G,l9)):]
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
the of i . (G,k9) is set
[G,k9] is non empty V15() set
{G,k9} is non empty set
{G} is non empty trivial 1 -element set
{{G,k9},{G}} is non empty set
the of i . [G,k9] is set
[:( the of i . (k9,l9)),( the of i . (G,k9)):] is Relation-like set
the of i . (G,l9) is set
[G,l9] is non empty V15() set
{G,l9} is non empty set
{{G,l9},{G}} is non empty set
the of i . [G,l9] is set
[:[:( the of i . (k9,l9)),( the of i . (G,k9)):],( the of i . (G,l9)):] is Relation-like set
bool [:[:( the of i . (k9,l9)),( the of i . (G,k9)):],( the of i . (G,l9)):] is non empty set
(i,k9,l9) is set
(i,G,k9) is set
[:(i,k9,l9),(i,G,k9):] is Relation-like set
(i,G,l9) is set
[:[:(i,k9,l9),(i,G,k9):],(i,G,l9):] is Relation-like set
bool [:[:(i,k9,l9),(i,G,k9):],(i,G,l9):] is non empty 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 carrier of C, the of C, the of C,c,i9,j9) is Relation-like [:( the of C . (i9,j9)),( the of C . (c,i9)):] -defined the of C . (c,j9) -valued Function-like quasi_total Element of bool [:[:( the of C . (i9,j9)),( the of C . (c,i9)):],( the of C . (c,j9)):]
[:( the of C . (i9,j9)),( the of C . (c,i9)):] is Relation-like set
the of C . (c,j9) is set
[c,j9] is non empty V15() set
{c,j9} is non empty set
{{c,j9},{c}} is non empty set
the of C . [c,j9] is set
[:[:( the of C . (i9,j9)),( the of C . (c,i9)):],( the of C . (c,j9)):] is Relation-like set
bool [:[:( the of C . (i9,j9)),( the of C . (c,i9)):],( the of C . (c,j9)):] is non empty set
[:(C,i9,j9),(C,c,i9):] is Relation-like set
(C,c,j9) is set
[:[:(C,i9,j9),(C,c,i9):],(C,c,j9):] is Relation-like set
bool [:[:(C,i9,j9),(C,c,i9):],(C,c,j9):] is non empty set
the of C . (j,k,l) is set
the of i . (j,k,l) 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 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 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 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 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 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 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 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 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 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 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 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
j is Element of A
k is Element of A
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
G is Element of the carrier of C
(C,G,G) is set
the of C . (G,G) is set
[G,G] is non empty V15() set
{G,G} is non empty set
{G} is non empty trivial 1 -element set
{{G,G},{G}} is non empty set
the of C . [G,G] is set
id j is Relation-like j -defined j -valued Function-like one-to-one V14(j) set
{(id j)} is functional non empty trivial 1 -element set
l is Element of the carrier of i
(i,l,l) is set
the of i . (l,l) is set
[l,l] is non empty V15() set
{l,l} is non empty set
{l} is non empty trivial 1 -element set
{{l,l},{l}} is non empty set
the of i . [l,l] is set
the of i . (j,k) is set
the of i . [j,k] is set
k is Element of A
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
G is Element of the carrier of C
i9 is Element of the carrier of C
(C,G,i9) is set
the of C . (G,i9) is set
[G,i9] is non empty V15() set
{G,i9} is non empty set
{G} is non empty trivial 1 -element set
{{G,i9},{G}} is non empty set
the of C . [G,i9] is set
l is Element of the carrier of i
c is Element of the carrier of i
(i,l,c) is set
the of i . (l,c) is set
[l,c] is non empty V15() set
{l,c} is non empty set
{l} is non empty trivial 1 -element set
{{l,c},{l}} is non empty set
the of i . [l,c] is set
the of i . (j,k) is set
the of i . [j,k] is set
k is Element of A
A is ()
the carrier of A is 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 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
A is non empty 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),C,i) is set
((A),i,j) is set
A is non empty 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)
( the carrier of (A), the of (A), the of (A),C,C,C) is Relation-like [:( the of (A) . (C,C)),( the of (A) . (C,C)):] -defined the of (A) . (C,C) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (C,C)),( the of (A) . (C,C)):],( the of (A) . (C,C)):]
the of (A) . (C,C) is set
[C,C] is non empty V15() set
{C,C} is non empty set
{C} is non empty trivial 1 -element set
{{C,C},{C}} is non empty set
the of (A) . [C,C] is set
[:( the of (A) . (C,C)),( the of (A) . (C,C)):] is Relation-like set
[:[:( the of (A) . (C,C)),( the of (A) . (C,C)):],( the of (A) . (C,C)):] is Relation-like set
bool [:[:( the of (A) . (C,C)),( the of (A) . (C,C)):],( the of (A) . (C,C)):] is non empty set
id C is Relation-like C -defined C -valued Function-like one-to-one V14(C) set
((id C),(id C)) :-> (id C) is Relation-like [:{(id C)},{(id C)}:] -defined {(id C)} -valued Function-like non empty V14([:{(id C)},{(id C)}:]) quasi_total Function-yielding V25() Element of bool [:[:{(id C)},{(id C)}:],{(id C)}:]
{(id C)} is functional non empty trivial 1 -element set
[:{(id C)},{(id C)}:] is Relation-like non empty set
[:[:{(id C)},{(id C)}:],{(id C)}:] is Relation-like non empty set
bool [:[:{(id C)},{(id C)}:],{(id C)}:] is non empty set
[(id C),(id C)] is non empty V15() set
{(id C),(id C)} is functional non empty set
{{(id C),(id C)},{(id C)}} is non empty set
{[(id C),(id C)]} is Relation-like Function-like constant non empty trivial 1 -element set
{[(id C),(id C)]} --> (id C) is Relation-like {[(id C),(id C)]} -defined {(id C)} -valued Function-like constant non empty V14({[(id C),(id C)]}) quasi_total Function-yielding V25() Element of bool [:{[(id C),(id C)]},{(id C)}:]
[:{[(id C),(id C)]},{(id C)}:] is Relation-like non empty set
bool [:{[(id C),(id C)]},{(id C)}:] is non empty set
((A),C,C) is set
A is non empty 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
i is Element of the carrier of (A)
j is Element of the carrier of (A)
k is Element of the carrier of (A)
( the carrier of (A), the of (A), the of (A),i,j,k) is Relation-like [:( the of (A) . (j,k)),( the of (A) . (i,j)):] -defined the of (A) . (i,k) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (j,k)),( the of (A) . (i,j)):],( the of (A) . (i,k)):]
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
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) . (j,k)),( the of (A) . (i,j)):] is Relation-like set
the of (A) . (i,k) is set
[i,k] is non empty V15() set
{i,k} is non empty set
{{i,k},{i}} is non empty set
the of (A) . [i,k] is set
[:[:( the of (A) . (j,k)),( the of (A) . (i,j)):],( the of (A) . (i,k)):] is Relation-like set
bool [:[:( the of (A) . (j,k)),( the of (A) . (i,j)):],( the of (A) . (i,k)):] is non empty set
Funcs (i,j) is functional set
Funcs (j,k) is functional set
((Funcs (i,j)),(Funcs (j,k))) is Relation-like [:(Funcs (j,k)),(Funcs (i,j)):] -defined Function-like V14([:(Funcs (j,k)),(Funcs (i,j)):]) Function-yielding V25() () set
[:(Funcs (j,k)),(Funcs (i,j)):] is Relation-like set
((A),j,k) is set
((A),i,j) is set
[:((A),j,k),((A),i,j):] is Relation-like set
((Funcs (i,j)),(Funcs (j,k))) | [:((A),j,k),((A),i,j):] is Relation-like [:((A),j,k),((A),i,j):] -defined [:(Funcs (j,k)),(Funcs (i,j)):] -defined Function-like Function-yielding V25() set
id i is Relation-like i -defined i -valued Function-like one-to-one V14(i) set
Funcs (i,i) is functional non empty set
{(id i)} is functional non empty trivial 1 -element set
((id i),(id i)) :-> (id i) is Relation-like [:{(id i)},{(id i)}:] -defined {(id i)} -valued Function-like non empty V14([:{(id i)},{(id i)}:]) quasi_total Function-yielding V25() Element of bool [:[:{(id i)},{(id i)}:],{(id i)}:]
[:{(id i)},{(id i)}:] is Relation-like non empty set
[:[:{(id i)},{(id i)}:],{(id i)}:] is Relation-like non empty set
bool [:[:{(id i)},{(id i)}:],{(id i)}:] is non empty set
[(id i),(id i)] is non empty V15() set
{(id i),(id i)} is functional non empty set
{{(id i),(id i)},{(id i)}} is non empty set
{[(id i),(id i)]} is Relation-like Function-like constant non empty trivial 1 -element set
{[(id i),(id i)]} --> (id i) is Relation-like {[(id i),(id i)]} -defined {(id i)} -valued Function-like constant non empty V14({[(id i),(id i)]}) quasi_total Function-yielding V25() Element of bool [:{[(id i),(id i)]},{(id i)}:]
[:{[(id i),(id i)]},{(id i)}:] is Relation-like non empty set
bool [:{[(id i),(id i)]},{(id i)}:] is non empty set
({(id i)},{(id i)}) is Relation-like [:{(id i)},{(id i)}:] -defined Function-like V14([:{(id i)},{(id i)}:]) Function-yielding V25() () set
the carrier of (A) is non empty set
i is Element of the carrier of (A)
((A),i,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) . (i,i) is set
[i,i] is non empty V15() set
{i,i} is non empty set
{i} is non empty trivial 1 -element set
{{i,i},{i}} is non empty set
the of (A) . [i,i] is set
id i is Relation-like i -defined i -valued Function-like one-to-one V14(i) set
{(id i)} is functional non empty trivial 1 -element set
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
i is Element of the carrier of (A)
the of (A) . (i,i) is set
[i,i] is non empty V15() set
{i,i} is non empty set
{i} is non empty trivial 1 -element set
{{i,i},{i}} is non empty set
the of (A) . [i,i] is set
j is Element of the carrier of (A)
id j is Relation-like j -defined j -valued Function-like one-to-one V14(j) set
((A),j,j) is set
the of (A) . (j,j) is set
[j,j] is non empty V15() set
{j,j} is non empty set
{j} is non empty trivial 1 -element set
{{j,j},{j}} is non empty set
the of (A) . [j,j] is set
{(id j)} is functional non empty trivial 1 -element set
k is Element of the carrier of (A)
the of (A) . (k,i) is set
[k,i] is non empty V15() set
{k,i} is non empty set
{k} is non empty trivial 1 -element set
{{k,i},{k}} is non empty set
the of (A) . [k,i] is set
( the carrier of (A), the of (A), the of (A),k,i,i) is Relation-like [:( the of (A) . (i,i)),( the of (A) . (k,i)):] -defined the of (A) . (k,i) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (i,i)),( the of (A) . (k,i)):],( the of (A) . (k,i)):]
[:( the of (A) . (i,i)),( the of (A) . (k,i)):] is Relation-like set
[:[:( the of (A) . (i,i)),( the of (A) . (k,i)):],( the of (A) . (k,i)):] is Relation-like set
bool [:[:( the of (A) . (i,i)),( the of (A) . (k,i)):],( the of (A) . (k,i)):] is non empty set
l is set
( the carrier of (A), the of (A), the of (A),k,i,i) . ((id j),l) is set
[(id j),l] is non empty V15() set
{(id j),l} is non empty set
{{(id j),l},{(id j)}} is non empty set
( the carrier of (A), the of (A), the of (A),k,i,i) . [(id j),l] is set
G is Element of the carrier of (A)
((A),G,j) is set
the of (A) . (G,j) is set
[G,j] is non empty V15() set
{G,j} is non empty set
{G} is non empty trivial 1 -element set
{{G,j},{G}} is non empty set
the of (A) . [G,j] is set
id G is Relation-like G -defined G -valued Function-like one-to-one V14(G) set
{(id G)} is functional non empty trivial 1 -element set
((id G),(id G)) :-> (id G) is Relation-like [:{(id G)},{(id G)}:] -defined {(id G)} -valued Function-like non empty V14([:{(id G)},{(id G)}:]) quasi_total Function-yielding V25() Element of bool [:[:{(id G)},{(id G)}:],{(id G)}:]
[:{(id G)},{(id G)}:] is Relation-like non empty set
[:[:{(id G)},{(id G)}:],{(id G)}:] is Relation-like non empty set
bool [:[:{(id G)},{(id G)}:],{(id G)}:] is non empty set
[(id G),(id G)] is non empty V15() set
{(id G),(id G)} is functional non empty set
{{(id G),(id G)},{(id G)}} is non empty set
{[(id G),(id G)]} is Relation-like Function-like constant non empty trivial 1 -element set
{[(id G),(id G)]} --> (id G) is Relation-like {[(id G),(id G)]} -defined {(id G)} -valued Function-like constant non empty V14({[(id G),(id G)]}) quasi_total Function-yielding V25() Element of bool [:{[(id G),(id G)]},{(id G)}:]
[:{[(id G),(id G)]},{(id G)}:] is Relation-like non empty set
bool [:{[(id G),(id G)]},{(id G)}:] is non empty set
(((id G),(id G)) :-> (id G)) . ((id j),l) is set
(((id G),(id G)) :-> (id G)) . [(id j),l] is Relation-like Function-like set
i is Element of the carrier of (A)
the of (A) . (i,i) is set
[i,i] is non empty V15() set
{i,i} is non empty set
{i} is non empty trivial 1 -element set
{{i,i},{i}} is non empty set
the of (A) . [i,i] is set
j is Element of the carrier of (A)
id j is Relation-like j -defined j -valued Function-like one-to-one V14(j) set
((A),j,j) is set
the of (A) . (j,j) is set
[j,j] is non empty V15() set
{j,j} is non empty set
{j} is non empty trivial 1 -element set
{{j,j},{j}} is non empty set
the of (A) . [j,j] is set
{(id j)} is functional non empty trivial 1 -element set
k is Element of the carrier of (A)
the of (A) . (i,k) is set
[i,k] is non empty V15() set
{i,k} is non empty set
{{i,k},{i}} is non empty set
the of (A) . [i,k] is set
( the carrier of (A), the of (A), the of (A),i,i,k) is Relation-like [:( the of (A) . (i,k)),( the of (A) . (i,i)):] -defined the of (A) . (i,k) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (i,k)),( the of (A) . (i,i)):],( the of (A) . (i,k)):]
[:( the of (A) . (i,k)),( the of (A) . (i,i)):] is Relation-like set
[:[:( the of (A) . (i,k)),( the of (A) . (i,i)):],( the of (A) . (i,k)):] is Relation-like set
bool [:[:( the of (A) . (i,k)),( the of (A) . (i,i)):],( the of (A) . (i,k)):] is non empty set
l is set
( the carrier of (A), the of (A), the of (A),i,i,k) . (l,(id j)) is set
[l,(id j)] is non empty V15() set
{l,(id j)} is non empty set
{l} is non empty trivial 1 -element set
{{l,(id j)},{l}} is non empty set
( the carrier of (A), the of (A), the of (A),i,i,k) . [l,(id j)] is set
G is Element of the carrier of (A)
((A),j,G) is set
the of (A) . (j,G) is set
[j,G] is non empty V15() set
{j,G} is non empty set
{{j,G},{j}} is non empty set
the of (A) . [j,G] is set
id G is Relation-like G -defined G -valued Function-like one-to-one V14(G) set
{(id G)} is functional non empty trivial 1 -element set
((id G),(id G)) :-> (id G) is Relation-like [:{(id G)},{(id G)}:] -defined {(id G)} -valued Function-like non empty V14([:{(id G)},{(id G)}:]) quasi_total Function-yielding V25() Element of bool [:[:{(id G)},{(id G)}:],{(id G)}:]
[:{(id G)},{(id G)}:] is Relation-like non empty set
[:[:{(id G)},{(id G)}:],{(id G)}:] is Relation-like non empty set
bool [:[:{(id G)},{(id G)}:],{(id G)}:] is non empty set
[(id G),(id G)] is non empty V15() set
{(id G),(id G)} is functional non empty set
{{(id G),(id G)},{(id G)}} is non empty set
{[(id G),(id G)]} is Relation-like Function-like constant non empty trivial 1 -element set
{[(id G),(id G)]} --> (id G) is Relation-like {[(id G),(id G)]} -defined {(id G)} -valued Function-like constant non empty V14({[(id G),(id G)]}) quasi_total Function-yielding V25() Element of bool [:{[(id G),(id G)]},{(id G)}:]
[:{[(id G),(id G)]},{(id G)}:] is Relation-like non empty set
bool [:{[(id G),(id G)]},{(id G)}:] is non empty set
(((id G),(id G)) :-> (id G)) . (l,(id j)) is set
(((id G),(id G)) :-> (id G)) . [l,(id j)] is Relation-like Function-like set
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
i is Element of the carrier of (A)
j is Element of the carrier of (A)
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
k is Element of the carrier of (A)
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)
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
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),i,k,l) is Relation-like [:( the of (A) . (k,l)),( the of (A) . (i,k)):] -defined the of (A) . (i,l) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (k,l)),( the of (A) . (i,k)):],( the of (A) . (i,l)):]
the of (A) . (i,k) is set
[i,k] is non empty V15() set
{i,k} is non empty set
{{i,k},{i}} is non empty set
the of (A) . [i,k] is set
[:( the of (A) . (k,l)),( the of (A) . (i,k)):] is Relation-like set
the of (A) . (i,l) is set
[i,l] is non empty V15() set
{i,l} is non empty set
{{i,l},{i}} is non empty set
the of (A) . [i,l] is set
[:[:( the of (A) . (k,l)),( the of (A) . (i,k)):],( the of (A) . (i,l)):] is Relation-like set
bool [:[:( the of (A) . (k,l)),( the of (A) . (i,k)):],( the of (A) . (i,l)):] is non empty set
( the carrier of (A), the of (A), the of (A),i,j,k) is Relation-like [:( the of (A) . (j,k)),( the of (A) . (i,j)):] -defined the of (A) . (i,k) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (j,k)),( the of (A) . (i,j)):],( the of (A) . (i,k)):]
[:( the of (A) . (j,k)),( the of (A) . (i,j)):] is Relation-like set
[:[:( the of (A) . (j,k)),( the of (A) . (i,j)):],( the of (A) . (i,k)):] is Relation-like set
bool [:[:( the of (A) . (j,k)),( the of (A) . (i,j)):],( the of (A) . (i,k)):] is non empty set
( the carrier of (A), the of (A), the of (A),i,j,l) is Relation-like [:( the of (A) . (j,l)),( the of (A) . (i,j)):] -defined the of (A) . (i,l) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (j,l)),( the of (A) . (i,j)):],( the of (A) . (i,l)):]
the of (A) . (j,l) is set
[j,l] is non empty V15() set
{j,l} is non empty set
{{j,l},{j}} is non empty set
the of (A) . [j,l] is set
[:( the of (A) . (j,l)),( the of (A) . (i,j)):] is Relation-like set
[:[:( the of (A) . (j,l)),( the of (A) . (i,j)):],( the of (A) . (i,l)):] is Relation-like set
bool [:[:( the of (A) . (j,l)),( the of (A) . (i,j)):],( the of (A) . (i,l)):] is non empty set
( the carrier of (A), the of (A), the of (A),j,k,l) is Relation-like [:( the of (A) . (k,l)),( the of (A) . (j,k)):] -defined the of (A) . (j,l) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (k,l)),( the of (A) . (j,k)):],( the of (A) . (j,l)):]
[:( the of (A) . (k,l)),( the of (A) . (j,k)):] is Relation-like set
[:[:( the of (A) . (k,l)),( the of (A) . (j,k)):],( the of (A) . (j,l)):] is Relation-like set
bool [:[:( the of (A) . (k,l)),( the of (A) . (j,k)):],( the of (A) . (j,l)):] is non empty set
f is set
g is set
h is set
( the carrier of (A), the of (A), the of (A),i,j,k) . (g,f) is set
[g,f] is non empty V15() set
{g,f} is non empty set
{g} is non empty trivial 1 -element set
{{g,f},{g}} is non empty set
( the carrier of (A), the of (A), the of (A),i,j,k) . [g,f] is set
( the carrier of (A), the of (A), the of (A),i,k,l) . (h,(( the carrier of (A), the of (A), the of (A),i,j,k) . (g,f))) is set
[h,(( the carrier of (A), the of (A), the of (A),i,j,k) . (g,f))] is non empty V15() set
{h,(( the carrier of (A), the of (A), the of (A),i,j,k) . (g,f))} is non empty set
{h} is non empty trivial 1 -element set
{{h,(( the carrier of (A), the of (A), the of (A),i,j,k) . (g,f))},{h}} is non empty set
( the carrier of (A), the of (A), the of (A),i,k,l) . [h,(( the carrier of (A), the of (A), the of (A),i,j,k) . (g,f))] is set
( the carrier of (A), the of (A), the of (A),j,k,l) . (h,g) is set
[h,g] is non empty V15() set
{h,g} is non empty set
{{h,g},{h}} is non empty set
( the carrier of (A), the of (A), the of (A),j,k,l) . [h,g] is set
( the carrier of (A), the of (A), the of (A),i,j,l) . ((( the carrier of (A), the of (A), the of (A),j,k,l) . (h,g)),f) is set
[(( the carrier of (A), the of (A), the of (A),j,k,l) . (h,g)),f] is non empty V15() set
{(( the carrier of (A), the of (A), the of (A),j,k,l) . (h,g)),f} is non empty set
{(( the carrier of (A), the of (A), the of (A),j,k,l) . (h,g))} is non empty trivial 1 -element set
{{(( the carrier of (A), the of (A), the of (A),j,k,l) . (h,g)),f},{(( the carrier of (A), the of (A), the of (A),j,k,l) . (h,g))}} is non empty set
( the carrier of (A), the of (A), the of (A),i,j,l) . [(( the carrier of (A), the of (A), the of (A),j,k,l) . (h,g)),f] is set
i9 is Element of the carrier of (A)
j9 is Element of the carrier of (A)
((A),i9,j9) is set
the of (A) . (i9,j9) is set
[i9,j9] is non empty V15() set
{i9,j9} is non empty set
{i9} is non empty trivial 1 -element set
{{i9,j9},{i9}} is non empty set
the of (A) . [i9,j9] is set
((A),i9,i9) is set
the of (A) . (i9,i9) is set
[i9,i9] is non empty V15() set
{i9,i9} is non empty set
{{i9,i9},{i9}} is non empty set
the of (A) . [i9,i9] is set
id i9 is Relation-like i9 -defined i9 -valued Function-like one-to-one V14(i9) set
{(id i9)} is functional non empty trivial 1 -element set
k9 is Element of the carrier of (A)
((A),j9,k9) is set
the of (A) . (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 (A) . [j9,k9] is set
( the carrier of (A), the of (A), the of (A),i9,i9,i9) is Relation-like [:( the of (A) . (i9,i9)),( the of (A) . (i9,i9)):] -defined the of (A) . (i9,i9) -valued Function-like quasi_total Element of bool [:[:( the of (A) . (i9,i9)),( the of (A) . (i9,i9)):],( the of (A) . (i9,i9)):]
[:( the of (A) . (i9,i9)),( the of (A) . (i9,i9)):] is Relation-like set
[:[:( the of (A) . (i9,i9)),( the of (A) . (i9,i9)):],( the of (A) . (i9,i9)):] is Relation-like set
bool [:[:( the of (A) . (i9,i9)),( the of (A) . (i9,i9)):],( the of (A) . (i9,i9)):] is non empty set
((id i9),(id i9)) :-> (id i9) is Relation-like [:{(id i9)},{(id i9)}:] -defined {(id i9)} -valued Function-like non empty V14([:{(id i9)},{(id i9)}:]) quasi_total Function-yielding V25() Element of bool [:[:{(id i9)},{(id i9)}:],{(id i9)}:]
[:{(id i9)},{(id i9)}:] is Relation-like non empty set
[:[:{(id i9)},{(id i9)}:],{(id i9)}:] is Relation-like non empty set
bool [:[:{(id i9)},{(id i9)}:],{(id i9)}:] is non empty set
[(id i9),(id i9)] is non empty V15() set
{(id i9),(id i9)} is functional non empty set
{{(id i9),(id i9)},{(id i9)}} is non empty set
{[(id i9),(id i9)]} is Relation-like Function-like constant non empty trivial 1 -element set
{[(id i9),(id i9)]} --> (id i9) is Relation-like {[(id i9),(id i9)]} -defined {(id i9)} -valued Function-like constant non empty V14({[(id i9),(id i9)]}) quasi_total Function-yielding V25() Element of bool [:{[(id i9),(id i9)]},{(id i9)}:]
[:{[(id i9),(id i9)]},{(id i9)}:] is Relation-like non empty set
bool [:{[(id i9),(id i9)]},{(id i9)}:] is non empty set
l9 is Element of the carrier of (A)
((A),k9,l9) is set
the of (A) . (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 (A) . [k9,l9] is set