:: FUNCOP_1 semantic presentation

1 is non empty set
{{},1} is non empty set
z is set
delta z is Relation-like z -defined [:z,z:] -valued Function-like V18(z,[:z,z:]) Element of bool [:z,[:z,z:]:]
[:z,z:] is Relation-like set
[:z,[:z,z:]:] is Relation-like set
bool [:z,[:z,z:]:] is non empty set

bool [:z,z:] is non empty set
<:(id z),(id z):> is Relation-like Function-like set
id [:z,z:] is Relation-like [:z,z:] -defined [:z,z:] -valued Function-like one-to-one total V18([:z,z:],[:z,z:]) Element of bool [:[:z,z:],[:z,z:]:]
[:[:z,z:],[:z,z:]:] is Relation-like set
bool [:[:z,z:],[:z,z:]:] is non empty set
(id [:z,z:]) * () is Relation-like z -defined [:z,z:] -valued Function-like V18(z,[:z,z:]) Element of bool [:z,[:z,z:]:]
[:(id z),(id z):] is Relation-like [:z,z:] -defined [:z,z:] -valued Function-like one-to-one total V18([:z,z:],[:z,z:]) Element of bool [:[:z,z:],[:z,z:]:]
[:(id z),(id z):] * () is Relation-like z -defined [:z,z:] -valued Function-like V18(z,[:z,z:]) Element of bool [:z,[:z,z:]:]

proj1 z is set
A is set
z . A is set
x is set
y is set
[x,y] is V15() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
x is set
y is set
[x,y] is V15() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
[y,x] is V15() set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
e is V15() set
g is set
z is set
[g,z] is V15() set
{g,z} is non empty set
{g} is non empty set
{{g,z},{g}} is non empty set
[z,g] is V15() set
{z,g} is non empty set
{z} is non empty set
{{z,g},{z}} is non empty set
g is set
z is set
[g,z] is V15() set
{g,z} is non empty set
{g} is non empty set
{{g,z},{g}} is non empty set
z . A is set
x is set
y is set
e is set
[y,e] is V15() set
{y,e} is non empty set
{y} is non empty set
{{y,e},{y}} is non empty set
[e,y] is V15() set
{e,y} is non empty set
{e} is non empty set
{{e,y},{e}} is non empty set
z . A is set
x is set
y is set
[x,y] is V15() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
z . A is set
x is V15() set
y is set
e is set
[y,e] is V15() set
{y,e} is non empty set
{y} is non empty set
{{y,e},{y}} is non empty set
A is set
x is set
z . A is set
y is set
e is set
g is set
[e,g] is V15() set
{e,g} is non empty set
{e} is non empty set
{{e,g},{e}} is non empty set
e is set
g is set
[e,g] is V15() set
{e,g} is non empty set
{e} is non empty set
{{e,g},{e}} is non empty set
[g,e] is V15() set
{g,e} is non empty set
{g} is non empty set
{{g,e},{g}} is non empty set
z is set
x1 is set
[z,x1] is V15() set
{z,x1} is non empty set
{z} is non empty set
{{z,x1},{z}} is non empty set
z is set
x1 is set
[z,x1] is V15() set
{z,x1} is non empty set
{z} is non empty set
{{z,x1},{z}} is non empty set
e is set
g is set
[e,g] is V15() set
{e,g} is non empty set
{e} is non empty set
{{e,g},{e}} is non empty set
z is set
x1 is set
[z,x1] is V15() set
{z,x1} is non empty set
{z} is non empty set
{{z,x1},{z}} is non empty set
e is set
g is set
[e,g] is V15() set
{e,g} is non empty set
{e} is non empty set
{{e,g},{e}} is non empty set

proj1 A is set

proj1 x is set
y is set
z . y is set
e is set
g is set
[e,g] is V15() set
{e,g} is non empty set
{e} is non empty set
{{e,g},{e}} is non empty set
e is set
g is set
[e,g] is V15() set
{e,g} is non empty set
{e} is non empty set
{{e,g},{e}} is non empty set
A . y is set
[g,e] is V15() set
{g,e} is non empty set
{g} is non empty set
{{g,e},{g}} is non empty set
x . y is set
z . y is set
A . y is set
x . y is set
z . y is set
e is set
g is set
[e,g] is V15() set
{e,g} is non empty set
{e} is non empty set
{{e,g},{e}} is non empty set
A . y is set
x . y is set
A . y is set
x . y is set

proj1 A is set

proj1 x is set
y is set
A . y is set
x . y is set
e is set
g is set
[e,g] is V15() set
{e,g} is non empty set
{e} is non empty set
{{e,g},{e}} is non empty set
[g,e] is V15() set
{g,e} is non empty set
{g} is non empty set
{{g,e},{g}} is non empty set
z is set
x1 is set
[z,x1] is V15() set
{z,x1} is non empty set
{z} is non empty set
{{z,x1},{z}} is non empty set
z is set
x1 is set
[z,x1] is V15() set
{z,x1} is non empty set
{z} is non empty set
{{z,x1},{z}} is non empty set
[x1,z] is V15() set
{x1,z} is non empty set
{x1} is non empty set
{{x1,z},{x1}} is non empty set
z is set
x1 is set
[z,x1] is V15() set
{z,x1} is non empty set
{z} is non empty set
{{z,x1},{z}} is non empty set
e is set
g is set
[e,g] is V15() set
{e,g} is non empty set
{e} is non empty set
{{e,g},{e}} is non empty set
[g,e] is V15() set
{g,e} is non empty set
{g} is non empty set
{{g,e},{g}} is non empty set

proj1 <:z,A:> is set
proj1 A is set
proj1 z is set
() /\ () is set
proj1 <:A,z:> is set
x is set
<:A,z:> . x is set
A . x is set
z . x is set
[(A . x),(z . x)] is V15() set
{(A . x),(z . x)} is non empty set
{(A . x)} is non empty set
{{(A . x),(z . x)},{(A . x)}} is non empty set
<:z,A:> . x is set
[(z . x),(A . x)] is V15() set
{(z . x),(A . x)} is non empty set
{(z . x)} is non empty set
{{(z . x),(A . x)},{(z . x)}} is non empty set
(<:A,z:>) . x is set
proj1 (<:A,z:>) is set

A is set

((z | A)) is Relation-like Function-like set

proj1 (z | A) is set
proj1 z is set
() /\ A is set
proj1 (z) is set
(proj1 (z)) /\ A is set
proj1 ((z) | A) is set
x is set
(z | A) . x is set
y is set
e is set
[y,e] is V15() set
{y,e} is non empty set
{y} is non empty set
{{y,e},{y}} is non empty set
y is set
e is set
[y,e] is V15() set
{y,e} is non empty set
{y} is non empty set
{{y,e},{y}} is non empty set
z . x is set
((z | A)) . x is set
[e,y] is V15() set
{e,y} is non empty set
{e} is non empty set
{{e,y},{e}} is non empty set
(z) . x is set
((z) | A) . x is set
(z | A) . x is set
z . x is set
((z | A)) . x is set
(z) . x is set
((z) | A) . x is set
(z | A) . x is set
y is set
e is set
[y,e] is V15() set
{y,e} is non empty set
{y} is non empty set
{{y,e},{y}} is non empty set
((z | A)) . x is set
((z) | A) . x is set
((z | A)) . x is set
((z) | A) . x is set
proj1 ((z | A)) is set
z is set
delta z is Relation-like z -defined [:z,z:] -valued Function-like V18(z,[:z,z:]) Element of bool [:z,[:z,z:]:]
[:z,z:] is Relation-like set
[:z,[:z,z:]:] is Relation-like set
bool [:z,[:z,z:]:] is non empty set
(()) is Relation-like Function-like set

bool [:z,z:] is non empty set
<:(id z),(id z):> is Relation-like Function-like set
(<:(id z),(id z):>) is Relation-like Function-like set

x is set

<:(z | x),A:> is Relation-like Function-like set
proj1 (<:z,A:> | x) is set
proj1 <:z,A:> is set
(proj1 <:z,A:>) /\ x is set
proj1 z is set
proj1 A is set
() /\ () is set
(() /\ ()) /\ x is set
() /\ x is set
(() /\ x) /\ () is set
proj1 (z | x) is set
(proj1 (z | x)) /\ () is set
y is set
(<:z,A:> | x) . y is set
<:z,A:> . y is set
z . y is set
A . y is set
[(z . y),(A . y)] is V15() set
{(z . y),(A . y)} is non empty set
{(z . y)} is non empty set
{{(z . y),(A . y)},{(z . y)}} is non empty set
(z | x) . y is set
[((z | x) . y),(A . y)] is V15() set
{((z | x) . y),(A . y)} is non empty set
{((z | x) . y)} is non empty set
{{((z | x) . y),(A . y)},{((z | x) . y)}} is non empty set

x is set

<:z,(A | x):> is Relation-like Function-like set

((<:A,z:> | x)) is Relation-like Function-like set
<:(A | x),z:> is Relation-like Function-like set
(<:(A | x),z:>) is Relation-like Function-like set
z is set
A is set
{A} is non empty set

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

x is set
y is set
[x,y] is V15() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
e is set
[x,e] is V15() set
{x,e} is non empty set
{{x,e},{x}} is non empty set
x is set
z is set
A is set
x is set
(z,x) is Relation-like Function-like set
{x} is non empty set

(z,x) . A is set
[A,x] is V15() set
{A,x} is non empty set
{A} is non empty set
{{A,x},{A}} is non empty set
z is set
A is set
(z,A) is Relation-like Function-like set
{A} is non empty set

proj2 (z,A) is set

proj2 z is set
proj1 z is set
A is set
{A} is non empty set
((),A) is Relation-like Function-like set
[:(),{A}:] is Relation-like set
proj1 ((),A) is set
proj2 ((),A) is set
z is set

{z} is non empty set

z is set
(A,z) is Relation-like Function-like set
{z} is non empty set

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

{z} is non empty set

A is set

{A} is non empty set

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

the Element of proj1 z is Element of proj1 z
y is set
z . the Element of proj1 z is set
e is set
z . e is set
proj2 z is set
z is set
A is set
(z,A) is Relation-like Function-like set
{A} is non empty set

x is set
(z,A) | x is Relation-like Function-like set
z /\ x is set
((z /\ x),A) is Relation-like Function-like set
[:(z /\ x),{A}:] is Relation-like set
proj1 ((z,A) | x) is set
proj1 (z,A) is set
(proj1 (z,A)) /\ x is set
proj1 ((z /\ x),A) is set
y is set
((z,A) | x) . y is set
(z,A) . y is set
((z /\ x),A) . y is set
z is set
A is set
(z,A) is Relation-like Function-like set
{A} is non empty set

proj1 (z,A) is set
proj2 (z,A) is set

z is set
A is set
(z,A) is Relation-like Function-like set
{A} is non empty set

x is set
(z,A) " x is set
proj2 (z,A) is set
{A} /\ x is set
(z,A) " {A} is set
proj1 (z,A) is set
z is set
A is set
(z,A) is Relation-like Function-like set
{A} is non empty set

(z,A) " {A} is set
z is set
A is set
(z,A) is Relation-like Function-like set
{A} is non empty set

x is set
(z,A) " x is set
proj2 (z,A) is set

proj1 z is set
A is set
x is set
(A,x) is Relation-like Function-like set
{x} is non empty set

(A,x) * z is Relation-like Function-like set
z . x is set
(A,(z . x)) is Relation-like Function-like set
{(z . x)} is non empty set
[:A,{(z . x)}:] is Relation-like set
y is set
proj1 ((A,x) * z) is set
proj1 (A,x) is set
((A,x) * z) . y is set
(A,x) . y is set
z . ((A,x) . y) is set
(A,(z . x)) . y is set
(A,x) " () is set
proj1 (A,(z . x)) is set

proj1 z is set
A is set
x is set
(A,x) is Relation-like Function-like set
{x} is non empty set

(A,x) * z is Relation-like Function-like set
proj1 ((A,x) * z) is set
the Element of A is Element of A
proj1 (A,x) is set
(A,x) . the Element of A is set

A is set
z " A is set
x is set
(A,x) is Relation-like Function-like set
{x} is non empty set

z * (A,x) is Relation-like Function-like set
((z " A),x) is Relation-like Function-like set
[:(z " A),{x}:] is Relation-like set
proj1 (z * (A,x)) is set
proj1 (A,x) is set
z " (proj1 (A,x)) is set
y is set
z . y is set
(z * (A,x)) . y is set
(A,x) . (z . y) is set
((z " A),x) . y is set
proj1 ((z " A),x) is set
z is set
A is set
x is set
[A,x] is V15() set
{A,x} is non empty set
{A} is non empty set
{{A,x},{A}} is non empty set
(z,[A,x]) is Relation-like Function-like set

[:z,{[A,x]}:] is Relation-like set
((z,[A,x])) is Relation-like Function-like set
[x,A] is V15() set
{x,A} is non empty set
{x} is non empty set
{{x,A},{x}} is non empty set
(z,[x,A]) is Relation-like Function-like set

[:z,{[x,A]}:] is Relation-like set
proj1 ((z,[A,x])) is set
proj1 (z,[A,x]) is set
y is set
(z,[A,x]) . y is set
((z,[A,x])) . y is set
(z,[x,A]) . y is set
proj1 (z,[x,A]) is set

(z,A,x) is set

proj1 (<:z,A:> * x) is set
y is set
(<:z,A:> * x) . y is set
z . y is set
A . y is set
x . ((z . y),(A . y)) is set
[(z . y),(A . y)] is V15() set
{(z . y),(A . y)} is non empty set
{(z . y)} is non empty set
{{(z . y),(A . y)},{(z . y)}} is non empty set
x . [(z . y),(A . y)] is set
proj1 <:z,A:> is set
<:z,A:> . y is set
x . (<:z,A:> . y) is set

(x,z,A) is Relation-like Function-like set

proj1 (x,z,A) is set

proj1 y is set
e is set
y . e is set
z . e is set
A . e is set
x . ((z . e),(A . e)) is set
[(z . e),(A . e)] is V15() set
{(z . e),(A . e)} is non empty set
{(z . e)} is non empty set
{{(z . e),(A . e)},{(z . e)}} is non empty set
x . [(z . e),(A . e)] is set
(x,z,A) . e is set
y is set

(x,z,A) is Relation-like Function-like set

proj1 (x,z,A) is set
(x,z,A) . y is set
z . y is set
A . y is set
x . ((z . y),(A . y)) is set
[(z . y),(A . y)] is V15() set
{(z . y),(A . y)} is non empty set
{(z . y)} is non empty set
{{(z . y),(A . y)},{(z . y)}} is non empty set
x . [(z . y),(A . y)] is set

y is set

(e,z,x) is Relation-like Function-like set

(e,z,x) | y is Relation-like Function-like set
(e,A,x) is Relation-like Function-like set

(e,A,x) | y is Relation-like Function-like set

(<:z,x:> | y) * e is Relation-like Function-like set
<:(z | y),x:> is Relation-like Function-like set
<:(z | y),x:> * e is Relation-like Function-like set

(<:A,x:> | y) * e is Relation-like Function-like set

y is set

(e,x,z) is Relation-like Function-like set

(e,x,z) | y is Relation-like Function-like set
(e,x,A) is Relation-like Function-like set

(e,x,A) | y is Relation-like Function-like set

(<:x,z:> | y) * e is Relation-like Function-like set
<:x,(z | y):> is Relation-like Function-like set
<:x,(z | y):> * e is Relation-like Function-like set

(<:x,A:> | y) * e is Relation-like Function-like set

(y,z,A) is Relation-like Function-like set

x * (y,z,A) is Relation-like Function-like set
(y,(x * z),(x * A)) is Relation-like Function-like set
<:(x * z),(x * A):> is Relation-like Function-like set
<:(x * z),(x * A):> * y is Relation-like Function-like set

(x * <:z,A:>) * y is Relation-like Function-like set

proj1 A is set
x is set
((),x) is Relation-like Function-like set
{x} is non empty set
[:(),{x}:] is Relation-like set
<:A,((),x):> is Relation-like Function-like set

<:A,((),x):> * z is Relation-like Function-like set

x is set
(z,A,x) is set
proj1 A is set
((),x) is Relation-like Function-like set
{x} is non empty set
[:(),{x}:] is Relation-like set
<:A,((),x):> is Relation-like Function-like set
<:A,((),x):> * z is Relation-like Function-like set

x is set
(A,z,x) is Relation-like Function-like set
proj1 z is set
((),x) is Relation-like Function-like set
{x} is non empty set
[:(),{x}:] is Relation-like set
<:z,((),x):> is Relation-like Function-like set
<:z,((),x):> * A is Relation-like Function-like set
(A,z,((),x)) is Relation-like Function-like set

x is set
z . x is set
y is set
(A,z,y) is Relation-like Function-like set
proj1 z is set
((),y) is Relation-like Function-like set
{y} is non empty set
[:(),{y}:] is Relation-like set
<:z,((),y):> is Relation-like Function-like set
<:z,((),y):> * A is Relation-like Function-like set
proj1 (A,z,y) is set
(A,z,y) . x is set
A . ((z . x),y) is set
[(z . x),y] is V15() set
{(z . x),y} is non empty set
{(z . x)} is non empty set
{{(z . x),y},{(z . x)}} is non empty set
A . [(z . x),y] is set
proj1 <:z,((),y):> is set
proj1 ((),y) is set
() /\ (proj1 ((),y)) is set
((),y) . x is set
A . ((z . x),(((),y) . x)) is set
[(z . x),(((),y) . x)] is V15() set
{(z . x),(((),y) . x)} is non empty set
{{(z . x),(((),y) . x)},{(z . x)}} is non empty set
A . [(z . x),(((),y) . x)] is set

x is set

e is set
(y,z,e) is Relation-like Function-like set
proj1 z is set
((),e) is Relation-like Function-like set
{e} is non empty set
[:(),{e}:] is Relation-like set
<:z,((),e):> is Relation-like Function-like set
<:z,((),e):> * y is Relation-like Function-like set
(y,z,e) | x is Relation-like Function-like set
(y,A,e) is Relation-like Function-like set
proj1 A is set
((),e) is Relation-like Function-like set
[:(),{e}:] is Relation-like set
<:A,((),e):> is Relation-like Function-like set
<:A,((),e):> * y is Relation-like Function-like set
(y,A,e) | x is Relation-like Function-like set
() /\ x is set
proj1 (z | x) is set
() /\ x is set
((),e) | x is Relation-like Function-like set
((() /\ x),e) is Relation-like Function-like set
[:(() /\ x),{e}:] is Relation-like set
((),e) | x is Relation-like Function-like set
(y,z,((),e)) is Relation-like Function-like set
(y,z,((),e)) | x is Relation-like Function-like set
(y,A,((),e)) is Relation-like Function-like set
<:A,((),e):> is Relation-like Function-like set
<:A,((),e):> * y is Relation-like Function-like set
(y,A,((),e)) | x is Relation-like Function-like set
(y,A,((),e)) is Relation-like Function-like set
(y,A,((),e)) | x is Relation-like Function-like set

y is set
(x,z,y) is Relation-like Function-like set
proj1 z is set
((),y) is Relation-like Function-like set
{y} is non empty set
[:(),{y}:] is Relation-like set
<:z,((),y):> is Relation-like Function-like set
<:z,((),y):> * x is Relation-like Function-like set
A * (x,z,y) is Relation-like Function-like set
(x,(A * z),y) is Relation-like Function-like set
proj1 (A * z) is set
((proj1 (A * z)),y) is Relation-like Function-like set
[:(proj1 (A * z)),{y}:] is Relation-like set
<:(A * z),((proj1 (A * z)),y):> is Relation-like Function-like set
<:(A * z),((proj1 (A * z)),y):> * x is Relation-like Function-like set
proj1 ((),y) is set
A * ((),y) is Relation-like Function-like set
proj1 (A * ((),y)) is set
e is set
A . e is set
(A * ((),y)) . e is set
((),y) . (A . e) is set
(x,z,((),y)) is Relation-like Function-like set
A * (x,z,((),y)) is Relation-like Function-like set
(x,(A * z),(A * ((),y))) is Relation-like Function-like set
<:(A * z),(A * ((),y)):> is Relation-like Function-like set
<:(A * z),(A * ((),y)):> * x is Relation-like Function-like set

A is set

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

y is set
(x,z,y) is Relation-like Function-like set
proj1 z is set
((),y) is Relation-like Function-like set
{y} is non empty set
[:(),{y}:] is Relation-like set
<:z,((),y):> is Relation-like Function-like set
<:z,((),y):> * x is Relation-like Function-like set
(id A) * (x,z,y) is Relation-like A -defined Function-like set
(x,(z | A),y) is Relation-like Function-like set
proj1 (z | A) is set
((proj1 (z | A)),y) is Relation-like Function-like set
[:(proj1 (z | A)),{y}:] is Relation-like set
<:(z | A),((proj1 (z | A)),y):> is Relation-like Function-like set
<:(z | A),((proj1 (z | A)),y):> * x is Relation-like Function-like set

(x,((id A) * z),y) is Relation-like Function-like set
proj1 ((id A) * z) is set
((proj1 ((id A) * z)),y) is Relation-like Function-like set
[:(proj1 ((id A) * z)),{y}:] is Relation-like set
<:((id A) * z),((proj1 ((id A) * z)),y):> is Relation-like Function-like set
<:((id A) * z),((proj1 ((id A) * z)),y):> * x is Relation-like Function-like set

proj1 x is set
A is set
((),A) is Relation-like Function-like set
{A} is non empty set
[:(),{A}:] is Relation-like set
<:((),A),x:> is Relation-like Function-like set

<:((),A),x:> * z is Relation-like Function-like set

A is set

(z,A,x) is set
proj1 x is set
((),A) is Relation-like Function-like set
{A} is non empty set
[:(),{A}:] is Relation-like set
<:((),A),x:> is Relation-like Function-like set
<:((),A),x:> * z is Relation-like Function-like set

x is set

(A,x,z) is Relation-like Function-like set
proj1 z is set
((),x) is Relation-like Function-like set
{x} is non empty set
[:(),{x}:] is Relation-like set
<:((),x),z:> is Relation-like Function-like set
<:((),x),z:> * A is Relation-like Function-like set
(A,((),x),z) is Relation-like Function-like set

x is set
z . x is set
y is set
(A,y,z) is Relation-like Function-like set
proj1 z is set
((),y) is Relation-like Function-like set
{y} is non empty set
[:(),{y}:] is Relation-like set
<:((),y),z:> is Relation-like Function-like set
<:((),y),z:> * A is Relation-like Function-like set
proj1 (A,y,z) is set
(A,y,z) . x is set
A . (y,(z . x)) is set
[y,(z . x)] is V15() set
{y,(z . x)} is non empty set
{{y,(z . x)},{y}} is non empty set
A . [y,(z . x)] is set
proj1 <:((),y),z:> is set
proj1 ((),y) is set
(proj1 ((),y)) /\ () is set
((),y) . x is set
A . ((((),y) . x),(z . x)) is set
[(((),y) . x),(z . x)] is V15() set
{(((),y) . x),(z . x)} is non empty set
{(((),y) . x)} is non empty set
{{(((),y) . x),(z . x)},{(((),y) . x)}} is non empty set
A . [(((),y) . x),(z . x)] is set

x is set

e is set
(y,e,z) is Relation-like Function-like set
proj1 z is set
((),e) is Relation-like Function-like set
{e} is non empty set
[:(),{e}:] is Relation-like set
<:((),e),z:> is Relation-like Function-like set
<:((),e),z:> * y is Relation-like Function-like set
(y,e,z) | x is Relation-like Function-like set
(y,e,A) is Relation-like Function-like set
proj1 A is set
((),e) is Relation-like Function-like set
[:(),{e}:] is Relation-like set
<:((),e),A:> is Relation-like Function-like set
<:((),e),A:> * y is Relation-like Function-like set
(y,e,A) | x is Relation-like Function-like set
() /\ x is set
proj1 (z | x) is set
() /\ x is set
((),e) | x is Relation-like Function-like set
((() /\ x),e) is Relation-like Function-like set
[:(() /\ x),{e}:] is Relation-like set
((),e) | x is Relation-like Function-like set
(y,((),e),z) is Relation-like Function-like set
(y,((),e),z) | x is Relation-like Function-like set
(y,((),e),A) is Relation-like Function-like set
<:((),e),A:> is Relation-like Function-like set
<:((),e),A:> * y is Relation-like Function-like set
(y,((),e),A) | x is Relation-like Function-like set
(y,((),e),A) is Relation-like Function-like set
(y,((),e),A) | x is Relation-like Function-like set

y is set
(x,y,z) is Relation-like Function-like set
proj1 z is set
((),y) is Relation-like Function-like set
{y} is non empty set
[:(),{y}:] is Relation-like set
<:((),y),z:> is Relation-like Function-like set
<:((),y),z:> * x is Relation-like Function-like set
A * (x,y,z) is Relation-like Function-like set
(x,y,(A * z)) is Relation-like Function-like set
proj1 (A * z) is set
((proj1 (A * z)),y) is Relation-like Function-like set
[:(proj1 (A * z)),{y}:] is Relation-like set
<:((proj1 (A * z)),y),(A * z):> is Relation-like Function-like set
<:((proj1 (A * z)),y),(A * z):> * x is Relation-like Function-like set
proj1 ((),y) is set
A * ((),y) is Relation-like Function-like set
proj1 (A * ((),y)) is set
e is set
A . e is set
(A * ((),y)) . e is set
((),y) . (A . e) is set
(x,((),y),z) is Relation-like Function-like set
A * (x,((),y),z) is Relation-like Function-like set
(x,(A * ((),y)),(A * z)) is Relation-like Function-like set
<:(A * ((),y)),(A * z):> is Relation-like Function-like set
<:(A * ((),y)),(A * z):> * x is Relation-like Function-like set

A is set

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

y is set
(x,y,z) is Relation-like Function-like set
proj1 z is set
((),y) is Relation-like Function-like set
{y} is non empty set
[:(),{y}:] is Relation-like set
<:((),y),z:> is Relation-like Function-like set
<:((),y),z:> * x is Relation-like Function-like set
(id A) * (x,y,z) is Relation-like A -defined Function-like set
(x,y,(z | A)) is Relation-like Function-like set
proj1 (z | A) is set
((proj1 (z | A)),y) is Relation-like Function-like set
[:(proj1 (z | A)),{y}:] is Relation-like set
<:((proj1 (z | A)),y),(z | A):> is Relation-like Function-like set
<:((proj1 (z | A)),y),(z | A):> * x is Relation-like Function-like set

(x,y,((id A) * z)) is Relation-like Function-like set
proj1 ((id A) * z) is set
((proj1 ((id A) * z)),y) is Relation-like Function-like set
[:(proj1 ((id A) * z)),{y}:] is Relation-like set
<:((proj1 ((id A) * z)),y),((id A) * z):> is Relation-like Function-like set
<:((proj1 ((id A) * z)),y),((id A) * z):> * x is Relation-like Function-like set
z is non empty set
[:z,z:] is Relation-like non empty set
[:[:z,z:],z:] is Relation-like non empty set
bool [:[:z,z:],z:] is non empty set
A is set
[:A,z:] is Relation-like set
bool [:A,z:] is non empty set
x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

(x,y,e) is Relation-like Function-like set

<:y,e:> is Relation-like A -defined [:z,z:] -valued Function-like total V18(A,[:z,z:]) Element of bool [:A,[:z,z:]:]
[:A,[:z,z:]:] is Relation-like set
bool [:A,[:z,z:]:] is non empty set
x * <:y,e:> is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
z is non empty set
[:z,z:] is Relation-like non empty set
[:[:z,z:],z:] is Relation-like non empty set
bool [:[:z,z:],z:] is non empty set
A is set
[:A,z:] is Relation-like set
bool [:A,z:] is non empty set
x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

(x,y,e) is Relation-like Function-like set

z is non empty set
[:z,z:] is Relation-like non empty set
[:[:z,z:],z:] is Relation-like non empty set
bool [:[:z,z:],z:] is non empty set
A is non empty set
[:A,z:] is Relation-like non empty set
bool [:A,z:] is non empty set
x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]
y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
e is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
(z,A,x,y,e) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

g is Element of A
(z,A,x,y,e) . g is Element of z
y . g is Element of z
e . g is Element of z
x . ((y . g),(e . g)) is Element of z
[(y . g),(e . g)] is V15() set
{(y . g),(e . g)} is non empty set
{(y . g)} is non empty set
{{(y . g),(e . g)},{(y . g)}} is non empty set
x . [(y . g),(e . g)] is set
dom (z,A,x,y,e) is non empty Element of bool A
bool A is non empty set
z is non empty set
[:z,z:] is Relation-like non empty set
[:[:z,z:],z:] is Relation-like non empty set
bool [:[:z,z:],z:] is non empty set
A is non empty set
[:A,z:] is Relation-like non empty set
bool [:A,z:] is non empty set
x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]
y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
e is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
(z,A,x,y,e) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

g is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
z is Element of A
g . z is Element of z
y . z is Element of z
e . z is Element of z
x . ((y . z),(e . z)) is Element of z
[(y . z),(e . z)] is V15() set
{(y . z),(e . z)} is non empty set
{(y . z)} is non empty set
{{(y . z),(e . z)},{(y . z)}} is non empty set
x . [(y . z),(e . z)] is set
(z,A,x,y,e) . z is Element of z
z is non empty set
[:z,z:] is Relation-like non empty set
[:[:z,z:],z:] is Relation-like non empty set
bool [:[:z,z:],z:] is non empty set
bool [:z,z:] is non empty set

A is non empty set
[:A,z:] is Relation-like non empty set
bool [:A,z:] is non empty set
x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]
y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
e is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]
(z,z,x,(id z),e) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

(z,z,x,(id z),e) * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
e * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
(z,A,x,y,(e * y)) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
<:y,(e * y):> is Relation-like Function-like set
<:y,(e * y):> * x is Relation-like z -valued Function-like set
(id z) * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
(z,A,x,((id z) * y),(e * y)) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
<:((id z) * y),(e * y):> is Relation-like Function-like set
<:((id z) * y),(e * y):> * x is Relation-like z -valued Function-like set
z is non empty set
[:z,z:] is Relation-like non empty set
[:[:z,z:],z:] is Relation-like non empty set
bool [:[:z,z:],z:] is non empty set
bool [:z,z:] is non empty set

A is non empty set
[:A,z:] is Relation-like non empty set
bool [:A,z:] is non empty set
x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]
y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
e is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]
(z,z,x,e,(id z)) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

(z,z,x,e,(id z)) * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
e * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
(z,A,x,(e * y),y) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
<:(e * y),y:> is Relation-like Function-like set
<:(e * y),y:> * x is Relation-like z -valued Function-like set
(id z) * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
(z,A,x,(e * y),((id z) * y)) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
<:(e * y),((id z) * y):> is Relation-like Function-like set
<:(e * y),((id z) * y):> * x is Relation-like z -valued Function-like set
z is non empty set
[:z,z:] is Relation-like non empty set
[:[:z,z:],z:] is Relation-like non empty set
bool [:[:z,z:],z:] is non empty set

bool [:z,z:] is non empty set
A is non empty set
[:A,z:] is Relation-like non empty set
bool [:A,z:] is non empty set
x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]
(z,z,x,(id z),(id z)) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]
<:(id z),(id z):> is Relation-like Function-like set
<:(id z),(id z):> * x is Relation-like z -valued Function-like set
y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
(z,z,x,(id z),(id z)) * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
(z,A,x,y,y) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

(id z) * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
(z,A,x,((id z) * y),((id z) * y)) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
<:((id z) * y),((id z) * y):> is Relation-like Function-like set
<:((id z) * y),((id z) * y):> * x is Relation-like z -valued Function-like set
(z,A,x,((id z) * y),y) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
<:((id z) * y),y:> is Relation-like Function-like set
<:((id z) * y),y:> * x is Relation-like z -valued Function-like set
z is non empty set
[:z,z:] is Relation-like non empty set
[:[:z,z:],z:] is Relation-like non empty set
bool [:[:z,z:],z:] is non empty set
bool [:z,z:] is non empty set

A is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]
x is Element of z
y is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]
(z,z,A,(id z),y) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

(z,z,A,(id z),y) . x is Element of z
y . x is Element of z
A . (x,(y . x)) is Element of z
[x,(y . x)] is V15() set
{x,(y . x)} is non empty set
{x} is non empty set
{{x,(y . x)},{x}} is non empty set
A . [x,(y . x)] is set
(id z) . x is Element of z
A . (((id z) . x),(y . x)) is Element of z
[((id z) . x),(y . x)] is V15() set
{((id z) . x),(y . x)} is non empty set
{((id z) . x)} is non empty set
{{((id z) . x),(y . x)},{((id z) . x)}} is non empty set
A . [((id z) . x),(y . x)] is set
z is non empty set
[:z,z:] is Relation-like non empty set
[:[:z,z:],z:] is Relation-like non empty set
bool [:[:z,z:],z:] is non empty set
bool [:z,z:] is non empty set

A is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]
x is Element of z
y is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]
(z,z,A,y,(id z)) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

(z,z,A,y,(id z)) . x is Element of z
y . x is Element of z
A . ((y . x),x) is Element of z
[(y . x),x] is V15() set
{(y . x),x} is non empty set
{(y . x)} is non empty set
{{(y . x),x},{(y . x)}} is non empty set
A . [(y . x),x] is set
(id z) . x is Element of z
A . ((y . x),((id z) . x)) is Element of z
[(y . x),((id z) . x)] is V15() set
{(y . x),((id z) . x)} is non empty set
{{(y . x),((id z) . x)},{(y . x)}} is non empty set
A . [(y . x),((id z) . x)] is set
z is non empty set
[:z,z:] is Relation-like non empty set
[:[:z,z:],z:] is Relation-like non empty set
bool [:[:z,z:],z:] is non empty set

bool [:z,z:] is non empty set
A is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]
(z,z,A,(id z),(id z)) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]
<:(id z),(id z):> is Relation-like Function-like set
<:(id z),(id z):> * A is Relation-like z -valued Function-like set
x is Element of z
(z,z,A,(id z),(id z)) . x is Element of z
A . (x,x) is Element of z
[x,x] is V15() set
{x,x} is non empty set
{x} is non empty set
{{x,x},{x}} is non empty set
A . [x,x] is set
(id z) . x is Element of z
A . (((id z) . x),((id z) . x)) is Element of z
[((id z) . x),((id z) . x)] is V15() set
{((id z) . x),((id z) . x)} is non empty set
{((id z) . x)} is non empty set
{{((id z) . x),((id z) . x)},{((id z) . x)}} is non empty set
A . [((id z) . x),((id z) . x)] is set
A . (((id z) . x),x) is Element of z
[((id z) . x),x] is V15() set
{((id z) . x),x} is non empty set
{{((id z) . x),x},{((id z) . x)}} is non empty set
A . [((id z) . x),x] is set
z is set
A is set
[:z,A:] is Relation-like set
bool [:z,A:] is non empty set
x is set
(z,x) is Relation-like Function-like set
{x} is non empty set

proj2 (z,x) is set
proj1 (z,x) is set
z is set
A is set
(z,A) is Relation-like Function-like set
{A} is non empty set

bool [:z,{A}:] is non empty set
proj1 (z,A) is set
proj2 (z,A) is set
z is non empty set
A is set
x is Element of z
(A,x) is Relation-like Function-like set
{x} is non empty set

[:A,z:] is Relation-like set
bool [:A,z:] is non empty set
A is non empty set
z is set
x is Element of A
(A,z,x) is Relation-like z -defined A -valued Function-like total V18(z,A) Element of bool [:z,A:]
[:z,A:] is Relation-like set
bool [:z,A:] is non empty set
{x} is non empty set

z is non empty set
[:z,z:] is Relation-like non empty set
[:[:z,z:],z:] is Relation-like non empty set
bool [:[:z,z:],z:] is non empty set
A is set
[:A,z:] is Relation-like set
bool [:A,z:] is non empty set
x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

e is Element of z
(x,y,e) is Relation-like Function-like set
proj1 y is set
((),e) is Relation-like Function-like set
{e} is non empty set
[:(),{e}:] is Relation-like set
<:y,((),e):> is Relation-like Function-like set
<:y,((),e):> * x is Relation-like z -valued Function-like set
dom y is Element of bool A
bool A is non empty set
(z,(dom y),e) is Relation-like dom y -defined z -valued Function-like total V18( dom y,z) Element of bool [:(dom y),z:]
[:(dom y),z:] is Relation-like set
bool [:(dom y),z:] is non empty set
[:(dom y),{e}:] is Relation-like set

<:y,g:> is Relation-like A -defined [:z,z:] -valued Function-like total V18(A,[:z,z:]) Element of bool [:A,[:z,z:]:]
[:A,[:z,z:]:] is Relation-like set
bool [:A,[:z,z:]:] is non empty set
x * <:y,g:> is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
z is non empty set
[:z,z:] is Relation-like non empty set
[:[:z,z:],z:] is Relation-like non empty set