begin
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) st
f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
is_integrable_on M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
is_integrable_on M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
- f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) is
nonnegative holds
ex
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
(
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= (dom f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
/\ (dom g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
Integral (
M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
<= Integral (
M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) ) ;
begin
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) st
f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
is_integrable_on M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
ex
F being ( (
V18()
V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued V18()
V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
( ( for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V51()
V75()
V76()
V77()
V78()
V79()
V80()
V84() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) holds
F : ( (
V18()
V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued V18()
V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V51()
V75()
V76()
V77()
V78()
V79()
V80()
V84() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= (dom f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
/\ (great_eq_dom (|.f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) ,(R_EAL (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() ) Element of K6(REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) : ( ( ) ( non empty ) set ) ) ) / (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V51() V75() V76() V77() V78() V79() V80() V84() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() ) Element of K6(REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() ) Element of K6(REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() ) Element of K6(REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V76() ) set ) ) )) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
(dom f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
\ (eq_dom (f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ,0. : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V21() FinSequence-membered ext-real non positive non negative V75() V76() V77() V78() V79() V80() V81() ) Element of ExtREAL : ( ( ) ( non empty V76() ) set ) ) )) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
= union (rng F : ( ( V18() V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() ) Element of K6(REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() ) Element of K6(REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued V18() V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() ) Element of K6(REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() ) Element of K6(REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( )
Element of
K6(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) & ( for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V51()
V75()
V76()
V77()
V78()
V79()
V80()
V84() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) holds
(
F : ( (
V18()
V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-valued V18()
V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V51()
V75()
V76()
V77()
V78()
V79()
V80()
V84() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V75()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
K6(
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
in S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) &
M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. (F : ( ( V18() V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() ) Element of K6(REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() ) Element of K6(REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued V18() V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() ) Element of K6(REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() ) Element of K6(REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V51() V75() V76() V77() V78() V79() V80() V84() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() ) Element of K6(REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
< +infty : ( ( ) ( non
empty non
real ext-real positive non
negative )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) ) ) ) ;
begin
definition
let k be ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative )
Nat) ;
let X be ( ( non
empty ) ( non
empty )
set ) ;
let f be ( (
V18() ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) ;
func f |^ k -> ( (
V18() ) (
Relation-like X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
means
(
dom it : ( (
V18() ) (
Relation-like k : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
k : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
set ) )
= dom f : ( (
V18()
V27(
k : ( ( non
empty ) ( non
empty )
set ) ,
X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ) ) (
Relation-like k : ( ( non
empty ) ( non
empty )
set )
-defined X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
-valued V18()
V27(
k : ( ( non
empty ) ( non
empty )
set ) ,
X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ) )
Element of
K6(
K7(
k : ( ( non
empty ) ( non
empty )
set ) ,
X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
set ) ) & ( for
x being ( ( ) ( )
Element of
X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ) st
x : ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) )
in dom it : ( (
V18() ) (
Relation-like k : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
k : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
set ) ) holds
it : ( (
V18() ) (
Relation-like k : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
k : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) )
. x : ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
= (f : ( ( V18() V27(k : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) Element of K6(K6(k : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like k : ( ( non empty ) ( non empty ) set ) -defined X : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) Element of K6(K6(k : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued V18() V27(k : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) Element of K6(K6(k : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Element of K6(K7(k : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) Element of K6(K6(k : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
|^ k : ( ( non
empty ) ( non
empty )
set ) : ( ( ) (
ext-real )
R_eal) ) );
end;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
f,
g being ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
for
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
(dom f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
/\ (dom g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
= E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) is
V67() &
g : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) is
V67() &
f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
is_measurable_on E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
is_measurable_on E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
(#) g : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) )
is_measurable_on E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
for
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
F being ( ( non
empty ) ( non
empty V76() )
Subset of ( ( ) ( non
empty )
set ) ) st
(dom f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
/\ (dom g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
= E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
rng f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) : ( ( ) (
V76() )
Element of
K6(
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty )
set ) )
= F : ( ( non
empty ) ( non
empty V76() )
Subset of ( ( ) ( non
empty )
set ) ) &
g : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) is
V67() &
f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
is_measurable_on E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
rng f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) : ( ( ) (
V76() )
Element of
K6(
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty )
set ) ) is
real-bounded &
g : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
is_integrable_on M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
(
(f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) (#) g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) )
| E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) & ex
c being ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) ) st
(
c : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) )
>= inf F : ( ( non
empty ) ( non
empty V76() )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) &
c : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V34()
V75()
V76()
V77()
V81() )
set ) )
<= sup F : ( ( non
empty ) ( non
empty V76() )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) &
Integral (
M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
((f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) (#) |.g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
= (R_EAL c : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V75() V76() V77() V81() ) set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
* (Integral (M : ( ( V18() V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V76() ) set ) ) zeroed nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V76() ) set ) ) extreal-yielding zeroed nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,(|.g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) ) ) ;
begin
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
f,
g being ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) holds
(
dom (|.f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) + |.g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
= (dom f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
/\ (dom g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
dom |.(f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) + g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) .| : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding nonnegative )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
c= dom |.f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding nonnegative )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
f,
g being ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) holds
(|.f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) | (dom |.(f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) + g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6(b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) )
+ (|.g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) | (dom |.(f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) + g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K6(b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) )
= (|.f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) + |.g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) )
| (dom |.(f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) + g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
f,
g being ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
for
x being ( ( ) ( )
set ) st
x : ( ( ) ( )
set )
in dom |.(f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) + g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) .| : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding nonnegative )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
|.(f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) + g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) .| : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding nonnegative )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) )
. x : ( ( ) ( )
set ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
<= (|.f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) + |.g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) )
. x : ( ( ) ( )
set ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) st
f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
is_integrable_on M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
is_integrable_on M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
ex
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
(
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= dom (f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) + g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
Integral (
M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(|.(f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) + g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) ) : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
<= (Integral (M : ( ( V18() V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V76() ) set ) ) zeroed nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V76() ) set ) ) extreal-yielding zeroed nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,(|.f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
+ (Integral (M : ( ( V18() V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V76() ) set ) ) zeroed nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V76() ) set ) ) extreal-yielding zeroed nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,(|.g : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) .| : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding nonnegative ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
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 V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
< +infty : ( ( ) ( non
empty non
real ext-real positive non
negative )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) holds
(
chi (
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
X : ( ( non
empty ) ( non
empty )
set ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
Integral (
M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(chi (E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,X : ( ( non empty ) ( non empty ) set ) )) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
= M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
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 V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) &
Integral (
M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
((chi (E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,X : ( ( non empty ) ( non empty ) set ) )) : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
= M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
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 V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
E1,
E2 being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. (E1 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) /\ E2 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( )
M9(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
< +infty : ( ( ) ( non
empty non
real ext-real positive non
negative )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) holds
Integral (
M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
((chi (E1 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,X : ( ( non empty ) ( non empty ) set ) )) : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V76() ) set ) ) : ( ( ) ( non empty extreal-yielding ) set ) ) : ( ( ) ( non empty ) set ) ) | E2 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
= M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. (E1 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) /\ E2 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( )
M9(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
for
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
a,
b being ( (
real ) (
V11()
real ext-real )
number ) st
f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
is_integrable_on M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
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 V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
c= dom f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
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 V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
< +infty : ( ( ) ( non
empty non
real ext-real positive non
negative )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
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 V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
(
a : ( (
real ) (
V11()
real ext-real )
number )
<= f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) &
f : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
PartFunc of ,)
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
<= b : ( (
real ) (
V11()
real ext-real )
number ) ) ) holds
(
(R_EAL a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
* (M : ( ( V18() V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V76() ) set ) ) zeroed nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V76() ) set ) ) extreal-yielding zeroed nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() 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 V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
<= Integral (
M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) &
Integral (
M : ( (
V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
zeroed nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
extreal-yielding zeroed nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty V30()
V31()
V32()
compl-closed sigma-multiplicative sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( V18() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() extreal-yielding ) PartFunc of ,) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
V18() ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V76() )
set )
-valued V18()
extreal-yielding )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) ( non
empty extreal-yielding )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
<= (R_EAL b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) )
* (M : ( ( V18() V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V76() ) set ) ) zeroed nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V76() ) set ) -valued V18() V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V76() ) set ) ) extreal-yielding zeroed nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty V30() V31() V32() 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 V30() V31() V32() compl-closed sigma-multiplicative sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V76() )
set ) ) ) ;