:: RANDOM_1 semantic presentation

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
is non empty V13() V62() set
bool 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

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
is non empty V13() V61() V62() V63() set
bool is non empty set
is non empty V13() V61() V62() V63() set
bool is non empty set
bool () is non empty set
is non empty V13() V61() set
bool is non empty set
is non empty V13() V61() set

is non empty V13() V61() V62() V63() set
bool is non empty set
is non empty V13() V17( RAT ) V61() V62() V63() set
bool is non empty set
is non empty V13() V17( RAT ) V61() V62() V63() set
bool is non empty set
is non empty V13() V17( RAT ) V17( INT ) V61() V62() V63() set
bool is non empty set
is non empty V13() V17( RAT ) V17( INT ) V61() V62() V63() set
bool is non empty set
is non empty V13() V17( RAT ) V17( INT ) V61() V62() V63() V64() set
is non empty V13() V17( RAT ) V17( INT ) V61() V62() V63() V64() set
bool 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

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

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)
is non empty V13() V62() set
bool 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
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) * (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

(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)
is non empty V13() V62() set
bool 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
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) * (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)
is non empty V13() V62() set
bool 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
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) * (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

(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)
is non empty V13() V62() set
bool 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
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) * (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)
is non empty V13() V62() set
bool 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
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

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

dom PM 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

dom (R_EAL Sigma) is Element of bool Omega
S is set
(R_EAL Sigma) . S is ext-real Element of ExtREAL

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

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

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 . 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

dom X is finite V71() V72() V73() V74() V75() V76() Element of bool NAT

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

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

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

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)
is non empty V13() V62() set
bool 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
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 () 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 ()) /\ (dom (chi (X,Omega))) is Element of bool Omega
X /\ Omega 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
PM is set
(() (#) (chi (X,Omega))) . PM is ext-real Element of ExtREAL
() . PM is ext-real Element of ExtREAL
(chi (X,Omega)) . PM is ext-real Element of ExtREAL
(() . PM) * ((chi (X,Omega)) . PM) is ext-real Element of ExtREAL

(() . PM) * () is ext-real Element of ExtREAL
P . PM is V11() real ext-real Element of REAL
(() (#) (chi (X,Omega))) | X is V13() V16(Omega) V16(X) V16(Omega) V17( ExtREAL ) Function-like V62() Element of bool [:Omega,ExtREAL:]
((() (#) (chi (X,Omega))) | X) . PM is ext-real Element of ExtREAL
rng () is V72() Element of bool ExtREAL
dom ((() (#) (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)
is non empty V13() V62() set
bool 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
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

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

(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

(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

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

K . S is set
(canFS (dom r)) . S is set
{((canFS (dom r)) . S)} is finite 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

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

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)
is non empty V13() V62() set
bool 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
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

r * (canFS (dom r)) is V13() V16( NAT ) V17( REAL ) Function-like finite V61() V62() V63() Element of bool
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

r * (canFS (dom r)) is V13() V16( NAT ) V17( REAL ) Function-like finite V61() V62() V63() Element of bool
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
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
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

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

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

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

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

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

- () is ext-real Element of ExtREAL
(- ()) * (Integral (r,(max- Sigma))) is ext-real Element of ExtREAL
() * (Integral (r,(max- Sigma))) is ext-real Element of ExtREAL
- (() * (Integral (r,(max- Sigma)))) is ext-real Element of ExtREAL
- (Integral (r,(max- Sigma))) is ext-real Element of ExtREAL

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

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

(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

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

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

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 . 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

dom z is finite V71() V72() V73() V74() V75() V76() Element of bool NAT

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

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 xm1 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