:: MESFUN6C semantic presentation

REAL is non empty V45() V50() V51() V52() V56() set

NAT is V50() V51() V52() V53() V54() V55() V56() Element of K6(REAL)

K6(REAL) is non empty set

ExtREAL is non empty V51() set

K7(NAT,ExtREAL) is Relation-like V34() set

K6(K7(NAT,ExtREAL)) is non empty set

K6(ExtREAL) is non empty set

K7(NAT,REAL) is Relation-like V33() V34() V35() set

K6(K7(NAT,REAL)) is non empty set

COMPLEX is non empty V45() V50() V56() set

RAT is non empty V45() V50() V51() V52() V53() V56() set

INT is non empty V45() V50() V51() V52() V53() V54() V56() set

omega is V50() V51() V52() V53() V54() V55() V56() set

K6(omega) is non empty set

K6(NAT) is non empty set

K6(K6(REAL)) is non empty set

K6(RAT) is non empty set

{} is empty Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() V50() V51() V52() V53() V54() V55() V56() set

1 is non empty natural complex real ext-real positive non negative V43() V44() V50() V51() V52() V53() V54() V55() Element of NAT

{{},1} is non empty set

K7(COMPLEX,COMPLEX) is non empty Relation-like V33() set

K6(K7(COMPLEX,COMPLEX)) is non empty set

K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty Relation-like V33() set

K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty set

K7(REAL,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(REAL,REAL)) is non empty set

K7(K7(REAL,REAL),REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(K7(REAL,REAL),REAL)) is non empty set

K7(RAT,RAT) is non empty Relation-like RAT -valued V33() V34() V35() set

K6(K7(RAT,RAT)) is non empty set

K7(K7(RAT,RAT),RAT) is non empty Relation-like RAT -valued V33() V34() V35() set

K6(K7(K7(RAT,RAT),RAT)) is non empty set

K7(INT,INT) is non empty Relation-like RAT -valued INT -valued V33() V34() V35() set

K6(K7(INT,INT)) is non empty set

K7(K7(INT,INT),INT) is non empty Relation-like RAT -valued INT -valued V33() V34() V35() set

K6(K7(K7(INT,INT),INT)) is non empty set

K7(NAT,NAT) is Relation-like RAT -valued INT -valued V33() V34() V35() V36() set

K7(K7(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V33() V34() V35() V36() set

K6(K7(K7(NAT,NAT),NAT)) is non empty set

K7(NAT,COMPLEX) is Relation-like V33() set

K6(K7(NAT,COMPLEX)) is non empty set

0. is empty Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() V50() V51() V52() V53() V54() V55() V56() Element of ExtREAL

0 is empty natural complex real Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V33() V34() V35() V36() V43() V44() V50() V51() V52() V53() V54() V55() V56() Element of NAT

2 is non empty natural complex real ext-real positive non negative V43() V44() V50() V51() V52() V53() V54() V55() Element of NAT

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

K478() is non empty non real ext-real positive non negative Element of ExtREAL

+infty is non empty non real ext-real positive non negative set

-infty is non empty non real ext-real non positive negative set

K479() is non empty non real ext-real non positive negative Element of ExtREAL

K7(2,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(2,REAL)) is non empty set

Re 0 is complex real ext-real Element of REAL

Im 0 is complex real ext-real Element of REAL

<i> is complex Element of COMPLEX

Re <i> is complex real ext-real Element of REAL

Im <i> is complex real ext-real Element of REAL

|.0.| is complex real ext-real Element of REAL

(Re 0) ^2 is complex real ext-real Element of REAL

(Im 0) ^2 is complex real ext-real Element of REAL

((Re 0) ^2) + ((Im 0) ^2) is complex real ext-real Element of REAL

sqrt (((Re 0) ^2) + ((Im 0) ^2)) is complex real ext-real Element of REAL

sqrt 0 is complex real ext-real Element of REAL

X is complex real ext-real set

R_EAL X is ext-real Element of ExtREAL

S is complex real ext-real set

R_EAL S is ext-real Element of ExtREAL

(R_EAL X) + (R_EAL S) is ext-real Element of ExtREAL

X + S is complex real ext-real set

- (R_EAL X) is ext-real Element of ExtREAL

- X is complex real ext-real set

(R_EAL X) - (R_EAL S) is ext-real Element of ExtREAL

X - S is complex real ext-real set

- S is complex real ext-real set

X + (- S) is complex real ext-real set

(R_EAL X) * (R_EAL S) is ext-real Element of ExtREAL

X * S is complex real ext-real set

f is complex real ext-real Element of REAL

A is complex real ext-real Element of REAL

- A is complex real ext-real Element of REAL

R_EAL (- X) is ext-real Element of ExtREAL

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

X is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re S is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

Im S is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

A is complex real ext-real Element of REAL

A (#) (Re S) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

A (#) S is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re (A (#) S) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

A (#) (Im S) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Im (A (#) S) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom (A (#) (Re S)) is Element of K6(X)

K6(X) is non empty set

dom (Re S) is Element of K6(X)

Im A is complex real ext-real Element of REAL

dom S is Element of K6(X)

Re A is complex real ext-real Element of REAL

dom (A (#) S) is Element of K6(X)

dom (Re (A (#) S)) is Element of K6(X)

f is set

S . f is complex set

A * (S . f) is complex set

Re (A * (S . f)) is complex real ext-real Element of REAL

Re (S . f) is complex real ext-real Element of REAL

(Re A) * (Re (S . f)) is complex real ext-real Element of REAL

Im (S . f) is complex real ext-real Element of REAL

(Im A) * (Im (S . f)) is complex real ext-real Element of REAL

((Re A) * (Re (S . f))) - ((Im A) * (Im (S . f))) is complex real ext-real Element of REAL

- ((Im A) * (Im (S . f))) is complex real ext-real set

((Re A) * (Re (S . f))) + (- ((Im A) * (Im (S . f)))) is complex real ext-real set

(Re S) . f is complex real ext-real Element of REAL

(Re (A (#) S)) . f is complex real ext-real Element of REAL

(A (#) S) . f is complex set

Re ((A (#) S) . f) is complex real ext-real Element of REAL

A * (Re (S . f)) is complex real ext-real Element of REAL

(A (#) (Re S)) . f is complex real ext-real Element of REAL

dom (A (#) (Im S)) is Element of K6(X)

dom (Im S) is Element of K6(X)

dom (Im (A (#) S)) is Element of K6(X)

f is set

S . f is complex set

A * (S . f) is complex set

Im (A * (S . f)) is complex real ext-real Element of REAL

Re (S . f) is complex real ext-real Element of REAL

(Im A) * (Re (S . f)) is complex real ext-real Element of REAL

Im (S . f) is complex real ext-real Element of REAL

(Re A) * (Im (S . f)) is complex real ext-real Element of REAL

((Im A) * (Re (S . f))) + ((Re A) * (Im (S . f))) is complex real ext-real Element of REAL

(Im S) . f is complex real ext-real Element of REAL

(Im (A (#) S)) . f is complex real ext-real Element of REAL

(A (#) S) . f is complex set

Im ((A (#) S) . f) is complex real ext-real Element of REAL

A * (Im (S . f)) is complex real ext-real Element of REAL

(A (#) (Im S)) . f is complex real ext-real Element of REAL

X is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re S is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

Im S is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

A is complex set

A (#) S is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re (A (#) S) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Re A is complex real ext-real Element of REAL

(Re A) (#) (Re S) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Im A is complex real ext-real Element of REAL

(Im A) (#) (Im S) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

((Re A) (#) (Re S)) - ((Im A) (#) (Im S)) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

- ((Im A) (#) (Im S)) is Relation-like Function-like V33() set

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

(- 1) (#) ((Im A) (#) (Im S)) is Relation-like Function-like set

((Re A) (#) (Re S)) + (- ((Im A) (#) (Im S))) is Relation-like Function-like set

Im (A (#) S) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Im A) (#) (Re S) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Re A) (#) (Im S) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

((Im A) (#) (Re S)) + ((Re A) (#) (Im S)) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom ((Re A) (#) (Re S)) is Element of K6(X)

K6(X) is non empty set

dom (Re S) is Element of K6(X)

dom ((Im A) (#) (Im S)) is Element of K6(X)

dom (Im S) is Element of K6(X)

dom (A (#) S) is Element of K6(X)

dom S is Element of K6(X)

dom (Re (A (#) S)) is Element of K6(X)

dom (((Re A) (#) (Re S)) - ((Im A) (#) (Im S))) is Element of K6(X)

(dom ((Re A) (#) (Re S))) /\ (dom ((Im A) (#) (Im S))) is Element of K6(X)

f is set

S . f is complex set

A * (S . f) is complex set

Re (A * (S . f)) is complex real ext-real Element of REAL

Re (S . f) is complex real ext-real Element of REAL

(Re A) * (Re (S . f)) is complex real ext-real Element of REAL

Im (S . f) is complex real ext-real Element of REAL

(Im A) * (Im (S . f)) is complex real ext-real Element of REAL

((Re A) * (Re (S . f))) - ((Im A) * (Im (S . f))) is complex real ext-real Element of REAL

- ((Im A) * (Im (S . f))) is complex real ext-real set

((Re A) * (Re (S . f))) + (- ((Im A) * (Im (S . f)))) is complex real ext-real set

((Im A) (#) (Im S)) . f is complex real ext-real Element of REAL

(Im S) . f is complex real ext-real Element of REAL

(Im A) * ((Im S) . f) is complex real ext-real Element of REAL

(Re S) . f is complex real ext-real Element of REAL

(Re (A (#) S)) . f is complex real ext-real Element of REAL

(A (#) S) . f is complex set

Re ((A (#) S) . f) is complex real ext-real Element of REAL

((Re A) (#) (Re S)) . f is complex real ext-real Element of REAL

(Re A) * ((Re S) . f) is complex real ext-real Element of REAL

(((Re A) (#) (Re S)) - ((Im A) (#) (Im S))) . f is complex real ext-real Element of REAL

dom ((Im A) (#) (Re S)) is Element of K6(X)

dom ((Re A) (#) (Im S)) is Element of K6(X)

dom (Im (A (#) S)) is Element of K6(X)

dom (((Im A) (#) (Re S)) + ((Re A) (#) (Im S))) is Element of K6(X)

(dom ((Im A) (#) (Re S))) /\ (dom ((Re A) (#) (Im S))) is Element of K6(X)

f is set

((Im A) (#) (Re S)) . f is complex real ext-real Element of REAL

(Re S) . f is complex real ext-real Element of REAL

(Im A) * ((Re S) . f) is complex real ext-real Element of REAL

(Im (A (#) S)) . f is complex real ext-real Element of REAL

(A (#) S) . f is complex set

Im ((A (#) S) . f) is complex real ext-real Element of REAL

S . f is complex set

A * (S . f) is complex set

Im (A * (S . f)) is complex real ext-real Element of REAL

(Im S) . f is complex real ext-real Element of REAL

Im (S . f) is complex real ext-real Element of REAL

Re (S . f) is complex real ext-real Element of REAL

((Re A) (#) (Im S)) . f is complex real ext-real Element of REAL

(Re A) * ((Im S) . f) is complex real ext-real Element of REAL

(((Im A) (#) (Re S)) + ((Re A) (#) (Im S))) . f is complex real ext-real Element of REAL

(((Im A) (#) (Re S)) . f) + (((Re A) (#) (Im S)) . f) is complex real ext-real Element of REAL

X is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Im S is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

- (Im S) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

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

(- 1) (#) (Im S) is Relation-like Function-like set

<i> (#) S is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re (<i> (#) S) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Re S is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Im (<i> (#) S) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom (- (Im S)) is Element of K6(X)

K6(X) is non empty set

dom (Im S) is Element of K6(X)

dom (<i> (#) S) is Element of K6(X)

dom S is Element of K6(X)

dom (Re (<i> (#) S)) is Element of K6(X)

A is set

(- (Im S)) . A is complex real ext-real Element of REAL

(Im S) . A is complex real ext-real Element of REAL

- ((Im S) . A) is complex real ext-real Element of REAL

S . A is complex set

<i> * (S . A) is complex set

Re (<i> * (S . A)) is complex real ext-real Element of REAL

Re (S . A) is complex real ext-real Element of REAL

(Re <i>) * (Re (S . A)) is complex real ext-real Element of REAL

Im (S . A) is complex real ext-real Element of REAL

(Im <i>) * (Im (S . A)) is complex real ext-real Element of REAL

((Re <i>) * (Re (S . A))) - ((Im <i>) * (Im (S . A))) is complex real ext-real Element of REAL

- ((Im <i>) * (Im (S . A))) is complex real ext-real set

((Re <i>) * (Re (S . A))) + (- ((Im <i>) * (Im (S . A)))) is complex real ext-real set

(Re (<i> (#) S)) . A is complex real ext-real Element of REAL

(<i> (#) S) . A is complex set

Re ((<i> (#) S) . A) is complex real ext-real Element of REAL

- (Im (S . A)) is complex real ext-real Element of REAL

dom (Re S) is Element of K6(X)

dom (Im (<i> (#) S)) is Element of K6(X)

A is set

S . A is complex set

<i> * (S . A) is complex set

Im (<i> * (S . A)) is complex real ext-real Element of REAL

Re (S . A) is complex real ext-real Element of REAL

(Im <i>) * (Re (S . A)) is complex real ext-real Element of REAL

Im (S . A) is complex real ext-real Element of REAL

(Re <i>) * (Im (S . A)) is complex real ext-real Element of REAL

((Im <i>) * (Re (S . A))) + ((Re <i>) * (Im (S . A))) is complex real ext-real Element of REAL

(Im (<i> (#) S)) . A is complex real ext-real Element of REAL

(<i> (#) S) . A is complex set

Im ((<i> (#) S) . A) is complex real ext-real Element of REAL

(Re S) . A is complex real ext-real Element of REAL

X is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re S is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

Im S is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

S + A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re (S + A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Re A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Re S) + (Re A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Im (S + A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Im A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Im S) + (Im A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom (Re (S + A)) is Element of K6(X)

K6(X) is non empty set

dom (S + A) is Element of K6(X)

dom (Re A) is Element of K6(X)

dom A is Element of K6(X)

dom (Re S) is Element of K6(X)

dom S is Element of K6(X)

dom ((Re S) + (Re A)) is Element of K6(X)

(dom S) /\ (dom A) is Element of K6(X)

f is set

(Re (S + A)) . f is complex real ext-real Element of REAL

(S + A) . f is complex set

Re ((S + A) . f) is complex real ext-real Element of REAL

S . f is complex set

A . f is complex set

(S . f) + (A . f) is complex set

Re ((S . f) + (A . f)) is complex real ext-real Element of REAL

Re (S . f) is complex real ext-real Element of REAL

Re (A . f) is complex real ext-real Element of REAL

(Re (S . f)) + (Re (A . f)) is complex real ext-real Element of REAL

(Re A) . f is complex real ext-real Element of REAL

(Re S) . f is complex real ext-real Element of REAL

((Re S) + (Re A)) . f is complex real ext-real Element of REAL

dom (Im (S + A)) is Element of K6(X)

dom (Im A) is Element of K6(X)

dom (Im S) is Element of K6(X)

dom ((Im S) + (Im A)) is Element of K6(X)

f is set

(Im (S + A)) . f is complex real ext-real Element of REAL

(S + A) . f is complex set

Im ((S + A) . f) is complex real ext-real Element of REAL

S . f is complex set

A . f is complex set

(S . f) + (A . f) is complex set

Im ((S . f) + (A . f)) is complex real ext-real Element of REAL

Im (S . f) is complex real ext-real Element of REAL

Im (A . f) is complex real ext-real Element of REAL

(Im (S . f)) + (Im (A . f)) is complex real ext-real Element of REAL

(Im A) . f is complex real ext-real Element of REAL

(Im S) . f is complex real ext-real Element of REAL

((Im S) + (Im A)) . f is complex real ext-real Element of REAL

X is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re S is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

Im S is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

S - A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

- A is Relation-like Function-like V33() set

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

(- 1) (#) A is Relation-like Function-like set

S + (- A) is Relation-like Function-like set

Re (S - A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Re A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Re S) - (Re A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

- (Re A) is Relation-like Function-like V33() set

(- 1) (#) (Re A) is Relation-like Function-like set

(Re S) + (- (Re A)) is Relation-like Function-like set

Im (S - A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Im A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Im S) - (Im A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

- (Im A) is Relation-like Function-like V33() set

(- 1) (#) (Im A) is Relation-like Function-like set

(Im S) + (- (Im A)) is Relation-like Function-like set

- A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re (- A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Re S) + (Re (- A)) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(- 1) (#) (Re A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Re S) + ((- 1) (#) (Re A)) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Im (- A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Im S) + (Im (- A)) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

Im A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

f is Element of S

(Re A) | f is Relation-like X -defined f -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

A | f is Relation-like X -defined f -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re (A | f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Im A) | f is Relation-like X -defined f -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Im (A | f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom ((Re A) | f) is Element of K6(X)

dom (Re A) is Element of K6(X)

(dom (Re A)) /\ f is Element of K6(X)

dom A is Element of K6(X)

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

dom (A | f) is Element of K6(X)

dom (Re (A | f)) is Element of K6(X)

a is set

(Re (A | f)) . a is complex real ext-real Element of REAL

(A | f) . a is complex set

Re ((A | f) . a) is complex real ext-real Element of REAL

A . a is complex set

Re (A . a) is complex real ext-real Element of REAL

(Re A) . a is complex real ext-real Element of REAL

((Re A) | f) . a is complex real ext-real Element of REAL

dom ((Im A) | f) is Element of K6(X)

dom (Im A) is Element of K6(X)

(dom (Im A)) /\ f is Element of K6(X)

dom (Im (A | f)) is Element of K6(X)

a is set

(Im (A | f)) . a is complex real ext-real Element of REAL

(A | f) . a is complex set

Im ((A | f) . a) is complex real ext-real Element of REAL

A . a is complex set

Im (A . a) is complex real ext-real Element of REAL

(Im A) . a is complex real ext-real Element of REAL

((Im A) | f) . a is complex real ext-real Element of REAL

X is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re S is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

Im S is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

<i> (#) (Im S) is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

(Re S) + (<i> (#) (Im S)) is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

dom S is Element of K6(X)

K6(X) is non empty set

dom (Re S) is Element of K6(X)

dom (Im S) is Element of K6(X)

dom ((Re S) + (<i> (#) (Im S))) is Element of K6(X)

dom (<i> (#) (Im S)) is Element of K6(X)

(dom (Re S)) /\ (dom (<i> (#) (Im S))) is Element of K6(X)

(dom S) /\ (dom S) is Element of K6(X)

A is set

((Re S) + (<i> (#) (Im S))) . A is complex set

(Re S) . A is complex real ext-real Element of REAL

(<i> (#) (Im S)) . A is complex set

((Re S) . A) + ((<i> (#) (Im S)) . A) is complex set

S . A is complex set

Re (S . A) is complex real ext-real Element of REAL

(Re (S . A)) + ((<i> (#) (Im S)) . A) is complex set

(Im S) . A is complex real ext-real Element of REAL

<i> * ((Im S) . A) is complex set

(Re (S . A)) + (<i> * ((Im S) . A)) is complex set

Im (S . A) is complex real ext-real Element of REAL

<i> * (Im (S . A)) is complex set

(Re (S . A)) + (<i> * (Im (S . A))) is complex set

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

f is Element of S

a is Element of S

Im A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

Re A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

f is Element of S

a is Element of S

f \/ a is M11(X,S)

Im A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

Re A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

A + f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

a is Element of S

Im f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

Im A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Im A) + (Im f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Im (A + f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Re f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Re A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Re A) + (Re f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Re (A + f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

dom f is Element of K6(X)

A - f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

- f is Relation-like Function-like V33() set

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

(- 1) (#) f is Relation-like Function-like set

A + (- f) is Relation-like Function-like set

a is Element of S

Im f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

Re f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

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

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

Im A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Im A) - (Im f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

- (Im f) is Relation-like Function-like V33() set

(- 1) (#) (Im f) is Relation-like Function-like set

(Im A) + (- (Im f)) is Relation-like Function-like set

Im (A - f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Re A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Re A) - (Re f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

- (Re f) is Relation-like Function-like V33() set

(- 1) (#) (Re f) is Relation-like Function-like set

(Re A) + (- (Re f)) is Relation-like Function-like set

Re (A - f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

X is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is set

A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

A | S is Relation-like X -defined S -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

A + f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

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

K6(X) is non empty set

f | S is Relation-like X -defined S -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

(A | S) + (f | S) is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

dom ((A | S) + (f | S)) is Element of K6(X)

(A + f) | S is Relation-like X -defined S -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

dom A is Element of K6(X)

dom f is Element of K6(X)

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

dom ((A + f) | S) is Element of K6(X)

dom (f | S) is Element of K6(X)

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

dom (A | S) is Element of K6(X)

(dom A) /\ S is Element of K6(X)

S /\ S is set

a is set

((A + f) | S) . a is complex set

(A + f) . a is complex set

A . a is complex set

f . a is complex set

(A . a) + (f . a) is complex set

(A | S) . a is complex set

((A | S) . a) + (f . a) is complex set

(f | S) . a is complex set

((A | S) . a) + ((f | S) . a) is complex set

((A | S) + (f | S)) . a is complex set

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

dom A is Element of K6(X)

f is Element of S

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

A | f is Relation-like X -defined f -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

a is Element of S

Im A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

dom (Im A) is Element of K6(X)

(dom (Im A)) /\ f is Element of K6(X)

(Im A) | f is Relation-like X -defined f -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Im (A | f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Re A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom (Re A) is Element of K6(X)

(dom (Re A)) /\ f is Element of K6(X)

(Re A) | f is Relation-like X -defined f -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Re (A | f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

dom A is Element of K6(X)

f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

dom f is Element of K6(X)

A + f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

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

a is Element of S

x is Element of S

a /\ x is M11(X,S)

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

dom A is Element of K6(X)

f is Element of S

a is Element of S

f /\ a is M11(X,S)

Re A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

dom (Re A) is Element of K6(X)

Im A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom (Im A) is Element of K6(X)

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

dom A is Element of K6(X)

f is complex set

f (#) A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

a is Element of S

Im A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

dom (Im A) is Element of K6(X)

Re f is complex real ext-real Element of REAL

(Re f) (#) (Im A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Im f is complex real ext-real Element of REAL

(Im f) (#) (Im A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Re A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom (Re A) is Element of K6(X)

(Im f) (#) (Re A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

((Im f) (#) (Re A)) + ((Re f) (#) (Im A)) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Im (f (#) A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

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

(Re f) (#) (Re A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

((Re f) (#) (Re A)) - ((Im f) (#) (Im A)) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

- ((Im f) (#) (Im A)) is Relation-like Function-like V33() set

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

(- 1) (#) ((Im f) (#) (Im A)) is Relation-like Function-like set

((Re f) (#) (Re A)) + (- ((Im f) (#) (Im A))) is Relation-like Function-like set

Re (f (#) A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

dom A is Element of K6(X)

f is Element of S

f is Element of S

Re A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

a is complex set

Re a is complex real ext-real Element of REAL

(Re a) (#) (Re A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom ((Re a) (#) (Re A)) is Element of K6(X)

dom (Re A) is Element of K6(X)

Im A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Im a is complex real ext-real Element of REAL

(Im a) (#) (Im A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom ((Im a) (#) (Im A)) is Element of K6(X)

dom (Im A) is Element of K6(X)

a (#) A is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re (a (#) A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom (Re (a (#) A)) is Element of K6(X)

((Re a) (#) (Re A)) - ((Im a) (#) (Im A)) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

- ((Im a) (#) (Im A)) is Relation-like Function-like V33() set

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

(- 1) (#) ((Im a) (#) (Im A)) is Relation-like Function-like set

((Re a) (#) (Re A)) + (- ((Im a) (#) (Im A))) is Relation-like Function-like set

dom (((Re a) (#) (Re A)) - ((Im a) (#) (Im A))) is Element of K6(X)

(dom ((Re a) (#) (Re A))) /\ (dom ((Im a) (#) (Im A))) is Element of K6(X)

(Im a) (#) (Re A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom ((Im a) (#) (Re A)) is Element of K6(X)

Im (a (#) A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom (Im (a (#) A)) is Element of K6(X)

(Re a) (#) (Im A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

((Im a) (#) (Re A)) + ((Re a) (#) (Im A)) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom (((Im a) (#) (Re A)) + ((Re a) (#) (Im A))) is Element of K6(X)

dom ((Re a) (#) (Im A)) is Element of K6(X)

(dom ((Im a) (#) (Re A))) /\ (dom ((Re a) (#) (Im A))) is Element of K6(X)

x is Element of S

f /\ x is M11(X,S)

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

K7(S,ExtREAL) is non empty Relation-like V34() set

K6(K7(S,ExtREAL)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

K7(S,ExtREAL) is non empty Relation-like V34() set

K6(K7(S,ExtREAL)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

A is Relation-like S -defined ExtREAL -valued Function-like V27(S, ExtREAL ) V34() V42() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))

f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

Re f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

Integral (A,(Re f)) is ext-real Element of ExtREAL

R_EAL (Re f) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

K7(X,ExtREAL) is non empty Relation-like V34() set

K6(K7(X,ExtREAL)) is non empty set

Integral (A,(R_EAL (Re f))) is ext-real Element of ExtREAL

max+ (R_EAL (Re f)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max+ (R_EAL (Re f)))) is ext-real Element of ExtREAL

max- (R_EAL (Re f)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max- (R_EAL (Re f)))) is ext-real Element of ExtREAL

(integral+ (A,(max+ (R_EAL (Re f))))) - (integral+ (A,(max- (R_EAL (Re f))))) is ext-real Element of ExtREAL

Im f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Integral (A,(Im f)) is ext-real Element of ExtREAL

R_EAL (Im f) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

Integral (A,(R_EAL (Im f))) is ext-real Element of ExtREAL

max+ (R_EAL (Im f)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max+ (R_EAL (Im f)))) is ext-real Element of ExtREAL

max- (R_EAL (Im f)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max- (R_EAL (Im f)))) is ext-real Element of ExtREAL

(integral+ (A,(max+ (R_EAL (Im f))))) - (integral+ (A,(max- (R_EAL (Im f))))) is ext-real Element of ExtREAL

a is complex real ext-real Element of REAL

x is complex real ext-real Element of REAL

x * <i> is complex set

a + (x * <i>) is complex set

x is complex real ext-real Element of REAL

I1 is complex real ext-real Element of REAL

a is complex set

I1 * <i> is complex set

x + (I1 * <i>) is complex set

R2 is complex real ext-real Element of REAL

I2 is complex real ext-real Element of REAL

x is complex set

I2 * <i> is complex set

R2 + (I2 * <i>) is complex set

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,ExtREAL) is non empty Relation-like V34() set

K6(K7(X,ExtREAL)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

K7(S,ExtREAL) is non empty Relation-like V34() set

K6(K7(S,ExtREAL)) is non empty set

f is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

max+ f is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

max- f is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

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

a is set

(max- f) . a is ext-real Element of ExtREAL

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

a is set

(max+ f) . a is ext-real Element of ExtREAL

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,ExtREAL) is non empty Relation-like V34() set

K6(K7(X,ExtREAL)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

K7(S,ExtREAL) is non empty Relation-like V34() set

K6(K7(S,ExtREAL)) is non empty set

A is Relation-like S -defined ExtREAL -valued Function-like V27(S, ExtREAL ) V34() V42() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))

f is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

dom f is Element of K6(X)

a is Element of S

A . a is ext-real Element of ExtREAL

f | a is Relation-like X -defined a -defined X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

max+ f is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

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

(max+ f) | a is Relation-like X -defined a -defined X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,((max+ f) | a)) is ext-real Element of ExtREAL

x is Element of S

max+ (f | a) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max+ (f | a))) is ext-real Element of ExtREAL

x is Element of S

x is Element of S

a /\ x is M11(X,S)

(dom f) /\ (a /\ x) is Element of K6(X)

max- f is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

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

(max- f) | a is Relation-like X -defined a -defined X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,((max- f) | a)) is ext-real Element of ExtREAL

x is Element of S

max- (f | a) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max- (f | a))) is ext-real Element of ExtREAL

dom (f | a) is Element of K6(X)

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

f | (a /\ x) is Relation-like X -defined a /\ x -defined X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

f | x is Relation-like X -defined x -defined X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

(f | a) /\ (f | x) is Relation-like X -defined ExtREAL -valued V34() Element of K6(K7(X,ExtREAL))

(f | a) /\ f is Relation-like X -defined ExtREAL -valued V34() Element of K6(K7(X,ExtREAL))

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

K7(S,ExtREAL) is non empty Relation-like V34() set

K6(K7(S,ExtREAL)) is non empty set

A is Relation-like S -defined ExtREAL -valued Function-like V27(S, ExtREAL ) V34() V42() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))

f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

dom f is Element of K6(X)

x is Element of S

A . x is ext-real Element of ExtREAL

f | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

x is Element of S

x is Element of S

R_EAL f is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

K7(X,ExtREAL) is non empty Relation-like V34() set

K6(K7(X,ExtREAL)) is non empty set

R_EAL (f | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

K7(S,ExtREAL) is non empty Relation-like V34() set

K6(K7(S,ExtREAL)) is non empty set

A is Relation-like S -defined ExtREAL -valued Function-like V27(S, ExtREAL ) V34() V42() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))

f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

dom f is Element of K6(X)

a is Element of S

A . a is ext-real Element of ExtREAL

f | a is Relation-like X -defined a -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

(X,S,A,(f | a)) is complex set

x is Element of S

x is Element of S

Im f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

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

(Im f) | a is Relation-like X -defined a -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Integral (A,((Im f) | a)) is ext-real Element of ExtREAL

R_EAL ((Im f) | a) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

K7(X,ExtREAL) is non empty Relation-like V34() set

K6(K7(X,ExtREAL)) is non empty set

Integral (A,(R_EAL ((Im f) | a))) is ext-real Element of ExtREAL

max+ (R_EAL ((Im f) | a)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max+ (R_EAL ((Im f) | a)))) is ext-real Element of ExtREAL

max- (R_EAL ((Im f) | a)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max- (R_EAL ((Im f) | a)))) is ext-real Element of ExtREAL

(integral+ (A,(max+ (R_EAL ((Im f) | a))))) - (integral+ (A,(max- (R_EAL ((Im f) | a))))) is ext-real Element of ExtREAL

Im (f | a) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Re f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

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

Re (f | a) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

(Re f) | a is Relation-like X -defined a -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Integral (A,(Re (f | a))) is ext-real Element of ExtREAL

R_EAL (Re (f | a)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

Integral (A,(R_EAL (Re (f | a)))) is ext-real Element of ExtREAL

max+ (R_EAL (Re (f | a))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max+ (R_EAL (Re (f | a))))) is ext-real Element of ExtREAL

max- (R_EAL (Re (f | a))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max- (R_EAL (Re (f | a))))) is ext-real Element of ExtREAL

(integral+ (A,(max+ (R_EAL (Re (f | a)))))) - (integral+ (A,(max- (R_EAL (Re (f | a)))))) is ext-real Element of ExtREAL

Integral (A,(Im (f | a))) is ext-real Element of ExtREAL

R_EAL (Im (f | a)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

Integral (A,(R_EAL (Im (f | a)))) is ext-real Element of ExtREAL

max+ (R_EAL (Im (f | a))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max+ (R_EAL (Im (f | a))))) is ext-real Element of ExtREAL

max- (R_EAL (Im (f | a))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max- (R_EAL (Im (f | a))))) is ext-real Element of ExtREAL

(integral+ (A,(max+ (R_EAL (Im (f | a)))))) - (integral+ (A,(max- (R_EAL (Im (f | a)))))) is ext-real Element of ExtREAL

I1 is complex real ext-real Element of REAL

R2 is complex real ext-real Element of REAL

R2 * <i> is complex set

I1 + (R2 * <i>) is complex set

X is non empty set

K6(X) is non empty set

K6(K6(X)) is non empty set

K7(X,COMPLEX) is non empty Relation-like V33() set

K6(K7(X,COMPLEX)) is non empty set

S is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(X))

K7(S,ExtREAL) is non empty Relation-like V34() set

K6(K7(S,ExtREAL)) is non empty set

A is Relation-like S -defined ExtREAL -valued Function-like V27(S, ExtREAL ) V34() V42() nonnegative sigma-additive Element of K6(K7(S,ExtREAL))

f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

dom f is Element of K6(X)

(X,S,A,f) is complex set

a is Element of S

x is Element of S

A . x is ext-real Element of ExtREAL

a \ x is M11(X,S)

f | (a \ x) is Relation-like X -defined a \ x -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))

(X,S,A,(f | (a \ x))) is complex set

Re f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

K7(X,REAL) is non empty Relation-like V33() V34() V35() set

K6(K7(X,REAL)) is non empty set

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

Im f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

R_EAL (Im f) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

K7(X,ExtREAL) is non empty Relation-like V34() set

K6(K7(X,ExtREAL)) is non empty set

dom (R_EAL (Im f)) is Element of K6(X)

I1 is Element of S

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

(Im f) | (a \ x) is Relation-like X -defined a \ x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Integral (A,((Im f) | (a \ x))) is ext-real Element of ExtREAL

R_EAL ((Im f) | (a \ x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

Integral (A,(R_EAL ((Im f) | (a \ x)))) is ext-real Element of ExtREAL

max+ (R_EAL ((Im f) | (a \ x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max+ (R_EAL ((Im f) | (a \ x))))) is ext-real Element of ExtREAL

max- (R_EAL ((Im f) | (a \ x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max- (R_EAL ((Im f) | (a \ x))))) is ext-real Element of ExtREAL

(integral+ (A,(max+ (R_EAL ((Im f) | (a \ x)))))) - (integral+ (A,(max- (R_EAL ((Im f) | (a \ x)))))) is ext-real Element of ExtREAL

Im (f | (a \ x)) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Integral (A,(Im (f | (a \ x)))) is ext-real Element of ExtREAL

R_EAL (Im (f | (a \ x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

Integral (A,(R_EAL (Im (f | (a \ x))))) is ext-real Element of ExtREAL

max+ (R_EAL (Im (f | (a \ x)))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max+ (R_EAL (Im (f | (a \ x)))))) is ext-real Element of ExtREAL

max- (R_EAL (Im (f | (a \ x)))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max- (R_EAL (Im (f | (a \ x)))))) is ext-real Element of ExtREAL

(integral+ (A,(max+ (R_EAL (Im (f | (a \ x))))))) - (integral+ (A,(max- (R_EAL (Im (f | (a \ x))))))) is ext-real Element of ExtREAL

Integral (A,(Im f)) is ext-real Element of ExtREAL

Integral (A,(R_EAL (Im f))) is ext-real Element of ExtREAL

max+ (R_EAL (Im f)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max+ (R_EAL (Im f)))) is ext-real Element of ExtREAL

max- (R_EAL (Im f)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

integral+ (A,(max- (R_EAL (Im f)))) is ext-real Element of ExtREAL

(integral+ (A,(max+ (R_EAL (Im f))))) - (integral+ (A,(max- (R_EAL (Im f))))) is ext-real Element of ExtREAL

R_EAL (Re f) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

dom (R_EAL (Re f)) is Element of K6(X)

R2 is Element of S

(Re f) | (a \ x) is Relation-like X -defined a \ x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))

Integral (A,((Re f) | (a \ x))) is ext-real Element of ExtREAL

R_EAL ((Re f) | (a \ x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))

Integral (A,(R_EAL ((