let K be disjoint_valued Function of NAT,Family_of_Intervals; :: thesis: ( Union K in Family_of_Intervals implies pre-Meas . (Union K) <= SUM (pre-Meas * K) )
assume A1: Union K in Family_of_Intervals ; :: thesis: pre-Meas . (Union K) <= SUM (pre-Meas * K)
reconsider F = K as sequence of (bool REAL) by FUNCT_2:7;
pre-Meas . (Union K) = OS_Meas . (Union F) by A1, FUNCT_1:49
.= OS_Meas . (union (rng F)) by CARD_3:def 4 ;
then A2: pre-Meas . (Union K) <= SUM (OS_Meas * F) by MEASURE4:def 1;
for n being Element of NAT holds (OS_Meas * F) . n = (pre-Meas * K) . n
proof
let n be Element of NAT ; :: thesis: (OS_Meas * F) . n = (pre-Meas * K) . n
reconsider A = F . n as Subset of REAL ;
A3: ( dom F = NAT & dom K = NAT ) by FUNCT_2:def 1;
then (pre-Meas * K) . n = pre-Meas . (K . n) by FUNCT_1:13
.= OS_Meas . (K . n) by FUNCT_1:49 ;
hence (OS_Meas * F) . n = (pre-Meas * K) . n by A3, FUNCT_1:13; :: thesis: verum
end;
hence pre-Meas . (Union K) <= SUM (pre-Meas * K) by A2, FUNCT_2:def 8; :: thesis: verum