REAL is non empty non trivial non finite V71() V72() V73() V77() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() Element of bool REAL
bool REAL is non empty set
ExtREAL is non empty V72() set
[:NAT,ExtREAL:] is non empty V13() V62() set
bool [:NAT,ExtREAL:] is non empty set
bool ExtREAL is non empty set
COMPLEX is non empty non trivial non finite V71() V77() set
omega is non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() set
bool omega is non empty set
bool NAT is non empty set
RAT is non empty non trivial non finite V71() V72() V73() V74() V77() set
INT is non empty non trivial non finite V71() V72() V73() V74() V75() V77() set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() non-empty empty-yielding V17( RAT ) functional finite finite-yielding V27() FinSequence-like FinSequence-membered ext-real non positive non negative V61() V62() V63() V64() V71() V72() V73() V74() V75() V76() V77() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() non-empty empty-yielding V17( RAT ) functional finite finite-yielding V27() FinSequence-like FinSequence-membered ext-real non positive non negative V61() V62() V63() V64() V71() V72() V73() V74() V75() V76() V77() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
{{},1} is finite set
K335() is set
bool K335() is non empty set
K336() is Element of bool K335()
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
K199() is V71() V72() V73() V74() V75() V76() Element of bool NAT
[:REAL,REAL:] is non empty V13() V61() V62() V63() set
bool [:REAL,REAL:] is non empty set
[:NAT,REAL:] is non empty V13() V61() V62() V63() set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
[:COMPLEX,COMPLEX:] is non empty V13() V61() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V13() V61() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty V13() V61() V62() V63() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty V13() V17( RAT ) V61() V62() V63() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty V13() V17( RAT ) V61() V62() V63() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty V13() V17( RAT ) V17( INT ) V61() V62() V63() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty V13() V17( RAT ) V17( INT ) V61() V62() V63() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty V13() V17( RAT ) V17( INT ) V61() V62() V63() V64() set
[:[:NAT,NAT:],NAT:] is non empty V13() V17( RAT ) V17( INT ) V61() V62() V63() V64() set
bool [:[:NAT,NAT:],NAT:] is non empty set
K223(1,NAT) is M8( NAT )
bool RAT is non empty set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real positive non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
+infty is non empty non real ext-real positive non negative set
-infty is non empty non real ext-real non positive negative set
0. is ext-real Element of ExtREAL
K668() is non empty non real ext-real non positive negative Element of ExtREAL
K667() is non empty non real ext-real positive non negative Element of ExtREAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
[:r,ExtREAL:] is non empty V13() V62() set
bool [:r,ExtREAL:] is non empty set
Sigma is non empty V13() V16(r) V17( ExtREAL ) Function-like total V32(r, ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:r,ExtREAL:]
P is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
dom P is Element of bool Omega
X is Element of r
Sigma . X is ext-real Element of ExtREAL
P | X is V13() V16(Omega) V16(X) V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (Sigma,(P | X)) is ext-real Element of ExtREAL
max+ (P | X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max+ (P | X))) is ext-real Element of ExtREAL
max- (P | X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max- (P | X))) is ext-real Element of ExtREAL
(integral+ (Sigma,(max+ (P | X)))) - (integral+ (Sigma,(max- (P | X)))) is ext-real Element of ExtREAL
K409((integral+ (Sigma,(max- (P | X))))) is ext-real set
K408((integral+ (Sigma,(max+ (P | X)))),K409((integral+ (Sigma,(max- (P | X)))))) is ext-real set
PM is V11() real ext-real Element of REAL
R_EAL PM is ext-real Element of ExtREAL
(R_EAL PM) * (Sigma . X) is ext-real Element of ExtREAL
chi (X,Omega) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
(chi (X,Omega)) | X is V13() V16(Omega) V16(X) V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
PM (#) ((chi (X,Omega)) | X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
dom (PM (#) ((chi (X,Omega)) | X)) is Element of bool Omega
S is Element of Omega
(PM (#) ((chi (X,Omega)) | X)) . S is ext-real Element of ExtREAL
(P | X) . S is ext-real Element of ExtREAL
dom ((chi (X,Omega)) | X) is Element of bool Omega
dom (chi (X,Omega)) is Element of bool Omega
(dom (chi (X,Omega))) /\ X is Element of bool Omega
P . S is ext-real Element of ExtREAL
((chi (X,Omega)) | X) . S is ext-real Element of ExtREAL
(R_EAL PM) * (((chi (X,Omega)) | X) . S) is ext-real Element of ExtREAL
(chi (X,Omega)) . S is ext-real Element of ExtREAL
(R_EAL PM) * ((chi (X,Omega)) . S) is ext-real Element of ExtREAL
1. is ext-real Element of ExtREAL
(R_EAL PM) * 1. is ext-real Element of ExtREAL
(P | X) - (PM (#) ((chi (X,Omega)) | X)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
dom ((chi (X,Omega)) | X) is Element of bool Omega
dom (chi (X,Omega)) is Element of bool Omega
(dom (chi (X,Omega))) /\ X is Element of bool Omega
Omega /\ X is Element of bool Omega
X /\ X is Element of r
Integral (Sigma,((chi (X,Omega)) | X)) is ext-real Element of ExtREAL
max+ ((chi (X,Omega)) | X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max+ ((chi (X,Omega)) | X))) is ext-real Element of ExtREAL
max- ((chi (X,Omega)) | X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max- ((chi (X,Omega)) | X))) is ext-real Element of ExtREAL
(integral+ (Sigma,(max+ ((chi (X,Omega)) | X)))) - (integral+ (Sigma,(max- ((chi (X,Omega)) | X)))) is ext-real Element of ExtREAL
K409((integral+ (Sigma,(max- ((chi (X,Omega)) | X))))) is ext-real set
K408((integral+ (Sigma,(max+ ((chi (X,Omega)) | X)))),K409((integral+ (Sigma,(max- ((chi (X,Omega)) | X)))))) is ext-real set
dom (P | X) is Element of bool Omega
(dom (P | X)) /\ (dom (PM (#) ((chi (X,Omega)) | X))) is Element of bool Omega
S is Element of r
(PM (#) ((chi (X,Omega)) | X)) | S is V13() V16(Omega) V16(S) V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (Sigma,((PM (#) ((chi (X,Omega)) | X)) | S)) is ext-real Element of ExtREAL
max+ ((PM (#) ((chi (X,Omega)) | X)) | S) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max+ ((PM (#) ((chi (X,Omega)) | X)) | S))) is ext-real Element of ExtREAL
max- ((PM (#) ((chi (X,Omega)) | X)) | S) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max- ((PM (#) ((chi (X,Omega)) | X)) | S))) is ext-real Element of ExtREAL
(integral+ (Sigma,(max+ ((PM (#) ((chi (X,Omega)) | X)) | S)))) - (integral+ (Sigma,(max- ((PM (#) ((chi (X,Omega)) | X)) | S)))) is ext-real Element of ExtREAL
K409((integral+ (Sigma,(max- ((PM (#) ((chi (X,Omega)) | X)) | S))))) is ext-real set
K408((integral+ (Sigma,(max+ ((PM (#) ((chi (X,Omega)) | X)) | S)))),K409((integral+ (Sigma,(max- ((PM (#) ((chi (X,Omega)) | X)) | S)))))) is ext-real set
(P | X) | S is V13() V16(Omega) V16(S) V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (Sigma,((P | X) | S)) is ext-real Element of ExtREAL
max+ ((P | X) | S) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max+ ((P | X) | S))) is ext-real Element of ExtREAL
max- ((P | X) | S) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max- ((P | X) | S))) is ext-real Element of ExtREAL
(integral+ (Sigma,(max+ ((P | X) | S)))) - (integral+ (Sigma,(max- ((P | X) | S)))) is ext-real Element of ExtREAL
K409((integral+ (Sigma,(max- ((P | X) | S))))) is ext-real set
K408((integral+ (Sigma,(max+ ((P | X) | S)))),K409((integral+ (Sigma,(max- ((P | X) | S)))))) is ext-real set
(dom P) /\ X is Element of bool Omega
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
[:r,ExtREAL:] is non empty V13() V62() set
bool [:r,ExtREAL:] is non empty set
Sigma is non empty V13() V16(r) V17( ExtREAL ) Function-like total V32(r, ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:r,ExtREAL:]
P is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom P is Element of bool Omega
X is Element of r
Sigma . X is ext-real Element of ExtREAL
P | X is V13() V16(Omega) V16(X) V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
Integral (Sigma,(P | X)) is ext-real Element of ExtREAL
R_EAL (P | X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral (Sigma,(R_EAL (P | X))) is ext-real Element of ExtREAL
max+ (R_EAL (P | X)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max+ (R_EAL (P | X)))) is ext-real Element of ExtREAL
max- (R_EAL (P | X)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max- (R_EAL (P | X)))) is ext-real Element of ExtREAL
(integral+ (Sigma,(max+ (R_EAL (P | X))))) - (integral+ (Sigma,(max- (R_EAL (P | X))))) is ext-real Element of ExtREAL
K409((integral+ (Sigma,(max- (R_EAL (P | X)))))) is ext-real set
K408((integral+ (Sigma,(max+ (R_EAL (P | X))))),K409((integral+ (Sigma,(max- (R_EAL (P | X))))))) is ext-real set
PM is V11() real ext-real Element of REAL
R_EAL PM is ext-real Element of ExtREAL
(R_EAL PM) * (Sigma . X) is ext-real Element of ExtREAL
R_EAL P is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
[:r,ExtREAL:] is non empty V13() V62() set
bool [:r,ExtREAL:] is non empty set
Sigma is non empty V13() V16(r) V17( ExtREAL ) Function-like total V32(r, ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:r,ExtREAL:]
P is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
dom P is Element of bool Omega
X is Element of r
Sigma . X is ext-real Element of ExtREAL
P | X is V13() V16(Omega) V16(X) V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (Sigma,(P | X)) is ext-real Element of ExtREAL
max+ (P | X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max+ (P | X))) is ext-real Element of ExtREAL
max- (P | X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max- (P | X))) is ext-real Element of ExtREAL
(integral+ (Sigma,(max+ (P | X)))) - (integral+ (Sigma,(max- (P | X)))) is ext-real Element of ExtREAL
K409((integral+ (Sigma,(max- (P | X))))) is ext-real set
K408((integral+ (Sigma,(max+ (P | X)))),K409((integral+ (Sigma,(max- (P | X)))))) is ext-real set
PM is V11() real ext-real Element of REAL
R_EAL PM is ext-real Element of ExtREAL
(R_EAL PM) * (Sigma . X) is ext-real Element of ExtREAL
chi (X,Omega) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
(chi (X,Omega)) | X is V13() V16(Omega) V16(X) V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
PM (#) ((chi (X,Omega)) | X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
dom (PM (#) ((chi (X,Omega)) | X)) is Element of bool Omega
dom ((chi (X,Omega)) | X) is Element of bool Omega
dom (chi (X,Omega)) is Element of bool Omega
(dom (chi (X,Omega))) /\ X is Element of bool Omega
Omega /\ X is Element of bool Omega
dom (P | X) is Element of bool Omega
(dom P) /\ X is Element of bool Omega
S is Element of Omega
(P | X) . S is ext-real Element of ExtREAL
(PM (#) ((chi (X,Omega)) | X)) . S is ext-real Element of ExtREAL
P . S is ext-real Element of ExtREAL
((chi (X,Omega)) | X) . S is ext-real Element of ExtREAL
(R_EAL PM) * (((chi (X,Omega)) | X) . S) is ext-real Element of ExtREAL
(chi (X,Omega)) . S is ext-real Element of ExtREAL
(R_EAL PM) * ((chi (X,Omega)) . S) is ext-real Element of ExtREAL
1. is ext-real Element of ExtREAL
(R_EAL PM) * 1. is ext-real Element of ExtREAL
(PM (#) ((chi (X,Omega)) | X)) - (P | X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
X /\ X is Element of r
Integral (Sigma,((chi (X,Omega)) | X)) is ext-real Element of ExtREAL
max+ ((chi (X,Omega)) | X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max+ ((chi (X,Omega)) | X))) is ext-real Element of ExtREAL
max- ((chi (X,Omega)) | X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max- ((chi (X,Omega)) | X))) is ext-real Element of ExtREAL
(integral+ (Sigma,(max+ ((chi (X,Omega)) | X)))) - (integral+ (Sigma,(max- ((chi (X,Omega)) | X)))) is ext-real Element of ExtREAL
K409((integral+ (Sigma,(max- ((chi (X,Omega)) | X))))) is ext-real set
K408((integral+ (Sigma,(max+ ((chi (X,Omega)) | X)))),K409((integral+ (Sigma,(max- ((chi (X,Omega)) | X)))))) is ext-real set
(dom (P | X)) /\ (dom (PM (#) ((chi (X,Omega)) | X))) is Element of bool Omega
S is Element of r
(P | X) | S is V13() V16(Omega) V16(S) V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (Sigma,((P | X) | S)) is ext-real Element of ExtREAL
max+ ((P | X) | S) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max+ ((P | X) | S))) is ext-real Element of ExtREAL
max- ((P | X) | S) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max- ((P | X) | S))) is ext-real Element of ExtREAL
(integral+ (Sigma,(max+ ((P | X) | S)))) - (integral+ (Sigma,(max- ((P | X) | S)))) is ext-real Element of ExtREAL
K409((integral+ (Sigma,(max- ((P | X) | S))))) is ext-real set
K408((integral+ (Sigma,(max+ ((P | X) | S)))),K409((integral+ (Sigma,(max- ((P | X) | S)))))) is ext-real set
(PM (#) ((chi (X,Omega)) | X)) | S is V13() V16(Omega) V16(S) V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (Sigma,((PM (#) ((chi (X,Omega)) | X)) | S)) is ext-real Element of ExtREAL
max+ ((PM (#) ((chi (X,Omega)) | X)) | S) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max+ ((PM (#) ((chi (X,Omega)) | X)) | S))) is ext-real Element of ExtREAL
max- ((PM (#) ((chi (X,Omega)) | X)) | S) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max- ((PM (#) ((chi (X,Omega)) | X)) | S))) is ext-real Element of ExtREAL
(integral+ (Sigma,(max+ ((PM (#) ((chi (X,Omega)) | X)) | S)))) - (integral+ (Sigma,(max- ((PM (#) ((chi (X,Omega)) | X)) | S)))) is ext-real Element of ExtREAL
K409((integral+ (Sigma,(max- ((PM (#) ((chi (X,Omega)) | X)) | S))))) is ext-real set
K408((integral+ (Sigma,(max+ ((PM (#) ((chi (X,Omega)) | X)) | S)))),K409((integral+ (Sigma,(max- ((PM (#) ((chi (X,Omega)) | X)) | S)))))) is ext-real set
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
[:r,ExtREAL:] is non empty V13() V62() set
bool [:r,ExtREAL:] is non empty set
Sigma is non empty V13() V16(r) V17( ExtREAL ) Function-like total V32(r, ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:r,ExtREAL:]
P is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom P is Element of bool Omega
X is Element of r
Sigma . X is ext-real Element of ExtREAL
P | X is V13() V16(Omega) V16(X) V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
Integral (Sigma,(P | X)) is ext-real Element of ExtREAL
R_EAL (P | X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral (Sigma,(R_EAL (P | X))) is ext-real Element of ExtREAL
max+ (R_EAL (P | X)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max+ (R_EAL (P | X)))) is ext-real Element of ExtREAL
max- (R_EAL (P | X)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (Sigma,(max- (R_EAL (P | X)))) is ext-real Element of ExtREAL
(integral+ (Sigma,(max+ (R_EAL (P | X))))) - (integral+ (Sigma,(max- (R_EAL (P | X))))) is ext-real Element of ExtREAL
K409((integral+ (Sigma,(max- (R_EAL (P | X)))))) is ext-real set
K408((integral+ (Sigma,(max+ (R_EAL (P | X))))),K409((integral+ (Sigma,(max- (R_EAL (P | X))))))) is ext-real set
PM is V11() real ext-real Element of REAL
R_EAL PM is ext-real Element of ExtREAL
(R_EAL PM) * (Sigma . X) is ext-real Element of ExtREAL
R_EAL P is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
[:r,ExtREAL:] is non empty V13() V62() set
bool [:r,ExtREAL:] is non empty set
Sigma is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom Sigma is Element of bool Omega
P is non empty V13() V16(r) V17( ExtREAL ) Function-like total V32(r, ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:r,ExtREAL:]
Integral (P,Sigma) is ext-real Element of ExtREAL
R_EAL Sigma is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral (P,(R_EAL Sigma)) is ext-real Element of ExtREAL
max+ (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (P,(max+ (R_EAL Sigma))) is ext-real Element of ExtREAL
max- (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (P,(max- (R_EAL Sigma))) is ext-real Element of ExtREAL
(integral+ (P,(max+ (R_EAL Sigma)))) - (integral+ (P,(max- (R_EAL Sigma)))) is ext-real Element of ExtREAL
K409((integral+ (P,(max- (R_EAL Sigma))))) is ext-real set
K408((integral+ (P,(max+ (R_EAL Sigma)))),K409((integral+ (P,(max- (R_EAL Sigma)))))) is ext-real set
X is V13() V16( NAT ) V17(r) Function-like finite FinSequence-like FinSubsequence-like V126() FinSequence of r
rng X is finite Element of bool r
bool r is non empty set
union (rng X) is set
dom X is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
P * X is V13() V16( NAT ) V17( ExtREAL ) Function-like finite V62() Element of bool [:NAT,ExtREAL:]
PM is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
dom PM is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
K is V13() V16( NAT ) V17( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom K is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Sum K is ext-real Element of ExtREAL
dom (R_EAL Sigma) is Element of bool Omega
S is set
(R_EAL Sigma) . S is ext-real Element of ExtREAL
S is V13() V16( NAT ) V17( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
K . K is ext-real Element of ExtREAL
S . K is ext-real Element of ExtREAL
(P * X) . K is ext-real Element of ExtREAL
(S . K) * ((P * X) . K) is ext-real Element of ExtREAL
PM . K is V11() real ext-real Element of REAL
R_EAL (PM . K) is ext-real Element of ExtREAL
(R_EAL (PM . K)) * ((P * X) . K) is ext-real Element of ExtREAL
integral' (P,(R_EAL Sigma)) is ext-real Element of ExtREAL
integral (Omega,r,P,(R_EAL Sigma)) is ext-real Element of ExtREAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom Sigma is Element of bool Omega
P is V13() V16( NAT ) V17(r) Function-like finite FinSequence-like FinSubsequence-like V126() FinSequence of r
rng P is finite Element of bool r
bool r is non empty set
union (rng P) is set
dom P is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
len P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Seg (len P) is finite len P -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len P ) } is set
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
P . X is set
PM is set
Sigma . PM is V11() real ext-real Element of REAL
PM is set
Sigma . PM is V11() real ext-real Element of REAL
K is set
Sigma . K is V11() real ext-real Element of REAL
X is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
dom X is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
PM is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
P . PM is set
X . PM is V11() real ext-real Element of REAL
K is set
Sigma . K is V11() real ext-real Element of REAL
PM is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
K is set
P . PM is set
Sigma . K is V11() real ext-real Element of REAL
X . PM is V11() real ext-real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
rng Sigma is V71() V72() V73() Element of bool REAL
dom Sigma is Element of bool Omega
P is V13() V16( NAT ) V17(r) Function-like finite FinSequence-like FinSubsequence-like V126() FinSequence of r
rng P is finite Element of bool r
bool r is non empty set
union (rng P) is set
dom P is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
X is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
dom X is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
rng X is finite V71() V72() V73() V147() Element of bool REAL
PM is set
K is set
Sigma . K is V11() real ext-real Element of REAL
S is set
K is set
P . K is set
X . K is V11() real ext-real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
[:r,ExtREAL:] is non empty V13() V62() set
bool [:r,ExtREAL:] is non empty set
Sigma is non empty V13() V16(r) V17( ExtREAL ) Function-like total V32(r, ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:r,ExtREAL:]
P is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom P is Element of bool Omega
rng P is V71() V72() V73() Element of bool REAL
Sigma . (dom P) is ext-real Element of ExtREAL
X is Element of r
X is Element of r
R_EAL P is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
dom (R_EAL P) is Element of bool Omega
chi (X,Omega) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
dom (chi (X,Omega)) is Element of bool Omega
(dom (R_EAL P)) /\ (dom (chi (X,Omega))) is Element of bool Omega
X /\ Omega is Element of bool Omega
(R_EAL P) (#) (chi (X,Omega)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
dom ((R_EAL P) (#) (chi (X,Omega))) is Element of bool Omega
PM is set
((R_EAL P) (#) (chi (X,Omega))) . PM is ext-real Element of ExtREAL
(R_EAL P) . PM is ext-real Element of ExtREAL
(chi (X,Omega)) . PM is ext-real Element of ExtREAL
((R_EAL P) . PM) * ((chi (X,Omega)) . PM) is ext-real Element of ExtREAL
R_EAL 1 is ext-real Element of ExtREAL
((R_EAL P) . PM) * (R_EAL 1) is ext-real Element of ExtREAL
P . PM is V11() real ext-real Element of REAL
((R_EAL P) (#) (chi (X,Omega))) | X is V13() V16(Omega) V16(X) V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
(((R_EAL P) (#) (chi (X,Omega))) | X) . PM is ext-real Element of ExtREAL
rng (R_EAL P) is V72() Element of bool ExtREAL
dom (((R_EAL P) (#) (chi (X,Omega))) | X) is Element of bool Omega
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
[:r,ExtREAL:] is non empty V13() V62() set
bool [:r,ExtREAL:] is non empty set
Sigma is non empty V13() V16(r) V17( ExtREAL ) Function-like total V32(r, ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:r,ExtREAL:]
P is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom P is Element of bool Omega
Sigma . (dom P) is ext-real Element of ExtREAL
rng P is V71() V72() V73() Element of bool REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Omega is non empty finite set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
r is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom r is finite Element of bool Omega
canFS (dom r) is V13() V16( NAT ) V17( dom r) Function-like one-to-one finite V33( dom r) V34( NAT , dom r) FinSequence-like FinSubsequence-like FinSequence of dom r
dom (canFS (dom r)) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
len (canFS (dom r)) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Seg (len (canFS (dom r))) is finite len (canFS (dom r)) -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len (canFS (dom r)) ) } is set
PM is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(canFS (dom r)) . PM is set
{((canFS (dom r)) . PM)} is finite set
rng (canFS (dom r)) is finite Element of bool (dom r)
bool (dom r) is non empty finite V27() set
PM is V13() V16( NAT ) V17( bool Omega) Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool Omega
dom PM is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(canFS (dom r)) . K is set
(canFS (dom r)) . S is set
PM . K is set
{((canFS (dom r)) . K)} is finite set
PM . S is set
{((canFS (dom r)) . S)} is finite set
S is set
rng (canFS (dom r)) is finite Element of bool (dom r)
bool (dom r) is non empty finite V27() set
K is set
(canFS (dom r)) . K is set
IX is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
K is V13() V16( NAT ) V17((Omega)) Function-like finite FinSequence-like FinSubsequence-like V126() FinSequence of (Omega)
dom K is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
K . IX is set
rng K is finite V27() Element of bool (Omega)
bool (Omega) is non empty finite V27() set
(canFS (dom r)) . IX is set
{((canFS (dom r)) . IX)} is finite set
union (rng K) is finite set
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
K . S is set
K is Element of Omega
IX is Element of Omega
r . K is V11() real ext-real Element of REAL
r . IX is V11() real ext-real Element of REAL
(canFS (dom r)) . S is set
{((canFS (dom r)) . S)} is finite set
r . ((canFS (dom r)) . S) is V11() real ext-real Element of REAL
S is set
K is set
IX is set
K . IX is set
PMK is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
K . PMK is set
(canFS (dom r)) . PMK is set
{((canFS (dom r)) . PMK)} is finite set
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
K . S is set
(canFS (dom r)) . S is set
{((canFS (dom r)) . S)} is finite set
K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
IX is Element of Omega
K . K is set
PMK is Element of Omega
r . IX is V11() real ext-real Element of REAL
r . PMK is V11() real ext-real Element of REAL
Omega is non empty finite set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
r is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom r is finite Element of bool Omega
card (dom r) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
canFS (dom r) is V13() V16( NAT ) V17( dom r) Function-like one-to-one finite V33( dom r) V34( NAT , dom r) FinSequence-like FinSubsequence-like FinSequence of dom r
len (canFS (dom r)) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom (canFS (dom r)) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
rng (canFS (dom r)) is finite Element of bool (dom r)
bool (dom r) is non empty finite V27() set
PM is V13() V16( NAT ) V17((Omega)) Function-like finite FinSequence-like FinSubsequence-like V126() FinSequence of (Omega)
rng PM is finite V27() Element of bool (Omega)
bool (Omega) is non empty finite V27() set
union (rng PM) is finite set
dom PM is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Omega is non empty finite set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
r is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom r is finite Element of bool Omega
canFS (dom r) is V13() V16( NAT ) V17( dom r) Function-like one-to-one finite V33( dom r) V34( NAT , dom r) FinSequence-like FinSubsequence-like FinSequence of dom r
dom (canFS (dom r)) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
X is V13() V16( NAT ) V17((Omega)) Function-like finite FinSequence-like FinSubsequence-like V126() FinSequence of (Omega)
rng X is finite V27() Element of bool (Omega)
bool (Omega) is non empty finite V27() set
union (rng X) is finite set
dom X is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
[:(Omega),ExtREAL:] is non empty V13() V62() set
bool [:(Omega),ExtREAL:] is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
Sigma is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom Sigma is finite Element of bool Omega
r is non empty V13() V16((Omega)) V17( ExtREAL ) Function-like finite total V32((Omega), ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:(Omega),ExtREAL:]
r . (dom Sigma) is ext-real Element of ExtREAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
[:r,ExtREAL:] is non empty V13() V62() set
bool [:r,ExtREAL:] is non empty set
Sigma is non empty V13() V16(r) V17( ExtREAL ) Function-like total V32(r, ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:r,ExtREAL:]
P is set
X is set
Sigma . X is ext-real Element of ExtREAL
Sigma . P is ext-real Element of ExtREAL
Omega is non empty finite set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
r is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom r is finite Element of bool Omega
bool Omega is non empty finite V27() set
canFS (dom r) is V13() V16( NAT ) V17( dom r) Function-like one-to-one finite V33( dom r) V34( NAT , dom r) FinSequence-like FinSubsequence-like FinSequence of dom r
r * (canFS (dom r)) is V13() V16( NAT ) V17( REAL ) Function-like finite V61() V62() V63() Element of bool [:NAT,REAL:]
rng (canFS (dom r)) is finite Element of bool (dom r)
bool (dom r) is non empty finite V27() set
rng (r * (canFS (dom r))) is finite V71() V72() V73() V147() Element of bool REAL
Omega is non empty finite set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
r is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom r is finite Element of bool Omega
bool Omega is non empty finite V27() set
canFS (dom r) is V13() V16( NAT ) V17( dom r) Function-like one-to-one finite V33( dom r) V34( NAT , dom r) FinSequence-like FinSubsequence-like FinSequence of dom r
r * (canFS (dom r)) is V13() V16( NAT ) V17( REAL ) Function-like finite V61() V62() V63() Element of bool [:NAT,REAL:]
dom (r * (canFS (dom r))) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
dom (canFS (dom r)) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
rng (canFS (dom r)) is finite Element of bool (dom r)
bool (dom r) is non empty finite V27() set
Omega is non empty finite set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
bool Omega is non empty finite V27() set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool (bool Omega) is non empty finite V27() set
r is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom r is finite Element of bool Omega
P is finite Element of (Omega)
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
[:(Omega),ExtREAL:] is non empty V13() V62() set
bool [:(Omega),ExtREAL:] is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
canFS Omega is non empty V13() V16( NAT ) V17(Omega) Function-like one-to-one finite V33(Omega) V34( NAT ,Omega) FinSequence-like FinSubsequence-like FinSequence of Omega
r is non empty V13() V16((Omega)) V17( ExtREAL ) Function-like finite total V32((Omega), ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:(Omega),ExtREAL:]
r . Omega is ext-real Element of ExtREAL
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
Integral (r,Sigma) is ext-real Element of ExtREAL
R_EAL Sigma is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral (r,(R_EAL Sigma)) is ext-real Element of ExtREAL
max+ (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL Sigma))) is ext-real Element of ExtREAL
max- (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL Sigma))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL Sigma)))) - (integral+ (r,(max- (R_EAL Sigma)))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL Sigma))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL Sigma)))),K409((integral+ (r,(max- (R_EAL Sigma)))))) is ext-real set
max- Sigma is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom (max- Sigma) is finite Element of bool Omega
canFS (dom (max- Sigma)) is V13() V16( NAT ) V17( dom (max- Sigma)) Function-like one-to-one finite V33( dom (max- Sigma)) V34( NAT , dom (max- Sigma)) FinSequence-like FinSubsequence-like FinSequence of dom (max- Sigma)
(max- Sigma) * (canFS (dom (max- Sigma))) is V13() V16( NAT ) V17( REAL ) Function-like finite V61() V62() V63() Element of bool [:NAT,REAL:]
max+ Sigma is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom (max+ Sigma) is finite Element of bool Omega
canFS (dom (max+ Sigma)) is V13() V16( NAT ) V17( dom (max+ Sigma)) Function-like one-to-one finite V33( dom (max+ Sigma)) V34( NAT , dom (max+ Sigma)) FinSequence-like FinSubsequence-like FinSequence of dom (max+ Sigma)
(max+ Sigma) * (canFS (dom (max+ Sigma))) is V13() V16( NAT ) V17( REAL ) Function-like finite V61() V62() V63() Element of bool [:NAT,REAL:]
dom Sigma is non empty finite Element of bool Omega
canFS (dom Sigma) is non empty V13() V16( NAT ) V17( dom Sigma) Function-like one-to-one finite V33( dom Sigma) V34( NAT , dom Sigma) FinSequence-like FinSubsequence-like FinSequence of dom Sigma
dom (canFS (dom Sigma)) is non empty finite V71() V72() V73() V74() V75() V76() Element of bool NAT
t is V13() V16( NAT ) V17((Omega)) Function-like finite FinSequence-like FinSubsequence-like V126() FinSequence of (Omega)
rng t is finite V27() Element of bool (Omega)
bool (Omega) is non empty finite V27() set
union (rng t) is finite set
dom t is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
len t is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom (canFS (dom (max+ Sigma))) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
am is V13() V16( NAT ) V17((Omega)) Function-like finite FinSequence-like FinSubsequence-like V126() FinSequence of (Omega)
rng am is finite V27() Element of bool (Omega)
union (rng am) is finite set
dom am is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
K is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
r * am is V13() V16( NAT ) V17( ExtREAL ) Function-like finite V62() Element of bool [:NAT,ExtREAL:]
Seg (len t) is finite len t -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len t ) } is set
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
K . E is V11() real ext-real Element of REAL
R_EAL (K . E) is ext-real Element of ExtREAL
(r * am) . E is ext-real Element of ExtREAL
(R_EAL (K . E)) * ((r * am) . E) is ext-real Element of ExtREAL
E is V13() V16( NAT ) V17( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom E is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
dom K is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
xp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
am . xp is set
K . xp is V11() real ext-real Element of REAL
xp1 is set
(max+ Sigma) . xp1 is V11() real ext-real Element of REAL
(canFS (dom (max+ Sigma))) . xp is set
{((canFS (dom (max+ Sigma))) . xp)} is finite set
Sigma * (canFS (dom Sigma)) is V13() V16( NAT ) V17( REAL ) Function-like finite V61() V62() V63() Element of bool [:NAT,REAL:]
- 1 is non empty V11() real ext-real non positive negative Element of REAL
R_EAL (- 1) is ext-real Element of ExtREAL
Integral (r,(max- Sigma)) is ext-real Element of ExtREAL
R_EAL (max- Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL (max- Sigma))) is ext-real Element of ExtREAL
max+ (R_EAL (max- Sigma)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL (max- Sigma)))) is ext-real Element of ExtREAL
max- (R_EAL (max- Sigma)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL (max- Sigma)))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL (max- Sigma))))) - (integral+ (r,(max- (R_EAL (max- Sigma))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL (max- Sigma)))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL (max- Sigma))))),K409((integral+ (r,(max- (R_EAL (max- Sigma))))))) is ext-real set
(R_EAL (- 1)) * (Integral (r,(max- Sigma))) is ext-real Element of ExtREAL
R_EAL 1 is ext-real Element of ExtREAL
- (R_EAL 1) is ext-real Element of ExtREAL
(- (R_EAL 1)) * (Integral (r,(max- Sigma))) is ext-real Element of ExtREAL
(R_EAL 1) * (Integral (r,(max- Sigma))) is ext-real Element of ExtREAL
- ((R_EAL 1) * (Integral (r,(max- Sigma)))) is ext-real Element of ExtREAL
- (Integral (r,(max- Sigma))) is ext-real Element of ExtREAL
xp is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
r * t is V13() V16( NAT ) V17( ExtREAL ) Function-like finite V62() Element of bool [:NAT,ExtREAL:]
xp1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
xp . xp1 is V11() real ext-real Element of REAL
R_EAL (xp . xp1) is ext-real Element of ExtREAL
(r * t) . xp1 is ext-real Element of ExtREAL
(R_EAL (xp . xp1)) * ((r * t) . xp1) is ext-real Element of ExtREAL
xp1 is V13() V16( NAT ) V17( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom xp1 is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
dom (canFS Omega) is non empty finite V71() V72() V73() V74() V75() V76() Element of bool NAT
xm is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(canFS Omega) . xm is set
{((canFS Omega) . xm)} is finite set
r . {((canFS Omega) . xm)} is ext-real Element of ExtREAL
rng (canFS Omega) is non empty finite Element of bool Omega
xm is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
xp1 . xm is ext-real Element of ExtREAL
(canFS Omega) . xm is set
Sigma . ((canFS Omega) . xm) is V11() real ext-real Element of REAL
R_EAL (Sigma . ((canFS Omega) . xm)) is ext-real Element of ExtREAL
{((canFS Omega) . xm)} is finite set
r . {((canFS Omega) . xm)} is ext-real Element of ExtREAL
(R_EAL (Sigma . ((canFS Omega) . xm))) * (r . {((canFS Omega) . xm)}) is ext-real Element of ExtREAL
(r * t) . xm is ext-real Element of ExtREAL
t . xm is set
r . (t . xm) is ext-real Element of ExtREAL
(canFS (dom Sigma)) . xm is set
Sigma . ((canFS (dom Sigma)) . xm) is V11() real ext-real Element of REAL
xp . xm is V11() real ext-real Element of REAL
R_EAL (xp . xm) is ext-real Element of ExtREAL
(R_EAL (xp . xm)) * ((r * t) . xm) is ext-real Element of ExtREAL
xm is set
rng xp1 is finite V72() set
rng xp1 is finite V72() Element of bool ExtREAL
xm1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
xp1 . xm1 is ext-real Element of ExtREAL
(canFS Omega) . xm1 is set
{((canFS Omega) . xm1)} is finite set
r . {((canFS Omega) . xm1)} is ext-real Element of ExtREAL
Sigma . ((canFS Omega) . xm1) is V11() real ext-real Element of REAL
R_EAL (Sigma . ((canFS Omega) . xm1)) is ext-real Element of ExtREAL
(R_EAL (Sigma . ((canFS Omega) . xm1))) * (r . {((canFS Omega) . xm1)}) is ext-real Element of ExtREAL
z is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
z * k is V11() real ext-real Element of REAL
len xp1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Sum xp1 is ext-real Element of ExtREAL
xm1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
E . xm1 is ext-real Element of ExtREAL
(canFS Omega) . xm1 is set
(max+ Sigma) . ((canFS Omega) . xm1) is V11() real ext-real Element of REAL
R_EAL ((max+ Sigma) . ((canFS Omega) . xm1)) is ext-real Element of ExtREAL
{((canFS Omega) . xm1)} is finite set
r . {((canFS Omega) . xm1)} is ext-real Element of ExtREAL
(R_EAL ((max+ Sigma) . ((canFS Omega) . xm1))) * (r . {((canFS Omega) . xm1)}) is ext-real Element of ExtREAL
(r * am) . xm1 is ext-real Element of ExtREAL
am . xm1 is set
r . (am . xm1) is ext-real Element of ExtREAL
(canFS (dom Sigma)) . xm1 is set
(max+ Sigma) . ((canFS (dom Sigma)) . xm1) is V11() real ext-real Element of REAL
K . xm1 is V11() real ext-real Element of REAL
R_EAL (K . xm1) is ext-real Element of ExtREAL
(R_EAL (K . xm1)) * ((r * am) . xm1) is ext-real Element of ExtREAL
xm1 is set
rng E is finite V72() Element of bool ExtREAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
E . k is ext-real Element of ExtREAL
(canFS Omega) . k is set
{((canFS Omega) . k)} is finite set
r . {((canFS Omega) . k)} is ext-real Element of ExtREAL
(max+ Sigma) . ((canFS Omega) . k) is V11() real ext-real Element of REAL
R_EAL ((max+ Sigma) . ((canFS Omega) . k)) is ext-real Element of ExtREAL
(R_EAL ((max+ Sigma) . ((canFS Omega) . k))) * (r . {((canFS Omega) . k)}) is ext-real Element of ExtREAL
w is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
w * z is V11() real ext-real Element of REAL
dom (canFS (dom (max- Sigma))) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
k is V13() V16( NAT ) V17((Omega)) Function-like finite FinSequence-like FinSubsequence-like V126() FinSequence of (Omega)
rng k is finite V27() Element of bool (Omega)
union (rng k) is finite set
dom k is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
PM is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
r * k is V13() V16( NAT ) V17( ExtREAL ) Function-like finite V62() Element of bool [:NAT,ExtREAL:]
z is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
PM . z is V11() real ext-real Element of REAL
R_EAL (PM . z) is ext-real Element of ExtREAL
(r * k) . z is ext-real Element of ExtREAL
(R_EAL (PM . z)) * ((r * k) . z) is ext-real Element of ExtREAL
z is V13() V16( NAT ) V17( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom z is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
w is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
z . w is ext-real Element of ExtREAL
(canFS Omega) . w is set
(max- Sigma) . ((canFS Omega) . w) is V11() real ext-real Element of REAL
R_EAL ((max- Sigma) . ((canFS Omega) . w)) is ext-real Element of ExtREAL
{((canFS Omega) . w)} is finite set
r . {((canFS Omega) . w)} is ext-real Element of ExtREAL
(R_EAL ((max- Sigma) . ((canFS Omega) . w))) * (r . {((canFS Omega) . w)}) is ext-real Element of ExtREAL
(r * k) . w is ext-real Element of ExtREAL
k . w is set
r . (k . w) is ext-real Element of ExtREAL
PM . w is V11() real ext-real Element of REAL
R_EAL (PM . w) is ext-real Element of ExtREAL
(R_EAL (PM . w)) * ((r * k) . w) is ext-real Element of ExtREAL
w is set
rng z is finite V72() Element of bool ExtREAL
E is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
z . E is ext-real Element of ExtREAL
(canFS Omega) . E is set
{((canFS Omega) . E)} is finite set
r . {((canFS Omega) . E)} is ext-real Element of ExtREAL
(max- Sigma) . ((canFS Omega) . E) is V11() real ext-real Element of REAL
R_EAL ((max- Sigma) . ((canFS Omega) . E)) is ext-real Element of ExtREAL
(R_EAL ((max- Sigma) . ((canFS Omega) . E))) * (r . {((canFS Omega) . E)}) is ext-real Element of ExtREAL
z is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
z * k is V11() real ext-real Element of REAL
Sum E is ext-real Element of ExtREAL
xm1 is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
Sum xm1 is V11() real ext-real Element of REAL
Sum z is ext-real Element of ExtREAL
w is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
Sum w is V11() real ext-real Element of REAL
(- 1) (#) (max- Sigma) is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom ((- 1) (#) (max- Sigma)) is finite Element of bool Omega
r . (dom ((- 1) (#) (max- Sigma))) is ext-real Element of ExtREAL
(dom (max+ Sigma)) /\ (dom ((- 1) (#) (max- Sigma))) is finite Element of bool Omega
(max+ Sigma) + ((- 1) (#) (max- Sigma)) is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
Integral (r,((max+ Sigma) + ((- 1) (#) (max- Sigma)))) is ext-real Element of ExtREAL
R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma))))) is ext-real Element of ExtREAL
max+ (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma)))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma)))))) is ext-real Element of ExtREAL
max- (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma)))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma)))))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma))))))) - (integral+ (r,(max- (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma))))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma)))))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma))))))),K409((integral+ (r,(max- (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma))))))))) is ext-real set
E is finite Element of (Omega)
(max+ Sigma) | E is V13() V16(Omega) V16(E) V16(Omega) V17( REAL ) Function-like finite V61() V62() V63() Element of bool [:Omega,REAL:]
Integral (r,((max+ Sigma) | E)) is ext-real Element of ExtREAL
R_EAL ((max+ Sigma) | E) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL ((max+ Sigma) | E))) is ext-real Element of ExtREAL
max+ (R_EAL ((max+ Sigma) | E)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL ((max+ Sigma) | E)))) is ext-real Element of ExtREAL
max- (R_EAL ((max+ Sigma) | E)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL ((max+ Sigma) | E)))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL ((max+ Sigma) | E))))) - (integral+ (r,(max- (R_EAL ((max+ Sigma) | E))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL ((max+ Sigma) | E)))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL ((max+ Sigma) | E))))),K409((integral+ (r,(max- (R_EAL ((max+ Sigma) | E))))))) is ext-real set
((- 1) (#) (max- Sigma)) | E is V13() V16(Omega) V16(E) V16(Omega) V17( REAL ) Function-like finite V61() V62() V63() Element of bool [:Omega,REAL:]
Integral (r,(((- 1) (#) (max- Sigma)) | E)) is ext-real Element of ExtREAL
R_EAL (((- 1) (#) (max- Sigma)) | E) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL (((- 1) (#) (max- Sigma)) | E))) is ext-real Element of ExtREAL
max+ (R_EAL (((- 1) (#) (max- Sigma)) | E)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL (((- 1) (#) (max- Sigma)) | E)))) is ext-real Element of ExtREAL
max- (R_EAL (((- 1) (#) (max- Sigma)) | E)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL (((- 1) (#) (max- Sigma)) | E)))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL (((- 1) (#) (max- Sigma)) | E))))) - (integral+ (r,(max- (R_EAL (((- 1) (#) (max- Sigma)) | E))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL (((- 1) (#) (max- Sigma)) | E)))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL (((- 1) (#) (max- Sigma)) | E))))),K409((integral+ (r,(max- (R_EAL (((- 1) (#) (max- Sigma)) | E))))))) is ext-real set
(Integral (r,((max+ Sigma) | E))) + (Integral (r,(((- 1) (#) (max- Sigma)) | E))) is ext-real Element of ExtREAL
Omega /\ Omega is finite set
Integral (r,(max+ Sigma)) is ext-real Element of ExtREAL
R_EAL (max+ Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL (max+ Sigma))) is ext-real Element of ExtREAL
max+ (R_EAL (max+ Sigma)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL (max+ Sigma)))) is ext-real Element of ExtREAL
max- (R_EAL (max+ Sigma)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL (max+ Sigma)))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL (max+ Sigma))))) - (integral+ (r,(max- (R_EAL (max+ Sigma))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL (max+ Sigma)))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL (max+ Sigma))))),K409((integral+ (r,(max- (R_EAL (max+ Sigma))))))) is ext-real set
Integral (r,((- 1) (#) (max- Sigma))) is ext-real Element of ExtREAL
R_EAL ((- 1) (#) (max- Sigma)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL ((- 1) (#) (max- Sigma)))) is ext-real Element of ExtREAL
max+ (R_EAL ((- 1) (#) (max- Sigma))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL ((- 1) (#) (max- Sigma))))) is ext-real Element of ExtREAL
max- (R_EAL ((- 1) (#) (max- Sigma))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL ((- 1) (#) (max- Sigma))))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL ((- 1) (#) (max- Sigma)))))) - (integral+ (r,(max- (R_EAL ((- 1) (#) (max- Sigma)))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL ((- 1) (#) (max- Sigma))))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL ((- 1) (#) (max- Sigma)))))),K409((integral+ (r,(max- (R_EAL ((- 1) (#) (max- Sigma)))))))) is ext-real set
(Integral (r,(max+ Sigma))) + (Integral (r,((- 1) (#) (max- Sigma)))) is ext-real Element of ExtREAL
(Integral (r,(max+ Sigma))) + (- (Integral (r,(max- Sigma)))) is ext-real Element of ExtREAL
dom PM is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
k . k is set
PM . k is V11() real ext-real Element of REAL
z is set
(max- Sigma) . z is V11() real ext-real Element of REAL
(canFS (dom (max- Sigma))) . k is set
{((canFS (dom (max- Sigma))) . k)} is finite set
len (canFS (dom Sigma)) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
xm1 - w is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
- w is V13() V16( NAT ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() set
K38(1) is non empty V11() real ext-real non positive negative set
K38(1) (#) w is V13() V16( NAT ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() set
xm1 + (- w) is V13() V16( NAT ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() set
dom (xm1 - w) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
dom xm1 is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
dom w is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
(dom xm1) /\ (dom w) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
xm is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
dom xm is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
len xm1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
len w is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(xm1 - w) . k is V11() real ext-real Element of REAL
xm . k is V11() real ext-real Element of REAL
(max+ Sigma) - (max- Sigma) is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
- (max- Sigma) is V13() V16(Omega) Function-like V61() V62() V63() set
K38(1) (#) (max- Sigma) is V13() V16(Omega) Function-like V61() V62() V63() set
(max+ Sigma) + (- (max- Sigma)) is V13() V16(Omega) Function-like V61() V62() V63() set
(canFS Omega) . k is set
{((canFS Omega) . k)} is finite set
r . {((canFS Omega) . k)} is ext-real Element of ExtREAL
w . k is V11() real ext-real Element of REAL
(max- Sigma) . ((canFS Omega) . k) is V11() real ext-real Element of REAL
R_EAL ((max- Sigma) . ((canFS Omega) . k)) is ext-real Element of ExtREAL
(R_EAL ((max- Sigma) . ((canFS Omega) . k))) * (r . {((canFS Omega) . k)}) is ext-real Element of ExtREAL
z is V11() real ext-real Element of REAL
((max- Sigma) . ((canFS Omega) . k)) * z is V11() real ext-real Element of REAL
rng (canFS Omega) is non empty finite Element of bool Omega
xm1 . k is V11() real ext-real Element of REAL
(max+ Sigma) . ((canFS Omega) . k) is V11() real ext-real Element of REAL
R_EAL ((max+ Sigma) . ((canFS Omega) . k)) is ext-real Element of ExtREAL
(R_EAL ((max+ Sigma) . ((canFS Omega) . k))) * (r . {((canFS Omega) . k)}) is ext-real Element of ExtREAL
((max+ Sigma) . ((canFS Omega) . k)) * z is V11() real ext-real Element of REAL
(((max+ Sigma) . ((canFS Omega) . k)) * z) - (((max- Sigma) . ((canFS Omega) . k)) * z) is V11() real ext-real Element of REAL
K38((((max- Sigma) . ((canFS Omega) . k)) * z)) is V11() real ext-real set
K36((((max+ Sigma) . ((canFS Omega) . k)) * z),K38((((max- Sigma) . ((canFS Omega) . k)) * z))) is V11() real ext-real set
((max+ Sigma) . ((canFS Omega) . k)) - ((max- Sigma) . ((canFS Omega) . k)) is V11() real ext-real Element of REAL
K38(((max- Sigma) . ((canFS Omega) . k))) is V11() real ext-real set
K36(((max+ Sigma) . ((canFS Omega) . k)),K38(((max- Sigma) . ((canFS Omega) . k)))) is V11() real ext-real set
(((max+ Sigma) . ((canFS Omega) . k)) - ((max- Sigma) . ((canFS Omega) . k))) * z is V11() real ext-real Element of REAL
Sigma . ((canFS Omega) . k) is V11() real ext-real Element of REAL
(Sigma . ((canFS Omega) . k)) * z is V11() real ext-real Element of REAL
R_EAL (Sigma . ((canFS Omega) . k)) is ext-real Element of ExtREAL
(R_EAL (Sigma . ((canFS Omega) . k))) * (r . {((canFS Omega) . k)}) is ext-real Element of ExtREAL
(max+ Sigma) - (max- Sigma) is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
- (max- Sigma) is V13() V16(Omega) Function-like V61() V62() V63() set
K38(1) (#) (max- Sigma) is V13() V16(Omega) Function-like V61() V62() V63() set
(max+ Sigma) + (- (max- Sigma)) is V13() V16(Omega) Function-like V61() V62() V63() set
Integral (r,((max+ Sigma) - (max- Sigma))) is ext-real Element of ExtREAL
R_EAL ((max+ Sigma) - (max- Sigma)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL ((max+ Sigma) - (max- Sigma)))) is ext-real Element of ExtREAL
max+ (R_EAL ((max+ Sigma) - (max- Sigma))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL ((max+ Sigma) - (max- Sigma))))) is ext-real Element of ExtREAL
max- (R_EAL ((max+ Sigma) - (max- Sigma))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL ((max+ Sigma) - (max- Sigma))))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL ((max+ Sigma) - (max- Sigma)))))) - (integral+ (r,(max- (R_EAL ((max+ Sigma) - (max- Sigma)))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL ((max+ Sigma) - (max- Sigma))))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL ((max+ Sigma) - (max- Sigma)))))),K409((integral+ (r,(max- (R_EAL ((max+ Sigma) - (max- Sigma)))))))) is ext-real set
(Sum E) - (Sum z) is ext-real Element of ExtREAL
K409((Sum z)) is ext-real set
K408((Sum E),K409((Sum z))) is ext-real set
(Sum xm1) - (Sum w) is V11() real ext-real Element of REAL
K38((Sum w)) is V11() real ext-real set
K36((Sum xm1),K38((Sum w))) is V11() real ext-real set
Sum (xm1 - w) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
xp1 . k is ext-real Element of ExtREAL
(canFS Omega) . k is set
Sigma . ((canFS Omega) . k) is V11() real ext-real Element of REAL
R_EAL (Sigma . ((canFS Omega) . k)) is ext-real Element of ExtREAL
{((canFS Omega) . k)} is finite set
r . {((canFS Omega) . k)} is ext-real Element of ExtREAL
(R_EAL (Sigma . ((canFS Omega) . k))) * (r . {((canFS Omega) . k)}) is ext-real Element of ExtREAL
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
[:(Omega),ExtREAL:] is non empty V13() V62() set
bool [:(Omega),ExtREAL:] is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
dom Sigma is non empty finite Element of bool Omega
X is V13() V16( NAT ) V17(Omega) Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng X is finite Element of bool Omega
dom X is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
len X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Seg (len X) is finite len X -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len X ) } is set
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
X . S is set
{(X . S)} is finite set
S is V13() V16( NAT ) V17( bool Omega) Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool Omega
dom S is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
IX is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
X . K is set
X . IX is set
S . K is set
{(X . K)} is finite set
S . IX is set
{(X . IX)} is finite set
K is V13() V16( NAT ) V17((Omega)) Function-like finite FinSequence-like FinSubsequence-like V126() FinSequence of (Omega)
rng K is finite V27() Element of bool (Omega)
bool (Omega) is non empty finite V27() set
union (rng K) is finite set
IX is set
PMK is set
dom K is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
t is set
K . t is set
X . t is set
{(X . t)} is finite set
IX is set
PMK is set
X . PMK is set
t is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
K . t is set
X . t is set
{(X . t)} is finite set
dom K is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
IX is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
K . IX is set
PMK is Element of Omega
t is Element of Omega
Sigma . PMK is V11() real ext-real Element of REAL
Sigma . t is V11() real ext-real Element of REAL
X . IX is set
{(X . IX)} is finite set
Sigma . (X . IX) is V11() real ext-real Element of REAL
IX is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
X . IX is set
Sigma . (X . IX) is V11() real ext-real Element of REAL
IX is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
dom IX is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
[:(Omega),ExtREAL:] is non empty V13() V62() set
bool [:(Omega),ExtREAL:] is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
r is non empty V13() V16((Omega)) V17( ExtREAL ) Function-like finite total V32((Omega), ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:(Omega),ExtREAL:]
r . Omega is ext-real Element of ExtREAL
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
Integral (r,Sigma) is ext-real Element of ExtREAL
R_EAL Sigma is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral (r,(R_EAL Sigma)) is ext-real Element of ExtREAL
max+ (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL Sigma))) is ext-real Element of ExtREAL
max- (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL Sigma))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL Sigma)))) - (integral+ (r,(max- (R_EAL Sigma)))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL Sigma))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL Sigma)))),K409((integral+ (r,(max- (R_EAL Sigma)))))) is ext-real set
P is V13() V16( NAT ) V17( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
len P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom P is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Sum P is ext-real Element of ExtREAL
X is V13() V16( NAT ) V17(Omega) Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng X is finite Element of bool Omega
len X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom Sigma is non empty finite Element of bool Omega
dom X is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
K is V13() V16( NAT ) V17((Omega)) Function-like finite FinSequence-like FinSubsequence-like V126() FinSequence of (Omega)
rng K is finite V27() Element of bool (Omega)
bool (Omega) is non empty finite V27() set
union (rng K) is finite set
S is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
dom S is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
dom K is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Seg (len X) is finite len X -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len X ) } is set
max- Sigma is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
max+ Sigma is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom (max+ Sigma) is finite Element of bool Omega
PMK is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
X . PMK is set
{(X . PMK)} is finite set
r . {(X . PMK)} is ext-real Element of ExtREAL
PMK is set
rng P is finite V72() Element of bool ExtREAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
P . t is ext-real Element of ExtREAL
X . t is set
{(X . t)} is finite set
r . {(X . t)} is ext-real Element of ExtREAL
Sigma . (X . t) is V11() real ext-real Element of REAL
R_EAL (Sigma . (X . t)) is ext-real Element of ExtREAL
(R_EAL (Sigma . (X . t))) * (r . {(X . t)}) is ext-real Element of ExtREAL
am is V11() real ext-real Element of REAL
ap is V11() real ext-real Element of REAL
am * ap is V11() real ext-real Element of REAL
len K is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Seg (len K) is finite len K -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len K ) } is set
ap is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
K . ap is set
X . ap is set
(max+ Sigma) . (X . ap) is V11() real ext-real Element of REAL
{(X . ap)} is finite set
am is set
(max+ Sigma) . am is V11() real ext-real Element of REAL
ap is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
dom ap is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
am is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
K . am is set
X . am is set
(max- Sigma) . (X . am) is V11() real ext-real Element of REAL
{(X . am)} is finite set
E is set
(max- Sigma) . E is V11() real ext-real Element of REAL
am is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
dom am is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
dom (max- Sigma) is finite Element of bool Omega
- 1 is non empty V11() real ext-real non positive negative Element of REAL
(- 1) (#) (max- Sigma) is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
dom ((- 1) (#) (max- Sigma)) is finite Element of bool Omega
r . (dom ((- 1) (#) (max- Sigma))) is ext-real Element of ExtREAL
(dom (max+ Sigma)) /\ (dom ((- 1) (#) (max- Sigma))) is finite Element of bool Omega
(max+ Sigma) + ((- 1) (#) (max- Sigma)) is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
Integral (r,((max+ Sigma) + ((- 1) (#) (max- Sigma)))) is ext-real Element of ExtREAL
R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma))))) is ext-real Element of ExtREAL
max+ (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma)))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma)))))) is ext-real Element of ExtREAL
max- (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma)))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma)))))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma))))))) - (integral+ (r,(max- (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma))))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma)))))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma))))))),K409((integral+ (r,(max- (R_EAL ((max+ Sigma) + ((- 1) (#) (max- Sigma))))))))) is ext-real set
E is finite Element of (Omega)
(max+ Sigma) | E is V13() V16(Omega) V16(E) V16(Omega) V17( REAL ) Function-like finite V61() V62() V63() Element of bool [:Omega,REAL:]
Integral (r,((max+ Sigma) | E)) is ext-real Element of ExtREAL
R_EAL ((max+ Sigma) | E) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL ((max+ Sigma) | E))) is ext-real Element of ExtREAL
max+ (R_EAL ((max+ Sigma) | E)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL ((max+ Sigma) | E)))) is ext-real Element of ExtREAL
max- (R_EAL ((max+ Sigma) | E)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL ((max+ Sigma) | E)))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL ((max+ Sigma) | E))))) - (integral+ (r,(max- (R_EAL ((max+ Sigma) | E))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL ((max+ Sigma) | E)))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL ((max+ Sigma) | E))))),K409((integral+ (r,(max- (R_EAL ((max+ Sigma) | E))))))) is ext-real set
((- 1) (#) (max- Sigma)) | E is V13() V16(Omega) V16(E) V16(Omega) V17( REAL ) Function-like finite V61() V62() V63() Element of bool [:Omega,REAL:]
Integral (r,(((- 1) (#) (max- Sigma)) | E)) is ext-real Element of ExtREAL
R_EAL (((- 1) (#) (max- Sigma)) | E) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL (((- 1) (#) (max- Sigma)) | E))) is ext-real Element of ExtREAL
max+ (R_EAL (((- 1) (#) (max- Sigma)) | E)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL (((- 1) (#) (max- Sigma)) | E)))) is ext-real Element of ExtREAL
max- (R_EAL (((- 1) (#) (max- Sigma)) | E)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL (((- 1) (#) (max- Sigma)) | E)))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL (((- 1) (#) (max- Sigma)) | E))))) - (integral+ (r,(max- (R_EAL (((- 1) (#) (max- Sigma)) | E))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL (((- 1) (#) (max- Sigma)) | E)))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL (((- 1) (#) (max- Sigma)) | E))))),K409((integral+ (r,(max- (R_EAL (((- 1) (#) (max- Sigma)) | E))))))) is ext-real set
(Integral (r,((max+ Sigma) | E))) + (Integral (r,(((- 1) (#) (max- Sigma)) | E))) is ext-real Element of ExtREAL
R_EAL (- 1) is ext-real Element of ExtREAL
Integral (r,(max- Sigma)) is ext-real Element of ExtREAL
R_EAL (max- Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL (max- Sigma))) is ext-real Element of ExtREAL
max+ (R_EAL (max- Sigma)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL (max- Sigma)))) is ext-real Element of ExtREAL
max- (R_EAL (max- Sigma)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL (max- Sigma)))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL (max- Sigma))))) - (integral+ (r,(max- (R_EAL (max- Sigma))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL (max- Sigma)))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL (max- Sigma))))),K409((integral+ (r,(max- (R_EAL (max- Sigma))))))) is ext-real set
(R_EAL (- 1)) * (Integral (r,(max- Sigma))) is ext-real Element of ExtREAL
R_EAL 1 is ext-real Element of ExtREAL
- (R_EAL 1) is ext-real Element of ExtREAL
(- (R_EAL 1)) * (Integral (r,(max- Sigma))) is ext-real Element of ExtREAL
(R_EAL 1) * (Integral (r,(max- Sigma))) is ext-real Element of ExtREAL
- ((R_EAL 1) * (Integral (r,(max- Sigma)))) is ext-real Element of ExtREAL
- (Integral (r,(max- Sigma))) is ext-real Element of ExtREAL
r * K is V13() V16( NAT ) V17( ExtREAL ) Function-like finite V62() Element of bool [:NAT,ExtREAL:]
xp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
ap . xp is V11() real ext-real Element of REAL
R_EAL (ap . xp) is ext-real Element of ExtREAL
(r * K) . xp is ext-real Element of ExtREAL
(R_EAL (ap . xp)) * ((r * K) . xp) is ext-real Element of ExtREAL
xp is V13() V16( NAT ) V17( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom xp is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
xp1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
xp . xp1 is ext-real Element of ExtREAL
X . xp1 is set
(max+ Sigma) . (X . xp1) is V11() real ext-real Element of REAL
R_EAL ((max+ Sigma) . (X . xp1)) is ext-real Element of ExtREAL
{(X . xp1)} is finite set
r . {(X . xp1)} is ext-real Element of ExtREAL
(R_EAL ((max+ Sigma) . (X . xp1))) * (r . {(X . xp1)}) is ext-real Element of ExtREAL
(r * K) . xp1 is ext-real Element of ExtREAL
K . xp1 is set
r . (K . xp1) is ext-real Element of ExtREAL
ap . xp1 is V11() real ext-real Element of REAL
R_EAL (ap . xp1) is ext-real Element of ExtREAL
(R_EAL (ap . xp1)) * ((r * K) . xp1) is ext-real Element of ExtREAL
xp1 is set
rng xp is finite V72() Element of bool ExtREAL
xm is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
xp . xm is ext-real Element of ExtREAL
X . xm is set
{(X . xm)} is finite set
r . {(X . xm)} is ext-real Element of ExtREAL
(max+ Sigma) . (X . xm) is V11() real ext-real Element of REAL
R_EAL ((max+ Sigma) . (X . xm)) is ext-real Element of ExtREAL
(R_EAL ((max+ Sigma) . (X . xm))) * (r . {(X . xm)}) is ext-real Element of ExtREAL
k is V11() real ext-real Element of REAL
xm1 is V11() real ext-real Element of REAL
k * xm1 is V11() real ext-real Element of REAL
xm is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
am . xm is V11() real ext-real Element of REAL
R_EAL (am . xm) is ext-real Element of ExtREAL
(r * K) . xm is ext-real Element of ExtREAL
(R_EAL (am . xm)) * ((r * K) . xm) is ext-real Element of ExtREAL
xm is V13() V16( NAT ) V17( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom xm is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
xm1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
xm . xm1 is ext-real Element of ExtREAL
X . xm1 is set
(max- Sigma) . (X . xm1) is V11() real ext-real Element of REAL
R_EAL ((max- Sigma) . (X . xm1)) is ext-real Element of ExtREAL
{(X . xm1)} is finite set
r . {(X . xm1)} is ext-real Element of ExtREAL
(R_EAL ((max- Sigma) . (X . xm1))) * (r . {(X . xm1)}) is ext-real Element of ExtREAL
(r * K) . xm1 is ext-real Element of ExtREAL
K . xm1 is set
r . (K . xm1) is ext-real Element of ExtREAL
am . xm1 is V11() real ext-real Element of REAL
R_EAL (am . xm1) is ext-real Element of ExtREAL
(R_EAL (am . xm1)) * ((r * K) . xm1) is ext-real Element of ExtREAL
xm1 is set
rng xm is finite V72() Element of bool ExtREAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
xm . k is ext-real Element of ExtREAL
X . k is set
{(X . k)} is finite set
r . {(X . k)} is ext-real Element of ExtREAL
(max- Sigma) . (X . k) is V11() real ext-real Element of REAL
R_EAL ((max- Sigma) . (X . k)) is ext-real Element of ExtREAL
(R_EAL ((max- Sigma) . (X . k))) * (r . {(X . k)}) is ext-real Element of ExtREAL
w is V11() real ext-real Element of REAL
z is V11() real ext-real Element of REAL
w * z is V11() real ext-real Element of REAL
Sum xp is ext-real Element of ExtREAL
xp1 is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
Sum xp1 is V11() real ext-real Element of REAL
Sum xm is ext-real Element of ExtREAL
xm1 is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
Sum xm1 is V11() real ext-real Element of REAL
PMK is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
dom PMK is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
xp1 - xm1 is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
- xm1 is V13() V16( NAT ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() set
K38(1) is non empty V11() real ext-real non positive negative set
K38(1) (#) xm1 is V13() V16( NAT ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() set
xp1 + (- xm1) is V13() V16( NAT ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() set
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(xp1 - xm1) . k is V11() real ext-real Element of REAL
PMK . k is V11() real ext-real Element of REAL
(max+ Sigma) - (max- Sigma) is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
- (max- Sigma) is V13() V16(Omega) Function-like V61() V62() V63() set
K38(1) (#) (max- Sigma) is V13() V16(Omega) Function-like V61() V62() V63() set
(max+ Sigma) + (- (max- Sigma)) is V13() V16(Omega) Function-like V61() V62() V63() set
X . k is set
{(X . k)} is finite set
r . {(X . k)} is ext-real Element of ExtREAL
xm1 . k is V11() real ext-real Element of REAL
(max- Sigma) . (X . k) is V11() real ext-real Element of REAL
R_EAL ((max- Sigma) . (X . k)) is ext-real Element of ExtREAL
(R_EAL ((max- Sigma) . (X . k))) * (r . {(X . k)}) is ext-real Element of ExtREAL
z is V11() real ext-real Element of REAL
((max- Sigma) . (X . k)) * z is V11() real ext-real Element of REAL
dom xp1 is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
dom xm1 is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
(dom xp1) /\ (dom xm1) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
dom (xp1 - xm1) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
xp1 . k is V11() real ext-real Element of REAL
(max+ Sigma) . (X . k) is V11() real ext-real Element of REAL
R_EAL ((max+ Sigma) . (X . k)) is ext-real Element of ExtREAL
(R_EAL ((max+ Sigma) . (X . k))) * (r . {(X . k)}) is ext-real Element of ExtREAL
((max+ Sigma) . (X . k)) * z is V11() real ext-real Element of REAL
(((max+ Sigma) . (X . k)) * z) - (((max- Sigma) . (X . k)) * z) is V11() real ext-real Element of REAL
K38((((max- Sigma) . (X . k)) * z)) is V11() real ext-real set
K36((((max+ Sigma) . (X . k)) * z),K38((((max- Sigma) . (X . k)) * z))) is V11() real ext-real set
((max+ Sigma) . (X . k)) - ((max- Sigma) . (X . k)) is V11() real ext-real Element of REAL
K38(((max- Sigma) . (X . k))) is V11() real ext-real set
K36(((max+ Sigma) . (X . k)),K38(((max- Sigma) . (X . k)))) is V11() real ext-real set
(((max+ Sigma) . (X . k)) - ((max- Sigma) . (X . k))) * z is V11() real ext-real Element of REAL
Sigma . (X . k) is V11() real ext-real Element of REAL
(Sigma . (X . k)) * z is V11() real ext-real Element of REAL
R_EAL (Sigma . (X . k)) is ext-real Element of ExtREAL
(R_EAL (Sigma . (X . k))) * (r . {(X . k)}) is ext-real Element of ExtREAL
dom (xp1 - xm1) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
dom xp1 is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
dom xm1 is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
(dom xp1) /\ (dom xm1) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
len xp1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
len xm1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Omega /\ Omega is finite set
Integral (r,(max+ Sigma)) is ext-real Element of ExtREAL
R_EAL (max+ Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL (max+ Sigma))) is ext-real Element of ExtREAL
max+ (R_EAL (max+ Sigma)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL (max+ Sigma)))) is ext-real Element of ExtREAL
max- (R_EAL (max+ Sigma)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL (max+ Sigma)))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL (max+ Sigma))))) - (integral+ (r,(max- (R_EAL (max+ Sigma))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL (max+ Sigma)))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL (max+ Sigma))))),K409((integral+ (r,(max- (R_EAL (max+ Sigma))))))) is ext-real set
Integral (r,((- 1) (#) (max- Sigma))) is ext-real Element of ExtREAL
R_EAL ((- 1) (#) (max- Sigma)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL ((- 1) (#) (max- Sigma)))) is ext-real Element of ExtREAL
max+ (R_EAL ((- 1) (#) (max- Sigma))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL ((- 1) (#) (max- Sigma))))) is ext-real Element of ExtREAL
max- (R_EAL ((- 1) (#) (max- Sigma))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL ((- 1) (#) (max- Sigma))))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL ((- 1) (#) (max- Sigma)))))) - (integral+ (r,(max- (R_EAL ((- 1) (#) (max- Sigma)))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL ((- 1) (#) (max- Sigma))))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL ((- 1) (#) (max- Sigma)))))),K409((integral+ (r,(max- (R_EAL ((- 1) (#) (max- Sigma)))))))) is ext-real set
(Integral (r,(max+ Sigma))) + (Integral (r,((- 1) (#) (max- Sigma)))) is ext-real Element of ExtREAL
(Integral (r,(max+ Sigma))) + (- (Integral (r,(max- Sigma)))) is ext-real Element of ExtREAL
(max+ Sigma) - (max- Sigma) is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
- (max- Sigma) is V13() V16(Omega) Function-like V61() V62() V63() set
K38(1) (#) (max- Sigma) is V13() V16(Omega) Function-like V61() V62() V63() set
(max+ Sigma) + (- (max- Sigma)) is V13() V16(Omega) Function-like V61() V62() V63() set
Integral (r,((max+ Sigma) - (max- Sigma))) is ext-real Element of ExtREAL
R_EAL ((max+ Sigma) - (max- Sigma)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral (r,(R_EAL ((max+ Sigma) - (max- Sigma)))) is ext-real Element of ExtREAL
max+ (R_EAL ((max+ Sigma) - (max- Sigma))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL ((max+ Sigma) - (max- Sigma))))) is ext-real Element of ExtREAL
max- (R_EAL ((max+ Sigma) - (max- Sigma))) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL ((max+ Sigma) - (max- Sigma))))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL ((max+ Sigma) - (max- Sigma)))))) - (integral+ (r,(max- (R_EAL ((max+ Sigma) - (max- Sigma)))))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL ((max+ Sigma) - (max- Sigma))))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL ((max+ Sigma) - (max- Sigma)))))),K409((integral+ (r,(max- (R_EAL ((max+ Sigma) - (max- Sigma)))))))) is ext-real set
(Sum xp) - (Sum xm) is ext-real Element of ExtREAL
K409((Sum xm)) is ext-real set
K408((Sum xp),K409((Sum xm))) is ext-real set
(Sum xp1) - (Sum xm1) is V11() real ext-real Element of REAL
K38((Sum xm1)) is V11() real ext-real set
K36((Sum xp1),K38((Sum xm1))) is V11() real ext-real set
Sum (xp1 - xm1) is V11() real ext-real Element of REAL
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
[:(Omega),ExtREAL:] is non empty V13() V62() set
bool [:(Omega),ExtREAL:] is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
r is non empty V13() V16((Omega)) V17( ExtREAL ) Function-like finite total V32((Omega), ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:(Omega),ExtREAL:]
r . Omega is ext-real Element of ExtREAL
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
Integral (r,Sigma) is ext-real Element of ExtREAL
R_EAL Sigma is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral (r,(R_EAL Sigma)) is ext-real Element of ExtREAL
max+ (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max+ (R_EAL Sigma))) is ext-real Element of ExtREAL
max- (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ (r,(max- (R_EAL Sigma))) is ext-real Element of ExtREAL
(integral+ (r,(max+ (R_EAL Sigma)))) - (integral+ (r,(max- (R_EAL Sigma)))) is ext-real Element of ExtREAL
K409((integral+ (r,(max- (R_EAL Sigma))))) is ext-real set
K408((integral+ (r,(max+ (R_EAL Sigma)))),K409((integral+ (r,(max- (R_EAL Sigma)))))) is ext-real set
canFS Omega is non empty V13() V16( NAT ) V17(Omega) Function-like one-to-one finite V33(Omega) V34( NAT ,Omega) FinSequence-like FinSubsequence-like FinSequence of Omega
rng (canFS Omega) is non empty finite Element of bool Omega
len (canFS Omega) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
X is V13() V16( NAT ) V17( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
len X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom X is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Sum X is ext-real Element of ExtREAL
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
canFS Omega is non empty V13() V16( NAT ) V17(Omega) Function-like one-to-one finite V33(Omega) V34( NAT ,Omega) FinSequence-like FinSubsequence-like FinSequence of Omega
r is non empty V13() V16((Omega)) V17( REAL ) Function-like finite total V32((Omega), REAL ) V61() V62() V63() Probability of (Omega)
P2M r is non empty V13() V16((Omega)) V17( ExtREAL ) Function-like finite total V32((Omega), ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:(Omega),ExtREAL:]
[:(Omega),ExtREAL:] is non empty V13() V62() set
bool [:(Omega),ExtREAL:] is non empty set
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
Integral ((P2M r),Sigma) is ext-real Element of ExtREAL
R_EAL Sigma is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral ((P2M r),(R_EAL Sigma)) is ext-real Element of ExtREAL
max+ (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M r),(max+ (R_EAL Sigma))) is ext-real Element of ExtREAL
max- (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M r),(max- (R_EAL Sigma))) is ext-real Element of ExtREAL
(integral+ ((P2M r),(max+ (R_EAL Sigma)))) - (integral+ ((P2M r),(max- (R_EAL Sigma)))) is ext-real Element of ExtREAL
K409((integral+ ((P2M r),(max- (R_EAL Sigma))))) is ext-real set
K408((integral+ ((P2M r),(max+ (R_EAL Sigma)))),K409((integral+ ((P2M r),(max- (R_EAL Sigma)))))) is ext-real set
r . Omega is V11() real ext-real Element of REAL
PM is V13() V16( NAT ) V17( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
len PM is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom PM is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Sum PM is ext-real Element of ExtREAL
(P2M r) . Omega is ext-real Element of ExtREAL
dom (canFS Omega) is non empty finite V71() V72() V73() V74() V75() V76() Element of bool NAT
K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(canFS Omega) . K is set
{((canFS Omega) . K)} is finite set
(P2M r) . {((canFS Omega) . K)} is ext-real Element of ExtREAL
rng (canFS Omega) is non empty finite Element of bool Omega
K is set
rng PM is finite V72() Element of bool ExtREAL
S is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
PM . S is ext-real Element of ExtREAL
Seg (len PM) is finite len PM -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len PM ) } is set
len (canFS Omega) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Seg (len (canFS Omega)) is finite len (canFS Omega) -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len (canFS Omega) ) } is set
(canFS Omega) . S is set
{((canFS Omega) . S)} is finite set
(P2M r) . {((canFS Omega) . S)} is ext-real Element of ExtREAL
Sigma . ((canFS Omega) . S) is V11() real ext-real Element of REAL
R_EAL (Sigma . ((canFS Omega) . S)) is ext-real Element of ExtREAL
(R_EAL (Sigma . ((canFS Omega) . S))) * ((P2M r) . {((canFS Omega) . S)}) is ext-real Element of ExtREAL
IX is V11() real ext-real Element of REAL
K is V11() real ext-real Element of REAL
IX * K is V11() real ext-real Element of REAL
K is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
len K is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom K is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Sum K is V11() real ext-real Element of REAL
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
K . S is V11() real ext-real Element of REAL
(canFS Omega) . S is set
Sigma . ((canFS Omega) . S) is V11() real ext-real Element of REAL
R_EAL (Sigma . ((canFS Omega) . S)) is ext-real Element of ExtREAL
{((canFS Omega) . S)} is finite set
(P2M r) . {((canFS Omega) . S)} is ext-real Element of ExtREAL
(R_EAL (Sigma . ((canFS Omega) . S))) * ((P2M r) . {((canFS Omega) . S)}) is ext-real Element of ExtREAL
r . {((canFS Omega) . S)} is V11() real ext-real Element of REAL
(Sigma . ((canFS Omega) . S)) * (r . {((canFS Omega) . S)}) is V11() real ext-real Element of REAL
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
K . S is V11() real ext-real Element of REAL
(canFS Omega) . S is set
Sigma . ((canFS Omega) . S) is V11() real ext-real Element of REAL
{((canFS Omega) . S)} is finite set
r . {((canFS Omega) . S)} is V11() real ext-real Element of REAL
(Sigma . ((canFS Omega) . S)) * (r . {((canFS Omega) . S)}) is V11() real ext-real Element of REAL
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
r is non empty V13() V16((Omega)) V17( REAL ) Function-like finite total V32((Omega), REAL ) V61() V62() V63() Probability of (Omega)
P2M r is non empty V13() V16((Omega)) V17( ExtREAL ) Function-like finite total V32((Omega), ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:(Omega),ExtREAL:]
[:(Omega),ExtREAL:] is non empty V13() V62() set
bool [:(Omega),ExtREAL:] is non empty set
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
Integral ((P2M r),Sigma) is ext-real Element of ExtREAL
R_EAL Sigma is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral ((P2M r),(R_EAL Sigma)) is ext-real Element of ExtREAL
max+ (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M r),(max+ (R_EAL Sigma))) is ext-real Element of ExtREAL
max- (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M r),(max- (R_EAL Sigma))) is ext-real Element of ExtREAL
(integral+ ((P2M r),(max+ (R_EAL Sigma)))) - (integral+ ((P2M r),(max- (R_EAL Sigma)))) is ext-real Element of ExtREAL
K409((integral+ ((P2M r),(max- (R_EAL Sigma))))) is ext-real set
K408((integral+ ((P2M r),(max+ (R_EAL Sigma)))),K409((integral+ ((P2M r),(max- (R_EAL Sigma)))))) is ext-real set
P is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
len P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom P is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Sum P is V11() real ext-real Element of REAL
X is V13() V16( NAT ) V17(Omega) Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng X is finite Element of bool Omega
len X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
rng P is finite V71() V72() V73() V147() Element of bool REAL
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
K is V13() V16( NAT ) V17( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V62() FinSequence of ExtREAL
dom K is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
K . S is ext-real Element of ExtREAL
X . S is set
Sigma . (X . S) is V11() real ext-real Element of REAL
{(X . S)} is finite set
r . {(X . S)} is V11() real ext-real Element of REAL
(Sigma . (X . S)) * (r . {(X . S)}) is V11() real ext-real Element of REAL
R_EAL (Sigma . (X . S)) is ext-real Element of ExtREAL
(P2M r) . {(X . S)} is ext-real Element of ExtREAL
(R_EAL (Sigma . (X . S))) * ((P2M r) . {(X . S)}) is ext-real Element of ExtREAL
r . Omega is V11() real ext-real Element of REAL
Sum K is ext-real Element of ExtREAL
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
r is non empty V13() V16((Omega)) V17( REAL ) Function-like finite total V32((Omega), REAL ) V61() V62() V63() Probability of (Omega)
P2M r is non empty V13() V16((Omega)) V17( ExtREAL ) Function-like finite total V32((Omega), ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:(Omega),ExtREAL:]
[:(Omega),ExtREAL:] is non empty V13() V62() set
bool [:(Omega),ExtREAL:] is non empty set
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
Integral ((P2M r),Sigma) is ext-real Element of ExtREAL
R_EAL Sigma is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral ((P2M r),(R_EAL Sigma)) is ext-real Element of ExtREAL
max+ (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M r),(max+ (R_EAL Sigma))) is ext-real Element of ExtREAL
max- (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M r),(max- (R_EAL Sigma))) is ext-real Element of ExtREAL
(integral+ ((P2M r),(max+ (R_EAL Sigma)))) - (integral+ ((P2M r),(max- (R_EAL Sigma)))) is ext-real Element of ExtREAL
K409((integral+ ((P2M r),(max- (R_EAL Sigma))))) is ext-real set
K408((integral+ ((P2M r),(max+ (R_EAL Sigma)))),K409((integral+ ((P2M r),(max- (R_EAL Sigma)))))) is ext-real set
canFS Omega is non empty V13() V16( NAT ) V17(Omega) Function-like one-to-one finite V33(Omega) V34( NAT ,Omega) FinSequence-like FinSubsequence-like FinSequence of Omega
len (canFS Omega) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
rng (canFS Omega) is non empty finite Element of bool Omega
X is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
len X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom X is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Sum X is V11() real ext-real Element of REAL
Omega is non empty finite set
K458(Omega) is non empty finite V27() Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
[:NAT,K458(Omega):] is non empty V13() set
bool [:NAT,K458(Omega):] is non empty set
r is non empty V13() V16( NAT ) V17(K458(Omega)) Function-like total V32( NAT ,K458(Omega)) Element of bool [:NAT,K458(Omega):]
Sigma is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . Sigma is finite Element of K458(Omega)
card (r . Sigma) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
Sigma is non empty V13() V16( NAT ) V17( REAL ) Function-like total V32( NAT , REAL ) V61() V62() V63() Element of bool [:NAT,REAL:]
P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Sigma . P is V11() real ext-real Element of REAL
r . P is finite Element of K458(Omega)
card (r . P) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
- 1 is non empty V11() real ext-real non positive negative Element of REAL
P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . X is finite Element of K458(Omega)
r . P is finite Element of K458(Omega)
Sigma . X is V11() real ext-real Element of REAL
card (r . X) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
Sigma . P is V11() real ext-real Element of REAL
card (r . P) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
P is V11() real ext-real set
1 / 2 is non empty V11() real ext-real positive non negative Element of COMPLEX
K39(2) is non empty V11() real ext-real positive non negative set
K37(1,K39(2)) is non empty V11() real ext-real positive non negative set
X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . X is finite Element of K458(Omega)
Sigma . X is V11() real ext-real Element of REAL
(Sigma . X) - P is V11() real ext-real Element of REAL
K38(P) is V11() real ext-real set
K36((Sigma . X),K38(P)) is V11() real ext-real set
abs ((Sigma . X) - P) is V11() real ext-real Element of REAL
P - (Sigma . X) is V11() real ext-real Element of REAL
K38((Sigma . X)) is V11() real ext-real set
K36(P,K38((Sigma . X))) is V11() real ext-real set
abs (P - (Sigma . X)) is V11() real ext-real Element of REAL
card (r . X) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
PM is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Sigma . PM is V11() real ext-real Element of REAL
r . PM is finite Element of K458(Omega)
card (r . PM) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
(Sigma . PM) - P is V11() real ext-real Element of REAL
K36((Sigma . PM),K38(P)) is V11() real ext-real set
abs ((Sigma . PM) - P) is V11() real ext-real Element of REAL
(1 / 2) + (1 / 2) is non empty V11() real ext-real positive non negative Element of COMPLEX
(abs ((Sigma . PM) - P)) + (abs (P - (Sigma . X))) is V11() real ext-real Element of REAL
(Sigma . PM) - (Sigma . X) is V11() real ext-real Element of REAL
K36((Sigma . PM),K38((Sigma . X))) is V11() real ext-real set
abs ((Sigma . PM) - (Sigma . X)) is V11() real ext-real Element of REAL
(Sigma . X) - (Sigma . PM) is V11() real ext-real Element of REAL
K38((Sigma . PM)) is V11() real ext-real set
K36((Sigma . X),K38((Sigma . PM))) is V11() real ext-real set
abs ((Sigma . X) - (Sigma . PM)) is V11() real ext-real Element of REAL
1 + (Sigma . PM) is V11() real ext-real Element of REAL
((Sigma . X) - (Sigma . PM)) + (Sigma . PM) is V11() real ext-real Element of REAL
PM is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . PM is finite Element of K458(Omega)
Omega is non empty finite set
K458(Omega) is non empty finite V27() Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
[:NAT,K458(Omega):] is non empty V13() set
bool [:NAT,K458(Omega):] is non empty set
r is non empty V13() V16( NAT ) V17(K458(Omega)) Function-like total V32( NAT ,K458(Omega)) Element of bool [:NAT,K458(Omega):]
Intersection r is finite Element of bool Omega
Sigma is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . Sigma is finite Element of K458(Omega)
P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . P is finite Element of K458(Omega)
X is set
X is set
PM is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . PM is finite Element of K458(Omega)
PM is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . PM is finite Element of K458(Omega)
PM is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Omega is non empty finite set
K458(Omega) is non empty finite V27() Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
[:NAT,K458(Omega):] is non empty V13() set
bool [:NAT,K458(Omega):] is non empty set
r is non empty V13() V16( NAT ) V17(K458(Omega)) Function-like total V32( NAT ,K458(Omega)) Element of bool [:NAT,K458(Omega):]
Sigma is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . Sigma is finite Element of K458(Omega)
card (r . Sigma) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
Sigma is non empty V13() V16( NAT ) V17( REAL ) Function-like total V32( NAT , REAL ) V61() V62() V63() Element of bool [:NAT,REAL:]
P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . P is finite Element of K458(Omega)
card (r . P) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
(card Omega) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL
Sigma . P is V11() real ext-real Element of REAL
P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . P is finite Element of K458(Omega)
r . X is finite Element of K458(Omega)
Sigma . X is V11() real ext-real Element of REAL
card (r . X) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
Sigma . P is V11() real ext-real Element of REAL
card (r . P) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
P is V11() real ext-real set
1 / 2 is non empty V11() real ext-real positive non negative Element of COMPLEX
K39(2) is non empty V11() real ext-real positive non negative set
K37(1,K39(2)) is non empty V11() real ext-real positive non negative set
X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . X is finite Element of K458(Omega)
Sigma . X is V11() real ext-real Element of REAL
(Sigma . X) - P is V11() real ext-real Element of REAL
K38(P) is V11() real ext-real set
K36((Sigma . X),K38(P)) is V11() real ext-real set
abs ((Sigma . X) - P) is V11() real ext-real Element of REAL
P - (Sigma . X) is V11() real ext-real Element of REAL
K38((Sigma . X)) is V11() real ext-real set
K36(P,K38((Sigma . X))) is V11() real ext-real set
abs (P - (Sigma . X)) is V11() real ext-real Element of REAL
card (r . X) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
PM is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
Sigma . PM is V11() real ext-real Element of REAL
r . PM is finite Element of K458(Omega)
card (r . PM) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
(Sigma . PM) - P is V11() real ext-real Element of REAL
K36((Sigma . PM),K38(P)) is V11() real ext-real set
abs ((Sigma . PM) - P) is V11() real ext-real Element of REAL
(1 / 2) + (1 / 2) is non empty V11() real ext-real positive non negative Element of COMPLEX
(abs ((Sigma . PM) - P)) + (abs (P - (Sigma . X))) is V11() real ext-real Element of REAL
(Sigma . PM) - (Sigma . X) is V11() real ext-real Element of REAL
K36((Sigma . PM),K38((Sigma . X))) is V11() real ext-real set
abs ((Sigma . PM) - (Sigma . X)) is V11() real ext-real Element of REAL
1 + (Sigma . X) is V11() real ext-real Element of REAL
((Sigma . PM) - (Sigma . X)) + (Sigma . X) is V11() real ext-real Element of REAL
PM is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . PM is finite Element of K458(Omega)
Omega is non empty finite set
K458(Omega) is non empty finite V27() Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
[:NAT,K458(Omega):] is non empty V13() set
bool [:NAT,K458(Omega):] is non empty set
r is non empty V13() V16( NAT ) V17(K458(Omega)) Function-like total V32( NAT ,K458(Omega)) Element of bool [:NAT,K458(Omega):]
Union r is finite Element of bool Omega
Sigma is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . Sigma is finite Element of K458(Omega)
P is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r . X is set
K is set
S is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . S is finite Element of K458(Omega)
r . P is set
PM is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . PM is finite Element of K458(Omega)
r . P is set
PM is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
r . PM is finite Element of K458(Omega)
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
[:(Omega),REAL:] is non empty V13() V61() V62() V63() set
bool [:(Omega),REAL:] is non empty set
r is non empty V13() V16((Omega)) V17( REAL ) Function-like finite total V32((Omega), REAL ) V61() V62() V63() Element of bool [:(Omega),REAL:]
Sigma is finite Event of (Omega)
P is finite Event of (Omega)
Sigma \/ P is finite Element of (Omega)
r . (Sigma \/ P) is V11() real ext-real Element of REAL
r . Sigma is V11() real ext-real Element of REAL
r . P is V11() real ext-real Element of REAL
(r . Sigma) + (r . P) is V11() real ext-real Element of REAL
prob (Sigma \/ P) is V11() real ext-real Element of REAL
card (Sigma \/ P) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
K41((card (Sigma \/ P)),(card Omega)) is V11() real ext-real non negative set
K39((card Omega)) is V11() real ext-real non negative set
K37((card (Sigma \/ P)),K39((card Omega))) is V11() real ext-real non negative set
prob Sigma is V11() real ext-real Element of REAL
card Sigma is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
K41((card Sigma),(card Omega)) is V11() real ext-real non negative set
K37((card Sigma),K39((card Omega))) is V11() real ext-real non negative set
prob P is V11() real ext-real Element of REAL
card P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
K41((card P),(card Omega)) is V11() real ext-real non negative set
K37((card P),K39((card Omega))) is V11() real ext-real non negative set
(prob Sigma) + (prob P) is V11() real ext-real Element of REAL
Sigma /\ P is finite Element of (Omega)
prob (Sigma /\ P) is V11() real ext-real Element of REAL
card (Sigma /\ P) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
K41((card (Sigma /\ P)),(card Omega)) is V11() real ext-real non negative set
K37((card (Sigma /\ P)),K39((card Omega))) is V11() real ext-real non negative set
((prob Sigma) + (prob P)) - (prob (Sigma /\ P)) is V11() real ext-real Element of REAL
K38((prob (Sigma /\ P))) is V11() real ext-real set
K36(((prob Sigma) + (prob P)),K38((prob (Sigma /\ P)))) is V11() real ext-real set
((prob Sigma) + (prob P)) - 0 is V11() real ext-real Element of REAL
K38(0) is V11() real ext-real non positive set
K36(((prob Sigma) + (prob P)),K38(0)) is V11() real ext-real set
(r . Sigma) + (prob P) is V11() real ext-real Element of REAL
Sigma is finite Event of (Omega)
r . Sigma is V11() real ext-real Element of REAL
prob Sigma is V11() real ext-real Element of REAL
card Sigma is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
K41((card Sigma),(card Omega)) is V11() real ext-real non negative set
K39((card Omega)) is V11() real ext-real non negative set
K37((card Sigma),K39((card Omega))) is V11() real ext-real non negative set
K458(Omega) is non empty finite V27() Element of bool (bool Omega)
[:NAT,K458(Omega):] is non empty V13() set
bool [:NAT,K458(Omega):] is non empty set
Sigma is non empty V13() V16( NAT ) V17((Omega)) V17(K458(Omega)) Function-like total V32( NAT ,K458(Omega)) Element of bool [:NAT,K458(Omega):]
r * Sigma is non empty V13() V16( NAT ) V17( REAL ) Function-like total V32( NAT , REAL ) V61() V62() V63() Element of bool [:NAT,REAL:]
lim (r * Sigma) is V11() real ext-real Element of REAL
Intersection Sigma is finite Element of bool Omega
r . (Intersection Sigma) is V11() real ext-real Element of REAL
P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom Sigma is non empty V71() V72() V73() V74() V75() V76() Element of bool NAT
(r * Sigma) . X is V11() real ext-real Element of REAL
Sigma . X is finite Element of (Omega)
r . (Sigma . X) is V11() real ext-real Element of REAL
r . Omega is V11() real ext-real Element of REAL
[#] Omega is non empty non proper finite Element of bool Omega
prob ([#] Omega) is V11() real ext-real Element of REAL
card ([#] Omega) is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
K41((card ([#] Omega)),(card Omega)) is V11() real ext-real non negative set
K39((card Omega)) is V11() real ext-real non negative set
K37((card ([#] Omega)),K39((card Omega))) is V11() real ext-real non negative set
Sigma is finite Element of bool Omega
r . Sigma is V11() real ext-real Element of REAL
prob Sigma is V11() real ext-real Element of REAL
card Sigma is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
K41((card Sigma),(card Omega)) is V11() real ext-real non negative set
K37((card Sigma),K39((card Omega))) is V11() real ext-real non negative set
r is non empty V13() V16((Omega)) V17( REAL ) Function-like finite total V32((Omega), REAL ) V61() V62() V63() Probability of (Omega)
Sigma is non empty V13() V16((Omega)) V17( REAL ) Function-like finite total V32((Omega), REAL ) V61() V62() V63() Probability of (Omega)
P is set
r . P is V11() real ext-real Element of REAL
X is finite Element of bool Omega
prob X is V11() real ext-real Element of REAL
card X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
K41((card X),(card Omega)) is V11() real ext-real non negative set
K39((card Omega)) is V11() real ext-real non negative set
K37((card X),K39((card Omega))) is V11() real ext-real non negative set
Sigma . P is V11() real ext-real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is Element of r
chi (Sigma,Omega) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
dom (chi (Sigma,Omega)) is Element of bool Omega
rng (chi (Sigma,Omega)) is V72() Element of bool ExtREAL
P is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
R_EAL P is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
P is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
Sigma + P is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
X is Element of r
PM is Element of r
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
P is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
Sigma + P is V13() V16(Omega) Function-like total V61() V62() V63() set
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
P is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
Sigma - P is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
- P is V13() V16(Omega) Function-like total V61() V62() V63() set
K38(1) is non empty V11() real ext-real non positive negative set
K38(1) (#) P is V13() V16(Omega) Function-like total V61() V62() V63() set
Sigma + (- P) is V13() V16(Omega) Function-like total V61() V62() V63() set
X is Element of r
dom P is non empty Element of bool Omega
PM is Element of r
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
P is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
Sigma - P is V13() V16(Omega) Function-like total V61() V62() V63() set
- P is V13() V16(Omega) Function-like total V61() V62() V63() set
K38(1) is non empty V11() real ext-real non positive negative set
K38(1) (#) P is V13() V16(Omega) Function-like total V61() V62() V63() set
Sigma + (- P) is V13() V16(Omega) Function-like total V61() V62() V63() set
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
P is V11() real ext-real Element of REAL
P (#) Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
X is Element of r
dom Sigma is non empty Element of bool Omega
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
P is V11() real ext-real Element of REAL
P (#) Sigma is V13() V16(Omega) Function-like total V61() V62() V63() set
Omega is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
r is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
R_EAL r is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Sigma is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
R_EAL Sigma is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
(R_EAL r) (#) (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
r (#) Sigma is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
R_EAL (r (#) Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
dom ((R_EAL r) (#) (R_EAL Sigma)) is Element of bool Omega
bool Omega is non empty set
dom (R_EAL r) is Element of bool Omega
dom (R_EAL Sigma) is Element of bool Omega
(dom (R_EAL r)) /\ (dom (R_EAL Sigma)) is Element of bool Omega
dom (r (#) Sigma) is Element of bool Omega
P is set
((R_EAL r) (#) (R_EAL Sigma)) . P is ext-real Element of ExtREAL
(R_EAL r) . P is ext-real Element of ExtREAL
(R_EAL Sigma) . P is ext-real Element of ExtREAL
((R_EAL r) . P) * ((R_EAL Sigma) . P) is ext-real Element of ExtREAL
r . P is V11() real ext-real Element of REAL
Sigma . P is V11() real ext-real Element of REAL
(r . P) * (Sigma . P) is V11() real ext-real Element of REAL
(r (#) Sigma) . P is V11() real ext-real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
P is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
Sigma (#) P is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
X is Element of r
R_EAL Sigma is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
dom (R_EAL Sigma) is Element of bool Omega
R_EAL P is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
dom (R_EAL P) is Element of bool Omega
(dom (R_EAL Sigma)) /\ (dom (R_EAL P)) is Element of bool Omega
PM is Element of r
(R_EAL Sigma) (#) (R_EAL P) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
R_EAL (Sigma (#) P) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
P is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
Sigma (#) P is V13() V16(Omega) Function-like total V61() V62() V63() set
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
P is V11() real ext-real set
Sigma to_power P is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
dom Sigma is non empty Element of bool Omega
rng (Sigma to_power P) is V71() V72() V73() Element of bool REAL
dom (Sigma to_power P) is Element of bool Omega
X is Element of r
Omega is non empty set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
r is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
abs r is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
Sigma is set
dom (abs r) is Element of bool Omega
bool Omega is non empty set
(abs r) . Sigma is V11() real ext-real Element of REAL
r . Sigma is V11() real ext-real Element of REAL
abs (r . Sigma) is V11() real ext-real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
abs Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
P is Element of r
dom Sigma is non empty Element of bool Omega
R_EAL Sigma is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
|.(R_EAL Sigma).| is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
R_EAL (abs Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
|.Sigma.| is V13() V16(Omega) Function-like total V61() V62() V63() set
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
(Omega,r,Sigma) is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
P is V11() real ext-real set
(Omega,r,Sigma) to_power P is V13() V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
Sigma is non empty V13() V16(r) V17( REAL ) Function-like total V32(r, REAL ) V61() V62() V63() Probability of r
P2M Sigma is non empty V13() V16(r) V17( ExtREAL ) Function-like total V32(r, ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:r,ExtREAL:]
[:r,ExtREAL:] is non empty V13() V62() set
bool [:r,ExtREAL:] is non empty set
Integral ((P2M Sigma),P) is ext-real Element of ExtREAL
R_EAL P is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral ((P2M Sigma),(R_EAL P)) is ext-real Element of ExtREAL
max+ (R_EAL P) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M Sigma),(max+ (R_EAL P))) is ext-real Element of ExtREAL
max- (R_EAL P) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M Sigma),(max- (R_EAL P))) is ext-real Element of ExtREAL
(integral+ ((P2M Sigma),(max+ (R_EAL P)))) - (integral+ ((P2M Sigma),(max- (R_EAL P)))) is ext-real Element of ExtREAL
K409((integral+ ((P2M Sigma),(max- (R_EAL P))))) is ext-real set
K408((integral+ ((P2M Sigma),(max+ (R_EAL P)))),K409((integral+ ((P2M Sigma),(max- (R_EAL P)))))) is ext-real set
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(r) V17( REAL ) Function-like total V32(r, REAL ) V61() V62() V63() Probability of r
P is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
(Omega,r,Sigma,P) is V11() real ext-real Element of REAL
X is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
(Omega,r,P,X) is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
(Omega,r,Sigma,(Omega,r,P,X)) is V11() real ext-real Element of REAL
(Omega,r,Sigma,X) is V11() real ext-real Element of REAL
(Omega,r,Sigma,P) + (Omega,r,Sigma,X) is V11() real ext-real Element of REAL
P2M Sigma is non empty V13() V16(r) V17( ExtREAL ) Function-like total V32(r, ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:r,ExtREAL:]
[:r,ExtREAL:] is non empty V13() V62() set
bool [:r,ExtREAL:] is non empty set
Integral ((P2M Sigma),P) is ext-real Element of ExtREAL
R_EAL P is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral ((P2M Sigma),(R_EAL P)) is ext-real Element of ExtREAL
max+ (R_EAL P) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M Sigma),(max+ (R_EAL P))) is ext-real Element of ExtREAL
max- (R_EAL P) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M Sigma),(max- (R_EAL P))) is ext-real Element of ExtREAL
(integral+ ((P2M Sigma),(max+ (R_EAL P)))) - (integral+ ((P2M Sigma),(max- (R_EAL P)))) is ext-real Element of ExtREAL
K409((integral+ ((P2M Sigma),(max- (R_EAL P))))) is ext-real set
K408((integral+ ((P2M Sigma),(max+ (R_EAL P)))),K409((integral+ ((P2M Sigma),(max- (R_EAL P)))))) is ext-real set
Integral ((P2M Sigma),X) is ext-real Element of ExtREAL
R_EAL X is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral ((P2M Sigma),(R_EAL X)) is ext-real Element of ExtREAL
max+ (R_EAL X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M Sigma),(max+ (R_EAL X))) is ext-real Element of ExtREAL
max- (R_EAL X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M Sigma),(max- (R_EAL X))) is ext-real Element of ExtREAL
(integral+ ((P2M Sigma),(max+ (R_EAL X)))) - (integral+ ((P2M Sigma),(max- (R_EAL X)))) is ext-real Element of ExtREAL
K409((integral+ ((P2M Sigma),(max- (R_EAL X))))) is ext-real set
K408((integral+ ((P2M Sigma),(max+ (R_EAL X)))),K409((integral+ ((P2M Sigma),(max- (R_EAL X)))))) is ext-real set
dom P is non empty Element of bool Omega
dom X is non empty Element of bool Omega
(dom P) /\ (dom X) is Element of bool Omega
Integral ((P2M Sigma),(Omega,r,P,X)) is ext-real Element of ExtREAL
R_EAL (Omega,r,P,X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral ((P2M Sigma),(R_EAL (Omega,r,P,X))) is ext-real Element of ExtREAL
max+ (R_EAL (Omega,r,P,X)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M Sigma),(max+ (R_EAL (Omega,r,P,X)))) is ext-real Element of ExtREAL
max- (R_EAL (Omega,r,P,X)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M Sigma),(max- (R_EAL (Omega,r,P,X)))) is ext-real Element of ExtREAL
(integral+ ((P2M Sigma),(max+ (R_EAL (Omega,r,P,X))))) - (integral+ ((P2M Sigma),(max- (R_EAL (Omega,r,P,X))))) is ext-real Element of ExtREAL
K409((integral+ ((P2M Sigma),(max- (R_EAL (Omega,r,P,X)))))) is ext-real set
K408((integral+ ((P2M Sigma),(max+ (R_EAL (Omega,r,P,X))))),K409((integral+ ((P2M Sigma),(max- (R_EAL (Omega,r,P,X))))))) is ext-real set
K is Element of r
P | K is V13() V16(Omega) V16(K) V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
Integral ((P2M Sigma),(P | K)) is ext-real Element of ExtREAL
R_EAL (P | K) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral ((P2M Sigma),(R_EAL (P | K))) is ext-real Element of ExtREAL
max+ (R_EAL (P | K)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M Sigma),(max+ (R_EAL (P | K)))) is ext-real Element of ExtREAL
max- (R_EAL (P | K)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M Sigma),(max- (R_EAL (P | K)))) is ext-real Element of ExtREAL
(integral+ ((P2M Sigma),(max+ (R_EAL (P | K))))) - (integral+ ((P2M Sigma),(max- (R_EAL (P | K))))) is ext-real Element of ExtREAL
K409((integral+ ((P2M Sigma),(max- (R_EAL (P | K)))))) is ext-real set
K408((integral+ ((P2M Sigma),(max+ (R_EAL (P | K))))),K409((integral+ ((P2M Sigma),(max- (R_EAL (P | K))))))) is ext-real set
X | K is V13() V16(Omega) V16(K) V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
Integral ((P2M Sigma),(X | K)) is ext-real Element of ExtREAL
R_EAL (X | K) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral ((P2M Sigma),(R_EAL (X | K))) is ext-real Element of ExtREAL
max+ (R_EAL (X | K)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M Sigma),(max+ (R_EAL (X | K)))) is ext-real Element of ExtREAL
max- (R_EAL (X | K)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M Sigma),(max- (R_EAL (X | K)))) is ext-real Element of ExtREAL
(integral+ ((P2M Sigma),(max+ (R_EAL (X | K))))) - (integral+ ((P2M Sigma),(max- (R_EAL (X | K))))) is ext-real Element of ExtREAL
K409((integral+ ((P2M Sigma),(max- (R_EAL (X | K)))))) is ext-real set
K408((integral+ ((P2M Sigma),(max+ (R_EAL (X | K))))),K409((integral+ ((P2M Sigma),(max- (R_EAL (X | K))))))) is ext-real set
(Integral ((P2M Sigma),(P | K))) + (Integral ((P2M Sigma),(X | K))) is ext-real Element of ExtREAL
(Integral ((P2M Sigma),P)) + (Integral ((P2M Sigma),X)) is ext-real Element of ExtREAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is V11() real ext-real Element of REAL
Sigma is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like total V32(Sigma, REAL ) V61() V62() V63() Probability of Sigma
X is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,Sigma)
(Omega,Sigma,X,r) is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,Sigma)
(Omega,Sigma,P,(Omega,Sigma,X,r)) is V11() real ext-real Element of REAL
(Omega,Sigma,P,X) is V11() real ext-real Element of REAL
r * (Omega,Sigma,P,X) is V11() real ext-real Element of REAL
P2M P is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like total V32(Sigma, ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]
[:Sigma,ExtREAL:] is non empty V13() V62() set
bool [:Sigma,ExtREAL:] is non empty set
Integral ((P2M P),X) is ext-real Element of ExtREAL
R_EAL X is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral ((P2M P),(R_EAL X)) is ext-real Element of ExtREAL
max+ (R_EAL X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M P),(max+ (R_EAL X))) is ext-real Element of ExtREAL
max- (R_EAL X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M P),(max- (R_EAL X))) is ext-real Element of ExtREAL
(integral+ ((P2M P),(max+ (R_EAL X)))) - (integral+ ((P2M P),(max- (R_EAL X)))) is ext-real Element of ExtREAL
K409((integral+ ((P2M P),(max- (R_EAL X))))) is ext-real set
K408((integral+ ((P2M P),(max+ (R_EAL X)))),K409((integral+ ((P2M P),(max- (R_EAL X)))))) is ext-real set
Integral ((P2M P),(Omega,Sigma,X,r)) is ext-real Element of ExtREAL
R_EAL (Omega,Sigma,X,r) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral ((P2M P),(R_EAL (Omega,Sigma,X,r))) is ext-real Element of ExtREAL
max+ (R_EAL (Omega,Sigma,X,r)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M P),(max+ (R_EAL (Omega,Sigma,X,r)))) is ext-real Element of ExtREAL
max- (R_EAL (Omega,Sigma,X,r)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M P),(max- (R_EAL (Omega,Sigma,X,r)))) is ext-real Element of ExtREAL
(integral+ ((P2M P),(max+ (R_EAL (Omega,Sigma,X,r))))) - (integral+ ((P2M P),(max- (R_EAL (Omega,Sigma,X,r))))) is ext-real Element of ExtREAL
K409((integral+ ((P2M P),(max- (R_EAL (Omega,Sigma,X,r)))))) is ext-real set
K408((integral+ ((P2M P),(max+ (R_EAL (Omega,Sigma,X,r))))),K409((integral+ ((P2M P),(max- (R_EAL (Omega,Sigma,X,r))))))) is ext-real set
R_EAL r is ext-real Element of ExtREAL
(R_EAL r) * (Integral ((P2M P),X)) is ext-real Element of ExtREAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
Sigma is non empty V13() V16(r) V17( REAL ) Function-like total V32(r, REAL ) V61() V62() V63() Probability of r
P is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
(Omega,r,Sigma,P) is V11() real ext-real Element of REAL
X is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
(Omega,r,P,X) is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
- X is V13() V16(Omega) Function-like total V61() V62() V63() set
K38(1) (#) X is V13() V16(Omega) Function-like total V61() V62() V63() set
P + (- X) is V13() V16(Omega) Function-like total V61() V62() V63() set
(Omega,r,Sigma,(Omega,r,P,X)) is V11() real ext-real Element of REAL
(Omega,r,Sigma,X) is V11() real ext-real Element of REAL
(Omega,r,Sigma,P) - (Omega,r,Sigma,X) is V11() real ext-real Element of REAL
K38((Omega,r,Sigma,X)) is V11() real ext-real set
K36((Omega,r,Sigma,P),K38((Omega,r,Sigma,X))) is V11() real ext-real set
P2M Sigma is non empty V13() V16(r) V17( ExtREAL ) Function-like total V32(r, ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:r,ExtREAL:]
[:r,ExtREAL:] is non empty V13() V62() set
bool [:r,ExtREAL:] is non empty set
- 1 is non empty V11() real ext-real non positive negative Element of REAL
(Omega,r,X,(- 1)) is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,r)
(Omega,r,Sigma,(Omega,r,X,(- 1))) is V11() real ext-real Element of REAL
(Omega,r,Sigma,P) + (Omega,r,Sigma,(Omega,r,X,(- 1))) is V11() real ext-real Element of REAL
(- 1) * (Omega,r,Sigma,X) is V11() real ext-real Element of REAL
(Omega,r,Sigma,P) + ((- 1) * (Omega,r,Sigma,X)) is V11() real ext-real Element of REAL
Omega is non empty finite set
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
r is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() Element of bool [:Omega,REAL:]
dom r is non empty finite Element of bool Omega
P is finite Element of (Omega)
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
r is non empty V13() V16((Omega)) V17( REAL ) Function-like finite total V32((Omega), REAL ) V61() V62() V63() Probability of (Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() (Omega,(Omega))
P2M r is non empty V13() V16((Omega)) V17( ExtREAL ) Function-like finite total V32((Omega), ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:(Omega),ExtREAL:]
[:(Omega),ExtREAL:] is non empty V13() V62() set
bool [:(Omega),ExtREAL:] is non empty set
dom Sigma is non empty finite Element of bool Omega
(P2M r) . (dom Sigma) is ext-real Element of ExtREAL
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
r is non empty V13() V16((Omega)) V17( REAL ) Function-like finite total V32((Omega), REAL ) V61() V62() V63() Probability of (Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() (Omega,(Omega))
(Omega,(Omega),r,Sigma) is V11() real ext-real Element of REAL
P is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
len P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom P is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Sum P is V11() real ext-real Element of REAL
X is V13() V16( NAT ) V17(Omega) Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng X is finite Element of bool Omega
len X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
P2M r is non empty V13() V16((Omega)) V17( ExtREAL ) Function-like finite total V32((Omega), ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:(Omega),ExtREAL:]
[:(Omega),ExtREAL:] is non empty V13() V62() set
bool [:(Omega),ExtREAL:] is non empty set
Integral ((P2M r),Sigma) is ext-real Element of ExtREAL
R_EAL Sigma is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral ((P2M r),(R_EAL Sigma)) is ext-real Element of ExtREAL
max+ (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M r),(max+ (R_EAL Sigma))) is ext-real Element of ExtREAL
max- (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M r),(max- (R_EAL Sigma))) is ext-real Element of ExtREAL
(integral+ ((P2M r),(max+ (R_EAL Sigma)))) - (integral+ ((P2M r),(max- (R_EAL Sigma)))) is ext-real Element of ExtREAL
K409((integral+ ((P2M r),(max- (R_EAL Sigma))))) is ext-real set
K408((integral+ ((P2M r),(max+ (R_EAL Sigma)))),K409((integral+ ((P2M r),(max- (R_EAL Sigma)))))) is ext-real set
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
r is non empty V13() V16((Omega)) V17( REAL ) Function-like finite total V32((Omega), REAL ) V61() V62() V63() Probability of (Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() (Omega,(Omega))
(Omega,(Omega),r,Sigma) is V11() real ext-real Element of REAL
P2M r is non empty V13() V16((Omega)) V17( ExtREAL ) Function-like finite total V32((Omega), ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:(Omega),ExtREAL:]
[:(Omega),ExtREAL:] is non empty V13() V62() set
bool [:(Omega),ExtREAL:] is non empty set
Integral ((P2M r),Sigma) is ext-real Element of ExtREAL
R_EAL Sigma is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral ((P2M r),(R_EAL Sigma)) is ext-real Element of ExtREAL
max+ (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M r),(max+ (R_EAL Sigma))) is ext-real Element of ExtREAL
max- (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M r),(max- (R_EAL Sigma))) is ext-real Element of ExtREAL
(integral+ ((P2M r),(max+ (R_EAL Sigma)))) - (integral+ ((P2M r),(max- (R_EAL Sigma)))) is ext-real Element of ExtREAL
K409((integral+ ((P2M r),(max- (R_EAL Sigma))))) is ext-real set
K408((integral+ ((P2M r),(max+ (R_EAL Sigma)))),K409((integral+ ((P2M r),(max- (R_EAL Sigma)))))) is ext-real set
P is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
len P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
X is V13() V16( NAT ) V17(Omega) Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng X is finite Element of bool Omega
len X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom P is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Sum P is V11() real ext-real Element of REAL
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
r is non empty V13() V16((Omega)) V17( REAL ) Function-like finite total V32((Omega), REAL ) V61() V62() V63() Probability of (Omega)
Sigma is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() (Omega,(Omega))
(Omega,(Omega),r,Sigma) is V11() real ext-real Element of REAL
P2M r is non empty V13() V16((Omega)) V17( ExtREAL ) Function-like finite total V32((Omega), ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:(Omega),ExtREAL:]
[:(Omega),ExtREAL:] is non empty V13() V62() set
bool [:(Omega),ExtREAL:] is non empty set
Integral ((P2M r),Sigma) is ext-real Element of ExtREAL
R_EAL Sigma is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral ((P2M r),(R_EAL Sigma)) is ext-real Element of ExtREAL
max+ (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M r),(max+ (R_EAL Sigma))) is ext-real Element of ExtREAL
max- (R_EAL Sigma) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M r),(max- (R_EAL Sigma))) is ext-real Element of ExtREAL
(integral+ ((P2M r),(max+ (R_EAL Sigma)))) - (integral+ ((P2M r),(max- (R_EAL Sigma)))) is ext-real Element of ExtREAL
K409((integral+ ((P2M r),(max- (R_EAL Sigma))))) is ext-real set
K408((integral+ ((P2M r),(max+ (R_EAL Sigma)))),K409((integral+ ((P2M r),(max- (R_EAL Sigma)))))) is ext-real set
P is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
len P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
X is V13() V16( NAT ) V17(Omega) Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng X is finite Element of bool Omega
len X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom P is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Sum P is V11() real ext-real Element of REAL
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
(Omega) is non empty V13() V16((Omega)) V17( REAL ) Function-like finite total V32((Omega), REAL ) V61() V62() V63() Probability of (Omega)
r is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() (Omega,(Omega))
(Omega,(Omega),(Omega),r) is V11() real ext-real Element of REAL
Sigma is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
len Sigma is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom Sigma is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Sum Sigma is V11() real ext-real Element of REAL
(Sum Sigma) / (card Omega) is V11() real ext-real Element of COMPLEX
K39((card Omega)) is V11() real ext-real non negative set
K37((Sum Sigma),K39((card Omega))) is V11() real ext-real set
P is V13() V16( NAT ) V17(Omega) Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng P is finite Element of bool Omega
len P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
PM is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
len PM is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom PM is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
dom P is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Seg (len P) is finite len P -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len P ) } is set
P . K is set
{(P . K)} is finite set
(Omega) . {(P . K)} is V11() real ext-real Element of REAL
S is finite 1 -element Element of bool Omega
prob S is V11() real ext-real Element of REAL
card S is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
K41((card S),(card Omega)) is V11() real ext-real non negative set
K37((card S),K39((card Omega))) is V11() real ext-real non negative set
1 / (card Omega) is V11() real ext-real non negative Element of COMPLEX
K37(1,K39((card Omega))) is V11() real ext-real non negative set
(1 / (card Omega)) (#) Sigma is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() Element of bool [:NAT,REAL:]
((1 / (card Omega)) (#) Sigma) . K is V11() real ext-real Element of REAL
Sigma . K is V11() real ext-real Element of REAL
(1 / (card Omega)) * (Sigma . K) is V11() real ext-real Element of REAL
r . (P . K) is V11() real ext-real Element of REAL
(1 / (card Omega)) * (r . (P . K)) is V11() real ext-real Element of REAL
PM . K is V11() real ext-real Element of REAL
dom ((1 / (card Omega)) (#) Sigma) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Sum ((1 / (card Omega)) (#) Sigma) is V11() set
Omega is non empty finite set
(Omega) is non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
bool Omega is non empty finite V27() set
bool (bool Omega) is non empty finite V27() set
card Omega is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
(Omega) is non empty V13() V16((Omega)) V17( REAL ) Function-like finite total V32((Omega), REAL ) V61() V62() V63() Probability of (Omega)
r is non empty V13() V16(Omega) V17( REAL ) Function-like finite total V32(Omega, REAL ) V61() V62() V63() (Omega,(Omega))
(Omega,(Omega),(Omega),r) is V11() real ext-real Element of REAL
P is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
len P is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
X is V13() V16( NAT ) V17(Omega) Function-like finite FinSequence-like FinSubsequence-like FinSequence of Omega
rng X is finite Element of bool Omega
len X is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom P is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Sum P is V11() real ext-real Element of REAL
PM is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() FinSequence of REAL
len PM is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT
dom PM is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
K is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
dom X is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Seg (len X) is finite len X -element V71() V72() V73() V74() V75() V76() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of NAT : ( 1 <= b1 & b1 <= len X ) } is set
X . K is set
{(X . K)} is finite set
(Omega) . {(X . K)} is V11() real ext-real Element of REAL
S is finite 1 -element Element of bool Omega
prob S is V11() real ext-real Element of REAL
card S is epsilon-transitive epsilon-connected ordinal natural V11() real V39() ext-real non negative V52() V71() V72() V73() V74() V75() V76() Element of omega
K41((card S),(card Omega)) is V11() real ext-real non negative set
K39((card Omega)) is V11() real ext-real non negative set
K37((card S),K39((card Omega))) is V11() real ext-real non negative set
1 / (card Omega) is V11() real ext-real non negative Element of COMPLEX
K37(1,K39((card Omega))) is V11() real ext-real non negative set
(1 / (card Omega)) (#) PM is V13() V16( NAT ) V17( REAL ) Function-like finite FinSequence-like FinSubsequence-like V61() V62() V63() Element of bool [:NAT,REAL:]
((1 / (card Omega)) (#) PM) . K is V11() real ext-real Element of REAL
PM . K is V11() real ext-real Element of REAL
(1 / (card Omega)) * (PM . K) is V11() real ext-real Element of REAL
r . (X . K) is V11() real ext-real Element of REAL
(1 / (card Omega)) * (r . (X . K)) is V11() real ext-real Element of REAL
P . K is V11() real ext-real Element of REAL
Sum PM is V11() real ext-real Element of REAL
(Sum PM) / (card Omega) is V11() real ext-real Element of COMPLEX
K37((Sum PM),K39((card Omega))) is V11() real ext-real set
dom ((1 / (card Omega)) (#) PM) is finite V71() V72() V73() V74() V75() V76() Element of bool NAT
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
r is V11() real ext-real Element of REAL
Sigma is non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like total V32(Sigma, REAL ) V61() V62() V63() Probability of Sigma
X is non empty V13() V16(Omega) V17( REAL ) Function-like total V32(Omega, REAL ) V61() V62() V63() (Omega,Sigma)
{ b1 where b1 is Element of Omega : r <= X . b1 } is set
P . { b1 where b1 is Element of Omega : r <= X . b1 } is V11() real ext-real Element of REAL
(Omega,Sigma,P,X) is V11() real ext-real Element of REAL
(Omega,Sigma,P,X) / r is V11() real ext-real Element of COMPLEX
K39(r) is V11() real ext-real set
K37((Omega,Sigma,P,X),K39(r)) is V11() real ext-real set
P2M P is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like total V32(Sigma, ExtREAL ) V62() V70() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]
[:Sigma,ExtREAL:] is non empty V13() V62() set
bool [:Sigma,ExtREAL:] is non empty set
S is Element of Sigma
K is set
great_eq_dom (X,r) is set
S /\ (great_eq_dom (X,r)) is Element of bool Omega
dom X is non empty Element of bool Omega
X . K is V11() real ext-real Element of REAL
K is set
IX is Element of Omega
X . IX is V11() real ext-real Element of REAL
IX is Element of Omega
X . IX is V11() real ext-real Element of REAL
K is Element of Sigma
X | K is V13() V16(Omega) V16(K) V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
[:Omega,REAL:] is non empty V13() V61() V62() V63() set
bool [:Omega,REAL:] is non empty set
Integral ((P2M P),(X | K)) is ext-real Element of ExtREAL
R_EAL (X | K) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is non empty V13() V62() set
bool [:Omega,ExtREAL:] is non empty set
Integral ((P2M P),(R_EAL (X | K))) is ext-real Element of ExtREAL
max+ (R_EAL (X | K)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M P),(max+ (R_EAL (X | K)))) is ext-real Element of ExtREAL
max- (R_EAL (X | K)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M P),(max- (R_EAL (X | K)))) is ext-real Element of ExtREAL
(integral+ ((P2M P),(max+ (R_EAL (X | K))))) - (integral+ ((P2M P),(max- (R_EAL (X | K))))) is ext-real Element of ExtREAL
K409((integral+ ((P2M P),(max- (R_EAL (X | K)))))) is ext-real set
K408((integral+ ((P2M P),(max+ (R_EAL (X | K))))),K409((integral+ ((P2M P),(max- (R_EAL (X | K))))))) is ext-real set
X | S is V13() V16(Omega) V16(S) V16(Omega) V17( REAL ) Function-like V61() V62() V63() Element of bool [:Omega,REAL:]
Integral ((P2M P),(X | S)) is ext-real Element of ExtREAL
R_EAL (X | S) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral ((P2M P),(R_EAL (X | S))) is ext-real Element of ExtREAL
max+ (R_EAL (X | S)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M P),(max+ (R_EAL (X | S)))) is ext-real Element of ExtREAL
max- (R_EAL (X | S)) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M P),(max- (R_EAL (X | S)))) is ext-real Element of ExtREAL
(integral+ ((P2M P),(max+ (R_EAL (X | S))))) - (integral+ ((P2M P),(max- (R_EAL (X | S))))) is ext-real Element of ExtREAL
K409((integral+ ((P2M P),(max- (R_EAL (X | S)))))) is ext-real set
K408((integral+ ((P2M P),(max+ (R_EAL (X | S))))),K409((integral+ ((P2M P),(max- (R_EAL (X | S))))))) is ext-real set
Integral ((P2M P),X) is ext-real Element of ExtREAL
R_EAL X is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
Integral ((P2M P),(R_EAL X)) is ext-real Element of ExtREAL
max+ (R_EAL X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M P),(max+ (R_EAL X))) is ext-real Element of ExtREAL
max- (R_EAL X) is V13() V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
integral+ ((P2M P),(max- (R_EAL X))) is ext-real Element of ExtREAL
(integral+ ((P2M P),(max+ (R_EAL X)))) - (integral+ ((P2M P),(max- (R_EAL X)))) is ext-real Element of ExtREAL
K409((integral+ ((P2M P),(max- (R_EAL X))))) is ext-real set
K408((integral+ ((P2M P),(max+ (R_EAL X)))),K409((integral+ ((P2M P),(max- (R_EAL X)))))) is ext-real set
(P2M P) . K is ext-real Element of ExtREAL
t is Element of Omega
X . t is V11() real ext-real Element of REAL
ap is Element of Omega
X . ap is V11() real ext-real Element of REAL
R_EAL r is ext-real Element of ExtREAL
(R_EAL r) * ((P2M P) . K) is ext-real Element of ExtREAL
PMK is V11() real ext-real Element of REAL
r * PMK is V11() real ext-real Element of REAL
(r * PMK) / r is V11() real ext-real Element of COMPLEX
K37((r * PMK),K39(r)) is V11() real ext-real set
IX is V11() real ext-real Element of REAL
IX / r is V11() real ext-real Element of COMPLEX
K37(IX,K39(r)) is V11() real ext-real set