set M = (bool X) --> 0.;
take (bool X) --> 0. ; :: thesis: ( (bool X) --> 0. is nonnegative & (bool X) --> 0. is zeroed & ( for A, B being Subset of X st A c= B holds
( ((bool X) --> 0.) . A <= ((bool X) --> 0.) . B & ( for F being Function of NAT,(bool X) holds ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F) ) ) ) )
A1: for A being Subset of X holds 0. <= ((bool X) --> 0.) . A ;
then A2: (bool X) --> 0. is nonnegative by MEASURE1:def 4;
A3: for F being Function of NAT,(bool X) holds ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F)

proof

let F be Function of NAT,(bool X); :: thesis: ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F)
A4: ((bool X) --> 0.) . (union (rng F)) = 0. by FUNCOP_1:13;
A5: for r being Element of NAT st 0 <= r holds
(((bool X) --> 0.) * F) . r = 0.

proof

let r be Element of NAT ; :: thesis: ( 0 <= r implies (((bool X) --> 0.) * F) . r = 0. )
dom (((bool X) --> 0.) * F) = NAT by FUNCT_2:def 1;
then (((bool X) --> 0.) * F) . r = ((bool X) --> 0.) . (F . r) by FUNCT_1:22;
hence ( 0 <= r implies (((bool X) --> 0.) * F) . r = 0. ) by FUNCOP_1:13; :: thesis: verum

end;

A6: (Ser (((bool X) --> 0.) * F)) . 0 = (((bool X) --> 0.) * F) . 0 by SUPINF_2:63;
((bool X) --> 0.) * F is nonnegative by A2, MEASURE1:54;
hence ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F) by A4, A5, A6, SUPINF_2:67; :: thesis: verum

end;

{} c= X by XBOOLE_1:2;
then ((bool X) --> 0.) . {} = 0. by FUNCOP_1:13;
hence ( (bool X) --> 0. is nonnegative & (bool X) --> 0. is zeroed & ( for A, B being Subset of X st A c= B holds
( ((bool X) --> 0.) . A <= ((bool X) --> 0.) . B & ( for F being Function of NAT,(bool X) holds ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F) ) ) ) ) by A1, A3, FUNCOP_1:13, MEASURE1:def 4, VALUED_0:def 19; :: thesis: verum