:: FUNCT_2 semantic presentation

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

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

dom f is Element of bool x
bool x is non empty set

A is set
[:x,A:] is Relation-like set
bool [:x,A:] 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

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

proj1 x is set
proj2 x is set
[:(),():] is Relation-like set
bool [:(),():] is non empty set
A is Relation-like proj1 x -defined proj2 x -valued Element of bool [:(),():]
rng A is Element of bool ()
bool () is non empty set
x is set

proj2 A is set
proj1 A is set
[:(),x:] is Relation-like set
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

proj1 f is set
proj2 f is set
g is set
y is set
f . y is set
[:(),A:] is Relation-like set
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 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
F1() is set
F2() is set
[:F1(),F2():] is Relation-like set
bool [:F1(),F2():] is non empty set

proj1 x is set
proj2 x is set
A is Relation-like F1() -defined F2() -valued Function-like (F1(),F2()) Element of bool [:F1(),F2():]
f is set
A . f is set
F1() is set
F2() is set
[:F1(),F2():] is Relation-like set
bool [:F1(),F2():] is non empty set
x is set
F3(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

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

proj1 g is set
proj2 g is 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

(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

(x,A) is set
the Element of (x,A) is Element of (x,A)

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

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

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

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

dom y is Element of bool A
dom g is Element of bool A

proj1 g is set

proj1 y is set

proj2 g is set
proj2 y is set
() \/ () is set
[:A,(() \/ ()):] is Relation-like set
bool [:A,(() \/ ()):] is non empty set
x is set

[: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,A:] is Relation-like set
bool [:A,A:] is non empty set

(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

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

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

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

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

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

proj2 g is set

proj2 y is set
proj1 g is set
proj1 y is set
[:(),x:] is Relation-like set
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
[: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:]

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

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

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

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

proj2 (f ") is set
g is set
dom f is Element of bool x
bool x is non empty set
proj1 (f ") is set

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

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

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

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

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

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

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

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

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

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

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) . 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

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

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

bool [:{},x:] is non empty set

A is set

bool x is non empty set
x is set

bool [:{},x:] is non empty set

A is set

bool {} is non empty set
x is set
{x} is non empty set
A is set

bool [:{x},A:] is non empty set

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

bool [:{x},A:] is non empty set

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

bool [:{x},A:] is non empty set
f is set

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

bool [:x,{A}:] is non empty set
f is set

g . f is set
x is set
A is set
{A} is non empty set

bool [:x,{A}:] is non empty set

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

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

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
dom (f * g) is Element of bool x
g " x is Element of bool x
dom g is Element of bool x

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

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

x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set

rng A is Element of bool x
bool x is non empty set

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

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

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

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

x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set

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

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

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

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

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

x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set

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

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

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

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

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

y is Relation-like A -defined f -valued Function-like (A,f) Element of bool [:A,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
F1() is non empty set
F2() is non empty set
[:F1(),F2():] is Relation-like non empty set
bool [:F1(),F2():] is non empty set
x is set
A is Element of F2()
x is Relation-like F1() -defined F2() -valued Function-like total (F1(),F2()) Element of bool [:F1(),F2():]
A is Element of F1()
(F1(),F2(),x,A) is Element of F2()
F1() is non empty set
F2() is non empty set
[:F1(),F2():] is Relation-like non empty set
bool [:F1(),F2():] is non empty set
x is Element of F1()
F3(x) is Element of F2()
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

proj1 g is set
proj2 g is set
F1() is set
F2() is set
[:F1(),F2():] is Relation-like set
bool [:F1(),F2():] is non empty set
the Element of F1() is Element of F1()
F3( the Element of F1()) is set

proj1 x is set
proj2 x is set
A is set
f is set
x . f is set
F4(f) is set
F3(f) is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty 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
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

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

x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set

x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set

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

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

x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set

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

dom A is Element of bool x
bool x is non empty set

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

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

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

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

TotFuncs A is set
x is set
A is set
[:x,A:] is Relation-like set
bool [:x,A:] is non empty set

TotFuncs f is set
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

TotFuncs f is set
g is set
x is set
A is set

[:x,A:] is Relation-like set
bool [:x,A:] is non empty set

TotFuncs <:{},x,A:> is set
(x,A) is set
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:]

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,x,x:> is Relation-like x -defined x -valued Function-like total (x,x) Element of bool [:x,x:]

TotFuncs <:A,x,x:> is set
{A} is functional non empty set
x is set
A is set
{A} is non empty set

bool [:x,{A}:] is non empty set

TotFuncs f is set

{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

TotFuncs f is set
TotFuncs g is set
y is set

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

TotFuncs f is set

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
() /\ () 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

TotFuncs f is set

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

F1() is non empty set
F2() is non empty set
[:F1(),F2():] is Relation-like non empty set
bool [:F1(),F2():] is non empty set
F3() is Element of F1()
F4() is Element of F2()
x is Element of F1()
F5(x) is Element of F2()
A is Element of F2()
x is Relation-like F1() -defined F2() -valued Function-like non empty total (F1(),F2()) Element of bool [:F1(),F2():]
(F1(),F2(),x,F3()) is Element of F2()
A is Element of F1()
(F1(),F2(),x,A) is Element of F2()
F5(A) is Element of F2()
F1() is non empty set
F2() is non empty set
F3() is Element of F1()
F4() is Element of F1()
[:F1(),F2():] is Relation-like non empty set
bool [:F1(),F2():] is non empty set
F5() is Element of F2()
F6() is Element of F2()
x is Element of F1()
F7(x) is Element of F2()
A is Element of F2()
f is Element of F2()
x is Relation-like F1() -defined F2() -valued Function-like non empty total (F1(),F2()) Element of bool [:F1(),F2():]
(F1(),F2(),x,F3()) is Element of F2()
(F1(),F2(),x,F4()) is Element of F2()
A is Element of F1()
(F1(),F2(),x,A) is Element of F2()
F7(A) is Element of F2()
x is set
A is set
(x,A) is set

proj1 f is set
proj2 f is set

proj1 g is set
proj2 g is set
F1() is non empty set
F2() is set
[:F1(),F2():] is Relation-like set
bool [:F1(),F2():] is non empty set
x is set
F3(x) is set
x is Relation-like F1() -defined F2() -valued Function-like (F1(),F2()) Element of bool [:F1(),F2():]
x is Relation-like F1() -defined F2() -valued Function-like (F1(),F2()) Element of bool [:F1(),F2():]
A is Element of F1()
(F1(),F2(),x,A) is Element of F2()
F3(A) is set
F1() is non empty set
F2() is non empty set
[:F1(),F2():] is Relation-like non empty set
bool [:F1(),F2():] is non empty set
x is Element of F1()
F3(x) is set
x is Relation-like F1() -defined F2() -valued Function-like non empty total (F1(),F2()) Element of bool [:F1(),F2():]
A is Element of F1()
(F1(),F2(),x,A) is Element of F2()
F3(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:]:]

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

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

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

[#] 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):]

y is set
Im (g,y) is set
A . y is set
x is set
bool x is non empty set

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

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

f is set
A is set
x .: f is set

(x | A) .: f is set

[:A,A:] is Relation-like set
bool [:A,A:] is non empty 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

f is set
x " f is set
A is set

(x | A) " f is set

[:A,A:] is Relation-like set
bool [:A,A:] is non empty set

((id A) * x) " f is set
(id A) " (x " f) is Element of bool A
bool A is non empty set
F1() is non empty set
F2() is non empty set
[:F1(),F2():] is Relation-like non empty set
bool [:F1(),F2():] is non empty set
x is set
F3(x) is set

proj1 x is set
proj2 x is set
A is Relation-like F1() -defined F2() -valued Function-like non empty total (F1(),F2()) Element of bool [:F1(),F2():]
f is Element of F1()
(F1(),F2(),A,f) is Element of F2()
F3(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