:: 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)
K6(X) is set
x is set
(f ^) . x is complex real ext-real Element of REAL
dom f is Element of K6(X)
f " {0} is Element of K6(X)
(dom f) \ (f " {0}) 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 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)
K6(X) is set
x is set
(f ^) . x is complex real ext-real Element of REAL
dom f is Element of K6(X)
f " {0} is Element of K6(X)
(dom f) \ (f " {0}) 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 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 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 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)
K6(X) is set
x is set
(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 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 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 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)
K6(X) is set
x is set
(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 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 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 complex-valued ext-real-valued real-valued Element of K6(K7(X,REAL))
rng (f ^) is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (f ^) is Element of K6(X)
K6(X) is set
R is set
(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 Relation-like Function-like complex-valued ext-real-valued real-valued set
dom X is set
f is Relation-like Function-like set
dom f is set
f is Relation-like Function-like set
dom f is set
g is Relation-like Function-like set
dom g is set
R is set
f . R is set
X . R is complex real ext-real Element of REAL
sqrt (X . R) is complex real ext-real Element of REAL
g . R is set
X is Relation-like Function-like complex-valued ext-real-valued real-valued set
(X) is Relation-like Function-like set
f is set
dom (X) is set
(X) . f is set
X . f is complex real ext-real Element of REAL
sqrt (X . f) is complex real ext-real Element of REAL
X is set
f is 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 Relation-like X -defined f -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(X,f))
(g) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K7(X,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(X,REAL)) is set
dom (g) is set
dom g is Element of K6(X)
K6(X) is set
rng (g) is complex-membered ext-real-membered real-membered 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))
(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 (X,REAL,f) is complex-membered ext-real-membered real-membered set
rng (X,REAL,f) is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (X,REAL,f) is Element of K6(X)
K6(X) is set
x is set
(X,REAL,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
sqrt 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))
(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 (X,REAL,f) is complex-membered ext-real-membered real-membered set
rng (X,REAL,f) is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (X,REAL,f) is Element of K6(X)
K6(X) is set
x is set
(X,REAL,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
sqrt 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 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 Function-like complex-valued ext-real-valued real-valued set
(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))
dom (X,REAL,f) is Element of K6(X)
K6(X) is set
dom f 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 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 Function-like 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
dom f is Element of K6(X)
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))
g is non empty 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 / g is Relation-like Function-like 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))
dom (f / g) is Element of K6(X)
K6(X) is set
dom f is Element of K6(X)
dom g is Element of K6(X)
(dom f) /\ (dom g) is Element of K6(X)
X /\ (dom g) is Element of K6(X)
X /\ X is set