begin
theorem
for
X being ( ( ) ( )
set )
for
F being ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
for
M being ( (
Function-like quasi_total zeroed nonnegative V102(
b1 : ( ( ) ( )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) ) ( non
empty Relation-like b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
quasi_total ext-real-valued zeroed nonnegative V102(
b1 : ( ( ) ( )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) )
Measure of
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
for
Sets being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool b1 : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
SetSequence of ( ( ) ( non
empty )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural ext-real non
negative V56()
real )
Nat)
for
Cvr being ( ( ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined Funcs (
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) ,
(bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) ,
bool b1 : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
Covering of
Sets : ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool b1 : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
SetSequence of ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) ,
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) holds
0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non
positive non
negative Function-like functional V56()
real V58()
V62()
V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
<= (Volume (M : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ,Cvr : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,(bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Covering of b4 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued )
ExtREAL_sequence)
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural ext-real non
negative V56()
real )
Nat) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V74() )
set ) ) ;
definition
let X be ( ( ) ( )
set ) ;
let F be ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ;
let Sets be ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool X : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
SetSequence of ( ( ) ( non
empty )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) ;
let Cvr be ( ( ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined Funcs (
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) ,
(bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) ,
bool X : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
Covering of
Sets : ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool X : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
SetSequence of ( ( ) ( non
empty )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) ,
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) ;
func On Cvr -> ( ( ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool X : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
Covering of
union (rng Sets : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
bool X : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ,
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
means
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural ext-real non
negative V56()
real )
Nat) holds
it : ( ( ) ( )
set )
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural ext-real non
negative V56()
real )
Nat) : ( ( ) ( )
Element of
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
= (Cvr : ( ( Function-like quasi_total zeroed nonnegative V102(X : ( ( ) ( ) set ) ,Sets : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( non empty Relation-like Sets : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(Sets : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ext-real-valued zeroed nonnegative V102(X : ( ( ) ( ) set ) ,Sets : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:Sets : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V74() ) set ) :] : ( ( ) ( non empty ext-real-valued ) set ) : ( ( ) ( non empty ) set ) ) . ((pr1 InvPairFunc : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty RAT : ( ( ) ( non empty V34() V73() V74() V75() V76() V79() ) set ) -valued INT : ( ( ) ( non empty V34() V73() V74() V75() V76() V77() V79() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty RAT : ( ( ) ( non empty V34() V73() V74() V75() V76() V79() ) set ) -valued INT : ( ( ) ( non empty V34() V73() V74() V75() V76() V77() V79() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total complex-valued ext-real-valued real-valued natural-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty RAT : ( ( ) ( non empty V34() V73() V74() V75() V76() V79() ) set ) -valued INT : ( ( ) ( non empty V34() V73() V74() V75() V76() V77() V79() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( non empty ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real V58() V62() V73() V74() V75() V76() V77() V78() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty ext-real Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool X : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
Covering of
Sets : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
. ((pr1 InvPairFunc : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty RAT : ( ( ) ( non empty V34() V73() V74() V75() V76() V79() ) set ) -valued INT : ( ( ) ( non empty V34() V73() V74() V75() V76() V77() V79() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty RAT : ( ( ) ( non empty V34() V73() V74() V75() V76() V79() ) set ) -valued INT : ( ( ) ( non empty V34() V73() V74() V75() V76() V77() V79() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total complex-valued ext-real-valued real-valued natural-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty RAT : ( ( ) ( non empty V34() V73() V74() V75() V76() V79() ) set ) -valued INT : ( ( ) ( non empty V34() V73() V74() V75() V76() V77() V79() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( non empty ) set ) ) . b1 : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real ) Nat) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural ext-real non
negative V56()
real V58()
V62()
V73()
V74()
V75()
V76()
V77()
V78() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
bool X : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) ,
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
. ((pr2 InvPairFunc : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty RAT : ( ( ) ( non empty V34() V73() V74() V75() V76() V79() ) set ) -valued INT : ( ( ) ( non empty V34() V73() V74() V75() V76() V77() V79() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty RAT : ( ( ) ( non empty V34() V73() V74() V75() V76() V79() ) set ) -valued INT : ( ( ) ( non empty V34() V73() V74() V75() V76() V77() V79() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total complex-valued ext-real-valued real-valued natural-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty RAT : ( ( ) ( non empty V34() V73() V74() V75() V76() V79() ) set ) -valued INT : ( ( ) ( non empty V34() V73() V74() V75() V76() V77() V79() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( non empty ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real ) Nat) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural ext-real non
negative V56()
real V58()
V62()
V73()
V74()
V75()
V76()
V77()
V78() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) ;
end;
theorem
for
X being ( ( ) ( )
set )
for
F being ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
for
M being ( (
Function-like quasi_total zeroed nonnegative V102(
b1 : ( ( ) ( )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) ) ( non
empty Relation-like b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
quasi_total ext-real-valued zeroed nonnegative V102(
b1 : ( ( ) ( )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) )
Measure of
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
for
k being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural ext-real non
negative V56()
real V58()
V62()
V73()
V74()
V75()
V76()
V77()
V78() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) ) ex
m being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural ext-real non
negative V56()
real )
Nat) st
for
Sets being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool b1 : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
SetSequence of ( ( ) ( non
empty )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
for
Cvr being ( ( ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined Funcs (
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) ,
(bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) ,
bool b1 : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
Covering of
Sets : ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool b1 : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
SetSequence of ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) ,
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) holds
(Partial_Sums (vol (M : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ,(On Cvr : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,(bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Covering of b6 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Covering of union (rng b6 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ext-real-valued ) ExtREAL_sequence) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V74() ) set ) :] : ( ( ) ( non
empty ext-real-valued )
set ) : ( ( ) ( non
empty )
set ) )
. k : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural ext-real non
negative V56()
real V58()
V62()
V73()
V74()
V75()
V76()
V77()
V78() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V74() )
set ) )
<= (Partial_Sums (Volume (M : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ,Cvr : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,(bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Covering of b6 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ext-real-valued ) ExtREAL_sequence) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued )
Element of
bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V74() ) set ) :] : ( ( ) ( non
empty ext-real-valued )
set ) : ( ( ) ( non
empty )
set ) )
. m : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural ext-real non
negative V56()
real )
Nat) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V74() )
set ) ) ;
theorem
for
X being ( ( ) ( )
set )
for
F being ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
for
M being ( (
Function-like quasi_total zeroed nonnegative V102(
b1 : ( ( ) ( )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) ) ( non
empty Relation-like b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
quasi_total ext-real-valued zeroed nonnegative V102(
b1 : ( ( ) ( )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) )
Measure of
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
for
Sets being ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool b1 : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
SetSequence of ( ( ) ( non
empty )
Element of
bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
for
Cvr being ( ( ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined Funcs (
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) ,
(bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty functional )
FUNCTION_DOMAIN of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) ,
bool b1 : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
Covering of
Sets : ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool b1 : ( ( ) ( )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
SetSequence of ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) ,
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) holds
inf (Svc (M : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ,(union (rng Sets : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) ( non
empty V74() )
Subset of ( ( ) ( non
empty )
set ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V74() )
set ) )
<= SUM (Volume (M : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( ) ( ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ,Cvr : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ,(bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty functional ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Covering of b4 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V27( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() ) Element of bool REAL : ( ( ) ( non empty V34() V73() V74() V75() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) )) : ( (
Function-like quasi_total ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued )
ExtREAL_sequence) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V74() )
set ) ) ;
begin
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
F being ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
for
m being ( (
Function-like quasi_total zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) ) ( non
empty Relation-like b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
quasi_total ext-real-valued zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) )
Measure of
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) st
m : ( (
Function-like quasi_total zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) ) ( non
empty Relation-like b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
quasi_total ext-real-valued zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) )
Measure of
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) is
completely-additive holds
ex
M being ( (
Function-like quasi_total zeroed nonnegative sigma-additive ) ( non
empty Relation-like sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued zeroed nonnegative sigma-additive )
sigma_Measure of
sigma F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) st
(
M : ( (
Function-like quasi_total zeroed nonnegative sigma-additive ) ( non
empty Relation-like sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued zeroed nonnegative sigma-additive )
sigma_Measure of
sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
is_extension_of m : ( (
Function-like quasi_total zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) ) ( non
empty Relation-like b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
quasi_total ext-real-valued zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) )
Measure of
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) &
M : ( (
Function-like quasi_total zeroed nonnegative sigma-additive ) ( non
empty Relation-like sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued zeroed nonnegative sigma-additive )
sigma_Measure of
sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
= (sigma_Meas (C_Meas m : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) : ( ( ) ( non empty Relation-like bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27( bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ext-real-valued ) C_Measure of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like sigma_Field (C_Meas b3 : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) : ( ( ) ( non
empty Relation-like bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued )
C_Measure of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( non
empty ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
sigma_Field (C_Meas b3 : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) : ( ( ) ( non
empty Relation-like bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued )
C_Measure of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( non
empty ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued zeroed nonnegative sigma-additive )
Element of
bool [:(sigma_Field (C_Meas b3 : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) : ( ( ) ( non empty Relation-like bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27( bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ext-real-valued ) C_Measure of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V74() ) set ) :] : ( ( ) ( non
empty ext-real-valued )
set ) : ( ( ) ( non
empty )
set ) )
| (sigma F : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like sigma_Field (C_Meas b3 : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) : ( ( ) ( non
empty Relation-like bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued )
C_Measure of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( non
empty ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like ext-real-valued )
Element of
bool [:(sigma_Field (C_Meas b3 : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) : ( ( ) ( non empty Relation-like bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27( bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ext-real-valued ) C_Measure of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V74() ) set ) :] : ( ( ) ( non
empty ext-real-valued )
set ) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
F being ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
for
m being ( (
Function-like quasi_total zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) ) ( non
empty Relation-like b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
quasi_total ext-real-valued zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) )
Measure of
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) st
m : ( (
Function-like quasi_total zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) ) ( non
empty Relation-like b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
quasi_total ext-real-valued zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) )
Measure of
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) is
completely-additive & ex
Aseq being ( ( ) ( non
empty Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) )
-defined bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like V27(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V73()
V74()
V75()
V76()
V77()
V78()
V79() )
Element of
bool REAL : ( ( ) ( non
empty V34()
V73()
V74()
V75()
V79() )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total )
Set_Sequence of
F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) st
( ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural ext-real non
negative V56()
real )
Nat) holds
m : ( (
Function-like quasi_total zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) ) ( non
empty Relation-like b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
quasi_total ext-real-valued zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) )
Measure of
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
. (Aseq : ( ( Function-like quasi_total zeroed nonnegative sigma-additive ) ( non empty Relation-like sigma b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27( sigma b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ext-real-valued zeroed nonnegative sigma-additive ) sigma_Measure of sigma b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural ext-real non negative V56() real ) Nat) ) : ( ( ) (
ext-real )
Element of
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty V74() )
set ) )
< +infty : ( ( ) ( non
empty ext-real positive non
negative non
real )
Element of
ExtREAL : ( ( ) ( non
empty V74() )
set ) ) ) &
X : ( ( non
empty ) ( non
empty )
set )
= union (rng Aseq : ( ( Function-like quasi_total zeroed nonnegative sigma-additive ) ( non empty Relation-like sigma b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27( sigma b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ext-real-valued zeroed nonnegative sigma-additive ) sigma_Measure of sigma b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) (
V74() )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) holds
for
M being ( (
Function-like quasi_total zeroed nonnegative sigma-additive ) ( non
empty Relation-like sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued zeroed nonnegative sigma-additive )
sigma_Measure of
sigma F : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ) st
M : ( (
Function-like quasi_total zeroed nonnegative sigma-additive ) ( non
empty Relation-like sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued zeroed nonnegative sigma-additive )
sigma_Measure of
sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
is_extension_of m : ( (
Function-like quasi_total zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) ) ( non
empty Relation-like b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) )
quasi_total ext-real-valued zeroed nonnegative V102(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) )
Measure of
b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) ) holds
M : ( (
Function-like quasi_total zeroed nonnegative sigma-additive ) ( non
empty Relation-like sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued zeroed nonnegative sigma-additive )
sigma_Measure of
sigma b2 : ( ( non
empty compl-closed V85() ) ( non
empty compl-closed V84()
V85()
V86() )
Field_Subset of ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
= (sigma_Meas (C_Meas m : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) : ( ( ) ( non empty Relation-like bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27( bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ext-real-valued ) C_Measure of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) ( non
empty Relation-like sigma_Field (C_Meas b3 : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) : ( ( ) ( non
empty Relation-like bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued )
C_Measure of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( non
empty ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
sigma_Field (C_Meas b3 : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) : ( ( ) ( non
empty Relation-like bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued )
C_Measure of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( non
empty ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued zeroed nonnegative sigma-additive )
Element of
bool [:(sigma_Field (C_Meas b3 : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) : ( ( ) ( non empty Relation-like bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27( bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ext-real-valued ) C_Measure of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V74() ) set ) :] : ( ( ) ( non
empty ext-real-valued )
set ) : ( ( ) ( non
empty )
set ) )
| (sigma F : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) : ( ( non
empty compl-closed sigma-multiplicative ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like sigma_Field (C_Meas b3 : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) : ( ( ) ( non
empty Relation-like bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like V27(
bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) )
quasi_total ext-real-valued )
C_Measure of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( non
empty ) ( non
empty compl-closed sigma-multiplicative V84()
V85()
V86()
sigma-additive )
Element of
bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined ExtREAL : ( ( ) ( non
empty V74() )
set )
-valued Function-like ext-real-valued )
Element of
bool [:(sigma_Field (C_Meas b3 : ( ( Function-like quasi_total zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) ( non empty Relation-like b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27(b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) quasi_total ext-real-valued zeroed nonnegative V102(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) Measure of b2 : ( ( non empty compl-closed V85() ) ( non empty compl-closed V84() V85() V86() ) Field_Subset of ) ) ) : ( ( ) ( non empty Relation-like bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V74() ) set ) -valued Function-like V27( bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ext-real-valued ) C_Measure of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V74() ) set ) :] : ( ( ) ( non
empty ext-real-valued )
set ) : ( ( ) ( non
empty )
set ) ) ;