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

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

{ b

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

{ b

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

{ b

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