begin
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
PartFunc of ,)
for
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
a being ( ( ) (
V11()
real ext-real )
Real) st
f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
c= dom f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
PartFunc of ,) : ( ( ) ( )
Element of
Trivial-SigmaField b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
M : ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
< +infty : ( ( ) ( non
empty non
real ext-real positive non
negative )
set ) & ( for
x being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) st
x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) )
in E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
a : ( ( ) (
V11()
real ext-real )
Real)
<= f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
PartFunc of ,)
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) ) holds
(R_EAL a : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
* (M : ( ( Function-like V32(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V72() ) set ) ) V70() nonnegative sigma-additive ) ( non empty V13() V16(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V17( ExtREAL : ( ( ) ( non empty V72() ) set ) ) Function-like total V32(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V72() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
<= Integral (
M : ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( Function-like ) ( V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( ExtREAL : ( ( ) ( non empty V72() ) set ) ) Function-like V62() ) PartFunc of ,) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V16(
b5 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) )
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
Element of
Trivial-SigmaField [:b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V72() ) set ) :] : ( ( ) ( non
empty V13()
V62() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,)
for
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
a being ( ( ) (
V11()
real ext-real )
Real) st
f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
c= dom f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) ( )
Element of
Trivial-SigmaField b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
M : ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
< +infty : ( ( ) ( non
empty non
real ext-real positive non
negative )
set ) & ( for
x being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) st
x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) )
in E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
a : ( ( ) (
V11()
real ext-real )
Real)
<= f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,)
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) holds
(R_EAL a : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
* (M : ( ( Function-like V32(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V72() ) set ) ) V70() nonnegative sigma-additive ) ( non empty V13() V16(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V17( ExtREAL : ( ( ) ( non empty V72() ) set ) ) Function-like total V32(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V72() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
<= Integral (
M : ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( Function-like ) ( V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like V61() V62() V63() ) PartFunc of ,) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V16(
b5 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) )
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
Element of
Trivial-SigmaField [:b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) :] : ( ( ) ( non
empty V13()
V61()
V62()
V63() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
PartFunc of ,)
for
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
a being ( ( ) (
V11()
real ext-real )
Real) st
f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
c= dom f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
PartFunc of ,) : ( ( ) ( )
Element of
Trivial-SigmaField b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
M : ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
< +infty : ( ( ) ( non
empty non
real ext-real positive non
negative )
set ) & ( for
x being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) st
x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) )
in E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
PartFunc of ,)
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
<= a : ( ( ) (
V11()
real ext-real )
Real) ) holds
Integral (
M : ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( Function-like ) ( V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( ExtREAL : ( ( ) ( non empty V72() ) set ) ) Function-like V62() ) PartFunc of ,) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V16(
b5 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) )
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
Element of
Trivial-SigmaField [:b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V72() ) set ) :] : ( ( ) ( non
empty V13()
V62() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
<= (R_EAL a : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
* (M : ( ( Function-like V32(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V72() ) set ) ) V70() nonnegative sigma-additive ) ( non empty V13() V16(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V17( ExtREAL : ( ( ) ( non empty V72() ) set ) ) Function-like total V32(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V72() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,)
for
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
a being ( ( ) (
V11()
real ext-real )
Real) st
f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
c= dom f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) ( )
Element of
Trivial-SigmaField b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
M : ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
< +infty : ( ( ) ( non
empty non
real ext-real positive non
negative )
set ) & ( for
x being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) st
x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) )
in E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,)
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
<= a : ( ( ) (
V11()
real ext-real )
Real) ) holds
Integral (
M : ( (
Function-like V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( Function-like ) ( V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like V61() V62() V63() ) PartFunc of ,) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V16(
b5 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) )
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
Element of
Trivial-SigmaField [:b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) :] : ( ( ) ( non
empty V13()
V61()
V62()
V63() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
<= (R_EAL a : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
* (M : ( ( Function-like V32(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V72() ) set ) ) V70() nonnegative sigma-additive ) ( non empty V13() V16(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V17( ExtREAL : ( ( ) ( non empty V72() ) set ) ) Function-like total V32(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V72() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) ;
begin
theorem
for
Omega being ( ( non
empty finite ) ( non
empty finite )
set )
for
f being ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) ex
F being ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ) ex
s being ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
dom b2 : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
dom f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) ) st
(
dom f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) )
= union (rng F : ( ( V126() ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() ) Element of Trivial-SigmaField REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) : ( ( ) ( non empty ) set ) ) ) V17( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) Function-like finite FinSequence-like FinSubsequence-like V126() ) Finite_Sep_Sequence of Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) ) : ( ( ) (
finite V27() )
Element of
Trivial-SigmaField (Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) ( non
empty finite V27() )
set ) ) : ( ( ) (
finite )
set ) &
dom F : ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
= dom s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
dom b2 : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
dom b2 : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
dom b2 : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
dom b2 : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) ) is
one-to-one &
rng s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
dom b2 : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
dom b2 : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) ) : ( ( ) (
finite )
Element of
Trivial-SigmaField (dom b2 : ( ( Function-like ) ( V13() V16(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like V61() V62() V63() ) PartFunc of ,) ) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) : ( ( ) ( non
empty finite V27() )
set ) )
= dom f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) &
len s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
dom b2 : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
dom b2 : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
= card (dom f : ( ( Function-like ) ( V13() V16(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like V61() V62() V63() ) PartFunc of ,) ) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
omega : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
set ) ) & ( for
k being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) st
k : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat)
in dom F : ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
F : ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
. k : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) : ( ( ) ( )
set )
= {(s : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() ) Element of Trivial-SigmaField REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) : ( ( ) ( non empty ) set ) ) ) V17( dom b2 : ( ( Function-like ) ( V13() V16(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like V61() V62() V63() ) PartFunc of ,) : ( ( ) ( finite ) Element of Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty finite V27() ) set ) ) ) Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of dom b2 : ( ( Function-like ) ( V13() V16(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like V61() V62() V63() ) PartFunc of ,) : ( ( ) ( finite ) Element of Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty finite V27() ) set ) ) ) . k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Nat) ) : ( ( ) ( ) set ) } : ( ( ) (
finite )
set ) ) & ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat)
for
x,
y being ( ( ) ( )
Element of
Omega : ( ( non
empty finite ) ( non
empty finite )
set ) ) st
n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat)
in dom F : ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
x : ( ( ) ( )
Element of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
in F : ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) : ( ( ) ( )
set ) &
y : ( ( ) ( )
Element of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
in F : ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) : ( ( ) ( )
set ) holds
f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,)
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
= f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,)
. y : ( ( ) ( )
Element of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ) ;
theorem
for
Omega being ( ( non
empty finite ) ( non
empty finite )
set )
for
M being ( (
Function-like V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
Trivial-SigmaField Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
for
f being ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) st
dom f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) )
<> {} : ( ( ) ( )
set ) &
M : ( (
Function-like V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
. (dom f : ( ( Function-like ) ( V13() V16(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like V61() V62() V63() ) PartFunc of ,) ) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
< +infty : ( ( ) ( non
empty non
real ext-real positive non
negative )
set ) holds
f : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ) ;
theorem
for
Omega being ( ( non
empty finite ) ( non
empty finite )
set )
for
M being ( (
Function-like V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
Trivial-SigmaField Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
for
f being ( (
Function-like V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ( non
empty V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Function of
Omega : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
for
x being ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
for
s being ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
Omega : ( ( non
empty finite ) ( non
empty finite )
set ) ) st
s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) is
one-to-one &
rng s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) )
= Omega : ( ( non
empty finite ) ( non
empty finite )
set ) holds
ex
F being ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ) ex
a being ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V61()
V62()
V63() )
FinSequence of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) st
(
dom f : ( (
Function-like V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ( non
empty V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Function of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) : ( ( ) ( non
empty finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) )
= union (rng F : ( ( V126() ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() ) Element of Trivial-SigmaField REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) : ( ( ) ( non empty ) set ) ) ) V17( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) Function-like finite FinSequence-like FinSubsequence-like V126() ) Finite_Sep_Sequence of Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) ) : ( ( ) (
finite V27() )
Element of
Trivial-SigmaField (Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) ( non
empty finite V27() )
set ) ) : ( ( ) (
finite )
set ) &
dom a : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V61()
V62()
V63() )
FinSequence of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
= dom s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
dom F : ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
= dom s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) & ( for
k being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) st
k : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat)
in dom F : ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
F : ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
. k : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) : ( ( ) ( )
set )
= {(s : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() ) Element of Trivial-SigmaField REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) : ( ( ) ( non empty ) set ) ) ) V17(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) . k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Nat) ) : ( ( ) ( ) set ) } : ( ( ) (
finite )
set ) ) & ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat)
for
x,
y being ( ( ) ( )
Element of
Omega : ( ( non
empty finite ) ( non
empty finite )
set ) ) st
n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat)
in dom F : ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
x : ( ( ) ( )
Element of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
in F : ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) : ( ( ) ( )
set ) &
y : ( ( ) ( )
Element of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
in F : ( (
V126() ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like V126() )
Finite_Sep_Sequence of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) : ( ( ) ( )
set ) holds
f : ( (
Function-like V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ( non
empty V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Function of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
= f : ( (
Function-like V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ( non
empty V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Function of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
. y : ( ( ) ( )
Element of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ) ;
theorem
for
Omega being ( ( non
empty finite ) ( non
empty finite )
set )
for
M being ( (
Function-like V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
Trivial-SigmaField Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
for
f being ( (
Function-like V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ( non
empty V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Function of
Omega : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
for
x being ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
for
s being ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
Omega : ( ( non
empty finite ) ( non
empty finite )
set ) ) st
M : ( (
Function-like V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
. Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
< +infty : ( ( ) ( non
empty non
real ext-real positive non
negative )
set ) &
len x : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
= card Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
omega : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
set ) ) &
s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) is
one-to-one &
rng s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) )
= Omega : ( ( non
empty finite ) ( non
empty finite )
set ) &
len s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
= card Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
omega : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
set ) ) & ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) st
n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat)
in dom x : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
x : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
= (R_EAL (f : ( ( Function-like V32(b1 : ( ( non empty finite ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) ) ( non empty V13() V16(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like finite total V32(b1 : ( ( non empty finite ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Function of b1 : ( ( non empty finite ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) . (s : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() ) Element of Trivial-SigmaField REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) : ( ( ) ( non empty ) set ) ) ) V17(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Nat) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
* (M : ( ( Function-like V32( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) , ExtREAL : ( ( ) ( non empty V72() ) set ) ) V70() nonnegative sigma-additive ) ( non empty V13() V16( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) V17( ExtREAL : ( ( ) ( non empty V72() ) set ) ) Function-like finite total V32( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) , ExtREAL : ( ( ) ( non empty V72() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) . {(s : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() ) Element of Trivial-SigmaField REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) : ( ( ) ( non empty ) set ) ) ) V17(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Nat) ) : ( ( ) ( ) set ) } : ( ( ) ( finite ) set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) ) holds
Integral (
M : ( (
Function-like V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ) ,
f : ( (
Function-like V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ( non
empty V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Function of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
= Sum x : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) ;
theorem
for
Omega being ( ( non
empty finite ) ( non
empty finite )
set )
for
M being ( (
Function-like V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
Trivial-SigmaField Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
for
f being ( (
Function-like V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ( non
empty V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Function of
Omega : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) st
M : ( (
Function-like V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
. Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
< +infty : ( ( ) ( non
empty non
real ext-real positive non
negative )
set ) holds
ex
x being ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) ex
s being ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
Omega : ( ( non
empty finite ) ( non
empty finite )
set ) ) st
(
len x : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
= card Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
omega : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
set ) ) &
s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) is
one-to-one &
rng s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) )
= Omega : ( ( non
empty finite ) ( non
empty finite )
set ) &
len s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
= card Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
omega : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
set ) ) & ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) st
n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat)
in dom x : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
x : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
= (R_EAL (f : ( ( Function-like V32(b1 : ( ( non empty finite ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) ) ( non empty V13() V16(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like finite total V32(b1 : ( ( non empty finite ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Function of b1 : ( ( non empty finite ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) . (s : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() ) Element of Trivial-SigmaField REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) : ( ( ) ( non empty ) set ) ) ) V17(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Nat) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
* (M : ( ( Function-like V32( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) , ExtREAL : ( ( ) ( non empty V72() ) set ) ) V70() nonnegative sigma-additive ) ( non empty V13() V16( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) V17( ExtREAL : ( ( ) ( non empty V72() ) set ) ) Function-like finite total V32( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) , ExtREAL : ( ( ) ( non empty V72() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) . {(s : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() ) Element of Trivial-SigmaField REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) : ( ( ) ( non empty ) set ) ) ) V17(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Nat) ) : ( ( ) ( ) set ) } : ( ( ) ( finite ) set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) ) &
Integral (
M : ( (
Function-like V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ) ,
f : ( (
Function-like V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ( non
empty V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Function of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
= Sum x : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) ) ) ;
theorem
for
Omega being ( ( non
empty finite ) ( non
empty finite )
set )
for
P being ( ( ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
Trivial-SigmaField Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
for
f being ( (
Function-like V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ( non
empty V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Function of
Omega : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
for
x being ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V61()
V62()
V63() )
FinSequence of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
for
s being ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
Omega : ( ( non
empty finite ) ( non
empty finite )
set ) ) st
len x : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V61()
V62()
V63() )
FinSequence of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
= card Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
omega : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
set ) ) &
s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) is
one-to-one &
rng s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) )
= Omega : ( ( non
empty finite ) ( non
empty finite )
set ) &
len s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
= card Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
omega : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
set ) ) & ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) st
n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat)
in dom x : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V61()
V62()
V63() )
FinSequence of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
x : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V61()
V62()
V63() )
FinSequence of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
= (f : ( ( Function-like V32(b1 : ( ( non empty finite ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) ) ( non empty V13() V16(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like finite total V32(b1 : ( ( non empty finite ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Function of b1 : ( ( non empty finite ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) . (s : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() ) Element of Trivial-SigmaField REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) : ( ( ) ( non empty ) set ) ) ) V17(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Nat) ) : ( ( ) ( ) set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
* (P : ( ( ) ( non empty V13() V16( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like finite total V32( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Probability of Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) . {(s : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() ) Element of Trivial-SigmaField REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) : ( ( ) ( non empty ) set ) ) ) V17(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Nat) ) : ( ( ) ( ) set ) } : ( ( ) ( finite ) set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) holds
Integral (
(P2M P : ( ( ) ( non empty V13() V16( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like finite total V32( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Probability of Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) ) : ( (
Function-like V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
Element of
Trivial-SigmaField [:(Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ,ExtREAL : ( ( ) ( non empty V72() ) set ) :] : ( ( ) ( non
empty V13()
V62() )
set ) : ( ( ) ( non
empty )
set ) ) ,
f : ( (
Function-like V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ( non
empty V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Function of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
= Sum x : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V61()
V62()
V63() )
FinSequence of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ;
theorem
for
Omega being ( ( non
empty finite ) ( non
empty finite )
set )
for
P being ( ( ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
Trivial-SigmaField Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
for
f being ( (
Function-like V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ( non
empty V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Function of
Omega : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ex
F being ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V61()
V62()
V63() )
FinSequence of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ex
s being ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
Omega : ( ( non
empty finite ) ( non
empty finite )
set ) ) st
(
len F : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V61()
V62()
V63() )
FinSequence of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
= card Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
omega : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
set ) ) &
s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) is
one-to-one &
rng s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
finite )
Element of
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) ( non
empty finite V27() )
set ) )
= Omega : ( ( non
empty finite ) ( non
empty finite )
set ) &
len s : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
= card Omega : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
omega : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
set ) ) & ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) st
n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat)
in dom F : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V61()
V62()
V63() )
FinSequence of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) : ( ( ) (
finite V71()
V72()
V73()
V74()
V75()
V76() )
Element of
Trivial-SigmaField NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
F : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V61()
V62()
V63() )
FinSequence of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
= (f : ( ( Function-like V32(b1 : ( ( non empty finite ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) ) ( non empty V13() V16(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like finite total V32(b1 : ( ( non empty finite ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Function of b1 : ( ( non empty finite ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) . (s : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() ) Element of Trivial-SigmaField REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) : ( ( ) ( non empty ) set ) ) ) V17(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Nat) ) : ( ( ) ( ) set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
* (P : ( ( ) ( non empty V13() V16( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like finite total V32( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Probability of Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) . {(s : ( ( ) ( V13() V16( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() ) Element of Trivial-SigmaField REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) : ( ( ) ( non empty ) set ) ) ) V17(b1 : ( ( non empty finite ) ( non empty finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative ) Nat) ) : ( ( ) ( ) set ) } : ( ( ) ( finite ) set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) &
Integral (
(P2M P : ( ( ) ( non empty V13() V16( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like finite total V32( Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Probability of Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ) ) : ( (
Function-like V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V70()
nonnegative sigma-additive ) ( non
empty V13()
V16(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like finite total V32(
Trivial-SigmaField b1 : ( ( non
empty finite ) ( non
empty finite )
set ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty finite V27()
V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
V62()
V70()
nonnegative sigma-additive )
Element of
Trivial-SigmaField [:(Trivial-SigmaField b1 : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty finite V27() V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty finite ) ( non empty finite ) set ) ) ,ExtREAL : ( ( ) ( non empty V72() ) set ) :] : ( ( ) ( non
empty V13()
V62() )
set ) : ( ( ) ( non
empty )
set ) ) ,
f : ( (
Function-like V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ( non
empty V13()
V16(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite total V32(
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Function of
b1 : ( ( non
empty finite ) ( non
empty finite )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
= Sum F : ( ( ) (
V13()
V16(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V61()
V62()
V63() )
FinSequence of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ) ;
theorem
for
Omega being ( ( non
empty ) ( non
empty )
set )
for
f,
g being ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
PartFunc of ,) holds
(R_EAL f : ( ( Function-like ) ( V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like V61() V62() V63() ) PartFunc of ,) ) : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
Element of
Trivial-SigmaField [:b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V72() ) set ) :] : ( ( ) ( non
empty V13()
V62() )
set ) : ( ( ) ( non
empty )
set ) )
(#) (R_EAL g : ( ( Function-like ) ( V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like V61() V62() V63() ) PartFunc of ,) ) : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
Element of
Trivial-SigmaField [:b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V72() ) set ) :] : ( ( ) ( non
empty V13()
V62() )
set ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
Element of
Trivial-SigmaField [:b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V72() ) set ) :] : ( ( ) ( non
empty V13()
V62() )
set ) : ( ( ) ( non
empty )
set ) )
= R_EAL (f : ( ( Function-like ) ( V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like V61() V62() V63() ) PartFunc of ,) (#) g : ( ( Function-like ) ( V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like V61() V62() V63() ) PartFunc of ,) ) : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like V61()
V62()
V63() )
Element of
Trivial-SigmaField [:b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) :] : ( ( ) ( non
empty V13()
V61()
V62()
V63() )
set ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
ExtREAL : ( ( ) ( non
empty V72() )
set ) )
Function-like V62() )
Element of
Trivial-SigmaField [:b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V72() ) set ) :] : ( ( ) ( non
empty V13()
V62() )
set ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
Omega being ( ( non
empty ) ( non
empty )
set )
for
Sigma being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
Omega : ( ( non
empty ) ( non
empty )
set ) )
for
P being ( ( ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
Sigma : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
Sigma : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
f : ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
is_integrable_on P : ( ( ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
is_integrable_on P : ( ( ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
expect (
(f : ( ( ) ( non empty V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Real-Valued-Random-Variable of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) + g : ( ( ) ( non empty V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Real-Valued-Random-Variable of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
P : ( ( ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
= (expect (f : ( ( ) ( non empty V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Real-Valued-Random-Variable of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,P : ( ( ) ( non empty V13() V16(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) )) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
+ (expect (g : ( ( ) ( non empty V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Real-Valued-Random-Variable of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,P : ( ( ) ( non empty V13() V16(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) )) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ;
theorem
for
Omega being ( ( non
empty ) ( non
empty )
set )
for
r being ( ( ) (
V11()
real ext-real )
Real)
for
Sigma being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
Omega : ( ( non
empty ) ( non
empty )
set ) )
for
P being ( ( ) ( non
empty V13()
V16(
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
Sigma : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
Sigma : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
f : ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
is_integrable_on P : ( ( ) ( non
empty V13()
V16(
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
expect (
(r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( ) ( non empty V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Real-Valued-Random-Variable of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
P : ( ( ) ( non
empty V13()
V16(
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
= r : ( ( ) (
V11()
real ext-real )
Real)
* (expect (f : ( ( ) ( non empty V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Real-Valued-Random-Variable of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,P : ( ( ) ( non empty V13() V16(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Probability of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) )) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ;
theorem
for
Omega being ( ( non
empty ) ( non
empty )
set )
for
Sigma being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
Omega : ( ( non
empty ) ( non
empty )
set ) )
for
P being ( ( ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
Sigma : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
Sigma : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
f : ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
is_integrable_on P : ( ( ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
is_integrable_on P : ( ( ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
expect (
(f : ( ( ) ( non empty V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Real-Valued-Random-Variable of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) - g : ( ( ) ( non empty V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Real-Valued-Random-Variable of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
P : ( ( ) ( non
empty V13()
V16(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
= (expect (f : ( ( ) ( non empty V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Real-Valued-Random-Variable of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,P : ( ( ) ( non empty V13() V16(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) )) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
- (expect (g : ( ( ) ( non empty V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Real-Valued-Random-Variable of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,P : ( ( ) ( non empty V13() V16(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) )) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) ) ;
theorem
for
Omega being ( ( non
empty ) ( non
empty )
set )
for
r being ( ( ) (
V11()
real ext-real )
Real)
for
Sigma being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
Omega : ( ( non
empty ) ( non
empty )
set ) )
for
P being ( ( ) ( non
empty V13()
V16(
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
Sigma : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
X being ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
Sigma : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real V39()
ext-real non
negative V52()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V71()
V72()
V73()
V74()
V75()
V76()
V77() )
Element of
Trivial-SigmaField REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) : ( ( ) ( non
empty )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) &
X : ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) is
nonnegative &
X : ( ( ) ( non
empty V13()
V16(
b1 : ( ( non
empty ) ( non
empty )
set ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Real-Valued-Random-Variable of
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
is_integrable_on P : ( ( ) ( non
empty V13()
V16(
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
P : ( ( ) ( non
empty V13()
V16(
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
V17(
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
Function-like total V32(
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
V61()
V62()
V63() )
Probability of
b3 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V35()
V36()
V37()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. { t : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) where t is ( ( ) ( ) Element of Omega : ( ( non empty ) ( non empty ) set ) ) : r : ( ( ) ( V11() real ext-real ) Real) <= X : ( ( ) ( non empty V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Real-Valued-Random-Variable of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . t : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) } : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
<= (expect (X : ( ( ) ( non empty V13() V16(b1 : ( ( non empty ) ( non empty ) set ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b1 : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Real-Valued-Random-Variable of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,P : ( ( ) ( non empty V13() V16(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V17( REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) Function-like total V32(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V71() V72() V73() V77() ) set ) ) V61() V62() V63() ) Probability of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V35() V36() V37() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) )) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V71()
V72()
V73()
V77() )
set ) )
/ r : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
COMPLEX : ( ( ) ( non
empty non
trivial non
finite V71()
V77() )
set ) ) ;