MEASURE7

:: MEASURE7 semantic presentation

begin

theorem :: MEASURE7:4

theorem :: MEASURE7:5

theorem :: MEASURE7:6

definition

let S be ( ( non empty ) ( non empty ) set ) ;
let H be ( ( Function-like quasi_total ) ( Relation-like S : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14(S : ( ( non empty ) ( non empty ) set ) ) quasi_total V68() ) Function of S : ( ( non empty ) ( non empty ) set ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) ;

end;

theorem :: MEASURE7:7

for X being ( ( non empty ) ( non empty ) set )
for G being ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14(b₁ : ( ( non empty ) ( non empty ) set ) ) quasi_total V68() ) Function of X : ( ( non empty ) ( non empty ) set ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) st G : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14(b₁ : ( ( non empty ) ( non empty ) set ) ) quasi_total V68() ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) is V93() holds
On G : ( ( Function-like quasi_total ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14(b₁ : ( ( non empty ) ( non empty ) set ) ) quasi_total V68() ) Function of b₁ : ( ( non empty ) ( non empty ) set ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) is V93() ;

theorem :: MEASURE7:8

theorem :: MEASURE7:9

theorem :: MEASURE7:10

for G being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) st G : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) is V93() holds
for S being ( ( non empty ) ( non empty V56() V57() V58() V59() V60() V61() left_end bounded_below ) Subset of ( ( ) ( non empty ) set ) )
for H being ( ( Function-like quasi_total ) ( Relation-like b₂ : ( ( non empty ) ( non empty V56() V57() V58() V59() V60() V61() left_end bounded_below ) Subset of ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14(b₂ : ( ( non empty ) ( non empty V56() V57() V58() V59() V60() V61() left_end bounded_below ) Subset of ( ( ) ( non empty ) set ) ) ) quasi_total V67() V68() V69() V70() ) Function of S : ( ( non empty ) ( non empty V56() V57() V58() V59() V60() V61() left_end bounded_below ) Subset of ( ( ) ( non empty ) set ) ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) st H : ( ( Function-like quasi_total ) ( Relation-like b₂ : ( ( non empty ) ( non empty V56() V57() V58() V59() V60() V61() left_end bounded_below ) Subset of ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14(b₂ : ( ( non empty ) ( non empty V56() V57() V58() V59() V60() V61() left_end bounded_below ) Subset of ( ( ) ( non empty ) set ) ) ) quasi_total V67() V68() V69() V70() ) Function of b₂ : ( ( non empty ) ( non empty V56() V57() V58() V59() V60() V61() left_end bounded_below ) Subset of ( ( ) ( non empty ) set ) ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) is one-to-one holds
SUM (On (G : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) * H : ( ( Function-like quasi_total ) ( Relation-like b₂ : ( ( non empty ) ( non empty V56() V57() V58() V59() V60() V61() left_end bounded_below ) Subset of ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14(b₂ : ( ( non empty ) ( non empty V56() V57() V58() V59() V60() V61() left_end bounded_below ) Subset of ( ( ) ( non empty ) set ) ) ) quasi_total V67() V68() V69() V70() ) Function of b₂ : ( ( non empty ) ( non empty V56() V57() V58() V59() V60() V61() left_end bounded_below ) Subset of ( ( ) ( non empty ) set ) ) , NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty V56() V57() V58() V59() V60() V61() left_end bounded_below ) Subset of ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14(b₂ : ( ( non empty ) ( non empty V56() V57() V58() V59() V60() V61() left_end bounded_below ) Subset of ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Element of bool [:b₂ : ( ( non empty ) ( non empty V56() V57() V58() V59() V60() V61() left_end bounded_below ) Subset of ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V57() interval ) set ) :] : ( ( ) ( Relation-like non empty V68() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) <= SUM G : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) ;

theorem :: MEASURE7:11

definition

let A be ( ( ) ( V56() V57() V58() ) Subset of ( ( ) ( non empty ) set ) ) ;

mode Interval_Covering of A -> ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) means :: MEASURE7:def 2
( A : ( ( Relation-like Function-like V70() ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued Function-like V67() V68() V69() V70() ) set ) c= union (rng it : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) holds it : ( ( ) ( ) set ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is ( ( interval ) ( V56() V57() V58() interval ) Interval) ) );

end;

definition

let A be ( ( ) ( V56() V57() V58() ) Subset of ( ( ) ( non empty ) set ) ) ;
let F be ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of A : ( ( ) ( V56() V57() V58() ) Subset of ( ( ) ( non empty ) set ) ) ) ;
let n be ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ;
:: original: .
redefine func F . n -> ( ( interval ) ( V56() V57() V58() interval ) Interval) ;

end;

definition

mode Interval_Covering of F -> ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,(bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,(bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) means :: MEASURE7:def 3
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) holds it : ( ( ) ( ) set ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like Function-like ) Element of Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,(bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) is ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of F : ( ( Relation-like Function-like V70() ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued Function-like V67() V68() V69() V70() ) set ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() real ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

end;

definition

end;

theorem :: MEASURE7:12

for A being ( ( ) ( V56() V57() V58() ) Subset of ( ( ) ( non empty ) set ) )
for F being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of A : ( ( ) ( V56() V57() V58() ) Subset of ( ( ) ( non empty ) set ) ) ) holds F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of b₁ : ( ( ) ( V56() V57() V58() ) Subset of ( ( ) ( non empty ) set ) ) ) vol : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) is V93() ;

definition

end;

definition

end;

definition

func vol F -> ( ( ) ( ext-real ) R_eal) equals :: MEASURE7:def 6
SUM (F : ( ( ) ( ) set ) vol) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) ;

end;

definition

end;

theorem :: MEASURE7:13

for F being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for G being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,(bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of F : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) )
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) holds 0. : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() ext-real V56() V57() V58() V59() V60() V61() V62() V67() V68() V69() V70() real bounded_below interval ) Element of ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) <= (vol G : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,(bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of b₁ : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) ;

definition

let A be ( ( ) ( V56() V57() V58() ) Subset of ( ( ) ( non empty ) set ) ) ;

func Svc A -> ( ( ) ( V57() ) Subset of ( ( ) ( non empty ) set ) ) means :: MEASURE7:def 8
for x being ( ( ) ( ext-real ) R_eal) holds
( x : ( ( ) ( ext-real ) R_eal) in it : ( ( ) ( ) set ) iff ex F being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of A : ( ( Relation-like Function-like V70() ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued Function-like V67() V68() V69() V70() ) set ) ) st x : ( ( ) ( ext-real ) R_eal) = vol F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of A : ( ( ) ( V56() V57() V58() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real ) R_eal) );

end;

registration

let A be ( ( ) ( V56() V57() V58() ) Subset of ( ( ) ( non empty ) set ) ) ;

cluster Svc A : ( ( ) ( V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V57() ) Subset of ( ( ) ( non empty ) set ) ) -> non empty ;

end;

definition

let A be ( ( ) ( V56() V57() V58() ) Subset of ( ( ) ( non empty ) set ) ) ;

func COMPLEX A -> ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) equals :: MEASURE7:def 9
inf (Svc A : ( ( ) ( ) set ) ) : ( ( ) ( V57() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) ;

end;

definition

func OS_Meas -> ( ( Function-like quasi_total ) ( Relation-like bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) means :: MEASURE7:def 10
for A being ( ( ) ( V56() V57() V58() ) Subset of ( ( ) ( non empty ) set ) ) holds it : ( ( ) ( ) set ) . A : ( ( ) ( V56() V57() V58() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) = inf (Svc A : ( ( ) ( V56() V57() V58() ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V57() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) ;

end;

definition

let F be ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
let G be ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,(bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of F : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;
let H be ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) ) ;
assume rng H : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -valued non empty V67() V68() V69() V70() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) : ( ( ) ( non empty ) set ) ) = [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) ;

func On (G,H) -> ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of union (rng F : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) means :: MEASURE7:def 11
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) holds it : ( ( ) ( ) Element of G : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( interval ) ( V56() V57() V58() interval ) Interval) = (G : ( ( ) ( ) set ) . ((pr1 H : ( ( ) ( non empty V48() ) M9(F : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) )) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V67() V68() V69() V70() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) : ( ( ) ( non empty ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of F : ( ( ) ( ) set ) . ((pr1 H : ( ( ) ( non empty V48() ) M9(F : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) )) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V67() V68() V69() V70() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) : ( ( ) ( non empty ) set ) ) . b₁ : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) . ((pr2 H : ( ( ) ( non empty V48() ) M9(F : ( ( ) ( ) set ) ,G : ( ( ) ( ) set ) )) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V67() V68() V69() V70() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) : ( ( ) ( non empty ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( interval ) ( V56() V57() V58() interval ) Interval) ;

end;

theorem :: MEASURE7:14

for H being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) ) st H : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) ) is one-to-one & rng H : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -valued non empty V67() V68() V69() V70() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) : ( ( ) ( non empty ) set ) ) = [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) holds
for k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ex m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) st
for F being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for G being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,(bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of F : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) holds (Ser ((On (G : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,(bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of b₄ : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ,H : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V34() V56() V57() V58() V59() V62() ) set ) -valued INT : ( ( ) ( non empty V34() V56() V57() V58() V59() V60() V62() ) set ) -valued non empty V67() V68() V69() V70() ) set ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of union (rng b₄ : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) vol) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V57() interval ) set ) :] : ( ( ) ( Relation-like non empty V68() ) set ) : ( ( ) ( non empty ) set ) ) . k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) <= (Ser (vol G : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,(bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of b₄ : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V57() interval ) set ) :] : ( ( ) ( Relation-like non empty V68() ) set ) : ( ( ) ( non empty ) set ) ) . m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() ext-real V56() V57() V58() V59() V60() V61() real bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) ;

theorem :: MEASURE7:15

for F being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for G being ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,(bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of F : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) holds inf (Svc (union (rng F : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty V57() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) <= SUM (vol G : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined Funcs (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ,(bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Interval_Covering of b₁ : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() V62() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) ;

theorem :: MEASURE7:16

OS_Meas : ( ( Function-like quasi_total ) ( Relation-like bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) Function of bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V57() interval ) set ) ) is ( ( ) ( Relation-like bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) C_Measure of REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) ;

definition

:: original: OS_Meas
redefine func OS_Meas -> ( ( ) ( Relation-like bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) C_Measure of REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) ;

end;

definition

func Lmi_sigmaFIELD -> ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) SigmaField of REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) equals :: MEASURE7:def 12
sigma_Field OS_Meas : ( ( ) ( Relation-like bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) C_Measure of REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

definition

func L_mi -> ( ( Function-like quasi_total V76() nonnegative sigma-additive ) ( Relation-like Lmi_sigmaFIELD : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) SigmaField of REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( Lmi_sigmaFIELD : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) SigmaField of REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) ) quasi_total V68() V76() nonnegative sigma-additive ) sigma_Measure of Lmi_sigmaFIELD : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) SigmaField of REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) ) equals :: MEASURE7:def 13
sigma_Meas OS_Meas : ( ( ) ( Relation-like bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) C_Measure of REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like sigma_Field OS_Meas : ( ( ) ( Relation-like bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) C_Measure of REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( sigma_Field OS_Meas : ( ( ) ( Relation-like bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) C_Measure of REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() V76() nonnegative sigma-additive ) Element of bool [:(sigma_Field OS_Meas : ( ( ) ( Relation-like bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V57() interval ) set ) -valued Function-like non empty V14( bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V68() ) C_Measure of REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V84() V85() V86() sigma-additive ) Element of bool (bool REAL : ( ( ) ( non empty V34() V56() V57() V58() V62() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V57() interval ) set ) :] : ( ( ) ( Relation-like non empty V68() ) set ) : ( ( ) ( non empty ) set ) ) ;

end;