:: ENS_1 semantic presentation

K170() is Element of bool K166()

K166() is set

bool K166() is non empty set

{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

1 is non empty set

{{},1} is non empty set

K111() is set

bool K111() is non empty set

bool K170() is non empty set

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

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

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

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

V is non empty set

{ (Funcs (b

union { (Funcs (b

V is non empty set

(V) is set

{ (Funcs (b

union { (Funcs (b

the Element of V is Element of V

id the Element of V is Relation-like the Element of V -defined the Element of V -valued Function-like one-to-one total quasi_total Element of bool [: the Element of V, the Element of V:]

[: the Element of V, the Element of V:] is Relation-like set

bool [: the Element of V, the Element of V:] is non empty set

Funcs ( the Element of V, the Element of V) is functional non empty set

A is set

b is non empty set

d is set

g9 is Element of V

f is Element of V

Funcs (g9,f) is functional set

V is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

C is set

b is set

A is Element of V

d is Element of V

Funcs (A,d) is functional set

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

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

A is Element of V

b is Element of V

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

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

Funcs (b,A) is functional set

V is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

C is Element of V

a is Element of V

Funcs (C,a) is functional set

b is set

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

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

V is non empty set

bool V is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

C is non empty Element of bool V

(C) is functional non empty set

{ (Funcs (b

union { (Funcs (b

a is set

A is Element of C

b is Element of C

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

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

V is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

V is non empty set

(V) is set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

the Element of V is Element of V

id the Element of V is Relation-like the Element of V -defined the Element of V -valued Function-like one-to-one total quasi_total Element of bool [: the Element of V, the Element of V:]

[: the Element of V, the Element of V:] is Relation-like set

bool [: the Element of V, the Element of V:] is non empty set

[:[:V,V:],(bool [: the Element of V, the Element of V:]):] is Relation-like non empty set

[ the Element of V, the Element of V] is V15() Element of [:V,V:]

{ the Element of V, the Element of V} is non empty set

{ the Element of V} is non empty set

{{ the Element of V, the Element of V},{ the Element of V}} is non empty set

[[ the Element of V, the Element of V],(id the Element of V)] is V15() Element of [:[:V,V:],(bool [: the Element of V, the Element of V:]):]

{[ the Element of V, the Element of V],(id the Element of V)} is non empty set

{[ the Element of V, the Element of V]} is Relation-like Function-like non empty set

{{[ the Element of V, the Element of V],(id the Element of V)},{[ the Element of V, the Element of V]}} is non empty set

A is V15() Element of [:[:V,V:],(bool [: the Element of V, the Element of V:]):]

b is V15() Element of [:[:V,V:],(bool [: the Element of V, the Element of V:]):]

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of (V)

a is Element of V

b is Element of V

[a,b] is V15() Element of [:V,V:]

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

A is Relation-like Function-like Element of (V)

[[a,b],A] is V15() Element of [:[:V,V:],(V):]

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

{[a,b],A} is non empty set

{[a,b]} is Relation-like Function-like non empty set

{{[a,b],A},{[a,b]}} is non empty set

[:a,b:] is Relation-like set

bool [:a,b:] is non empty set

V is non empty set

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

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

{ [[b

C is Element of V

a is Element of V

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

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

[C,a] is V15() Element of [:V,V:]

{C,a} is non empty set

{C} is non empty set

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

b is Relation-like C -defined a -valued Function-like quasi_total Element of bool [:C,a:]

[[C,a],b] is V15() Element of [:[:V,V:],(bool [:C,a:]):]

[:[:V,V:],(bool [:C,a:]):] is Relation-like non empty set

{[C,a],b} is non empty set

{[C,a]} is Relation-like Function-like non empty set

{{[C,a],b},{[C,a]}} is non empty set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

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

C is set

a is Element of V

b is Element of V

[a,b] is V15() Element of [:V,V:]

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

A is Relation-like Function-like Element of (V)

[[a,b],A] is V15() Element of [:[:V,V:],(V):]

{[a,b],A} is non empty set

{[a,b]} is Relation-like Function-like non empty set

{{[a,b],A},{[a,b]}} is non empty set

[:a,b:] is Relation-like set

bool [:a,b:] is non empty set

V is non empty set

bool V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is non empty Element of bool V

(C) is non empty set

(C) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

a is set

b is Element of C

A is Element of C

[b,A] is V15() Element of [:C,C:]

{b,A} is non empty set

{b} is non empty set

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

d is Relation-like Function-like Element of (C)

[[b,A],d] is V15() Element of [:[:C,C:],(C):]

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

{[b,A],d} is non empty set

{[b,A]} is Relation-like Function-like non empty set

{{[b,A],d},{[b,A]}} is non empty set

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

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

V is set

a is set

[V,a] is V15() set

{V,a} is non empty set

{V} is non empty set

{{V,a},{V}} is non empty set

A is set

[[V,a],A] is V15() set

{[V,a],A} is non empty set

{[V,a]} is Relation-like Function-like non empty set

{{[V,a],A},{[V,a]}} is non empty set

C is set

b is set

[C,b] is V15() set

{C,b} is non empty set

{C} is non empty set

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

d is set

[[C,b],d] is V15() set

{[C,b],d} is non empty set

{[C,b]} is Relation-like Function-like non empty set

{{[C,b],d},{[C,b]}} is non empty set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of (V)

C `2 is set

b is Element of V

A is Element of V

[b,A] is V15() Element of [:V,V:]

{b,A} is non empty set

{b} is non empty set

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

a is Relation-like Function-like Element of (V)

[[b,A],a] is V15() Element of [:[:V,V:],(V):]

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

{[b,A],a} is non empty set

{[b,A]} is Relation-like Function-like non empty set

{{[b,A],a},{[b,A]}} is non empty set

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

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

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of (V)

C `1 is set

(C `1) `1 is set

b is Element of V

A is Element of V

[b,A] is V15() Element of [:V,V:]

{b,A} is non empty set

{b} is non empty set

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

a is Relation-like Function-like Element of (V)

[[b,A],a] is V15() Element of [:[:V,V:],(V):]

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

{[b,A],a} is non empty set

{[b,A]} is Relation-like Function-like non empty set

{{[b,A],a},{[b,A]}} is non empty set

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

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

(C `1) `2 is set

b is Element of V

A is Element of V

[b,A] is V15() Element of [:V,V:]

{b,A} is non empty set

{b} is non empty set

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

a is Relation-like Function-like Element of (V)

[[b,A],a] is V15() Element of [:[:V,V:],(V):]

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

{[b,A],a} is non empty set

{[b,A]} is Relation-like Function-like non empty set

{{[b,A],a},{[b,A]}} is non empty set

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

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

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of (V)

(V,C) is Element of V

C `1 is set

(C `1) `1 is set

(V,C) is Element of V

(C `1) `2 is set

[(V,C),(V,C)] is V15() Element of [:V,V:]

{(V,C),(V,C)} is non empty set

{(V,C)} is non empty set

{{(V,C),(V,C)},{(V,C)}} is non empty set

C `2 is Relation-like Function-like set

[[(V,C),(V,C)],(C `2)] is V15() set

{[(V,C),(V,C)],(C `2)} is non empty set

{[(V,C),(V,C)]} is Relation-like Function-like non empty set

{{[(V,C),(V,C)],(C `2)},{[(V,C),(V,C)]}} is non empty set

b is Element of V

A is Element of V

[b,A] is V15() Element of [:V,V:]

{b,A} is non empty set

{b} is non empty set

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

a is Relation-like Function-like Element of (V)

[[b,A],a] is V15() Element of [:[:V,V:],(V):]

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

{[b,A],a} is non empty set

{[b,A]} is Relation-like Function-like non empty set

{{[b,A],a},{[b,A]}} is non empty set

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

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

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of (V)

C `2 is Relation-like Function-like set

(V,C) is Element of V

C `1 is set

(C `1) `1 is set

(V,C) is Element of V

(C `1) `2 is set

a is Element of (V)

a `2 is Relation-like Function-like set

(V,a) is Element of V

a `1 is set

(a `1) `1 is set

(V,a) is Element of V

(a `1) `2 is set

[(V,C),(V,C)] is V15() Element of [:V,V:]

{(V,C),(V,C)} is non empty set

{(V,C)} is non empty set

{{(V,C),(V,C)},{(V,C)}} is non empty set

[[(V,C),(V,C)],(C `2)] is V15() set

{[(V,C),(V,C)],(C `2)} is non empty set

{[(V,C),(V,C)]} is Relation-like Function-like non empty set

{{[(V,C),(V,C)],(C `2)},{[(V,C),(V,C)]}} is non empty set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of (V)

(V,C) is Element of V

C `1 is set

(C `1) `2 is set

(V,C) is Element of V

(C `1) `1 is set

C `2 is Relation-like Function-like set

[:(V,C),(V,C):] is Relation-like set

bool [:(V,C),(V,C):] is non empty set

b is Element of V

A is Element of V

[b,A] is V15() Element of [:V,V:]

{b,A} is non empty set

{b} is non empty set

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

a is Relation-like Function-like Element of (V)

[[b,A],a] is V15() Element of [:[:V,V:],(V):]

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

{[b,A],a} is non empty set

{[b,A]} is Relation-like Function-like non empty set

{{[b,A],a},{[b,A]}} is non empty set

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

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

[(V,C),(V,C)] is V15() Element of [:V,V:]

{(V,C),(V,C)} is non empty set

{(V,C)} is non empty set

{{(V,C),(V,C)},{(V,C)}} is non empty set

[[(V,C),(V,C)],(C `2)] is V15() set

{[(V,C),(V,C)],(C `2)} is non empty set

{[(V,C),(V,C)]} is Relation-like Function-like non empty set

{{[(V,C),(V,C)],(C `2)},{[(V,C),(V,C)]}} is non empty set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of (V)

C `2 is Relation-like Function-like set

proj1 (C `2) is set

(V,C) is Element of V

C `1 is set

(C `1) `1 is set

proj2 (C `2) is set

(V,C) is Element of V

(C `1) `2 is set

[:(V,C),(V,C):] is Relation-like set

bool [:(V,C),(V,C):] is non empty set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Relation-like Function-like set

a is set

b is set

[a,b] is V15() set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

[[a,b],C] is V15() set

{[a,b],C} is non empty set

{[a,b]} is Relation-like Function-like non empty set

{{[a,b],C},{[a,b]}} is non empty set

[:a,b:] is Relation-like set

bool [:a,b:] is non empty set

d is Element of V

g9 is Element of V

[d,g9] is V15() Element of [:V,V:]

{d,g9} is non empty set

{d} is non empty set

{{d,g9},{d}} is non empty set

A is Relation-like Function-like Element of (V)

[[d,g9],A] is V15() Element of [:[:V,V:],(V):]

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

{[d,g9],A} is non empty set

{[d,g9]} is Relation-like Function-like non empty set

{{[d,g9],A},{[d,g9]}} is non empty set

[:d,g9:] is Relation-like set

bool [:d,g9:] is non empty set

V is non empty set

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

C is Element of V

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

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

[C,C] is V15() Element of [:V,V:]

{C,C} is non empty set

{C} is non empty set

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

id C is Relation-like C -defined C -valued Function-like one-to-one total quasi_total Element of bool [:C,C:]

[[C,C],(id C)] is V15() Element of [:[:V,V:],(bool [:C,C:]):]

[:[:V,V:],(bool [:C,C:]):] is Relation-like non empty set

{[C,C],(id C)} is non empty set

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

{{[C,C],(id C)},{[C,C]}} is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

{ [[b

V is non empty set

C is Element of V

(V,C) is Element of (V)

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

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

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

[C,C] is V15() Element of [:V,V:]

{C,C} is non empty set

{C} is non empty set

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

id C is Relation-like C -defined C -valued Function-like one-to-one total quasi_total Element of bool [:C,C:]

[[C,C],(id C)] is V15() Element of [:[:V,V:],(bool [:C,C:]):]

[:[:V,V:],(bool [:C,C:]):] is Relation-like non empty set

{[C,C],(id C)} is non empty set

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

{{[C,C],(id C)},{[C,C]}} is non empty set

(V,C) `2 is Relation-like Function-like set

(V,(V,C)) is Element of V

(V,C) `1 is set

((V,C) `1) `1 is set

(V,(V,C)) is Element of V

((V,C) `1) `2 is set

[(V,(V,C)),(V,(V,C))] is V15() Element of [:V,V:]

{(V,(V,C)),(V,(V,C))} is non empty set

{(V,(V,C))} is non empty set

{{(V,(V,C)),(V,(V,C))},{(V,(V,C))}} is non empty set

[[(V,(V,C)),(V,(V,C))],((V,C) `2)] is V15() set

{[(V,(V,C)),(V,(V,C))],((V,C) `2)} is non empty set

{[(V,(V,C)),(V,(V,C))]} is Relation-like Function-like non empty set

{{[(V,(V,C)),(V,(V,C))],((V,C) `2)},{[(V,(V,C)),(V,(V,C))]}} is non empty set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of (V)

(V,C) is Element of V

C `1 is set

(C `1) `2 is set

a is Element of (V)

(V,a) is Element of V

a `1 is set

(a `1) `1 is set

(V,C) is Element of V

(C `1) `1 is set

(V,a) is Element of V

(a `1) `2 is set

[(V,C),(V,a)] is V15() Element of [:V,V:]

{(V,C),(V,a)} is non empty set

{(V,C)} is non empty set

{{(V,C),(V,a)},{(V,C)}} is non empty set

C `2 is Relation-like Function-like set

a `2 is Relation-like Function-like set

(C `2) * (a `2) is Relation-like Function-like set

[[(V,C),(V,a)],((C `2) * (a `2))] is V15() set

{[(V,C),(V,a)],((C `2) * (a `2))} is non empty set

{[(V,C),(V,a)]} is Relation-like Function-like non empty set

{{[(V,C),(V,a)],((C `2) * (a `2))},{[(V,C),(V,a)]}} is non empty set

[:(V,C),(V,C):] is Relation-like set

bool [:(V,C),(V,C):] is non empty set

[:(V,a),(V,a):] is Relation-like set

bool [:(V,a),(V,a):] is non empty set

[:(V,C),(V,a):] is Relation-like set

bool [:(V,C),(V,a):] is non empty set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of (V)

(V,C) is Element of V

C `1 is set

(C `1) `1 is set

C `2 is Relation-like Function-like set

(V,C) is Element of V

(C `1) `2 is set

a is Element of (V)

(V,a) is Element of V

a `1 is set

(a `1) `2 is set

(V,a,C) is Element of (V)

(V,a,C) `2 is Relation-like Function-like set

a `2 is Relation-like Function-like set

(a `2) * (C `2) is Relation-like Function-like set

(V,(V,a,C)) is Element of V

(V,a,C) `1 is set

((V,a,C) `1) `1 is set

(V,a) is Element of V

(a `1) `1 is set

(V,(V,a,C)) is Element of V

((V,a,C) `1) `2 is set

[(V,a),(V,C)] is V15() Element of [:V,V:]

{(V,a),(V,C)} is non empty set

{(V,a)} is non empty set

{{(V,a),(V,C)},{(V,a)}} is non empty set

[[(V,a),(V,C)],((a `2) * (C `2))] is V15() set

{[(V,a),(V,C)],((a `2) * (C `2))} is non empty set

{[(V,a),(V,C)]} is Relation-like Function-like non empty set

{{[(V,a),(V,C)],((a `2) * (C `2))},{[(V,a),(V,C)]}} is non empty set

[(V,(V,a,C)),(V,(V,a,C))] is V15() Element of [:V,V:]

{(V,(V,a,C)),(V,(V,a,C))} is non empty set

{(V,(V,a,C))} is non empty set

{{(V,(V,a,C)),(V,(V,a,C))},{(V,(V,a,C))}} is non empty set

[[(V,(V,a,C)),(V,(V,a,C))],((V,a,C) `2)] is V15() set

{[(V,(V,a,C)),(V,(V,a,C))],((V,a,C) `2)} is non empty set

{[(V,(V,a,C)),(V,(V,a,C))]} is Relation-like Function-like non empty set

{{[(V,(V,a,C)),(V,(V,a,C))],((V,a,C) `2)},{[(V,(V,a,C)),(V,(V,a,C))]}} is non empty set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of (V)

(V,C) is Element of V

C `1 is set

(C `1) `1 is set

(V,C) is Element of V

(C `1) `2 is set

a is Element of (V)

(V,a) is Element of V

a `1 is set

(a `1) `2 is set

(V,a,C) is Element of (V)

b is Element of (V)

(V,b) is Element of V

b `1 is set

(b `1) `1 is set

(V,(V,a,C),b) is Element of (V)

(V,C,b) is Element of (V)

(V,a,(V,C,b)) is Element of (V)

(V,(V,a,C)) is Element of V

(V,a,C) `1 is set

((V,a,C) `1) `2 is set

(V,a,C) `2 is Relation-like Function-like set

a `2 is Relation-like Function-like set

C `2 is Relation-like Function-like set

(a `2) * (C `2) is Relation-like Function-like set

(V,(V,a,C),b) `2 is Relation-like Function-like set

b `2 is Relation-like Function-like set

((a `2) * (C `2)) * (b `2) is Relation-like Function-like set

(V,(V,C,b)) is Element of V

(V,C,b) `1 is set

((V,C,b) `1) `1 is set

(V,(V,a,(V,C,b))) is Element of V

(V,a,(V,C,b)) `1 is set

((V,a,(V,C,b)) `1) `1 is set

(V,a) is Element of V

(a `1) `1 is set

(V,(V,a,C)) is Element of V

((V,a,C) `1) `1 is set

(V,(V,(V,a,C),b)) is Element of V

(V,(V,a,C),b) `1 is set

((V,(V,a,C),b) `1) `1 is set

(V,(V,C,b)) is Element of V

((V,C,b) `1) `2 is set

(V,b) is Element of V

(b `1) `2 is set

(V,(V,a,(V,C,b))) is Element of V

((V,a,(V,C,b)) `1) `2 is set

(V,C,b) `2 is Relation-like Function-like set

(C `2) * (b `2) is Relation-like Function-like set

(V,a,(V,C,b)) `2 is Relation-like Function-like set

(a `2) * ((C `2) * (b `2)) is Relation-like Function-like set

(V,(V,(V,a,C),b)) is Element of V

((V,(V,a,C),b) `1) `2 is set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of (V)

(V,C) is Element of V

C `1 is set

(C `1) `1 is set

(V,(V,C)) is Element of (V)

[:(V,C),(V,C):] is Relation-like set

bool [:(V,C),(V,C):] is non empty set

[(V,C),(V,C)] is V15() Element of [:V,V:]

{(V,C),(V,C)} is non empty set

{(V,C)} is non empty set

{{(V,C),(V,C)},{(V,C)}} is non empty set

id (V,C) is Relation-like (V,C) -defined (V,C) -valued Function-like one-to-one total quasi_total Element of bool [:(V,C),(V,C):]

[[(V,C),(V,C)],(id (V,C))] is V15() Element of [:[:V,V:],(bool [:(V,C),(V,C):]):]

[:[:V,V:],(bool [:(V,C),(V,C):]):] is Relation-like non empty set

{[(V,C),(V,C)],(id (V,C))} is non empty set

{[(V,C),(V,C)]} is Relation-like Function-like non empty set

{{[(V,C),(V,C)],(id (V,C))},{[(V,C),(V,C)]}} is non empty set

(V,(V,(V,C)),C) is Element of (V)

(V,C) is Element of V

(C `1) `2 is set

(V,(V,C)) is Element of (V)

[:(V,C),(V,C):] is Relation-like set

bool [:(V,C),(V,C):] is non empty set

[(V,C),(V,C)] is V15() Element of [:V,V:]

{(V,C),(V,C)} is non empty set

{(V,C)} is non empty set

{{(V,C),(V,C)},{(V,C)}} is non empty set

id (V,C) is Relation-like (V,C) -defined (V,C) -valued Function-like one-to-one total quasi_total Element of bool [:(V,C),(V,C):]

[[(V,C),(V,C)],(id (V,C))] is V15() Element of [:[:V,V:],(bool [:(V,C),(V,C):]):]

[:[:V,V:],(bool [:(V,C),(V,C):]):] is Relation-like non empty set

{[(V,C),(V,C)],(id (V,C))} is non empty set

{[(V,C),(V,C)]} is Relation-like Function-like non empty set

{{[(V,C),(V,C)],(id (V,C))},{[(V,C),(V,C)]}} is non empty set

(V,C,(V,(V,C))) is Element of (V)

(V,(V,C)) `2 is Relation-like Function-like set

(V,(V,(V,C))) is Element of V

(V,(V,C)) `1 is set

((V,(V,C)) `1) `1 is set

C `2 is Relation-like Function-like set

[:(V,C),(V,C):] is Relation-like set

bool [:(V,C),(V,C):] is non empty set

proj2 (C `2) is set

proj1 (C `2) is set

(V,(V,(V,C))) is Element of V

((V,(V,C)) `1) `2 is set

(V,(V,(V,(V,C)),C)) is Element of V

(V,(V,(V,C)),C) `1 is set

((V,(V,(V,C)),C) `1) `2 is set

(V,(V,(V,C)),C) `2 is Relation-like Function-like set

((V,(V,C)) `2) * (C `2) is Relation-like Function-like set

(V,(V,(V,(V,C)),C)) is Element of V

((V,(V,(V,C)),C) `1) `1 is set

(V,(V,C)) `2 is Relation-like Function-like set

(V,(V,(V,C))) is Element of V

(V,(V,C)) `1 is set

((V,(V,C)) `1) `2 is set

(V,(V,(V,C))) is Element of V

((V,(V,C)) `1) `1 is set

(V,(V,C,(V,(V,C)))) is Element of V

(V,C,(V,(V,C))) `1 is set

((V,C,(V,(V,C))) `1) `2 is set

(V,C,(V,(V,C))) `2 is Relation-like Function-like set

(C `2) * ((V,(V,C)) `2) is Relation-like Function-like set

(V,(V,C,(V,(V,C)))) is Element of V

((V,C,(V,(V,C))) `1) `1 is set

V is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

C is Element of V

a is Element of V

[C,a] is V15() Element of [:V,V:]

{C,a} is non empty set

{C} is non empty set

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

(V) is non empty set

{ [[b

{ [[C,a],b

V is non empty set

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

C is Element of V

a is Element of V

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

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

[C,a] is V15() Element of [:V,V:]

{C,a} is non empty set

{C} is non empty set

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

(V,C,a) is set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

(V) is non empty set

{ [[b

{ [[C,a],b

b is Relation-like C -defined a -valued Function-like quasi_total Element of bool [:C,a:]

[[C,a],b] is V15() Element of [:[:V,V:],(bool [:C,a:]):]

[:[:V,V:],(bool [:C,a:]):] is Relation-like non empty set

{[C,a],b} is non empty set

{[C,a]} is Relation-like Function-like non empty set

{{[C,a],b},{[C,a]}} is non empty set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of V

a is Element of V

(V,C,a) is set

[C,a] is V15() Element of [:V,V:]

{C,a} is non empty set

{C} is non empty set

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

{ [[C,a],b

b is Element of (V)

b `2 is Relation-like Function-like set

[[C,a],(b `2)] is V15() set

{[C,a],(b `2)} is non empty set

{[C,a]} is Relation-like Function-like non empty set

{{[C,a],(b `2)},{[C,a]}} is non empty set

(V,b) is Element of V

b `1 is set

(b `1) `1 is set

(V,b) is Element of V

(b `1) `2 is set

[(V,b),(V,b)] is V15() Element of [:V,V:]

{(V,b),(V,b)} is non empty set

{(V,b)} is non empty set

{{(V,b),(V,b)},{(V,b)}} is non empty set

[[(V,b),(V,b)],(b `2)] is V15() set

{[(V,b),(V,b)],(b `2)} is non empty set

{[(V,b),(V,b)]} is Relation-like Function-like non empty set

{{[(V,b),(V,b)],(b `2)},{[(V,b),(V,b)]}} is non empty set

A is Relation-like Function-like Element of (V)

[[C,a],A] is V15() Element of [:[:V,V:],(V):]

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

{[C,a],A} is non empty set

{{[C,a],A},{[C,a]}} is non empty set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of V

a is Element of V

(V,C,a) is set

[C,a] is V15() Element of [:V,V:]

{C,a} is non empty set

{C} is non empty set

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

{ [[C,a],b

b is set

A is Relation-like Function-like Element of (V)

[[C,a],A] is V15() Element of [:[:V,V:],(V):]

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

{[C,a],A} is non empty set

{[C,a]} is Relation-like Function-like non empty set

{{[C,a],A},{[C,a]}} is non empty set

V is non empty set

C is Element of V

a is Element of V

[C,a] is V15() Element of [:V,V:]

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

{C,a} is non empty set

{C} is non empty set

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

(V,C,a) is set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

(V) is non empty set

{ [[b

{ [[C,a],b

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

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

b is Relation-like Function-like set

[[C,a],b] is V15() set

{[C,a],b} is non empty set

{[C,a]} is Relation-like Function-like non empty set

{{[C,a],b},{[C,a]}} is non empty set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

{ (V,b

union { (V,b

a is set

A is Element of V

d is Element of V

[A,d] is V15() Element of [:V,V:]

{A,d} is non empty set

{A} is non empty set

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

b is Relation-like Function-like Element of (V)

[[A,d],b] is V15() Element of [:[:V,V:],(V):]

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

{[A,d],b} is non empty set

{[A,d]} is Relation-like Function-like non empty set

{{[A,d],b},{[A,d]}} is non empty set

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

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

(V,A,d) is set

{ [[A,d],b

b is set

A is Element of V

d is Element of V

(V,A,d) is set

[A,d] is V15() Element of [:V,V:]

{A,d} is non empty set

{A} is non empty set

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

{ [[A,d],b

g9 is Relation-like Function-like Element of (V)

[[A,d],g9] is V15() Element of [:[:V,V:],(V):]

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

{[A,d],g9} is non empty set

{[A,d]} is Relation-like Function-like non empty set

{{[A,d],g9},{[A,d]}} is non empty set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of V

a is Element of V

(V,C,a) is set

[C,a] is V15() Element of [:V,V:]

{C,a} is non empty set

{C} is non empty set

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

{ [[C,a],b

b is Element of (V)

(V,b) is Element of V

b `1 is set

(b `1) `1 is set

(V,b) is Element of V

(b `1) `2 is set

b `2 is Relation-like Function-like set

[:(V,b),(V,b):] is Relation-like set

bool [:(V,b),(V,b):] is non empty set

[[C,a],(b `2)] is V15() set

{[C,a],(b `2)} is non empty set

{[C,a]} is Relation-like Function-like non empty set

{{[C,a],(b `2)},{[C,a]}} is non empty set

[(V,b),(V,b)] is V15() Element of [:V,V:]

{(V,b),(V,b)} is non empty set

{(V,b)} is non empty set

{{(V,b),(V,b)},{(V,b)}} is non empty set

[[(V,b),(V,b)],(b `2)] is V15() set

{[(V,b),(V,b)],(b `2)} is non empty set

{[(V,b),(V,b)]} is Relation-like Function-like non empty set

{{[(V,b),(V,b)],(b `2)},{[(V,b),(V,b)]}} is non empty set

[(V,b),(V,b)] is V15() Element of [:V,V:]

{(V,b),(V,b)} is non empty set

{(V,b)} is non empty set

{{(V,b),(V,b)},{(V,b)}} is non empty set

[[(V,b),(V,b)],(b `2)] is V15() set

{[(V,b),(V,b)],(b `2)} is non empty set

{[(V,b),(V,b)]} is Relation-like Function-like non empty set

{{[(V,b),(V,b)],(b `2)},{[(V,b),(V,b)]}} is non empty set

(V,(V,b),(V,b)) is set

{ [[(V,b),(V,b)],b

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

C is Element of V

a is Element of V

(V,C,a) is set

[C,a] is V15() Element of [:V,V:]

{C,a} is non empty set

{C} is non empty set

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

{ [[C,a],b

Funcs (C,a) is functional set

b is Element of (V)

b `2 is Relation-like Function-like set

[[C,a],(b `2)] is V15() set

{[C,a],(b `2)} is non empty set

{[C,a]} is Relation-like Function-like non empty set

{{[C,a],(b `2)},{[C,a]}} is non empty set

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

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

V is non empty set

bool V is non empty set

C is non empty Element of bool V

a is Element of C

b is Element of C

(C,a,b) is set

(C) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

[a,b] is V15() Element of [:C,C:]

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

(C) is non empty set

{ [[b

{ [[a,b],b

A is Element of V

d is Element of V

(V,A,d) is set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

[A,d] is V15() Element of [:V,V:]

{A,d} is non empty set

{A} is non empty set

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

(V) is non empty set

{ [[b

{ [[A,d],b

g9 is set

f is Element of (C)

(C,f) is Element of C

f `1 is set

(f `1) `1 is set

(C,f) is Element of C

(f `1) `2 is set

[(C,f),(C,f)] is V15() Element of [:C,C:]

{(C,f),(C,f)} is non empty set

{(C,f)} is non empty set

{{(C,f),(C,f)},{(C,f)}} is non empty set

f `2 is Relation-like Function-like set

[[(C,f),(C,f)],(f `2)] is V15() set

{[(C,f),(C,f)],(f `2)} is non empty set

{[(C,f),(C,f)]} is Relation-like Function-like non empty set

{{[(C,f),(C,f)],(f `2)},{[(C,f),(C,f)]}} is non empty set

f9 is Element of (V)

(V,f9) is Element of V

f9 `1 is set

(f9 `1) `1 is set

(V,f9) is Element of V

(f9 `1) `2 is set

[[a,b],(f `2)] is V15() set

{[a,b],(f `2)} is non empty set

{[a,b]} is Relation-like Function-like non empty set

{{[a,b],(f `2)},{[a,b]}} is non empty set

f is Element of (V)

f `2 is Relation-like Function-like set

[[A,d],(f `2)] is V15() set

{[A,d],(f `2)} is non empty set

{[A,d]} is Relation-like Function-like non empty set

{{[A,d],(f `2)},{[A,d]}} is non empty set

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

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

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

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

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

C is Relation-like (V) -defined V -valued Function-like non empty total quasi_total Element of bool [:(V),V:]

C is Relation-like (V) -defined V -valued Function-like non empty total quasi_total Element of bool [:(V),V:]

a is Relation-like (V) -defined V -valued Function-like non empty total quasi_total Element of bool [:(V),V:]

b is Element of (V)

C . b is Element of V

(V,b) is Element of V

b `1 is set

(b `1) `1 is set

a . b is Element of V

C is Relation-like (V) -defined V -valued Function-like non empty total quasi_total Element of bool [:(V),V:]

C is Relation-like (V) -defined V -valued Function-like non empty total quasi_total Element of bool [:(V),V:]

a is Relation-like (V) -defined V -valued Function-like non empty total quasi_total Element of bool [:(V),V:]

b is Element of (V)

C . b is Element of V

(V,b) is Element of V

b `1 is set

(b `1) `2 is set

a . b is Element of V

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

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

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

C is set

a is set

b is set

A is set

g9 is Element of (V)

d is Element of (V)

(V,g9,d) is Element of (V)

C is set

a is set

b is set

d is Element of (V)

A is Element of (V)

(V,d,A) is Element of (V)

C is Relation-like [:(V),(V):] -defined (V) -valued Function-like Element of bool [:[:(V),(V):],(V):]

proj1 C is Relation-like set

a is Element of (V)

(V,a) is Element of V

a `1 is set

(a `1) `1 is set

b is Element of (V)

[a,b] is V15() Element of [:(V),(V):]

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

(V,b) is Element of V

b `1 is set

(b `1) `2 is set

A is set

(V,b,a) is Element of (V)

A is Element of (V)

d is Element of (V)

(V,A) is Element of V

A `1 is set

(A `1) `1 is set

(V,d) is Element of V

d `1 is set

(d `1) `2 is set

(V,d,A) is Element of (V)

a is Element of (V)

(V,a) is Element of V

a `1 is set

(a `1) `1 is set

b is Element of (V)

(V,b) is Element of V

b `1 is set

(b `1) `2 is set

[a,b] is V15() Element of [:(V),(V):]

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

C . [a,b] is set

(V,b,a) is Element of (V)

C . (a,b) is set

[a,b] is V15() set

C . [a,b] is set

A is Element of (V)

d is Element of (V)

(V,A) is Element of V

A `1 is set

(A `1) `1 is set

(V,d) is Element of V

d `1 is set

(d `1) `2 is set

(V,d,A) is Element of (V)

C is Relation-like [:(V),(V):] -defined (V) -valued Function-like Element of bool [:[:(V),(V):],(V):]

proj1 C is Relation-like set

a is Relation-like [:(V),(V):] -defined (V) -valued Function-like Element of bool [:[:(V),(V):],(V):]

proj1 a is Relation-like set

b is set

A is set

[b,A] is V15() set

{b,A} is non empty set

{b} is non empty set

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

d is Element of (V)

(V,d) is Element of V

d `1 is set

(d `1) `1 is set

g9 is Element of (V)

(V,g9) is Element of V

g9 `1 is set

(g9 `1) `2 is set

d is Element of (V)

(V,d) is Element of V

d `1 is set

(d `1) `1 is set

g9 is Element of (V)

(V,g9) is Element of V

g9 `1 is set

(g9 `1) `2 is set

b is Element of [:(V),(V):]

A is Element of (V)

d is Element of (V)

[A,d] is V15() Element of [:(V),(V):]

{A,d} is non empty set

{A} is non empty set

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

(V,A) is Element of V

A `1 is set

(A `1) `1 is set

(V,d) is Element of V

d `1 is set

(d `1) `2 is set

C . [A,d] is set

(V,d,A) is Element of (V)

C . b is set

a . b is set

V is non empty set

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

(V) is Relation-like (V) -defined V -valued Function-like non empty total quasi_total Element of bool [:(V),V:]

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

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

(V) is Relation-like (V) -defined V -valued Function-like non empty total quasi_total Element of bool [:(V),V:]

(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like Element of bool [:[:(V),(V):],(V):]

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

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

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

CatStr(# V,(V),(V),(V),(V) #) is non empty non void V59() strict CatStr

V is non empty set

(V) is non empty non void V59() strict CatStr

(V) is non empty set

(V) is functional non empty set

{ (Funcs (b

union { (Funcs (b

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

{ [[b

(V) is Relation-like (V) -defined V -valued Function-like non empty total quasi_total Element of bool [:(V),V:]

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

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

(V) is Relation-like (V) -defined V -valued Function-like non empty total quasi_total Element of bool [:(V),V:]

(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like Element of bool [:[:(V),(V):],(V):]

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

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

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

CatStr(# V,(V),(V),(V),(V) #) is non empty non void V59() strict CatStr

d is non empty non void V59() CatStr

the carrier' of d is non empty set

f is Element of the carrier' of d

g9 is Element of the carrier' of d

[f,g9] is V15() set

{f,g9} is non empty set

{f} is non empty set

{{f,g9},{f}} is non empty set

the Comp of d is Relation-like [: the carrier' of d, the carrier' of d:] -defined the carrier' of d -valued Function-like Element of bool [:[: the carrier' of d, the carrier' of d:], the carrier' of d:]

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

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

bool [:[: the carrier' of d, the carrier' of d:], the carrier' of d:] is non empty set

proj1 the Comp of d is Relation-like set

dom f is Element of the carrier of d

the carrier of d is non empty set

the Source of d is Relation-like the carrier' of d -defined the carrier of d -valued Function-like non empty total quasi_total Element of bool [: the carrier' of d, the carrier of d:]

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

bool [: the carrier' of d, the carrier of d:] is non empty set

the Source of d . f is Element of the carrier of d

cod g9 is Element of the carrier of d

the Target of d is Relation-like the carrier' of d -defined the carrier of d -valued Function-like non empty total quasi_total Element of bool [: the carrier' of d, the carrier of d:]

the Target of d . g9 is Element of the carrier of d

k is Element of (V)

(V) . k is Element of V

(V,k) is Element of V

k `1 is set

(k `1) `1 is set

f9 is Element of (V)

(V) . f9 is Element of V

(V,f9) is Element of V

f9 `1 is set

(f9 `1) `2 is set

the carrier' of d is non empty set

f is Element of the carrier' of d

dom f is Element of the carrier of d

the carrier of d is non empty set

the Source of d is Relation-like the carrier' of d -defined the carrier of d -valued Function-like non empty total quasi_total Element of bool [: the carrier' of d, the carrier of d:]

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

bool [: the carrier' of d, the carrier of d:] is non empty set

the Source of d . f is Element of the carrier of d

g9 is Element of the carrier' of d

cod g9 is Element of the carrier of d

the Target of d is Relation-like the carrier' of d -defined the carrier of d -valued Function-like non empty total quasi_total Element of bool [: the carrier' of d, the carrier of d:]

the Target of d . g9 is Element of the carrier of d

f (*) g9 is Element of the carrier' of d

dom (f (*) g9) is Element of the carrier of d

the Source of d . (f (*) g9) is Element of the carrier of d

dom g9 is Element of the carrier of d

the Source of d . g9 is Element of the carrier of d

cod (f (*) g9) is Element of the carrier of d

the Target of d . (f (*) g9) is Element of the carrier of d

cod f is Element of the carrier of d

the Target of d . f is Element of the carrier of d

[f,g9] is V15()