:: FUNCT_4 semantic presentation

{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() set

the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() set

f is set

g is set

[f,g] is non empty set

{f,g} is non empty set

{f} is non empty trivial set

{{f,g},{f}} is non empty set

h is set

x is set

[h,x] is non empty set

{h,x} is non empty set

{h} is non empty trivial set

{{h,x},{h}} is non empty set

[[f,g],[h,x]] is non empty set

{[f,g],[h,x]} is Relation-like non empty set

{[f,g]} is Relation-like Function-like constant non empty trivial set

{{[f,g],[h,x]},{[f,g]}} is non empty set

y is set

b is set

[y,b] is non empty set

{y,b} is non empty set

{y} is non empty trivial set

{{y,b},{y}} is non empty set

z is set

nm is set

[z,nm] is non empty set

{z,nm} is non empty set

{z} is non empty trivial set

{{z,nm},{z}} is non empty set

[[y,b],[z,nm]] is non empty set

{[y,b],[z,nm]} is Relation-like non empty set

{[y,b]} is Relation-like Function-like constant non empty trivial set

{{[y,b],[z,nm]},{[y,b]}} is non empty set

f is set

union f is set

union (union f) is set

g is set

h is set

[:g,h:] is Relation-like set

x is set

y is set

b is set

[y,b] is non empty set

{y,b} is non empty set

{y} is non empty trivial set

{{y,b},{y}} is non empty set

f is Relation-like Function-like set

g is Relation-like Function-like set

g * f is Relation-like Function-like set

rng g is set

f | (rng g) is Relation-like Function-like set

g * (f | (rng g)) is Relation-like Function-like set

dom (g * f) is set

dom (g * (f | (rng g))) is set

h is set

dom (f | (rng g)) is set

dom f is set

(dom f) /\ (rng g) is set

dom g is set

g . h is set

g . h is set

dom g is set

h is set

(g * f) . h is set

(g * (f | (rng g))) . h is set

dom g is set

g . h is set

f . (g . h) is set

(f | (rng g)) . (g . h) is set

f is set

id f is Relation-like f -defined f -valued Function-like one-to-one total Element of bool [:f,f:]

[:f,f:] is Relation-like set

bool [:f,f:] is set

g is set

id g is Relation-like g -defined g -valued Function-like one-to-one total Element of bool [:g,g:]

[:g,g:] is Relation-like set

bool [:g,g:] is set

h is set

[h,h] is non empty set

{h,h} is non empty set

{h} is non empty trivial set

{{h,h},{h}} is non empty set

h is set

x is 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 is set

g is set

h is set

{h} is non empty trivial set

f --> h is Relation-like f -defined {h} -valued Function-like constant total quasi_total Element of bool [:f,{h}:]

[:f,{h}:] is Relation-like set

bool [:f,{h}:] is set

g --> h is Relation-like g -defined {h} -valued Function-like constant total quasi_total Element of bool [:g,{h}:]

[:g,{h}:] is Relation-like set

bool [:g,{h}:] is set

dom (f --> h) is Element of bool f

bool f is set

x is set

(f --> h) . x is set

(g --> h) . x is set

dom (g --> h) is Element of bool g

bool g is set

f is set

g is set

{g} is non empty trivial set

f --> g is Relation-like f -defined {g} -valued Function-like constant total quasi_total Element of bool [:f,{g}:]

[:f,{g}:] is Relation-like set

bool [:f,{g}:] is set

h is set

x is set

h --> x is Relation-like h -defined {x} -valued Function-like constant total quasi_total Element of bool [:h,{x}:]

{x} is non empty trivial set

[:h,{x}:] is Relation-like set

bool [:h,{x}:] is set

dom (f --> g) is Element of bool f

bool f is set

dom (h --> x) is Element of bool h

bool h is set

f is set

g is set

{g} is non empty trivial set

f --> g is Relation-like f -defined {g} -valued Function-like constant total quasi_total Element of bool [:f,{g}:]

[:f,{g}:] is Relation-like set

bool [:f,{g}:] is set

h is set

x is set

h --> x is Relation-like h -defined {x} -valued Function-like constant total quasi_total Element of bool [:h,{x}:]

{x} is non empty trivial set

[:h,{x}:] is Relation-like set

bool [:h,{x}:] is set

the Element of f is Element of f

(h --> x) . the Element of f is set

dom (f --> g) is Element of bool f

bool f is set

(f --> g) . the Element of f is set

f is set

g is Relation-like Function-like set

dom g is set

g . f is set

f .--> (g . f) is Relation-like {f} -defined Function-like one-to-one set

{f} is non empty trivial set

{f} --> (g . f) is Relation-like {f} -defined {(g . f)} -valued Function-like constant non empty total quasi_total Element of bool [:{f},{(g . f)}:]

{(g . f)} is non empty trivial set

[:{f},{(g . f)}:] is Relation-like set

bool [:{f},{(g . f)}:] is set

h is set

dom (f .--> (g . f)) is Element of bool {f}

bool {f} is set

(f .--> (g . f)) . h is set

g . h is set

h is set

f is set

g is set

h is Relation-like Function-like set

f |` h is Relation-like Function-like set

(f |` h) | g is Relation-like Function-like set

f is set

g is set

h is Relation-like Function-like set

f |` h is Relation-like Function-like set

(f |` h) | g is Relation-like Function-like set

x is Relation-like Function-like set

f |` x is Relation-like Function-like set

(f |` x) | g is Relation-like Function-like set

f is Relation-like Function-like set

dom f is set

g is Relation-like Function-like set

dom g is set

(dom f) \/ (dom g) is set

h is Relation-like Function-like set

dom h is set

x is Relation-like Function-like set

dom x is set

y is set

h . y is set

x . y is set

f . y is set

g . y is set

h is Relation-like Function-like set

dom h is set

(dom h) \/ (dom h) is set

y is set

x is Relation-like Function-like set

dom x is set

(dom x) \/ (dom x) is set

x . y is set

f is Relation-like Function-like set

dom f is set

g is Relation-like Function-like set

(f,g) is Relation-like Function-like set

dom (f,g) is set

dom g is set

(dom f) \/ (dom g) is set

f is set

g is Relation-like Function-like set

dom g is set

h is Relation-like Function-like set

(h,g) is Relation-like Function-like set

(h,g) . f is set

h . f is set

dom h is set

(dom h) \/ (dom g) is set

dom h is set

(dom h) \/ (dom g) is set

dom (h,g) is set

dom h is set

f is set

g is Relation-like Function-like set

dom g is set

h is Relation-like Function-like set

(g,h) is Relation-like Function-like set

dom (g,h) is set

dom h is set

(dom g) \/ (dom h) is set

f is set

g is Relation-like Function-like set

dom g is set

g . f is set

h is Relation-like Function-like set

(h,g) is Relation-like Function-like set

(h,g) . f is set

dom h is set

(dom h) \/ (dom g) is set

f is Relation-like Function-like set

g is Relation-like Function-like set

(f,g) is Relation-like Function-like set

h is Relation-like Function-like set

((f,g),h) is Relation-like Function-like set

(g,h) is Relation-like Function-like set

(f,(g,h)) is Relation-like Function-like set

x is set

dom f is set

dom (g,h) is set

(dom f) \/ (dom (g,h)) is set

dom g is set

dom h is set

((f,g),h) . x is set

(f,g) . x is set

g . x is set

(g,h) . x is set

dom h is set

((f,g),h) . x is set

h . x is set

(g,h) . x is set

dom g is set

dom h is set

((f,g),h) . x is set

(g,h) . x is set

((f,g),h) . x is set

(g,h) . x is set

dom g is set

dom h is set

(f,g) . x is set

f . x is set

dom ((f,g),h) is set

dom (f,g) is set

(dom (f,g)) \/ (dom h) is set

(dom f) \/ (dom g) is set

((dom f) \/ (dom g)) \/ (dom h) is set

(dom g) \/ (dom h) is set

(dom f) \/ ((dom g) \/ (dom h)) is set

f is set

g is Relation-like Function-like set

dom g is set

g . f is set

h is Relation-like Function-like set

(g,h) is Relation-like Function-like set

(g,h) . f is set

dom h is set

(dom g) /\ (dom h) is set

h . f is set

dom h is set

dom h is set

f is set

g is Relation-like Function-like set

dom g is set

g . f is set

h is Relation-like Function-like set

dom h is set

(g,h) is Relation-like Function-like set

(g,h) . f is set

(dom g) /\ (dom h) is set

f is Relation-like Function-like set

rng f is set

g is Relation-like Function-like set

(f,g) is Relation-like Function-like set

rng (f,g) is set

rng g is set

(rng f) \/ (rng g) is set

h is set

dom (f,g) is set

x is set

(f,g) . x is set

dom f is set

dom g is set

f . x is set

g . x is set

f is Relation-like Function-like set

rng f is set

g is Relation-like Function-like set

(g,f) is Relation-like Function-like set

rng (g,f) is set

h is set

dom f is set

x is set

f . x is set

dom (g,f) is set

(g,f) . x is set

f is Relation-like Function-like set

dom f is set

g is Relation-like Function-like set

dom g is set

(f,g) is Relation-like Function-like set

(dom f) \/ (dom g) is set

dom (f,g) is set

h is set

(f,g) . h is set

g . h is set

g is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() set

f is Relation-like Function-like set

(g,f) is Relation-like Function-like set

dom g is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() set

dom f is set

(f,g) is Relation-like Function-like set

dom f is set

h is set

(f,g) . h is set

f . h is set

dom g is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() set

(dom f) \ (dom g) is Element of bool (dom f)

bool (dom f) is set

dom g is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Function-yielding V25() set

(dom f) \/ (dom g) is set

dom (f,g) is set

f is Relation-like Function-like set

({},f) is Relation-like Function-like set

f is Relation-like Function-like set

(f,{}) is Relation-like Function-like set

f is set

id f is Relation-like f -defined f -valued Function-like one-to-one total Element of bool [:f,f:]

[:f,f:] is Relation-like set

bool [:f,f:] is set

g is set

id g is Relation-like g -defined g -valued Function-like one-to-one total Element of bool [:g,g:]

[:g,g:] is Relation-like set

bool [:g,g:] is set

((id f),(id g)) is Relation-like Function-like set

f \/ g is set

id (f \/ g) is Relation-like f \/ g -defined f \/ g -valued Function-like one-to-one total Element of bool [:(f \/ g),(f \/ g):]

[:(f \/ g),(f \/ g):] is Relation-like set

bool [:(f \/ g),(f \/ g):] is set

dom (id (f \/ g)) is Element of bool (f \/ g)

bool (f \/ g) is set

h is set

((id f),(id g)) . h is set

(id (f \/ g)) . h is set

dom (id g) is Element of bool g

bool g is set

(id g) . h is set

dom (id g) is Element of bool g

bool g is set

(id f) . h is set

dom ((id f),(id g)) is set

dom (id f) is Element of bool f

bool f is set

dom (id g) is Element of bool g

bool g is set

(dom (id f)) \/ (dom (id g)) is set

f \/ (dom (id g)) is set

f is Relation-like Function-like set

g is Relation-like Function-like set

(f,g) is Relation-like Function-like set

dom g is set

(f,g) | (dom g) is Relation-like Function-like set

dom f is set

(dom f) \/ (dom g) is set

dom (f,g) is set

dom ((f,g) | (dom g)) is set

h is set

((f,g) | (dom g)) . h is set

g . h is set

(f,g) . h is set

f is Relation-like Function-like set

dom f is set

g is Relation-like Function-like set

(f,g) is Relation-like Function-like set

dom g is set

(dom f) \ (dom g) is Element of bool (dom f)

bool (dom f) is set

(f,g) | ((dom f) \ (dom g)) is Relation-like Function-like set

dom ((f,g) | ((dom f) \ (dom g))) is set

h is set

((f,g) | ((dom f) \ (dom g))) . h is set

f . h is set

(f,g) . h is set

f is Relation-like Function-like set

g is Relation-like Function-like set

(g,f) is Relation-like Function-like set

dom (g,f) is set

dom g is set

dom f is set

(dom g) \/ (dom f) is set

h is set

(g,f) . h is set

f . h is set

f is Relation-like Function-like set

dom f is set

g is Relation-like Function-like set

h is Relation-like Function-like set

(g,h) is Relation-like Function-like set

dom h is set

(dom f) \ (dom h) is Element of bool (dom f)

bool (dom f) is set

f | ((dom f) \ (dom h)) is Relation-like Function-like set

x is set

dom (f | ((dom f) \ (dom h))) is set

dom g is set

(dom (f | ((dom f) \ (dom h)))) /\ (dom g) is set

(f | ((dom f) \ (dom h))) . x is set

g . x is set

dom (g,h) is set

(dom f) /\ (dom (g,h)) is set

(g,h) . x is set

f . x is set

f is Relation-like Function-like set

g is Relation-like Function-like set

h is Relation-like Function-like set

(g,h) is Relation-like Function-like set

x is set

dom f is set

dom h is set

(dom f) /\ (dom h) is set

f . x is set

h . x is set

dom (g,h) is set

(dom f) /\ (dom (g,h)) is set

(g,h) . x is set

f is Relation-like Function-like set

g is Relation-like Function-like set

(f,g) is Relation-like Function-like set

dom f is set

dom g is set

(dom f) \/ (dom g) is set

dom (f,g) is set

h is set

(f,g) . h is set

f . h is set

f is Relation-like Function-like set

g is Relation-like Function-like set

(f,g) is Relation-like Function-like set

f \/ g is Relation-like set

h is set

x is 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

dom (f,g) is set

dom f is set

dom g is set

(f,g) . x is set

f . x is set

g . x is set

f is Relation-like Function-like set

g is Relation-like Function-like set

f \/ g is Relation-like set

(f,g) is Relation-like Function-like set

f is Relation-like Function-like set

dom f is set

g is Relation-like Function-like set

dom g is set

f \/ g is Relation-like set

(f,g) is Relation-like Function-like set

f is Relation-like Function-like set

dom f is set

g is Relation-like Function-like set

dom g is set

(f,g) is Relation-like Function-like set

f \/ g is Relation-like set

f is Relation-like Function-like set

dom f is set

g is Relation-like Function-like set

dom g is set

(f,g) is Relation-like Function-like set

(f,g) | (dom f) is Relation-like Function-like set

(dom f) \ (dom g) is Element of bool (dom f)

bool (dom f) is set

dom ((f,g) | (dom f)) is set

dom (f,g) is set

(dom (f,g)) /\ (dom f) is set

(dom f) \/ (dom g) is set

((dom f) \/ (dom g)) /\ (dom f) is set

f is Relation-like Function-like set

g is Relation-like Function-like set

(f,g) is Relation-like Function-like set

(g,f) is Relation-like Function-like set

dom (f,g) is set

h is set

(f,g) . h is set

(g,f) . h is set

dom f is set

dom g is set

(dom f) \/ (dom g) is set

f . h is set

(dom f) /\ (dom g) is set

g . h is set

f . h is set

g . h is set

dom g is set

dom f is set

(dom g) \/ (dom f) is set

dom (g,f) is set

h is set

dom f is set

dom g is set

(dom f) /\ (dom g) is set

f . h is set

g . h is set

(f,g) . h is set

f is Relation-like Function-like set

dom f is set

g is Relation-like Function-like set

dom g is set

(f,g) is Relation-like Function-like set

(g,f) is Relation-like Function-like set

f is set

g is set

[:f,g:] is Relation-like set

bool [:f,g:] is set

x is Relation-like f -defined g -valued Function-like Element of bool [:f,g:]

h is Relation-like f -defined g -valued Function-like Element of bool [:f,g:]

(h,x) is Relation-like Function-like set

dom x is Element of bool f

bool f is set

dom h is Element of bool f

f is set

g is set

[:f,g:] is Relation-like set

bool [:f,g:] is set

h is Relation-like f -defined g -valued Function-like quasi_total Element of bool [:f,g:]

x is Relation-like f -defined g -valued Function-like quasi_total Element of bool [:f,g:]

(h,x) is Relation-like Function-like set

dom h is Element of bool f

bool f is set

dom x is Element of bool f

f is set

[:f,f:] is Relation-like set

bool [:f,f:] is set

g is Relation-like f -defined f -valued Function-like quasi_total Element of bool [:f,f:]

h is Relation-like f -defined f -valued Function-like quasi_total Element of bool [:f,f:]

(g,h) is Relation-like Function-like set

f is set

g is non empty set

[:f,g:] is Relation-like set

bool [:f,g:] is set

h is Relation-like f -defined g -valued Function-like quasi_total Element of bool [:f,g:]

x is Relation-like f -defined g -valued Function-like quasi_total Element of bool [:f,g:]

(h,x) is Relation-like Function-like set

f is set

g is set

[:f,g:] is Relation-like set

bool [:f,g:] is set

h is Relation-like f -defined g -valued Function-like Element of bool [:f,g:]

x is Relation-like f -defined g -valued Function-like Element of bool [:f,g:]

(h,x) is Relation-like Function-like set

rng (h,x) is set

rng h is Element of bool g

bool g is set

rng x is Element of bool g

(rng h) \/ (rng x) is Element of bool g

dom (h,x) is set

dom h is Element of bool f

bool f is set

dom x is Element of bool f

(dom h) \/ (dom x) is Element of bool f

f is Relation-like Function-like set

dom f is set

union (dom f) is set

union (union (dom f)) is set

g is set

h is set

[:h,g:] is Relation-like set

x is set

y is set

b is set

z is set

R is set

nm is set

[R,nm] is non empty set

{R,nm} is non empty set

{R} is non empty trivial set

{{R,nm},{R}} is non empty set

[nm,R] is non empty set

{nm,R} is non empty set

{nm} is non empty trivial set

{{nm,R},{nm}} is non empty set

f . [nm,R] is set

y9 is set

y is set

[y9,y] is non empty set

{y9,y} is non empty set

{y9} is non empty trivial set

{{y9,y},{y9}} is non empty set

[y,y9] is non empty set

{y,y9} is non empty set

{y} is non empty trivial set

{{y,y9},{y}} is non empty set

f . [y,y9] is set

y is set

z is set

b is set

[z,b] is non empty set

{z,b} is non empty set

{z} is non empty trivial set

{{z,b},{z}} is non empty set

[b,z] is non empty set

{b,z} is non empty set

{b} is non empty trivial set

{{b,z},{b}} is non empty set

f . [b,z] is set

y is Relation-like Function-like set

dom y is set

b is set

nm is set

z is set

[nm,z] is non empty set

{nm,z} is non empty set

{nm} is non empty trivial set

{{nm,z},{nm}} is non empty set

[z,nm] is non empty set

{z,nm} is non empty set

{z} is non empty trivial set

{{z,nm},{z}} is non empty set

b is set

z is set

[b,z] is non empty set

{b,z} is non empty set

{b} is non empty trivial set

{{b,z},{b}} is non empty set

y . (z,b) is set

[z,b] is non empty set

{z,b} is non empty set

{z} is non empty trivial set

{{z,b},{z}} is non empty set

y . [z,b] is set

f . (b,z) is set

f . [b,z] is set

R is set

nm is set

[R,nm] is non empty set

{R,nm} is non empty set

{R} is non empty trivial set

{{R,nm},{R}} is non empty set

[nm,R] is non empty set

{nm,R} is non empty set

{nm} is non empty trivial set

{{nm,R},{nm}} is non empty set

f . [nm,R] is set

g is Relation-like Function-like set

dom g is set

h is Relation-like Function-like set

dom h is set

x is set

g . x is set

h . x is set

b is set

y is set

[b,y] is non empty set

{b,y} is non empty set

{b} is non empty trivial set

{{b,y},{b}} is non empty set

[y,b] is non empty set

{y,b} is non empty set

{y} is non empty trivial set

{{y,b},{y}} is non empty set

g . (b,y) is set

g . [b,y] is set

f . (y,b) is set

f . [y,b] is set

h . (b,y) is set

h . [b,y] is set

x is set

b is set

y is set

[b,y] is non empty set

{b,y} is non empty set

{b} is non empty trivial set

{{b,y},{b}} is non empty set

[y,b] is non empty set

{y,b} is non empty set

{y} is non empty trivial set

{{y,b},{y}} is non empty set

b is set

y is set

[b,y] is non empty set

{b,y} is non empty set

{b} is non empty trivial set

{{b,y},{b}} is non empty set

[y,b] is non empty set

{y,b} is non empty set

{y} is non empty trivial set

{{y,b},{y}} is non empty set

f is Relation-like Function-like set

(f) is Relation-like Function-like set

rng (f) is set

rng f is set

g is set

dom (f) is set

h is set

(f) . h is set

dom f is set

y is set

x 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

[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,x) is set

(f) . [y,x] is set

f . (x,y) is set

f . [x,y] is set

f is set

g is set

[f,g] is non empty set

{f,g} is non empty set

{f} is non empty trivial set

{{f,g},{f}} is non empty set

[g,f] is non empty set

{g,f} is non empty set

{g} is non empty trivial set

{{g,f},{g}} is non empty set

h is Relation-like Function-like set

dom h is set

(h) is Relation-like Function-like set

dom (h) is set

y is set

x 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

[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 is set

g is set

[f,g] is non empty set

{f,g} is non empty set

{f} is non empty trivial set

{{f,g},{f}} is non empty set

h is Relation-like Function-like set

(h) is Relation-like Function-like set

dom (h) is set

(h) . (f,g) is set

(h) . [f,g] is set

h . (g,f) is set

[g,f] is non empty set

{g,f} is non empty set

{g} is non empty trivial set

{{g,f},{g}} is non empty set

h . [g,f] is set

dom h is set

f is Relation-like Function-like set

(f) is Relation-like Function-like set

dom (f) is set

g is set

dom f is set

x is set

h is set

[x,h] is non empty set

{x,h} is non empty set

{x} is non empty trivial set

{{x,h},{x}} is non empty set

[h,x] is non empty set

{h,x} is non empty set

{h} is non empty trivial set

{{h,x},{h}} is non empty set

f is set

g is set

[:f,g:] is Relation-like set

[:g,f:] is Relation-like set

h is Relation-like Function-like set

dom h is set

(h) is Relation-like Function-like set

dom (h) is set

x is set

b is set

y is set

[b,y] is non empty set

{b,y} is non empty set

{b} is non empty trivial set

{{b,y},{b}} is non empty set

[y,b] is non empty set

{y,b} is non empty set

{y} is non empty trivial set

{{y,b},{y}} is non empty set

f is set

g is set

[:f,g:] is Relation-like set

[:g,f:] is Relation-like set

h is Relation-like Function-like set

dom h is set

(h) is Relation-like Function-like set

dom (h) is set

x is set

y is set

b is set

[y,b] is non empty set

{y,b} is non empty set

{y} is non empty trivial set

{{y,b},{y}} is non empty set

[b,y] is non empty set

{b,y} is non empty set

{b} is non empty trivial set

{{b,y},{b}} is non empty set

f is set

g is set

[:f,g:] is Relation-like set

h is Relation-like Function-like set

dom h is set

(h) is Relation-like Function-like set

rng (h) is set

rng h is set

x is set

y is set

h . y is set

b is set

z is set

[b,z] is non empty set

{b,z} is non empty set

{b} is non empty trivial set

{{b,z},{b}} is non empty set

[z,b] is non empty set

{z,b} is non empty set

{z} is non empty trivial set

{{z,b},{z}} is non empty set

dom (h) is set

h . (b,z) is set

h . [b,z] is set

(h) . (z,b) is set

(h) . [z,b] is set

f is set

g is set

[:f,g:] is Relation-like set

[:g,f:] is Relation-like set

h is set

[:[:f,g:],h:] is Relation-like set

bool [:[:f,g:],h:] is set

[:[:g,f:],h:] is Relation-like set

bool [:[:g,f:],h:] is set

x is Relation-like [:f,g:] -defined h -valued Function-like Element of bool [:[:f,g:],h:]

(x) is Relation-like Function-like set

dom x is Relation-like f -defined g -valued Element of bool [:f,g:]

bool [:f,g:] is set

dom (x) is set

rng x is Element of bool h

bool h is set

rng (x) is set

f is set

g is set

[:f,g:] is Relation-like set

[:g,f:] is Relation-like set

h is set

[:[:f,g:],h:] is Relation-like set

bool [:[:f,g:],h:] is set

[:[:g,f:],h:] is Relation-like set

bool [:[:g,f:],h:] is set

x is Relation-like [:f,g:] -defined h -valued Function-like quasi_total Element of bool [:[:f,g:],h:]

(x) is Relation-like Function-like set

dom x is Relation-like f -defined g -valued Element of bool [:f,g:]

bool [:f,g:] is set

dom (x) is set

rng x is Element of bool h

bool h is set

rng (x) is set

y is Relation-like [:g,f:] -defined h -valued Element of bool [:[:g,f:],h:]

dom y is Relation-like g -defined f -valued Element of bool [:g,f:]

bool [:g,f:] is set

f is set

g is set

[:f,g:] is Relation-like set

h is non empty set

[:[:f,g:],h:] is Relation-like set

bool [:[:f,g:],h:] is set

x is Relation-like [:f,g:] -defined h -valued Function-like quasi_total Element of bool [:[:f,g:],h:]

(x) is Relation-like Function-like set

[:g,f:] is Relation-like set

[:[:g,f:],h:] is Relation-like set

bool [:[:g,f:],h:] is set

f is Relation-like Function-like set

(f) is Relation-like Function-like set

((f)) is Relation-like Function-like set

g is set

dom ((f)) is set

dom (f) is set

x is set

h is set

[x,h] is non empty set

{x,h} is non empty set

{x} is non empty trivial set

{{x,h},{x}} is non empty set

[h,x] is non empty set

{h,x} is non empty set

{h} is non empty trivial set

{{h,x},{h}} is non empty set

b is set

y is set

[b,y] is non empty set

{b,y} is non empty set

{b} is non empty trivial set

{{b,y},{b}} is non empty set

[y,b] is non empty set

{y,b} is non empty set

{y} is non empty trivial set

{{y,b},{y}} is non empty set

dom f is set

g is set

((f)) . g is set

f . g is set

x is set

h is set

[x,h] is non empty set

{x,h} is non empty set

{x} is non empty trivial set

{{x,h},{x}} is non empty set

[h,x] is non empty set

{h,x} is non empty set

{h} is non empty trivial set

{{h,x},{h}} is non empty set

((f)) . (x,h) is set

((f)) . [x,h] is set

(f) . (h,x) is set

(f) . [h,x] is set

f . (x,h) is set

f . [x,h] is set

g is set

x is set

h is set

[x,h] is non empty set

{x,h} is non empty set

{x} is non empty trivial set

{{x,h},{x}} is non empty set

[h,x] is non empty set

{h,x} is non empty set

{h} is non empty trivial set

{{h,x},{h}} is non empty set

f is set

g is set

[:f,g:] is Relation-like set

h is Relation-like Function-like set

dom h is set

(h) is Relation-like Function-like set

((h)) is Relation-like Function-like set

dom ((h)) is set

x is set

y is set

b is set

[y,b] is non empty set

{y,b} is non empty set

{y} is non empty trivial set

{{y,b},{y}} is non empty set

[b,y] is non empty set

{b,y} is non empty set

{b} is non empty trivial set

{{b,y},{b}} is non empty set

dom (h) is set

f is set

g is set

[:f,g:] is Relation-like set

h is set

[:[:f,g:],h:] is Relation-like set

bool [:[:f,g:],h:] is set

x is Relation-like [:f,g:] -defined h -valued Function-like Element of bool [:[:f,g:],h:]

(x) is Relation-like Function-like set

((x)) is Relation-like Function-like set

dom x is Relation-like f -defined g -valued Element of bool [:f,g:]

bool [:f,g:] is set

f is Relation-like Function-like set

dom f is set

g is Relation-like Function-like set

dom g is set

union (dom f) is set

union (union (dom f)) is set

h is set

x is set

union (dom g) is set

union (union (dom g)) is set

y is set

b is set

[:h,y:] is Relation-like set

[:x,b:] is Relation-like set

[:[:h,y:],[:x,b:]:] is Relation-like set

z is set

nm is set

R is set

y is set

y9 is set

x9 is set

[y9,x9] is non empty set

{y9,x9} is non empty set

{y9} is non empty trivial set

{{y9,x9},{y9}} is non empty set

x is set

y1 is set

[x,y1] is non empty set

{x,y1} is non empty set

{x} is non empty trivial set

{{x,y1},{x}} is non empty set

[[y9,x9],[x,y1]] is non empty set

{[y9,x9],[x,y1]} is Relation-like non empty set

{[y9,x9]} is Relation-like Function-like constant non empty trivial set

{{[y9,x9],[x,y1]},{[y9,x9]}} is non empty set

[y9,x] is non empty set

{y9,x} is non empty set

{{y9,x},{y9}} is non empty set

f . [y9,x] is set

[x9,y1] is non empty set

{x9,y1} is non empty set

{x9} is non empty trivial set

{{x9,y1},{x9}} is non empty set

g . [x9,y1] is set

[(f . [y9,x]),(g . [x9,y1])] is non empty set

{(f . [y9,x]),(g . [x9,y1])} is non empty set

{(f . [y9,x])} is non empty trivial set

{{(f . [y9,x]),(g . [x9,y1])},{(f . [y9,x])}} is non empty set

x19 is set

x19 is set

[x19,x19] is non empty set

{x19,x19} is non empty set

{x19} is non empty trivial set

{{x19,x19},{x19}} is non empty set

y19 is set

y19 is set

[y19,y19] is non empty set

{y19,y19} is non empty set

{y19} is non empty trivial set

{{y19,y19},{y19}} is non empty set

[[x19,x19],[y19,y19]] is non empty set

{[x19,x19],[y19,y19]} is Relation-like non empty set

{[x19,x19]} is Relation-like Function-like constant non empty trivial set

{{[x19,x19],[y19,y19]},{[x19,x19]}} is non empty set

[x19,y19] is non empty set

{x19,y19} is non empty set

{{x19,y19},{x19}} is non empty set

f . [x19,y19] is set

[x19,y19] is non empty set

{x19,y19} is non empty set

{x19} is non empty trivial set

{{x19,y19},{x19}} is non empty set

g . [x19,y19] is set

[(f . [x19,y19]),(g . [x19,y19])] is non empty set

{(f . [x19,y19]),(g . [x19,y19])} is non empty set

{(f . [x19,y19])} is non empty trivial set

{{(f . [x19,y19]),(g . [x19,y19])},{(f . [x19,y19])}} is non empty set

nm is set

R is set

y9 is set

[R,y9] is non empty set

{R,y9} is non empty set

{R} is non empty trivial set

{{R,y9},{R}} is non empty set

y is set

x 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

[[R,y9],[y,x]] is non empty set

{[R,y9],[y,x]} is Relation-like non empty set

{[R,y9]} is Relation-like Function-like constant non empty trivial set

{{[R,y9],[y,x]},{[R,y9]}} is non empty set

[R,y] is non empty set

{R,y} is non empty set

{{R,y},{R}} is non empty set

[y9,x] is non empty set

{y9,x} is non empty set

{y9} is non empty trivial set

{{y9,x},{y9}} is non empty set

f . [R,y] is set

g . [y9,x] is set

[(f . [R,y]),(g . [y9,x])] is non empty set

{(f . [R,y]),(g . [y9,x])} is non empty set

{(f . [R,y])} is non empty trivial set

{{(f . [R,y]),(g . [y9,x])},{(f . [R,y])}} is non empty set

nm is Relation-like Function-like set

dom nm is set

R is set

y is set

x 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

y9 is set

x9 is set

[y9,x9] is non empty set

{y9,x9} is non empty set

{y9} is non empty trivial set

{{y9,x9},{y9}} is non empty set

[[y,x],[y9,x9]] is non empty set

{[y,x],[y9,x9]} is Relation-like non empty set

{[y,x]} is Relation-like Function-like constant non empty trivial set

{{[y,x],[y9,x9]},{[y,x]}} is non empty set

[y,y9] is non empty set

{y,y9} is non empty set

{{y,y9},{y}} is non empty set

[x,x9] is non empty set

{x,x9} is non empty set

{x} is non empty trivial set

{{x,x9},{x}} is non empty set

R is set

y is set

[R,y] is non empty set

{R,y} is non empty set

{R} is non empty trivial set

{{R,y},{R}} is non empty set

f . (R,y) is set

f . [R,y] is set

y9 is set

[R,y9] is non empty set

{R,y9} is non empty set

{{R,y9},{R}} is non empty set

x is set

[y9,x] is non empty set

{y9,x} is non empty set

{y9} is non empty trivial set

{{y9,x},{y9}} 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

nm . ([R,y9],[y,x]) is set

[[R,y9],[y,x]] is non empty set

{[R,y9],[y,x]} is Relation-like non empty set

{[R,y9]} is Relation-like Function-like constant non empty trivial set

{{[R,y9],[y,x]},{[R,y9]}} is non empty set

nm . [[R,y9],[y,x]] is set

g . (y9,x) is set

g . [y9,x] is set

[(f . (R,y)),(g . (y9,x))] is non empty set

{(f . (R,y)),(g . (y9,x))} is non empty set

{(f . (R,y))} is non empty trivial set

{{(f . (R,y)),(g . (y9,x))},{(f . (R,y))}} is non empty set

x9 is set

x19 is set

[x9,x19] is non empty set

{x9,x19} is non empty set

{x9} is non empty trivial set

{{x9,x19},{x9}} is non empty set

y1 is set

y19 is set

[y1,y19] is non empty set

{y1,y19} is non empty set

{y1} is non empty trivial set

{{y1,y19},{y1}} is non empty set

[[x9,x19],[y1,y19]] is non empty set

{[x9,x19],[y1,y19]} is Relation-like non empty set

{[x9,x19]} is Relation-like Function-like constant non empty trivial set

{{[x9,x19],[y1,y19]},{[x9,x19]}} is non empty set

[x9,y1] is non empty set

{x9,y1} is non empty set

{{x9,y1},{x9}} is non empty set

f . [x9,y1] is set

[x19,y19] is non empty set

{x19,y19} is non empty set

{x19} is non empty trivial set

{{x19,y19},{x19}} is non empty set

g . [x19,y19] is set

[(f . [x9,y1]),(g . [x19,y19])] is non empty set

{(f . [x9,y1]),(g . [x19,y19])} is non empty set

{(f . [x9,y1])} is non empty trivial set

{{(f . [x9,y1]),(g . [x19,y19])},{(f . [x9,y1])}} is non empty set

h is Relation-like Function-like set

dom h is set

x is Relation-like Function-like set

dom x is set

y is set

h . y is set

x . y is set

b is set

nm is set

[b,nm] is non empty set

{b,nm} is non empty set

{b} is non empty trivial set

{{b,nm},{b}} is non empty set

z is set

R is set

[z,R] is non empty set

{z,R} is non empty set

{z} is non empty trivial set

{{z,R},{z}} is non empty set

[[b,nm],[z,R]] is non empty set

{[b,nm],[z,R]} is Relation-like non empty set

{[b,nm]} is Relation-like Function-like constant non empty trivial set

{{[b,nm],[z,R]},{[b,nm]}} is non empty set

[b,z] is non empty set

{b,z} is non empty set

{{b,z},{b}} is non empty set

[nm,R] is non empty set

{nm,R} is non empty set

{nm} is non empty trivial set

{{nm,R},{nm}} is non empty set

h . ([b,nm],[z,R]) is set

h . [[b,nm],[z,R]] is set

f . (b,z) is set

f . [b,z] is set

g . (nm,R) is set

g . [nm,R] is set

[(f . (b,z)),(g . (nm,R))] is non empty set

{(f . (b,z)),(g . (nm,R))} is non empty set

{(f . (b,z))} is non empty trivial set

{{(f . (b,z)),(g . (nm,R))},{(f . (b,z))}} is non empty set

x . ([b,nm],[z,R]) is set

x . [[b,nm],[z,R]] is set

y is set

b is set

nm is set

[b,nm] is non empty set

{b,nm} is non empty set

{b} is non empty trivial set

{{b,nm},{b}} is non empty set

z is set

R is set

[z,R] is non empty set

{z,R} is non empty set

{z} is non empty trivial set

{{z,R},{z}} is non empty set

[[b,nm],[z,R]] is non empty set

{[b,nm],[z,R]} is Relation-like non empty set

{[b,nm]} is Relation-like Function-like constant non empty trivial set

{{[b,nm],[z,R]},{[b,nm]}} is non empty set

[b,z] is non empty set

{b,z} is non empty set

{{b,z},{b}} is non empty set

[nm,R] is non empty set

{nm,R} is non empty set

{nm} is non empty trivial set

{{nm,R},{nm}} is non empty set

b is set

nm is set

[b,nm] is non empty set

{b,nm} is non empty set

{b} is non empty trivial set

{{b,nm},{b}} is non empty set

z is set

R is set

[z,R] is non empty set

{z,R} is non empty set

{z} is non empty trivial set

{{z,R},{z}} is non empty set

[[b,nm],[z,R]] is non empty set

{[b,nm],[z,R]} is Relation-like non empty set

{[b,nm]} is Relation-like Function-like constant non empty trivial set

{{[b,nm],[z,R]},{[b,nm]}} is non empty set

[b,z] is non empty set

{b,z} is non empty set

{{b,z},{b}} is non empty set

[nm,R] is non empty set

{nm,R} is non empty set

{nm} is non empty trivial set

{{nm,R},{nm}} is non empty set

f is set

g is set

[f,g] is non empty set

{f,g} is non empty set

{f} is non empty trivial set

{{f,g},{f}} is non empty set

h is set

[f,h] is non empty set

{f,h} is non empty set

{{f,h},{f}} is non empty set

x is set

[h,x] is non empty set

{h,x} is non empty set

{h} is non empty trivial set

{{h,x},{h}} is non empty set

[[f,g],[h,x]] is non empty set

{[f,g],[h,x]} is Relation-like non empty set

{[f,g]} is Relation-like Function-like constant non empty trivial set

{{[f,g],[h,x]},{[f,g]}} 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

y is Relation-like Function-like set

dom y is set

b is Relation-like Function-like set

(y,b) is Relation-like Function-like set

dom (y,b) is set

dom b is set

z is set

R is set

[z,R] is non empty set

{z,R} is non empty set

{z} is non empty trivial set

{{z,R},{z}} is non empty set

nm is set

y is set

[nm,y] is non empty set

{nm,y} is non empty set

{nm} is non empty trivial set

{{nm,y},{nm}} is non empty set

[[z,R],[nm,y]] is non empty set

{[z,R],[nm,y]} is Relation-like non empty set

{[z,R]} is Relation-like Function-like constant non empty trivial set

{{[z,R],[nm,y]},{[z,R]}} is non empty set

[z,nm] is non empty set

{z,nm} is non empty set

{{z,nm},{z}} is non empty set

[R,y] is non empty set

{R,y} is non empty set

{R} is non empty trivial set

{{R,y},{R}} is non empty set

f is set

g is set

[f,g] is non empty set

{f,g} is non empty set

{f} is non empty trivial set

{{f,g},{f}} is non empty set

h is set

x is set

[h,x] is non empty set

{h,x} is non empty set

{h} is non empty trivial set

{{h,x},{h}} is non empty set

[[f,g],[h,x]] is non empty set

{[f,g],[h,x]} is Relation-like non empty set

{[f,g]} is Relation-like Function-like constant non empty trivial set

{{[f,g],[h,x]},{[f,g]}} is non empty set

y is Relation-like Function-like set

y . (f,h) is set

[f,h] is non empty set

{f,h} is non empty set

{{f,h},{f}} is non empty set

y . [f,h] is set

b is Relation-like Function-like set

(y,b) is Relation-like Function-like set

dom (y,b) is set

(y,b) . ([f,g],[h,x]) is set

(y,b) . [[f,g],[h,x]] is set

b . (g,x) is 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

b . [g,x] is set

[(y . (f,h)),(b . (g,x))] is non empty set

{(y . (f,h)),(b . (g,x))} is non empty set

{(y . (f,h))} is non empty trivial set

{{(y . (f,h)),(b . (g,x))},{(y . (f,h))}} is non empty set

dom y is set

dom b is set

f is Relation-like Function-like set

rng f is set

g is Relation-like Function-like set

(f,g) is Relation-like Function-like set

rng (f,g) is set

rng g is set

[:(rng f),(rng g):] is Relation-like set

h is set

dom (f,g) is set

x is set

(f,g) . x is set

dom f is set

dom g is set

y is set

z is set

[y,z] is non empty set

{y,z} is non empty set

{y} is non empty trivial set

{{y,z},{y}} is non empty set

b is set

nm is set

[b,nm] is non empty set

{b,nm} is non empty set

{b} is non empty trivial set

{{b,nm},{b}} is non empty set

[[y,z],[b,nm]] is non empty set

{[y,z],[b,nm]} is Relation-like non empty set

{[y,z]} is Relation-like Function-like constant non empty trivial set

{{[y,z],[b,nm]},{[y,z]}} is non empty set

[y,b] is non empty set

{y,b} is non empty set

{{y,b},{y}} is non empty set

[z,nm] is non empty set

{z,nm} is non empty set

{z} is non empty trivial set

{{z,nm},{z}} is non empty set

f . [y,b] is set

g . [z,nm] is set

(f,g) . ([y,z],[b,nm]) is set

(f,g) . [[y,z],[b,nm]] is set

f . (y,b) is set

g . (z,nm) is set

[(f . (y,b)),(g . (z,nm))] is non empty set

{(f . (y,b)),(g . (z,nm))} is non empty set

{(f . (y,b))} is non empty trivial set

{{(f . (y,b)),(g . (z,nm))},{(f . (y,b))}} is non empty set

f is set

g is set

[:f,g:] is Relation-like set

h is set

[:f,h:] is Relation-like set

x is set

[:h,x:] is Relation-like set

[:g,x:] is Relation-like set

[:[:f,h:],[:g,x:]:] is Relation-like set

y is Relation-like Function-like set

dom y is set

b is Relation-like Function-like set

dom b is set

(y,b) is Relation-like Function-like set

dom (y,b) is set

z is set

nm is set

y is set

[nm,y] is non empty set

{nm,y} is non empty set

{nm} is non empty trivial set

{{nm,y},{nm}} is non empty set

R is set

y9 is set

[R,y9] is non empty set

{R,y9} is non empty set

{R} is non empty trivial set

{{R,y9},{R}} is non empty set

[[nm,y],[R,y9]] is non empty set

{[nm,y],[R,y9]} is Relation-like non empty set

{[nm,y]} is Relation-like Function-like constant non empty trivial set

{{[nm,y],[R,y9]},{[nm,y]}} is non empty set

[nm,R] is non empty set

{nm,R} is non empty set

{{nm,R},{nm}} is non empty set

[y,y9] is non empty set

{y,y9} is non empty set

{y} is non empty trivial set

{{y,y9},{y}} is non empty set

f is set

g is set

[:f,g:] is Relation-like set

h is set

[:f,h:] is Relation-like set

x is set

[:h,x:] is Relation-like set

[:g,x:] is Relation-like set

[:[:f,h:],[:g,x:]:] is Relation-like set

y is Relation-like Function-like set

dom y is set

b is Relation-like Function-like set

dom b is set

(y,b) is Relation-like Function-like set

dom (y,b) is set

z is set

nm is set

R is set

[nm,R] is non empty set

{nm,R} is non empty set

{nm} is non empty trivial set

{{nm,R},{nm}} is non empty set

y is set

y9 is set

[y,y9] is non empty set

{y,y9} is non empty set

{y} is non empty trivial set

{{y,y9},{y}} is non empty set

x is set

x9 is set

[x,x9] is non empty set

{x,x9} is non empty set

{x} is non empty trivial set

{{x,x9},{x}} is non empty set

[x,y] is non empty set

{x,y} is non empty set

{{x,y},{x}} is non empty set

[x9,y9] is non empty set

{x9,y9} is non empty set

{x9} is non empty trivial set

{{x9,y9},{x9}} is non empty set

f is set

g is set

[:f,g:] is Relation-like set

h is set

[:[:f,g:],h:] is Relation-like set

bool [:[:f,g:],h:] is set

x is set

[:f,x:] is Relation-like set

y is set

[:x,y:] is Relation-like set

[:g,y:] is Relation-like set

[:[:f,x:],[:g,y:]:] is Relation-like set

b is set

[:[:x,y:],b:] is Relation-like set

bool [:[:x,y:],b:] is set

[:h,b:] is Relation-like set

[:[:[:f,x:],[:g,y:]:],[:h,b:]:] is Relation-like set

bool [:[:[:f,x:],[:g,y:]:],[:h,b:]:] is set

z is Relation-like [:f,g:] -defined h -valued Function-like Element of bool [:[:f,g:],h:]

nm is Relation-like [:x,y:] -defined b -valued Function-like Element of bool [:[:x,y:],b:]

(z,nm) is Relation-like Function-like set

rng (z,nm) is set

rng z is Element of bool h

bool h is set

rng nm is Element of bool b

bool b is set

[:(rng z),(rng nm):] is Relation-like set

dom z is Relation-like f -defined g -valued Element of bool [:f,g:]

bool [:f,g:] is set

dom nm is Relation-like x -defined y -valued Element of bool [:x,y:]

bool [:x,y:] is set

dom (z,nm) is set

f is set

g is set

[:f,g:] is Relation-like set

h is set

[:[:f,g:],h:] is Relation-like set

bool [:[:f,g:],h:] is set

x is set

[:f,x:] is Relation-like set

y is set

[:x,y:] is Relation-like set

[:g,y:] is Relation-like set

[:[:f,x:],[:g,y:]:] is Relation-like set

b is set

[:[:x,y:],b:] is Relation-like set

bool [:[:x,y:],b:] is set

[:h,b:] is Relation-like set

[:[:[:f,x:],[:g,y:]:],[:h,b:]:] is Relation-like set

bool [:[:[:f,x:],[:g,y:]:],[:h,b:]:] is set

z is Relation-like [:f,g:] -defined h -valued Function-like quasi_total Element of bool [:[:f,g:],h:]

nm is Relation-like [:x,y:] -defined b -valued Function-like quasi_total Element of bool [:[:x,y:],b:]

(z,nm) is Relation-like Function-like set

rng (z,nm) is set

rng z is Element of bool h

bool h is set

rng nm is Element of bool b

bool b is set

[:(rng z),(rng nm):] is Relation-like set

dom z is Relation-like f -defined g -valued Element of