:: FUNCOP_1 semantic presentation

{} 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
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
id z is Relation-like z -defined z -valued Function-like one-to-one total V18(z,z) Element of bool [:z,z:]
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:]) * (delta 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):] * (delta z) is Relation-like z -defined [:z,z:] -valued Function-like V18(z,[:z,z:]) Element of bool [:z,[:z,z:]:]
z is Relation-like Function-like set
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
A is Relation-like Function-like set
proj1 A is set
x is Relation-like Function-like 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
A is Relation-like Function-like set
proj1 A is set
x is Relation-like Function-like 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
z is Relation-like Function-like set
A is Relation-like Function-like set
<:z,A:> is Relation-like Function-like set
<:A,z:> is Relation-like Function-like set
(<:A,z:>) is Relation-like Function-like set
proj1 <:z,A:> is set
proj1 A is set
proj1 z is set
(proj1 A) /\ (proj1 z) 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
z is Relation-like Function-like set
(z) is Relation-like Function-like set
A is set
z | A is Relation-like Function-like set
((z | A)) is Relation-like Function-like set
(z) | A is Relation-like Function-like set
proj1 (z | A) is set
proj1 z is set
(proj1 z) /\ 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
((delta z)) is Relation-like Function-like set
id z is Relation-like z -defined z -valued Function-like one-to-one total V18(z,z) Element of bool [:z,z:]
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
z is Relation-like Function-like set
A is Relation-like Function-like set
<:z,A:> is Relation-like Function-like set
x is set
<:z,A:> | x is Relation-like Function-like set
z | x is Relation-like Function-like 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
(proj1 z) /\ (proj1 A) is set
((proj1 z) /\ (proj1 A)) /\ x is set
(proj1 z) /\ x is set
((proj1 z) /\ x) /\ (proj1 A) is set
proj1 (z | x) is set
(proj1 (z | x)) /\ (proj1 A) 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
z is Relation-like Function-like set
A is Relation-like Function-like set
<:z,A:> is Relation-like Function-like set
x is set
<:z,A:> | x is Relation-like Function-like set
A | x is Relation-like Function-like set
<:z,(A | x):> is Relation-like Function-like set
<:A,z:> is Relation-like Function-like set
(<:A,z:>) is Relation-like Function-like set
(<:A,z:>) | x is Relation-like Function-like set
<:A,z:> | 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,{A}:] is Relation-like set
z is set
A is set
(z,A) is set
{A} is non empty set
[:z,{A}:] is Relation-like 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}:] is Relation-like 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
[:z,{A}:] is Relation-like set
proj2 (z,A) is set
z is Relation-like Function-like set
proj2 z is set
proj1 z is set
A is set
{A} is non empty set
((proj1 z),A) is Relation-like Function-like set
[:(proj1 z),{A}:] is Relation-like set
proj1 ((proj1 z),A) is set
proj2 ((proj1 z),A) is set
z is set
({},z) is Relation-like Function-like set
{z} is non empty set
[:{},{z}:] is Relation-like set
A is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
z is set
(A,z) is Relation-like Function-like set
{z} is non empty set
[:A,{z}:] is Relation-like 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 Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
{z} is non empty set
[:{},{z}:] is Relation-like set
proj1 ({},z) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
A is set
({},A) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
{A} is non empty set
[:{},{A}:] is Relation-like set
proj2 ({},A) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial set
z is Relation-like Function-like set
proj1 z is set
A is set
((proj1 z),A) is Relation-like Function-like set
{A} is non empty set
[:(proj1 z),{A}:] is Relation-like set
({},A) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
[:{},{A}:] is Relation-like set
proj1 ({},A) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty 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
[:z,{A}:] is Relation-like 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
[:z,{A}:] is Relation-like set
proj1 (z,A) is set
proj2 (z,A) is set
({},A) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
[:{},{A}:] is Relation-like set
proj2 ({},A) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial set
z is set
A is set
(z,A) is Relation-like Function-like set
{A} is non empty set
[:z,{A}:] is Relation-like 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}:] is Relation-like 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
[:z,{A}:] is Relation-like set
x is set
(z,A) " x is set
proj2 (z,A) is set
z is Relation-like Function-like 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}:] is Relation-like 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) " (proj1 z) is set
proj1 (A,(z . x)) is set
z is Relation-like Function-like 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}:] is Relation-like 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
z is Relation-like Function-like set
A is set
z " A is set
x is set
(A,x) is Relation-like Function-like set
{x} is non empty set
[:A,{x}:] is Relation-like 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
{[A,x]} is Relation-like Function-like non empty 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
{[x,A]} is Relation-like Function-like non empty 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
A is Relation-like Function-like set
x is Relation-like Function-like set
<:A,x:> is Relation-like Function-like set
z is Relation-like Function-like set
<:A,x:> * z is Relation-like Function-like set
z is Relation-like Function-like set
A is Relation-like Function-like set
x is Relation-like Function-like set
(z,A,x) is set
<:A,x:> is Relation-like Function-like set
<:A,x:> * z is Relation-like Function-like set
z is Relation-like Function-like set
A is Relation-like Function-like set
<:z,A:> is Relation-like Function-like set
x is Relation-like Function-like set
<:z,A:> * x is Relation-like Function-like 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
z is Relation-like Function-like set
A is Relation-like Function-like set
x is Relation-like Function-like set
(x,z,A) is Relation-like Function-like set
<:z,A:> is Relation-like Function-like set
<:z,A:> * x is Relation-like Function-like set
proj1 (x,z,A) is set
y is Relation-like Function-like 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 is Relation-like Function-like set
z is Relation-like Function-like set
A is Relation-like Function-like set
(x,z,A) is Relation-like Function-like set
<:z,A:> is Relation-like Function-like set
<:z,A:> * x 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
z is Relation-like Function-like set
A is Relation-like Function-like set
x is Relation-like Function-like set
y is set
z | y is Relation-like Function-like set
A | y is Relation-like Function-like set
e is Relation-like Function-like set
(e,z,x) is Relation-like Function-like set
<:z,x:> is Relation-like Function-like set
<:z,x:> * e 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
<:A,x:> is Relation-like Function-like set
<:A,x:> * e is Relation-like Function-like set
(e,A,x) | y is Relation-like Function-like set
<:z,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 is Relation-like Function-like set
(<:A,x:> | y) * e is Relation-like Function-like set
z is Relation-like Function-like set
A is Relation-like Function-like set
x is Relation-like Function-like set
y is set
z | y is Relation-like Function-like set
A | y is Relation-like Function-like set
e is Relation-like Function-like set
(e,x,z) is Relation-like Function-like set
<:x,z:> is Relation-like Function-like set
<:x,z:> * e 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
<:x,A:> is Relation-like Function-like set
<:x,A:> * e is Relation-like Function-like set
(e,x,A) | y 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,(z | y):> is Relation-like Function-like set
<:x,(z | y):> * e is Relation-like Function-like set
<:x,A:> | y is Relation-like Function-like set
(<:x,A:> | y) * e is Relation-like Function-like set
z is Relation-like Function-like set
A is Relation-like Function-like set
x is Relation-like Function-like set
x * z is Relation-like Function-like set
x * A is Relation-like Function-like set
y is Relation-like Function-like set
(y,z,A) is Relation-like Function-like set
<:z,A:> is Relation-like Function-like set
<:z,A:> * y 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:> is Relation-like Function-like set
(x * <:z,A:>) * y is Relation-like Function-like set
A is Relation-like Function-like set
proj1 A is set
x is set
((proj1 A),x) is Relation-like Function-like set
{x} is non empty set
[:(proj1 A),{x}:] is Relation-like set
<:A,((proj1 A),x):> is Relation-like Function-like set
z is Relation-like Function-like set
<:A,((proj1 A),x):> * z is Relation-like Function-like set
z is Relation-like Function-like set
A is Relation-like Function-like set
x is set
(z,A,x) is set
proj1 A is set
((proj1 A),x) is Relation-like Function-like set
{x} is non empty set
[:(proj1 A),{x}:] is Relation-like set
<:A,((proj1 A),x):> is Relation-like Function-like set
<:A,((proj1 A),x):> * z is Relation-like Function-like set
A is Relation-like Function-like set
z is Relation-like Function-like set
x is set
(A,z,x) is Relation-like Function-like set
proj1 z is set
((proj1 z),x) is Relation-like Function-like set
{x} is non empty set
[:(proj1 z),{x}:] is Relation-like set
<:z,((proj1 z),x):> is Relation-like Function-like set
<:z,((proj1 z),x):> * A is Relation-like Function-like set
(A,z,((proj1 z),x)) is Relation-like Function-like set
z is Relation-like Function-like set
A 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
((proj1 z),y) is Relation-like Function-like set
{y} is non empty set
[:(proj1 z),{y}:] is Relation-like set
<:z,((proj1 z),y):> is Relation-like Function-like set
<:z,((proj1 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,((proj1 z),y):> is set
proj1 ((proj1 z),y) is set
(proj1 z) /\ (proj1 ((proj1 z),y)) is set
((proj1 z),y) . x is set
A . ((z . x),(((proj1 z),y) . x)) is set
[(z . x),(((proj1 z),y) . x)] is V15() set
{(z . x),(((proj1 z),y) . x)} is non empty set
{{(z . x),(((proj1 z),y) . x)},{(z . x)}} is non empty set
A . [(z . x),(((proj1 z),y) . x)] is set
z is Relation-like Function-like set
A is Relation-like Function-like set
x is set
z | x is Relation-like Function-like set
A | x is Relation-like Function-like set
y is Relation-like Function-like set
e is set
(y,z,e) is Relation-like Function-like set
proj1 z is set
((proj1 z),e) is Relation-like Function-like set
{e} is non empty set
[:(proj1 z),{e}:] is Relation-like set
<:z,((proj1 z),e):> is Relation-like Function-like set
<:z,((proj1 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
((proj1 A),e) is Relation-like Function-like set
[:(proj1 A),{e}:] is Relation-like set
<:A,((proj1 A),e):> is Relation-like Function-like set
<:A,((proj1 A),e):> * y is Relation-like Function-like set
(y,A,e) | x is Relation-like Function-like set
(proj1 z) /\ x is set
proj1 (z | x) is set
(proj1 A) /\ x is set
((proj1 z),e) | x is Relation-like Function-like set
(((proj1 A) /\ x),e) is Relation-like Function-like set
[:((proj1 A) /\ x),{e}:] is Relation-like set
((proj1 A),e) | x is Relation-like Function-like set
(y,z,((proj1 z),e)) is Relation-like Function-like set
(y,z,((proj1 z),e)) | x is Relation-like Function-like set
(y,A,((proj1 z),e)) is Relation-like Function-like set
<:A,((proj1 z),e):> is Relation-like Function-like set
<:A,((proj1 z),e):> * y is Relation-like Function-like set
(y,A,((proj1 z),e)) | x is Relation-like Function-like set
(y,A,((proj1 A),e)) is Relation-like Function-like set
(y,A,((proj1 A),e)) | x is Relation-like Function-like set
z is Relation-like Function-like set
A is Relation-like Function-like set
A * z is Relation-like Function-like set
x is Relation-like Function-like set
y is set
(x,z,y) is Relation-like Function-like set
proj1 z is set
((proj1 z),y) is Relation-like Function-like set
{y} is non empty set
[:(proj1 z),{y}:] is Relation-like set
<:z,((proj1 z),y):> is Relation-like Function-like set
<:z,((proj1 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 ((proj1 z),y) is set
A * ((proj1 z),y) is Relation-like Function-like set
proj1 (A * ((proj1 z),y)) is set
e is set
A . e is set
(A * ((proj1 z),y)) . e is set
((proj1 z),y) . (A . e) is set
(x,z,((proj1 z),y)) is Relation-like Function-like set
A * (x,z,((proj1 z),y)) is Relation-like Function-like set
(x,(A * z),(A * ((proj1 z),y))) is Relation-like Function-like set
<:(A * z),(A * ((proj1 z),y)):> is Relation-like Function-like set
<:(A * z),(A * ((proj1 z),y)):> * x is Relation-like Function-like set
z is Relation-like Function-like set
A is set
id A is Relation-like A -defined A -valued Function-like one-to-one total V18(A,A) Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
z | A is Relation-like Function-like set
x is Relation-like Function-like set
y is set
(x,z,y) is Relation-like Function-like set
proj1 z is set
((proj1 z),y) is Relation-like Function-like set
{y} is non empty set
[:(proj1 z),{y}:] is Relation-like set
<:z,((proj1 z),y):> is Relation-like Function-like set
<:z,((proj1 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
(id A) * z is Relation-like A -defined 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
x is Relation-like Function-like set
proj1 x is set
A is set
((proj1 x),A) is Relation-like Function-like set
{A} is non empty set
[:(proj1 x),{A}:] is Relation-like set
<:((proj1 x),A),x:> is Relation-like Function-like set
z is Relation-like Function-like set
<:((proj1 x),A),x:> * z is Relation-like Function-like set
z is Relation-like Function-like set
A is set
x is Relation-like Function-like set
(z,A,x) is set
proj1 x is set
((proj1 x),A) is Relation-like Function-like set
{A} is non empty set
[:(proj1 x),{A}:] is Relation-like set
<:((proj1 x),A),x:> is Relation-like Function-like set
<:((proj1 x),A),x:> * z is Relation-like Function-like set
A is Relation-like Function-like set
x is set
z is Relation-like Function-like set
(A,x,z) is Relation-like Function-like set
proj1 z is set
((proj1 z),x) is Relation-like Function-like set
{x} is non empty set
[:(proj1 z),{x}:] is Relation-like set
<:((proj1 z),x),z:> is Relation-like Function-like set
<:((proj1 z),x),z:> * A is Relation-like Function-like set
(A,((proj1 z),x),z) is Relation-like Function-like set
z is Relation-like Function-like set
A 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
((proj1 z),y) is Relation-like Function-like set
{y} is non empty set
[:(proj1 z),{y}:] is Relation-like set
<:((proj1 z),y),z:> is Relation-like Function-like set
<:((proj1 z),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 <:((proj1 z),y),z:> is set
proj1 ((proj1 z),y) is set
(proj1 ((proj1 z),y)) /\ (proj1 z) is set
((proj1 z),y) . x is set
A . ((((proj1 z),y) . x),(z . x)) is set
[(((proj1 z),y) . x),(z . x)] is V15() set
{(((proj1 z),y) . x),(z . x)} is non empty set
{(((proj1 z),y) . x)} is non empty set
{{(((proj1 z),y) . x),(z . x)},{(((proj1 z),y) . x)}} is non empty set
A . [(((proj1 z),y) . x),(z . x)] is set
z is Relation-like Function-like set
A is Relation-like Function-like set
x is set
z | x is Relation-like Function-like set
A | x is Relation-like Function-like set
y is Relation-like Function-like set
e is set
(y,e,z) is Relation-like Function-like set
proj1 z is set
((proj1 z),e) is Relation-like Function-like set
{e} is non empty set
[:(proj1 z),{e}:] is Relation-like set
<:((proj1 z),e),z:> is Relation-like Function-like set
<:((proj1 z),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
((proj1 A),e) is Relation-like Function-like set
[:(proj1 A),{e}:] is Relation-like set
<:((proj1 A),e),A:> is Relation-like Function-like set
<:((proj1 A),e),A:> * y is Relation-like Function-like set
(y,e,A) | x is Relation-like Function-like set
(proj1 z) /\ x is set
proj1 (z | x) is set
(proj1 A) /\ x is set
((proj1 z),e) | x is Relation-like Function-like set
(((proj1 A) /\ x),e) is Relation-like Function-like set
[:((proj1 A) /\ x),{e}:] is Relation-like set
((proj1 A),e) | x is Relation-like Function-like set
(y,((proj1 z),e),z) is Relation-like Function-like set
(y,((proj1 z),e),z) | x is Relation-like Function-like set
(y,((proj1 z),e),A) is Relation-like Function-like set
<:((proj1 z),e),A:> is Relation-like Function-like set
<:((proj1 z),e),A:> * y is Relation-like Function-like set
(y,((proj1 z),e),A) | x is Relation-like Function-like set
(y,((proj1 A),e),A) is Relation-like Function-like set
(y,((proj1 A),e),A) | x is Relation-like Function-like set
z is Relation-like Function-like set
A is Relation-like Function-like set
A * z is Relation-like Function-like set
x is Relation-like Function-like set
y is set
(x,y,z) is Relation-like Function-like set
proj1 z is set
((proj1 z),y) is Relation-like Function-like set
{y} is non empty set
[:(proj1 z),{y}:] is Relation-like set
<:((proj1 z),y),z:> is Relation-like Function-like set
<:((proj1 z),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 ((proj1 z),y) is set
A * ((proj1 z),y) is Relation-like Function-like set
proj1 (A * ((proj1 z),y)) is set
e is set
A . e is set
(A * ((proj1 z),y)) . e is set
((proj1 z),y) . (A . e) is set
(x,((proj1 z),y),z) is Relation-like Function-like set
A * (x,((proj1 z),y),z) is Relation-like Function-like set
(x,(A * ((proj1 z),y)),(A * z)) is Relation-like Function-like set
<:(A * ((proj1 z),y)),(A * z):> is Relation-like Function-like set
<:(A * ((proj1 z),y)),(A * z):> * x is Relation-like Function-like set
z is Relation-like Function-like set
A is set
id A is Relation-like A -defined A -valued Function-like one-to-one total V18(A,A) Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
z | A is Relation-like Function-like set
x is Relation-like Function-like set
y is set
(x,y,z) is Relation-like Function-like set
proj1 z is set
((proj1 z),y) is Relation-like Function-like set
{y} is non empty set
[:(proj1 z),{y}:] is Relation-like set
<:((proj1 z),y),z:> is Relation-like Function-like set
<:((proj1 z),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
(id A) * z is Relation-like A -defined 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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
e is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
(x,y,e) is Relation-like Function-like set
<:y,e:> is Relation-like Function-like set
<:y,e:> * x is Relation-like z -valued 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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
e is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
(x,y,e) is Relation-like Function-like set
<:y,e:> is Relation-like Function-like set
<:y,e:> * 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
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:]
<:y,e:> is Relation-like Function-like set
<:y,e:> * x is Relation-like z -valued Function-like set
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:]
<:y,e:> is Relation-like Function-like set
<:y,e:> * x is Relation-like z -valued Function-like set
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
id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]
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:]
<:(id z),e:> is Relation-like Function-like set
<:(id z),e:> * x is Relation-like z -valued Function-like set
(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
id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]
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:]
<:e,(id z):> is Relation-like Function-like set
<:e,(id z):> * x is Relation-like z -valued Function-like set
(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
id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]
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:]
<:y,y:> is Relation-like Function-like set
<: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,((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
id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]
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:]
<:(id z),y:> is Relation-like Function-like set
<:(id z),y:> * A is Relation-like z -valued Function-like set
(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
id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]
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:]
<:y,(id z):> is Relation-like Function-like set
<:y,(id z):> * A is Relation-like z -valued Function-like set
(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
id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]
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
[:z,{x}:] is Relation-like 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
[:z,{A}:] is Relation-like 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,{x}:] is Relation-like 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,{x}:] is Relation-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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
e is Element of z
(x,y,e) is Relation-like Function-like set
proj1 y is set
((proj1 y),e) is Relation-like Function-like set
{e} is non empty set
[:(proj1 y),{e}:] is Relation-like set
<:y,((proj1 y),e):> is Relation-like Function-like set
<:y,((proj1 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
g is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
<: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
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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
e is Element of z
(x,y,e) is Relation-like Function-like set
proj1 y is set
((proj1 y),e) is Relation-like Function-like set
{e} is non empty set
[:(proj1 y),{e}:] is Relation-like set
<:y,((proj1 y),e):> is Relation-like Function-like set
<:y,((proj1 y),e):> * 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
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 Element of 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:]
proj1 y is non empty set
((proj1 y),e) is Relation-like Function-like non empty set
{e} is non empty set
[:(proj1 y),{e}:] is Relation-like non empty set
<:y,((proj1 y),e):> is Relation-like Function-like set
<:y,((proj1 y),e):> * x is Relation-like z -valued Function-like set
g is Element of A
(z,A,x,y,e) . g is Element of z
y . g is Element of z
x . ((y . g),e) is Element of z
[(y . g),e] is V15() set
{(y . g),e} is non empty set
{(y . g)} is non empty set
{{(y . g),e},{(y . g)}} is non empty set
x . [(y . g),e] 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:]
g is Element of z
(z,A,x,e,g) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
proj1 e is non empty set
((proj1 e),g) is Relation-like Function-like non empty set
{g} is non empty set
[:(proj1 e),{g}:] is Relation-like non empty set
<:e,((proj1 e),g):> is Relation-like Function-like set
<:e,((proj1 e),g):> * x is Relation-like z -valued Function-like set
z is Element of A
y . z is Element of z
e . z is Element of z
x . ((e . z),g) is Element of z
[(e . z),g] is V15() set
{(e . z),g} is non empty set
{(e . z)} is non empty set
{{(e . z),g},{(e . z)}} is non empty set
x . [(e . z),g] is set
(z,A,x,e,g) . 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
id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]
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 Element of 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:]
proj1 (id z) is non empty set
((proj1 (id z)),e) is Relation-like Function-like non empty set
{e} is non empty set
[:(proj1 (id z)),{e}:] is Relation-like non empty set
<:(id z),((proj1 (id z)),e):> is Relation-like Function-like set
<:(id z),((proj1 (id z)),e):> * x is Relation-like z -valued Function-like set
(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:]
(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:]
proj1 y is non empty set
((proj1 y),e) is Relation-like Function-like non empty set
[:(proj1 y),{e}:] is Relation-like non empty set
<:y,((proj1 y),e):> is Relation-like Function-like set
<:y,((proj1 y),e):> * 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) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
proj1 ((id z) * y) is non empty set
((proj1 ((id z) * y)),e) is Relation-like Function-like non empty set
[:(proj1 ((id z) * y)),{e}:] is Relation-like non empty set
<:((id z) * y),((proj1 ((id z) * y)),e):> is Relation-like Function-like set
<:((id z) * y),((proj1 ((id z) * y)),e):> * 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
id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]
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
(z,z,A,(id z),x) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]
proj1 (id z) is non empty set
((proj1 (id z)),x) is Relation-like Function-like non empty set
{x} is non empty set
[:(proj1 (id z)),{x}:] is Relation-like non empty set
<:(id z),((proj1 (id z)),x):> is Relation-like Function-like set
<:(id z),((proj1 (id z)),x):> * A is Relation-like z -valued Function-like set
(z,z,A,(id z),x) . x is Element of z
A . (x,x) is Element of z
[x,x] is V15() set
{x,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),x) is Element of z
[((id z) . x),x] is V15() set
{((id z) . x),x} is non empty set
{((id z) . 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 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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
e is Element of z
(x,e,y) is Relation-like Function-like set
proj1 y is set
((proj1 y),e) is Relation-like Function-like set
{e} is non empty set
[:(proj1 y),{e}:] is Relation-like set
<:((proj1 y),e),y:> is Relation-like Function-like set
<:((proj1 y),e),y:> * 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
g is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
<:g,y:> 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 * <:g,y:> 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:]
y is Element of z
e is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
(x,y,e) is Relation-like Function-like set
proj1 e is set
((proj1 e),y) is Relation-like Function-like set
{y} is non empty set
[:(proj1 e),{y}:] is Relation-like set
<:((proj1 e),y),e:> is Relation-like Function-like set
<:((proj1 e),y),e:> * 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
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 Element of z
(z,A,x,e,y) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
proj1 y is non empty set
((proj1 y),e) is Relation-like Function-like non empty set
{e} is non empty set
[:(proj1 y),{e}:] is Relation-like non empty set
<:((proj1 y),e),y:> is Relation-like Function-like set
<:((proj1 y),e),y:> * x is Relation-like z -valued Function-like set
g is Element of A
(z,A,x,e,y) . g is Element of z
y . g is Element of z
x . (e,(y . g)) is Element of z
[e,(y . g)] is V15() set
{e,(y . g)} is non empty set
{{e,(y . g)},{e}} is non empty set
x . [e,(y . g)] is set
dom (z,A,x,e,y) 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:]
g is Element of z
(z,A,x,g,e) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
proj1 e is non empty set
((proj1 e),g) is Relation-like Function-like non empty set
{g} is non empty set
[:(proj1 e),{g}:] is Relation-like non empty set
<:((proj1 e),g),e:> is Relation-like Function-like set
<:((proj1 e),g),e:> * x is Relation-like z -valued Function-like set
z is Element of A
y . z is Element of z
e . z is Element of z
x . (g,(e . z)) is Element of z
[g,(e . z)] is V15() set
{g,(e . z)} is non empty set
{{g,(e . z)},{g}} is non empty set
x . [g,(e . z)] is set
(z,A,x,g,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
id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]
bool [: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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
e is Element of 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:]
proj1 (id z) is non empty set
((proj1 (id z)),e) is Relation-like Function-like non empty set
{e} is non empty set
[:(proj1 (id z)),{e}:] is Relation-like non empty set
<:((proj1 (id z)),e),(id z):> is Relation-like Function-like set
<:((proj1 (id z)),e),(id z):> * x is Relation-like z -valued Function-like set
(z,z,x,e,(id z)) * y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
(z,A,x,e,y) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
proj1 y is set
((proj1 y),e) is Relation-like Function-like set
[:(proj1 y),{e}:] is Relation-like set
<:((proj1 y),e),y:> is Relation-like Function-like set
<:((proj1 y),e),y:> * x is Relation-like z -valued Function-like set
(id z) * y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
(z,A,x,e,((id z) * y)) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
proj1 ((id z) * y) is set
((proj1 ((id z) * y)),e) is Relation-like Function-like set
[:(proj1 ((id z) * y)),{e}:] is Relation-like set
<:((proj1 ((id z) * y)),e),((id z) * y):> is Relation-like Function-like set
<:((proj1 ((id z) * y)),e),((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
id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]
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
(z,z,A,x,(id z)) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]
proj1 (id z) is non empty set
((proj1 (id z)),x) is Relation-like Function-like non empty set
{x} is non empty set
[:(proj1 (id z)),{x}:] is Relation-like non empty set
<:((proj1 (id z)),x),(id z):> is Relation-like Function-like set
<:((proj1 (id z)),x),(id z):> * A is Relation-like z -valued Function-like set
(z,z,A,x,(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,x},{x}} is non empty set
A . [x,x] is set
(id z) . x is Element of z
A . (x,((id z) . x)) is Element of z
[x,((id z) . x)] is V15() set
{x,((id z) . x)} is non empty set
{{x,((id z) . x)},{x}} is non empty set
A . [x,((id z) . x)] is set
z is non empty set
A is non empty set
x is non empty set
[:A,x:] is Relation-like non empty set
[:z,[:A,x:]:] is Relation-like non empty set
bool [:z,[:A,x:]:] is non empty set
y is Relation-like z -defined [:A,x:] -valued Function-like non empty total V18(z,[:A,x:]) Element of bool [:z,[:A,x:]:]
(y) is Relation-like Function-like set
e is Element of z
(y) . e is set
y . e is Element of [:A,x:]
(y . e) `2 is set
(y . e) `1 is set
[((y . e) `2),((y . e) `1)] is V15() set
{((y . e) `2),((y . e) `1)} is non empty set
{((y . e) `2)} is non empty set
{{((y . e) `2),((y . e) `1)},{((y . e) `2)}} is non empty set
dom y is non empty Element of bool z
bool z is non empty set
[((y . e) `1),((y . e) `2)] is V15() set
{((y . e) `1),((y . e) `2)} is non empty set
{((y . e) `1)} is non empty set
{{((y . e) `1),((y . e) `2)},{((y . e) `1)}} is non empty set
z is non empty set
A is non empty set
x is non empty set
[:A,x:] is Relation-like non empty set
[:z,[:A,x:]:] is Relation-like non empty set
bool [:z,[:A,x:]:] is non empty set
y is Relation-like z -defined [:A,x:] -valued Function-like non empty total V18(z,[:A,x:]) Element of bool [:z,[:A,x:]:]
proj2 y is Relation-like non empty set
bool [:A,x:] is non empty set
z is non empty set
A is non empty set
x is non empty set
[:A,x:] is Relation-like non empty set
[:z,[:A,x:]:] is Relation-like non empty set
bool [:z,[:A,x:]:] is non empty set
y is Relation-like z -defined [:A,x:] -valued Function-like non empty total V18(z,[:A,x:]) Element of bool [:z,[:A,x:]:]
(y) is Relation-like Function-like set
[:x,A:] is Relation-like non empty set
[:z,[:x,A:]:] is Relation-like non empty set
bool [:z,[:x,A:]:] is non empty set
proj2 (y) is set
e is set
proj1 (y) is set
g is set
(y) . g is set
dom y is non empty Element of bool z
bool z is non empty set
z is Element of z
y . z is Element of [:A,x:]
(y . z) `1 is set
(y . z) `2 is set
[((y . z) `1),((y . z) `2)] is V15() set
{((y . z) `1),((y . z) `2)} is non empty set
{((y . z) `1)} is non empty set
{{((y . z) `1),((y . z) `2)},{((y . z) `1)}} is non empty set
(y) . z is set
[((y . z) `2),((y . z) `1)] is V15() set
{((y . z) `2),((y . z) `1)} is non empty set
{((y . z) `2)} is non empty set
{{((y . z) `2),((y . z) `1)},{((y . z) `2)}} is non empty set
dom y is non empty Element of bool z
bool z is non empty set
proj1 (y) is set
z is non empty set
A is non empty set
x is non empty set
[:A,x:] is Relation-like non empty set
[:z,[:A,x:]:] is Relation-like non empty set
bool [:z,[:A,x:]:] is non empty set
y is Relation-like z -defined [:A,x:] -valued Function-like non empty total V18(z,[:A,x:]) Element of bool [:z,[:A,x:]:]
(z,A,x,y) is Relation-like z -defined [:x,A:] -valued Function-like non empty total V18(z,[:x,A:]) Element of bool [:z,[:x,A:]:]
[:x,A:] is Relation-like non empty set
[:z,[:x,A:]:] is Relation-like non empty set
bool [:z,[:x,A:]:] is non empty set
(z,x,A,(z,A,x,y)) is Relation-like x -defined A -valued non empty Element of bool [:x,A:]
bool [:x,A:] is non empty set
(z,A,x,y) is Relation-like A -defined x -valued non empty Element of bool [:A,x:]
bool [:A,x:] is non empty set
(z,A,x,y) ~ is Relation-like x -defined A -valued Element of bool [:x,A:]
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
dom (z,A,x,y) is non empty Element of bool z
bool z is non empty set
z is set
(z,A,x,y) . z is set
dom y is non empty Element of bool z
y . z is set
(z,x,A,(z,A,x,y)) is Relation-like z -defined [:A,x:] -valued Function-like non empty total V18(z,[:A,x:]) Element of bool [:z,[:A,x:]:]
(z,x,A,(z,A,x,y)) . z 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
[g,e] is V15() set
{g,e} is non empty set
{g} is non empty set
{{g,e},{g}} is non empty set
dom y is non empty Element of bool z
bool z is non empty set
z is set
y . z is set
dom (z,A,x,y) is non empty Element of bool z
(z,A,x,y) . z 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
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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
e is Element of z
(z,A,x,e,y) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
proj1 y is set
((proj1 y),e) is Relation-like Function-like set
{e} is non empty set
[:(proj1 y),{e}:] is Relation-like set
<:((proj1 y),e),y:> is Relation-like Function-like set
<:((proj1 y),e),y:> * x is Relation-like z -valued Function-like set
g is Element of z
(z,A,x,(z,A,x,e,y),g) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
proj1 (z,A,x,e,y) is set
((proj1 (z,A,x,e,y)),g) is Relation-like Function-like set
{g} is non empty set
[:(proj1 (z,A,x,e,y)),{g}:] is Relation-like set
<:(z,A,x,e,y),((proj1 (z,A,x,e,y)),g):> is Relation-like Function-like set
<:(z,A,x,e,y),((proj1 (z,A,x,e,y)),g):> * x is Relation-like z -valued Function-like set
(z,A,x,y,g) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
((proj1 y),g) is Relation-like Function-like set
[:(proj1 y),{g}:] is Relation-like set
<:y,((proj1 y),g):> is Relation-like Function-like set
<:y,((proj1 y),g):> * x is Relation-like z -valued Function-like set
(z,A,x,e,(z,A,x,y,g)) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
proj1 (z,A,x,y,g) is set
((proj1 (z,A,x,y,g)),e) is Relation-like Function-like set
[:(proj1 (z,A,x,y,g)),{e}:] is Relation-like set
<:((proj1 (z,A,x,y,g)),e),(z,A,x,y,g):> is Relation-like Function-like set
<:((proj1 (z,A,x,y,g)),e),(z,A,x,y,g):> * x is Relation-like z -valued Function-like set
z is Element of A
y . z is set
(z,A,x,(z,A,x,e,y),g) . z is set
(z,A,x,e,y) . z is set
x . (((z,A,x,e,y) . z),g) is set
[((z,A,x,e,y) . z),g] is V15() set
{((z,A,x,e,y) . z),g} is non empty set
{((z,A,x,e,y) . z)} is non empty set
{{((z,A,x,e,y) . z),g},{((z,A,x,e,y) . z)}} is non empty set
x . [((z,A,x,e,y) . z),g] is set
x1 is Element of z
x . (e,x1) is Element of z
[e,x1] is V15() set
{e,x1} is non empty set
{{e,x1},{e}} is non empty set
x . [e,x1] is set
x . ((x . (e,x1)),g) is Element of z
[(x . (e,x1)),g] is V15() set
{(x . (e,x1)),g} is non empty set
{(x . (e,x1))} is non empty set
{{(x . (e,x1)),g},{(x . (e,x1))}} is non empty set
x . [(x . (e,x1)),g] is set
x . (x1,g) is Element of z
[x1,g] is V15() set
{x1,g} is non empty set
{x1} is non empty set
{{x1,g},{x1}} is non empty set
x . [x1,g] is set
x . (e,(x . (x1,g))) is Element of z
[e,(x . (x1,g))] is V15() set
{e,(x . (x1,g))} is non empty set
{{e,(x . (x1,g))},{e}} is non empty set
x . [e,(x . (x1,g))] is set
(z,A,x,y,g) . z is set
x . (e,((z,A,x,y,g) . z)) is set
[e,((z,A,x,y,g) . z)] is V15() set
{e,((z,A,x,y,g) . z)} is non empty set
{{e,((z,A,x,y,g) . z)},{e}} is non empty set
x . [e,((z,A,x,y,g) . z)] 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
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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
e is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
g is Element of z
(z,A,x,y,g) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
proj1 y is set
((proj1 y),g) is Relation-like Function-like set
{g} is non empty set
[:(proj1 y),{g}:] is Relation-like set
<:y,((proj1 y),g):> is Relation-like Function-like set
<:y,((proj1 y),g):> * x is Relation-like z -valued Function-like set
(z,A,x,(z,A,x,y,g),e) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
<:(z,A,x,y,g),e:> is Relation-like Function-like set
<:(z,A,x,y,g),e:> * x is Relation-like z -valued Function-like set
(z,A,x,g,e) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
proj1 e is set
((proj1 e),g) is Relation-like Function-like set
[:(proj1 e),{g}:] is Relation-like set
<:((proj1 e),g),e:> is Relation-like Function-like set
<:((proj1 e),g),e:> * x is Relation-like z -valued Function-like set
(z,A,x,y,(z,A,x,g,e)) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
<:y,(z,A,x,g,e):> is Relation-like Function-like set
<:y,(z,A,x,g,e):> * x is Relation-like z -valued Function-like set
z is Element of A
y . z is set
e . z is set
(z,A,x,(z,A,x,y,g),e) . z is set
(z,A,x,y,g) . z is set
x . (((z,A,x,y,g) . z),(e . z)) is set
[((z,A,x,y,g) . z),(e . z)] is V15() set
{((z,A,x,y,g) . z),(e . z)} is non empty set
{((z,A,x,y,g) . z)} is non empty set
{{((z,A,x,y,g) . z),(e . z)},{((z,A,x,y,g) . z)}} is non empty set
x . [((z,A,x,y,g) . z),(e . z)] is set
x1 is Element of z
x . (x1,g) is Element of z
[x1,g] is V15() set
{x1,g} is non empty set
{x1} is non empty set
{{x1,g},{x1}} is non empty set
x . [x1,g] is set
x2 is Element of z
x . ((x . (x1,g)),x2) is Element of z
[(x . (x1,g)),x2] is V15() set
{(x . (x1,g)),x2} is non empty set
{(x . (x1,g))} is non empty set
{{(x . (x1,g)),x2},{(x . (x1,g))}} is non empty set
x . [(x . (x1,g)),x2] is set
x . (g,x2) is Element of z
[g,x2] is V15() set
{g,x2} is non empty set
{{g,x2},{g}} is non empty set
x . [g,x2] is set
x . (x1,(x . (g,x2))) is Element of z
[x1,(x . (g,x2))] is V15() set
{x1,(x . (g,x2))} is non empty set
{{x1,(x . (g,x2))},{x1}} is non empty set
x . [x1,(x . (g,x2))] is set
(z,A,x,g,e) . z is set
x . ((y . z),((z,A,x,g,e) . z)) is set
[(y . z),((z,A,x,g,e) . z)] is V15() set
{(y . z),((z,A,x,g,e) . z)} is non empty set
{(y . z)} is non empty set
{{(y . z),((z,A,x,g,e) . z)},{(y . z)}} is non empty set
x . [(y . z),((z,A,x,g,e) . z)] 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
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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
e is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
(z,A,x,y,e) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
<:y,e:> is Relation-like Function-like set
<:y,e:> * x is Relation-like z -valued Function-like set
g is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
(z,A,x,(z,A,x,y,e),g) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
<:(z,A,x,y,e),g:> is Relation-like Function-like set
<:(z,A,x,y,e),g:> * x is Relation-like z -valued Function-like set
(z,A,x,e,g) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
<:e,g:> is Relation-like Function-like set
<:e,g:> * x is Relation-like z -valued Function-like set
(z,A,x,y,(z,A,x,e,g)) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
<:y,(z,A,x,e,g):> is Relation-like Function-like set
<:y,(z,A,x,e,g):> * x is Relation-like z -valued Function-like set
z is Element of A
y . z is set
e . z is set
g . z is set
(z,A,x,(z,A,x,y,e),g) . z is set
(z,A,x,y,e) . z is set
x . (((z,A,x,y,e) . z),(g . z)) is set
[((z,A,x,y,e) . z),(g . z)] is V15() set
{((z,A,x,y,e) . z),(g . z)} is non empty set
{((z,A,x,y,e) . z)} is non empty set
{{((z,A,x,y,e) . z),(g . z)},{((z,A,x,y,e) . z)}} is non empty set
x . [((z,A,x,y,e) . z),(g . z)] is set
x . ((y . z),(e . z)) is set
[(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
x . ((x . ((y . z),(e . z))),(g . z)) is set
[(x . ((y . z),(e . z))),(g . z)] is V15() set
{(x . ((y . z),(e . z))),(g . z)} is non empty set
{(x . ((y . z),(e . z)))} is non empty set
{{(x . ((y . z),(e . z))),(g . z)},{(x . ((y . z),(e . z)))}} is non empty set
x . [(x . ((y . z),(e . z))),(g . z)] is set
x1 is Element of z
x2 is Element of z
x3 is Element of z
x . (x2,x3) is Element of z
[x2,x3] is V15() set
{x2,x3} is non empty set
{x2} is non empty set
{{x2,x3},{x2}} is non empty set
x . [x2,x3] is set
x . (x1,(x . (x2,x3))) is Element of z
[x1,(x . (x2,x3))] is V15() set
{x1,(x . (x2,x3))} is non empty set
{x1} is non empty set
{{x1,(x . (x2,x3))},{x1}} is non empty set
x . [x1,(x . (x2,x3))] is set
(z,A,x,e,g) . z is set
x . ((y . z),((z,A,x,e,g) . z)) is set
[(y . z),((z,A,x,e,g) . z)] is V15() set
{(y . z),((z,A,x,e,g) . z)} is non empty set
{{(y . z),((z,A,x,e,g) . z)},{(y . z)}} is non empty set
x . [(y . z),((z,A,x,e,g) . z)] 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
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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
e is Element of z
g is Element of z
x . (e,g) is Element of z
[e,g] is V15() set
{e,g} is non empty set
{e} is non empty set
{{e,g},{e}} is non empty set
x . [e,g] is set
(z,A,x,(x . (e,g)),y) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
proj1 y is set
((proj1 y),(x . (e,g))) is Relation-like Function-like set
{(x . (e,g))} is non empty set
[:(proj1 y),{(x . (e,g))}:] is Relation-like set
<:((proj1 y),(x . (e,g))),y:> is Relation-like Function-like set
<:((proj1 y),(x . (e,g))),y:> * x is Relation-like z -valued Function-like set
(z,A,x,g,y) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
((proj1 y),g) is Relation-like Function-like set
{g} is non empty set
[:(proj1 y),{g}:] is Relation-like set
<:((proj1 y),g),y:> is Relation-like Function-like set
<:((proj1 y),g),y:> * x is Relation-like z -valued Function-like set
(z,A,x,e,(z,A,x,g,y)) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
proj1 (z,A,x,g,y) is set
((proj1 (z,A,x,g,y)),e) is Relation-like Function-like set
[:(proj1 (z,A,x,g,y)),{e}:] is Relation-like set
<:((proj1 (z,A,x,g,y)),e),(z,A,x,g,y):> is Relation-like Function-like set
<:((proj1 (z,A,x,g,y)),e),(z,A,x,g,y):> * x is Relation-like z -valued Function-like set
z is Element of A
y . z is set
(z,A,x,(x . (e,g)),y) . z is set
x . ((x . (e,g)),(y . z)) is set
[(x . (e,g)),(y . z)] is V15() set
{(x . (e,g)),(y . z)} is non empty set
{{(x . (e,g)),(y . z)},{(x . (e,g))}} is non empty set
x . [(x . (e,g)),(y . z)] is set
x1 is Element of z
x . (g,x1) is Element of z
[g,x1] is V15() set
{g,x1} is non empty set
{{g,x1},{g}} is non empty set
x . [g,x1] is set
x . (e,(x . (g,x1))) is Element of z
[e,(x . (g,x1))] is V15() set
{e,(x . (g,x1))} is non empty set
{{e,(x . (g,x1))},{e}} is non empty set
x . [e,(x . (g,x1))] is set
(z,A,x,g,y) . z is set
x . (e,((z,A,x,g,y) . z)) is set
[e,((z,A,x,g,y) . z)] is V15() set
{e,((z,A,x,g,y) . z)} is non empty set
{{e,((z,A,x,g,y) . z)},{e}} is non empty set
x . [e,((z,A,x,g,y) . z)] 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
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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
e is Element of z
(z,A,x,y,e) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
proj1 y is set
((proj1 y),e) is Relation-like Function-like set
{e} is non empty set
[:(proj1 y),{e}:] is Relation-like set
<:y,((proj1 y),e):> is Relation-like Function-like set
<:y,((proj1 y),e):> * x is Relation-like z -valued Function-like set
g is Element of z
x . (e,g) is Element of z
[e,g] is V15() set
{e,g} is non empty set
{{e,g},{e}} is non empty set
x . [e,g] is set
(z,A,x,y,(x . (e,g))) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
((proj1 y),(x . (e,g))) is Relation-like Function-like set
{(x . (e,g))} is non empty set
[:(proj1 y),{(x . (e,g))}:] is Relation-like set
<:y,((proj1 y),(x . (e,g))):> is Relation-like Function-like set
<:y,((proj1 y),(x . (e,g))):> * x is Relation-like z -valued Function-like set
(z,A,x,(z,A,x,y,e),g) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
proj1 (z,A,x,y,e) is set
((proj1 (z,A,x,y,e)),g) is Relation-like Function-like set
{g} is non empty set
[:(proj1 (z,A,x,y,e)),{g}:] is Relation-like set
<:(z,A,x,y,e),((proj1 (z,A,x,y,e)),g):> is Relation-like Function-like set
<:(z,A,x,y,e),((proj1 (z,A,x,y,e)),g):> * x is Relation-like z -valued Function-like set
z is Element of A
y . z is set
(z,A,x,y,(x . (e,g))) . z is set
x . ((y . z),(x . (e,g))) is set
[(y . z),(x . (e,g))] is V15() set
{(y . z),(x . (e,g))} is non empty set
{(y . z)} is non empty set
{{(y . z),(x . (e,g))},{(y . z)}} is non empty set
x . [(y . z),(x . (e,g))] is set
x1 is Element of z
x . (x1,e) is Element of z
[x1,e] is V15() set
{x1,e} is non empty set
{x1} is non empty set
{{x1,e},{x1}} is non empty set
x . [x1,e] is set
x . ((x . (x1,e)),g) is Element of z
[(x . (x1,e)),g] is V15() set
{(x . (x1,e)),g} is non empty set
{(x . (x1,e))} is non empty set
{{(x . (x1,e)),g},{(x . (x1,e))}} is non empty set
x . [(x . (x1,e)),g] is set
(z,A,x,y,e) . z is set
x . (((z,A,x,y,e) . z),g) is set
[((z,A,x,y,e) . z),g] is V15() set
{((z,A,x,y,e) . z),g} is non empty set
{((z,A,x,y,e) . z)} is non empty set
{{((z,A,x,y,e) . z),g},{((z,A,x,y,e) . z)}} is non empty set
x . [((z,A,x,y,e) . z),g] 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
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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
e is Element of z
(z,A,x,e,y) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
proj1 y is set
((proj1 y),e) is Relation-like Function-like set
{e} is non empty set
[:(proj1 y),{e}:] is Relation-like set
<:((proj1 y),e),y:> is Relation-like Function-like set
<:((proj1 y),e),y:> * x is Relation-like z -valued Function-like set
(z,A,x,y,e) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
<:y,((proj1 y),e):> is Relation-like Function-like set
<:y,((proj1 y),e):> * x is Relation-like z -valued Function-like set
g is Element of A
y . g is set
(z,A,x,e,y) . g is set
z is Element of z
x . (e,z) is Element of z
[e,z] is V15() set
{e,z} is non empty set
{{e,z},{e}} is non empty set
x . [e,z] is set
x . ((y . g),e) is set
[(y . g),e] is V15() set
{(y . g),e} is non empty set
{(y . g)} is non empty set
{{(y . g),e},{(y . g)}} is non empty set
x . [(y . g),e] 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
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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
e is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
(z,A,x,y,e) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
<:y,e:> is Relation-like Function-like set
<:y,e:> * x is Relation-like z -valued Function-like set
(z,A,x,e,y) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
<:e,y:> is Relation-like Function-like set
<:e,y:> * x is Relation-like z -valued Function-like set
g is Element of A
y . g is set
e . g is set
(z,A,x,y,e) . g is set
z is Element of z
x1 is Element of z
x . (z,x1) is Element of z
[z,x1] is V15() set
{z,x1} is non empty set
{z} is non empty set
{{z,x1},{z}} is non empty set
x . [z,x1] is set
x . ((e . g),(y . g)) is set
[(e . g),(y . g)] is V15() set
{(e . g),(y . g)} is non empty set
{(e . g)} is non empty set
{{(e . g),(y . g)},{(e . g)}} is non empty set
x . [(e . g),(y . g)] 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
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:]
y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
(z,A,x,y,y) is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]
<:y,y:> is Relation-like Function-like set
<:y,y:> * x is Relation-like z -valued Function-like set
e is Element of A
y . e is set
g is Element of z
x . (g,g) is Element of z
[g,g] is V15() set
{g,g} is non empty set
{g} is non empty set
{{g,g},{g}} is non empty set
x . [g,g] is set
x . ((y . e),(y . e)) is set
[(y . e),(y . e)] is V15() set
{(y . e),(y . e)} is non empty set
{(y . e)} is non empty set
{{(y . e),(y . e)},{(y . e)}} is non empty set
x . [(y . e),(y . e)] 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
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 Element of A
y . e is Element of 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:]
proj1 y is non empty set
((proj1 y),(y . e)) is Relation-like Function-like non empty set
{(y . e)} is non empty set
[:(proj1 y),{(y . e)}:] is Relation-like non empty set
<:((proj1 y),(y . e)),y:> is Relation-like Function-like set
<:((proj1 y),(y . e)),y:> * x is Relation-like z -valued Function-like set
(z,A,x,(y . e),y) . e is Element of z
x . ((y . e),(y . e)) is Element of z
[(y . e),(y . e)] is V15() set
{(y . e),(y . e)} is non empty set
{{(y . e),(y . e)},{(y . e)}} is non empty set
x . [(y . e),(y . e)] 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
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 Element of A
y . e is Element of z
(z,A,x,y,(y . e)) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]
proj1 y is non empty set
((proj1 y),(y . e)) is Relation-like Function-like non empty set
{(y . e)} is non empty set
[:(proj1 y),{(y . e)}:] is Relation-like non empty set
<:y,((proj1 y),(y . e)):> is Relation-like Function-like set
<:y,((proj1 y),(y . e)):> * x is Relation-like z -valued Function-like set
(z,A,x,y,(y . e)) . e is Element of z
x . ((y . e),(y . e)) is Element of z
[(y . e),(y . e)] is V15() set
{(y . e),(y . e)} is non empty set
{{(y . e),(y . e)},{(y . e)}} is non empty set
x . [(y . e),(y . e)] is set
A is Relation-like Function-like set
proj2 A is set
x is Relation-like Function-like set
proj2 x is set
[:(proj2 A),(proj2 x):] is Relation-like set
z is Relation-like Function-like set
proj1 z is set
(z,A,x) is Relation-like Function-like set
<:A,x:> is Relation-like Function-like set
<:A,x:> * z is Relation-like Function-like set
proj1 (z,A,x) is set
proj1 A is set
proj1 x is set
(proj1 A) /\ (proj1 x) is set
proj2 <:A,x:> is set
proj1 <:A,x:> is set
the set is set
the Relation-like Function-like set is Relation-like Function-like set
( the set , the Relation-like Function-like set ) is Relation-like the set -defined { the Relation-like Function-like set } -valued Function-like total V18( the set ,{ the Relation-like Function-like set }) Element of bool [: the set ,{ the Relation-like Function-like set }:]
{ the Relation-like Function-like set } is functional non empty set
[: the set ,{ the Relation-like Function-like set }:] is Relation-like set
bool [: the set ,{ the Relation-like Function-like set }:] is non empty set
z is set
proj1 ( the set , the Relation-like Function-like set ) is set
( the set , the Relation-like Function-like set ) . z is Relation-like Function-like set
z is Relation-like Function-like () set
A is set
z . A is set
proj1 z is set
proj1 z is set
proj1 z is set
A is Relation-like Function-like set
z is Relation-like Function-like () set
A * z is Relation-like Function-like set
x is set
proj1 (A * z) is set
(A * z) . x is set
A . x is set
z . (A . x) is Relation-like Function-like set
z is set
A is non empty set
(z,A) is Relation-like z -defined {A} -valued Function-like total V18(z,{A}) Element of bool [:z,{A}:]
{A} is non empty set
[:z,{A}:] is Relation-like set
bool [:z,{A}:] is non empty set
rng (z,A) is Element of bool {A}
bool {A} is non empty set
z is set
{z} is non empty set
A is non empty set
x is non empty set
[:A,x:] is Relation-like non empty set
([:A,x:],z) is Relation-like [:A,x:] -defined {z} -valued Function-like non empty total V18([:A,x:],{z}) Element of bool [:[:A,x:],{z}:]
[:[:A,x:],{z}:] is Relation-like non empty set
bool [:[:A,x:],{z}:] is non empty set
y is Element of A
e is Element of x
([:A,x:],z) . (y,e) is Element of {z}
[y,e] is V15() set
{y,e} is non empty set
{y} is non empty set
{{y,e},{y}} is non empty set
([:A,x:],z) . [y,e] is set
z is set
A is set
[z,A] is V15() set
{z,A} is non empty set
{z} is non empty set
{{z,A},{z}} is non empty set
{[z,A]} is Relation-like Function-like non empty set
x is set
({[z,A]},x) is Relation-like {[z,A]} -defined {x} -valued Function-like non empty total V18({[z,A]},{x}) Element of bool [:{[z,A]},{x}:]
{x} is non empty set
[:{[z,A]},{x}:] is Relation-like non empty set
bool [:{[z,A]},{x}:] is non empty set
z is set
A is set
x is set
(z,A,x) is Relation-like Function-like set
[z,A] is V15() set
{z,A} is non empty set
{z} is non empty set
{{z,A},{z}} is non empty set
{[z,A]} is Relation-like Function-like non empty set
({[z,A]},x) is Relation-like {[z,A]} -defined {x} -valued Function-like non empty total V18({[z,A]},{x}) Element of bool [:{[z,A]},{x}:]
{x} is non empty set
[:{[z,A]},{x}:] is Relation-like non empty set
bool [:{[z,A]},{x}:] is non empty set
(z,A,x) . (z,A) is set
(z,A,x) . [z,A] is set
z is set
A is set
x is set
y is set
z is set
A is set
x is set
y is Element of z
e is Element of z
(A,x,y,e) is set
z is set
{z} is non empty set
A is set
({z},A) is Relation-like {z} -defined {A} -valued Function-like non empty total V18({z},{A}) Element of bool [:{z},{A}:]
{A} is non empty set
[:{z},{A}:] is Relation-like non empty set
bool [:{z},{A}:] is non empty set
z is set
A is set
(z,A) is set
{z} is non empty set
({z},A) is Relation-like {z} -defined {A} -valued Function-like non empty total V18({z},{A}) Element of bool [:{z},{A}:]
{A} is non empty set
[:{z},{A}:] is Relation-like non empty set
bool [:{z},{A}:] is non empty set
z is set
A is set
(z,A) is Relation-like Function-like set
{z} is non empty set
({z},A) is Relation-like {z} -defined {A} -valued Function-like non empty total V18({z},{A}) Element of bool [:{z},{A}:]
{A} is non empty set
[:{z},{A}:] is Relation-like non empty set
bool [:{z},{A}:] is non empty set
x is set
proj1 (z,A) is set
y is set
(z,A) . x is set
(z,A) . y is set
z is set
A is set
(z,A) is Relation-like Function-like one-to-one set
{z} is non empty set
({z},A) is Relation-like {z} -defined {A} -valued Function-like non empty total V18({z},{A}) Element of bool [:{z},{A}:]
{A} is non empty set
[:{z},{A}:] is Relation-like non empty set
bool [:{z},{A}:] is non empty set
(z,A) . z is set
z is set
A is set
(z,A) is Relation-like Function-like one-to-one set
{z} is non empty set
({z},A) is Relation-like {z} -defined {A} -valued Function-like non empty total V18({z},{A}) Element of bool [:{z},{A}:]
{A} is non empty set
[:{z},{A}:] is Relation-like non empty set
bool [:{z},{A}:] is non empty set
x is Relation-like Function-like set
proj1 x is set
x . z is set
proj1 (z,A) is set
(z,A) . z is set
y is set
(z,A) . y is set
x . y is set
z is set
A is set
x is set
(z,A,x) is Relation-like Function-like set
[z,A] is V15() set
{z,A} is non empty set
{z} is non empty set
{{z,A},{z}} is non empty set
{[z,A]} is Relation-like Function-like non empty set
({[z,A]},x) is Relation-like {[z,A]} -defined {x} -valued Function-like non empty total V18({[z,A]},{x}) Element of bool [:{[z,A]},{x}:]
{x} is non empty set
[:{[z,A]},{x}:] is Relation-like non empty set
bool [:{[z,A]},{x}:] is non empty set
{A} is non empty set
[:{z},{A}:] is Relation-like non empty set
[:[:{z},{A}:],{x}:] is Relation-like non empty set
bool [:[:{z},{A}:],{x}:] is non empty set
proj1 (z,A,x) is set
z is set
A is set
x is set
(z,A,x) is Relation-like Function-like set
[z,A] is V15() set
{z,A} is non empty set
{z} is non empty set
{{z,A},{z}} is non empty set
{[z,A]} is Relation-like Function-like non empty set
({[z,A]},x) is Relation-like {[z,A]} -defined {x} -valued Function-like non empty total V18({[z,A]},{x}) Element of bool [:{[z,A]},{x}:]
{x} is non empty set
[:{[z,A]},{x}:] is Relation-like non empty set
bool [:{[z,A]},{x}:] is non empty set
{A} is non empty set
[:{z},{A}:] is Relation-like non empty set
[:[:{z},{A}:],{x}:] is Relation-like non empty set
bool [:[:{z},{A}:],{x}:] is non empty set
y is Relation-like [:{z},{A}:] -defined {x} -valued Function-like non empty total V18([:{z},{A}:],{x}) Element of bool [:[:{z},{A}:],{x}:]
z is set
A is set
(z,A) is Relation-like Function-like one-to-one set
{z} is non empty set
({z},A) is Relation-like {z} -defined {A} -valued Function-like non empty total V18({z},{A}) Element of bool [:{z},{A}:]
{A} is non empty set
[:{z},{A}:] is Relation-like non empty set
bool [:{z},{A}:] is non empty set
proj1 (z,A) is set
z is set
A is set
x is set
(A,x) is Relation-like Function-like one-to-one set
{A} is non empty set
({A},x) is Relation-like {A} -defined {x} -valued Function-like non empty total V18({A},{x}) Element of bool [:{A},{x}:]
{x} is non empty set
[:{A},{x}:] is Relation-like non empty set
bool [:{A},{x}:] is non empty set
proj1 (A,x) is set
z is set
A is set
x is set
(A,x) is Relation-like Function-like one-to-one set
{A} is non empty set
({A},x) is Relation-like {A} -defined {x} -valued Function-like non empty total V18({A},{x}) Element of bool [:{A},{x}:]
{x} is non empty set
[:{A},{x}:] is Relation-like non empty set
bool [:{A},{x}:] is non empty set
(A,x) | z is Relation-like Function-like set
proj1 (A,x) is set
z is set
A is set
(z,A) is Relation-like Function-like one-to-one set
{z} is non empty set
({z},A) is Relation-like {z} -defined {A} -valued Function-like non empty total V18({z},{A}) Element of bool [:{z},{A}:]
{A} is non empty set
[:{z},{A}:] is Relation-like non empty set
bool [:{z},{A}:] is non empty set
z is set
{z} is non empty set
A is set
{A} is non empty set
x is set
{x} is non empty set
(z,A,x) is Relation-like [:{z},{A}:] -defined {x} -valued Function-like non empty total V18([:{z},{A}:],{x}) Element of bool [:[:{z},{A}:],{x}:]
[:{z},{A}:] is Relation-like non empty set
[:[:{z},{A}:],{x}:] is Relation-like non empty set
bool [:[:{z},{A}:],{x}:] is non empty set
[z,A] is V15() set
{z,A} is non empty set
{{z,A},{z}} is non empty set
{[z,A]} is Relation-like Function-like non empty set
({[z,A]},x) is Relation-like {[z,A]} -defined {x} -valued Function-like non empty total V18({[z,A]},{x}) Element of bool [:{[z,A]},{x}:]
[:{[z,A]},{x}:] is Relation-like non empty set
bool [:{[z,A]},{x}:] is non empty set
y is Element of {z}
e is Element of {A}
(z,A,x) . (y,e) is Element of {x}
[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) . [y,e] is set
z is Relation-like Function-like () set
A is set
z | A is Relation-like Function-like set
x is set
proj1 (z | A) is set
(z | A) . x is set
z . x is Relation-like Function-like set
z is set
A is Relation-like Function-like set
(z,A) is Relation-like z -defined {A} -valued Function-like total V18(z,{A}) Element of bool [:z,{A}:]
{A} is functional non empty set
[:z,{A}:] is Relation-like set
bool [:z,{A}:] is non empty set
x is set
proj1 (z,A) is set
(z,A) . x is Relation-like Function-like set
z is set
A is set
(z,A) is Relation-like z -defined {A} -valued Function-like total V18(z,{A}) Element of bool [:z,{A}:]
{A} is non empty set
[:z,{A}:] is Relation-like set
bool [:z,{A}:] is non empty set
x is set
proj1 (z,A) is set
y is set
(z,A) . x is set
(z,A) . y is set
dom (z,A) is Element of bool z
bool z is non empty set
{{}} is functional non empty set
({{}},{}) is Relation-like {{}} -defined {{}} -valued Function-like constant non empty total V18({{}},{{}}) () Element of bool [:{{}},{{}}:]
[:{{}},{{}}:] is Relation-like non empty set
bool [:{{}},{{}}:] is non empty set
z is Relation-like Function-like constant set
A is set
z | A is Relation-like Function-like set
x is set
proj1 (z | A) is set
y is set
(z | A) . x is set
(z | A) . y is set
proj1 z is set
z . x is set
z . y is set
z is Relation-like Function-like constant non empty set
proj1 z is non empty set
proj2 z is non empty trivial set
A is set
x is set
z . x is set
y is set
z . y is set
z is non empty set
A is set
(z,A) is Relation-like z -defined {A} -valued Function-like constant non empty total V18(z,{A}) Element of bool [:z,{A}:]
{A} is non empty set
[:z,{A}:] is Relation-like non empty set
bool [:z,{A}:] is non empty set
the_value_of (z,A) is set
dom (z,A) is non empty Element of bool z
bool z is non empty set
y is set
(z,A) . y is set
z is Relation-like Function-like constant set
proj1 z is set
the_value_of z is set
((proj1 z),(the_value_of z)) is Relation-like proj1 z -defined {(the_value_of z)} -valued Function-like constant total V18( proj1 z,{(the_value_of z)}) Element of bool [:(proj1 z),{(the_value_of z)}:]
{(the_value_of z)} is non empty set
[:(proj1 z),{(the_value_of z)}:] is Relation-like set
bool [:(proj1 z),{(the_value_of z)}:] is non empty set
dom ((proj1 z),(the_value_of z)) is Element of bool (proj1 z)
bool (proj1 z) is non empty set
A is set
z . A is set
((proj1 z),(the_value_of z)) . A is set
z is set
A is non empty set
[:z,A:] is Relation-like set
bool [:z,A:] is non empty set
x is set
y is Element of A
(A,z,y) is Relation-like z -defined A -valued Function-like constant total V18(z,A) Element of bool [:z,A:]
{y} is non empty set
[:z,{y}:] is Relation-like set
z is set
A is set
(z,A) is Relation-like z -defined {A} -valued Function-like constant total V18(z,{A}) Element of bool [:z,{A}:]
{A} is non empty set
[:z,{A}:] is Relation-like set
bool [:z,{A}:] is non empty set
z is set
{z} is non empty set
A is set
(z,A) is Relation-like Function-like one-to-one set
({z},A) is Relation-like {z} -defined {A} -valued Function-like constant non empty total V18({z},{A}) Element of bool [:{z},{A}:]
{A} is non empty set
[:{z},{A}:] is Relation-like non empty set
bool [:{z},{A}:] is non empty set
z is set
x is set
{x} is non empty set
(z,x) is Relation-like z -defined {x} -valued Function-like constant total V18(z,{x}) Element of bool [:z,{x}:]
[:z,{x}:] is Relation-like set
bool [:z,{x}:] is non empty set
A is set
(z,x) .: A is Element of bool {x}
bool {x} is non empty set
z is set
A is Relation-like Function-like set
(z,A) is Relation-like {z} -defined Function-like one-to-one set
{z} is non empty set
({z},A) is Relation-like {z} -defined {A} -valued Function-like constant non empty total V18({z},{A}) () Element of bool [:{z},{A}:]
{A} is functional non empty set
[:{z},{A}:] is Relation-like non empty set
bool [:{z},{A}:] is non empty set
z is set
(z,1) is Relation-like non-empty z -defined {1} -valued Function-like constant total V18(z,{1}) Element of bool [:z,{1}:]
{1} is non empty set
[:z,{1}:] is Relation-like set
bool [:z,{1}:] is non empty set
z is set
[z,z] is V15() set
{z,z} is non empty set
{z} is non empty set
{{z,z},{z}} is non empty set
{[z,z]} is Relation-like Function-like non empty set
A is set
[A,A] is V15() set
{A,A} is non empty set
{A} is non empty set
{{A,A},{A}} is non empty set
{[A,A]} is Relation-like Function-like non empty set
(z,A) is Relation-like {z} -defined Function-like one-to-one set
({z},A) is Relation-like {z} -defined {A} -valued Function-like constant non empty total V18({z},{A}) Element of bool [:{z},{A}:]
[:{z},{A}:] is Relation-like non empty set
bool [:{z},{A}:] is non empty set
field {[z,z]} is set
proj1 {[z,z]} is non empty set
proj2 {[z,z]} is non empty set
(proj1 {[z,z]}) \/ (proj2 {[z,z]}) is non empty set
dom (z,A) is Element of bool {z}
bool {z} is non empty set
proj2 (z,A) is set
field {[A,A]} is set
proj1 {[A,A]} is non empty set
proj2 {[A,A]} is non empty set
(proj1 {[A,A]}) \/ (proj2 {[A,A]}) 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) . g is set
(z,A) . z is set
[((z,A) . g),((z,A) . z)] is V15() set
{((z,A) . g),((z,A) . z)} is non empty set
{((z,A) . g)} is non empty set
{{((z,A) . g),((z,A) . z)},{((z,A) . g)}} is non empty set
(z,A) . z is set
z is set
[z,z] is V15() set
{z,z} is non empty set
{z} is non empty set
{{z,z},{z}} is non empty set
{[z,z]} is Relation-like Function-like non empty set
A is set
[A,A] is V15() set
{A,A} is non empty set
{A} is non empty set
{{A,A},{A}} is non empty set
{[A,A]} is Relation-like Function-like non empty set
(z,A) is Relation-like {z} -defined Function-like one-to-one set
({z},A) is Relation-like {z} -defined {A} -valued Function-like constant non empty total V18({z},{A}) Element of bool [:{z},{A}:]
[:{z},{A}:] is Relation-like non empty set
bool [:{z},{A}:] is non empty set
z is set
A is set
(z,A) is Relation-like z -defined {A} -valued Function-like constant total V18(z,{A}) Element of bool [:z,{A}:]
{A} is non empty set
[:z,{A}:] is Relation-like set
bool [:z,{A}:] is non empty set
x is Relation-like z -defined Function-like set
z is set
A is Relation-like Function-like set
proj1 A is set
A . z is set
(z,(A . z)) is Relation-like {z} -defined Function-like one-to-one set
{z} is non empty set
({z},(A . z)) is Relation-like {z} -defined {(A . z)} -valued Function-like constant non empty total V18({z},{(A . z)}) Element of bool [:{z},{(A . z)}:]
{(A . z)} is non empty set
[:{z},{(A . z)}:] is Relation-like non empty set
bool [:{z},{(A . z)}:] is non empty set
[z,(A . z)] is V15() set
{z,(A . z)} is non empty set
{{z,(A . z)},{z}} is non empty set
{[z,(A . z)]} is Relation-like Function-like non empty set
z is non empty set
A is set
x is Element of z
(A,x) is Relation-like {A} -defined Function-like one-to-one set
{A} is non empty set
({A},x) is Relation-like {A} -defined {x} -valued Function-like constant non empty total V18({A},{x}) Element of bool [:{A},{x}:]
{x} is non empty set
[:{A},{x}:] is Relation-like non empty set
bool [:{A},{x}:] is non empty set
proj2 (A,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
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 set
[:x,z:] is Relation-like set
bool [:x,z:] is non empty set
y is Relation-like x -defined z -valued Function-like total V18(x,z) Element of bool [:x,z:]
e is Relation-like x -defined z -valued Function-like total V18(x,z) Element of bool [:x,z:]
(z,x,A,y,e) is Relation-like x -defined z -valued Function-like total V18(x,z) Element of bool [:x,z:]
<:y,e:> is Relation-like Function-like set
<:y,e:> * A is Relation-like z -valued Function-like set
g is Element of z
(z,x,A,g,y) is Relation-like x -defined z -valued Function-like total V18(x,z) Element of bool [:x,z:]
proj1 y is set
((proj1 y),g) is Relation-like proj1 y -defined Function-like constant total set
{g} is non empty set
[:(proj1 y),{g}:] is Relation-like set
<:((proj1 y),g),y:> is Relation-like Function-like set
<:((proj1 y),g),y:> * A is Relation-like z -valued Function-like set
(z,x,A,(z,x,A,g,y),e) is Relation-like x -defined z -valued Function-like total V18(x,z) Element of bool [:x,z:]
<:(z,x,A,g,y),e:> is Relation-like Function-like set
<:(z,x,A,g,y),e:> * A is Relation-like z -valued Function-like set
(z,x,A,g,(z,x,A,y,e)) is Relation-like x -defined z -valued Function-like total V18(x,z) Element of bool [:x,z:]
proj1 (z,x,A,y,e) is set
((proj1 (z,x,A,y,e)),g) is Relation-like proj1 (z,x,A,y,e) -defined Function-like constant total set
[:(proj1 (z,x,A,y,e)),{g}:] is Relation-like set
<:((proj1 (z,x,A,y,e)),g),(z,x,A,y,e):> is Relation-like Function-like set
<:((proj1 (z,x,A,y,e)),g),(z,x,A,y,e):> * A is Relation-like z -valued Function-like set
z is Element of x
y . z is set
e . z is set
(z,x,A,g,(z,x,A,y,e)) . z is set
(z,x,A,y,e) . z is set
A . (g,((z,x,A,y,e) . z)) is set
[g,((z,x,A,y,e) . z)] is V15() set
{g,((z,x,A,y,e) . z)} is non empty set
{{g,((z,x,A,y,e) . z)},{g}} is non empty set
A . [g,((z,x,A,y,e) . z)] is set
x1 is Element of z
x2 is Element of z
A . (x1,x2) is Element of z
[x1,x2] is V15() set
{x1,x2} is non empty set
{x1} is non empty set
{{x1,x2},{x1}} is non empty set
A . [x1,x2] is set
A . (g,(A . (x1,x2))) is Element of z
[g,(A . (x1,x2))] is V15() set
{g,(A . (x1,x2))} is non empty set
{{g,(A . (x1,x2))},{g}} is non empty set
A . [g,(A . (x1,x2))] is set
A . (g,x1) is Element of z
[g,x1] is V15() set
{g,x1} is non empty set
{{g,x1},{g}} is non empty set
A . [g,x1] is set
A . ((A . (g,x1)),x2) is Element of z
[(A . (g,x1)),x2] is V15() set
{(A . (g,x1)),x2} is non empty set
{(A . (g,x1))} is non empty set
{{(A . (g,x1)),x2},{(A . (g,x1))}} is non empty set
A . [(A . (g,x1)),x2] is set
(z,x,A,g,y) . z is set
A . (((z,x,A,g,y) . z),(e . z)) is set
[((z,x,A,g,y) . z),(e . z)] is V15() set
{((z,x,A,g,y) . z),(e . z)} is non empty set
{((z,x,A,g,y) . z)} is non empty set
{{((z,x,A,g,y) . z),(e . z)},{((z,x,A,g,y) . z)}} is non empty set
A . [((z,x,A,g,y) . z),(e . z)] is 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 constant 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,{x}:] is Relation-like set
z is non empty set
A is Element of z
x is set
(A,x) is Relation-like {A} -defined Function-like one-to-one set
{A} is non empty set
({A},x) is Relation-like {A} -defined {x} -valued Function-like constant non empty total V18({A},{x}) Element of bool [:{A},{x}:]
{x} is non empty set
[:{A},{x}:] is Relation-like non empty set
bool [:{A},{x}:] is non empty set
dom (A,x) is Element of bool {A}
bool {A} is non empty set
z is set
x is set
A is set
(z,A) is Relation-like {z} -defined Function-like one-to-one set
{z} is non empty set
({z},A) is Relation-like {z} -defined {A} -valued Function-like constant non empty total V18({z},{A}) Element of bool [:{z},{A}:]
{A} is non empty set
[:{z},{A}:] is Relation-like non empty set
bool [:{z},{A}:] is non empty set
(z,A) | x is Relation-like x -defined {z} -defined Function-like set
dom (z,A) is Element of bool {z}
bool {z} is non empty set
z is functional set
A is Relation-like Function-like set
x is set
proj1 A is set
A . x is set
z is Relation-like Function-like set
A is set
proj1 z is set
z . A is set
z is Relation-like Function-like set
A is set
proj1 z is set
z . A is set
z is set
x is set
(z,x) is Relation-like z -defined {x} -valued Function-like constant total V18(z,{x}) Element of bool [:z,{x}:]
{x} is non empty set
[:z,{x}:] is Relation-like set
bool [:z,{x}:] is non empty set
A is set
y is set
(A,y) is Relation-like A -defined {y} -valued Function-like constant total V18(A,{y}) Element of bool [:A,{y}:]
{y} is non empty set
[:A,{y}:] is Relation-like set
bool [:A,{y}:] is non empty set
dom (A,y) is Element of bool A
bool A is non empty set
dom (z,x) is Element of bool z
bool z is non empty set
(dom (z,x)) /\ (dom (A,y)) is Element of bool A
z is set
(z,x) . z is set
(A,y) . z is set
z /\ A is set
z is set
proj1 (z,x) is set
proj1 (A,y) is set
(proj1 (z,x)) /\ (proj1 (A,y)) is set
(z,x) . z is set
(A,y) . z is set
(dom (z,x)) /\ (dom (A,y)) is Element of bool A
z is set
A is set
(z,A) is Relation-like {z} -defined Function-like one-to-one set
{z} is non empty set
({z},A) is Relation-like {z} -defined {A} -valued Function-like constant non empty total V18({z},{A}) Element of bool [:{z},{A}:]
{A} is non empty set
[:{z},{A}:] is Relation-like non empty set
bool [:{z},{A}:] is non empty set
proj2 (z,A) is set
dom (z,A) is Element of bool {z}
bool {z} is non empty set
(z,A) . z is set
{((z,A) . z)} is non empty set
z is set
A is set
x is set
(A,x) is Relation-like A -defined {x} -valued Function-like constant total V18(A,{x}) Element of bool [:A,{x}:]
{x} is non empty set
[:A,{x}:] is Relation-like set
bool [:A,{x}:] is non empty set
y is set
(y,z) is Relation-like {y} -defined Function-like one-to-one set
{y} is non empty set
({y},z) is Relation-like {y} -defined {z} -valued Function-like constant non empty total V18({y},{z}) Element of bool [:{y},{z}:]
{z} is non empty set
[:{y},{z}:] is Relation-like non empty set
bool [:{y},{z}:] is non empty set
(y,z) * (A,x) is Relation-like {y} -defined {x} -valued Function-like set
(y,x) is Relation-like {y} -defined Function-like one-to-one set
({y},x) is Relation-like {y} -defined {x} -valued Function-like constant non empty total V18({y},{x}) Element of bool [:{y},{x}:]
[:{y},{x}:] is Relation-like non empty set
bool [:{y},{x}:] is non empty set
dom (y,z) is Element of bool {y}
bool {y} is non empty set
dom (y,x) is Element of bool {y}
proj2 (y,z) is set
dom (A,x) is Element of bool A
bool A is non empty set
dom ((y,z) * (A,x)) is Element of bool {y}
proj1 ((y,z) * (A,x)) is set
e is set
((y,z) * (A,x)) . e is set
(y,x) . e is set
(y,z) . e is set
(A,x) . ((y,z) . e) is set
(A,x) . z is set