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

x /. c

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

x /. c

c

x /. c

x is set

c

x /. c

x /. c

f /. (x /. c

x . c

x . x is set

f . (x /. c

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

g /. c

x is Element of f

x /. x is Element of Y

x is Element of f

x /. x is Element of Y

c

g /. c

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

K20(x,c

K19(K20(x,c

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

dom c is Element of K19(x)

K19(x) is set

c /. d2 is Element of c

x is set

(x,c

dom (x,c

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

f /. c

x is Element of g

f /. x is Element of f

f . x is set

x is set

x is Element of f

c

f /. c

f . c

x is set

f . x is set

c

f /. c

g is non empty set

f is non empty set

K20(f,g) is set

K19(K20(f,g)) is set

c

x is non empty set

K20(x,c

K19(K20(x,c

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

c is Relation-like x -defined c

dom c is Element of K19(x)

K19(x) is set

x is set

d2 is Element of c

c /. c

c .: x is Element of K19(c

K19(c

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

F

K20(F

K19(K20(F

the Element of F

f is set

g is set

K19(F

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

g is Element of K19(F

x | g is Relation-like F

f is Relation-like 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

F

K20(F

K19(K20(F

Y is Relation-like F

dom Y is Element of K19(F

K19(F

f is Element of F

F

g is Element of F

F

g is Element of F

f is Element of F

Y /. f is Element of F

F

F

F

K20(F

K19(K20(F

F

Y is Relation-like F

dom Y is Element of K19(F

K19(F

f is Relation-like F

dom f is Element of K19(F

g is Element of F

Y /. g is Element of F

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

x /. c

(x | Y) /. c

the Element of Y /\ (dom x) is Element of Y /\ (dom x)

c

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

x /. c

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

f /\ (dom f) is Element of K19(g)

d2 is Element of x

f /. c

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