begin
begin
definition
let X be ( ( non
empty ) ( non
empty )
set ) ;
let S be ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) ) ;
let f be ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) ;
let E be ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) ) ) ;
pred f is_measurable_on E means
(
Re f : ( (
Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
Element of
K6(
K7(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) : ( ( ) ( non
empty Relation-like V34() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_measurable_on E : ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) &
Im f : ( (
Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
Element of
K6(
K7(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) : ( ( ) ( non
empty Relation-like V34() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_measurable_on E : ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) );
end;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
for
r being ( ( ) (
complex real ext-real )
Real) holds
(
r : ( ( ) (
complex real ext-real )
Real)
(#) (Re f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
= Re (r : ( ( ) ( complex real ext-real ) Real) (#) f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) &
r : ( ( ) (
complex real ext-real )
Real)
(#) (Im f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
= Im (r : ( ( ) ( complex real ext-real ) Real) (#) f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
for
c being ( (
complex ) (
complex )
number ) holds
(
Re (c : ( ( complex ) ( complex ) number ) (#) f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
= ((Re c : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) ) (#) (Re f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() V34() V35() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
- ((Im c : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) ) (#) (Im f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() V34() V35() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) &
Im (c : ( ( complex ) ( complex ) number ) (#) f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
= ((Im c : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) ) (#) (Re f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() V34() V35() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
+ ((Re c : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) ) (#) (Im f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() V34() V35() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) holds
(
- (Im f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
= Re (<i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) ) (#) f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) &
Re f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
= Im (<i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) ) (#) f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
f,
g being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) holds
(
Re (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
= (Re f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
+ (Re g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) &
Im (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
= (Im f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
+ (Im g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
f,
g being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) holds
(
Re (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) - g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
= (Re f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
- (Re g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) &
Im (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) - g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
= (Im f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
- (Im g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
for
A being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
(
(Re f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
| A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b4 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
= Re (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | A : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b4 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) &
(Im f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
| A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b4 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
= Im (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | A : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b4 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y being ( ( ) ( )
set )
for
f,
g being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) st
Y : ( ( ) ( )
set )
c= dom (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
(
dom ((f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | Y : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( ) ( ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() ) set ) ) : ( ( ) ( non empty ) set ) ) + (g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | Y : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( ) ( ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
= Y : ( ( ) ( )
set ) &
(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) )
| Y : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( ) ( )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) )
= (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | Y : ( ( ) ( ) set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( ) ( )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) )
+ (g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | Y : ( ( ) ( ) set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( ) ( )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) ;
begin
definition
let X be ( ( non
empty ) ( non
empty )
set ) ;
let S be ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) ) ;
let M be ( (
Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) ) ) ;
let f be ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) ;
pred f is_integrable_on M means
(
Re f : ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
Element of
K6(
K7(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) : ( ( ) ( non
empty Relation-like V34() )
set ) ) : ( ( ) ( non
empty )
set ) ) &
Im f : ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
Element of
K6(
K7(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) : ( ( ) ( non
empty Relation-like V34() )
set ) ) : ( ( ) ( non
empty )
set ) ) );
end;
definition
let X be ( ( non
empty ) ( non
empty )
set ) ;
let S be ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) ) ;
let M be ( (
Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) ) ) ;
let f be ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) ;
assume
f : ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) ) )
;
func Integral (
M,
f)
-> ( (
complex ) (
complex )
number )
means
ex
R,
I being ( ( ) (
complex real ext-real )
Real) st
(
R : ( ( ) (
complex real ext-real )
Real)
= Integral (
M : ( (
Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
Element of
K6(
K7(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) : ( ( ) ( non
empty Relation-like V34() )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
(Re f : ( ( Function-like ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() V34() V35() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) &
I : ( ( ) (
complex real ext-real )
Real)
= Integral (
M : ( (
Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
Element of
K6(
K7(
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) : ( ( ) ( non
empty Relation-like V34() )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
(Im f : ( ( Function-like ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() V34() V35() ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
X : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) &
it : ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) )
= R : ( ( ) (
complex real ext-real )
Real)
+ (I : ( ( ) ( complex real ext-real ) Real) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) ) ) : ( ( ) (
complex )
set ) : ( ( ) (
complex )
set ) );
end;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V34() )
PartFunc of ,)
for
A being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st ex
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
(
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V34() )
PartFunc of ,) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V34() )
PartFunc of ,)
is_measurable_on E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ) &
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
= 0 : ( ( ) (
empty natural complex real Relation-like non-empty empty-yielding RAT : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V53()
V56() )
set )
-valued Function-like one-to-one constant functional ext-real non
positive non
negative V33()
V34()
V35()
V36()
V43()
V44()
V50()
V51()
V52()
V53()
V54()
V55()
V56() )
Element of
NAT : ( ( ) (
V50()
V51()
V52()
V53()
V54()
V55()
V56() )
Element of
K6(
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) holds
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V34() )
PartFunc of ,)
| A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b5 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V34() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) : ( ( ) ( non
empty Relation-like V34() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
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 compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
for
E,
A being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st ex
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
(
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
is_measurable_on E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ) &
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
= 0 : ( ( ) (
empty natural complex real Relation-like non-empty empty-yielding RAT : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V53()
V56() )
set )
-valued Function-like one-to-one constant functional ext-real non
positive non
negative V33()
V34()
V35()
V36()
V43()
V44()
V50()
V51()
V52()
V53()
V54()
V55()
V56() )
Element of
NAT : ( ( ) (
V50()
V51()
V52()
V53()
V54()
V55()
V56() )
Element of
K6(
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) holds
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
| A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b6 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
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 compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
for
A being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st ex
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
(
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_measurable_on E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ) &
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
= 0 : ( ( ) (
empty natural complex real Relation-like non-empty empty-yielding RAT : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V53()
V56() )
set )
-valued Function-like one-to-one constant functional ext-real non
positive non
negative V33()
V34()
V35()
V36()
V43()
V44()
V50()
V51()
V52()
V53()
V54()
V55()
V56() )
Element of
NAT : ( ( ) (
V50()
V51()
V52()
V53()
V54()
V55()
V56() )
Element of
K6(
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) holds
(
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
| A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b5 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
Integral (
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | A : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b5 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
complex ) (
complex )
number )
= 0 : ( ( ) (
empty natural complex real Relation-like non-empty empty-yielding RAT : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V53()
V56() )
set )
-valued Function-like one-to-one constant functional ext-real non
positive non
negative V33()
V34()
V35()
V36()
V43()
V44()
V50()
V51()
V52()
V53()
V54()
V55()
V56() )
Element of
NAT : ( ( ) (
V50()
V51()
V52()
V53()
V54()
V55()
V56() )
Element of
K6(
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
for
E,
A being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
. A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
= 0 : ( ( ) (
empty natural complex real Relation-like non-empty empty-yielding RAT : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V53()
V56() )
set )
-valued Function-like one-to-one constant functional ext-real non
positive non
negative V33()
V34()
V35()
V36()
V43()
V44()
V50()
V51()
V52()
V53()
V54()
V55()
V56() )
Element of
NAT : ( ( ) (
V50()
V51()
V52()
V53()
V54()
V55()
V56() )
Element of
K6(
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) holds
Integral (
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | (E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) \ A : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) M11(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b5 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
\ b6 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) ( )
M11(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ))
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
complex ) (
complex )
number )
= Integral (
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) ) : ( (
complex ) (
complex )
number ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
for
A being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
| A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b5 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
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 compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
for
A,
B being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
misses B : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
Integral (
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | (A : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) \/ B : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) M11(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b5 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
\/ b6 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) ( )
M11(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ))
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
complex ) (
complex )
number )
= (Integral (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | A : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b5 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() ) set ) ) : ( ( ) ( non empty ) set ) ) )) : ( (
complex ) (
complex )
number )
+ (Integral (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | B : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b6 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() ) set ) ) : ( ( ) ( non empty ) set ) ) )) : ( (
complex ) (
complex )
number ) : ( ( ) (
complex )
set ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
for
B,
A being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
B : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= (dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
\ A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
(
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
| A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b6 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
Integral (
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) ) : ( (
complex ) (
complex )
number )
= (Integral (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | A : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b6 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() ) set ) ) : ( ( ) ( non empty ) set ) ) )) : ( (
complex ) (
complex )
number )
+ (Integral (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | B : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b5 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() ) set ) ) : ( ( ) ( non empty ) set ) ) )) : ( (
complex ) (
complex )
number ) : ( ( ) (
complex )
set ) ) ;
definition
let k be ( (
real ) (
complex real ext-real )
number ) ;
let X be ( ( non
empty ) ( non
empty )
set ) ;
let f be ( (
Function-like ) (
Relation-like X : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,) ;
func f to_power k -> ( (
Function-like ) (
Relation-like X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
means
(
dom it : ( (
Function-like ) (
Relation-like k : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
k : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
set ) )
= dom f : ( (
Function-like V27(
X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
Element of
K6(
K7(
X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) : ( ( ) ( non
empty Relation-like V34() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
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 compl-closed sigma-multiplicative V90()
V91()
V92()
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 : ( (
Function-like ) (
Relation-like k : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
k : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
X : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
Element of
K6(
K6(
k : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
set ) ) holds
it : ( (
Function-like ) (
Relation-like k : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
k : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
. x : ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) )
= (f : ( ( Function-like V27(X : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) Element of K6(K6(k : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like X : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) Element of K6(K6(k : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(X : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) Element of K6(K6(k : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) Element of K6(K7(X : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) Element of K6(K6(k : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V51() ) set ) ) : ( ( ) ( non empty Relation-like V34() ) set ) ) : ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) )
to_power k : ( ( non
empty ) ( non
empty )
set ) : ( (
real ) (
complex real ext-real )
set ) ) );
end;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) st ex
A being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
(
A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_measurable_on A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ) holds
(
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) iff
|.f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) .| : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
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 compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
dom (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
in S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
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 compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
+ g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
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 compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
- g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
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 compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
- g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
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 compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
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 compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
(
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= (dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
/\ (dom g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) 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 : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
complex ) (
complex )
number )
= (Integral (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b6 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() ) set ) ) : ( ( ) ( non empty ) set ) ) )) : ( (
complex ) (
complex )
number )
+ (Integral (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,(g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b6 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() ) set ) ) : ( ( ) ( non empty ) set ) ) )) : ( (
complex ) (
complex )
number ) : ( ( ) (
complex )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
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 compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
(
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= (dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
/\ (dom g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) 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 : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) - g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
= (Integral (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b6 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() V34() V35() ) set ) ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
+ (Integral (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,((- g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() V34() V35() ) set ) ) : ( ( ) ( non empty ) set ) ) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b6 : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) ) : ( ( ) ( non empty Relation-like V33() V34() V35() ) set ) ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
for
r being ( ( ) (
complex real ext-real )
Real) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
(
r : ( ( ) (
complex real ext-real )
Real)
(#) f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
Integral (
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(r : ( ( ) ( complex real ext-real ) Real) (#) f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
complex ) (
complex )
number )
= r : ( ( ) (
complex real ext-real )
Real)
* (Integral (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) )) : ( (
complex ) (
complex )
number ) : ( ( ) (
complex )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
(
<i> : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) )
(#) f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
Integral (
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(<i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) ) (#) f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
complex ) (
complex )
number )
= <i> : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) )
* (Integral (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) )) : ( (
complex ) (
complex )
number ) : ( ( ) (
complex )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
for
c being ( (
complex ) (
complex )
number ) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
(
c : ( (
complex ) (
complex )
number )
(#) f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
Integral (
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(c : ( ( complex ) ( complex ) number ) (#) f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
complex ) (
complex )
number )
= c : ( (
complex ) (
complex )
number )
* (Integral (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) )) : ( (
complex ) (
complex )
number ) : ( ( ) (
complex )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,) st ex
A being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
(
A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= (dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
/\ (dom g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) 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 ) ) &
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
is_measurable_on A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
is_measurable_on A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ) &
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,)
- f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) is
nonnegative holds
ex
E being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
(
E : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= (dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) )
/\ (dom g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) 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 : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b6 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
<= Integral (
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V45() V50() V51() V52() V56() ) set ) -valued Function-like V33() V34() V35() ) PartFunc of ,) | E : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b6 : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) st ex
A being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
(
A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
= dom f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_measurable_on A : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ) &
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
|.(Integral (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) )) : ( ( complex ) ( complex ) number ) .| : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) )
<= Integral (
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
|.f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) .| : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set )
-valued Function-like V33()
V34()
V35() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty V45()
V50()
V51()
V52()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33()
V34()
V35() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V51() )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f,
g being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
for
B being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
B : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
c= dom (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
K6(
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
(
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
+ g : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) )
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) &
Integral_on (
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
B : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
complex ) (
complex )
number )
= (Integral_on (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,B : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) )) : ( (
complex ) (
complex )
number )
+ (Integral_on (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,B : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) )) : ( (
complex ) (
complex )
number ) : ( ( ) (
complex )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
S being ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
X : ( ( non
empty ) ( non
empty )
set ) )
for
M being ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) )
for
f being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
for
c being ( (
complex ) (
complex )
number )
for
B being ( ( ) ( )
Element of
S : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) st
f : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
PartFunc of ,)
is_integrable_on M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) holds
Integral_on (
M : ( (
Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V42()
nonnegative sigma-additive ) (
Relation-like b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V51() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
ExtREAL : ( ( ) ( non
empty V51() )
set ) )
V34()
V42()
nonnegative sigma-additive )
sigma_Measure of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
B : ( ( ) ( )
Element of
b2 : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V90()
V91()
V92()
sigma-additive )
SigmaField of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ,
(c : ( ( complex ) ( complex ) number ) (#) f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set )
-valued Function-like V33() )
Element of
K6(
K7(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
COMPLEX : ( ( ) ( non
empty V45()
V50()
V56() )
set ) ) : ( ( ) ( non
empty Relation-like V33() )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
complex ) (
complex )
number )
= c : ( (
complex ) (
complex )
number )
* (Integral_on (M : ( ( Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V42() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V51() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V51() ) set ) ) V34() V42() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,B : ( ( ) ( ) Element of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V90() V91() V92() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V45() V50() V56() ) set ) -valued Function-like V33() ) PartFunc of ,) )) : ( (
complex ) (
complex )
number ) : ( ( ) (
complex )
set ) ;
begin