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

f is set

[:F

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

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

f is set

F

f is set

x is set

F

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

f is Relation-like () set

dom f is set

x is Element of F

(f,x) is set

F

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

union { (dom b

{ (rng b

union { (rng b

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

F

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