MEASURE4

:: MEASURE4 semantic presentation

for X being ( ( ) ( ) set )
for S being ( ( non empty ) ( non empty ) Subset-Family of )
for F, G being ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,S : ( ( non empty ) ( non empty ) Subset-Family of ) ) st G : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) . 0 : ( ( ) ( empty V15() V16() V17() V19() V20() V21() V22() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) = F : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) . 0 : ( ( ) ( empty V15() V16() V17() V19() V20() V21() V22() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) & ( for n being ( ( ) ( V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) holds G : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) . (n : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) + 1 : ( ( ) ( non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) = (F : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) . (n : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) + 1 : ( ( ) ( non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) \/ (G : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) . n : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) : ( ( ) ( ) set ) ) holds
for H being ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,S : ( ( non empty ) ( non empty ) Subset-Family of ) ) st H : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) . 0 : ( ( ) ( empty V15() V16() V17() V19() V20() V21() V22() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) = F : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) . 0 : ( ( ) ( empty V15() V16() V17() V19() V20() V21() V22() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) & ( for n being ( ( ) ( V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) holds H : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) . (n : ( ( ) ( V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) = (F : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) . (n : ( ( ) ( V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) \ (G : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) . n : ( ( ) ( V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) : ( ( ) ( ) Element of bool (b₃ : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) . (b₆ : ( ( ) ( V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) : ( ( ) ( non empty ) set ) ) ) holds
union (rng F : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of bool b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = union (rng H : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) ) ) : ( ( ) ( ) Element of bool b₂ : ( ( non empty ) ( non empty ) Subset-Family of ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ;

theorem :: MEASURE4:3

for X being ( ( ) ( ) set ) holds bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of X : ( ( ) ( ) set ) ) ;

definition

let X be ( ( ) ( ) set ) ;

mode C_Measure of X -> ( ( Function-like V30( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ) ( V1() V4( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) Function of bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) means :: MEASURE4:def 1
( it : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is V87() & it : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is zeroed & ( for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( it : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V60() ) set ) ) <= it : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V60() ) set ) ) & ( for F being ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds it : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (union (rng F : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V60() ) set ) ) <= SUM (it : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) * F : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) , bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like ext-real-valued ) Element of bool [:NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V60() ) set ) :] : ( ( ) ( non empty ext-real-valued ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V60() ) set ) ) ) ) ) );

end;

definition

let X be ( ( ) ( ) set ) ;
let C be ( ( ) ( V1() V4( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) ;

func sigma_Field C -> ( ( non empty ) ( non empty ) Subset-Family of ) means :: MEASURE4:def 2
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in it : ( ( Function-like V30(C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) zeroed nonnegative sigma-additive ) ( V1() V4(C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14(C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30(C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued zeroed nonnegative sigma-additive ) Element of bool [:C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V60() ) set ) :] : ( ( ) ( non empty ext-real-valued ) set ) : ( ( ) ( non empty ) set ) ) iff for W, Z being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st W : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & Z : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= X : ( ( ) ( ) set ) \ A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
(C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . W : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V60() ) set ) ) + (C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . Z : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V60() ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V60() ) set ) ) <= C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (W : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ Z : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V60() ) set ) ) );

end;

theorem :: MEASURE4:4

theorem :: MEASURE4:5

theorem :: MEASURE4:6

theorem :: MEASURE4:7

for A, X being ( ( ) ( ) set )
for C being ( ( ) ( V1() V4( bool b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₂ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₂ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₂ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) st A : ( ( ) ( ) set ) in sigma_Field C : ( ( ) ( V1() V4( bool b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₂ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₂ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₂ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₂ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) holds
X : ( ( ) ( ) set ) \ A : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) in sigma_Field C : ( ( ) ( V1() V4( bool b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₂ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₂ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₂ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₂ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) ;

theorem :: MEASURE4:8

for X, A, B being ( ( ) ( ) set )
for C being ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) st A : ( ( ) ( ) set ) in sigma_Field C : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) & B : ( ( ) ( ) set ) in sigma_Field C : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) holds
A : ( ( ) ( ) set ) \/ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) in sigma_Field C : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) ;

theorem :: MEASURE4:9

for X, A, B being ( ( ) ( ) set )
for C being ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) st A : ( ( ) ( ) set ) in sigma_Field C : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) & B : ( ( ) ( ) set ) in sigma_Field C : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) holds
A : ( ( ) ( ) set ) /\ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) in sigma_Field C : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) ;

theorem :: MEASURE4:10

for X, A, B being ( ( ) ( ) set )
for C being ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) st A : ( ( ) ( ) set ) in sigma_Field C : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) & B : ( ( ) ( ) set ) in sigma_Field C : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) holds
A : ( ( ) ( ) set ) \ B : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b₂ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) in sigma_Field C : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) ;

theorem :: MEASURE4:11

for X being ( ( ) ( ) set )
for S being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of X : ( ( ) ( ) set ) )
for N being ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) )
for A being ( ( ) ( ) Element of S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ex F being ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) st
for n being ( ( ) ( V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) holds F : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) . n : ( ( ) ( V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) = A : ( ( ) ( ) Element of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) /\ (N : ( ( Function-like V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ) ( V1() V4( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V5(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) Function-like non empty V14( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ) Function of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ,b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) . n : ( ( ) ( V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() ) Element of bool REAL : ( ( ) ( non empty V33() V59() V60() V61() V65() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ;

theorem :: MEASURE4:12

registration

cluster sigma_Field C : ( ( ) ( V1() V4( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) -> non empty compl-closed sigma-additive ;

end;

definition

let X be ( ( ) ( ) set ) ;
let S be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of X : ( ( ) ( ) set ) ) ;
let A be ( ( ) ( non empty V47() ) N_Sub_fam of S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) SigmaField of X : ( ( ) ( ) set ) ) ) ;
:: original: union
redefine func union A -> ( ( ) ( ) Element of S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

end;

definition

func sigma_Meas C -> ( ( Function-like V30( sigma_Field C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ) ( V1() V4( sigma_Field C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( sigma_Field C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) ) V30( sigma_Field C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) Function of sigma_Field C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) means :: MEASURE4:def 3
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in sigma_Field C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) Subset-Family of ) holds
it : ( ( Function-like V30(C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) zeroed nonnegative sigma-additive ) ( V1() V4(C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14(C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30(C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued zeroed nonnegative sigma-additive ) Element of bool [:C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,ExtREAL : ( ( ) ( non empty V60() ) set ) :] : ( ( ) ( non empty ext-real-valued ) set ) : ( ( ) ( non empty ) set ) ) . A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V60() ) set ) ) = C : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V60() ) set ) ) ;

end;

theorem :: MEASURE4:13

for X being ( ( ) ( ) set )
for C being ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) holds sigma_Meas C : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( Function-like V30( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ) ( V1() V4( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) V30( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) Function of sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) is ( ( Function-like V30( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) zeroed nonnegative V90(b₁ : ( ( ) ( ) set ) , sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) ) ( V1() V4( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) V30( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued zeroed nonnegative V90(b₁ : ( ( ) ( ) set ) , sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) ) Measure of sigma_Field C : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) ;

theorem :: MEASURE4:14

for X being ( ( ) ( ) set )
for C being ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) holds sigma_Meas C : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( Function-like V30( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ) ( V1() V4( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) V30( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) Function of sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) is ( ( Function-like V30( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) zeroed nonnegative sigma-additive ) ( V1() V4( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) V30( sigma_Field b₂ : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued zeroed nonnegative sigma-additive ) sigma_Measure of sigma_Field C : ( ( ) ( V1() V4( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of b₁ : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) ;

registration

cluster sigma_Meas C : ( ( ) ( V1() V4( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) : ( ( Function-like V30( sigma_Field C : ( ( ) ( V1() V4( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ) ( V1() V4( sigma_Field C : ( ( ) ( V1() V4( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( sigma_Field C : ( ( ) ( V1() V4( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) ) V30( sigma_Field C : ( ( ) ( V1() V4( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) Function of sigma_Field C : ( ( ) ( V1() V4( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) -> Function-like V30( sigma_Field C : ( ( ) ( V1() V4( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V5( ExtREAL : ( ( ) ( non empty V60() ) set ) ) Function-like non empty V14( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) V30( bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) ext-real-valued ) C_Measure of X : ( ( ) ( ) set ) ) : ( ( non empty ) ( non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive ) Subset-Family of ) , ExtREAL : ( ( ) ( non empty V60() ) set ) ) zeroed V87() sigma-additive ;

end;

theorem :: MEASURE4:15

theorem :: MEASURE4:16