:: PARTFUN3 semantic presentation

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

{{},1} is non empty set
ExtREAL is non empty ext-real-membered set

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

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

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

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

X " 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

K6(K7(X,{f})) is 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

K6(K7(X,{f})) is 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

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

K6({f}) is set
X is set

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

K6({f}) is set
X is non empty set

K6(K7(X,REAL)) is set

rng X is set

rng X is set

X is set

K6(K7(X,REAL)) is set
- 1 is non empty complex real ext-real non positive negative Element of REAL

K6(K7(0,REAL)) is set

dom (X ^) is set
dom X is set

(dom X) \ (X " ) is Element of K6((dom X))
K6((dom X)) is set
X is non empty set

K6(K7(X,REAL)) is set

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

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

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

K6(K7(X,REAL)) is set

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)

X is set

K6(K7(X,REAL)) is set

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)

X is set

K6(K7(X,REAL)) is set

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)

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

K6(K7(X,REAL)) is set

X is set

K6(K7(X,REAL)) is set

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)

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

K6(K7(X,REAL)) is set

X is set

K6(K7(X,REAL)) is set

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

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)

X is set

K6(K7(X,REAL)) is set

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)

X is set

K6(K7(X,REAL)) is set

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)

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

K6(K7(X,REAL)) is set

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)

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

K6(K7(X,REAL)) is set

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)

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

K6(K7(X,REAL)) is set

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)

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

K6(K7(X,REAL)) is set

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)

X is set

K6(K7(X,REAL)) is set

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)

X is set

K6(K7(X,REAL)) is set

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)

X is set

K6(K7(X,REAL)) is set

X is set

K6(K7(X,REAL)) is set

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)

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

K6(K7(X,REAL)) is set

X is set

K6(K7(X,REAL)) is set

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)

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

K6(K7(X,REAL)) is set

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)

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

K6(K7(X,REAL)) is set

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)

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

K6(K7(X,REAL)) is set

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) * (f . x) is complex real ext-real non negative Element of REAL
X is set

K6(K7(X,REAL)) is set

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)

X is set

K6(K7(X,REAL)) is set

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)

X is set

K6(K7(X,REAL)) is set

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)

X is set

K6(K7(X,REAL)) is set

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)

X is set

K6(K7(X,REAL)) is set

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

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)

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

K6(K7(X,REAL)) is set

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

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)

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

K6(K7(X,REAL)) is set

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

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)

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

K6(K7(X,REAL)) is set

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

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)

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

K6(K7(X,REAL)) is set

f is non empty complex real ext-real set

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)

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

K6(K7(X,REAL)) is set

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 " is Element of K6(X)
(dom g) \ (g " ) is Element of K6(X)
(dom f) /\ ((dom g) \ (g " )) is Element of K6(X)

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

K6(K7(X,REAL)) is set

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 " is Element of K6(X)
(dom g) \ (g " ) is Element of K6(X)
(dom f) /\ ((dom g) \ (g " )) is Element of K6(X)

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

K6(K7(X,REAL)) is set

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 " is Element of K6(X)
(dom g) \ (g " ) is Element of K6(X)
(dom f) /\ ((dom g) \ (g " )) is Element of K6(X)

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

K6(K7(X,REAL)) is set

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 " is Element of K6(X)
(dom g) \ (g " ) is Element of K6(X)
(dom f) /\ ((dom g) \ (g " )) is Element of K6(X)

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

K6(K7(X,REAL)) is set

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 g) \ (g " ) is Element of K6(X)
(dom f) /\ ((dom g) \ (g " )) is Element of K6(X)

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

K6(K7(X,REAL)) is set

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 g) \ (g " ) is Element of K6(X)
(dom f) /\ ((dom g) \ (g " )) is Element of K6(X)

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

K6(K7(X,REAL)) is set

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 g) \ (g " ) is Element of K6(X)
(dom f) /\ ((dom g) \ (g " )) is Element of K6(X)

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

K6(K7(X,REAL)) is set

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 g) \ (g " ) is Element of K6(X)
(dom f) /\ ((dom g) \ (g " )) is Element of K6(X)

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

K6(K7(X,REAL)) is set

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 non empty set

K6(K7(X,REAL)) is set

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 g) \ (g " ) is Element of K6(X)
(dom f) /\ ((dom g) \ (g " )) is Element of K6(X)

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

K6(K7(X,REAL)) is set

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)

X is set

K6(K7(X,REAL)) is set

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)

X is set

K6(K7(X,REAL)) is set

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)

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

K6(K7(X,REAL)) is set

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)

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

K6(K7(X,REAL)) is set

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)

x is non empty complex real ext-real set
x " is non empty complex real ext-real set
X is set

K6(K7(X,REAL)) is set

X is set

K6(K7(X,REAL)) is set

X is set

K6(K7(X,REAL)) is set

X is set

K6(K7(X,REAL)) is set

X is set

K6(K7(X,REAL)) is set

X is set

K6(K7(X,REAL)) is set

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

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

K6(K7(X,REAL)) is set

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)

a is non empty complex real ext-real set

X is non empty set

K6(K7(X,REAL)) is set

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