:: PARTFUN3 semantic presentation

REAL is non empty complex-membered ext-real-membered real-membered V52() V53() V58() set

NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V58() Element of K6(REAL)

K6(REAL) is set

COMPLEX is non empty complex-membered V52() V53() set

{} is empty Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() set

1 is non empty natural complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V63() V64() Element of NAT

{{},1} is non empty set

ExtREAL is non empty ext-real-membered set

RAT is non empty complex-membered ext-real-membered real-membered rational-membered V52() V53() set

INT is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered V52() V53() set

0 is empty natural complex real ext-real non positive non negative Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V63() V64() Element of NAT

{0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

X is complex real ext-real set

X / X is complex real ext-real set

X is complex real ext-real set

X * X is complex real ext-real set

X " is complex real ext-real set

X * (X ") is complex real ext-real set

X / X is complex real ext-real non negative set

X is complex real ext-real non negative set

sqrt X is complex real ext-real set

X is non empty complex real ext-real positive non negative set

sqrt X is complex real ext-real non negative set

X is Relation-like Function-like set

X " is Relation-like Function-like set

dom (X ") is set

f is set

(X ") .: f is set

X .: ((X ") .: f) is set

(X ") " is Relation-like Function-like set

((X ") ") .: ((X ") .: f) is set

X is Relation-like non-empty Function-like set

X " {0} is set

f is set

dom X is set

X . f is set

rng X is V58() set

X is set

f is non empty complex real ext-real positive non negative set

X --> f is Relation-like non-empty X -defined {f} -valued Function-like constant total V33(X,{f}) complex-valued ext-real-valued real-valued Element of K6(K7(X,{f}))

{f} is non empty complex-membered ext-real-membered real-membered set

K7(X,{f}) is complex-valued ext-real-valued real-valued set

K6(K7(X,{f})) is set

g is complex real ext-real set

rng (X --> f) is V2() complex-membered ext-real-membered real-membered V58() set

rng (X --> f) is V2() complex-membered ext-real-membered real-membered V58() Element of K6({f})

K6({f}) is set

X is set

f is non empty complex real ext-real non positive negative set

X --> f is Relation-like non-empty X -defined {f} -valued Function-like constant total V33(X,{f}) complex-valued ext-real-valued real-valued Element of K6(K7(X,{f}))

{f} is non empty complex-membered ext-real-membered real-membered set

K7(X,{f}) is complex-valued ext-real-valued real-valued set

K6(K7(X,{f})) is set

g is complex real ext-real set

rng (X --> f) is V2() complex-membered ext-real-membered real-membered V58() set

rng (X --> f) is V2() complex-membered ext-real-membered real-membered V58() Element of K6({f})

K6({f}) is set

X is set

f is complex real ext-real non positive set

X --> f is Relation-like X -defined {f} -valued Function-like constant total V33(X,{f}) complex-valued ext-real-valued real-valued Element of K6(K7(X,{f}))

{f} is non empty complex-membered ext-real-membered real-membered set

K7(X,{f}) is complex-valued ext-real-valued real-valued set

K6(K7(X,{f})) is set

g is complex real ext-real set

rng (X --> f) is V2() complex-membered ext-real-membered real-membered set

rng (X --> f) is V2() complex-membered ext-real-membered real-membered Element of K6({f})

K6({f}) is set

X is set

f is complex real ext-real non negative set

X --> f is Relation-like X -defined {f} -valued Function-like constant total V33(X,{f}) complex-valued ext-real-valued real-valued Element of K6(K7(X,{f}))

{f} is non empty complex-membered ext-real-membered real-membered set

K7(X,{f}) is complex-valued ext-real-valued real-valued set

K6(K7(X,{f})) is set

g is complex real ext-real set

rng (X --> f) is V2() complex-membered ext-real-membered real-membered set

rng (X --> f) is V2() complex-membered ext-real-membered real-membered Element of K6({f})

K6({f}) is set

X is non empty set

X --> 0 is non empty Relation-like X -defined REAL -valued RAT -valued INT -valued Function-like constant total V33(X, REAL ) complex-valued ext-real-valued real-valued natural-valued () () Element of K6(K7(X,REAL))

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

rng (X --> 0) is V2() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(REAL)

X is Relation-like set

rng X is set

f is complex real ext-real set

X is Relation-like set

rng X is set

f is complex real ext-real set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

- 1 is non empty complex real ext-real non positive negative Element of REAL

X --> (- 1) is Relation-like non-empty X -defined REAL -valued Function-like constant total V33(X, REAL ) complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

X --> 1 is Relation-like non-empty X -defined REAL -valued RAT -valued INT -valued Function-like constant total V33(X, REAL ) complex-valued ext-real-valued real-valued natural-valued () () Element of K6(K7(X,REAL))

K7(0,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(0,REAL)) is set

the empty Relation-like non-empty 0 -defined REAL -valued Function-like one-to-one constant functional total V33( 0 , REAL ) complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() Function-yielding V76() Element of K6(K7(0,REAL)) is empty Relation-like non-empty 0 -defined REAL -valued Function-like one-to-one constant functional total V33( 0 , REAL ) complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() Function-yielding V76() Element of K6(K7(0,REAL))

X is Relation-like non-empty Function-like complex-valued ext-real-valued real-valued set

X ^ is Relation-like Function-like set

dom (X ^) is set

dom X is set

X " {0} is empty Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() set

(dom X) \ (X " {0}) is Element of K6((dom X))

K6((dom X)) is set

X is non empty set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

dom f is Element of K6(X)

K6(X) is set

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

f / g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

dom (f / g) is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

g " {0} is empty Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() Element of K6(X)

(dom g) \ (g " {0}) is Element of K6(X)

(dom f) /\ ((dom g) \ (g " {0})) is Element of K6(X)

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f + g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f + g) is complex-membered ext-real-membered real-membered set

rng (f + g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f + g) is Element of K6(X)

K6(X) is set

a is set

(f + g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non positive set

b is complex real ext-real non positive set

b + b is complex real ext-real non positive set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f + g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f + g) is complex-membered ext-real-membered real-membered set

rng (f + g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f + g) is Element of K6(X)

K6(X) is set

a is set

(f + g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non negative set

b is complex real ext-real non negative set

b + b is complex real ext-real non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f + g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f + g) is complex-membered ext-real-membered real-membered set

rng (f + g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f + g) is Element of K6(X)

K6(X) is set

a is set

(f + g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is non empty complex real ext-real positive non negative set

b is complex real ext-real non negative set

b + b is non empty complex real ext-real positive non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f + g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f + g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f + g) is complex-membered ext-real-membered real-membered set

rng (f + g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f + g) is Element of K6(X)

K6(X) is set

a is set

(f + g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is complex real ext-real non positive set

b is non empty complex real ext-real non positive negative set

b + b is non empty complex real ext-real non positive negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f + g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f - g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

- g is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

- 1 is non empty complex real ext-real non positive negative set

(- 1) (#) g is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

f + (- g) is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

R is complex real ext-real set

rng (f - g) is complex-membered ext-real-membered real-membered set

rng (f - g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f - g) is Element of K6(X)

K6(X) is set

a is set

(f - g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non negative set

b is complex real ext-real non positive set

b - b is complex real ext-real non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f - g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

- g is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) g is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

f + (- g) is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

R is complex real ext-real set

rng (f - g) is complex-membered ext-real-membered real-membered set

rng (f - g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f - g) is Element of K6(X)

K6(X) is set

a is set

(f - g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non positive set

b is complex real ext-real non negative set

b - b is complex real ext-real non positive set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f - g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

- g is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) g is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

f + (- g) is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

R is complex real ext-real set

rng (f - g) is complex-membered ext-real-membered real-membered set

rng (f - g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f - g) is Element of K6(X)

K6(X) is set

a is set

(f - g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is non empty complex real ext-real positive non negative set

b is complex real ext-real non positive set

b - b is non empty complex real ext-real positive non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f - g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

- g is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) g is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

f + (- g) is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

R is complex real ext-real set

rng (f - g) is complex-membered ext-real-membered real-membered set

rng (f - g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f - g) is Element of K6(X)

K6(X) is set

a is set

(f - g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is complex real ext-real non positive set

b is non empty complex real ext-real positive non negative set

b - b is non empty complex real ext-real non positive negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f - g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

- g is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) g is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

f + (- g) is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

R is complex real ext-real set

rng (f - g) is complex-membered ext-real-membered real-membered set

rng (f - g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f - g) is Element of K6(X)

K6(X) is set

a is set

(f - g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is non empty complex real ext-real non positive negative set

b is complex real ext-real non negative set

b - b is non empty complex real ext-real non positive negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f - g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

- g is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) g is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

f + (- g) is Relation-like X -defined Function-like complex-valued ext-real-valued real-valued set

R is complex real ext-real set

rng (f - g) is complex-membered ext-real-membered real-membered set

rng (f - g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f - g) is Element of K6(X)

K6(X) is set

a is set

(f - g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is complex real ext-real non negative set

b is non empty complex real ext-real non positive negative set

b - b is non empty complex real ext-real positive non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non positive set

b is complex real ext-real non positive set

b * b is complex real ext-real non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non negative set

b is complex real ext-real non negative set

b * b is complex real ext-real non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non positive set

b is complex real ext-real non negative set

b * b is complex real ext-real non positive set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is non empty complex real ext-real positive non negative set

b is non empty complex real ext-real non positive negative set

b * b is non empty complex real ext-real non positive negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f (#) g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is non empty complex real ext-real positive non negative set

b is non empty complex real ext-real positive non negative set

b * b is non empty complex real ext-real positive non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is non empty complex real ext-real non positive negative set

b is non empty complex real ext-real non positive negative set

b * b is non empty complex real ext-real positive non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

x is set

(f (#) g) . x is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

(dom f) /\ (dom g) is Element of K6(X)

g . x is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

f . x is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

a is non empty complex real ext-real set

b is non empty complex real ext-real set

a * b is non empty complex real ext-real set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

f (#) f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

g is complex real ext-real set

rng (f (#) f) is complex-membered ext-real-membered real-membered set

rng (f (#) f) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) f) is Element of K6(X)

K6(X) is set

x is set

(f (#) f) . x is complex real ext-real Element of REAL

f . x is complex real ext-real Element of REAL

(f . x) * (f . x) is complex real ext-real non negative Element of REAL

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f is complex real ext-real non positive set

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom g is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non positive set

f * b is complex real ext-real non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f is complex real ext-real non negative set

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom g is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non negative set

f * b is complex real ext-real non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f is complex real ext-real non positive set

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom g is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non negative set

f * b is complex real ext-real non positive set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f is complex real ext-real non negative set

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom g is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non positive set

f * b is complex real ext-real non positive set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f is non empty complex real ext-real positive non negative set

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom g is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is non empty complex real ext-real non positive negative set

f * b is non empty complex real ext-real non positive negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f is non empty complex real ext-real non positive negative set

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom g is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is non empty complex real ext-real positive non negative set

f * b is non empty complex real ext-real non positive negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f is non empty complex real ext-real positive non negative set

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom g is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is non empty complex real ext-real positive non negative set

f * b is non empty complex real ext-real positive non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f is non empty complex real ext-real non positive negative set

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f (#) g) is complex-membered ext-real-membered real-membered set

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

a is set

(f (#) g) . a is complex real ext-real Element of REAL

dom g is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is non empty complex real ext-real non positive negative set

f * b is non empty complex real ext-real positive non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

f is non empty complex real ext-real set

f (#) g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

rng (f (#) g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f (#) g) is Element of K6(X)

K6(X) is set

x is set

(f (#) g) . x is complex real ext-real Element of REAL

dom g is Element of K6(X)

g . x is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

a is non empty complex real ext-real set

f * a is non empty complex real ext-real set

X is non empty set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f / g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f / g) is complex-membered ext-real-membered real-membered set

rng (f / g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f / g) is Element of K6(X)

K6(X) is set

a is set

(f / g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

g " {0} is Element of K6(X)

(dom g) \ (g " {0}) is Element of K6(X)

(dom f) /\ ((dom g) \ (g " {0})) is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non positive set

b is complex real ext-real non positive set

b " is complex real ext-real non positive set

b * (b ") is complex real ext-real non negative set

X is non empty set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f / g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f / g) is complex-membered ext-real-membered real-membered set

rng (f / g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f / g) is Element of K6(X)

K6(X) is set

a is set

(f / g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

g " {0} is Element of K6(X)

(dom g) \ (g " {0}) is Element of K6(X)

(dom f) /\ ((dom g) \ (g " {0})) is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non negative set

b is complex real ext-real non negative set

b " is complex real ext-real non negative set

b * (b ") is complex real ext-real non negative set

X is non empty set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f / g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f / g) is complex-membered ext-real-membered real-membered set

rng (f / g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f / g) is Element of K6(X)

K6(X) is set

a is set

(f / g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

g " {0} is Element of K6(X)

(dom g) \ (g " {0}) is Element of K6(X)

(dom f) /\ ((dom g) \ (g " {0})) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non positive set

b is complex real ext-real non negative set

b " is complex real ext-real non negative set

b * (b ") is complex real ext-real non positive set

X is non empty set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f / g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f / g) is complex-membered ext-real-membered real-membered set

rng (f / g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f / g) is Element of K6(X)

K6(X) is set

a is set

(f / g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

g " {0} is Element of K6(X)

(dom g) \ (g " {0}) is Element of K6(X)

(dom f) /\ ((dom g) \ (g " {0})) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered Element of K6(REAL)

b is complex real ext-real non negative set

b is complex real ext-real non positive set

b " is complex real ext-real non positive set

b * (b ") is complex real ext-real non positive set

X is non empty set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f / g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f / g) is complex-membered ext-real-membered real-membered set

rng (f / g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f / g) is Element of K6(X)

K6(X) is set

a is set

(f / g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

g " {0} is empty Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() Element of K6(X)

(dom g) \ (g " {0}) is Element of K6(X)

(dom f) /\ ((dom g) \ (g " {0})) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is non empty complex real ext-real positive non negative set

b is non empty complex real ext-real non positive negative set

b " is non empty complex real ext-real non positive negative set

b * (b ") is non empty complex real ext-real non positive negative set

X is non empty set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f / g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f / g) is complex-membered ext-real-membered real-membered set

rng (f / g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f / g) is Element of K6(X)

K6(X) is set

a is set

(f / g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

g " {0} is empty Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() Element of K6(X)

(dom g) \ (g " {0}) is Element of K6(X)

(dom f) /\ ((dom g) \ (g " {0})) is Element of K6(X)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is non empty complex real ext-real non positive negative set

b is non empty complex real ext-real positive non negative set

b " is non empty complex real ext-real positive non negative set

b * (b ") is non empty complex real ext-real non positive negative set

X is non empty set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f / g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f / g) is complex-membered ext-real-membered real-membered set

rng (f / g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f / g) is Element of K6(X)

K6(X) is set

a is set

(f / g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

g " {0} is empty Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() Element of K6(X)

(dom g) \ (g " {0}) is Element of K6(X)

(dom f) /\ ((dom g) \ (g " {0})) is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is non empty complex real ext-real positive non negative set

b is non empty complex real ext-real positive non negative set

b " is non empty complex real ext-real positive non negative set

b * (b ") is non empty complex real ext-real positive non negative set

X is non empty set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

f / g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

R is complex real ext-real set

rng (f / g) is complex-membered ext-real-membered real-membered set

rng (f / g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f / g) is Element of K6(X)

K6(X) is set

a is set

(f / g) . a is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

g " {0} is empty Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() Element of K6(X)

(dom g) \ (g " {0}) is Element of K6(X)

(dom f) /\ ((dom g) \ (g " {0})) is Element of K6(X)

g . a is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

f . a is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

b is non empty complex real ext-real non positive negative set

b is non empty complex real ext-real non positive negative set

b " is non empty complex real ext-real non positive negative set

b * (b ") is non empty complex real ext-real positive non negative set

X is non empty set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

f / f is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

g is complex real ext-real set

rng (f / f) is complex-membered ext-real-membered real-membered set

rng (f / f) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f / f) is Element of K6(X)

K6(X) is set

x is set

(f / f) . x is complex real ext-real Element of REAL

f . x is complex real ext-real Element of REAL

(f . x) " is complex real ext-real Element of REAL

(f . x) * ((f . x) ") is complex real ext-real non negative Element of REAL

X is non empty set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

g is Relation-like non-empty X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

f / g is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

rng (f / g) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f / g) is Element of K6(X)

K6(X) is set

x is set

(f / g) . x is complex real ext-real Element of REAL

dom f is Element of K6(X)

dom g is Element of K6(X)

g " {0} is empty Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() Element of K6(X)

(dom g) \ (g " {0}) is Element of K6(X)

(dom f) /\ ((dom g) \ (g " {0})) is Element of K6(X)

g . x is complex real ext-real Element of REAL

rng g is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

f . x is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

a is non empty complex real ext-real set

b is non empty complex real ext-real set

b " is non empty complex real ext-real set

a * (b ") is non empty complex real ext-real set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

Inv f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

g is complex real ext-real set

rng (Inv f) is complex-membered ext-real-membered real-membered set

rng (Inv f) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (Inv f) is Element of K6(X)

K6(X) is set

x is set

(Inv f) . x is complex real ext-real Element of REAL

dom f is Element of K6(X)

f . x is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

a is complex real ext-real non positive set

a " is complex real ext-real non positive set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

Inv f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

g is complex real ext-real set

rng (Inv f) is complex-membered ext-real-membered real-membered set

rng (Inv f) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (Inv f) is Element of K6(X)

K6(X) is set

x is set

(Inv f) . x is complex real ext-real Element of REAL

dom f is Element of K6(X)

f . x is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered Element of K6(REAL)

a is complex real ext-real non negative set

a " is complex real ext-real non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

Inv f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is complex real ext-real set

rng (Inv f) is complex-membered ext-real-membered real-membered set

rng (Inv f) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (Inv f) is Element of K6(X)

K6(X) is set

x is set

(Inv f) . x is complex real ext-real Element of REAL

dom f is Element of K6(X)

f . x is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

a is non empty complex real ext-real positive non negative set

a " is non empty complex real ext-real positive non negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

Inv f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is complex real ext-real set

rng (Inv f) is complex-membered ext-real-membered real-membered set

rng (Inv f) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (Inv f) is Element of K6(X)

K6(X) is set

x is set

(Inv f) . x is complex real ext-real Element of REAL

dom f is Element of K6(X)

f . x is complex real ext-real Element of REAL

rng f is complex-membered ext-real-membered real-membered V58() Element of K6(REAL)

a is non empty complex real ext-real non positive negative set

a " is non empty complex real ext-real non positive negative set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

Inv f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

rng (Inv f) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (Inv f) is Element of K6(X)

K6(X) is set

R is set

(Inv f) . R is complex real ext-real Element of REAL

dom f is Element of K6(X)

f . R is complex real ext-real Element of REAL

x is non empty complex real ext-real set

x " is non empty complex real ext-real set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

- f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

(- 1) (#) f is Relation-like non-empty X -defined Function-like total complex-valued ext-real-valued real-valued set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

- f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

(- 1) (#) f is Relation-like X -defined Function-like total complex-valued ext-real-valued real-valued () set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

- f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

(- 1) (#) f is Relation-like X -defined Function-like total complex-valued ext-real-valued real-valued () set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

- f is Relation-like non-empty X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

(- 1) (#) f is Relation-like non-empty X -defined Function-like total complex-valued ext-real-valued real-valued () () set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () () Element of K6(K7(X,REAL))

- f is Relation-like non-empty X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

(- 1) (#) f is Relation-like non-empty X -defined Function-like total complex-valued ext-real-valued real-valued () () set

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

abs f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

g is complex real ext-real set

rng (abs f) is complex-membered ext-real-membered real-membered set

rng (abs f) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (abs f) is Element of K6(X)

K6(X) is set

x is set

(abs f) . x is complex real ext-real Element of REAL

f . x is complex real ext-real Element of REAL

abs (f . x) is complex real ext-real Element of REAL

X is set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is Relation-like non-empty X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

abs f is Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

g is complex real ext-real set

rng (abs f) is complex-membered ext-real-membered real-membered set

rng (abs f) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (abs f) is Element of K6(X)

K6(X) is set

x is set

(abs f) . x is complex real ext-real Element of REAL

dom f is Element of K6(X)

f . x is complex real ext-real Element of REAL

a is non empty complex real ext-real set

abs a is complex real ext-real Element of REAL

X is non empty set

K7(X,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(X,REAL)) is set

f is non empty Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued () Element of K6(K7(X,REAL))

f ^ is Relation-like X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))

g is complex real ext-real set

rng (f ^) is complex-membered ext-real-membered real-membered set

rng (f ^) is complex-membered ext-real-membered real-membered Element of K6(REAL)

dom (f ^) is Element of K6(X)