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 sequence of (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 2;
A3: for F being sequence of (bool X) holds ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F)

proof

let F be sequence of (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:7;
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:12;
hence ( 0 <= r implies (((bool X) --> 0.) * F) . r = 0. ) by FUNCOP_1:7; :: thesis: verum

end;

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

end;

{} c= X ;
then ((bool X) --> 0.) . {} = 0. by FUNCOP_1:7;
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 sequence of (bool X) holds ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F) ) ) ) ) by A1, A3, FUNCOP_1:7, MEASURE1:def 2, VALUED_0:def 19; :: thesis: verum