:: 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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
V is non empty set
(V) is set
{ (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
C is non empty Element of bool V
(C) is functional non empty set
{ (Funcs (b₁,b₂)) where b₁, b₂ is Element of C : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of C : verum } is set
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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of V, b₃ is Relation-like Function-like Element of (V) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
V is non empty set
(V) is set
(V) is functional non empty set
{ (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of V, b₃ is Relation-like Function-like Element of (V) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of V, b₃ is Relation-like Function-like Element of (V) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of V, b₃ is Relation-like Function-like Element of (V) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is 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
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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of V, b₃ is Relation-like Function-like Element of (V) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
[:[: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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of V, b₃ is Relation-like Function-like Element of (V) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
C is non empty Element of bool V
(C) is non empty set
(C) is functional non empty set
{ (Funcs (b₁,b₂)) where b₁, b₂ is Element of C : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of C : verum } is set
[:C,C:] is Relation-like non empty set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of C, b₃ is Relation-like Function-like Element of (C) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of V, b₃ is Relation-like Function-like Element of (V) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of V, b₃ is Relation-like Function-like Element of (V) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of V, b₃ is Relation-like Function-like Element of (V) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
[: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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of V, b₃ is Relation-like Function-like Element of (V) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
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₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of V, b₃ is Relation-like Function-like Element of (V) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[: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<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
{ [[C,a],b<sub>1</sub>] where b<sub>1</sub> is Relation-like Function-like Element of (V) : [[C,a],b<sub>1</sub>] in (V) } is set
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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
(V) is non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
{ [[C,a],b<sub>1</sub>] where b<sub>1</sub> is Relation-like Function-like Element of (V) : [[C,a],b<sub>1</sub>] in (V) } is 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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
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<sub>1</sub>] where b<sub>1</sub> is Relation-like Function-like Element of (V) : [[C,a],b<sub>1</sub>] in (V) } is 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
(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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
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<sub>1</sub>] where b<sub>1</sub> is Relation-like Function-like Element of (V) : [[C,a],b<sub>1</sub>] in (V) } is set
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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
(V) is non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
{ [[C,a],b<sub>1</sub>] where b<sub>1</sub> is Relation-like Function-like Element of (V) : [[C,a],b<sub>1</sub>] in (V) } is set
[: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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
{ (V,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (V,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
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<sub>1</sub>] where b<sub>1</sub> is Relation-like Function-like Element of (V) : [[A,d],b<sub>1</sub>] in (V) } is set
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<sub>1</sub>] where b<sub>1</sub> is Relation-like Function-like Element of (V) : [[A,d],b<sub>1</sub>] in (V) } is set
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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
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<sub>1</sub>] where b<sub>1</sub> is Relation-like Function-like Element of (V) : [[C,a],b<sub>1</sub>] in (V) } is set
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₁] where b₁ is Relation-like Function-like Element of (V) : [[(V,b),(V,b)],b₁] in (V) } is set
V is non empty set
(V) is non empty set
(V) is functional non empty set
{ (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of V, b₃ is Relation-like Function-like Element of (V) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
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₁] where b₁ is Relation-like Function-like Element of (V) : [[C,a],b₁] in (V) } is set
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₁,b₂)) where b₁, b₂ is Element of C : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of C : verum } is set
[: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₁,b₂],b₃] where b₁, b₂ is Element of C, b₃ is Relation-like Function-like Element of (C) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
{ [[a,b],b₁] where b₁ is Relation-like Function-like Element of (C) : [[a,b],b₁] in (C) } is set
A is Element of V
d is Element of V
(V,A,d) is set
(V) is functional non empty set
{ (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
union { (Funcs (b₁,b₂)) where b₁, b₂ is Element of V : verum } is set
[: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₁,b₂],b₃] where b₁, b₂ is Element of V, b₃ is Relation-like Function-like Element of (V) : ( ( not b₂ = {} or b₁ = {} ) & b₃ is Relation-like b₁ -defined b₂ -valued Function-like quasi_total Element of bool [:b₁,b₂:] ) } is set
{ [[A,d],b₁] where b₁ is Relation-like Function-like Element of (V) : [[A,d],b₁] in (V) } is set
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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
V is non empty set
(V) is non empty set
(V) is functional non empty set
{ (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
[:(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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
(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<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
union { (Funcs (b<sub>1</sub>,b<sub>2</sub>)) where b<sub>1</sub>, b<sub>2</sub> is Element of V : verum } is set
[:V,V:] is Relation-like non empty set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of V, b<sub>3</sub> is Relation-like Function-like Element of (V) : ( ( not b<sub>2</sub> = {} or b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like b<sub>1</sub> -defined b<sub>2</sub> -valued Function-like quasi_total Element of bool [:b<sub>1</sub>,b<sub>2</sub>:] ) } is set
(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()