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

F

[:F

bool [:F

x is Relation-like Function-like set

proj1 x is set

proj2 x is set

A is Relation-like F

f is set

A . f is set

F

F

[:F

bool [:F

x is set

F

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

F

[:F

bool [:F

x is set

A is Element of F

x is Relation-like F

A is Element of F

(F

F

F

[:F

bool [:F

x is Element of F

F

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

F

[:F

bool [:F

the Element of F

F

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

F

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

F

[:F

bool [:F

F

F

x is Element of F

F

A is Element of F

x is Relation-like F

(F

A is Element of F

(F

F

F

F

F

F

[:F

bool [:F

F

F

x is Element of F

F

A is Element of F

f is Element of F

x is Relation-like F

(F

(F

A is Element of F

(F

F

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

F

[:F

bool [:F

x is set

F

x is Relation-like F

x is Relation-like F

A is Element of F

(F

F

F

F

[:F

bool [:F

x is Element of F

F

x is Relation-like F

A is Element of F

(F

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

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

F

[:F

bool [:F

x is set

F

x is Relation-like Function-like set

proj1 x is set

proj2 x is set

A is Relation-like F

f is Element of F

(F

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