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

Y is Relation-like Function-like set

dom Y is set

x is Relation-like Function-like set

dom x is set

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

Y \/ x is Relation-like set

X is set

f is set

[X,f] is set

{X,f} is non empty set

{X} is non empty set

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

p is set

[X,p] is set

{X,p} is non empty set

{{X,p},{X}} is non empty set

Y . X is set

x . X is set

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

X is Relation-like Function-like set

f is set

p is set

[f,p] is set

{f,p} is non empty set

{f} is non empty set

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

Y is Relation-like Function-like set

x is Relation-like Function-like set

Y \/ x is Relation-like set

X is Relation-like Function-like set

dom Y is set

dom x is set

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

f is set

Y . f is set

x . f is set

X . f is set

F

Y is set

F

F

Y is set

x is set

F

F

X is set

X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

dom X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

Y is set

rng X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial set

x is set

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Function-like set

dom X is set

rng X is set

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

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is set

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

rng f is set

dom f is Element of bool Y

bool Y is non empty set

p is set

f . p is set

Y is set

x is set

X is Relation-like Y -valued Function-like set

dom X is set

X . x is set

rng X is set

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

dom X is Element of bool Y

bool Y is non empty set

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

dom f is Element of bool Y

p is set

X . p is set

f . p is set

F

F

[:F

bool [:F

the set is set

x is set

X is set

X is set

f is set

x is set

X is set

p is set

f is set

q is set

x is Relation-like Function-like set

dom x is set

X is set

x | X is Relation-like Function-like set

dom (x | X) is set

rng (x | X) is set

p is set

q is set

(x | X) . q is set

x . q is set

p is set

p is Relation-like F

q is Relation-like F

dom q is Element of bool F

bool F

p is set

q is set

(dom x) /\ X is set

p is set

x . p is set

q is set

q . p is set

Y is Relation-like Function-like set

dom Y is set

rng Y is set

x is Relation-like F

X is Relation-like F

dom X is Element of bool F

f is set

p is set

q is set

f is set

X . f is set

Y is Relation-like F

dom Y is Element of bool F

x is Relation-like F

dom x is Element of bool F

F

F

[:F

bool [:F

Y is set

x is set

F

X is set

Y is set

x is set

F

Y is Relation-like F

dom Y is Element of bool F

bool F

x is set

F

X is set

F

X is set

x is set

Y . x is set

F

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is set

f is set

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

bool [:X,f:] is non empty set

p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

q is Relation-like X -defined f -valued Function-like Element of bool [:X,f:]

p * q is Relation-like Y -defined f -valued Function-like set

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

bool [:Y,f:] is non empty set

dom (p * q) is Element of bool Y

bool Y is non empty set

rng (p * q) is set

Y is set

id Y is Relation-like Y -defined Y -valued Function-like one-to-one set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Element of bool [:Y,x:]

(id Y) * X is Relation-like Y -defined x -valued set

dom X is Element of bool Y

bool Y is non empty set

Y is set

x is set

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

bool [:Y,x:] is non empty set

id x is Relation-like x -defined x -valued Function-like one-to-one set

X is Relation-like Y -defined x -valued Element of bool [:Y,x:]

X * (id x) is Relation-like Y -defined x -valued set

rng X is Element of bool x

bool x is non empty set

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

dom X is Element of bool Y

bool Y is non empty set

f is set

p is set

X . f is set

X . p is set

Y is set

x is set

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

bool [:Y,x:] is non empty set

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

bool [:x,Y:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

X " is Relation-like Function-like set

rng X is set

dom (X ") is set

dom X is Element of bool Y

bool Y is non empty set

rng (X ") is set

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is set

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

bool [:X,x:] is non empty set

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

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

dom (f | X) is Element of bool Y

bool Y is non empty set

rng (f | X) is set

Y is set

x is set

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

bool [:Y,x:] is non empty set

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

X is set

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

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

f is set

X | f is Relation-like f -defined Y -defined x -valued Function-like set

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is set

[:Y,X:] is Relation-like set

bool [:Y,X:] is non empty set

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

X |` f is Relation-like Y -defined x -valued X -valued x -valued Function-like Element of bool [:Y,x:]

dom (X |` f) is Element of bool Y

bool Y is non empty set

rng (X |` f) is set

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is set

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

X |` f is Relation-like Y -defined x -valued X -valued x -valued Function-like Element of bool [:Y,x:]

Y is set

x is set

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

bool [:x,Y:] is non empty set

X is Relation-like Function-like set

Y |` X is Relation-like Function-like set

(Y |` X) | x is Relation-like Function-like set

X | x is Relation-like Function-like set

Y |` (X | x) is Relation-like Function-like set

dom ((Y |` X) | x) is set

rng ((Y |` X) | x) is set

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is set

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

f .: Y is set

dom f is Element of bool Y

bool Y is non empty set

p is set

f . p is set

Y is set

{Y} is non empty set

x is set

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

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

X is Relation-like {Y} -defined x -valued Function-like Element of bool [:{Y},x:]

rng X is set

X . Y is set

{(X . Y)} is non empty set

dom X is Element of bool {Y}

bool {Y} is non empty set

Y is set

{Y} is non empty set

x is set

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

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

X is Relation-like {Y} -defined x -valued Function-like Element of bool [:{Y},x:]

f is set

dom X is set

X . f is set

p is set

X . p is set

dom X is Element of bool {Y}

bool {Y} is non empty set

Y is set

{Y} is non empty set

x is set

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

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

X is set

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

f .: X is set

f . Y is set

{(f . Y)} is non empty set

rng f is set

Y is set

{Y} is non empty set

x is set

X is set

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

bool [:x,X:] is non empty set

f is Relation-like Function-like set

dom f is set

f . Y is set

rng f is set

{(f . Y)} is non empty set

Y is set

x is set

{x} is non empty set

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

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

X is set

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

dom f is Element of bool Y

bool Y is non empty set

f . X is set

Y is set

x is set

{x} is non empty set

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

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

X is Relation-like Y -defined {x} -valued Function-like Element of bool [:Y,{x}:]

dom X is Element of bool Y

bool Y is non empty set

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

dom f is Element of bool Y

p is set

X . p is set

f . p is set

X is set

Y is Relation-like Function-like set

X |` Y is Relation-like Function-like set

x is set

(X |` Y) | x is Relation-like Function-like set

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

bool [:x,X:] is non empty set

Y is set

x is set

X is Relation-like Function-like set

(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

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

(x |` X) | Y is Relation-like Function-like set

Y is set

x is set

X is Relation-like Function-like set

(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

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

(x |` X) | Y is Relation-like Function-like set

dom (X,Y,x) is Element of bool Y

bool Y is non empty set

dom X is set

rng (X,Y,x) is set

rng X is set

Y is set

x is set

X is set

f is Relation-like Function-like set

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

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

bool [:x,X:] is non empty set

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

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

dom (f,x,X) is Element of bool x

bool x is non empty set

dom f is set

f . Y is set

dom (X |` f) is set

(dom (X |` f)) /\ x is set

dom (X |` f) is set

(dom (X |` f)) /\ x is set

Y is set

x is set

X is set

f is Relation-like Function-like set

dom f is set

f . Y is set

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

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

bool [:x,X:] is non empty set

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

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

(f,x,X) . Y is set

dom (X |` f) is set

(X |` f) . Y is set

((X |` f) | x) . Y is set

Y is set

x is set

X is set

f is Relation-like Function-like set

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

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

bool [:x,X:] is non empty set

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

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

dom (f,x,X) is Element of bool x

bool x is non empty set

(f,x,X) . Y is set

f . Y is set

dom f is set

Y is set

x is set

X is Relation-like Function-like set

f is Relation-like Function-like set

(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

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

(x |` X) | Y is Relation-like Function-like set

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

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

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

dom (X,Y,x) is Element of bool Y

bool Y is non empty set

dom X is set

dom (f,Y,x) is Element of bool Y

p is set

dom f is set

X . p is set

f . p is set

p is set

(X,Y,x) . p is set

X . p is set

(f,Y,x) . p is set

f . p is set

Y is set

x is set

X is set

f is Relation-like Function-like set

(f,Y,X) is Relation-like Y -defined X -valued Function-like Element of bool [:Y,X:]

[:Y,X:] is Relation-like set

bool [:Y,X:] is non empty set

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

(X |` f) | Y is Relation-like Function-like set

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

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

bool [:x,X:] is non empty set

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

dom (f,Y,X) is Element of bool Y

bool Y is non empty set

dom (f,x,X) is Element of bool x

bool x is non empty set

p is set

f . p is set

dom f is set

p is set

(f,Y,X) . p is set

f . p is set

(f,x,X) . p is set

Y is set

x is set

X is set

f is Relation-like Function-like set

(f,X,Y) is Relation-like X -defined Y -valued Function-like Element of bool [:X,Y:]

[:X,Y:] is Relation-like set

bool [:X,Y:] is non empty set

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

(Y |` f) | X is Relation-like Function-like set

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

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

bool [:X,x:] is non empty set

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

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

dom (f,X,Y) is Element of bool X

bool X is non empty set

dom (f,X,x) is Element of bool X

p is set

f . p is set

dom f is set

p is set

(f,X,Y) . p is set

f . p is set

(f,X,x) . p is set

Y is set

x is set

X is set

f is set

p is Relation-like Function-like set

(p,Y,X) is Relation-like Y -defined X -valued Function-like Element of bool [:Y,X:]

[:Y,X:] is Relation-like set

bool [:Y,X:] is non empty set

X |` p is Relation-like Function-like set

(X |` p) | Y is Relation-like Function-like set

(p,x,f) 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

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

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

(p,x,X) is Relation-like x -defined X -valued Function-like Element of bool [:x,X:]

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

bool [:x,X:] is non empty set

(X |` p) | x is Relation-like Function-like set

Y is set

x is set

X is Relation-like Function-like set

dom X is set

rng X is set

(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

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

(x |` X) | Y is Relation-like Function-like set

dom (X,Y,x) is Element of bool Y

bool Y is non empty set

f is set

X . f is set

f is set

X . f is set

(X,Y,x) . f is set

Y is Relation-like Function-like set

dom Y is set

rng Y is set

(Y,(dom Y),(rng Y)) is Relation-like dom Y -defined rng Y -valued Function-like Element of bool [:(dom Y),(rng Y):]

[:(dom Y),(rng Y):] is Relation-like set

bool [:(dom Y),(rng Y):] is non empty set

(rng Y) |` Y is Relation-like Function-like set

((rng Y) |` Y) | (dom Y) is Relation-like Function-like set

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

x |` X is Relation-like Y -defined x -valued x -valued Function-like set

(x |` X) | Y is Relation-like Y -defined Y -defined x -valued Function-like set

Y is set

x is set

({},Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

x |` {} is Relation-like Function-like set

(x |` {}) | Y is Relation-like Function-like set

dom {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

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

Y is set

x is set

X is set

f is Relation-like Function-like set

(f,X,Y) is Relation-like X -defined Y -valued Function-like Element of bool [:X,Y:]

[:X,Y:] is Relation-like set

bool [:X,Y:] is non empty set

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

(Y |` f) | X is Relation-like Function-like set

p is Relation-like Function-like set

(p,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

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

(x |` p) | Y is Relation-like Function-like set

(X,Y,Y,x,(f,X,Y),(p,Y,x)) is Relation-like X -defined x -valued Function-like Element of bool [:X,x:]

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

bool [:X,x:] is non empty set

f * p is Relation-like Function-like set

((f * p),X,x) is Relation-like X -defined x -valued Function-like Element of bool [:X,x:]

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

(x |` (f * p)) | X is Relation-like Function-like set

dom (X,Y,Y,x,(f,X,Y),(p,Y,x)) is Element of bool X

bool X is non empty set

q is set

(X,Y,Y,x,(f,X,Y),(p,Y,x)) . q is set

((f * p),X,x) . q is set

dom (f,X,Y) is Element of bool X

dom f is set

(f,X,Y) . q is set

dom (p,Y,x) is Element of bool Y

bool Y is non empty set

f . q is set

p . (f . q) is set

(f * p) . q is set

dom p is set

dom (f * p) is set

dom ((f * p),X,x) is Element of bool X

(p,Y,x) . ((f,X,Y) . q) is set

(p,Y,x) . (f . q) is set

dom ((f * p),X,x) is Element of bool X

q is set

dom (f,X,Y) is Element of bool X

dom f is set

(f,X,Y) . q is set

dom (p,Y,x) is Element of bool Y

bool Y is non empty set

f . q is set

p . (f . q) is set

(f * p) . q is set

dom p is set

dom (f * p) is set

Y is set

x is set

X is set

f is Relation-like Function-like set

rng f is set

p is Relation-like Function-like set

dom p is set

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

(f,X,Y) is Relation-like X -defined Y -valued Function-like Element of bool [:X,Y:]

[:X,Y:] is Relation-like set

bool [:X,Y:] is non empty set

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

(Y |` f) | X is Relation-like Function-like set

(p,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

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

(x |` p) | Y is Relation-like Function-like set

(X,Y,Y,x,(f,X,Y),(p,Y,x)) is Relation-like X -defined x -valued Function-like Element of bool [:X,x:]

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

bool [:X,x:] is non empty set

f * p is Relation-like Function-like set

((f * p),X,x) is Relation-like X -defined x -valued Function-like Element of bool [:X,x:]

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

(x |` (f * p)) | X is Relation-like Function-like set

dom ((f * p),X,x) is Element of bool X

bool X is non empty set

dom (X,Y,Y,x,(f,X,Y),(p,Y,x)) is Element of bool X

q is set

dom (f * p) is set

f . q is set

dom f is set

(f * p) . q is set

p . (f . q) is set

dom (p,Y,x) is Element of bool Y

bool Y is non empty set

dom (f,X,Y) is Element of bool X

(f,X,Y) . q is set

q is set

((f * p),X,x) . q is set

(X,Y,Y,x,(f,X,Y),(p,Y,x)) . q is set

dom (f * p) is set

f . q is set

dom f is set

(f * p) . q is set

p . (f . q) is set

dom (p,Y,x) is Element of bool Y

bool Y is non empty set

dom (f,X,Y) is Element of bool X

(p,Y,x) . (f . q) is set

(f,X,Y) . q is set

(p,Y,x) . ((f,X,Y) . q) is set

Y is set

x is set

X is Relation-like Function-like set

(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

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

(x |` X) | Y is Relation-like Function-like set

Y is set

x is set

X is Relation-like Function-like set

(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

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

(x |` X) | Y is Relation-like Function-like set

(X,Y,x) " is Relation-like Function-like set

X " is Relation-like Function-like set

((X "),x,Y) is Relation-like x -defined Y -valued Function-like Element of bool [:x,Y:]

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

bool [:x,Y:] is non empty set

Y |` (X ") is Relation-like Function-like set

(Y |` (X ")) | x is Relation-like Function-like set

dom ((X,Y,x) ") is set

dom ((X "),x,Y) is Element of bool x

bool x is non empty set

f is set

rng (X,Y,x) is set

dom (X,Y,x) is Element of bool Y

bool Y is non empty set

p is set

(X,Y,x) . p is set

X . p is set

rng X is set

dom (X ") is set

dom X is set

(X ") . f is set

dom (X ") is set

rng X is set

dom X is set

p is set

X . p is set

(X ") . (X . p) is set

dom (X,Y,x) is Element of bool Y

bool Y is non empty set

(X,Y,x) . p is set

rng (X,Y,x) is set

f is set

((X "),x,Y) . f is set

((X,Y,x) ") . f is set

rng (X,Y,x) is set

rng X is set

dom X is set

p is set

X . p is set

(X ") . (X . p) is set

dom (X,Y,x) is Element of bool Y

bool Y is non empty set

(X,Y,x) . p is set

((X,Y,x) ") . ((X,Y,x) . p) is set

Y is set

x is set

X is set

Y /\ X is set

f is Relation-like Function-like set

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

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

bool [:x,X:] is non empty set

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

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

Y |` (f,x,X) is Relation-like x -defined Y -valued X -valued Function-like Element of bool [:x,X:]

(f,x,(Y /\ X)) is Relation-like x -defined Y /\ X -valued Function-like Element of bool [:x,(Y /\ X):]

[:x,(Y /\ X):] is Relation-like set

bool [:x,(Y /\ X):] is non empty set

(Y /\ X) |` f is Relation-like Function-like set

((Y /\ X) |` f) | x is Relation-like Function-like set

f | x is Relation-like Function-like set

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

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

(Y /\ X) |` (f | x) is Relation-like Function-like set

Y is set

Y is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like non-empty empty-yielding Y -defined x -valued Function-like one-to-one constant functional empty Element of bool [:Y,x:]

dom X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty non proper Element of bool Y

bool Y is non empty set

Y is non empty set

x is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

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

bool [:Y,x:] is non empty set

X is Relation-like non-empty empty-yielding Y -defined x -valued Function-like one-to-one constant functional empty Element of bool [:Y,x:]

dom X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper Element of bool Y

bool Y is non empty set

Y is set

x is set

X is Relation-like Function-like set

(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

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

(x |` X) | Y is Relation-like Function-like set

dom X is set

dom (X,Y,x) is Element of bool Y

bool Y is non empty set

f is set

Y is set

x is set

({},Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

x |` {} is Relation-like Function-like set

(x |` {}) | Y is Relation-like Function-like set

dom {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

Y is set

x is set

X is Relation-like Function-like set

dom X is set

rng X is set

(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

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

(x |` X) | Y is Relation-like Function-like set

dom (X,Y,x) is Element of bool Y

bool Y is non empty set

f is set

X . f is set

Y is set

x is set

X is Relation-like Function-like set

(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

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

(x |` X) | Y is Relation-like Function-like set

X .: Y is set

dom (X,Y,x) is Element of bool Y

bool Y is non empty set

f is set

rng (X,Y,x) is set

dom X is set

p is set

X . p is set

(X,Y,x) . p is set

Y is set

x is set

X is Relation-like Function-like set

dom X is set

X .: Y is set

(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

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

(x |` X) | Y is Relation-like Function-like set

dom (X,Y,x) is Element of bool Y

bool Y is non empty set

f is set

X . f is set

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is set

f is set

p is Relation-like Function-like set

dom p is set

rng p is set

q is set

p is set

[q,p] is set

{q,p} is non empty set

{q} is non empty set

{{q,p},{q}} is non empty set

p . q is set

X is set

f is set

p is set

q is Relation-like Function-like set

dom q is set

rng q is set

q is Relation-like Function-like set

dom q is set

rng q is set

Y is set

x is set

(Y,x) is set

X is Relation-like Function-like set

dom X is set

rng X is set

Y is set

x is set

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

bool [:Y,x:] is non empty set

(Y,x) is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

dom X is Element of bool Y

bool Y is non empty set

rng X is set

Y is set

x is set

(Y,x) is non empty set

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

bool [:Y,x:] is non empty set

X is set

f is Relation-like Function-like set

dom f is set

rng f is set

Y is set

x is set

(Y,x) is non empty set

X is Element of (Y,x)

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

bool [:Y,x:] is non empty set

{{}} is functional non empty set

Y is set

({},Y) is non empty set

x is set

[:{},Y:] is Relation-like set

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

[:{},Y:] is Relation-like set

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

Y is set

(Y,{}) is non empty set

x is set

[:Y,{}:] is Relation-like set

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

[:Y,{}:] is Relation-like set

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

Y is set

x is set

X is set

(Y,X) is non empty set

f is set

(x,f) is non empty set

p is set

[:Y,X:] is Relation-like set

bool [:Y,X:] is non empty set

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

bool [:x,f:] is non empty set

f is set

X is Relation-like Function-like set

dom X is set

(dom X) /\ (dom X) is set

X . f is set

X is Relation-like Function-like set

dom X is set

f is Relation-like Function-like set

dom f is set

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

p is set

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

f . p is set

X . p is set

Y is Relation-like Function-like set

x is Relation-like Function-like set

Y \/ x is Relation-like set

dom Y is set

dom x is set

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

X is Relation-like Function-like set

f is set

Y . f is set

x . f is set

X is Relation-like Function-like set

f is set

Y . f is set

x . f is set

p is Relation-like Function-like set

Y is Relation-like Function-like set

x is Relation-like Function-like set

Y \/ x is Relation-like set

X is Relation-like Function-like set

X is Relation-like Function-like set

X is Relation-like Function-like set

f is Relation-like Function-like set

p is Relation-like Function-like set

Y is Relation-like Function-like set

dom Y is set

x is Relation-like Function-like set

dom x is set

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

X is set

Y . X is set

x . X is set

Y is Relation-like Function-like set

x is Relation-like Function-like set

Y is Relation-like Function-like set

dom Y is set

x is Relation-like Function-like set

dom x is set

X is set

Y . X is set

x . X is set

Y is Relation-like Function-like set

dom Y is set

x is Relation-like Function-like set

dom x is set

Y \/ x is Relation-like set

Y is Relation-like Function-like set

X is Relation-like Function-like set

x is Relation-like Function-like set

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

p is Relation-like Function-like set

dom f is Element of bool Y

bool Y is non empty set

dom X is Element of bool Y

q is set

dom f is set

dom p is set

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

f . q is set

p . q is set

(dom f) /\ (dom p) is Element of bool Y

X . q is set

(dom X) /\ (dom p) is Element of bool Y

Y is Relation-like Function-like set

{} \/ Y is Relation-like set

Y is set

x is set

({},Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

x |` {} is Relation-like Function-like set

(x |` {}) | Y is Relation-like Function-like set

X is Relation-like Function-like set

Y is set

x is set

{x} is non empty set

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

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

X is Relation-like Y -defined {x} -valued Function-like Element of bool [:Y,{x}:]

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

p is set

dom X is set

dom f is set

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

X . p is set

f . p is set

dom X is Element of bool Y

bool Y is non empty set

dom f is Element of bool Y

(dom X) /\ (dom f) is Element of bool Y

Y is set

x is Relation-like Function-like set

x | Y is Relation-like Function-like set

Y is set

x is Relation-like Function-like set

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

Y is set

x is set

X is Relation-like Function-like set

Y |` X is Relation-like Function-like set

(Y |` X) | x is Relation-like Function-like set

X is Relation-like Function-like set

Y is set

x is set

(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

bool [:Y,x:] is non empty set

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

(x |` X) | Y is Relation-like Function-like set

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

dom X is Element of bool Y

bool Y is non empty set

dom f is Element of bool Y

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

dom p is Element of bool Y

bool Y is non empty set

q is set

dom X is set

dom f is set

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

X . q is set

f . q is set

dom X is Element of bool Y

dom f is Element of bool Y

(dom X) /\ (dom f) is Element of bool Y

(dom X) /\ (dom p) is Element of bool Y

p . q is set

(dom f) /\ (dom p) is Element of bool Y

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

({},Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

x |` {} is Relation-like Function-like set

(x |` {}) | Y is Relation-like Function-like set

the Element of x is Element of x

dom X is Element of bool Y

bool Y is non empty set

dom f is Element of bool Y

q is set

X . q is set

f . q is set

p is set

(dom X) /\ (dom f) is Element of bool Y

p is set

p is set

p is set

q is set

p is set

X . q is set

f . q is set

q is set

q is Relation-like Function-like set

dom q is set

rng q is set

p is set

q is set

q . q is set

X . q is set

X . q is set

f . q is set

q is set

dom X is set

(dom X) /\ (dom q) is set

X . q is set

q . q is set

(dom X) /\ (dom q) is Element of bool Y

q is set

dom f is set

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

f . q is set

q . q is set

(dom f) /\ (dom q) is Element of bool Y

p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

(Y,x) is non empty set

f is set

q is set

p is set

p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

f is set

f is set

p is set

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

(Y,x,X) is set

f is set

p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

Y is set

x is set

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

bool [:Y,x:] is non empty set

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

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

(Y,x,X) is set

p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

(Y,x,X) is set

f is Relation-like Function-like set

p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

Y is non empty set

x is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

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

bool [:Y,x:] is non empty set

X is Relation-like non-empty empty-yielding Y -defined x -valued Function-like one-to-one constant functional empty (Y) Element of bool [:Y,x:]

(Y,x,X) is set

the Element of (Y,x,X) is Element of (Y,x,X)

[:Y,{}:] is Relation-like set

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

p is Relation-like non-empty empty-yielding Y -defined {} -valued Function-like one-to-one constant functional empty (Y) Element of bool [:Y,{}:]

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

(Y,x,X) is set

{X} is functional non empty set

f is set

p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

Y is set

[:{},Y:] is Relation-like set

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

x is Relation-like non-empty empty-yielding {} -defined Y -valued Function-like one-to-one constant functional empty ( {} ) Element of bool [:{},Y:]

({},Y,x) is set

{x} is functional non empty set

Y is set

[:{},Y:] is Relation-like set

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

x is Relation-like non-empty empty-yielding {} -defined Y -valued Function-like one-to-one constant functional empty ( {} ) Element of bool [:{},Y:]

({},Y,x) is set

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

(Y,x,X) is set

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

(Y,x,f) is set

(Y,x,X) /\ (Y,x,f) is set

the Element of (Y,x,X) /\ (Y,x,f) is Element of (Y,x,X) /\ (Y,x,f)

q is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

Y is set

x is set

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

bool [:Y,x:] is non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

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

(Y,x,X) is set

(Y,x,f) is set

p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

(Y,x,X) /\ (Y,x,f) is set

Y is set

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

bool [:Y,Y:] is non empty set

id Y is Relation-like Y -defined Y -valued Function-like one-to-one set

x is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]

dom x is Element of bool Y

bool Y is non empty set

Y is set

id Y is Relation-like Y -defined Y -valued Function-like one-to-one set

x is Relation-like set

dom x is set

rng x is set

field x is set

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

X is set

[X,X] is set

{X,X} is non empty set

{X} is non empty set

{{X,X},{X}} is non empty set

X is set

f is set

[X,f] is set

{X,f} is non empty set

{X} is non empty set

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

[f,X] is set

{f,X} is non empty set

{f} is non empty set

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

X is set

f is set

[X,f] is set

{X,f} is non empty set

{X} is non empty set

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

[f,X] is set

{f,X} is non empty set

{f} is non empty set

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

X is set

f is set

p is set

[X,f] is set

{X,f} is non empty set

{X} is non empty set

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

[f,p] is set

{f,p} is non empty set

{f} is non empty set

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

[X,p] is set

{X,p} is non empty set

{{X,p},{X}} is non empty set

Y is set

id Y is Relation-like Y -defined Y -valued Function-like one-to-one set

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

bool [:Y,Y:] is non empty set

dom (id Y) is Element of bool Y

bool Y is non empty set

rng (id Y) is set

Y is set

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

bool [:Y,Y:] is non empty set

id Y is Relation-like Y -defined Y -valued Function-like one-to-one set

x is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]

Y is Relation-like set

field Y is set

dom Y is set

rng Y is set

(dom Y) \/ (rng Y) is set

x is set

[x,x] is set

{x,x} is non empty set

{x} is non empty set

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

X is set

[x,X] is set

{x,X} is non empty set

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

[X,x] is set

{X,x} is non empty set

{X} is non empty set

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

Y is set

id Y is Relation-like Y -defined Y -valued Function-like one-to-one set

Y is set

id Y is Relation-like Y -defined Y -valued Function-like one-to-one reflexive symmetric antisymmetric transitive set

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

bool [:Y,Y:] is non empty set

F

Y is Relation-like Function-like set

dom Y is set

x is Element of F

Y . x is set

F

X is Element of F

Y . X is set

F

Y is set

x is set

[Y,x] is set

{Y,x} is non empty set

{Y} is non empty set

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

X is set

[Y,X] is set

{Y,X} is non empty set

{{Y,X},{Y}} is non empty set

f is Relation-like Function-like set

p is Relation-like Function-like set

f \/ p is Relation-like set

q is Relation-like Function-like set

Y is set

union Y is set

x is set

X is set

[x,X] is set

{x,X} is non empty set

{x} is non empty set

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

f is set

[x,f] is set

{x,f} is non empty set

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

p is set

q is set

p is Relation-like Function-like set

q is Relation-like Function-like set

x is set

X is set

f is Relation-like Function-like set

Y is set

X is set

x is Relation-like Y -valued Function-like set

dom x is set

x . X is set

Y is non empty set

x is non empty set

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

bool [:Y,x:] is non empty set

choose Y is Element of Y

choose x is Element of x

[(choose Y),(choose x)] is set

{(choose Y),(choose x)} is non empty set

{(choose Y)} is non empty set

{{(choose Y),(choose x)},{(choose Y)}} is non empty set

{[(choose Y),(choose x)]} is Relation-like Function-like non empty set

X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]

Y is set

x is set

(Y,x) is non empty set

X is set

f is Relation-like Function-like set

dom f is set

rng f is set

X is Relation-like Function-like set

rng X is set

Y is Relation-like Function-like set

dom Y is set

x is Relation-like Function-like set

dom x is set

X * Y is Relation-like Function-like set

X * x is Relation-like Function-like set

dom (X * x) is set

dom X is set

dom (X * Y) is set

f is set

(X * x) . f is set

X . f is set

x . (X . f) is set

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

(X * Y) . f is set

Y . (X . f) is set

Y is set

x is set

X is set

f is Relation-like Y -valued Function-like set

f | X is Relation-like Y -valued Function-like set

dom (f | X) is set

(Y,(f | X),x) is Element of Y

(Y,f,x) is Element of Y

dom f is set

(f | X) . x is set

f . x is set