:: PARTFUN2 semantic presentation

{} 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)
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
c8 is Element of g
x /. c8 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
c8 is Element of g
x /. c8 is Element of Y
c8 is Element of g
x /. c8 is Element of Y
x is set
c8 is Element of g
x /. c8 is Element of f
x /. c8 is Element of Y
f /. (x /. c8) is Element of f
x . c8 is set
x . x is set
f . (x /. c8) 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)

K20(Y,Y) is set
K19(K20(Y,Y)) is set

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

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

(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

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

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

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
c8 is Element of Y
g /. c8 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
c8 is Element of Y
g /. c8 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))

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
c8 is non empty set
K20(x,c8) is set
K19(K20(x,c8)) 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 c8 -valued Function-like Element of K19(K20(x,c8))
dom c is Element of K19(x)
K19(x) is set
c /. d2 is Element of c8
x is set
(x,c8,x,c) is Relation-like x -defined c8 -valued Function-like Element of K19(K20(x,c8))
dom (x,c8,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
c8 is Element of g
f /. c8 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
c8 is Element of g
f /. c8 is Element of f
f . c8 is set
x is set
f . x is set
c8 is Element of g
f /. c8 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
c8 is non empty set
x is non empty set
K20(x,c8) is set
K19(K20(x,c8)) 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
c11 is Element of x
c is Relation-like x -defined c8 -valued Function-like Element of K19(K20(x,c8))
dom c is Element of K19(x)
K19(x) is set
x is set
d2 is Element of c8
c /. c11 is Element of c8
c .: x is Element of K19(c8)
K19(c8) 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
F1() is non empty set
F2() is non empty set
K20(F1(),F2()) is set
K19(K20(F1(),F2())) is set
the Element of F2() is Element of F2()
f is set
g is set
K19(F1()) is set
x is Element of F1()
f is Element of F2()
x is Element of F2()
x is Element of F2()
x is Relation-like F1() -defined F2() -valued Function-like V18(F1(),F2()) Element of K19(K20(F1(),F2()))
g is Element of K19(F1())
x | g is Relation-like F1() -defined F2() -valued Function-like Element of K19(K20(F1(),F2()))
f is Relation-like F1() -defined F2() -valued Function-like Element of K19(K20(F1(),F2()))
dom f is Element of K19(F1())
dom x is Element of K19(F1())
x is Element of F1()
x is Element of F2()
(dom x) /\ g is Element of K19(F1())
x is Element of F1()
f /. x is Element of F2()
x . x is Element of F2()
x is Element of F2()
f . x is set
F2() is non empty set
F1() is non empty set
K20(F1(),F2()) is set
K19(K20(F1(),F2())) is set
Y is Relation-like F1() -defined F2() -valued Function-like Element of K19(K20(F1(),F2()))
dom Y is Element of K19(F1())
K19(F1()) is set
f is Element of F1()
F3(f) is Element of F2()
g is Element of F2()
F3(f) is Element of F2()
g is Element of F2()
f is Element of F1()
Y /. f is Element of F2()
F3(f) is Element of F2()
F2() is non empty set
F1() is non empty set
K20(F1(),F2()) is set
K19(K20(F1(),F2())) is set
F3() is set
Y is Relation-like F1() -defined F2() -valued Function-like Element of K19(K20(F1(),F2()))
dom Y is Element of K19(F1())
K19(F1()) is set
f is Relation-like F1() -defined F2() -valued Function-like Element of K19(K20(F1(),F2()))
dom f is Element of K19(F1())
g is Element of F1()
Y /. g is Element of F2()
F4(g) is Element of F2()
f /. g is Element of F2()
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
c8 is Element of f
x /. c8 is Element of g
(x | Y) /. c8 is Element of g
the Element of Y /\ (dom x) is Element of Y /\ (dom x)
c8 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
c8 is Element of f
x /. c8 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)
c8 is Element of g
f /\ (dom f) is Element of K19(g)
d2 is Element of x
f /. c8 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 ") . x is set
dom f is Element of K19(Y)
K19(Y) is set
f . g is set
Y is 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