:: FUNCT_2 semantic presentation

{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
proj1 {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
proj2 {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial with_non-empty_elements set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
g is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Element of bool [:x,A:]
dom f is Element of bool x
bool x is non empty set
x is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like non-empty empty-yielding x -defined A -valued Function-like one-to-one constant functional empty total (x,A) Element of bool [:x,A:]
x is set
A is non empty set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Element of bool [:x,A:]
dom f is Element of bool x
bool x is non empty set
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Element of bool [:x,x:]
A is Relation-like x -defined x -valued Element of bool [:x,x:]
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
[:(proj1 x),(proj2 x):] is Relation-like set
bool [:(proj1 x),(proj2 x):] is non empty set
A is Relation-like proj1 x -defined proj2 x -valued Element of bool [:(proj1 x),(proj2 x):]
rng A is Element of bool (proj2 x)
bool (proj2 x) is non empty set
x is set
A is Relation-like Function-like set
proj2 A is set
proj1 A is set
[:(proj1 A),x:] is Relation-like set
bool [:(proj1 A),x:] is non empty set
f is Relation-like proj1 A -defined x -valued Element of bool [:(proj1 A),x:]
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
g is set
y is set
f . y is set
[:(proj1 f),A:] is Relation-like set
bool [:(proj1 f),A:] is non empty set
g is Relation-like proj1 f -defined A -valued Element of bool [:(proj1 f),A:]
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g . f is set
rng g is Element of bool A
bool A is non empty set
dom g is Element of bool x
bool x is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g . f is set
rng g is Element of bool A
bool A is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
rng g is Element of bool A
bool A is non empty set
dom g is Element of bool x
bool x is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
F₁() is set
F₂() is set
[:F₁(),F₂():] is Relation-like set
bool [:F₁(),F₂():] is non empty set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
A is Relation-like F₁() -defined F₂() -valued Function-like (F₁(),F₂()) Element of bool [:F₁(),F₂():]
f is set
A . f is set
F₁() is set
F₂() is set
[:F₁(),F₂():] is Relation-like set
bool [:F₁(),F₂():] is non empty set
x is set
F₃(x) is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty Element of bool (bool [:x,A:])
bool [:x,A:] is non empty set
bool (bool [:x,A:]) is non empty set
f is set
g is set
y is Relation-like Function-like set
proj1 y is set
proj2 y is set
g is set
a is set
a is set
[a,a] is V23() set
{a,a} is non empty set
{a} is non empty set
{{a,a},{a}} is non empty set
y . a is set
f is set
g is set
y is set
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
(x,A) is set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
dom f is Element of bool x
bool x is non empty set
rng f is Element of bool A
bool A is non empty set
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
(x,x) is set
x is set
A is non empty set
(x,A) is set
x is set
(x,x) is set
x is non empty set
A is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
(x,A) is set
the Element of (x,A) is Element of (x,A)
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
rng f is Element of bool A
bool A is non empty set
g is set
dom f is Element of bool x
bool x is non empty set
y is set
f . y is set
y is set
f . y is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
rng g is Element of bool A
bool A is non empty set
dom g is Element of bool x
bool x is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
dom f is Element of bool x
bool x is non empty set
dom g is Element of bool x
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
g is Relation-like x -defined A -valued (x,A) Element of bool [:x,A:]
y is Relation-like A -defined f -valued (A,f) Element of bool [:A,f:]
g * y is Relation-like x -defined f -valued Element of bool [:x,f:]
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
dom (g * y) is Element of bool x
bool x is non empty set
dom y is Element of bool A
bool A is non empty set
dom g is Element of bool x
rng g is Element of bool A
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
rng g is Element of bool A
bool A is non empty set
y is Relation-like A -defined f -valued Function-like (A,f) Element of bool [:A,f:]
rng y is Element of bool f
bool f is non empty set
y * g is Relation-like x -defined f -valued Function-like Element of bool [:x,f:]
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
rng (y * g) is Element of bool f
dom y is Element of bool A
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g . f is set
y is Relation-like Function-like set
g * y is Relation-like x -defined Function-like set
(g * y) . f is set
y . (g . f) is set
dom g is Element of bool x
bool x is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
rng f is Element of bool A
bool A is non empty set
g is set
[:A,g:] is Relation-like set
bool [:A,g:] is non empty set
y is Relation-like A -defined g -valued Function-like (A,g) Element of bool [:A,g:]
y * f is Relation-like x -defined g -valued Function-like Element of bool [:x,g:]
[:x,g:] is Relation-like set
bool [:x,g:] is non empty set
g is Relation-like A -defined g -valued Function-like (A,g) Element of bool [:A,g:]
g * f is Relation-like x -defined g -valued Function-like Element of bool [:x,g:]
dom y is Element of bool A
dom g is Element of bool A
g is Relation-like Function-like set
proj1 g is set
y is Relation-like Function-like set
proj1 y is set
f * g is Relation-like x -defined Function-like set
f * y is Relation-like x -defined Function-like set
proj2 g is set
proj2 y is set
(proj2 g) \/ (proj2 y) is set
[:A,((proj2 g) \/ (proj2 y)):] is Relation-like set
bool [:A,((proj2 g) \/ (proj2 y)):] is non empty set
x is set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (x,x) Element of bool [:x,x:]
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
id A is Relation-like A -defined A -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (A,A) Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
f is Relation-like x -defined A -valued Element of bool [:x,A:]
(id x) * f is Relation-like x -defined A -valued Element of bool [:x,A:]
f * (id A) is Relation-like x -defined A -valued Element of bool [:x,A:]
dom f is Element of bool x
bool x is non empty set
rng f is Element of bool A
bool A is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
[:A,x:] is Relation-like set
bool [:A,x:] is non empty set
id A is Relation-like A -defined A -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (A,A) Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
rng f is Element of bool A
bool A is non empty set
g is Relation-like A -defined x -valued Function-like (A,x) Element of bool [:A,x:]
f * g is Relation-like A -defined A -valued Function-like Element of bool [:A,A:]
rng (f * g) is Element of bool A
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
dom f is Element of bool x
bool x is non empty set
g is set
y is set
f . g is set
f . y is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
y is Relation-like A -defined f -valued Function-like (A,f) Element of bool [:A,f:]
y * g is Relation-like x -defined f -valued Function-like Element of bool [:x,f:]
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
dom y is Element of bool A
bool A is non empty set
rng g is Element of bool A
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
dom f is Element of bool x
bool x is non empty set
g is set
[:g,x:] is Relation-like set
bool [:g,x:] is non empty set
y is Relation-like g -defined x -valued Function-like (g,x) Element of bool [:g,x:]
f * y is Relation-like g -defined A -valued Function-like Element of bool [:g,A:]
[:g,A:] is Relation-like set
bool [:g,A:] is non empty set
g is Relation-like g -defined x -valued Function-like (g,x) Element of bool [:g,x:]
f * g is Relation-like g -defined A -valued Function-like Element of bool [:g,A:]
rng y is Element of bool x
rng g is Element of bool x
dom y is Element of bool g
bool g is non empty set
dom g is Element of bool g
g is Relation-like Function-like set
proj2 g is set
y is Relation-like Function-like set
proj2 y is set
proj1 g is set
proj1 y is set
[:(proj1 g),x:] is Relation-like set
bool [:(proj1 g),x:] is non empty set
g * f is Relation-like A -valued Function-like set
y * f is Relation-like A -valued Function-like set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
rng g is Element of bool A
bool A is non empty set
y is Relation-like A -defined f -valued Function-like (A,f) Element of bool [:A,f:]
y * g is Relation-like x -defined f -valued Function-like Element of bool [:x,f:]
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
rng (y * g) is Element of bool f
bool f is non empty set
dom y is Element of bool A
rng y is Element of bool f
x is set
x is set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (x,x) Element of bool [:x,x:]
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
[:A,x:] is Relation-like set
bool [:A,x:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g is Relation-like A -defined x -valued Function-like (A,x) Element of bool [:A,x:]
g * f is Relation-like x -defined x -valued Function-like Element of bool [:x,x:]
dom f is Element of bool x
bool x is non empty set
rng (g * f) is Element of bool x
bool x is non empty set
rng g is Element of bool x
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
rng g is Element of bool A
bool A is non empty set
y is Relation-like A -defined f -valued Function-like (A,f) Element of bool [:A,f:]
y * g is Relation-like x -defined f -valued Function-like Element of bool [:x,f:]
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
dom y is Element of bool A
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
[:A,x:] is Relation-like set
bool [:A,x:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
rng f is Element of bool A
bool A is non empty set
f " is Relation-like Function-like set
proj2 (f ") is set
g is set
dom f is Element of bool x
bool x is non empty set
proj1 (f ") is set
g is Relation-like A -defined x -valued Element of bool [:A,x:]
dom g is Element of bool A
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g " is Relation-like Function-like set
g . f is set
(g ") . (g . f) is set
dom g is Element of bool x
bool x is non empty set
x is set
A is non empty set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is non empty set
[:A,f:] is Relation-like non empty set
bool [:A,f:] is non empty set
g is Relation-like x -defined A -valued Function-like total (x,A) Element of bool [:x,A:]
y is Relation-like A -defined f -valued Function-like total (A,f) Element of bool [:A,f:]
y * g is Relation-like x -defined f -valued Function-like Element of bool [:x,f:]
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
rng g is Element of bool A
bool A is non empty set
dom y is Element of bool A
rng (y * g) is Element of bool f
bool f is non empty set
rng y is Element of bool f
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
[:A,x:] is Relation-like set
bool [:A,x:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
rng f is Element of bool A
bool A is non empty set
f " is Relation-like Function-like set
g is Relation-like A -defined x -valued Function-like (A,x) Element of bool [:A,x:]
dom f is Element of bool x
bool x is non empty set
dom g is Element of bool A
x is set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (x,x) Element of bool [:x,x:]
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
id A is Relation-like A -defined A -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (A,A) Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
rng f is Element of bool A
bool A is non empty set
f " is Relation-like Function-like set
f * (f ") is Relation-like x -defined Function-like set
(f ") * f is Relation-like A -valued Function-like set
dom f is Element of bool x
bool x is non empty set
x is set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (x,x) Element of bool [:x,x:]
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
[:A,x:] is Relation-like set
bool [:A,x:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
rng f is Element of bool A
bool A is non empty set
f " is Relation-like Function-like set
g is Relation-like A -defined x -valued Function-like (A,x) Element of bool [:A,x:]
g * f is Relation-like x -defined x -valued Function-like Element of bool [:x,x:]
dom f is Element of bool x
bool x is non empty set
dom g is Element of bool A
x is set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (x,x) Element of bool [:x,x:]
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
[:A,x:] is Relation-like set
bool [:A,x:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
dom f is Element of bool x
bool x is non empty set
g is Relation-like A -defined x -valued Function-like (A,x) Element of bool [:A,x:]
g * f is Relation-like x -defined x -valued Function-like Element of bool [:x,x:]
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
[:f,A:] is Relation-like set
bool [:f,A:] is non empty set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g | f is Relation-like x -defined f -defined x -defined A -valued Function-like Element of bool [:x,A:]
dom g is Element of bool x
bool x is non empty set
dom (g | f) is Element of bool x
rng (g | f) is Element of bool A
bool A is non empty set
y is Relation-like f -defined A -valued Element of bool [:f,A:]
dom y is Element of bool f
bool f is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g | f is Relation-like x -defined f -defined x -defined A -valued Function-like Element of bool [:x,A:]
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is set
y is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
y . f is set
g |` y is Relation-like x -defined A -valued g -valued A -valued Function-like Element of bool [:x,A:]
(g |` y) . f is set
dom y is Element of bool x
bool x is non empty set
dom (g |` y) is Element of bool x
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g .: f is Element of bool A
bool A is non empty set
dom g is Element of bool x
bool x is non empty set
y is set
g is set
g . g is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
f is set
g .: f is Element of bool A
bool A is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g " f is Element of bool x
bool x is non empty set
dom g is Element of bool x
y is set
g . y is set
g is set
g . g is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
g is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
f is set
g " f is Element of bool x
bool x is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
f " A is Element of bool x
bool x is non empty set
rng f is Element of bool A
bool A is non empty set
(rng f) /\ A is Element of bool A
f " (rng f) is Element of bool x
dom f is Element of bool x
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
rng f is Element of bool A
bool A is non empty set
g is set
{g} is non empty set
f " {g} is Element of bool x
bool x is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g .: f is Element of bool A
bool A is non empty set
g " (g .: f) is Element of bool x
bool x is non empty set
dom g is Element of bool x
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
f .: x is Element of bool A
bool A is non empty set
f " (f .: x) is Element of bool x
bool x is non empty set
dom f is Element of bool x
rng f is Element of bool A
f " (rng f) is Element of bool x
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
g is set
y is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
y " g is Element of bool x
bool x is non empty set
g is Relation-like A -defined f -valued Function-like (A,f) Element of bool [:A,f:]
g * y is Relation-like x -defined f -valued Function-like Element of bool [:x,f:]
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
g .: g is Element of bool f
bool f is non empty set
(g * y) " (g .: g) is Element of bool x
dom g is Element of bool A
bool A is non empty set
rng y is Element of bool A
x is set
[:{},x:] is Relation-like set
bool [:{},x:] is non empty set
f is Relation-like non-empty empty-yielding {} -defined x -valued Function-like one-to-one constant functional empty total ( {} ,x) Element of bool [:{},x:]
A is set
f .: A is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Element of bool x
bool x is non empty set
x is set
[:{},x:] is Relation-like set
bool [:{},x:] is non empty set
f is Relation-like non-empty empty-yielding {} -defined x -valued Function-like one-to-one constant functional empty total ( {} ,x) Element of bool [:{},x:]
A is set
f " A is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty non proper Element of bool {}
bool {} is non empty set
x is set
{x} is non empty set
A is set
[:{x},A:] is Relation-like set
bool [:{x},A:] is non empty set
f is Relation-like {x} -defined A -valued Function-like ({x},A) Element of bool [:{x},A:]
f . x is set
dom f is Element of bool {x}
bool {x} is non empty set
rng f is Element of bool A
bool A is non empty set
{(f . x)} is non empty set
x is set
{x} is non empty set
A is set
[:{x},A:] is Relation-like set
bool [:{x},A:] is non empty set
f is Relation-like {x} -defined A -valued Function-like ({x},A) Element of bool [:{x},A:]
rng f is Element of bool A
bool A is non empty set
f . x is set
{(f . x)} is non empty set
dom f is Element of bool {x}
bool {x} is non empty set
x is set
{x} is non empty set
A is set
[:{x},A:] is Relation-like set
bool [:{x},A:] is non empty set
f is set
g is Relation-like {x} -defined A -valued Function-like ({x},A) Element of bool [:{x},A:]
g .: f is Element of bool A
bool A is non empty set
g . x is set
{(g . x)} is non empty set
rng g is Element of bool A
x is set
A is set
{A} is non empty set
[:x,{A}:] is Relation-like set
bool [:x,{A}:] is non empty set
f is set
g is Relation-like x -defined {A} -valued Function-like total (x,{A}) Element of bool [:x,{A}:]
g . f is set
x is set
A is set
{A} is non empty set
[:x,{A}:] is Relation-like set
bool [:x,{A}:] is non empty set
f is Relation-like x -defined {A} -valued Function-like total (x,{A}) Element of bool [:x,{A}:]
g is Relation-like x -defined {A} -valued Function-like total (x,{A}) Element of bool [:x,{A}:]
y is set
f . y is set
g . y is set
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
dom A is Element of bool x
bool x is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
g is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
f * g is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
y is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
dom f is Element of bool x
bool x is non empty set
dom (f * g) is Element of bool x
g " x is Element of bool x
dom g is Element of bool x
y is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
A is set
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
x is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
f is Relation-like A -defined A -valued Function-like total (A,A) Element of bool [:A,A:]
f * g is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
y is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
dom f is Element of bool A
bool A is non empty set
dom (f * g) is Element of bool x
bool x is non empty set
g " A is Element of bool x
dom g is Element of bool x
y is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Element of bool [:x,x:]
rng A is Element of bool x
bool x is non empty set
f is Relation-like x -defined x -valued Element of bool [:x,x:]
rng f is Element of bool x
f * A is Relation-like x -defined x -valued Element of bool [:x,x:]
rng (f * A) is Element of bool x
A .: x is Element of bool x
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (x,x) Element of bool [:x,x:]
A is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
f is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
f * A is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
rng A is Element of bool x
bool x is non empty set
dom f is Element of bool x
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (x,x) Element of bool [:x,x:]
f is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
A is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
A * f is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
rng f is Element of bool x
bool x is non empty set
dom A is Element of bool x
dom f is Element of bool x
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
dom A is Element of bool x
bool x is non empty set
f is set
g is set
A . f is set
A . g is set
x is set
A is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (x,x) Element of bool [:x,x:]
rng (id x) is Element of bool x
bool x is non empty set
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
rng A is Element of bool x
bool x is non empty set
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
f is set
g is set
A . f is set
A . g is set
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
f is Relation-like x -defined x -valued Function-like (x) Element of bool [:x,x:]
A is Relation-like x -defined x -valued Function-like (x) Element of bool [:x,x:]
A * f is Relation-like x -defined x -valued Function-like Element of bool [:x,x:]
rng A is Element of bool x
bool x is non empty set
rng f is Element of bool x
rng (A * f) is Element of bool x
g is Relation-like x -defined x -valued Function-like Element of bool [:x,x:]
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
f is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
f * A is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
g is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
field A is set
dom A is Element of bool x
bool x is non empty set
rng A is Element of bool x
(dom A) \/ (rng A) is Element of bool x
f is set
proj1 A is set
A . f is set
g is set
A . g is set
[f,f] is V23() set
{f,f} is non empty set
{f} is non empty set
{{f,f},{f}} is non empty set
[g,g] is V23() set
{g,g} is non empty set
{g} is non empty set
{{g,g},{g}} is non empty set
f is set
[f,f] is V23() set
{f,f} is non empty set
{f} is non empty set
{{f,f},{f}} is non empty set
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
A " is Relation-like Function-like one-to-one set
dom A is Element of bool x
bool x is non empty set
proj2 (A ") is set
rng A is Element of bool x
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
A is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
f is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
f * A is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
rng A is Element of bool x
bool x is non empty set
dom A is Element of bool x
dom f is Element of bool x
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
A is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
f is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
f * A is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
(x,A) is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
dom A is Element of bool x
bool x is non empty set
rng A is Element of bool x
dom f is Element of bool x
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
A is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
(x,A) is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
(x,A) * A is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
A * (x,A) is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
dom A is Element of bool x
bool x is non empty set
rng A is Element of bool x
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is set
f is Relation-like x -defined x -valued Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
f " A is Element of bool x
bool x is non empty set
f .: (f " A) is Element of bool x
f .: A is Element of bool x
f " (f .: A) is Element of bool x
dom f is Element of bool x
rng f is Element of bool x
x is set
A is non empty set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
g is Relation-like x -defined A -valued Function-like total (x,A) Element of bool [:x,A:]
y is Relation-like A -defined f -valued Function-like (A,f) Element of bool [:A,f:]
y * g is Relation-like x -defined f -valued Function-like Element of bool [:x,f:]
g is Relation-like x -defined f -valued Function-like Element of bool [:x,f:]
x is non empty set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g is Element of x
f . g is set
F<sub>1</sub>() is non empty set
F<sub>2</sub>() is non empty set
[:F<sub>1</sub>(),F<sub>2</sub>():] is Relation-like non empty set
bool [:F<sub>1</sub>(),F<sub>2</sub>():] is non empty set
x is set
A is Element of F<sub>2</sub>()
x is Relation-like F<sub>1</sub>() -defined F<sub>2</sub>() -valued Function-like total (F<sub>1</sub>(),F<sub>2</sub>()) Element of bool [:F<sub>1</sub>(),F<sub>2</sub>():]
A is Element of F<sub>1</sub>()
(F<sub>1</sub>(),F<sub>2</sub>(),x,A) is Element of F<sub>2</sub>()
F<sub>1</sub>() is non empty set
F<sub>2</sub>() is non empty set
[:F<sub>1</sub>(),F<sub>2</sub>():] is Relation-like non empty set
bool [:F<sub>1</sub>(),F<sub>2</sub>():] is non empty set
x is Element of F<sub>1</sub>()
F<sub>3</sub>(x) is Element of F<sub>2</sub>()
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
y is set
f . y is set
g . y is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g .: f is Element of bool A
bool A is non empty set
y is set
dom g is Element of bool x
bool x is non empty set
g is set
g . g is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g .: f is Element of bool A
bool A is non empty set
y is set
g is set
g . g is set
a is Element of x
g . a is set
x is set
A is set
(x,A) is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
F<sub>1</sub>() is set
F<sub>2</sub>() is set
[:F<sub>1</sub>(),F<sub>2</sub>():] is Relation-like set
bool [:F<sub>1</sub>(),F<sub>2</sub>():] is non empty set
the Element of F<sub>1</sub>() is Element of F<sub>1</sub>()
F<sub>3</sub>( the Element of F<sub>1</sub>()) is set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
A is set
f is set
x . f is set
F<sub>4</sub>(f) is set
F<sub>3</sub>(f) is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
dom f is Element of bool x
bool x is non empty set
rng f is Element of bool A
bool A is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
<:f,x,A:> is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
A |` f is Relation-like x -defined A -valued A -valued Function-like set
(A |` f) | x is Relation-like x -defined x -defined A -valued Function-like set
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
<:A,x,x:> is Relation-like x -defined x -valued Function-like Element of bool [:x,x:]
x |` A is Relation-like x -defined x -valued x -valued Function-like set
(x |` A) | x is Relation-like x -defined x -defined x -valued Function-like set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
dom f is Element of bool x
bool x is non empty set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
y is set
g . y is set
f . y is set
the Element of A is Element of A
y is set
f . y is set
y is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g is set
y . g is set
f . g is set
x is set
A is set
(x,A) is set
PFuncs (x,A) is functional non empty set
f is set
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
f is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
dom f is Element of bool x
bool x is non empty set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
dom g is Element of bool x
y is set
f . y is set
g . y is set
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like Element of bool [:x,x:]
dom A is Element of bool x
bool x is non empty set
f is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
g is set
A . g is set
f . g is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
dom f is Element of bool x
bool x is non empty set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like Element of bool [:x,x:]
g is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
f is Relation-like x -defined x -valued Function-like Element of bool [:x,x:]
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
g is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
y is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
TotFuncs f is set
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like Element of bool [:x,x:]
f is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
TotFuncs A is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
TotFuncs f is set
g is set
y is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
(x,A) is set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
TotFuncs f is set
g is set
x is set
A is set
<:{},x,A:> is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
A |` {} is Relation-like Function-like set
(A |` {}) | x is Relation-like Function-like set
TotFuncs <:{},x,A:> is set
(x,A) is set
f is set
g is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
<:f,x,A:> is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
A |` f is Relation-like x -defined A -valued A -valued Function-like set
(A |` f) | x is Relation-like x -defined x -defined A -valued Function-like set
TotFuncs <:f,x,A:> is set
{f} is functional non empty set
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
<:A,x,x:> is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]
x |` A is Relation-like x -defined x -valued x -valued Function-like set
(x |` A) | x is Relation-like x -defined x -defined x -valued Function-like set
TotFuncs <:A,x,x:> is set
{A} is functional non empty set
x is set
A is set
{A} is non empty set
[:x,{A}:] is Relation-like set
bool [:x,{A}:] is non empty set
f is Relation-like x -defined {A} -valued Function-like Element of bool [:x,{A}:]
TotFuncs f is set
g is Relation-like x -defined {A} -valued Function-like total (x,{A}) Element of bool [:x,{A}:]
{g} is functional non empty set
y is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
g is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
TotFuncs f is set
TotFuncs g is set
y is set
g is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
g is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
dom g is Element of bool x
bool x is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
dom f is Element of bool x
TotFuncs f is set
TotFuncs g is set
y is set
g . y is set
f . y is set
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
(dom f) /\ (dom g) is Element of bool x
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
TotFuncs f is set
g is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
TotFuncs g is set
dom g is Element of bool x
bool x is non empty set
dom f is Element of bool x
dom g is Element of bool x
bool x is non empty set
dom f is Element of bool x
y is set
g . y is set
{(g . y)} is non empty set
g is set
a is set
f . a is set
a is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
a is set
proj1 f is set
proj1 a is set
(proj1 f) /\ (proj1 a) is set
f . a is set
a . a is set
dom a is Element of bool x
(dom f) /\ (dom a) is Element of bool x
dom a is Element of bool x
(dom g) /\ (dom a) is Element of bool x
a . y is set
dom g is Element of bool x
bool x is non empty set
dom f is Element of bool x
dom g is Element of bool x
bool x is non empty set
dom f is Element of bool x
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
TotFuncs f is set
g is Relation-like x -defined A -valued Function-like Element of bool [:x,A:]
TotFuncs g is set
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like total (x,A) Element of bool [:x,A:]
F<sub>1</sub>() is non empty set
F<sub>2</sub>() is non empty set
[:F<sub>1</sub>(),F<sub>2</sub>():] is Relation-like non empty set
bool [:F<sub>1</sub>(),F<sub>2</sub>():] is non empty set
F<sub>3</sub>() is Element of F<sub>1</sub>()
F<sub>4</sub>() is Element of F<sub>2</sub>()
x is Element of F<sub>1</sub>()
F<sub>5</sub>(x) is Element of F<sub>2</sub>()
A is Element of F<sub>2</sub>()
x is Relation-like F<sub>1</sub>() -defined F<sub>2</sub>() -valued Function-like non empty total (F<sub>1</sub>(),F<sub>2</sub>()) Element of bool [:F<sub>1</sub>(),F<sub>2</sub>():]
(F<sub>1</sub>(),F<sub>2</sub>(),x,F<sub>3</sub>()) is Element of F<sub>2</sub>()
A is Element of F<sub>1</sub>()
(F<sub>1</sub>(),F<sub>2</sub>(),x,A) is Element of F<sub>2</sub>()
F<sub>5</sub>(A) is Element of F<sub>2</sub>()
F<sub>1</sub>() is non empty set
F<sub>2</sub>() is non empty set
F<sub>3</sub>() is Element of F<sub>1</sub>()
F<sub>4</sub>() is Element of F<sub>1</sub>()
[:F<sub>1</sub>(),F<sub>2</sub>():] is Relation-like non empty set
bool [:F<sub>1</sub>(),F<sub>2</sub>():] is non empty set
F<sub>5</sub>() is Element of F<sub>2</sub>()
F<sub>6</sub>() is Element of F<sub>2</sub>()
x is Element of F<sub>1</sub>()
F<sub>7</sub>(x) is Element of F<sub>2</sub>()
A is Element of F<sub>2</sub>()
f is Element of F<sub>2</sub>()
x is Relation-like F<sub>1</sub>() -defined F<sub>2</sub>() -valued Function-like non empty total (F<sub>1</sub>(),F<sub>2</sub>()) Element of bool [:F<sub>1</sub>(),F<sub>2</sub>():]
(F<sub>1</sub>(),F<sub>2</sub>(),x,F<sub>3</sub>()) is Element of F<sub>2</sub>()
(F<sub>1</sub>(),F<sub>2</sub>(),x,F<sub>4</sub>()) is Element of F<sub>2</sub>()
A is Element of F<sub>1</sub>()
(F<sub>1</sub>(),F<sub>2</sub>(),x,A) is Element of F<sub>2</sub>()
F<sub>7</sub>(A) is Element of F<sub>2</sub>()
x is set
A is set
(x,A) is set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
F<sub>1</sub>() is non empty set
F<sub>2</sub>() is set
[:F<sub>1</sub>(),F<sub>2</sub>():] is Relation-like set
bool [:F<sub>1</sub>(),F<sub>2</sub>():] is non empty set
x is set
F<sub>3</sub>(x) is set
x is Relation-like F<sub>1</sub>() -defined F<sub>2</sub>() -valued Function-like (F<sub>1</sub>(),F<sub>2</sub>()) Element of bool [:F<sub>1</sub>(),F<sub>2</sub>():]
x is Relation-like F<sub>1</sub>() -defined F<sub>2</sub>() -valued Function-like (F<sub>1</sub>(),F<sub>2</sub>()) Element of bool [:F<sub>1</sub>(),F<sub>2</sub>():]
A is Element of F<sub>1</sub>()
(F<sub>1</sub>(),F<sub>2</sub>(),x,A) is Element of F<sub>2</sub>()
F<sub>3</sub>(A) is set
F<sub>1</sub>() is non empty set
F<sub>2</sub>() is non empty set
[:F<sub>1</sub>(),F<sub>2</sub>():] is Relation-like non empty set
bool [:F<sub>1</sub>(),F<sub>2</sub>():] is non empty set
x is Element of F<sub>1</sub>()
F<sub>3</sub>(x) is set
x is Relation-like F<sub>1</sub>() -defined F<sub>2</sub>() -valued Function-like non empty total (F<sub>1</sub>(),F<sub>2</sub>()) Element of bool [:F<sub>1</sub>(),F<sub>2</sub>():]
A is Element of F<sub>1</sub>()
(F<sub>1</sub>(),F<sub>2</sub>(),x,A) is Element of F<sub>2</sub>()
F<sub>3</sub>(A) is set
x is non empty set
A is non empty set
f is non empty set
[:A,f:] is Relation-like non empty set
[:x,[:A,f:]:] is Relation-like non empty set
bool [:x,[:A,f:]:] is non empty set
g is Relation-like x -defined [:A,f:] -valued Function-like non empty total (x,[:A,f:]) Element of bool [:x,[:A,f:]:]
pr1 g is Relation-like Function-like set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
proj1 (pr1 g) is set
dom g is non empty Element of bool x
bool x is non empty set
proj2 (pr1 g) is set
y is set
g is set
(pr1 g) . g is set
g . g is set
(g . g) `1 is set
y is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
proj1 (pr1 g) is set
dom g is non empty Element of bool x
bool x is non empty set
g is Element of x
(x,A,y,g) is Element of A
(x,[:A,f:],g,g) is Element of [:A,f:]
(x,[:A,f:],g,g) `1 is set
g is set
y . g is set
g . g is set
(g . g) `1 is set
dom y is non empty Element of bool x
pr2 g is Relation-like Function-like set
[:x,f:] is Relation-like non empty set
bool [:x,f:] is non empty set
proj1 (pr2 g) is set
dom g is non empty Element of bool x
bool x is non empty set
proj2 (pr2 g) is set
y is set
g is set
(pr2 g) . g is set
g . g is set
(g . g) `2 is set
y is Relation-like x -defined f -valued Function-like non empty total (x,f) Element of bool [:x,f:]
proj1 (pr2 g) is set
dom g is non empty Element of bool x
bool x is non empty set
g is Element of x
(x,f,y,g) is Element of f
(x,[:A,f:],g,g) is Element of [:A,f:]
(x,[:A,f:],g,g) `2 is set
g is set
y . g is set
g . g is set
(g . g) `2 is set
dom y is non empty Element of bool x
x is set
A is non empty set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is non empty set
[:f,g:] is Relation-like set
bool [:f,g:] is non empty set
y is Relation-like x -defined A -valued Function-like total (x,A) Element of bool [:x,A:]
g is Relation-like f -defined g -valued Function-like total (f,g) Element of bool [:f,g:]
dom y is Element of bool x
bool x is non empty set
a is Element of x
y . a is set
g . a is set
dom g is Element of bool f
bool f is non empty set
a is set
y . a is set
g . a is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
y is Element of x
f . y is set
g . y is set
x is set
bool x is non empty Element of bool (bool x)
bool x is non empty set
bool (bool x) is non empty set
[:x,(bool x):] is Relation-like set
bool [:x,(bool x):] is non empty set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined bool x -valued Function-like total (x, bool x) Element of bool [:x,(bool x):]
[#] x is non proper Element of bool x
f is Element of x
A . f is set
[:([#] x),([#] x):] is Relation-like set
bool [:([#] x),([#] x):] is non empty set
f is Relation-like [#] x -defined [#] x -valued Element of bool [:([#] x),([#] x):]
g is Relation-like x -defined x -valued Element of bool [:x,x:]
y is set
Im (g,y) is set
A . y is set
x is set
bool x is non empty set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Element of bool x
(id x) " A is Element of bool x
(id x) .: A is Element of bool x
(id x) " ((id x) .: A) is Element of bool x
x is non empty set
bool x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
bool A is non empty set
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
g is Element of bool x
f .: g is Element of bool A
y is Element of bool A
f " y is Element of bool x
f " (f .: g) is Element of bool x
f .: (f " y) is Element of bool A
x is non empty set
bool x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
g is non empty Element of bool x
[:g,A:] is Relation-like non empty set
bool [:g,A:] is non empty set
f | g is Relation-like x -defined g -defined x -defined A -valued Function-like Element of bool [:x,A:]
y is Relation-like g -defined A -valued Function-like non empty total (g,A) Element of bool [:g,A:]
g is Relation-like g -defined A -valued Function-like non empty total (g,A) Element of bool [:g,A:]
a is Element of g
(g,A,g,a) is Element of A
(g,A,y,a) is Element of A
(x,A,f,a) is Element of A
x is Relation-like Function-like set
f is set
A is set
x .: f is set
x | A is Relation-like Function-like set
(x | A) .: f is set
id A is Relation-like A -defined A -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (A,A) (A) (A,A) Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
(id A) * x is Relation-like A -defined Function-like set
((id A) * x) .: f is set
(id A) .: f is Element of bool A
bool A is non empty set
x .: ((id A) .: f) is set
x is Relation-like Function-like set
f is set
x " f is set
A is set
x | A is Relation-like Function-like set
(x | A) " f is set
id A is Relation-like A -defined A -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (A,A) (A) (A,A) Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
(id A) * x is Relation-like A -defined Function-like set
((id A) * x) " f is set
(id A) " (x " f) is Element of bool A
bool A is non empty set
F<sub>1</sub>() is non empty set
F<sub>2</sub>() is non empty set
[:F<sub>1</sub>(),F<sub>2</sub>():] is Relation-like non empty set
bool [:F<sub>1</sub>(),F<sub>2</sub>():] is non empty set
x is set
F<sub>3</sub>(x) is set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
A is Relation-like F<sub>1</sub>() -defined F<sub>2</sub>() -valued Function-like non empty total (F<sub>1</sub>(),F<sub>2</sub>()) Element of bool [:F<sub>1</sub>(),F<sub>2</sub>():]
f is Element of F<sub>1</sub>()
(F<sub>1</sub>(),F<sub>2</sub>(),A,f) is Element of F<sub>2</sub>()
F<sub>3</sub>(f) is set
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
g is Element of x
f /. g is Element of A
(x,A,f,g) is Element of A
dom f is non empty Element of bool x
bool x is non empty set
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
g is Element of x
f /. g is Element of A
(x,A,f,g) is Element of A
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
bool A is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g is Element of bool A
f " g is Element of bool x
bool x is non empty set
(f " g) ` is Element of bool x
x \ (f " g) is set
g ` is Element of bool A
A \ g is set
f " (g `) is Element of bool x
g /\ (g `) is Element of bool A
(f " g) /\ (f " (g `)) is Element of bool x
{} A is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Element of bool A
f " ({} A) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Element of bool x
(f " g) \/ (f " (g `)) is Element of bool x
g \/ (g `) is Element of bool A
f " (g \/ (g `)) is Element of bool x
[#] A is non proper Element of bool A
f " ([#] A) is Element of bool x
[#] x is non proper Element of bool x
(f " (g `)) ` is Element of bool x
x \ (f " (g `)) is set
((f " g) `) /\ ((f " (g `)) `) is Element of bool x
([#] x) ` is Element of bool x
x \ ([#] x) is set
{} x is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Element of bool x
x is set
A is set
f is set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
g is non empty set
[:x,g:] is Relation-like set
bool [:x,g:] is non empty set
y is Relation-like x -defined g -valued Function-like total (x,g) Element of bool [:x,g:]
y .: A is Element of bool g
bool g is non empty set
y | A is Relation-like x -defined A -defined x -defined g -valued Function-like Element of bool [:x,g:]
dom y is Element of bool x
bool x is non empty set
dom (y | A) is Element of bool x
rng (y | A) is Element of bool g
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
bool A is non empty set
bool (bool A) is non empty set
bool x is non empty set
bool (bool x) is non empty set
g is Element of bool (bool A)
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
y is Element of bool (bool x)
y is Element of bool (bool x)
g is Element of bool (bool x)
a is set
a is Element of bool x
A2 is Element of bool A
f " A2 is Element of bool x
a is Element of bool x
A2 is Element of bool A
f " A2 is Element of bool x
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
bool A is non empty set
bool (bool A) is non empty set
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
g is Element of bool (bool A)
y is Element of bool (bool A)
(x,A,f,g) is Element of bool (bool x)
bool x is non empty set
bool (bool x) is non empty set
(x,A,f,y) is Element of bool (bool x)
g is set
a is Element of bool x
a is Element of bool A
f " a is Element of bool x
a is Element of bool A
f " a is Element of bool x
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
bool x is non empty set
bool (bool x) is non empty set
bool A is non empty set
bool (bool A) is non empty set
g is Element of bool (bool x)
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
y is Element of bool (bool A)
y is Element of bool (bool A)
g is Element of bool (bool A)
a is set
a is Element of bool A
A2 is Element of bool x
f .: A2 is Element of bool A
a is Element of bool A
A2 is Element of bool x
f .: A2 is Element of bool A
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
bool x is non empty set
bool (bool x) is non empty set
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
g is Element of bool (bool x)
y is Element of bool (bool x)
(x,A,f,g) is Element of bool (bool A)
bool A is non empty set
bool (bool A) is non empty set
(x,A,f,y) is Element of bool (bool A)
g is set
a is Element of bool A
a is Element of bool x
f .: a is Element of bool A
a is Element of bool x
f .: a is Element of bool A
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
bool A is non empty set
bool (bool A) is non empty set
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
g is Element of bool (bool A)
(x,A,f,g) is Element of bool (bool x)
bool x is non empty set
bool (bool x) is non empty set
(x,A,f,(x,A,f,g)) is Element of bool (bool A)
y is Element of bool A
union (x,A,f,(x,A,f,g)) is Element of bool A
union g is Element of bool A
g is set
a is set
a is Element of bool A
A2 is Element of bool x
f .: A2 is Element of bool A
c₁₀ is Element of bool A
f " c₁₀ is Element of bool x
f .: (f " c₁₀) is Element of bool A
Y2 is set
a is set
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
bool x is non empty set
bool (bool x) is non empty set
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
g is Element of bool (bool x)
(x,A,f,g) is Element of bool (bool A)
bool A is non empty set
bool (bool A) is non empty set
(x,A,f,(x,A,f,g)) is Element of bool (bool x)
y is Element of bool x
union g is Element of bool x
union (x,A,f,(x,A,f,g)) is Element of bool x
g is set
a is set
a is Element of bool x
f .: a is Element of bool A
f " (f .: a) is Element of bool x
dom f is non empty Element of bool x
a is set
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
bool A is non empty set
bool (bool A) is non empty set
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
g is Element of bool (bool A)
(x,A,f,g) is Element of bool (bool x)
bool x is non empty set
bool (bool x) is non empty set
(x,A,f,(x,A,f,g)) is Element of bool (bool A)
union (x,A,f,(x,A,f,g)) is Element of bool A
union g is Element of bool A
y is set
g is set
a is Element of bool A
a is Element of bool x
f .: a is Element of bool A
A2 is Element of bool A
f " A2 is Element of bool x
f .: (f " A2) is Element of bool A
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
bool x is non empty set
bool (bool x) is non empty set
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
g is Element of bool (bool x)
union g is Element of bool x
(x,A,f,g) is Element of bool (bool A)
bool A is non empty set
bool (bool A) is non empty set
(x,A,f,(x,A,f,g)) is Element of bool (bool x)
union (x,A,f,(x,A,f,g)) is Element of bool x
y is set
g is set
a is Element of bool x
f .: a is Element of bool A
a is Element of bool A
f " a is Element of bool x
dom f is non empty Element of bool x
A2 is Element of bool x
x is set
f is non empty set
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
A is set
g is Relation-like x -defined f -valued Function-like total (x,f) Element of bool [:x,f:]
rng g is Element of bool f
bool f is non empty set
y is Relation-like A -valued Function-like set
proj1 y is set
g * y is Relation-like x -defined A -valued Function-like set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
dom g is Element of bool x
bool x is non empty set
dom (g * y) is Element of bool x
rng (g * y) is Element of bool A
bool A is non empty set
x is set
A is set
f is non empty set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
[:f,x:] is Relation-like set
bool [:f,x:] is non empty set
g is Relation-like A -defined f -valued Function-like total (A,f) Element of bool [:A,f:]
rng g is Element of bool f
bool f is non empty set
y is Relation-like f -defined x -valued Function-like Element of bool [:f,x:]
dom y is Element of bool f
(A,x,f,g,y) is Relation-like A -defined x -valued Function-like (A,x) Element of bool [:A,x:]
[:A,x:] is Relation-like set
bool [:A,x:] is non empty set
g is Element of A
(A,x,f,g,y) . g is set
g . g is set
y . (g . g) is set
y * g is Relation-like A -defined x -valued Function-like Element of bool [:A,x:]
x is set
A is set
f is non empty set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
[:f,x:] is Relation-like set
bool [:f,x:] is non empty set
g is Relation-like A -defined f -valued Function-like total (A,f) Element of bool [:A,f:]
rng g is Element of bool f
bool f is non empty set
y is Relation-like f -defined x -valued Function-like Element of bool [:f,x:]
dom y is Element of bool f
(A,x,f,g,y) is Relation-like A -defined x -valued Function-like (A,x) Element of bool [:A,x:]
[:A,x:] is Relation-like set
bool [:A,x:] is non empty set
g is Element of A
(A,x,f,g,y) . g is set
g . g is set
y /. (g . g) is Element of x
y . (g . g) is set
x is set
A is set
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
f is non empty set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
[:f,x:] is Relation-like set
bool [:f,x:] is non empty set
g is Relation-like A -defined f -valued Function-like total (A,f) Element of bool [:A,f:]
rng g is Element of bool f
bool f is non empty set
y is Relation-like f -defined x -valued Function-like Element of bool [:f,x:]
dom y is Element of bool f
(A,x,f,g,y) is Relation-like A -defined x -valued Function-like (A,x) Element of bool [:A,x:]
[:A,x:] is Relation-like set
bool [:A,x:] is non empty set
g is Relation-like A -defined A -valued Function-like total (A,A) Element of bool [:A,A:]
(A,x,f,g,y) * g is Relation-like A -defined x -valued Function-like (A,x) Element of bool [:A,x:]
g * g is Relation-like A -defined f -valued Function-like total (A,f) Element of bool [:A,f:]
(A,x,f,(g * g),y) is Relation-like A -defined x -valued Function-like (A,x) Element of bool [:A,x:]
rng (g * g) is Element of bool f
y * g is Relation-like A -defined x -valued Function-like Element of bool [:A,x:]
(y * g) * g is Relation-like A -defined x -valued Function-like Element of bool [:A,x:]
y * (g * g) is Relation-like A -defined x -valued Function-like Element of bool [:A,x:]
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
rng f is non empty Element of bool A
bool A is non empty set
dom f is non empty Element of bool x
bool x is non empty set
g is set
f . g is set
g is Element of A
a is Element of A
a is set
A2 is set
f . A2 is set
{a} is non empty set
g is Element of A
{g} is non empty set
y is set
proj1 f is non empty set
g is set
f . y is set
f . g is set
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
f is Element of x
g is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
(x,A,g,f) is Element of A
rng g is non empty Element of bool A
bool A is non empty set
dom g is non empty Element of bool x
bool x is non empty set
x is set
A is set
f is set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
g is Relation-like A -defined f -valued Function-like (A,f) Element of bool [:A,f:]
rng g is Element of bool f
bool f is non empty set
y is set
g . y is set
g is Element of A
g . g is set
x is set
A is non empty set
f is non empty set
[:A,f:] is Relation-like non empty set
bool [:A,f:] is non empty set
g is Relation-like A -defined f -valued Function-like non empty total (A,f) Element of bool [:A,f:]
rng g is non empty Element of bool f
bool f is non empty set
y is set
g is Element of A
(A,f,g,g) is Element of f
x is non empty set
A is non empty set
[:A,x:] is Relation-like non empty set
bool [:A,x:] is non empty set
f is set
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
g is Relation-like A -defined x -valued Function-like non empty total (A,x) Element of bool [:A,x:]
y is Relation-like x -defined f -valued Function-like Element of bool [:x,f:]
(A,f,x,g,y) is Relation-like A -defined f -valued Function-like (A,f) Element of bool [:A,f:]
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
g is Element of A
(A,f,(A,f,x,g,y),g) is Element of f
(A,x,g,g) is Element of x
y . (A,x,g,g) is set
dom y is Element of bool x
bool x is non empty set
rng g is non empty Element of bool x
x is non empty set
A is non empty set
[:A,x:] is Relation-like non empty set
bool [:A,x:] is non empty set
f is set
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
g is Relation-like A -defined x -valued Function-like non empty total (A,x) Element of bool [:A,x:]
y is Relation-like x -defined f -valued Function-like Element of bool [:x,f:]
(A,f,x,g,y) is Relation-like A -defined f -valued Function-like (A,f) Element of bool [:A,f:]
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
g is Element of A
(A,f,(A,f,x,g,y),g) is Element of f
(A,x,g,g) is Element of x
y /. (A,x,g,g) is Element of f
dom y is Element of bool x
bool x is non empty set
rng g is non empty Element of bool x
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
f is set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
g is set
y is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
rng y is non empty Element of bool A
bool A is non empty set
g is Relation-like A -defined f -valued Function-like Element of bool [:A,f:]
g | g is Relation-like A -defined g -defined A -defined f -valued Function-like Element of bool [:A,f:]
dom (g | g) is Element of bool A
(x,f,A,y,(g | g)) is Relation-like x -defined f -valued Function-like (x,f) Element of bool [:x,f:]
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
(x,f,A,y,g) is Relation-like x -defined f -valued Function-like (x,f) Element of bool [:x,f:]
a is Element of x
(x,f,A,y,(g | g)) . a is set
(x,f,A,y,g) . a is set
dom g is Element of bool A
(x,A,y,a) is Element of A
(x,f,(x,f,A,y,(g | g)),a) is Element of f
(g | g) . (x,A,y,a) is set
g . (x,A,y,a) is set
(x,f,(x,f,A,y,g),a) is Element of f
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
f is set
[:A,f:] is Relation-like set
bool [:A,f:] is non empty set
g is set
y is set
g is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
rng g is non empty Element of bool A
bool A is non empty set
a is Relation-like A -defined f -valued Function-like Element of bool [:A,f:]
a | g is Relation-like A -defined g -defined A -defined f -valued Function-like Element of bool [:A,f:]
dom (a | g) is Element of bool A
(x,f,A,g,(a | g)) is Relation-like x -defined f -valued Function-like (x,f) Element of bool [:x,f:]
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
a | y is Relation-like A -defined y -defined A -defined f -valued Function-like Element of bool [:A,f:]
(x,f,A,g,(a | y)) is Relation-like x -defined f -valued Function-like (x,f) Element of bool [:x,f:]
dom (a | y) is Element of bool A
(x,f,A,g,a) is Relation-like x -defined f -valued Function-like (x,f) Element of bool [:x,f:]
x is non empty set
A is non empty set
f is non empty set
[:A,f:] is Relation-like non empty set
[:x,[:A,f:]:] is Relation-like non empty set
bool [:x,[:A,f:]:] is non empty set
g is Relation-like x -defined [:A,f:] -valued Function-like non empty total (x,[:A,f:]) Element of bool [:x,[:A,f:]:]
(x,A,f,g) is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
(x,A,f,g) is Relation-like x -defined f -valued Function-like non empty total (x,f) Element of bool [:x,f:]
[:x,f:] is Relation-like non empty set
bool [:x,f:] is non empty set
y is Element of x
(x,[:A,f:],g,y) is Element of [:A,f:]
(x,A,(x,A,f,g),y) is Element of A
(x,f,(x,A,f,g),y) is Element of f
[(x,A,(x,A,f,g),y),(x,f,(x,A,f,g),y)] is V23() set
{(x,A,(x,A,f,g),y),(x,f,(x,A,f,g),y)} is non empty set
{(x,A,(x,A,f,g),y)} is non empty set
{{(x,A,(x,A,f,g),y),(x,f,(x,A,f,g),y)},{(x,A,(x,A,f,g),y)}} is non empty set
(x,[:A,f:],g,y) `1 is set
(x,[:A,f:],g,y) `2 is set
[((x,[:A,f:],g,y) `1),((x,[:A,f:],g,y) `2)] is V23() set
{((x,[:A,f:],g,y) `1),((x,[:A,f:],g,y) `2)} is non empty set
{((x,[:A,f:],g,y) `1)} is non empty set
{{((x,[:A,f:],g,y) `1),((x,[:A,f:],g,y) `2)},{((x,[:A,f:],g,y) `1)}} is non empty set
[((x,[:A,f:],g,y) `1),(x,f,(x,A,f,g),y)] is V23() set
{((x,[:A,f:],g,y) `1),(x,f,(x,A,f,g),y)} is non empty set
{{((x,[:A,f:],g,y) `1),(x,f,(x,A,f,g),y)},{((x,[:A,f:],g,y) `1)}} is non empty set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is set
g is set
[:f,g:] is Relation-like set
bool [:f,g:] is non empty set
x /\ f is set
A /\ g is set
[:(x /\ f),(A /\ g):] is Relation-like set
bool [:(x /\ f),(A /\ g):] is non empty set
y is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
g is Relation-like f -defined g -valued Function-like (f,g) Element of bool [:f,g:]
y /\ g is Relation-like x -defined f -defined A -valued g -valued Function-like Element of bool [:f,g:]
dom (y /\ g) is Element of bool x
bool x is non empty set
dom y is Element of bool x
dom g is Element of bool f
bool f is non empty set
(dom y) /\ (dom g) is Element of bool f
the Element of x /\ f is Element of x /\ f
y . the Element of x /\ f is set
rng y is Element of bool A
bool A is non empty set
g . the Element of x /\ f is set
rng g is Element of bool g
bool g is non empty set
a is set
y . a is set
[a,(y . a)] is V23() set
{a,(y . a)} is non empty set
{a} is non empty set
{{a,(y . a)},{a}} is non empty set
g . a is set
rng (y /\ g) is Element of bool A
(rng y) /\ (rng g) is Element of bool g
x is set
A is set
(x,A) is set
f is set
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
the Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:] is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
{ the Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]} is functional non empty set
f is functional non empty set
g is Relation-like Function-like Element of f
x is set
A is set
f is non empty (x,A)
g is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like x -defined A -valued Function-like (x,A) Element of bool [:x,A:]
{f} is functional non empty set
g is Relation-like Function-like Element of {f}
x is set
A is non empty set
(x,A) is functional non empty set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
f is Relation-like Function-like Element of (x,A)
x is set
A is non empty set
(x,A) is functional non empty set
f is functional non empty (x,A)
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set
g is Relation-like Function-like Element of f
x is set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total (x,x) (x) (x,x) Element of bool [:x,x:]
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
A is Relation-like x -defined Function-like set
x is non empty set
A is non empty set
[:x,A:] is Relation-like non empty set
bool [:x,A:] is non empty set
g is set
f is Relation-like x -defined A -valued Function-like non empty total (x,A) Element of bool [:x,A:]
f /. g is Element of A
f . g is set
y is Element of A
dom f is non empty Element of bool x
bool x is non empty set
x is non empty set
[:x,x:] is Relation-like non empty set
bool [:x,x:] is non empty set
A is Relation-like x -defined x -valued Function-like non empty total (x,x) Element of bool [:x,x:]
f is Relation-like x -valued Function-like set
f * A is Relation-like x -valued Function-like set
proj1 (f * A) is set
proj1 f is set
dom A is non empty Element of bool x
bool x is non empty set
rng f is Element of bool x
x is non empty set
[:x,x:] is Relation-like non empty set
bool [:x,x:] is non empty set
id x is Relation-like x -defined x -valued reflexive symmetric antisymmetric transitive Function-like one-to-one non empty total (x,x) (x) (x,x) Element of bool [:x,x:]
A is Relation-like x -defined x -valued Function-like non empty total (x,x) Element of bool [:x,x:]
f is Element of x
A . f is set
(id x) . f is set
(x,x,(id x),f) is Element of x
x is set
{x} is non empty set
A is set
[:{x},A:] is Relation-like set
bool [:{x},A:] is non empty set
f is Relation-like {x} -defined A -valued Function-like ({x},A) Element of bool [:{x},A:]
f . x is set
g is Relation-like {x} -defined A -valued Function-like ({x},A) Element of bool [:{x},A:]
g . x is set
y is set
f . y is set
g . y is set