:: PARTFUN2 semantic presentation

{} is set
the Function-like functional empty set is Function-like functional empty set
Y is non empty set
f is non empty set
K20(f,Y) is set
K19(K20(f,Y)) is set
g is Relation-like f -defined Y -valued Function-like Element of K19(K20(f,Y))
dom g is Element of K19(f)
K19(f) is set
x is Relation-like f -defined Y -valued Function-like Element of K19(K20(f,Y))
dom x is Element of K19(f)
f is set
x is Element of f
g /. x is Element of Y
x /. x is Element of Y
g . x is set
g . f is set
x . f is set
Y is set
f is non empty set
g is non empty set
K20(g,f) is set
K19(K20(g,f)) is set
x is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
rng x is Element of K19(f)
K19(f) is set
dom x is Element of K19(g)
K19(g) is set
f is set
x . f is set
x is Element of g
x /. x is Element of f
f is Element of g
x /. f is Element of f
x . f is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is non empty set
K20(g,Y) is set
K19(K20(g,Y)) is set
K20(g,f) is set
K19(K20(g,f)) is set
x is Relation-like g -defined Y -valued Function-like Element of K19(K20(g,Y))
dom x is Element of K19(g)
K19(g) is set
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
f * x is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
dom f is Element of K19(Y)
K19(Y) is set
x is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
dom x is Element of K19(g)
x is Element of g
x /. x is Element of Y
x . x is set
x . x is set
x is Element of g
x /. x is Element of Y
c₈ is Element of g
x /. c₈ is Element of Y
x is Element of g
x /. x is Element of f
x /. x is Element of Y
f /. (x /. x) is Element of f
x . x is set
x . x is set
f . (x . x) is set
f . (x /. x) is set
x is set
x . x is set
c₈ is Element of g
x /. c₈ is Element of Y
c₈ is Element of g
x /. c₈ is Element of Y
x is set
c₈ is Element of g
x /. c₈ is Element of f
x /. c₈ is Element of Y
f /. (x /. c₈) is Element of f
x . c₈ is set
x . x is set
f . (x /. c₈) is set
x . x is set
f . (x . x) is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is non empty set
K20(f,g) is set
K19(K20(f,g)) is set
x is Element of Y
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom f is Element of K19(Y)
K19(Y) is set
f /. x is Element of f
x is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
dom x is Element of K19(f)
K19(f) is set
x * f is Relation-like Y -defined g -valued Function-like Element of K19(K20(Y,g))
K20(Y,g) is set
K19(K20(Y,g)) is set
(x * f) /. x is Element of g
x /. (f /. x) is Element of g
dom (x * f) is Element of K19(Y)
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is non empty set
K20(f,g) is set
K19(K20(f,g)) is set
x is Element of Y
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
rng f is Element of K19(f)
K19(f) is set
dom f is Element of K19(Y)
K19(Y) is set
f /. x is Element of f
x is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
dom x is Element of K19(f)
x * f is Relation-like Y -defined g -valued Function-like Element of K19(K20(Y,g))
K20(Y,g) is set
K19(K20(Y,g)) is set
(x * f) /. x is Element of g
x /. (f /. x) is Element of g
Y is non empty set
K19(Y) is set
f is Element of K19(Y)
id f is Relation-like Function-like one-to-one set
K20(Y,Y) is set
K19(K20(Y,Y)) is set
id f is Relation-like f -defined f -valued Function-like one-to-one total Element of K19(K20(f,f))
K20(f,f) is set
K19(K20(f,f)) is set
dom (id f) is Element of K19(f)
K19(f) is set
rng (id f) is Element of K19(f)
Y is non empty set
K19(Y) is set
K20(Y,Y) is set
K19(K20(Y,Y)) is set
f is Element of K19(Y)
(Y,f) is Relation-like Y -defined Y -valued Function-like one-to-one Element of K19(K20(Y,Y))
g is Relation-like Y -defined Y -valued Function-like Element of K19(K20(Y,Y))
dom g is Element of K19(Y)
x is Element of Y
g /. x is Element of Y
g . x is set
x is set
f is Element of Y
g /. f is Element of Y
g . x is set
Y is non empty set
K19(Y) is set
K20(Y,Y) is set
K19(K20(Y,Y)) is set
f is Element of K19(Y)
(Y,f) is Relation-like Y -defined Y -valued Function-like one-to-one Element of K19(K20(Y,Y))
g is Element of Y
x is Relation-like Y -defined Y -valued Function-like Element of K19(K20(Y,Y))
dom x is Element of K19(Y)
(dom x) /\ f is Element of K19(Y)
x /. g is Element of Y
x * (Y,f) is Relation-like Y -defined Y -valued Function-like Element of K19(K20(Y,Y))
(x * (Y,f)) /. g is Element of Y
x . g is set
(x * (Y,f)) . g is set
dom (Y,f) is Element of K19(Y)
(Y,f) /. g is Element of Y
dom (x * (Y,f)) is Element of K19(Y)
Y is non empty set
K19(Y) is set
K20(Y,Y) is set
K19(K20(Y,Y)) is set
f is Element of K19(Y)
(Y,f) is Relation-like Y -defined Y -valued Function-like one-to-one Element of K19(K20(Y,Y))
g is Element of Y
x is Relation-like Y -defined Y -valued Function-like Element of K19(K20(Y,Y))
(Y,f) * x is Relation-like Y -defined Y -valued Function-like Element of K19(K20(Y,Y))
dom ((Y,f) * x) is Element of K19(Y)
dom x is Element of K19(Y)
x /. g is Element of Y
dom (Y,f) is Element of K19(Y)
dom (Y,f) is Element of K19(Y)
Y is non empty set
f is non empty set
K20(f,Y) is set
K19(K20(f,Y)) is set
g is Relation-like f -defined Y -valued Function-like Element of K19(K20(f,Y))
dom g is Element of K19(f)
K19(f) is set
x is set
f is set
g . x is set
g . f is set
x is Element of f
g /. x is Element of Y
x is Element of f
g . x is set
g /. x is Element of Y
Y is set
f is set
g is non empty set
x is non empty set
K20(g,x) is set
K19(K20(g,x)) is set
f is Relation-like g -defined x -valued Function-like Element of K19(K20(g,x))
dom f is Element of K19(g)
K19(g) is set
f /. Y is Element of x
f /. f is Element of x
f . Y is set
f . f is set
Y is set
f is set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Relation-like Y -defined f -valued Function-like one-to-one Element of K19(K20(Y,f))
g " is Relation-like Function-like one-to-one set
K20(f,Y) is set
K19(K20(f,Y)) is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
K20(f,Y) is set
K19(K20(f,Y)) is set
g is Relation-like Y -defined f -valued Function-like one-to-one Element of K19(K20(Y,f))
(Y,f,g) is Relation-like f -defined Y -valued Function-like one-to-one Element of K19(K20(f,Y))
rng g is Element of K19(f)
K19(f) is set
dom g is Element of K19(Y)
K19(Y) is set
x is Relation-like f -defined Y -valued Function-like Element of K19(K20(f,Y))
dom x is Element of K19(f)
f is Element of f
x /. f is Element of Y
x is Element of Y
g /. x is Element of f
x . f is set
g . x is set
g . x is set
x . f is set
dom (Y,f,g) is Element of K19(f)
dom (Y,f,g) is Element of K19(f)
f is Element of f
(Y,f,g) /. f is Element of Y
x /. f is Element of Y
f is Element of f
(Y,f,g) /. f is Element of Y
x /. f is Element of Y
rng (Y,f,g) is Element of K19(Y)
(Y,f,g) . f is set
g . ((Y,f,g) . f) is set
g . ((Y,f,g) /. f) is set
g /. ((Y,f,g) /. f) is Element of f
dom (Y,f,g) is Element of K19(f)
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of Y
x is Relation-like Y -defined f -valued Function-like one-to-one Element of K19(K20(Y,f))
dom x is Element of K19(Y)
K19(Y) is set
(Y,f,x) is Relation-like f -defined Y -valued Function-like one-to-one Element of K19(K20(f,Y))
K20(f,Y) is set
K19(K20(f,Y)) is set
x /. g is Element of f
(Y,f,x) /. (x /. g) is Element of Y
(Y,f,x) * x is Relation-like Y -defined Y -valued Function-like one-to-one Element of K19(K20(Y,Y))
K20(Y,Y) is set
K19(K20(Y,Y)) is set
((Y,f,x) * x) /. g is Element of Y
rng x is Element of K19(f)
K19(f) is set
dom (Y,f,x) is Element of K19(f)
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of f
x is Relation-like Y -defined f -valued Function-like one-to-one Element of K19(K20(Y,f))
rng x is Element of K19(f)
K19(f) is set
(Y,f,x) is Relation-like f -defined Y -valued Function-like one-to-one Element of K19(K20(f,Y))
K20(f,Y) is set
K19(K20(f,Y)) is set
(Y,f,x) /. g is Element of Y
x /. ((Y,f,x) /. g) is Element of f
x * (Y,f,x) is Relation-like f -defined f -valued Function-like one-to-one Element of K19(K20(f,f))
K20(f,f) is set
K19(K20(f,f)) is set
(x * (Y,f,x)) /. g is Element of f
(x * (Y,f,x)) . g is set
dom (x * (Y,f,x)) is Element of K19(f)
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
K20(f,Y) is set
K19(K20(f,Y)) is set
g is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom g is Element of K19(Y)
K19(Y) is set
rng g is Element of K19(f)
K19(f) is set
g " is Relation-like Function-like set
x is Relation-like f -defined Y -valued Function-like Element of K19(K20(f,Y))
rng x is Element of K19(Y)
dom x is Element of K19(f)
f is set
x is set
g . f is set
x . x is set
c₈ is Element of Y
g /. c₈ is Element of f
x is Element of f
x /. x is Element of Y
x is Element of f
x /. x is Element of Y
c₈ is Element of Y
g /. c₈ is Element of f
Y is set
f is non empty set
g is non empty set
K20(g,f) is set
K19(K20(g,f)) is set
x is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
dom x is Element of K19(g)
K19(g) is set
f is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
f | Y is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
dom f is Element of K19(g)
(dom f) /\ Y is Element of K19(g)
x is Element of g
x /. x is Element of f
f /. x is Element of f
x . x is set
f . x is set
x is set
x is Element of g
x /. x is Element of f
f /. x is Element of f
x . x is set
x . x is set
f . x is set
Y is set
f is non empty set
g is non empty set
K20(f,g) is set
K19(K20(f,g)) is set
x is Element of f
f is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
dom f is Element of K19(f)
K19(f) is set
(dom f) /\ Y is Element of K19(f)
f | Y is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
(f | Y) /. x is Element of g
f /. x is Element of g
dom (f | Y) is Element of K19(f)
Y is set
f is non empty set
g is non empty set
K20(f,g) is set
K19(K20(f,g)) is set
x is Element of f
f is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
dom f is Element of K19(f)
K19(f) is set
f | Y is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
(f | Y) /. x is Element of g
f /. x is Element of g
(dom f) /\ Y is Element of K19(f)
Y is set
f is non empty set
g is non empty set
K20(f,g) is set
K19(K20(f,g)) is set
x is Element of f
f is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
dom f is Element of K19(f)
K19(f) is set
f /. x is Element of g
f | Y is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
rng (f | Y) is Element of K19(g)
K19(g) is set
f . x is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is set
x is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
g |` x is Relation-like Function-like set
Y is set
f is non empty set
g is non empty set
K20(g,f) is set
K19(K20(g,f)) is set
x is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
dom x is Element of K19(g)
K19(g) is set
f is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
(g,f,Y,f) is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
dom f is Element of K19(g)
x is Element of g
f /. x is Element of f
f . x is set
f . x is set
x is Element of g
f /. x is Element of f
x is Element of g
f /. x is Element of f
x is Element of g
x /. x is Element of f
f /. x is Element of f
x . x is set
f . x is set
x is set
f . x is set
x is Element of g
f /. x is Element of f
x is Element of g
f /. x is Element of f
x is set
x is Element of g
x /. x is Element of f
f /. x is Element of f
x . x is set
x . x is set
f . x is set
f is non empty set
g is non empty set
K20(f,g) is set
K19(K20(f,g)) is set
x is non empty set
c₈ is non empty set
K20(x,c₈) is set
K19(K20(x,c₈)) is set
x is Element of f
Y is set
f is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
(f,g,Y,f) is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
dom (f,g,Y,f) is Element of K19(f)
K19(f) is set
dom f is Element of K19(f)
f /. x is Element of g
d2 is Element of x
c is Relation-like x -defined c₈ -valued Function-like Element of K19(K20(x,c₈))
dom c is Element of K19(x)
K19(x) is set
c /. d2 is Element of c₈
x is set
(x,c₈,x,c) is Relation-like x -defined c₈ -valued Function-like Element of K19(K20(x,c₈))
dom (x,c₈,x,c) is Element of K19(x)
f is non empty set
g is non empty set
K20(f,g) is set
K19(K20(f,g)) is set
x is Element of f
Y is set
f is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
(f,g,Y,f) is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
dom (f,g,Y,f) is Element of K19(f)
K19(f) is set
(f,g,Y,f) /. x is Element of g
f /. x is Element of g
Y is set
f is non empty set
K19(f) is set
g is non empty set
K20(g,f) is set
K19(K20(g,f)) is set
x is Element of K19(f)
f is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
f .: Y is Element of K19(f)
dom f is Element of K19(g)
K19(g) is set
x is Element of f
x is set
f . x is set
c₈ is Element of g
f /. c₈ is Element of f
x is Element of g
f /. x is Element of f
f . x is set
x is set
x is Element of f
c₈ is Element of g
f /. c₈ is Element of f
f . c₈ is set
x is set
f . x is set
c₈ is Element of g
f /. c₈ is Element of f
g is non empty set
f is non empty set
K20(f,g) is set
K19(K20(f,g)) is set
c₈ is non empty set
x is non empty set
K20(x,c₈) is set
K19(K20(x,c₈)) is set
x is Element of g
f is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
Y is set
f .: Y is Element of K19(g)
K19(g) is set
dom f is Element of K19(f)
K19(f) is set
c₁₁ is Element of x
c is Relation-like x -defined c₈ -valued Function-like Element of K19(K20(x,c₈))
dom c is Element of K19(x)
K19(x) is set
x is set
d2 is Element of c₈
c /. c₁₁ is Element of c₈
c .: x is Element of K19(c₈)
K19(c₈) is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of Y
x is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom x is Element of K19(Y)
K19(Y) is set
Im (x,g) is set
x /. g is Element of f
{(x /. g)} is set
x . g is set
{(x . g)} is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of Y
x is Element of Y
{g,x} is set
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom f is Element of K19(Y)
K19(Y) is set
f .: {g,x} is Element of K19(f)
K19(f) is set
f /. g is Element of f
f /. x is Element of f
{(f /. g),(f /. x)} is set
f . g is set
f . x is set
{(f . g),(f . x)} is set
{(f /. g),(f . x)} is set
Y is set
f is non empty set
g is non empty set
K19(g) is set
K20(g,f) is set
K19(K20(g,f)) is set
x is Element of K19(g)
f is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
f " Y is Element of K19(g)
dom f is Element of K19(g)
x is Element of g
f /. x is Element of f
f . x is set
f . x is set
x is set
f . x is set
x is Element of g
f /. x is Element of f
x is Element of g
f /. x is Element of f
Y is non empty set
f is non empty set
K20(f,Y) is set
K19(K20(f,Y)) is set
g is Relation-like f -defined Y -valued Function-like Element of K19(K20(f,Y))
dom g is Element of K19(f)
K19(f) is set
x is Relation-like f -defined Y -valued Function-like V18(f,Y) Element of K19(K20(f,Y))
f is Element of f
x . f is Element of Y
g /. f is Element of Y
g . f is set
Y is non empty set
f is non empty set
K20(f,Y) is set
K19(K20(f,Y)) is set
g is Relation-like f -defined Y -valued Function-like Element of K19(K20(f,Y))
dom g is Element of K19(f)
K19(f) is set
x is Relation-like f -defined Y -valued Function-like Element of K19(K20(f,Y))
dom x is Element of K19(f)
(dom g) /\ (dom x) is Element of K19(f)
f is Element of f
g /. f is Element of Y
x /. f is Element of Y
g . f is set
x . f is set
f is set
x is Element of f
g /. x is Element of Y
x /. x is Element of Y
g . f is set
x . f is set
F₁() is non empty set
F₂() is non empty set
K20(F₁(),F₂()) is set
K19(K20(F₁(),F₂())) is set
the Element of F₂() is Element of F₂()
f is set
g is set
K19(F₁()) is set
x is Element of F₁()
f is Element of F₂()
x is Element of F₂()
x is Element of F₂()
x is Relation-like F₁() -defined F₂() -valued Function-like V18(F₁(),F₂()) Element of K19(K20(F₁(),F₂()))
g is Element of K19(F₁())
x | g is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
f is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
dom f is Element of K19(F₁())
dom x is Element of K19(F₁())
x is Element of F₁()
x is Element of F₂()
(dom x) /\ g is Element of K19(F₁())
x is Element of F₁()
f /. x is Element of F₂()
x . x is Element of F₂()
x is Element of F₂()
f . x is set
F₂() is non empty set
F₁() is non empty set
K20(F₁(),F₂()) is set
K19(K20(F₁(),F₂())) is set
Y is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
dom Y is Element of K19(F₁())
K19(F₁()) is set
f is Element of F₁()
F₃(f) is Element of F₂()
g is Element of F₂()
F₃(f) is Element of F₂()
g is Element of F₂()
f is Element of F₁()
Y /. f is Element of F₂()
F₃(f) is Element of F₂()
F₂() is non empty set
F₁() is non empty set
K20(F₁(),F₂()) is set
K19(K20(F₁(),F₂())) is set
F₃() is set
Y is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
dom Y is Element of K19(F₁())
K19(F₁()) is set
f is Relation-like F₁() -defined F₂() -valued Function-like Element of K19(K20(F₁(),F₂()))
dom f is Element of K19(F₁())
g is Element of F₁()
Y /. g is Element of F₂()
F₄(g) is Element of F₂()
f /. g is Element of F₂()
Y is non empty set
K19(Y) is set
f is non empty set
g is Element of K19(Y)
x is Element of f
g --> x is set
K20(Y,f) is set
K19(K20(Y,f)) is set
g --> x is Relation-like g -defined f -valued Function-like V18(g,f) Element of K19(K20(g,f))
K20(g,f) is set
K19(K20(g,f)) is set
dom (g --> x) is Element of K19(g)
K19(g) is set
Y is non empty set
K19(Y) is set
f is non empty set
g is Element of K19(Y)
x is Element of Y
f is Element of f
(Y,f,g,f) is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
K20(Y,f) is set
K19(K20(Y,f)) is set
(Y,f,g,f) /. x is Element of f
dom (Y,f,g,f) is Element of K19(Y)
(Y,f,g,f) . x is set
Y is non empty set
f is non empty set
K20(f,Y) is set
K19(K20(f,Y)) is set
g is Element of Y
x is Relation-like f -defined Y -valued Function-like Element of K19(K20(f,Y))
dom x is Element of K19(f)
K19(f) is set
(f,Y,(dom x),g) is Relation-like f -defined Y -valued Function-like Element of K19(K20(f,Y))
f is set
x is Element of f
x /. x is Element of Y
x . f is set
Y is non empty set
K19(Y) is set
f is non empty set
g is non empty set
K20(f,g) is set
K19(K20(f,g)) is set
x is Element of K19(Y)
f is Element of f
(Y,f,x,f) is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
K20(Y,f) is set
K19(K20(Y,f)) is set
x is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
dom x is Element of K19(f)
K19(f) is set
x * (Y,f,x,f) is Relation-like Y -defined g -valued Function-like Element of K19(K20(Y,g))
K20(Y,g) is set
K19(K20(Y,g)) is set
x /. f is Element of g
(Y,g,x,(x /. f)) is Relation-like Y -defined g -valued Function-like Element of K19(K20(Y,g))
x . f is set
x --> (x . f) is Relation-like x -defined {(x . f)} -valued Function-like V18(x,{(x . f)}) Element of K19(K20(x,{(x . f)}))
{(x . f)} is set
K20(x,{(x . f)}) is set
K19(K20(x,{(x . f)})) is set
Y is non empty set
K19(Y) is set
f is Element of K19(Y)
(Y,f) is Relation-like Y -defined Y -valued Function-like one-to-one Element of K19(K20(Y,Y))
K20(Y,Y) is set
K19(K20(Y,Y)) is set
dom (Y,f) is Element of K19(Y)
dom (Y,f) is Element of K19(Y)
Y is non empty set
K19(Y) is set
f is non empty set
g is Element of K19(Y)
x is Element of f
(Y,f,g,x) is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
K20(Y,f) is set
K19(K20(Y,f)) is set
dom (Y,f,g,x) is Element of K19(Y)
Y is non empty set
f is non empty set
K19(f) is set
g is Element of K19(f)
x is Element of Y
(f,Y,g,x) is Relation-like f -defined Y -valued Function-like Element of K19(K20(f,Y))
K20(f,Y) is set
K19(K20(f,Y)) is set
dom (f,Y,g,x) is Element of K19(f)
dom (f,Y,g,x) is Element of K19(f)
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom g is Element of K19(Y)
K19(Y) is set
the Element of f is Element of f
f is Element of Y
g . f is set
x is set
f is Element of Y
g /. f is Element of f
x is Element of f
x is Element of Y
g . x is set
g . f is set
x is Element of f
f is set
dom g is set
x is set
g . f is set
g . x is set
Y is set
f is non empty set
g is non empty set
K20(g,f) is set
K19(K20(g,f)) is set
x is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
x | Y is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
dom x is Element of K19(g)
K19(g) is set
Y /\ (dom x) is Element of K19(g)
dom (x | Y) is Element of K19(g)
f is Element of f
x is Element of g
x /. x is Element of f
x . x is set
(x | Y) . x is set
f is Element of f
dom (x | Y) is Element of K19(g)
x is Element of g
(x | Y) . x is set
x . x is set
x /. x is Element of f
Y is set
f is non empty set
g is non empty set
K20(g,f) is set
K19(K20(g,f)) is set
x is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
x | Y is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
dom x is Element of K19(g)
K19(g) is set
Y /\ (dom x) is Element of K19(g)
f is Element of f
x is Element of g
x /. x is Element of f
x is Element of g
x /. x is Element of f
the Element of f is Element of f
x is Element of g
x /. x is Element of f
x is Element of f
f is Element of f
the Element of Y /\ (dom x) is Element of Y /\ (dom x)
x is Element of g
x /. x is Element of f
x is Element of g
x /. x is Element of f
Y is set
f is non empty set
g is non empty set
K20(f,g) is set
K19(K20(f,g)) is set
x is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
dom x is Element of K19(f)
K19(f) is set
x | Y is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
rng (x | Y) is Element of K19(g)
K19(g) is set
Y /\ (dom x) is Element of K19(f)
f is Element of g
{f} is set
x is set
dom (x | Y) is Element of K19(f)
x is set
(x | Y) . x is set
c₈ is Element of f
x /. c₈ is Element of g
(x | Y) /. c₈ is Element of g
the Element of Y /\ (dom x) is Element of Y /\ (dom x)
c₈ is set
dom (x | Y) is Element of K19(f)
x is Element of f
(x | Y) /. x is Element of g
x /. x is Element of g
f is Element of g
{f} is set
dom (x | Y) is Element of K19(f)
x is Element of f
(x | Y) . x is set
(x | Y) /. x is Element of g
Y is set
f is set
g is non empty set
x is non empty set
K20(g,x) is set
K19(K20(g,x)) is set
f is Relation-like g -defined x -valued Function-like Element of K19(K20(g,x))
f | Y is Relation-like g -defined x -valued Function-like Element of K19(K20(g,x))
f | f is Relation-like g -defined x -valued Function-like Element of K19(K20(g,x))
dom f is Element of K19(g)
K19(g) is set
Y /\ (dom f) is Element of K19(g)
x is Element of x
x is Element of g
f /\ (dom f) is Element of K19(g)
f /. x is Element of x
Y is set
f is non empty set
g is non empty set
K20(f,g) is set
K19(K20(f,g)) is set
x is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
dom x is Element of K19(f)
K19(f) is set
x | Y is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
Y /\ (dom x) is Element of K19(f)
the Element of g is Element of g
x is Element of f
x /. x is Element of g
x is Element of g
f is Element of g
Y is non empty set
K19(Y) is set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of K19(Y)
x is Element of f
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
f | g is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom (f | g) is Element of K19(Y)
(Y,f,(dom (f | g)),x) is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
x is Element of Y
dom f is Element of K19(Y)
g /\ (dom f) is Element of K19(Y)
(f | g) /. x is Element of f
f /. x is Element of f
Y is set
{Y} is set
f is non empty set
g is non empty set
K20(f,g) is set
K19(K20(f,g)) is set
x is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
x | {Y} is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
dom x is Element of K19(f)
K19(f) is set
{Y} /\ (dom x) is Element of K19(f)
dom x is Element of K19(f)
K19(f) is set
{Y} /\ (dom x) is Element of K19(f)
the Element of {Y} /\ (dom x) is Element of {Y} /\ (dom x)
x is Element of f
x /. x is Element of g
c₈ is Element of f
x /. c₈ is Element of g
dom x is Element of K19(f)
K19(f) is set
{Y} /\ (dom x) is Element of K19(f)
Y is set
f is set
Y /\ f is set
Y \/ f is set
g is non empty set
x is non empty set
K20(g,x) is set
K19(K20(g,x)) is set
f is Relation-like g -defined x -valued Function-like Element of K19(K20(g,x))
f | Y is Relation-like g -defined x -valued Function-like Element of K19(K20(g,x))
f | f is Relation-like g -defined x -valued Function-like Element of K19(K20(g,x))
dom f is Element of K19(g)
K19(g) is set
f | (Y \/ f) is Relation-like g -defined x -valued Function-like Element of K19(K20(g,x))
(Y /\ f) /\ (dom f) is Element of K19(g)
Y /\ (dom f) is Element of K19(g)
x is Element of x
the Element of (Y /\ f) /\ (dom f) is Element of (Y /\ f) /\ (dom f)
c₈ is Element of g
f /\ (dom f) is Element of K19(g)
d2 is Element of x
f /. c₈ is Element of x
dom (f | (Y \/ f)) is Element of K19(g)
c is Element of g
(f | (Y \/ f)) . c is set
(Y \/ f) /\ (dom f) is Element of K19(g)
f /. c is Element of x
f /. c is Element of x
f /. c is Element of x
f /. c is Element of x
(f | (Y \/ f)) /. c is Element of x
Y is set
f is set
g is non empty set
x is non empty set
K20(g,x) is set
K19(K20(g,x)) is set
f is Relation-like g -defined x -valued Function-like Element of K19(K20(g,x))
f | Y is Relation-like g -defined x -valued Function-like Element of K19(K20(g,x))
f | f is Relation-like g -defined x -valued Function-like Element of K19(K20(g,x))
(f | f) | Y is Relation-like g -defined x -valued Function-like Element of K19(K20(g,x))
dom f is Element of K19(g)
K19(g) is set
Y /\ (dom f) is Element of K19(g)
x is Element of x
dom ((f | f) | Y) is Element of K19(g)
x is Element of g
((f | f) | Y) . x is set
dom (f | f) is Element of K19(g)
Y /\ (dom (f | f)) is Element of K19(g)
(dom f) /\ f is Element of K19(g)
f /. x is Element of x
(f | f) /. x is Element of x
((f | f) | Y) /. x is Element of x
Y is non empty set
K19(Y) is set
f is non empty set
g is Element of K19(Y)
x is Element of f
(Y,f,g,x) is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
K20(Y,f) is set
K19(K20(Y,f)) is set
(Y,f,g,x) | g is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom ((Y,f,g,x) | g) is Element of K19(Y)
f is Element of Y
((Y,f,g,x) | g) . f is set
dom (Y,f,g,x) is Element of K19(Y)
g /\ (dom (Y,f,g,x)) is Element of K19(Y)
(Y,f,g,x) /. f is Element of f
((Y,f,g,x) | g) /. f is Element of f
Y is non empty set
f is non empty set
K20(f,Y) is set
K19(K20(f,Y)) is set
g is Relation-like f -defined Y -valued Function-like Element of K19(K20(f,Y))
dom g is Element of K19(f)
K19(f) is set
x is Relation-like f -defined Y -valued Function-like Element of K19(K20(f,Y))
dom x is Element of K19(f)
f is set
x is Element of f
g /. x is Element of Y
x /. x is Element of Y
g . f is set
x . f is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of Y
x is Element of f
[g,x] is set
{g,x} is set
{g} is set
{{g,x},{g}} is set
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom f is Element of K19(Y)
K19(Y) is set
f /. g is Element of f
f . g is set
f . g is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is non empty set
K20(f,g) is set
K19(K20(f,g)) is set
x is Element of Y
f is Element of g
[x,f] is set
{x,f} is set
{x} is set
{{x,f},{x}} is set
x is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
x /. x is Element of f
[x,(x /. x)] is set
{x,(x /. x)} is set
{{x,(x /. x)},{x}} is set
[(x /. x),f] is set
{(x /. x),f} is set
{(x /. x)} is set
{{(x /. x),f},{(x /. x)}} is set
x is Relation-like f -defined g -valued Function-like Element of K19(K20(f,g))
x * x is Relation-like Y -defined g -valued Function-like Element of K19(K20(Y,g))
K20(Y,g) is set
K19(K20(Y,g)) is set
x . x is set
[(x . x),f] is set
{(x . x),f} is set
{(x . x)} is set
{{(x . x),f},{(x . x)}} is set
[x,(x . x)] is set
{x,(x . x)} is set
{{x,(x . x)},{x}} is set
dom x is Element of K19(Y)
K19(Y) is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of Y
x is Element of f
[g,x] is set
{g,x} is set
{g} is set
{{g,x},{g}} is set
{[g,x]} is Function-like set
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
f /. g is Element of f
dom f is Element of K19(Y)
K19(Y) is set
f . g is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of Y
{g} is set
x is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom x is Element of K19(Y)
K19(Y) is set
x /. g is Element of f
[g,(x /. g)] is set
{g,(x /. g)} is set
{{g,(x /. g)},{g}} is set
{[g,(x /. g)]} is Function-like set
x . g is set
[g,(x . g)] is set
{g,(x . g)} is set
{{g,(x . g)},{g}} is set
{[g,(x . g)]} is Function-like set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of Y
x is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom x is Element of K19(Y)
K19(Y) is set
x /. g is Element of f
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
f /. g is Element of f
x is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
f /\ x is Relation-like Y -defined f -valued Element of K19(K20(Y,f))
x /. g is Element of f
x . g is set
x . g is set
[g,(x . g)] is set
{g,(x . g)} is set
{g} is set
{{g,(x . g)},{g}} is set
dom f is Element of K19(Y)
dom x is Element of K19(Y)
f . g is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of Y
x is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom x is Element of K19(Y)
K19(Y) is set
x /. g is Element of f
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
f /. g is Element of f
x is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
x \/ x is Relation-like Y -defined f -valued Element of K19(K20(Y,f))
x . g is set
[g,(x . g)] is set
{g,(x . g)} is set
{g} is set
{{g,(x . g)},{g}} is set
dom f is Element of K19(Y)
f . g is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of Y
x is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom x is Element of K19(Y)
K19(Y) is set
x /. g is Element of f
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
f /. g is Element of f
x is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
x \/ x is Relation-like Y -defined f -valued Element of K19(K20(Y,f))
x . g is set
[g,(x . g)] is set
{g,(x . g)} is set
{g} is set
{{g,(x . g)},{g}} is set
dom f is Element of K19(Y)
f . g is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of Y
x is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom x is Element of K19(Y)
K19(Y) is set
x /. g is Element of f
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
f /. g is Element of f
x is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
f \/ x is Relation-like Y -defined f -valued Element of K19(K20(Y,f))
x /. g is Element of f
[g,(x /. g)] is set
{g,(x /. g)} is set
{g} is set
{{g,(x /. g)},{g}} is set
dom f is Element of K19(Y)
[g,(f /. g)] is set
{g,(f /. g)} is set
{{g,(f /. g)},{g}} is set
dom x is Element of K19(Y)
[g,(x /. g)] is set
{g,(x /. g)} is set
{{g,(x /. g)},{g}} is set
dom f is Element of K19(Y)
dom x is Element of K19(Y)
Y is non empty set
K19(Y) is set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of K19(Y)
x is Element of Y
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom f is Element of K19(Y)
f /. x is Element of f
[x,(f /. x)] is set
{x,(f /. x)} is set
{x} is set
{{x,(f /. x)},{x}} is set
f | g is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
f . x is set
[x,(f . x)] is set
{x,(f . x)} is set
{{x,(f . x)},{x}} is set
dom (f | g) is Element of K19(Y)
(dom f) /\ g is Element of K19(Y)
Y is non empty set
f is non empty set
K19(f) is set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of K19(f)
x is Element of Y
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
dom f is Element of K19(Y)
K19(Y) is set
f /. x is Element of f
[x,(f /. x)] is set
{x,(f /. x)} is set
{x} is set
{{x,(f /. x)},{x}} is set
(Y,f,g,f) is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
f . x is set
[x,(f . x)] is set
{x,(f . x)} is set
{{x,(f . x)},{x}} is set
dom (Y,f,g,f) is Element of K19(Y)
f . x is set
Y is non empty set
f is non empty set
K19(f) is set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of K19(f)
x is Element of Y
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
f " g is Element of K19(Y)
K19(Y) is set
f /. x is Element of f
[x,(f /. x)] is set
{x,(f /. x)} is set
{x} is set
{{x,(f /. x)},{x}} is set
f . x is set
[x,(f . x)] is set
{x,(f . x)} is set
{{x,(f . x)},{x}} is set
dom f is Element of K19(Y)
dom f is Element of K19(Y)
Y is set
f is non empty set
g is non empty set
K20(g,f) is set
K19(K20(g,f)) is set
x is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
x | Y is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
dom x is Element of K19(g)
K19(g) is set
Y /\ (dom x) is Element of K19(g)
f is Element of f
x is Element of g
x . x is set
x /. x is Element of f
x is Element of f
f is Element of f
dom (x | Y) is Element of K19(g)
x is Element of g
(x | Y) . x is set
(x | Y) /. x is Element of f
x /. x is Element of f
x . x is set
Y is set
f is non empty set
g is non empty set
K20(g,f) is set
K19(K20(g,f)) is set
x is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
x | Y is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
dom x is Element of K19(g)
K19(g) is set
Y /\ (dom x) is Element of K19(g)
f is Element of f
x is Element of g
x . x is set
x is Element of g
x . x is set
the Element of f is Element of f
x is Element of g
x . x is set
x is Element of f
f is Element of f
the Element of Y /\ (dom x) is Element of Y /\ (dom x)
x is Element of g
x . x is set
x . the Element of Y /\ (dom x) is set
x /. the Element of Y /\ (dom x) is Element of f
Y is set
f is non empty set
g is non empty set
K20(g,f) is set
K19(K20(g,f)) is set
x is Element of f
f is Relation-like g -defined f -valued Function-like Element of K19(K20(g,f))
f .: Y is Element of K19(f)
K19(f) is set
dom f is Element of K19(g)
K19(g) is set
x is set
f . x is set
x is Element of g
f . x is set
Y is non empty set
f is non empty set
K20(Y,f) is set
K19(K20(Y,f)) is set
g is Element of Y
x is Element of f
f is Relation-like Y -defined f -valued Function-like Element of K19(K20(Y,f))
rng f is Element of K19(f)
K19(f) is set
f " is Relation-like Function-like set
(f ") . x is set
dom f is Element of K19(Y)
K19(Y) is set
f . g is set
Y is set
f is Relation-like Y -valued Function-like set
g is Relation-like Y -valued Function-like set
dom f is set
dom g is set
x is set
f /. x is Element of Y
g /. x is Element of Y
f . x is set
g . x is set