:: FUNCT_1 semantic presentation

{} is empty trivial Relation-like non-empty empty-yielding set
the empty trivial Relation-like non-empty empty-yielding set is empty trivial Relation-like non-empty empty-yielding set
f is set
x is set
F is set
[x,F] is non empty set
{x,F} is non empty set
{x} is non empty trivial set
{{x,F},{x}} is non empty set
f is set
[x,f] is non empty set
{x,f} is non empty set
{{x,f},{x}} is non empty set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
{[f,x]} is non empty trivial Relation-like set
{x} is non empty trivial set
[:{f},{x}:] is Relation-like set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
y is set
[f,y] is non empty set
{f,y} is non empty set
{{f,y},{f}} is non empty set
F₁() is set
f is set
[:F₁(),f:] is Relation-like set
x is set
F is set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
F is set
f is set
[F,f] is non empty set
{F,f} is non empty set
{F} is non empty trivial set
{{F,f},{F}} is non empty set
y is set
g is set
[y,g] is non empty set
{y,g} is non empty set
{y} is non empty trivial set
{{y,g},{y}} is non empty set
x is set
[F,x] is non empty set
{F,x} is non empty set
{{F,x},{F}} is non empty set
x is set
Z is set
[x,Z] is non empty set
{x,Z} is non empty set
{x} is non empty trivial set
{{x,Z},{x}} is non empty set
F is Relation-like () set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
y is set
g is set
[y,g] is non empty set
{y,g} is non empty set
{y} is non empty trivial set
{{y,g},{y}} is non empty set
x is set
f is Relation-like () set
dom f is set
F is set
[x,F] is non empty set
{x,F} is non empty set
{x} is non empty trivial set
{{x,F},{x}} is non empty set
f is set
[x,f] is non empty set
{x,f} is non empty set
{{x,f},{x}} is non empty set
x is set
y is set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
F is Relation-like () set
dom F is set
(F,f) is set
f is Relation-like () set
dom f is set
x is Relation-like () set
dom x is set
F is set
f is set
[F,f] is non empty set
{F,f} is non empty set
{F} is non empty trivial set
{{F,f},{F}} is non empty set
(f,F) is set
(x,F) is set
(x,F) is set
(f,F) is set
f is Relation-like () set
rng f is set
dom f is set
x is set
F is set
f is set
[f,F] is non empty set
{f,F} is non empty set
{f} is non empty trivial set
{{f,F},{f}} is non empty set
x is set
(f,x) is set
f is set
(f,f) is set
[f,F] is non empty set
{f,F} is non empty set
{f} is non empty trivial set
{{f,F},{f}} is non empty set
F is set
f is set
(f,f) is set
[f,F] is non empty set
{f,F} is non empty set
{f} is non empty trivial set
{{f,F},{f}} is non empty set
F is set
f is set
[f,F] is non empty set
{f,F} is non empty set
{f} is non empty trivial set
{{f,F},{f}} is non empty set
(f,f) is set
f is set
x is Relation-like () set
dom x is set
(x,f) is set
rng x is set
f is set
{f} is non empty trivial set
x is Relation-like () set
dom x is set
rng x is set
(x,f) is set
{(x,f)} is non empty trivial set
F is set
f is set
(x,f) is set
F₁() is set
f is set
x is set
F is set
f is Relation-like () set
dom f is set
x is set
F is set
[x,F] is non empty set
{x,F} is non empty set
{x} is non empty trivial set
{{x,F},{x}} is non empty set
F is set
[x,F] is non empty set
{x,F} is non empty set
{x} is non empty trivial set
{{x,F},{x}} is non empty set
x is set
(f,x) is set
F is set
[x,F] is non empty set
{x,F} is non empty set
{x} is non empty trivial set
{{x,F},{x}} is non empty set
F₁() is set
f is set
F₂(f) is set
f is set
x is set
F₂(f) is set
F is set
f is set
x is set
{x} is non empty trivial set
F is Relation-like () set
dom F is set
rng F is set
f is set
the Element of f is Element of f
(F, the Element of f) is set
x is set
(F,x) is set
f is set
the Element of f is Element of f
F is Relation-like () set
dom F is set
(F, the Element of f) is set
1 is non empty set
f is Relation-like () set
dom f is set
(f, the Element of f) is set
f is set
{f} is non empty trivial set
x is Relation-like () set
dom x is set
rng x is set
F is Relation-like () set
dom F is set
rng F is set
f is set
(x,f) is set
(F,f) is set
f is set
x is set
the Element of f is Element of f
f is Relation-like () set
dom f is set
x is Relation-like () set
dom x is set
rng x is set
y is set
g is set
(x,g) is set
F is empty trivial Relation-like non-empty empty-yielding () set
dom F is empty trivial Relation-like non-empty empty-yielding () set
rng F is empty trivial Relation-like non-empty empty-yielding () set
F is empty trivial Relation-like non-empty empty-yielding () set
dom F is empty trivial Relation-like non-empty empty-yielding () set
rng F is empty trivial Relation-like non-empty empty-yielding () set
f is Relation-like () set
dom f is set
rng f is set
f is set
x is Relation-like () set
dom x is set
rng x is set
F is set
f is set
(x,f) is set
f is Relation-like () set
x is Relation-like () set
f * x is Relation-like set
F is set
f is set
[F,f] is non empty set
{F,f} is non empty set
{F} is non empty trivial set
{{F,f},{F}} is non empty set
x is set
[F,x] is non empty set
{F,x} is non empty set
{{F,x},{F}} is non empty set
y is set
[F,y] is non empty set
{F,y} is non empty set
{{F,y},{F}} is non empty set
[y,f] is non empty set
{y,f} is non empty set
{y} is non empty trivial set
{{y,f},{y}} is non empty set
g is set
[F,g] is non empty set
{F,g} is non empty set
{{F,g},{F}} is non empty set
[g,x] is non empty set
{g,x} is non empty set
{g} is non empty trivial set
{{g,x},{g}} is non empty set
f is Relation-like () set
dom f is set
x is Relation-like () set
dom x is set
f * x is Relation-like () set
F is Relation-like () set
dom F is set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
(f,f) is set
y is set
[f,y] is non empty set
{f,y} is non empty set
{{f,y},{f}} is non empty set
(F,f) is set
(x,(f,f)) is set
[y,x] is non empty set
{y,x} is non empty set
{y} is non empty trivial set
{{y,x},{y}} is non empty set
y is set
[f,y] is non empty set
{f,y} is non empty set
{{f,y},{f}} is non empty set
[y,x] is non empty set
{y,x} is non empty set
{y} is non empty trivial set
{{y,x},{y}} is non empty set
(x,y) is set
f is set
x is Relation-like () set
dom x is set
F is Relation-like () set
F * x is Relation-like () set
dom (F * x) is set
dom F is set
(F,f) is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
y is set
[f,y] is non empty set
{f,y} is non empty set
{{f,y},{f}} is non empty set
[y,x] is non empty set
{y,x} is non empty set
{y} is non empty trivial set
{{y,x},{y}} is non empty set
x is set
[f,x] is non empty set
{f,x} is non empty set
{{f,x},{f}} is non empty set
y is set
[(F,f),y] is non empty set
{(F,f),y} is non empty set
{(F,f)} is non empty trivial set
{{(F,f),y},{(F,f)}} is non empty set
[f,y] is non empty set
{f,y} is non empty set
{{f,y},{f}} is non empty set
f is set
x is Relation-like () set
F is Relation-like () set
F * x is Relation-like () set
dom (F * x) is set
((F * x),f) is set
(F,f) is set
(x,(F,f)) is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
y is set
[f,y] is non empty set
{f,y} is non empty set
{{f,y},{f}} is non empty set
[y,x] is non empty set
{y,x} is non empty set
{y} is non empty trivial set
{{y,x},{y}} is non empty set
dom F is set
dom x is set
f is set
x is Relation-like () set
dom x is set
(x,f) is set
F is Relation-like () set
x * F is Relation-like () set
((x * F),f) is set
(F,(x,f)) is set
dom F is set
dom (x * F) is set
dom F is set
dom (x * F) is set
dom F is set
f is set
x is Relation-like () set
rng x is set
F is Relation-like () set
F * x is Relation-like () set
rng (F * x) is set
dom (F * x) is set
f is set
((F * x),f) is set
(F,f) is set
dom x is set
(x,(F,f)) is set
f is Relation-like () set
dom f is set
x is Relation-like () set
x * f is Relation-like () set
dom (x * f) is set
dom x is set
rng x is set
F is set
f is set
(x,f) is set
f is set
x is Relation-like () set
rng x is set
F is set
1 is non empty set
f is set
x is set
f is set
x is set
y is set
f is Relation-like () set
dom f is set
x * f is Relation-like () set
dom (x * f) is set
dom x is set
x is Relation-like () set
dom x is set
x * x is Relation-like () set
dom (x * x) is set
y is set
((x * x),y) is set
((x * f),y) is set
(x,y) is set
(x,(x,y)) is set
(f,(x,y)) is set
(x,F) is set
f is set
id f is Relation-like f -defined f -valued set
x is set
F is set
[x,F] is non empty set
{x,F} is non empty set
{x} is non empty trivial set
{{x,F},{x}} is non empty set
f is set
[x,f] is non empty set
{x,f} is non empty set
{{x,f},{x}} is non empty set
f is set
id f is Relation-like f -defined f -valued () set
x is Relation-like () set
dom x is set
F is set
[F,F] is non empty set
{F,F} is non empty set
{F} is non empty trivial set
{{F,F},{F}} is non empty set
(x,F) is set
F is set
f is set
[F,f] is non empty set
{F,f} is non empty set
{F} is non empty trivial set
{{F,f},{F}} is non empty set
(x,F) is set
f is set
x is set
id x is Relation-like x -defined x -valued () set
((id x),f) is set
f is set
id f is Relation-like f -defined f -valued () set
x is Relation-like () set
(id f) * x is Relation-like f -defined () set
dom ((id f) * x) is set
dom x is set
(dom x) /\ f is set
F is set
dom (id f) is set
((id f),F) is set
dom (id f) is set
((id f),F) is set
f is set
x is set
id x is Relation-like x -defined x -valued () set
F is Relation-like () set
dom F is set
(dom F) /\ x is set
(F,f) is set
(id x) * F is Relation-like x -defined () set
(((id x) * F),f) is set
((id x),f) is set
dom (id x) is set
f is set
x is set
id x is Relation-like x -defined x -valued () set
F is Relation-like () set
F * (id x) is Relation-like x -valued () set
dom (F * (id x)) is set
dom F is set
(F,f) is set
dom (id x) is set
f is set
id f is Relation-like f -defined f -valued () set
x is set
id x is Relation-like x -defined x -valued () set
(id x) * (id f) is Relation-like x -defined f -valued () set
f /\ x is set
id (f /\ x) is Relation-like f /\ x -defined f /\ x -valued () set
dom ((id x) * (id f)) is set
dom (id f) is set
(dom (id f)) /\ x is set
F is set
(((id x) * (id f)),F) is set
((id (f /\ x)),F) is set
((id x),F) is set
((id f),((id x),F)) is set
((id f),F) is set
dom (id (f /\ x)) is set
f is Relation-like () set
rng f is set
x is Relation-like () set
dom x is set
f * x is Relation-like () set
id (dom x) is Relation-like dom x -defined dom x -valued () set
f is set
(x,f) is set
dom f is set
x is set
(f,x) is set
f is Relation-like () set
x is Relation-like () set
f * x is Relation-like () set
F is set
dom (f * x) is set
f is set
((f * x),F) is set
(f,F) is set
(x,(f,F)) is set
((f * x),f) is set
(f,f) is set
(x,(f,f)) is set
dom f is set
dom x is set
f is Relation-like () set
dom f is set
x is Relation-like () set
x * f is Relation-like () set
rng x is set
F is set
dom x is set
f is set
(x,F) is set
(x,f) is set
dom (x * f) is set
((x * f),F) is set
(f,(x,F)) is set
((x * f),f) is set
(f,(x,f)) is set
f is Relation-like () set
dom f is set
x is Relation-like () set
x * f is Relation-like () set
rng x is set
dom (x * f) is set
dom x is set
F is set
f is set
(f,F) is set
(f,f) is set
x is set
(x,x) is set
((x * f),x) is set
(f,(x,x)) is set
y is set
(x,y) is set
((x * f),y) is set
(f,(x,y)) is set
f is Relation-like () set
dom f is set
x is Relation-like () set
rng x is set
dom x is set
x * f is Relation-like () set
F is Relation-like () set
rng F is set
dom F is set
F * f is Relation-like () set
f is set
(x,f) is set
(F,f) is set
((x * f),f) is set
(f,(x,f)) is set
((F * f),f) is set
(f,(F,f)) is set
x is set
(f,x) is set
F is set
(f,F) is set
{{}} is non empty trivial set
f is Relation-like () set
dom f is set
(f,{}) is set
rng f is set
{x} is non empty trivial set
f * f is Relation-like () set
dom (f * f) is set
x is Relation-like () set
dom x is set
(x,{}) is set
rng x is set
{F} is non empty trivial set
x * f is Relation-like () set
dom (x * f) is set
y is set
((f * f),y) is set
((x * f),y) is set
(f,y) is set
(f,(f,y)) is set
(x,y) is set
(f,(x,y)) is set
f is set
id f is Relation-like f -defined f -valued () set
x is Relation-like () set
dom x is set
F is Relation-like () set
dom F is set
rng F is set
F * x is Relation-like () set
f is set
(F,f) is set
(x,f) is set
(x,(F,f)) is set
f is Relation-like () set
rng f is set
dom f is set
x is Relation-like () set
x * f is Relation-like () set
rng (x * f) is set
rng x is set
F is set
(f,F) is set
dom (x * f) is set
f is set
((x * f),f) is set
(x,f) is set
(f,(x,f)) is set
dom x is set
f is set
id f is Relation-like f -defined f -valued () set
x is set
dom (id f) is set
((id f),x) is set
F is set
((id f),F) is set
f is Relation-like () set
dom f is set
id (dom f) is Relation-like dom f -defined dom f -valued () () set
x is Relation-like () set
f * x is Relation-like () set
dom (f * x) is set
rng f is set
dom x is set
f is Relation-like () set
x is set
dom f is set
(f,x) is set
F is set
(f,F) is set
f is Relation-like () () set
f ~ is Relation-like set
x is set
F is set
[x,F] is non empty set
{x,F} is non empty set
{x} is non empty trivial set
{{x,F},{x}} is non empty set
f is set
[x,f] is non empty set
{x,f} is non empty set
{{x,f},{x}} is non empty set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
dom f is set
(f,f) is set
[F,x] is non empty set
{F,x} is non empty set
{F} is non empty trivial set
{{F,x},{F}} is non empty set
(f,F) is set
f is Relation-like () set
f ~ is Relation-like set
f is Relation-like () set
(f) is Relation-like () set
rng f is set
dom f is set
x is Relation-like () set
dom x is set
f ~ is Relation-like set
F is set
(x,F) is set
f is set
(f,f) is set
[F,f] is non empty set
{F,f} is non empty set
{F} is non empty trivial set
{{F,f},{F}} is non empty set
[f,F] is non empty set
{f,F} is non empty set
{f} is non empty trivial set
{{f,F},{f}} is non empty set
[f,F] is non empty set
{f,F} is non empty set
{f} is non empty trivial set
{{f,F},{f}} is non empty set
[F,f] is non empty set
{F,f} is non empty set
{F} is non empty trivial set
{{F,f},{F}} is non empty set
F is set
f is set
[F,f] is non empty set
{F,f} is non empty set
{F} is non empty trivial set
{{F,f},{F}} is non empty set
(x,F) is set
(f,f) is set
[f,F] is non empty set
{f,F} is non empty set
{f} is non empty trivial set
{{f,F},{f}} is non empty set
f ~ is Relation-like set
f ~ is Relation-like set
[f,F] is non empty set
{f,F} is non empty set
{f} is non empty trivial set
{{f,F},{f}} is non empty set
(f,f) is set
(x,F) is set
f is Relation-like () set
rng f is set
(f) is Relation-like () set
dom (f) is set
dom f is set
rng (f) is set
f ~ is Relation-like set
f is set
x is Relation-like () set
dom x is set
(x) is Relation-like () set
(x,f) is set
((x),(x,f)) is set
x * (x) is Relation-like () set
((x * (x)),f) is set
f is set
x is Relation-like () set
rng x is set
(x) is Relation-like () set
((x),f) is set
(x,((x),f)) is set
(x) * x is Relation-like () set
(((x) * x),f) is set
dom (x) is set
f is Relation-like () set
(f) is Relation-like () set
f * (f) is Relation-like () set
dom (f * (f)) is set
dom f is set
rng (f * (f)) is set
rng f is set
dom (f) is set
rng (f) is set
f is Relation-like () set
(f) is Relation-like () set
(f) * f is Relation-like () set
dom ((f) * f) is set
rng f is set
rng ((f) * f) is set
rng (f) is set
dom f is set
dom (f) is set
f is Relation-like () set
dom f is set
rng f is set
(f) is Relation-like () set
x is Relation-like () set
rng x is set
dom x is set
F is set
(x,F) is set
((f),F) is set
(f,(x,F)) is set
dom (f) is set
f is Relation-like () set
(f) is Relation-like () set
f * (f) is Relation-like () set
dom f is set
id (dom f) is Relation-like dom f -defined dom f -valued () () set
(f) * f is Relation-like () set
rng f is set
id (rng f) is Relation-like rng f -defined rng f -valued () () set
dom (f * (f)) is set
x is set
((f * (f)),x) is set
dom ((f) * f) is set
x is set
(((f) * f),x) is set
f is Relation-like () set
(f) is Relation-like () set
x is set
dom (f) is set
((f),x) is set
F is set
((f),F) is set
rng f is set
(f,((f),x)) is set
f is Relation-like () () set
(f) is Relation-like () set
x is Relation-like () () set
f * x is Relation-like () set
f is set
id f is Relation-like f -defined f -valued () () set
x is Relation-like () set
rng x is set
F is Relation-like () set
x * F is Relation-like () set
f is Relation-like () set
dom f is set
id (dom f) is Relation-like dom f -defined dom f -valued () () set
F * f is Relation-like () set
(x * F) * f is Relation-like () set
x * (F * f) is Relation-like () set
(id (dom f)) * f is Relation-like dom f -defined () set
f is Relation-like () set
rng f is set
dom f is set
id (dom f) is Relation-like dom f -defined dom f -valued () () set
(f) is Relation-like () set
x is Relation-like () set
dom x is set
f * x is Relation-like () set
(f) * f is Relation-like () set
id (rng f) is Relation-like rng f -defined rng f -valued () () set
rng (f) is set
f is Relation-like () set
dom f is set
rng f is set
id (rng f) is Relation-like rng f -defined rng f -valued () () set
(f) is Relation-like () set
x is Relation-like () set
rng x is set
x * f is Relation-like () set
f * (f) is Relation-like () set
id (dom f) is Relation-like dom f -defined dom f -valued () () set
dom (f) is set
f is Relation-like () set
(f) is Relation-like () set
((f)) is Relation-like () set
rng f is set
dom (f) is set
(f) * f is Relation-like () set
id (dom (f)) is Relation-like dom (f) -defined dom (f) -valued () () set
dom f is set
rng (f) is set
f is Relation-like () set
(f) is Relation-like () set
x is Relation-like () set
f * x is Relation-like () set
((f * x)) is Relation-like () set
(x) is Relation-like () set
(x) * (f) is Relation-like () set
rng (f * x) is set
dom ((x) * (f)) is set
F is set
dom (f * x) is set
f is set
((f * x),f) is set
(f,f) is set
dom x is set
(x,(f,f)) is set
rng x is set
dom (x) is set
dom f is set
((x),(x,(f,f))) is set
x * (x) is Relation-like () set
((x * (x)),(f,f)) is set
id (dom x) is Relation-like dom x -defined dom x -valued () () set
((id (dom x)),(f,f)) is set
((x),F) is set
rng f is set
dom (f) is set
dom (x) is set
rng x is set
dom x is set
f is set
(x,f) is set
((x),F) is set
dom (f) is set
((x),(x,f)) is set
rng f is set
x * (x) is Relation-like () set
((x * (x)),f) is set
id (dom x) is Relation-like dom x -defined dom x -valued () () set
((id (dom x)),f) is set
dom f is set
x is set
(f,x) is set
dom (f * x) is set
((f * x),x) is set
(f * x) * ((x) * (f)) is Relation-like () set
dom ((f * x) * ((x) * (f))) is set
dom (f * x) is set
F is set
((f * x),F) is set
F is set
(((f * x) * ((x) * (f))),F) is set
(f,F) is set
dom x is set
((f * x),F) is set
(x,(f,F)) is set
dom f is set
(((x) * (f)),((f * x),F)) is set
(((x) * (f)),(x,(f,F))) is set
((x),(x,(f,F))) is set
((f),((x),(x,(f,F)))) is set
x * (x) is Relation-like () set
((x * (x)),(f,F)) is set
((f),((x * (x)),(f,F))) is set
id (dom x) is Relation-like dom x -defined dom x -valued () () set
((id (dom x)),(f,F)) is set
((f),((id (dom x)),(f,F))) is set
((f),(f,F)) is set
id (dom (f * x)) is Relation-like dom (f * x) -defined dom (f * x) -valued () () set
f is set
id f is Relation-like f -defined f -valued () () set
((id f)) is Relation-like () () set
dom (id f) is set
(id f) * ((id f)) is Relation-like f -defined () () set
dom ((id f)) is set
rng (id f) is set
f is Relation-like () set
x is set
f | x is Relation-like set
F is set
f is set
[F,f] is non empty set
{F,f} is non empty set
{F} is non empty trivial set
{{F,f},{F}} is non empty set
x is set
[F,x] is non empty set
{F,x} is non empty set
{{F,x},{F}} is non empty set
f is set
x is Relation-like () set
dom x is set
F is Relation-like () set
dom F is set
(dom F) /\ f is set
F | f is Relation-like () set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
(x,f) is set
(F,f) is set
f is set
x is set
F is Relation-like () set
F | x is Relation-like () set
dom (F | x) is set
((F | x),f) is set
(F,f) is set
dom F is set
(dom F) /\ x is set
[f,((F | x),f)] is non empty set
{f,((F | x),f)} is non empty set
{f} is non empty trivial set
{{f,((F | x),f)},{f}} is non empty set
f is set
x is set
F is Relation-like () set
dom F is set
(dom F) /\ x is set
F | x is Relation-like () set
((F | x),f) is set
(F,f) is set
dom (F | x) is set
f is set
x is set
F is Relation-like () set
F | x is Relation-like () set
((F | x),f) is set
(F,f) is set
dom F is set
dom (F | x) is set
dom F is set
dom (F | x) is set
dom F is set
f is set
x is set
F is Relation-like () set
dom F is set
(F,f) is set
F | x is Relation-like () set
rng (F | x) is set
(dom F) /\ x is set
dom (F | x) is set
((F | x),f) is set
f is set
x is set
F is Relation-like () set
F | f is Relation-like () set
(F | f) | x is Relation-like () set
F | x is Relation-like () set
(F | x) | f is Relation-like () set
f is set
x is Relation-like () set
x | f is Relation-like () set
F is set
dom (x | f) is set
((x | f),F) is set
f is set
((x | f),f) is set
dom x is set
(dom x) /\ f is set
(x,F) is set
(x,f) is set
f is set
x is Relation-like () set
f |` x is Relation-like set
F is set
f is set
[F,f] is non empty set
{F,f} is non empty set
{F} is non empty trivial set
{{F,f},{F}} is non empty set
x is set
[F,x] is non empty set
{F,x} is non empty set
{{F,x},{F}} is non empty set
f is set
x is Relation-like () set
dom x is set
F is Relation-like () set
f |` F is Relation-like () set
dom F is set
f is set
(x,f) is set
[f,(x,f)] is non empty set
{f,(x,f)} is non empty set
{f} is non empty trivial set
{{f,(x,f)},{f}} is non empty set
(F,f) is set
[f,(F,f)] is non empty set
{f,(F,f)} is non empty set
{{f,(F,f)},{f}} is non empty set
f is set
(x,f) is set
[f,(x,f)] is non empty set
{f,(x,f)} is non empty set
{f} is non empty trivial set
{{f,(x,f)},{f}} is non empty set
(F,f) is set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
(x,f) is set
(F,f) is set
f is set
x is set
F is Relation-like () set
x |` F is Relation-like () set
dom (x |` F) is set
dom F is set
(F,f) is set
f is set
y is Relation-like () set
dom y is set
(y,f) is set
x is set
x |` y is Relation-like () set
dom (x |` y) is set
f is set
x is set
F is Relation-like () set
x |` F is Relation-like () set
dom (x |` F) is set
((x |` F),f) is set
(F,f) is set
f is set
x is Relation-like () set
f |` x is Relation-like () set
dom (f |` x) is set
dom x is set
F is set
f is set
x is set
F is Relation-like () set
f |` F is Relation-like () set
x |` (f |` F) is Relation-like () set
x |` F is Relation-like () set
f |` (x |` F) is Relation-like () set
f is set
x is Relation-like () set
f |` x is Relation-like () set
F is set
dom (f |` x) is set
((f |` x),F) is set
f is set
((f |` x),f) is set
dom x is set
(x,F) is set
(x,f) is set
f is Relation-like () set
x is set
f .: x is set
dom f is set
F is set
f is set
x is set
[x,f] is non empty set
{x,f} is non empty set
{x} is non empty trivial set
{{x,f},{x}} is non empty set
y is set
(f,y) is set
x is set
(f,x) is set
[x,f] is non empty set
{x,f} is non empty set
{x} is non empty trivial set
{{x,f},{x}} is non empty set
f is set
x is set
(f,x) is set
y is set
[y,f] is non empty set
{y,f} is non empty set
{y} is non empty trivial set
{{y,f},{y}} is non empty set
x is set
[x,f] is non empty set
{x,f} is non empty set
{x} is non empty trivial set
{{x,f},{x}} is non empty set
(f,x) is set
f is set
x is Relation-like () set
dom x is set
Im (x,f) is set
{f} is non empty trivial set
x .: {f} is set
(x,f) is set
{(x,f)} is non empty trivial set
F is set
f is set
(x,f) is set
f is set
x is set
{f,x} is non empty set
F is Relation-like () set
dom F is set
F .: {f,x} is set
(F,f) is set
(F,x) is set
{(F,f),(F,x)} is non empty set
f is set
x is set
(F,x) is set
f is set
x is set
F is Relation-like () set
f |` F is Relation-like () set
(f |` F) .: x is set
F .: x is set
f is set
dom (f |` F) is set
x is set
((f |` F),x) is set
(F,x) is set
dom F is set
f is set
x is set
f /\ x is set
F is Relation-like () set
F .: (f /\ x) is set
F .: f is set
F .: x is set
(F .: f) /\ (F .: x) is set
f is set
dom F is set
x is set
(F,x) is set
y is set
(F,y) is set
f is Relation-like () set
dom f is set
x is set
F is set
(f,x) is set
(f,F) is set
{x} is non empty trivial set
{F} is non empty trivial set
{x} /\ {F} is set
f .: ({x} /\ {F}) is set
f .: {x} is set
f .: {F} is set
(f .: {x}) /\ (f .: {F}) is set
Im (f,x) is set
{(f,x)} is non empty trivial set
Im (f,F) is set
{(f,F)} is non empty trivial set
f is set
x is set
f \ x is Element of bool f
bool f is set
F is Relation-like () set
F .: (f \ x) is set
F .: f is set
F .: x is set
(F .: f) \ (F .: x) is Element of bool (F .: f)
bool (F .: f) is set
f is set
dom F is set
x is set
(F,x) is set
y is set
(F,y) is set
f is Relation-like () set
dom f is set
x is set
F is set
(f,x) is set
(f,F) is set
{x} is non empty trivial set
{F} is non empty trivial set
{x} \ {F} is Element of bool {x}
bool {x} is set
f .: ({x} \ {F}) is set
f .: {x} is set
f .: {F} is set
(f .: {x}) \ (f .: {F}) is Element of bool (f .: {x})
bool (f .: {x}) is set
Im (f,x) is set
{(f,x)} is non empty trivial set
Im (f,F) is set
{(f,F)} is non empty trivial set
f is set
x is set
F is Relation-like () set
F .: f is set
F .: x is set
f /\ x is set
F .: (f /\ x) is set
(F .: f) /\ (F .: x) is set
f is set
x is set
F is Relation-like () set
f |` F is Relation-like () set
(f |` F) .: x is set
F .: x is set
f /\ (F .: x) is set
f is set
dom (f |` F) is set
x is set
((f |` F),x) is set
(F,x) is set
dom F is set
dom F is set
x is set
(F,x) is set
dom (f |` F) is set
((f |` F),x) is set
f is Relation-like () set
x is set
f " x is set
dom f is set
F is set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
(f,f) is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
[f,(f,f)] is non empty set
{f,(f,f)} is non empty set
{f} is non empty trivial set
{{f,(f,f)},{f}} is non empty set
f is set
(f,f) is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
x is set
[f,x] is non empty set
{f,x} is non empty set
{{f,x},{f}} is non empty set
f is set
x is set
f /\ x is set
F is Relation-like () set
F " (f /\ x) is set
F " f is set
F " x is set
(F " f) /\ (F " x) is set
f is set
(F,f) is set
dom F is set
f is set
x is set
f \ x is Element of bool f
bool f is set
F is Relation-like () set
F " (f \ x) is set
F " f is set
F " x is set
(F " f) \ (F " x) is Element of bool (F " f)
bool (F " f) is set
f is set
(F,f) is set
dom F is set
f is set
x is set
F is Relation-like set
F | f is Relation-like set
(F | f) " x is set
F " x is set
f /\ (F " x) is set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
f is Relation-like () set
x is set
F is set
f " x is set
f " F is set
x /\ F is set
f " (x /\ F) is set
(f " x) /\ (f " F) is set
f is set
{f} is non empty trivial set
x is Relation-like set
rng x is set
x " {f} is set
F is set
[F,f] is non empty set
{F,f} is non empty set
{F} is non empty trivial set
{{F,f},{F}} is non empty set
F is set
f is set
[F,f] is non empty set
{F,f} is non empty set
{F} is non empty trivial set
{{F,f},{F}} is non empty set
f is set
x is Relation-like set
rng x is set
F is set
{F} is non empty trivial set
x " {F} is set
f is Relation-like () set
rng f is set
x is set
dom f is set
(f,x) is set
F is set
(f,F) is set
{(f,x)} is non empty trivial set
f " {(f,x)} is set
f is set
{f} is non empty trivial set
{(f,F)} is non empty trivial set
f " {(f,F)} is set
x is set
{x} is non empty trivial set
x is set
{x} is non empty trivial set
f " {x} is set
dom f is set
F is set
(f,F) is set
{F} is non empty trivial set
f is set
(f,f) is set
f is set
x is Relation-like () set
x " f is set
x .: (x " f) is set
F is set
dom x is set
f is set
(x,f) is set
f is set
x is Relation-like set
dom x is set
x .: f is set
x " (x .: f) is set
F is set
f is set
[F,f] is non empty set
{F,f} is non empty set
{F} is non empty trivial set
{{F,f},{F}} is non empty set
f is set
x is Relation-like () set
rng x is set
x " f is set
x .: (x " f) is set
F is set
dom x is set
f is set
(x,f) is set
f is set
x is Relation-like () set
x " f is set
x .: (x " f) is set
dom x is set
x .: (dom x) is set
f /\ (x .: (dom x)) is set
F is set
f is set
(x,f) is set
f is set
x is set
F is Relation-like () set
F " x is set
f /\ (F " x) is set
F .: (f /\ (F " x)) is set
F .: f is set
(F .: f) /\ x is set
f is set
dom F is set
x is set
(F,x) is set
f is set
x is set
F is Relation-like () set
F " x is set
f /\ (F " x) is set
F .: (f /\ (F " x)) is set
F .: f is set
(F .: f) /\ x is set
f is set
dom F is set
x is set
(F,x) is set
f is set
x is set
F is Relation-like set
F " x is set
f /\ (F " x) is set
F .: f is set
(F .: f) /\ x is set
F " ((F .: f) /\ x) is set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
f is set
x is Relation-like () set
x .: f is set
x " (x .: f) is set
F is set
(x,F) is set
dom x is set
f is set
(x,f) is set
f is Relation-like () set
dom f is set
x is set
F is set
(f,x) is set
(f,F) is set
{x} is non empty trivial set
f .: {x} is set
f " (f .: {x}) is set
Im (f,F) is set
{F} is non empty trivial set
f .: {F} is set
{(f,F)} is non empty trivial set
Im (f,x) is set
{(f,x)} is non empty trivial set
rng f is set
f is set
x is Relation-like () set
x .: f is set
(x) is Relation-like () set
(x) " f is set
F is set
dom x is set
f is set
(x,f) is set
rng x is set
dom (x) is set
((x),(x,f)) is set
((x),F) is set
dom (x) is set
rng x is set
dom x is set
f is set
(x,f) is set
f is set
x is Relation-like () set
x " f is set
(x) is Relation-like () set
(x) .: f is set
F is set
(x,F) is set
dom x is set
rng x is set
dom (x) is set
((x),(x,F)) is set
dom (x) is set
f is set
((x),f) is set
rng x is set
(x,F) is set
dom x is set
f is set
x is Relation-like () set
rng x is set
F is Relation-like () set
dom F is set
x * F is Relation-like () set
f is Relation-like () set
dom f is set
x * f is Relation-like () set
x is set
(F,x) is set
(f,x) is set
dom x is set
y is set
(x,y) is set
((x * F),y) is set
f is set
x is set
F is Relation-like () set
F .: f is set
F .: x is set
dom F is set
f is set
(F,f) is set
x is set
(F,x) is set
f is set
x is set
F is Relation-like () set
F " f is set
F " x is set
rng F is set
f is set
dom F is set
x is set
(F,x) is set
f is Relation-like () set
rng f is set
x is set
{x} is non empty trivial set
f " {x} is set
F is set
{F} is non empty trivial set
dom f is set
f is set
(f,f) is set
x is set
{x} is non empty trivial set
f " {x} is set
the set is set
f is set
{f} is non empty trivial set
F is set
{F} is non empty trivial set
f is set
{f} is non empty trivial set
F is set
{F} is non empty trivial set
f is set
{f} is non empty trivial set
x is set
{x} is non empty trivial set
f " {x} is set
F is set
{F} is non empty trivial set
f " {F} is set
f is set
{f} is non empty trivial set
f " {f} is set
f is set
x is Relation-like set
rng x is set
x " f is set
F is Relation-like set
dom F is set
x * F is Relation-like set
F .: f is set
(x * F) " (F .: f) is set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
y is set
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial set
{{x,y},{x}} is non empty set
[f,y] is non empty set
{f,y} is non empty set
{{f,y},{f}} is non empty set
f is set
x is set
F is Relation-like () set
F " f is set
F " x is set
rng F is set
f is set
bool f is set
id f is Relation-like f -defined f -valued () () set
x is Element of bool f
(id f) .: x is set
F is set
dom (id f) is set
((id f),F) is set
f is set
((id f),f) is set
f is Relation-like () set
dom f is set
x is set
(f,x) is set
rng f is set
x is set
{{}} is non empty trivial set
F is set
(f,F) is set
f is Relation-like () set
dom f is set
rng f is set
x is set
(f,x) is set
x is set
(f,x) is set
f is set
dom {} is empty trivial Relation-like non-empty empty-yielding () () set
({},f) is set
F₁() is non empty set
f is Relation-like () set
dom f is set
x is Element of F₁()
(f,x) is set
F₂(x) is set
f is Relation-like non-empty () set
rng f is set
dom f is set
x is set
(f,x) is set
f is set
x is set
F is Relation-like () set
dom F is set
F .: f is set
F " x is set
F " (F .: f) is set
f is set
x is Relation-like () set
dom x is set
x .: f is set
x " (x .: f) is set
F is set
(x,F) is set
f is Relation-like () set
x is Relation-like () set
dom f is set
dom x is set
F is set
(f,F) is set
(x,F) is set
{{}} is non empty trivial set
{{{}}} is non empty trivial set
f is Relation-like () set
dom f is set
rng f is set
f is non empty Relation-like non-empty () set
dom f is non empty set
x is Element of dom f
(f,x) is set
rng f is non empty with_non-empty_elements set
f is Relation-like () set
bool f is set
x is Relation-like Element of bool f
F is set
f is set
[F,f] is non empty set
{F,f} is non empty set
{F} is non empty trivial set
{{F,f},{F}} is non empty set
x is set
[F,x] is non empty set
{F,x} is non empty set
{{F,x},{F}} is non empty set
f is Relation-like () set
dom f is set
x is Relation-like () set
dom x is set
F is set
f | F is Relation-like () set
x | F is Relation-like () set
dom (x | F) is set
(dom x) /\ F is set
f is set
(f,f) is set
((x | F),f) is set
(x,f) is set
f is set
((f | F),f) is set
(f,f) is set
(x,f) is set
((x | F),f) is set
dom (f | F) is set
(dom f) /\ F is set
f is Relation-like () set
dom f is set
x is Relation-like () set
dom x is set
F is set
f | F is Relation-like () set
x | F is Relation-like () set
dom (f | F) is set
(dom f) /\ F is set
dom (x | F) is set
f is set
((f | F),f) is set
(f,f) is set
((x | F),f) is set
(x,f) is set
f is set
{f} is non empty trivial set
x is Relation-like () set
x | {f} is Relation-like () set
rng (x | {f}) is set
(x,f) is set
{(x,f)} is non empty trivial set
F is set
dom (x | {f}) is set
f is set
((x | {f}),f) is set
f is set
{f} is non empty trivial set
x is Relation-like () set
dom x is set
x | {f} is Relation-like () set
rng (x | {f}) is set
(x,f) is set
{(x,f)} is non empty trivial set
dom (x | {f}) is set
F is set
((x | {f}),f) is set
f is Relation-like () set
x is set
dom f is set
(f,x) is set
F is set
(f,F) is set
f is Relation-like () () set
rng f is set
x is empty trivial Relation-like non-empty empty-yielding () () () set
rng x is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding () () () set
dom f is set
x is set
(f,x) is set
{(f,x)} is non empty trivial set
F is set
f is set
(f,f) is set
f is set
(f,f) is set
1 is non empty set
[1,1] is non empty set
{1,1} is non empty set
{1} is non empty trivial set
{{1,1},{1}} is non empty set
2 is non empty set
[2,2] is non empty set
{2,2} is non empty set
{2} is non empty trivial set
{{2,2},{2}} is non empty set
{[1,1],[2,2]} is non empty Relation-like set
x is set
F is set
[x,F] is non empty set
{x,F} is non empty set
{x} is non empty trivial set
{{x,F},{x}} is non empty set
f is set
[x,f] is non empty set
{x,f} is non empty set
{{x,f},{x}} is non empty set
x is Relation-like () set
dom x is set
(x,1) is set
(x,2) is set
f is Relation-like () () set
rng f is set
x is empty trivial Relation-like non-empty empty-yielding () () () set
x is set
F is set
dom f is set
f is set
(f,F) is set
(f,f) is set
f is Relation-like () set
dom f is set
x is set
F is set
(f,x) is set
(f,F) is set
f is non empty Relation-like () set
(f,x) is set
[x,(f,x)] is non empty set
{x,(f,x)} is non empty set
{x} is non empty trivial set
{{x,(f,x)},{x}} is non empty set
(f,F) is set
[F,(f,F)] is non empty set
{F,(f,F)} is non empty set
{F} is non empty trivial set
{{F,(f,F)},{F}} is non empty set
x is Element of f
y is Element of f
f is Relation-like () set
f is Relation-like () set
x is Relation-like () set
f * x is Relation-like () set
F is set
f | F is Relation-like () set
f .: F is set
x | (f .: F) is Relation-like () set
(f | F) * (x | (f .: F)) is Relation-like () set
(f * x) | F is Relation-like () set
dom ((f * x) | F) is set
x is set
dom ((f | F) * (x | (f .: F))) is set
dom (f | F) is set
dom f is set
(dom f) /\ F is set
((f | F),x) is set
dom (x | (f .: F)) is set
(f,x) is set
dom x is set
(dom x) /\ (f .: F) is set
dom (f * x) is set
(dom (f * x)) /\ F is set
dom (f * x) is set
(dom (f * x)) /\ F is set
(f,x) is set
dom x is set
dom f is set
(dom f) /\ F is set
dom (f | F) is set
(dom x) /\ (f .: F) is set
dom (x | (f .: F)) is set
((f | F),x) is set
x is set
(f,x) is set
(((f | F) * (x | (f .: F))),x) is set
((f | F),x) is set
((x | (f .: F)),((f | F),x)) is set
((x | (f .: F)),(f,x)) is set
(x,(f,x)) is set
((f * x),x) is set
(((f * x) | F),x) is set
f is Relation-like () set
x is Relation-like () set
f * x is Relation-like () set
F is set
f | F is Relation-like () set
f is set
x | f is Relation-like () set
(f | F) * (x | f) is Relation-like () set
f " f is set
F /\ (f " f) is set
(f * x) | (F /\ (f " f)) is Relation-like () set
dom ((f | F) * (x | f)) is set
y is set
dom ((f * x) | (F /\ (f " f))) is set
dom (f * x) is set
(dom (f * x)) /\ (F /\ (f " f)) is set
dom f is set
(dom f) /\ F is set
dom (f | F) is set
(f,y) is set
dom x is set
(dom x) /\ f is set
dom (x | f) is set
((f | F),y) is set
dom (f | F) is set
dom f is set
(dom f) /\ F is set
((f | F),y) is set
dom (x | f) is set
(f,y) is set
dom x is set
(dom x) /\ f is set
dom (f * x) is set
(dom (f * x)) /\ (F /\ (f " f)) is set
y is set
((f | F),y) is set
(f,y) is set
(((f | F) * (x | f)),y) is set
((x | f),((f | F),y)) is set
((x | f),(f,y)) is set
(x,(f,y)) is set
((f * x),y) is set
(((f * x) | (F /\ (f " f))),y) is set
f is Relation-like () set
x is Relation-like () set
f * x is Relation-like () set
dom (f * x) is set
dom f is set
dom x is set
F is set
f .: F is set
f is set
f is set
x is set
(f,x) is set
f is set
(f,f) is set
f is Relation-like () set
dom f is set
x is set
(f,x) is set
f is set
x is set
(f,f) is set
x is set
F is set
(f,x) is set
f is set
x is set
dom {} is empty trivial Relation-like non-empty empty-yielding () () () set
rng {} is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding () () () set
f is set
x is Relation-like f -valued () set
dom x is set
F is set
(x,F) is set
rng x is set
f is set
x is set
f is Relation-like () set
{f} is non empty trivial set
x is set
x is Relation-like () set
{f,x} is non empty set
F is set
{{}} is non empty trivial () set
f is () set
x is Element of f
f is () set
bool f is set
x is Element of bool f
F is set
f is Relation-like () set
dom f is set
x is Relation-like () set
dom x is set
F is set
(x,F) is set
f is Relation-like () set
x is set
dom {} is empty trivial Relation-like non-empty empty-yielding () () () () set
({},x) is set
(f,x) is set
f is set
x is Relation-like () set
x is Relation-like () set
F is Relation-like () (x) set
f is set
F | f is Relation-like () set
f is set
dom (F | f) is set
((F | f),f) is set
(x,f) is set
dom F is set
(F,f) is set
f is set
dom {} is empty trivial Relation-like non-empty empty-yielding () () () () set
f is Relation-like () set
dom f is set
x is Relation-like () (f) set
dom x is set
F is set
(x,F) is set
(f,F) is set
f is set
x is Relation-like f -defined () set
F is Relation-like () set
dom F is set
dom x is set
f is set
x is set
F is Relation-like f -valued () set
dom F is set
(F,x) is set
rng F is set
f is Relation-like () set
dom f is set
(f) is Relation-like () set
x is set
f .: x is set
(f) .: (f .: x) is set
f is set
dom (f) is set
x is set
((f),x) is set
y is set
(f,y) is set
f is set
(f,f) is set
((f),(f,f)) is set
rng f is set
dom (f) is set
f is () set
F is Relation-like f -valued () set
x is set
(F,x) is set
dom F is set
rng F is set
dom F is set
dom F is set
f is set
x is set
F is Relation-like () set
dom F is set
(F,f) is set
F .: x is set
x /\ (dom F) is set
F | x is Relation-like () set
dom (F | x) is set
((F | x),f) is set
rng (F | x) is set
f is set
x is Relation-like () set
dom x is set
x .: f is set
F is set
f is non empty non trivial Relation-like () set
dom f is non empty set
x is set
F is set
f is set
x is set
[f,x] is non empty set
{f,x} is non empty set
{f} is non empty trivial set
{{f,x},{f}} is non empty set
y is set
g is set
[y,g] is non empty set
{y,g} is non empty set
{y} is non empty trivial set
{{y,g},{y}} is non empty set
f is non empty () set
union f is set
{ (dom b₁) where b₁ is Relation-like () Element of f : verum } is set
union { (dom b₁) where b₁ is Relation-like () Element of f : verum } is set
{ (rng b₁) where b₁ is Relation-like () Element of f : verum } is set
union { (rng b₁) where b₁ is Relation-like () Element of f : verum } is set
x is Relation-like () set
dom x is set
rng x is set
f is set
(x,f) is set
[f,(x,f)] is non empty set
{f,(x,f)} is non empty set
{f} is non empty trivial set
{{f,(x,f)},{f}} is non empty set
x is set
y is Relation-like () set
dom y is set
g is set
x is set
y is Relation-like () Element of f
dom y is set
(y,f) is set
[f,(y,f)] is non empty set
{f,(y,f)} is non empty set
{{f,(y,f)},{f}} is non empty set
x is set
y is set
(x,y) is set
[y,x] is non empty set
{y,x} is non empty set
{y} is non empty trivial set
{{y,x},{y}} is non empty set
g is set
x is Relation-like () set
rng x is set
dom x is set
(x,y) is set
Z is set
y is set
g is Relation-like () Element of f
rng g is set
dom g is set
x is set
(g,x) is set
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial set
{{x,x},{x}} is non empty set
f is set
x is Relation-like () set
dom x is set
F is set
(x,F) is set
the Element of F is Element of F
F₁() is set
F₂() is set
dom {} is empty trivial Relation-like non-empty empty-yielding () () () () set
rng {} is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding () () () () set
f is set
({},f) is set
f is set
x is set
F is set
f is set
x is set
f is set
x is set
f is set
x is set
F is set
f is set
f is Relation-like () set
dom f is set
rng f is set
F is set
x is non empty set
f is set
(f,f) is set
x is set
y is set
x is set
F is Relation-like () set
dom F is set
f * F is Relation-like () set
dom (f * F) is set
f is Relation-like () set
dom f is set
rng f is set
rng F is set
x is set
y is set
(F,y) is set
g is set
(f,g) is set
x is set
(f,x) is set
(f,x) is set
(F,(f,x)) is set
f is Relation-like empty-yielding () set
x is set
(f,x) is set
dom f is set