begin
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V70()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
n being ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat)
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
for
F being ( (
V83() ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V83() )
Finite_Sep_Sequence of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
a,
x being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
is_simple_func_in S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) &
dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) & ( for
x being ( ( ) ( )
set ) st
x : ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat)
in dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set ) holds
0. : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
<= f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
. x : ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ) &
F : ( (
V83() ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V83() )
Finite_Sep_Sequence of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
a : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
are_Re-presentation_of f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) &
dom x : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
V85()
V86()
V87()
V88()
V89()
V90() )
Element of
K19(
NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) ) ) : ( ( ) (
V37() )
set ) )
= dom F : ( (
V83() ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V83() )
Finite_Sep_Sequence of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
V85()
V86()
V87()
V88()
V89()
V90() )
Element of
K19(
NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) ) ) : ( ( ) (
V37() )
set ) ) & ( for
i being ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat) st
i : ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat)
in dom x : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
V85()
V86()
V87()
V88()
V89()
V90() )
Element of
K19(
NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) ) ) : ( ( ) (
V37() )
set ) ) holds
x : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
. i : ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
= (a : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) . i : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
* ((M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) * F : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) Element of K19(K20(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ,ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V37() V62() ) set ) ) : ( ( ) ( V37() ) set ) ) . i : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ) &
len F : ( (
V83() ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V83() )
Finite_Sep_Sequence of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V33()
V37()
V42()
V71()
V85()
V86()
V87()
V88()
V89()
V90() )
Element of
NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) ) )
= n : ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat) holds
integral (
X : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
M : ( (
Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V70()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
= Sum x : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
for
M being ( (
Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V70()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
F being ( (
V83() ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V83() )
Finite_Sep_Sequence of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
a,
x being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
is_simple_func_in S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) &
dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) & ( for
x being ( ( ) ( )
set ) st
x : ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat)
in dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set ) holds
0. : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
<= f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
. x : ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ) &
F : ( (
V83() ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V83() )
Finite_Sep_Sequence of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
a : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
are_Re-presentation_of f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) &
dom x : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
V85()
V86()
V87()
V88()
V89()
V90() )
Element of
K19(
NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) ) ) : ( ( ) (
V37() )
set ) )
= dom F : ( (
V83() ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V83() )
Finite_Sep_Sequence of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
V85()
V86()
V87()
V88()
V89()
V90() )
Element of
K19(
NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) ) ) : ( ( ) (
V37() )
set ) ) & ( for
n being ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat) st
n : ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat)
in dom x : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
V85()
V86()
V87()
V88()
V89()
V90() )
Element of
K19(
NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) ) ) : ( ( ) (
V37() )
set ) ) holds
x : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
. n : ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
= (a : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) . n : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
* ((M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) * F : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) Element of K19(K20(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ,ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V37() V62() ) set ) ) : ( ( ) ( V37() ) set ) ) . n : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ) holds
integral (
X : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
M : ( (
Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V70()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
= Sum x : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
for
M being ( (
Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V70()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
is_simple_func_in S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) &
dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) & ( for
x being ( ( ) ( )
set ) st
x : ( (
V83() ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V83() )
Finite_Sep_Sequence of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
in dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set ) holds
0. : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
<= f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
. x : ( (
V83() ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V83() )
Finite_Sep_Sequence of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ) holds
ex
F being ( (
V83() ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V83() )
Finite_Sep_Sequence of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ex
a,
x being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) st
(
F : ( (
V83() ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V83() )
Finite_Sep_Sequence of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
a : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
are_Re-presentation_of f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) &
dom x : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
V85()
V86()
V87()
V88()
V89()
V90() )
Element of
K19(
NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) ) ) : ( ( ) (
V37() )
set ) )
= dom F : ( (
V83() ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V83() )
Finite_Sep_Sequence of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
V85()
V86()
V87()
V88()
V89()
V90() )
Element of
K19(
NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) ) ) : ( ( ) (
V37() )
set ) ) & ( for
n being ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat) st
n : ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat)
in dom x : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
V85()
V86()
V87()
V88()
V89()
V90() )
Element of
K19(
NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) ) ) : ( ( ) (
V37() )
set ) ) holds
x : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
. n : ( (
V21() ) (
V15()
V16()
V17()
V21()
V22()
V23()
ext-real non
negative V37()
V42() )
Nat) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
= (a : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) . n : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
* ((M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) * F : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) Element of K19(K20(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ,ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V37() V62() ) set ) ) : ( ( ) ( V37() ) set ) ) . n : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ) &
integral (
X : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
M : ( (
Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V70()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
= Sum x : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V15()
V16()
V17()
V37()
V42()
V43()
V85()
V86()
V87()
V88()
V89()
V90()
V91() )
Element of
K19(
REAL : ( ( ) ( non
empty V37()
V85()
V86()
V87()
V91() )
set ) ) : ( ( ) (
V37() )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V37()
FinSequence-like FinSubsequence-like V62() )
FinSequence of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V70()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
is_simple_func_in S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) &
dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) & ( for
x being ( ( ) ( )
set ) st
x : ( ( ) ( )
set )
in dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set ) holds
0. : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
<= f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
. x : ( ( ) ( )
set ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ) &
g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
is_simple_func_in S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) &
dom g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set )
= dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set ) & ( for
x being ( ( ) ( )
set ) st
x : ( ( ) ( )
set )
in dom g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set ) holds
0. : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
<= g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
. x : ( ( ) ( )
set ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ) holds
(
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
+ g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
V62() )
set ) ) : ( ( ) ( )
set ) )
is_simple_func_in S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) &
dom (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
V62() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) & ( for
x being ( ( ) ( )
set ) st
x : ( ( ) ( )
set )
in dom (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
V62() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) holds
0. : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
<= (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
V62() )
set ) ) : ( ( ) ( )
set ) )
. x : ( ( ) ( )
set ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ) &
integral (
X : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
M : ( (
Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V70()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
V62() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
= (integral (X : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) )) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
+ (integral (X : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) )) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V70()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
for
c being ( ( ) (
ext-real )
R_eal) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
is_simple_func_in S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) &
dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set )
<> {} : ( ( ) ( )
set ) & ( for
x being ( ( ) ( )
set ) st
x : ( ( ) ( )
set )
in dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set ) holds
0. : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
<= f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
. x : ( ( ) ( )
set ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ) &
0. : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
<= c : ( ( ) (
ext-real )
R_eal) &
c : ( ( ) (
ext-real )
R_eal)
< +infty : ( ( ) ( non
empty V23()
ext-real positive non
negative )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) &
dom g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set )
= dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set ) & ( for
x being ( ( ) ( )
set ) st
x : ( ( ) ( )
set )
in dom g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) : ( ( ) ( )
set ) holds
g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,)
. x : ( ( ) ( )
set ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
= c : ( ( ) (
ext-real )
R_eal)
* (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) . x : ( ( ) ( ) set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ) holds
integral (
X : ( ( non
empty ) ( non
empty )
set ) ,
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
M : ( (
Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V70()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V30(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
V62()
V70()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V79()
V80()
V81()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V86() )
set )
-valued Function-like V62() )
PartFunc of ,) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) )
= c : ( ( ) (
ext-real )
R_eal)
* (integral (X : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) )) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V86() )
set ) ) ;