:: 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 ((Re f) | (a \ x)))) is ext-real Element of ExtREAL
max+ (R_EAL ((Re f) | (a \ x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Re f) | (a \ x))))) is ext-real Element of ExtREAL
max- (R_EAL ((Re f) | (a \ x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Re f) | (a \ x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Re f) | (a \ x)))))) - (integral+ (A,(max- (R_EAL ((Re f) | (a \ x)))))) is ext-real Element of ExtREAL
Re (f | (a \ x)) is Relation-like 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 (Re (f | (a \ x))))) is ext-real Element of ExtREAL
max+ (R_EAL (Re (f | (a \ x)))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Re (f | (a \ x)))))) is ext-real Element of ExtREAL
max- (R_EAL (Re (f | (a \ x)))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Re (f | (a \ x)))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Re (f | (a \ x))))))) - (integral+ (A,(max- (R_EAL (Re (f | (a \ x))))))) is ext-real Element of ExtREAL
Integral (A,(Re f)) is ext-real Element of ExtREAL
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
I2 is complex real ext-real Element of REAL
R is complex real ext-real Element of REAL
R * <i> is complex set
I2 + (R * <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))
a is Element of S
f | a is Relation-like X -defined a -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
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 f) | a is Relation-like X -defined a -defined 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))
Re f 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))
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))
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))
a is Element of S
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
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
f | x is Relation-like X -defined x -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,(f | x)) is complex set
(X,S,A,(f | a)) + (X,S,A,(f | x)) is complex set
Re (f | x) 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 | x))) is ext-real Element of ExtREAL
R_EAL (Re (f | x)) 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 | x)))) is ext-real Element of ExtREAL
max+ (R_EAL (Re (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Re (f | x))))) is ext-real Element of ExtREAL
max- (R_EAL (Re (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Re (f | x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Re (f | x)))))) - (integral+ (A,(max- (R_EAL (Re (f | x)))))) is ext-real Element of ExtREAL
Im (f | x) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Im (f | x))) is ext-real Element of ExtREAL
R_EAL (Im (f | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Im (f | x)))) is ext-real Element of ExtREAL
max+ (R_EAL (Im (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Im (f | x))))) is ext-real Element of ExtREAL
max- (R_EAL (Im (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Im (f | x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Im (f | x)))))) - (integral+ (A,(max- (R_EAL (Im (f | x)))))) is ext-real Element of ExtREAL
Re (f | a) is Relation-like 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
Re (f | (a \/ x)) is Relation-like 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 (Re (f | (a \/ x))))) is ext-real Element of ExtREAL
max+ (R_EAL (Re (f | (a \/ x)))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Re (f | (a \/ x)))))) is ext-real Element of ExtREAL
max- (R_EAL (Re (f | (a \/ x)))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Re (f | (a \/ x)))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Re (f | (a \/ x))))))) - (integral+ (A,(max- (R_EAL (Re (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
I2 is complex real ext-real Element of REAL
R is complex real ext-real Element of REAL
R * <i> is complex set
I2 + (R * <i>) is complex set
Im (f | a) is Relation-like 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))
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 is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
(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 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))
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) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,((Im f) | x)) is ext-real Element of ExtREAL
R_EAL ((Im f) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Im f) | x))) is ext-real Element of ExtREAL
max+ (R_EAL ((Im f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Im f) | x)))) is ext-real Element of ExtREAL
max- (R_EAL ((Im f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Im f) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Im f) | x))))) - (integral+ (A,(max- (R_EAL ((Im f) | x))))) is ext-real Element of ExtREAL
(Integral (A,((Im f) | a))) + (Integral (A,((Im f) | x))) is ext-real Element of ExtREAL
(Integral (A,(Im (f | a)))) + (Integral (A,((Im f) | x))) is ext-real Element of ExtREAL
(Integral (A,(Im (f | a)))) + (Integral (A,(Im (f | x)))) is ext-real Element of ExtREAL
R_EAL R is ext-real Element of ExtREAL
E is complex real ext-real Element of REAL
R_EAL E is ext-real Element of ExtREAL
I1 is complex real ext-real Element of REAL
R_EAL I1 is ext-real Element of ExtREAL
(R_EAL E) + (R_EAL I1) is ext-real Element of ExtREAL
E + I1 is complex real ext-real Element of REAL
Re f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
(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 ((Re f) | (a \/ x)))) is ext-real Element of ExtREAL
max+ (R_EAL ((Re f) | (a \/ x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Re f) | (a \/ x))))) is ext-real Element of ExtREAL
max- (R_EAL ((Re f) | (a \/ x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Re f) | (a \/ x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Re f) | (a \/ x)))))) - (integral+ (A,(max- (R_EAL ((Re f) | (a \/ x)))))) is ext-real Element of ExtREAL
(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
(Re f) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,((Re f) | x)) is ext-real Element of ExtREAL
R_EAL ((Re f) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Re f) | x))) is ext-real Element of ExtREAL
max+ (R_EAL ((Re f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Re f) | x)))) is ext-real Element of ExtREAL
max- (R_EAL ((Re f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Re f) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Re f) | x))))) - (integral+ (A,(max- (R_EAL ((Re f) | x))))) is ext-real Element of ExtREAL
(Integral (A,((Re f) | a))) + (Integral (A,((Re f) | x))) is ext-real Element of ExtREAL
(Integral (A,(Re (f | a)))) + (Integral (A,((Re f) | x))) is ext-real Element of ExtREAL
(Integral (A,(Re (f | a)))) + (Integral (A,(Re (f | x)))) is ext-real Element of ExtREAL
R_EAL I2 is ext-real Element of ExtREAL
I is complex real ext-real Element of REAL
R_EAL I is ext-real Element of ExtREAL
x is complex real ext-real Element of REAL
R_EAL x is ext-real Element of ExtREAL
(R_EAL I) + (R_EAL x) is ext-real Element of ExtREAL
I + x is complex real ext-real Element of REAL
E * <i> is complex set
I + (E * <i>) is complex set
I1 * <i> is complex set
x + (I1 * <i>) is complex set
(I + (E * <i>)) + (x + (I1 * <i>)) is complex set
(X,S,A,(f | a)) + (x + (I1 * <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
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
(dom f) \ x is Element of K6(X)
f | x is Relation-like X -defined x -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,(f | x)) is complex set
(X,S,A,(f | x)) + (X,S,A,(f | a)) 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
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
x is complex real ext-real Element of REAL
I1 is complex real ext-real Element of REAL
I1 * <i> is complex set
x + (I1 * <i>) is complex set
Re (f | a) is Relation-like 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
Im (f | a) is Relation-like 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))
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
Re (f | x) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Re (f | x))) is ext-real Element of ExtREAL
R_EAL (Re (f | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Re (f | x)))) is ext-real Element of ExtREAL
max+ (R_EAL (Re (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Re (f | x))))) is ext-real Element of ExtREAL
max- (R_EAL (Re (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Re (f | x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Re (f | x)))))) - (integral+ (A,(max- (R_EAL (Re (f | x)))))) is ext-real Element of ExtREAL
Im (f | x) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Im (f | x))) is ext-real Element of ExtREAL
R_EAL (Im (f | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Im (f | x)))) is ext-real Element of ExtREAL
max+ (R_EAL (Im (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Im (f | x))))) is ext-real Element of ExtREAL
max- (R_EAL (Im (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Im (f | x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Im (f | x)))))) - (integral+ (A,(max- (R_EAL (Im (f | x)))))) is ext-real Element of ExtREAL
dom (Im f) is Element of K6(X)
(Im f) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,((Im f) | x)) is ext-real Element of ExtREAL
R_EAL ((Im f) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Im f) | x))) is ext-real Element of ExtREAL
max+ (R_EAL ((Im f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Im f) | x)))) is ext-real Element of ExtREAL
max- (R_EAL ((Im f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Im f) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Im f) | x))))) - (integral+ (A,(max- (R_EAL ((Im f) | x))))) is ext-real Element of ExtREAL
(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))
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
(Integral (A,((Im f) | x))) + (Integral (A,((Im f) | a))) is ext-real Element of ExtREAL
(Integral (A,(Im (f | x)))) + (Integral (A,((Im f) | a))) is ext-real Element of ExtREAL
(Integral (A,(Im (f | x)))) + (Integral (A,(Im (f | a)))) is ext-real Element of ExtREAL
I is complex real ext-real Element of REAL
I2 is complex real ext-real Element of REAL
I + I2 is complex real ext-real Element of REAL
dom (Re f) is Element of K6(X)
(Re f) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,((Re f) | x)) is ext-real Element of ExtREAL
R_EAL ((Re f) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Re f) | x))) is ext-real Element of ExtREAL
max+ (R_EAL ((Re f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Re f) | x)))) is ext-real Element of ExtREAL
max- (R_EAL ((Re f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Re f) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Re f) | x))))) - (integral+ (A,(max- (R_EAL ((Re f) | x))))) is ext-real Element of ExtREAL
(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,((Re f) | x))) + (Integral (A,((Re f) | a))) is ext-real Element of ExtREAL
(Integral (A,(Re (f | x)))) + (Integral (A,((Re f) | a))) is ext-real Element of ExtREAL
(Integral (A,(Re (f | x)))) + (Integral (A,(Re (f | a)))) is ext-real Element of ExtREAL
R is complex real ext-real Element of REAL
R2 is complex real ext-real Element of REAL
R + R2 is complex real ext-real Element of REAL
I * <i> is complex set
R + (I * <i>) is complex set
I2 * <i> is complex set
R2 + (I2 * <i>) is complex set
(R + (I * <i>)) + (R2 + (I2 * <i>)) is complex set
(X,S,A,(f | x)) + (R2 + (I2 * <i>)) is complex set
S is non empty set
K7(S,REAL) is non empty Relation-like V33() V34() V35() set
K6(K7(S,REAL)) is non empty set
A is Relation-like S -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(S,REAL))
dom A is Element of K6(S)
K6(S) is non empty set
X is complex real ext-real set
f is Relation-like S -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(S,REAL))
dom f is Element of K6(S)
a is Element of S
A . a is complex real ext-real Element of REAL
(A . a) to_power X is complex real ext-real set
x is complex real ext-real Element of REAL
a is Element of S
f . a is complex real ext-real Element of REAL
A . a is complex real ext-real Element of REAL
(A . a) to_power X is complex real ext-real set
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 Relation-like Function-like set
A is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
f is ext-real Element of ExtREAL
rng A is V50() V51() V52() set
S is non empty set
K7(S,REAL) is non empty Relation-like V33() V34() V35() set
K6(K7(S,REAL)) is non empty set
X is complex real ext-real non negative set
A is Relation-like S -defined REAL -valued Function-like V33() V34() V35() nonnegative Element of K6(K7(S,REAL))
(X,S,A) is Relation-like S -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(S,REAL))
f is set
dom (X,S,A) is Element of K6(S)
K6(S) is non empty set
A . f is complex real ext-real Element of REAL
(A . f) to_power X is complex real ext-real set
(X,S,A) . f is complex real ext-real Element of REAL
A . f is complex real ext-real Element of REAL
(A . f) to_power X is complex real ext-real set
(X,S,A) . f is complex real ext-real Element of REAL
A . f is complex real ext-real Element of REAL
(A . f) to_power X is complex real ext-real set
(X,S,A) . f is complex real ext-real Element of REAL
A . f is complex real ext-real Element of REAL
S is non empty set
K6(S) is non empty set
K6(K6(S)) is non empty set
A is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(S))
K7(S,REAL) is non empty Relation-like V33() V34() V35() set
K6(K7(S,REAL)) is non empty set
a is Relation-like S -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(S,REAL))
X is complex real ext-real set
(X,S,a) is Relation-like S -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(S,REAL))
1 / 2 is non empty complex real ext-real positive non negative Element of REAL
2 " is non empty complex real ext-real positive non negative set
1 * (2 ") is non empty complex real ext-real positive non negative set
X is set
S is non empty set
K6(S) is non empty set
K6(K6(S)) is non empty set
K7(S,REAL) is non empty Relation-like V33() V34() V35() set
K6(K7(S,REAL)) is non empty set
A is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(S))
a is Relation-like S -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(S,REAL))
a . X is complex real ext-real Element of REAL
(a . X) to_power (1 / 2) is complex real ext-real Element of REAL
sqrt (a . X) is complex real ext-real Element of REAL
2 -root (a . X) is complex real ext-real Element of REAL
2 -Root (a . X) is complex real ext-real Element of REAL
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))
A is Element of S
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)
a is complex real ext-real Element of REAL
less_dom (f,a) is set
A /\ (less_dom (f,a)) is Element of K6(X)
great_eq_dom (f,a) is set
A /\ (great_eq_dom (f,a)) is Element of K6(X)
A \ (A /\ (great_eq_dom (f,a))) is Element of K6(X)
x is set
f . x is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
I1 is complex real ext-real Element of REAL
x is set
f . x is complex real ext-real Element of REAL
X is complex real ext-real set
S is non empty set
K6(S) is non empty set
K6(K6(S)) is non empty set
K7(S,REAL) is non empty Relation-like V33() V34() V35() set
K6(K7(S,REAL)) is non empty set
A is non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive Element of K6(K6(S))
f is Element of A
a is Relation-like S -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(S,REAL))
dom a is Element of K6(S)
(X,S,a) is Relation-like S -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(S,REAL))
dom (X,S,a) is Element of K6(S)
x is complex real ext-real set
R2 is set
(X,S,a) . R2 is complex real ext-real Element of REAL
a . R2 is complex real ext-real Element of REAL
(a . R2) to_power X is complex real ext-real set
I1 is complex real ext-real Element of REAL
great_eq_dom ((X,S,a),I1) is set
great_eq_dom ((X,S,a),x) is set
f /\ (great_eq_dom ((X,S,a),x)) is Element of K6(S)
less_dom ((X,S,a),I1) is set
f /\ (less_dom ((X,S,a),I1)) is Element of K6(S)
f \ f is M11(S,A)
less_dom ((X,S,a),x) is set
f /\ (less_dom ((X,S,a),x)) is Element of K6(S)
R2 is set
(X,S,a) . R2 is complex real ext-real Element of REAL
a . R2 is complex real ext-real Element of REAL
(a . R2) to_power X is complex real ext-real set
less_dom ((X,S,a),x) is set
f /\ (less_dom ((X,S,a),x)) is Element of K6(S)
x is complex real ext-real set
great_eq_dom ((X,S,a),x) is set
f /\ (great_eq_dom ((X,S,a),x)) is Element of K6(S)
I1 is complex real ext-real Element of REAL
R2 is set
(X,S,a) . R2 is complex real ext-real Element of REAL
great_eq_dom ((X,S,a),I1) is set
I1 is complex real ext-real Element of REAL
1 / X is complex real ext-real Element of REAL
X " is complex real ext-real set
1 * (X ") is complex real ext-real set
x to_power (1 / X) is complex real ext-real set
I2 is set
I1 to_power (1 / X) is complex real ext-real Element of REAL
great_eq_dom (a,(I1 to_power (1 / X))) is set
(x to_power (1 / X)) to_power X is complex real ext-real set
(1 / X) * X is complex real ext-real Element of REAL
x to_power ((1 / X) * X) is complex real ext-real set
x to_power 1 is complex real ext-real set
a . I2 is complex real ext-real Element of REAL
I1 to_power 1 is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
(a . I2) to_power x is complex real ext-real Element of REAL
R is complex real ext-real Element of REAL
(a . I2) to_power X is complex real ext-real set
(X,S,a) . I2 is complex real ext-real Element of REAL
great_eq_dom ((X,S,a),I1) is set
R2 is set
a . R2 is complex real ext-real Element of REAL
(a . R2) to_power x is complex real ext-real Element of REAL
1 / x is complex real ext-real Element of REAL
x " is complex real ext-real set
1 * (x ") is complex real ext-real set
((a . R2) to_power x) to_power (1 / x) is complex real ext-real Element of REAL
x * 1 is complex real ext-real Element of REAL
(x * 1) / x is complex real ext-real Element of REAL
(x * 1) * (x ") is complex real ext-real set
(a . R2) to_power ((x * 1) / x) is complex real ext-real Element of REAL
(a . R2) to_power 1 is complex real ext-real Element of REAL
(a . R2) to_power X is complex real ext-real set
((a . R2) to_power X) to_power (1 / X) is complex real ext-real set
(X,S,a) . R2 is complex real ext-real Element of REAL
I2 is complex real ext-real Element of REAL
x to_power (1 / x) is complex real ext-real set
f /\ (great_eq_dom ((X,S,a),I1)) is Element of K6(S)
f /\ (great_eq_dom (a,(I1 to_power (1 / X)))) is Element of K6(S)
I1 is complex real ext-real Element of 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)
|.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
f is Element of S
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)
a is set
|.(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)
|.(Im A).| . a is complex real ext-real Element of REAL
(Im A) . a is complex real ext-real Element of REAL
|.((Im A) . a).| is complex real ext-real Element of REAL
Re ((Im A) . a) is complex real ext-real Element of REAL
(Re ((Im A) . a)) ^2 is complex real ext-real Element of REAL
Im ((Im A) . a) is complex real ext-real Element of REAL
(Im ((Im A) . a)) ^2 is complex real ext-real Element of REAL
((Re ((Im A) . a)) ^2) + ((Im ((Im A) . a)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((Im A) . a)) ^2) + ((Im ((Im A) . a)) ^2)) is complex real ext-real Element of REAL
(2,X,|.(Im A).|) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
dom (2,X,|.(Im A).|) is Element of K6(X)
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)
a is set
(Re A) . a is complex real ext-real Element of REAL
|.((Re A) . a).| is complex real ext-real Element of REAL
Re ((Re A) . a) is complex real ext-real Element of REAL
(Re ((Re A) . a)) ^2 is complex real ext-real Element of REAL
Im ((Re A) . a) is complex real ext-real Element of REAL
(Im ((Re A) . a)) ^2 is complex real ext-real Element of REAL
((Re ((Re A) . a)) ^2) + ((Im ((Re A) . a)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((Re A) . a)) ^2) + ((Im ((Re A) . a)) ^2)) is complex real ext-real Element of 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)
|.(Re A).| . a is complex real ext-real Element of REAL
(2,X,|.(Re A).|) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
(2,X,|.(Re A).|) + (2,X,|.(Im A).|) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
dom |.A.| is Element of K6(X)
dom (2,X,|.(Re A).|) is Element of K6(X)
dom ((2,X,|.(Re A).|) + (2,X,|.(Im A).|)) is Element of K6(X)
(dom (2,X,|.(Re A).|)) /\ (dom (2,X,|.(Im A).|)) is Element of K6(X)
((1 / 2),X,((2,X,|.(Re A).|) + (2,X,|.(Im A).|))) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
dom ((1 / 2),X,((2,X,|.(Re A).|) + (2,X,|.(Im A).|))) is Element of K6(X)
x is set
(2,X,|.(Re A).|) . x is complex real ext-real Element of REAL
|.(Re A).| . x is complex real ext-real Element of REAL
(|.(Re A).| . x) to_power 2 is complex real ext-real Element of REAL
(Re A) . x is complex real ext-real Element of REAL
|.((Re A) . x).| is complex real ext-real Element of REAL
Re ((Re A) . x) is complex real ext-real Element of REAL
(Re ((Re A) . x)) ^2 is complex real ext-real Element of REAL
Im ((Re A) . x) is complex real ext-real Element of REAL
(Im ((Re A) . x)) ^2 is complex real ext-real Element of REAL
((Re ((Re A) . x)) ^2) + ((Im ((Re A) . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((Re A) . x)) ^2) + ((Im ((Re A) . x)) ^2)) is complex real ext-real Element of REAL
|.((Re A) . x).| to_power 2 is complex real ext-real Element of REAL
A . x is complex set
Re (A . x) is complex real ext-real Element of REAL
|.(Re (A . x)).| is complex real ext-real Element of REAL
Re (Re (A . x)) is complex real ext-real Element of REAL
(Re (Re (A . x))) ^2 is complex real ext-real Element of REAL
Im (Re (A . x)) is complex real ext-real Element of REAL
(Im (Re (A . x))) ^2 is complex real ext-real Element of REAL
((Re (Re (A . x))) ^2) + ((Im (Re (A . x))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (Re (A . x))) ^2) + ((Im (Re (A . x))) ^2)) is complex real ext-real Element of REAL
|.(Re (A . x)).| to_power 2 is complex real ext-real Element of REAL
|.(Re (A . x)).| ^2 is complex real ext-real Element of REAL
(Re (A . x)) ^2 is complex real ext-real Element of REAL
(2,X,|.(Im A).|) . x is complex real ext-real Element of REAL
|.(Im A).| . x is complex real ext-real Element of REAL
(|.(Im A).| . x) to_power 2 is complex real ext-real Element of REAL
(Im A) . x is complex real ext-real Element of REAL
|.((Im A) . x).| is complex real ext-real Element of REAL
Re ((Im A) . x) is complex real ext-real Element of REAL
(Re ((Im A) . x)) ^2 is complex real ext-real Element of REAL
Im ((Im A) . x) is complex real ext-real Element of REAL
(Im ((Im A) . x)) ^2 is complex real ext-real Element of REAL
((Re ((Im A) . x)) ^2) + ((Im ((Im A) . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((Im A) . x)) ^2) + ((Im ((Im A) . x)) ^2)) is complex real ext-real Element of REAL
|.((Im A) . x).| to_power 2 is complex real ext-real Element of REAL
Im (A . x) is complex real ext-real Element of REAL
|.(Im (A . x)).| is complex real ext-real Element of REAL
Re (Im (A . x)) is complex real ext-real Element of REAL
(Re (Im (A . x))) ^2 is complex real ext-real Element of REAL
Im (Im (A . x)) is complex real ext-real Element of REAL
(Im (Im (A . x))) ^2 is complex real ext-real Element of REAL
((Re (Im (A . x))) ^2) + ((Im (Im (A . x))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (Im (A . x))) ^2) + ((Im (Im (A . x))) ^2)) is complex real ext-real Element of REAL
|.(Im (A . x)).| to_power 2 is complex real ext-real Element of REAL
|.(Im (A . x)).| ^2 is complex real ext-real Element of REAL
(Im (A . x)) ^2 is complex real ext-real Element of REAL
((2,X,|.(Re A).|) + (2,X,|.(Im A).|)) . x is complex real ext-real Element of REAL
(((2,X,|.(Re A).|) + (2,X,|.(Im A).|)) . x) to_power (1 / 2) is complex real ext-real Element of REAL
sqrt (((2,X,|.(Re A).|) + (2,X,|.(Im A).|)) . x) is complex real ext-real Element of REAL
((Re (A . x)) ^2) + ((Im (A . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (A . x)) ^2) + ((Im (A . x)) ^2)) is complex real ext-real Element of REAL
((1 / 2),X,((2,X,|.(Re A).|) + (2,X,|.(Im A).|))) . x is complex real ext-real Element of REAL
|.(A . x).| is complex real ext-real Element of REAL
|.A.| . x is complex real ext-real Element of 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))
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)
|.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))
|.(Re f).| is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
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 X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
|.(Re f).| + |.(Im f).| is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
dom (|.(Re f).| + |.(Im f).|) is Element of K6(X)
dom |.(Re f).| is Element of K6(X)
dom |.(Im f).| is Element of K6(X)
(dom |.(Re f).|) /\ (dom |.(Im f).|) is Element of K6(X)
dom (Re f) is Element of K6(X)
dom (Im f) is Element of K6(X)
dom |.f.| is Element of K6(X)
a is Element of S
a is Element of S
x is Element of X
|.f.| . x is complex real ext-real Element of REAL
f . x is complex set
|.(f . x).| is complex real ext-real Element of REAL
Re (f . x) is complex real ext-real Element of REAL
(Re (f . x)) ^2 is complex real ext-real Element of REAL
Im (f . x) is complex real ext-real Element of REAL
(Im (f . x)) ^2 is complex real ext-real Element of REAL
((Re (f . x)) ^2) + ((Im (f . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (f . x)) ^2) + ((Im (f . x)) ^2)) is complex real ext-real Element of REAL
(Im f) . x is complex real ext-real Element of REAL
|.((Im f) . x).| is complex real ext-real Element of REAL
Re ((Im f) . x) is complex real ext-real Element of REAL
(Re ((Im f) . x)) ^2 is complex real ext-real Element of REAL
Im ((Im f) . x) is complex real ext-real Element of REAL
(Im ((Im f) . x)) ^2 is complex real ext-real Element of REAL
((Re ((Im f) . x)) ^2) + ((Im ((Im f) . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((Im f) . x)) ^2) + ((Im ((Im f) . x)) ^2)) is complex real ext-real Element of REAL
|.(Im f).| . x is complex real ext-real Element of REAL
(Re f) . x is complex real ext-real Element of REAL
|.((Re f) . x).| is complex real ext-real Element of REAL
Re ((Re f) . x) is complex real ext-real Element of REAL
(Re ((Re f) . x)) ^2 is complex real ext-real Element of REAL
Im ((Re f) . x) is complex real ext-real Element of REAL
(Im ((Re f) . x)) ^2 is complex real ext-real Element of REAL
((Re ((Re f) . x)) ^2) + ((Im ((Re f) . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((Re f) . x)) ^2) + ((Im ((Re f) . x)) ^2)) is complex real ext-real Element of REAL
|.(Re f).| . x is complex real ext-real Element of REAL
(|.(Re f).| + |.(Im f).|) . x is complex real ext-real Element of REAL
(|.(Re f).| . x) + (|.(Im f).| . x) is complex real ext-real Element of REAL
|.(|.f.| . x).| is complex real ext-real Element of REAL
Re (|.f.| . x) is complex real ext-real Element of REAL
(Re (|.f.| . x)) ^2 is complex real ext-real Element of REAL
Im (|.f.| . x) is complex real ext-real Element of REAL
(Im (|.f.| . x)) ^2 is complex real ext-real Element of REAL
((Re (|.f.| . x)) ^2) + ((Im (|.f.| . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (|.f.| . x)) ^2) + ((Im (|.f.| . x)) ^2)) is complex real ext-real Element of REAL
x is Element of X
f . x is complex set
Im (f . x) is complex real ext-real Element of REAL
|.(Im (f . x)).| is complex real ext-real Element of REAL
Re (Im (f . x)) is complex real ext-real Element of REAL
(Re (Im (f . x))) ^2 is complex real ext-real Element of REAL
Im (Im (f . x)) is complex real ext-real Element of REAL
(Im (Im (f . x))) ^2 is complex real ext-real Element of REAL
((Re (Im (f . x))) ^2) + ((Im (Im (f . x))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (Im (f . x))) ^2) + ((Im (Im (f . x))) ^2)) is complex real ext-real Element of REAL
|.(f . x).| is complex real ext-real Element of REAL
Re (f . x) is complex real ext-real Element of REAL
(Re (f . x)) ^2 is complex real ext-real Element of REAL
(Im (f . x)) ^2 is complex real ext-real Element of REAL
((Re (f . x)) ^2) + ((Im (f . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (f . x)) ^2) + ((Im (f . x)) ^2)) is complex real ext-real Element of REAL
|.f.| . x is complex real ext-real Element of REAL
(Im f) . x is complex real ext-real Element of REAL
|.((Im f) . x).| is complex real ext-real Element of REAL
Re ((Im f) . x) is complex real ext-real Element of REAL
(Re ((Im f) . x)) ^2 is complex real ext-real Element of REAL
Im ((Im f) . x) is complex real ext-real Element of REAL
(Im ((Im f) . x)) ^2 is complex real ext-real Element of REAL
((Re ((Im f) . x)) ^2) + ((Im ((Im f) . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((Im f) . x)) ^2) + ((Im ((Im f) . x)) ^2)) is complex real ext-real Element of REAL
x is Element of X
f . x is complex set
Re (f . x) is complex real ext-real Element of REAL
|.(Re (f . x)).| is complex real ext-real Element of REAL
Re (Re (f . x)) is complex real ext-real Element of REAL
(Re (Re (f . x))) ^2 is complex real ext-real Element of REAL
Im (Re (f . x)) is complex real ext-real Element of REAL
(Im (Re (f . x))) ^2 is complex real ext-real Element of REAL
((Re (Re (f . x))) ^2) + ((Im (Re (f . x))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (Re (f . x))) ^2) + ((Im (Re (f . x))) ^2)) is complex real ext-real Element of REAL
|.(f . x).| is complex real ext-real Element of REAL
(Re (f . x)) ^2 is complex real ext-real Element of REAL
Im (f . x) is complex real ext-real Element of REAL
(Im (f . x)) ^2 is complex real ext-real Element of REAL
((Re (f . x)) ^2) + ((Im (f . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (f . x)) ^2) + ((Im (f . x)) ^2)) is complex real ext-real Element of REAL
|.f.| . x is complex real ext-real Element of REAL
(Re f) . x is complex real ext-real Element of REAL
|.((Re f) . x).| is complex real ext-real Element of REAL
Re ((Re f) . x) is complex real ext-real Element of REAL
(Re ((Re f) . x)) ^2 is complex real ext-real Element of REAL
Im ((Re f) . x) is complex real ext-real Element of REAL
(Im ((Re f) . x)) ^2 is complex real ext-real Element of REAL
((Re ((Re f) . x)) ^2) + ((Im ((Re f) . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((Re f) . x)) ^2) + ((Im ((Re f) . x)) ^2)) is complex real ext-real Element of 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))
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))
a is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
f + a is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
dom (f + a) is Element of K6(X)
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))
Im f 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 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)
Im (f + a) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
dom (Im (f + a)) is Element of K6(X)
Re f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
(Re f) + (Re a) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
dom ((Re f) + (Re a)) 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))
dom (Re (f + a)) is Element of K6(X)
<i> (#) (Im (f + a)) is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
dom (<i> (#) (Im (f + a))) is Element of K6(X)
(Re (f + a)) + (<i> (#) (Im (f + a))) is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
dom ((Re (f + a)) + (<i> (#) (Im (f + a)))) is Element of K6(X)
(dom (Re (f + a))) /\ (dom (Im (f + 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))
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))
a is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
f + a is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
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
Im f 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 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))
Re 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))
(Re f) + (Re 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 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,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))
a is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
f - a is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
- 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
f + (- a) is Relation-like Function-like set
R_EAL 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
(- 1) (#) (R_EAL a) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
- (R_EAL a) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
- a is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
R_EAL (- a) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
R_EAL f is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
(R_EAL f) + (R_EAL (- a)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
R_EAL (f - a) 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))
a is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
f - 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
f + (- a) is Relation-like Function-like set
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
Im f 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 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 f) + (- (Im a)) is Relation-like Function-like set
Im (f - 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 f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
(Re f) - (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 f) + (- (Re 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))
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 Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
dom a is Element of K6(X)
(dom f) /\ (dom a) is Element of K6(X)
f + a is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,(f + a)) is complex set
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
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 (Re a) is Element of K6(X)
(dom (Re f)) /\ (dom (Re 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))
Integral (A,((Re f) + (Re a))) is ext-real Element of ExtREAL
R_EAL ((Re f) + (Re 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 ((Re f) + (Re a)))) is ext-real Element of ExtREAL
max+ (R_EAL ((Re f) + (Re a))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Re f) + (Re a))))) is ext-real Element of ExtREAL
max- (R_EAL ((Re f) + (Re a))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Re f) + (Re a))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Re f) + (Re a)))))) - (integral+ (A,(max- (R_EAL ((Re f) + (Re a)))))) is ext-real Element of ExtREAL
x is Element of S
(Re f) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,((Re f) | x)) is ext-real Element of ExtREAL
R_EAL ((Re f) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Re f) | x))) is ext-real Element of ExtREAL
max+ (R_EAL ((Re f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Re f) | x)))) is ext-real Element of ExtREAL
max- (R_EAL ((Re f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Re f) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Re f) | x))))) - (integral+ (A,(max- (R_EAL ((Re f) | x))))) is ext-real Element of ExtREAL
(Re a) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,((Re a) | x)) is ext-real Element of ExtREAL
R_EAL ((Re a) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Re a) | x))) is ext-real Element of ExtREAL
max+ (R_EAL ((Re a) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Re a) | x)))) is ext-real Element of ExtREAL
max- (R_EAL ((Re a) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Re a) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Re a) | x))))) - (integral+ (A,(max- (R_EAL ((Re a) | x))))) is ext-real Element of ExtREAL
(Integral (A,((Re f) | x))) + (Integral (A,((Re a) | x))) is ext-real Element of ExtREAL
f | x is Relation-like X -defined x -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
Re (f | x) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Re (f | x))) is ext-real Element of ExtREAL
R_EAL (Re (f | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Re (f | x)))) is ext-real Element of ExtREAL
max+ (R_EAL (Re (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Re (f | x))))) is ext-real Element of ExtREAL
max- (R_EAL (Re (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Re (f | x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Re (f | x)))))) - (integral+ (A,(max- (R_EAL (Re (f | x)))))) is ext-real Element of ExtREAL
Im (f | x) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Im (f | x))) is ext-real Element of ExtREAL
R_EAL (Im (f | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Im (f | x)))) is ext-real Element of ExtREAL
max+ (R_EAL (Im (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Im (f | x))))) is ext-real Element of ExtREAL
max- (R_EAL (Im (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Im (f | x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Im (f | x)))))) - (integral+ (A,(max- (R_EAL (Im (f | x)))))) is ext-real Element of ExtREAL
Im a is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Im f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
dom (Im f) is Element of K6(X)
dom (Im a) is Element of K6(X)
(dom (Im f)) /\ (dom (Im a)) is Element of K6(X)
(Im f) + (Im a) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,((Im f) + (Im a))) is ext-real Element of ExtREAL
R_EAL ((Im f) + (Im a)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Im f) + (Im a)))) is ext-real Element of ExtREAL
max+ (R_EAL ((Im f) + (Im a))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Im f) + (Im a))))) is ext-real Element of ExtREAL
max- (R_EAL ((Im f) + (Im a))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Im f) + (Im a))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Im f) + (Im a)))))) - (integral+ (A,(max- (R_EAL ((Im f) + (Im 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))
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
Re (f + a) is Relation-like 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
R2 is complex real ext-real Element of REAL
I2 is complex real ext-real Element of REAL
I2 * <i> is complex set
R2 + (I2 * <i>) is complex set
a | x is Relation-like X -defined x -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
Re (a | x) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Re (a | x))) is ext-real Element of ExtREAL
R_EAL (Re (a | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Re (a | x)))) is ext-real Element of ExtREAL
max+ (R_EAL (Re (a | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Re (a | x))))) is ext-real Element of ExtREAL
max- (R_EAL (Re (a | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Re (a | x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Re (a | x)))))) - (integral+ (A,(max- (R_EAL (Re (a | x)))))) is ext-real Element of ExtREAL
Im (a | x) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Im (a | x))) is ext-real Element of ExtREAL
R_EAL (Im (a | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Im (a | x)))) is ext-real Element of ExtREAL
max+ (R_EAL (Im (a | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Im (a | x))))) is ext-real Element of ExtREAL
max- (R_EAL (Im (a | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Im (a | x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Im (a | x)))))) - (integral+ (A,(max- (R_EAL (Im (a | x)))))) is ext-real Element of ExtREAL
(Integral (A,(Re (f | x)))) + (Integral (A,((Re a) | x))) is ext-real Element of ExtREAL
(Integral (A,(Re (f | x)))) + (Integral (A,(Re (a | x)))) is ext-real Element of ExtREAL
x is complex real ext-real Element of REAL
R is complex real ext-real Element of REAL
x + R is complex real ext-real Element of REAL
(Im a) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,((Im a) | x)) is ext-real Element of ExtREAL
R_EAL ((Im a) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Im a) | x))) is ext-real Element of ExtREAL
max+ (R_EAL ((Im a) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Im a) | x)))) is ext-real Element of ExtREAL
max- (R_EAL ((Im a) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Im a) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Im a) | x))))) - (integral+ (A,(max- (R_EAL ((Im a) | x))))) is ext-real Element of ExtREAL
(Integral (A,(Im (f | x)))) + (Integral (A,((Im a) | x))) is ext-real Element of ExtREAL
E is Element of S
(Im f) | E is Relation-like X -defined E -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,((Im f) | E)) is ext-real Element of ExtREAL
R_EAL ((Im f) | E) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Im f) | E))) is ext-real Element of ExtREAL
max+ (R_EAL ((Im f) | E)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Im f) | E)))) is ext-real Element of ExtREAL
max- (R_EAL ((Im f) | E)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Im f) | E)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Im f) | E))))) - (integral+ (A,(max- (R_EAL ((Im f) | E))))) is ext-real Element of ExtREAL
(Im a) | E is Relation-like X -defined E -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,((Im a) | E)) is ext-real Element of ExtREAL
R_EAL ((Im a) | E) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Im a) | E))) is ext-real Element of ExtREAL
max+ (R_EAL ((Im a) | E)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Im a) | E)))) is ext-real Element of ExtREAL
max- (R_EAL ((Im a) | E)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Im a) | E)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Im a) | E))))) - (integral+ (A,(max- (R_EAL ((Im a) | E))))) is ext-real Element of ExtREAL
(Integral (A,((Im f) | E))) + (Integral (A,((Im a) | E))) is ext-real Element of ExtREAL
R_EAL I2 is ext-real Element of ExtREAL
I1 is complex real ext-real Element of REAL
R_EAL I1 is ext-real Element of ExtREAL
I is complex real ext-real Element of REAL
R_EAL I is ext-real Element of ExtREAL
(R_EAL I1) + (R_EAL I) is ext-real Element of ExtREAL
I1 + I is complex real ext-real Element of REAL
I1 * <i> is complex set
x + (I1 * <i>) is complex set
I * <i> is complex set
R + (I * <i>) is complex set
(x + (I1 * <i>)) + (R + (I * <i>)) is complex set
(X,S,A,(f | x)) is complex set
(X,S,A,(f | x)) + (R + (I * <i>)) is complex set
(X,S,A,(a | x)) is complex set
(X,S,A,(f | x)) + (X,S,A,(a | x)) is complex set
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))
a 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)
dom a is Element of K6(X)
(dom f) /\ (dom a) is Element of K6(X)
f - a is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
- 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
f + (- a) is Relation-like Function-like set
Integral (A,(f - a)) is ext-real Element of ExtREAL
R_EAL (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 (f - a))) is ext-real Element of ExtREAL
max+ (R_EAL (f - a)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (f - a)))) is ext-real Element of ExtREAL
max- (R_EAL (f - a)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (f - a)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (f - a))))) - (integral+ (A,(max- (R_EAL (f - a))))) is ext-real Element of ExtREAL
- a is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
R_EAL a is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
(- 1) (#) (R_EAL a) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
- (R_EAL a) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
R_EAL (- a) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
R_EAL f is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
dom (R_EAL f) is Element of K6(X)
dom (R_EAL (- a)) is Element of K6(X)
(dom (R_EAL f)) /\ (dom (R_EAL (- a))) is Element of K6(X)
(R_EAL f) + (R_EAL (- a)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,((R_EAL f) + (R_EAL (- a)))) is ext-real Element of ExtREAL
max+ ((R_EAL f) + (R_EAL (- a))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ ((R_EAL f) + (R_EAL (- a))))) is ext-real Element of ExtREAL
max- ((R_EAL f) + (R_EAL (- a))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- ((R_EAL f) + (R_EAL (- a))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ ((R_EAL f) + (R_EAL (- a)))))) - (integral+ (A,(max- ((R_EAL f) + (R_EAL (- a)))))) is ext-real Element of ExtREAL
x is Element of S
(R_EAL f) | x is Relation-like X -defined x -defined X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,((R_EAL f) | x)) is ext-real Element of ExtREAL
max+ ((R_EAL f) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ ((R_EAL f) | x))) is ext-real Element of ExtREAL
max- ((R_EAL f) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- ((R_EAL f) | x))) is ext-real Element of ExtREAL
(integral+ (A,(max+ ((R_EAL f) | x)))) - (integral+ (A,(max- ((R_EAL f) | x)))) is ext-real Element of ExtREAL
(R_EAL (- a)) | x is Relation-like X -defined x -defined X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,((R_EAL (- a)) | x)) is ext-real Element of ExtREAL
max+ ((R_EAL (- a)) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ ((R_EAL (- a)) | x))) is ext-real Element of ExtREAL
max- ((R_EAL (- a)) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- ((R_EAL (- a)) | x))) is ext-real Element of ExtREAL
(integral+ (A,(max+ ((R_EAL (- a)) | x)))) - (integral+ (A,(max- ((R_EAL (- a)) | x)))) is ext-real Element of ExtREAL
(Integral (A,((R_EAL f) | x))) + (Integral (A,((R_EAL (- 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))
Integral (A,(f | x)) is ext-real Element of ExtREAL
R_EAL (f | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (f | x))) is ext-real Element of ExtREAL
max+ (R_EAL (f | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (f | x)))) is ext-real Element of ExtREAL
max- (R_EAL (f | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (f | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (f | x))))) - (integral+ (A,(max- (R_EAL (f | x))))) is ext-real Element of ExtREAL
(- a) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,((- a) | x)) is ext-real Element of ExtREAL
R_EAL ((- a) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((- a) | x))) is ext-real Element of ExtREAL
max+ (R_EAL ((- a) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((- a) | x)))) is ext-real Element of ExtREAL
max- (R_EAL ((- a) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((- a) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((- a) | x))))) - (integral+ (A,(max- (R_EAL ((- a) | x))))) is ext-real Element of ExtREAL
(Integral (A,(f | x))) + (Integral (A,((- a) | x))) is ext-real Element of ExtREAL
dom (- (R_EAL 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))
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))
(X,S,A,f) is complex set
a is complex real ext-real Element of REAL
a (#) f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,(a (#) f)) is complex set
a * (X,S,A,f) 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
a (#) (Re f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(a (#) (Re f))) is ext-real Element of ExtREAL
R_EAL (a (#) (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 (a (#) (Re f)))) is ext-real Element of ExtREAL
max+ (R_EAL (a (#) (Re f))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (a (#) (Re f))))) is ext-real Element of ExtREAL
max- (R_EAL (a (#) (Re f))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (a (#) (Re f))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (a (#) (Re f)))))) - (integral+ (A,(max- (R_EAL (a (#) (Re f)))))) is ext-real Element of ExtREAL
Re (a (#) f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Re (a (#) f))) is ext-real Element of ExtREAL
R_EAL (Re (a (#) f)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Re (a (#) f)))) is ext-real Element of ExtREAL
max+ (R_EAL (Re (a (#) f))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Re (a (#) f))))) is ext-real Element of ExtREAL
max- (R_EAL (Re (a (#) f))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Re (a (#) f))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Re (a (#) f)))))) - (integral+ (A,(max- (R_EAL (Re (a (#) 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))
a (#) (Im f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(a (#) (Im f))) is ext-real Element of ExtREAL
R_EAL (a (#) (Im f)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (a (#) (Im f)))) is ext-real Element of ExtREAL
max+ (R_EAL (a (#) (Im f))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (a (#) (Im f))))) is ext-real Element of ExtREAL
max- (R_EAL (a (#) (Im f))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (a (#) (Im f))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (a (#) (Im f)))))) - (integral+ (A,(max- (R_EAL (a (#) (Im f)))))) is ext-real Element of ExtREAL
Im (a (#) f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Im (a (#) f))) is ext-real Element of ExtREAL
R_EAL (Im (a (#) f)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Im (a (#) f)))) is ext-real Element of ExtREAL
max+ (R_EAL (Im (a (#) f))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Im (a (#) f))))) is ext-real Element of ExtREAL
max- (R_EAL (Im (a (#) f))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Im (a (#) f))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Im (a (#) f)))))) - (integral+ (A,(max- (R_EAL (Im (a (#) f)))))) is ext-real Element of ExtREAL
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))
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
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
R_EAL a is ext-real Element of ExtREAL
x is complex real ext-real Element of REAL
R_EAL x is ext-real Element of ExtREAL
(R_EAL a) * (R_EAL x) is ext-real Element of ExtREAL
a * x is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
R_EAL x is ext-real Element of ExtREAL
(R_EAL a) * (R_EAL x) is ext-real Element of ExtREAL
a * x is complex real ext-real Element of REAL
(R_EAL a) * (Integral (A,(Im f))) is ext-real Element of ExtREAL
(R_EAL a) * (Integral (A,(Re f))) 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 * <i> is complex set
x + (x * <i>) is complex set
a * (x + (x * <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))
<i> (#) f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,(<i> (#) f)) is complex set
(X,S,A,f) is complex set
<i> * (X,S,A,f) is complex set
Re (<i> (#) 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 f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
- (Im f) 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 f) is Relation-like Function-like set
Im (<i> (#) 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))
(- 1) (#) (Im f) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Re (<i> (#) f))) is ext-real Element of ExtREAL
R_EAL (Re (<i> (#) 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 (<i> (#) f)))) is ext-real Element of ExtREAL
max+ (R_EAL (Re (<i> (#) f))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Re (<i> (#) f))))) is ext-real Element of ExtREAL
max- (R_EAL (Re (<i> (#) f))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Re (<i> (#) f))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Re (<i> (#) f)))))) - (integral+ (A,(max- (R_EAL (Re (<i> (#) f)))))) is ext-real Element of ExtREAL
Integral (A,(Im (<i> (#) f))) is ext-real Element of ExtREAL
R_EAL (Im (<i> (#) f)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Im (<i> (#) f)))) is ext-real Element of ExtREAL
max+ (R_EAL (Im (<i> (#) f))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Im (<i> (#) f))))) is ext-real Element of ExtREAL
max- (R_EAL (Im (<i> (#) f))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Im (<i> (#) f))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Im (<i> (#) f)))))) - (integral+ (A,(max- (R_EAL (Im (<i> (#) 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
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))
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
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
x is complex real ext-real Element of REAL
I1 is complex real ext-real Element of REAL
I1 * <i> is complex set
x + (I1 * <i>) is complex set
R_EAL (- 1) is ext-real Element of ExtREAL
R_EAL I1 is ext-real Element of ExtREAL
(R_EAL (- 1)) * (R_EAL I1) is ext-real Element of ExtREAL
(- 1) * I1 is complex real ext-real Element of 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))
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))
(X,S,A,f) is complex set
a is complex set
a (#) f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,(a (#) f)) is complex set
a * (X,S,A,f) is complex set
Re a is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
(Im a) * <i> is complex set
(Re a) + ((Im a) * <i>) is complex set
<i> (#) f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
dom (<i> (#) f) is Element of K6(X)
dom f is Element of K6(X)
(Re a) (#) f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,((Re a) (#) f)) is complex set
(Re a) * (X,S,A,f) is complex set
(Im a) (#) (<i> (#) f) is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
dom ((Re a) (#) f) is Element of K6(X)
dom ((Im a) (#) (<i> (#) f)) is Element of K6(X)
(dom ((Re a) (#) f)) /\ (dom ((Im a) (#) (<i> (#) f))) is Element of K6(X)
((Re a) (#) f) + ((Im a) (#) (<i> (#) f)) is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,(((Re a) (#) f) + ((Im a) (#) (<i> (#) f)))) is complex set
x is Element of S
((Re a) (#) f) | x is Relation-like X -defined x -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,(((Re a) (#) f) | x)) is complex set
((Im a) (#) (<i> (#) f)) | x is Relation-like X -defined x -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,(((Im a) (#) (<i> (#) f)) | x)) is complex set
(X,S,A,(((Re a) (#) f) | x)) + (X,S,A,(((Im a) (#) (<i> (#) f)) | x)) is complex set
dom (a (#) f) is Element of K6(X)
(X,S,A,((Im a) (#) (<i> (#) f))) is complex set
(X,S,A,(<i> (#) f)) is complex set
(Im a) * (X,S,A,(<i> (#) f)) is complex set
dom (((Re a) (#) f) + ((Im a) (#) (<i> (#) f))) is Element of K6(X)
x is Element of X
(a (#) f) . x is complex set
f . x is complex set
a * (f . x) is complex set
((Im a) (#) (<i> (#) f)) . x is complex set
(<i> (#) f) . x is complex set
(Im a) * ((<i> (#) f) . x) is complex set
((Re a) (#) f) . x is complex set
(Re a) * (f . x) is complex set
<i> * (f . x) is complex set
(((Re a) (#) f) + ((Im a) (#) (<i> (#) f))) . x is complex set
(((Re a) (#) f) . x) + (((Im a) (#) (<i> (#) f)) . x) is complex set
<i> * (X,S,A,f) is complex set
((Im a) * <i>) * (X,S,A,f) is complex set
((Re a) * (X,S,A,f)) + (((Im a) * <i>) * (X,S,A,f)) 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
|.(X,S,A,f).| is complex real ext-real Element of REAL
Re (X,S,A,f) is complex real ext-real Element of REAL
(Re (X,S,A,f)) ^2 is complex real ext-real Element of REAL
Im (X,S,A,f) is complex real ext-real Element of REAL
(Im (X,S,A,f)) ^2 is complex real ext-real Element of REAL
((Re (X,S,A,f)) ^2) + ((Im (X,S,A,f)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (X,S,A,f)) ^2) + ((Im (X,S,A,f)) ^2)) is complex real ext-real Element of REAL
|.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,|.f.|) is ext-real Element of ExtREAL
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
Integral (A,(R_EAL |.f.|)) is ext-real Element of ExtREAL
max+ (R_EAL |.f.|) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL |.f.|))) is ext-real Element of ExtREAL
max- (R_EAL |.f.|) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL |.f.|))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL |.f.|)))) - (integral+ (A,(max- (R_EAL |.f.|)))) is ext-real Element of ExtREAL
a is Element of S
Re f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
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))
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
|.(Integral (A,(Re f))).| is ext-real Element of ExtREAL
|.(Re f).| is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
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))
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
dom |.f.| is Element of K6(X)
x is Element of S
x is Element of S
dom (Re f) is Element of K6(X)
I1 is Element of X
(Re f) . I1 is complex real ext-real Element of REAL
f . I1 is complex set
Re (f . I1) is complex real ext-real Element of REAL
|.f.| . I1 is complex real ext-real Element of REAL
|.(f . I1).| is complex real ext-real Element of REAL
(Re (f . I1)) ^2 is complex real ext-real Element of REAL
Im (f . I1) is complex real ext-real Element of REAL
(Im (f . I1)) ^2 is complex real ext-real Element of REAL
((Re (f . I1)) ^2) + ((Im (f . I1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (f . I1)) ^2) + ((Im (f . I1)) ^2)) is complex real ext-real Element of REAL
|.((Re f) . I1).| is complex real ext-real Element of REAL
Re ((Re f) . I1) is complex real ext-real Element of REAL
(Re ((Re f) . I1)) ^2 is complex real ext-real Element of REAL
Im ((Re f) . I1) is complex real ext-real Element of REAL
(Im ((Re f) . I1)) ^2 is complex real ext-real Element of REAL
((Re ((Re f) . I1)) ^2) + ((Im ((Re f) . I1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((Re f) . I1)) ^2) + ((Im ((Re f) . I1)) ^2)) is complex real ext-real Element of REAL
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 Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
A is set
S | A is Relation-like X -defined A -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
f is complex real ext-real Element of REAL
f (#) S is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
(f (#) S) | A is Relation-like X -defined A -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
f (#) (S | A) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
dom ((f (#) S) | A) is Element of K6(X)
K6(X) is non empty set
dom (f (#) S) is Element of K6(X)
(dom (f (#) S)) /\ A is Element of K6(X)
dom S is Element of K6(X)
(dom S) /\ A is Element of K6(X)
dom (S | A) is Element of K6(X)
a is Element of X
dom (f (#) (S | A)) is Element of K6(X)
(f (#) (S | A)) . a is complex real ext-real Element of REAL
(S | A) . a is complex real ext-real Element of REAL
f * ((S | A) . a) is complex real ext-real Element of REAL
S . a is complex real ext-real Element of REAL
f * (S . a) is complex real ext-real Element of REAL
(f (#) S) . a is complex real ext-real Element of REAL
((f (#) S) | A) . a is complex real ext-real Element of REAL
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)
a is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
dom a is Element of K6(X)
(dom f) /\ (dom a) is Element of K6(X)
a - f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
- 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
(- 1) (#) f is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
dom ((- 1) (#) f) is Element of K6(X)
(dom ((- 1) (#) f)) /\ (dom a) is Element of K6(X)
((- 1) (#) f) + a is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(((- 1) (#) f) + a)) is ext-real Element of ExtREAL
R_EAL (((- 1) (#) 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 (((- 1) (#) f) + a))) is ext-real Element of ExtREAL
max+ (R_EAL (((- 1) (#) f) + a)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (((- 1) (#) f) + a)))) is ext-real Element of ExtREAL
max- (R_EAL (((- 1) (#) f) + a)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (((- 1) (#) f) + a)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (((- 1) (#) f) + a))))) - (integral+ (A,(max- (R_EAL (((- 1) (#) f) + a))))) is ext-real Element of ExtREAL
x is Element of S
((- 1) (#) f) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(((- 1) (#) f) | x)) is ext-real Element of ExtREAL
R_EAL (((- 1) (#) f) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (((- 1) (#) f) | x))) is ext-real Element of ExtREAL
max+ (R_EAL (((- 1) (#) f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (((- 1) (#) f) | x)))) is ext-real Element of ExtREAL
max- (R_EAL (((- 1) (#) f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (((- 1) (#) f) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (((- 1) (#) f) | x))))) - (integral+ (A,(max- (R_EAL (((- 1) (#) f) | x))))) is ext-real Element of ExtREAL
a | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(a | x)) is ext-real Element of ExtREAL
R_EAL (a | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (a | x))) is ext-real Element of ExtREAL
max+ (R_EAL (a | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (a | x)))) is ext-real Element of ExtREAL
max- (R_EAL (a | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (a | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (a | x))))) - (integral+ (A,(max- (R_EAL (a | x))))) is ext-real Element of ExtREAL
(Integral (A,(((- 1) (#) f) | x))) + (Integral (A,(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))
Integral (A,(f | x)) is ext-real Element of ExtREAL
R_EAL (f | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (f | x))) is ext-real Element of ExtREAL
max+ (R_EAL (f | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (f | x)))) is ext-real Element of ExtREAL
max- (R_EAL (f | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (f | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (f | x))))) - (integral+ (A,(max- (R_EAL (f | x))))) is ext-real Element of ExtREAL
R_EAL (- 1) is ext-real Element of ExtREAL
(R_EAL (- 1)) * (Integral (A,(f | x))) is ext-real Element of ExtREAL
I1 is complex real ext-real Element of REAL
(- 1) * I1 is complex real ext-real Element of REAL
(- 1) (#) (f | x) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
I2 is Element of S
I2 is Element of S
dom (((- 1) (#) f) + a) is Element of K6(X)
((R_EAL (- 1)) * (Integral (A,(f | x)))) + (Integral (A,(a | x))) is ext-real Element of ExtREAL
- I1 is complex real ext-real Element of REAL
R2 is complex real ext-real Element of REAL
(- I1) + R2 is complex real ext-real Element of REAL
0 + I1 is complex real ext-real Element of REAL
((- I1) + R2) + I1 is complex real ext-real Element of 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))
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
|.(X,S,A,f).| is complex real ext-real Element of REAL
Re (X,S,A,f) is complex real ext-real Element of REAL
(Re (X,S,A,f)) ^2 is complex real ext-real Element of REAL
Im (X,S,A,f) is complex real ext-real Element of REAL
(Im (X,S,A,f)) ^2 is complex real ext-real Element of REAL
((Re (X,S,A,f)) ^2) + ((Im (X,S,A,f)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (X,S,A,f)) ^2) + ((Im (X,S,A,f)) ^2)) is complex real ext-real Element of REAL
|.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,|.f.|) is ext-real Element of ExtREAL
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
Integral (A,(R_EAL |.f.|)) is ext-real Element of ExtREAL
max+ (R_EAL |.f.|) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL |.f.|))) is ext-real Element of ExtREAL
max- (R_EAL |.f.|) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL |.f.|))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL |.f.|)))) - (integral+ (A,(max- (R_EAL |.f.|)))) is ext-real Element of ExtREAL
a is Element of S
|.(X,S,A,f).| / |.(X,S,A,f).| is complex real ext-real Element of REAL
|.(X,S,A,f).| " is complex real ext-real set
|.(X,S,A,f).| * (|.(X,S,A,f).| ") is complex real ext-real set
|.f.| " is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
f (#) (|.f.| ") is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,f) / |.(X,S,A,f).| is complex Element of COMPLEX
(X,S,A,f) * (|.(X,S,A,f).| ") is complex set
dom |.f.| is Element of K6(X)
|.((X,S,A,f) / |.(X,S,A,f).|).| is complex real ext-real Element of REAL
Re ((X,S,A,f) / |.(X,S,A,f).|) is complex real ext-real Element of REAL
(Re ((X,S,A,f) / |.(X,S,A,f).|)) ^2 is complex real ext-real Element of REAL
Im ((X,S,A,f) / |.(X,S,A,f).|) is complex real ext-real Element of REAL
(Im ((X,S,A,f) / |.(X,S,A,f).|)) ^2 is complex real ext-real Element of REAL
((Re ((X,S,A,f) / |.(X,S,A,f).|)) ^2) + ((Im ((X,S,A,f) / |.(X,S,A,f).|)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((X,S,A,f) / |.(X,S,A,f).|)) ^2) + ((Im ((X,S,A,f) / |.(X,S,A,f).|)) ^2)) is complex real ext-real Element of REAL
((X,S,A,f) / |.(X,S,A,f).|) *' is complex Element of COMPLEX
(Im ((X,S,A,f) / |.(X,S,A,f).|)) * <i> is complex set
(Re ((X,S,A,f) / |.(X,S,A,f).|)) - ((Im ((X,S,A,f) / |.(X,S,A,f).|)) * <i>) is complex set
- ((Im ((X,S,A,f) / |.(X,S,A,f).|)) * <i>) is complex set
(Re ((X,S,A,f) / |.(X,S,A,f).|)) + (- ((Im ((X,S,A,f) / |.(X,S,A,f).|)) * <i>)) is complex set
|.(((X,S,A,f) / |.(X,S,A,f).|) *').| is complex real ext-real Element of REAL
Re (((X,S,A,f) / |.(X,S,A,f).|) *') is complex real ext-real Element of REAL
(Re (((X,S,A,f) / |.(X,S,A,f).|) *')) ^2 is complex real ext-real Element of REAL
Im (((X,S,A,f) / |.(X,S,A,f).|) *') is complex real ext-real Element of REAL
(Im (((X,S,A,f) / |.(X,S,A,f).|) *')) ^2 is complex real ext-real Element of REAL
((Re (((X,S,A,f) / |.(X,S,A,f).|) *')) ^2) + ((Im (((X,S,A,f) / |.(X,S,A,f).|) *')) ^2) is complex real ext-real Element of REAL
sqrt (((Re (((X,S,A,f) / |.(X,S,A,f).|) *')) ^2) + ((Im (((X,S,A,f) / |.(X,S,A,f).|) *')) ^2)) is complex real ext-real Element of REAL
|.((X,S,A,f) / |.(X,S,A,f).|).| * |.(((X,S,A,f) / |.(X,S,A,f).|) *').| is complex real ext-real Element of REAL
((X,S,A,f) / |.(X,S,A,f).|) * (((X,S,A,f) / |.(X,S,A,f).|) *') is complex Element of COMPLEX
|.(((X,S,A,f) / |.(X,S,A,f).|) * (((X,S,A,f) / |.(X,S,A,f).|) *')).| is complex real ext-real Element of REAL
Re (((X,S,A,f) / |.(X,S,A,f).|) * (((X,S,A,f) / |.(X,S,A,f).|) *')) is complex real ext-real Element of REAL
(Re (((X,S,A,f) / |.(X,S,A,f).|) * (((X,S,A,f) / |.(X,S,A,f).|) *'))) ^2 is complex real ext-real Element of REAL
Im (((X,S,A,f) / |.(X,S,A,f).|) * (((X,S,A,f) / |.(X,S,A,f).|) *')) is complex real ext-real Element of REAL
(Im (((X,S,A,f) / |.(X,S,A,f).|) * (((X,S,A,f) / |.(X,S,A,f).|) *'))) ^2 is complex real ext-real Element of REAL
((Re (((X,S,A,f) / |.(X,S,A,f).|) * (((X,S,A,f) / |.(X,S,A,f).|) *'))) ^2) + ((Im (((X,S,A,f) / |.(X,S,A,f).|) * (((X,S,A,f) / |.(X,S,A,f).|) *'))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (((X,S,A,f) / |.(X,S,A,f).|) * (((X,S,A,f) / |.(X,S,A,f).|) *'))) ^2) + ((Im (((X,S,A,f) / |.(X,S,A,f).|) * (((X,S,A,f) / |.(X,S,A,f).|) *'))) ^2)) is complex real ext-real Element of REAL
((X,S,A,f) / |.(X,S,A,f).|) * ((X,S,A,f) / |.(X,S,A,f).|) is complex Element of COMPLEX
|.(((X,S,A,f) / |.(X,S,A,f).|) * ((X,S,A,f) / |.(X,S,A,f).|)).| is complex real ext-real Element of REAL
Re (((X,S,A,f) / |.(X,S,A,f).|) * ((X,S,A,f) / |.(X,S,A,f).|)) is complex real ext-real Element of REAL
(Re (((X,S,A,f) / |.(X,S,A,f).|) * ((X,S,A,f) / |.(X,S,A,f).|))) ^2 is complex real ext-real Element of REAL
Im (((X,S,A,f) / |.(X,S,A,f).|) * ((X,S,A,f) / |.(X,S,A,f).|)) is complex real ext-real Element of REAL
(Im (((X,S,A,f) / |.(X,S,A,f).|) * ((X,S,A,f) / |.(X,S,A,f).|))) ^2 is complex real ext-real Element of REAL
((Re (((X,S,A,f) / |.(X,S,A,f).|) * ((X,S,A,f) / |.(X,S,A,f).|))) ^2) + ((Im (((X,S,A,f) / |.(X,S,A,f).|) * ((X,S,A,f) / |.(X,S,A,f).|))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (((X,S,A,f) / |.(X,S,A,f).|) * ((X,S,A,f) / |.(X,S,A,f).|))) ^2) + ((Im (((X,S,A,f) / |.(X,S,A,f).|) * ((X,S,A,f) / |.(X,S,A,f).|))) ^2)) is complex real ext-real Element of REAL
|.((X,S,A,f) / |.(X,S,A,f).|).| * |.((X,S,A,f) / |.(X,S,A,f).|).| is complex real ext-real Element of REAL
f /" |.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
f (#) (|.f.| ") is Relation-like Function-like set
dom (f (#) (|.f.| ")) is Element of K6(X)
(dom f) /\ (dom |.f.|) is Element of K6(X)
(((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")) is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
dom ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) is Element of K6(X)
|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
dom (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) is Element of K6(X)
(dom f) /\ (dom f) is Element of K6(X)
Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
dom (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) is Element of K6(X)
|.f.| (#) (f (#) (|.f.| ")) is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
dom (|.f.| (#) (f (#) (|.f.| "))) is Element of K6(X)
(dom |.f.|) /\ (dom (f (#) (|.f.| "))) is Element of K6(X)
(((X,S,A,f) / |.(X,S,A,f).|) *') (#) (|.f.| (#) (f (#) (|.f.| "))) is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
dom ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) is Element of K6(X)
I1 is set
(|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1 is complex set
|.f.| . I1 is complex real ext-real Element of REAL
((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1 is complex set
(|.f.| . I1) * (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1) is complex set
f . I1 is complex set
|.(f . I1).| is complex real ext-real Element of REAL
Re (f . I1) is complex real ext-real Element of REAL
(Re (f . I1)) ^2 is complex real ext-real Element of REAL
Im (f . I1) is complex real ext-real Element of REAL
(Im (f . I1)) ^2 is complex real ext-real Element of REAL
((Re (f . I1)) ^2) + ((Im (f . I1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (f . I1)) ^2) + ((Im (f . I1)) ^2)) is complex real ext-real Element of REAL
|.(f . I1).| * (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1) is complex set
(f (#) (|.f.| ")) . I1 is complex set
(((X,S,A,f) / |.(X,S,A,f).|) *') * ((f (#) (|.f.| ")) . I1) is complex set
((((X,S,A,f) / |.(X,S,A,f).|) *') * ((f (#) (|.f.| ")) . I1)) * |.(f . I1).| is complex set
((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . I1 is complex set
(|.f.| (#) (f (#) (|.f.| "))) . I1 is complex set
(((X,S,A,f) / |.(X,S,A,f).|) *') * ((|.f.| (#) (f (#) (|.f.| "))) . I1) is complex set
(|.f.| . I1) * ((f (#) (|.f.| ")) . I1) is complex set
(((X,S,A,f) / |.(X,S,A,f).|) *') * ((|.f.| . I1) * ((f (#) (|.f.| ")) . I1)) is complex set
|.(f . I1).| * ((f (#) (|.f.| ")) . I1) is complex set
(((X,S,A,f) / |.(X,S,A,f).|) *') * (|.(f . I1).| * ((f (#) (|.f.| ")) . I1)) is complex set
|.|.(X,S,A,f).|.| is complex real ext-real Element of REAL
Re |.(X,S,A,f).| is complex real ext-real Element of REAL
(Re |.(X,S,A,f).|) ^2 is complex real ext-real Element of REAL
Im |.(X,S,A,f).| is complex real ext-real Element of REAL
(Im |.(X,S,A,f).|) ^2 is complex real ext-real Element of REAL
((Re |.(X,S,A,f).|) ^2) + ((Im |.(X,S,A,f).|) ^2) is complex real ext-real Element of REAL
sqrt (((Re |.(X,S,A,f).|) ^2) + ((Im |.(X,S,A,f).|) ^2)) is complex real ext-real Element of REAL
|.(X,S,A,f).| / |.|.(X,S,A,f).|.| is complex real ext-real Element of REAL
|.|.(X,S,A,f).|.| " is complex real ext-real set
|.(X,S,A,f).| * (|.|.(X,S,A,f).|.| ") is complex real ext-real set
I1 is set
(f (#) (|.f.| ")) . I1 is complex set
f . I1 is complex set
|.f.| . I1 is complex real ext-real Element of REAL
(f . I1) / (|.f.| . I1) is complex Element of COMPLEX
(|.f.| . I1) " is complex real ext-real set
(f . I1) * ((|.f.| . I1) ") is complex set
(dom (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))))) /\ (dom |.f.|) is Element of K6(X)
|.(f . I1).| is complex real ext-real Element of REAL
Re (f . I1) is complex real ext-real Element of REAL
(Re (f . I1)) ^2 is complex real ext-real Element of REAL
Im (f . I1) is complex real ext-real Element of REAL
(Im (f . I1)) ^2 is complex real ext-real Element of REAL
((Re (f . I1)) ^2) + ((Im (f . I1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (f . I1)) ^2) + ((Im (f . I1)) ^2)) is complex real ext-real Element of REAL
|.((f (#) (|.f.| ")) . I1).| is complex real ext-real Element of REAL
Re ((f (#) (|.f.| ")) . I1) is complex real ext-real Element of REAL
(Re ((f (#) (|.f.| ")) . I1)) ^2 is complex real ext-real Element of REAL
Im ((f (#) (|.f.| ")) . I1) is complex real ext-real Element of REAL
(Im ((f (#) (|.f.| ")) . I1)) ^2 is complex real ext-real Element of REAL
((Re ((f (#) (|.f.| ")) . I1)) ^2) + ((Im ((f (#) (|.f.| ")) . I1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((f (#) (|.f.| ")) . I1)) ^2) + ((Im ((f (#) (|.f.| ")) . I1)) ^2)) is complex real ext-real Element of REAL
|.|.(f . I1).|.| is complex real ext-real Element of REAL
Re |.(f . I1).| is complex real ext-real Element of REAL
(Re |.(f . I1).|) ^2 is complex real ext-real Element of REAL
Im |.(f . I1).| is complex real ext-real Element of REAL
(Im |.(f . I1).|) ^2 is complex real ext-real Element of REAL
((Re |.(f . I1).|) ^2) + ((Im |.(f . I1).|) ^2) is complex real ext-real Element of REAL
sqrt (((Re |.(f . I1).|) ^2) + ((Im |.(f . I1).|) ^2)) is complex real ext-real Element of REAL
|.(f . I1).| / |.|.(f . I1).|.| is complex real ext-real Element of REAL
|.|.(f . I1).|.| " is complex real ext-real set
|.(f . I1).| * (|.|.(f . I1).|.| ") is complex real ext-real set
(|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1 is complex set
Re ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1) is complex real ext-real Element of REAL
(Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) . I1 is complex real ext-real Element of REAL
((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1 is complex set
(|.f.| . I1) * (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1) is complex set
|.(f . I1).| * (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1) is complex set
|.((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1).| is complex real ext-real Element of REAL
(Re ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1)) ^2 is complex real ext-real Element of REAL
Im ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1) is complex real ext-real Element of REAL
(Im ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1)) ^2 is complex real ext-real Element of REAL
((Re ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1)) ^2) + ((Im ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1)) ^2) + ((Im ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1)) ^2)) is complex real ext-real Element of REAL
|.(((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1).| is complex real ext-real Element of REAL
Re (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1) is complex real ext-real Element of REAL
(Re (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1)) ^2 is complex real ext-real Element of REAL
Im (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1) is complex real ext-real Element of REAL
(Im (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1)) ^2 is complex real ext-real Element of REAL
((Re (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1)) ^2) + ((Im (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1)) ^2) + ((Im (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1)) ^2)) is complex real ext-real Element of REAL
|.|.(f . I1).|.| * |.(((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1).| is complex real ext-real Element of REAL
(((X,S,A,f) / |.(X,S,A,f).|) *') * ((f (#) (|.f.| ")) . I1) is complex set
|.(((X,S,A,f) / |.(X,S,A,f).|) *').| * |.((f (#) (|.f.| ")) . I1).| is complex real ext-real Element of REAL
|.(f . I1).| / |.(f . I1).| is complex real ext-real Element of REAL
|.(f . I1).| " is complex real ext-real set
|.(f . I1).| * (|.(f . I1).| ") is complex real ext-real set
(|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1 is complex set
((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1 is complex set
(|.f.| . I1) * (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1) is complex set
|.(f . I1).| * (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1) is complex set
|.((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1).| is complex real ext-real Element of REAL
Re ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1) is complex real ext-real Element of REAL
(Re ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1)) ^2 is complex real ext-real Element of REAL
Im ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1) is complex real ext-real Element of REAL
(Im ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1)) ^2 is complex real ext-real Element of REAL
((Re ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1)) ^2) + ((Im ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1)) ^2) + ((Im ((|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) . I1)) ^2)) is complex real ext-real Element of REAL
|.(((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1).| is complex real ext-real Element of REAL
Re (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1) is complex real ext-real Element of REAL
(Re (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1)) ^2 is complex real ext-real Element of REAL
Im (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1) is complex real ext-real Element of REAL
(Im (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1)) ^2 is complex real ext-real Element of REAL
((Re (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1)) ^2) + ((Im (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1)) ^2) + ((Im (((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1)) ^2)) is complex real ext-real Element of REAL
|.|.(f . I1).|.| * |.(((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))) . I1).| is complex real ext-real Element of REAL
(Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) . I1 is complex real ext-real Element of REAL
|.f.| - (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
- (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) is Relation-like Function-like V33() set
- 1 is non empty complex real ext-real non positive negative set
(- 1) (#) (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) is Relation-like Function-like set
|.f.| + (- (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))))) is Relation-like Function-like set
R2 is complex Element of COMPLEX
R2 *' is complex Element of COMPLEX
Re R2 is complex real ext-real Element of REAL
Im R2 is complex real ext-real Element of REAL
(Im R2) * <i> is complex set
(Re R2) - ((Im R2) * <i>) is complex set
- ((Im R2) * <i>) is complex set
(Re R2) + (- ((Im R2) * <i>)) is complex set
R2 * (R2 *') is complex Element of COMPLEX
Re (R2 * (R2 *')) is complex real ext-real Element of REAL
(Re R2) ^2 is complex real ext-real Element of REAL
(Im R2) ^2 is complex real ext-real Element of REAL
((Re R2) ^2) + ((Im R2) ^2) is complex real ext-real Element of REAL
I2 is Element of S
I2 is Element of S
R is set
(f (#) (|.f.| ")) . R is complex set
f . R is complex set
|.f.| . R is complex real ext-real Element of REAL
(f . R) / (|.f.| . R) is complex Element of COMPLEX
(|.f.| . R) " is complex real ext-real set
(f . R) * ((|.f.| . R) ") is complex set
|.(f . R).| is complex real ext-real Element of REAL
Re (f . R) is complex real ext-real Element of REAL
(Re (f . R)) ^2 is complex real ext-real Element of REAL
Im (f . R) is complex real ext-real Element of REAL
(Im (f . R)) ^2 is complex real ext-real Element of REAL
((Re (f . R)) ^2) + ((Im (f . R)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (f . R)) ^2) + ((Im (f . R)) ^2)) is complex real ext-real Element of REAL
(|.f.| (#) (f (#) (|.f.| "))) . R is complex set
(|.f.| . R) * ((f (#) (|.f.| ")) . R) is complex set
((f (#) (|.f.| ")) . R) * |.(f . R).| is complex set
Integral (A,(Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))))) is ext-real Element of ExtREAL
R_EAL (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))))) is ext-real Element of ExtREAL
max+ (R_EAL (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))))))) is ext-real Element of ExtREAL
max- (R_EAL (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))))))) - (integral+ (A,(max- (R_EAL (Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))))))) is ext-real Element of ExtREAL
Im (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Im (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))))) is ext-real Element of ExtREAL
R_EAL (Im (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Im (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))))) is ext-real Element of ExtREAL
max+ (R_EAL (Im (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Im (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))))))) is ext-real Element of ExtREAL
max- (R_EAL (Im (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Im (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| ")))))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Im (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))))))) - (integral+ (A,(max- (R_EAL (Im (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))))))) is ext-real Element of ExtREAL
(X,S,A,(|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) is complex set
R is complex real ext-real Element of REAL
I is complex real ext-real Element of REAL
I * <i> is complex set
R + (I * <i>) is complex set
Im (R2 * (R2 *')) is complex real ext-real Element of REAL
(Im (((X,S,A,f) / |.(X,S,A,f).|) * (((X,S,A,f) / |.(X,S,A,f).|) *'))) * <i> is complex set
(Re (((X,S,A,f) / |.(X,S,A,f).|) * (((X,S,A,f) / |.(X,S,A,f).|) *'))) + ((Im (((X,S,A,f) / |.(X,S,A,f).|) * (((X,S,A,f) / |.(X,S,A,f).|) *'))) * <i>) is complex set
(((X,S,A,f) / |.(X,S,A,f).|) *') * (X,S,A,f) is complex set
((((X,S,A,f) / |.(X,S,A,f).|) *') * (X,S,A,f)) / |.(X,S,A,f).| is complex Element of COMPLEX
((((X,S,A,f) / |.(X,S,A,f).|) *') * (X,S,A,f)) * (|.(X,S,A,f).| ") is complex set
Re (R + (I * <i>)) is complex real ext-real Element of REAL
E is Element of S
(Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) | E is Relation-like X -defined E -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,((Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) | E)) is ext-real Element of ExtREAL
R_EAL ((Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) | E) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) | E))) is ext-real Element of ExtREAL
max+ (R_EAL ((Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) | E)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) | E)))) is ext-real Element of ExtREAL
max- (R_EAL ((Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) | E)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) | E)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) | E))))) - (integral+ (A,(max- (R_EAL ((Re (|.f.| (#) ((((X,S,A,f) / |.(X,S,A,f).|) *') (#) (f (#) (|.f.| "))))) | E))))) is ext-real Element of ExtREAL
|.f.| | E is Relation-like X -defined E -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(|.f.| | E)) is ext-real Element of ExtREAL
R_EAL (|.f.| | E) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (|.f.| | E))) is ext-real Element of ExtREAL
max+ (R_EAL (|.f.| | E)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (|.f.| | E)))) is ext-real Element of ExtREAL
max- (R_EAL (|.f.| | E)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (|.f.| | E)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (|.f.| | E))))) - (integral+ (A,(max- (R_EAL (|.f.| | E))))) 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))
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
|.(X,S,A,f).| is complex real ext-real Element of REAL
Re (X,S,A,f) is complex real ext-real Element of REAL
(Re (X,S,A,f)) ^2 is complex real ext-real Element of REAL
Im (X,S,A,f) is complex real ext-real Element of REAL
(Im (X,S,A,f)) ^2 is complex real ext-real Element of REAL
((Re (X,S,A,f)) ^2) + ((Im (X,S,A,f)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (X,S,A,f)) ^2) + ((Im (X,S,A,f)) ^2)) is complex real ext-real Element of REAL
|.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,|.f.|) is ext-real Element of ExtREAL
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
Integral (A,(R_EAL |.f.|)) is ext-real Element of ExtREAL
max+ (R_EAL |.f.|) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL |.f.|))) is ext-real Element of ExtREAL
max- (R_EAL |.f.|) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL |.f.|))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL |.f.|)))) - (integral+ (A,(max- (R_EAL |.f.|)))) is ext-real Element of ExtREAL
a is Element of S
a is Element of 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
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))
a is Element of S
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 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))
a is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
f + a is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
dom (f + a) is Element of K6(X)
x is Element of S
(X,S,A,(f + a),x) is complex set
(f + a) | x is Relation-like X -defined x -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,((f + a) | x)) is complex set
(X,S,A,f,x) is complex set
f | x is Relation-like X -defined x -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,(f | x)) is complex set
(X,S,A,a,x) is complex set
a | x is Relation-like X -defined x -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,(a | x)) is complex set
(X,S,A,f,x) + (X,S,A,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
(Re f) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Re (f | x) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Re (f | x))) is ext-real Element of ExtREAL
R_EAL (Re (f | x)) 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 | x)))) is ext-real Element of ExtREAL
max+ (R_EAL (Re (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Re (f | x))))) is ext-real Element of ExtREAL
max- (R_EAL (Re (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Re (f | x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Re (f | x)))))) - (integral+ (A,(max- (R_EAL (Re (f | x)))))) 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))
(Im f) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Im (f | x) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Im (f | x))) is ext-real Element of ExtREAL
R_EAL (Im (f | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Im (f | x)))) is ext-real Element of ExtREAL
max+ (R_EAL (Im (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Im (f | x))))) is ext-real Element of ExtREAL
max- (R_EAL (Im (f | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Im (f | x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Im (f | x)))))) - (integral+ (A,(max- (R_EAL (Im (f | x)))))) is ext-real Element of ExtREAL
x is complex real ext-real Element of REAL
I1 is complex real ext-real Element of REAL
I1 * <i> is complex set
x + (I1 * <i>) is complex set
Im a is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
(Im a) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Im (a | x) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Im (a | x))) is ext-real Element of ExtREAL
R_EAL (Im (a | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Im (a | x)))) is ext-real Element of ExtREAL
max+ (R_EAL (Im (a | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Im (a | x))))) is ext-real Element of ExtREAL
max- (R_EAL (Im (a | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Im (a | x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Im (a | x)))))) - (integral+ (A,(max- (R_EAL (Im (a | x)))))) is ext-real Element of ExtREAL
Re a is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
(Re a) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Re (a | x) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(Re (a | x))) is ext-real Element of ExtREAL
R_EAL (Re (a | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (Re (a | x)))) is ext-real Element of ExtREAL
max+ (R_EAL (Re (a | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Re (a | x))))) is ext-real Element of ExtREAL
max- (R_EAL (Re (a | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Re (a | x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Re (a | x)))))) - (integral+ (A,(max- (R_EAL (Re (a | x)))))) 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))
dom (Im (f + a)) is Element of K6(X)
(Im f) + (Im 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)
Integral_on (A,x,((Im f) + (Im a))) is ext-real Element of ExtREAL
((Im f) + (Im a)) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(((Im f) + (Im a)) | x)) is ext-real Element of ExtREAL
R_EAL (((Im f) + (Im a)) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (((Im f) + (Im a)) | x))) is ext-real Element of ExtREAL
max+ (R_EAL (((Im f) + (Im 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) + (Im a)) | x)))) is ext-real Element of ExtREAL
max- (R_EAL (((Im f) + (Im 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) + (Im a)) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (((Im f) + (Im a)) | x))))) - (integral+ (A,(max- (R_EAL (((Im f) + (Im a)) | x))))) is ext-real Element of ExtREAL
Integral_on (A,x,(Im f)) is ext-real Element of ExtREAL
Integral (A,((Im f) | x)) is ext-real Element of ExtREAL
R_EAL ((Im f) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Im f) | x))) is ext-real Element of ExtREAL
max+ (R_EAL ((Im f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Im f) | x)))) is ext-real Element of ExtREAL
max- (R_EAL ((Im f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Im f) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Im f) | x))))) - (integral+ (A,(max- (R_EAL ((Im f) | x))))) is ext-real Element of ExtREAL
Integral_on (A,x,(Im a)) is ext-real Element of ExtREAL
Integral (A,((Im a) | x)) is ext-real Element of ExtREAL
R_EAL ((Im a) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Im a) | x))) is ext-real Element of ExtREAL
max+ (R_EAL ((Im a) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Im a) | x)))) is ext-real Element of ExtREAL
max- (R_EAL ((Im a) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Im a) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Im a) | x))))) - (integral+ (A,(max- (R_EAL ((Im a) | x))))) is ext-real Element of ExtREAL
(Integral_on (A,x,(Im f))) + (Integral_on (A,x,(Im a))) is ext-real Element of ExtREAL
(Im (f + a)) | x is Relation-like X -defined 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
(Integral (A,((Im f) | x))) + (Integral (A,((Im a) | x))) is ext-real Element of ExtREAL
R2 is complex real ext-real Element of REAL
I2 is complex real ext-real Element of REAL
I2 * <i> is complex set
R2 + (I2 * <i>) is complex set
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
Re (f + a) is Relation-like X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
dom (Re (f + 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))
dom ((Re f) + (Re a)) is Element of K6(X)
Integral_on (A,x,((Re f) + (Re a))) is ext-real Element of ExtREAL
((Re f) + (Re a)) | x is Relation-like X -defined x -defined X -defined REAL -valued Function-like V33() V34() V35() Element of K6(K7(X,REAL))
Integral (A,(((Re f) + (Re a)) | x)) is ext-real Element of ExtREAL
R_EAL (((Re f) + (Re a)) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL (((Re f) + (Re a)) | x))) is ext-real Element of ExtREAL
max+ (R_EAL (((Re f) + (Re a)) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (((Re f) + (Re a)) | x)))) is ext-real Element of ExtREAL
max- (R_EAL (((Re f) + (Re a)) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (((Re f) + (Re a)) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (((Re f) + (Re a)) | x))))) - (integral+ (A,(max- (R_EAL (((Re f) + (Re a)) | x))))) is ext-real Element of ExtREAL
Integral_on (A,x,(Re f)) is ext-real Element of ExtREAL
Integral (A,((Re f) | x)) is ext-real Element of ExtREAL
R_EAL ((Re f) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Re f) | x))) is ext-real Element of ExtREAL
max+ (R_EAL ((Re f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Re f) | x)))) is ext-real Element of ExtREAL
max- (R_EAL ((Re f) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Re f) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Re f) | x))))) - (integral+ (A,(max- (R_EAL ((Re f) | x))))) is ext-real Element of ExtREAL
Integral_on (A,x,(Re a)) is ext-real Element of ExtREAL
Integral (A,((Re a) | x)) is ext-real Element of ExtREAL
R_EAL ((Re a) | x) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
Integral (A,(R_EAL ((Re a) | x))) is ext-real Element of ExtREAL
max+ (R_EAL ((Re a) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Re a) | x)))) is ext-real Element of ExtREAL
max- (R_EAL ((Re a) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Re a) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Re a) | x))))) - (integral+ (A,(max- (R_EAL ((Re a) | x))))) is ext-real Element of ExtREAL
(Integral_on (A,x,(Re f))) + (Integral_on (A,x,(Re a))) is ext-real Element of ExtREAL
(Re (f + a)) | x is Relation-like X -defined 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 ((Re (f + a)) | x))) is ext-real Element of ExtREAL
max+ (R_EAL ((Re (f + a)) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL ((Re (f + a)) | x)))) is ext-real Element of ExtREAL
max- (R_EAL ((Re (f + a)) | x)) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL ((Re (f + a)) | x)))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL ((Re (f + a)) | x))))) - (integral+ (A,(max- (R_EAL ((Re (f + a)) | x))))) is ext-real Element of ExtREAL
(Integral (A,((Re f) | x))) + (Integral (A,((Re a) | x))) is ext-real Element of ExtREAL
Re ((f + a) | x) is Relation-like 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 (Re ((f + a) | x)))) is ext-real Element of ExtREAL
max+ (R_EAL (Re ((f + a) | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max+ (R_EAL (Re ((f + a) | x))))) is ext-real Element of ExtREAL
max- (R_EAL (Re ((f + a) | x))) is Relation-like X -defined ExtREAL -valued Function-like V34() Element of K6(K7(X,ExtREAL))
integral+ (A,(max- (R_EAL (Re ((f + a) | x))))) is ext-real Element of ExtREAL
(integral+ (A,(max+ (R_EAL (Re ((f + a) | x)))))) - (integral+ (A,(max- (R_EAL (Re ((f + a) | x)))))) is ext-real Element of ExtREAL
I is complex real ext-real Element of REAL
R_EAL I is ext-real Element of ExtREAL
R_EAL I1 is ext-real Element of ExtREAL
R_EAL I2 is ext-real Element of ExtREAL
(R_EAL I1) + (R_EAL I2) is ext-real Element of ExtREAL
I1 + I2 is complex real ext-real Element of REAL
R is complex real ext-real Element of REAL
R_EAL R is ext-real Element of ExtREAL
R_EAL x is ext-real Element of ExtREAL
R_EAL R2 is ext-real Element of ExtREAL
(R_EAL x) + (R_EAL R2) is ext-real Element of ExtREAL
x + R2 is complex real ext-real Element of REAL
I * <i> is complex set
R + (I * <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))
a is complex set
a (#) f is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
x is Element of S
(X,S,A,(a (#) f),x) is complex set
(a (#) f) | x is Relation-like X -defined x -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,((a (#) f) | x)) is complex set
(X,S,A,f,x) is complex set
f | x is Relation-like X -defined x -defined X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
(X,S,A,(f | x)) is complex set
a * (X,S,A,f,x) is complex set
dom ((a (#) f) | x) is Element of K6(X)
dom (a (#) f) is Element of K6(X)
(dom (a (#) f)) /\ x is Element of K6(X)
dom f is Element of K6(X)
(dom f) /\ x is Element of K6(X)
dom (f | x) is Element of K6(X)
x is set
((a (#) f) | x) . x is complex set
(a (#) f) . x is complex set
f . x is complex set
a * (f . x) is complex set
(f | x) . x is complex set
a * ((f | x) . x) is complex set
a (#) (f | x) is Relation-like X -defined COMPLEX -valued Function-like V33() Element of K6(K7(X,COMPLEX))
dom (a (#) (f | x)) is Element of K6(X)
(a (#) (f | x)) . x is complex set
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))
A is Element of S
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)
a is complex real ext-real Element of REAL
great_eq_dom (f,a) is set
A /\ (great_eq_dom (f,a)) is Element of K6(X)
less_dom (f,a) is set
A /\ (less_dom (f,a)) is Element of K6(X)
A \ (A /\ (less_dom (f,a))) is Element of K6(X)
x is set
f . x is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
I1 is complex real ext-real Element of REAL
x is set
f . x is complex real ext-real Element of REAL
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))
A is Element of S
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)
a is complex real ext-real Element of REAL
great_dom (f,a) is set
A /\ (great_dom (f,a)) is Element of K6(X)
less_eq_dom (f,a) is set
A /\ (less_eq_dom (f,a)) is Element of K6(X)
A \ (A /\ (less_eq_dom (f,a))) is Element of K6(X)
x is set
f . x is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
I1 is complex real ext-real Element of REAL
x is set
f . x is complex real ext-real Element of REAL
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))
A is Element of S
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)
a is complex real ext-real Element of REAL
less_eq_dom (f,a) is set
A /\ (less_eq_dom (f,a)) is Element of K6(X)
great_dom (f,a) is set
A /\ (great_dom (f,a)) is Element of K6(X)
A \ (A /\ (great_dom (f,a))) is Element of K6(X)
x is set
f . x is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
I1 is complex real ext-real Element of REAL
x is set
f . x is complex real ext-real Element of REAL
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))
A is Element of S
f 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
Coim (f,a) is set
A /\ (Coim (f,a)) is Element of K6(X)
great_eq_dom (f,a) is set
A /\ (great_eq_dom (f,a)) is Element of K6(X)
less_eq_dom (f,a) is set
(A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) is Element of K6(X)
x is set
dom f is Element of K6(X)
f . x is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
I1 is complex real ext-real Element of REAL
x is set
f . x is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL