consider M being Function of S,ExtREAL such that
A1: for A being Element of S holds M . A = 0. by Th57;
take M ; :: thesis: ( M is nonnegative & M is sigma-additive & M is zeroed )
for A being Element of S holds 0. <= M . A by A1;
hence A2: M is nonnegative by Def4; :: thesis: ( M is sigma-additive & M is zeroed )
thus M is sigma-additive :: thesis: M is zeroed

proof

let F be Sep_Sequence of S; :: according to MEASURE1:def 6 :: thesis: SUM (M * F) = M . (union (rng F))
A3: for r being Element of NAT st 0 <= r holds
(M * F) . r = 0.

proof

let r be Element of NAT ; :: thesis: ( 0 <= r implies (M * F) . r = 0. )
dom (M * F) = NAT by FUNCT_2:def 1;
then (M * F) . r = M . (F . r) by FUNCT_1:12;
hence ( 0 <= r implies (M * F) . r = 0. ) by A1; :: thesis: verum

end;

M * F is nonnegative by A2, Th54;
then A4: SUM (M * F) = (Ser (M * F)) . 0 by A3, SUPINF_2:48;
union (rng F) is Element of S by Th53;
then A5: M . (union (rng F)) = 0. by A1;
(Ser (M * F)) . 0 = (M * F) . 0 by SUPINF_2:44;
hence SUM (M * F) = M . (union (rng F)) by A5, A3, A4; :: thesis: verum

end;

{} is Element of S by PROB_1:4;
then M . {} = 0. by A1;
hence M is zeroed by VALUED_0:def 19; :: thesis: verum