:: PARTFUN1 semantic presentation

dom Y is set

dom x is set
(dom Y) /\ (dom x) is 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

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

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
F1() is set
Y is set
F2(Y) is set
F3(Y) is set
Y is set
x is set
F2(Y) is set
F3(Y) is set
X is set

Y is set

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

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

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

dom X is Element of bool Y
bool Y is non empty set

dom f is Element of bool Y
p is set
X . p is set
f . p is set
F1() is set
F2() is set
[:F1(),F2():] is Relation-like set
bool [:F1(),F2():] is non empty set
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

dom x is set
X is 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 F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
q is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom q is Element of bool F1()
bool F1() is non empty set
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

dom Y is set
rng Y is set
x is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
X is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom X is Element of bool F1()
f is set
p is set
q is set
f is set
X . f is set
Y is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom Y is Element of bool F1()
x is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom x is Element of bool F1()
F2() is set
F1() is set
[:F1(),F2():] is Relation-like set
bool [:F1(),F2():] is non empty set
Y is set
x is set
F3(Y) is set
X is set
Y is set
x is set
F3(Y) is set
Y is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom Y is Element of bool F1()
bool F1() is non empty set
x is set
F3(x) is set
X is set
F3(x) is set
X is set
x is set
Y . x is set
F3(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 set
[:X,f:] is Relation-like set
bool [:X,f:] is non empty 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

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

(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

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

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

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

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

X is set

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

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

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

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

(Y |` 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 .: 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

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

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

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

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

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

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

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

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

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

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

dom X is Element of bool Y
bool Y is non empty set

dom f is Element of bool Y
p is set
X . p is set
f . p is set
X is 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,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) | Y 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) | 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,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,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

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

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

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

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

rng f is 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) | 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) | 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),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,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) | Y 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) | Y is Relation-like Function-like set
(X,Y,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 ")) | 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,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
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

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

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

bool Y is non empty set
Y is non empty set

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

bool Y is non empty 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) | 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

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

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

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

dom q is set
rng q is set

dom q is set
rng q is set
Y is set
x is set
(Y,x) is 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

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

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

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

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

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

bool [:Y,{}:] is non empty 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

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

dom X is 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

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

f is set
Y . f is set
x . f is set

dom Y is set

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

dom Y is set

dom x is set
X is set
Y . X is set
x . X is set

dom Y is set

dom x is set

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

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

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

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

Y is set

Y is set
x is set

(Y |` X) | 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) | 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

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

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

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

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

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

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
f is set
q is set
p is set

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

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

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

(Y,x,X) is set

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

(Y,x,X) is set

Y is non empty set

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

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

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

(Y,x,X) is set
{X} is functional non empty set
f is set

Y is set

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

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

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

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

(Y,x,X) is set

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

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

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

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

dom x is Element of bool Y
bool Y is non empty set
Y is 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

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

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

Y is set

[:Y,Y:] is Relation-like set
bool [:Y,Y:] is non empty set
F1() is non empty set

dom Y is set
x is Element of F1()
Y . x is set
F2(x) is set
X is Element of F1()
Y . X is set
F3(X) is set
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

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

x is set
X is set

Y is set
X is 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
[(),()] is set
{(),()} is non empty set
{()} is non empty set
{{(),()},{()}} is non empty set
{[(),()]} is Relation-like Function-like non empty set

Y is set
x is set
(Y,x) is non empty set
X is set

dom f is set
rng f is set

rng X is set

dom Y is set

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

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