:: 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 [:[: