reconsider M = P --> 0. as Function of P,ExtREAL ;
( ( for x being Element of P holds 0. <= M . x ) & M . {} = 0 ) by FUNCOP_1:7, SETFAM_1:def 8;
then reconsider M = M as zeroed nonnegative Function of P,ExtREAL by MEASURE1:def 2, VALUED_0:def 19;
take M ; :: thesis: ( ( for F being disjoint_valued FinSequence of P st Union F in P holds
M . (Union F) = Sum (M * F) ) & ( for K being disjoint_valued Function of NAT,P st Union K in P holds
M . (Union K) <= SUM (M * K) ) )
0 is Element of REAL by XREAL_0:def 1;
then reconsider m = P --> 0 as Function of P,REAL by FUNCOP_1:46;
A2: for F being disjoint_valued FinSequence of P st Union F in P holds
M . (Union F) = Sum (M * F)

proof

let F be disjoint_valued FinSequence of P; :: thesis: ( Union F in P implies M . (Union F) = Sum (M * F) )
assume Union F in P ; :: thesis: M . (Union F) = Sum (M * F)
then A3: M . (Union F) = 0. by FUNCOP_1:7;
( rng F c= P & dom M = P & dom m = P ) by FUNCT_2:def 1;
then A4: ( dom (M * F) = dom F & dom (m * F) = dom F ) by RELAT_1:27;
A7: Sum (M * F) = Sum (m * F) by MESFUNC3:2;
A8: m * F = (F " P) --> 0 by FUNCOP_1:19;
then dom F = F " P by A4, FUNCOP_1:13;
then Seg (len F) = F " P by FINSEQ_1:def 3;
then m * F = (len F) |-> 0 by A8, FINSEQ_2:def 2;
hence M . (Union F) = Sum (M * F) by A3, A7, RVSUM_1:81; :: thesis: verum

end;

for K being disjoint_valued Function of NAT,P st Union K in P holds
M . (Union K) <= SUM (M * K)

proof

let K be disjoint_valued Function of NAT,P; :: thesis: ( Union K in P implies M . (Union K) <= SUM (M * K) )
assume Union K in P ; :: thesis: M . (Union K) <= SUM (M * K)
then A10: M . (Union K) = 0. by FUNCOP_1:7;

now :: thesis: for n being Element of NAT holds (M * K) . n = 0.

let n be Element of NAT ; :: thesis: (M * K) . n = 0.
(M * K) . n = M . (K . n) by FUNCT_2:15;
hence (M * K) . n = 0. by FUNCOP_1:7; :: thesis: verum

end;

hence M . (Union K) <= SUM (M * K) by A10, MEASURE7:1; :: thesis: verum

end;

hence ( ( for F being disjoint_valued FinSequence of P st Union F in P holds
M . (Union F) = Sum (M * F) ) & ( for K being disjoint_valued Function of NAT,P st Union K in P holds
M . (Union K) <= SUM (M * K) ) ) by A2; :: thesis: verum