consider M being Function of S,ExtREAL such that

A1: for A being Element of S holds M . A = 0. by Th28;

take M ; :: thesis: ( M is V94() & M is sigma-additive & M is zeroed )

for A being Element of S holds 0. <= M . A by A1;

hence A2: M is V94() ; :: thesis: ( M is sigma-additive & M is zeroed )

thus M is sigma-additive :: thesis: M is zeroed

then M . {} = 0. by A1;

hence M is zeroed by VALUED_0:def 19; :: thesis: verum

A1: for A being Element of S holds M . A = 0. by Th28;

take M ; :: thesis: ( M is V94() & M is sigma-additive & M is zeroed )

for A being Element of S holds 0. <= M . A by A1;

hence A2: M is V94() ; :: thesis: ( M is sigma-additive & M is zeroed )

thus M is sigma-additive :: thesis: M is zeroed

proof

{} is Element of S
by PROB_1:4;
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.

then A4: SUM (M * F) = (Ser (M * F)) . 0 by A3, SUPINF_2:48;

union (rng F) is Element of S by Th24;

then A5: M . (union (rng F)) = 0. by A1;

(Ser (M * F)) . 0 = (M * F) . 0 by SUPINF_2:def 11;

hence SUM (M * F) = M . (union (rng F)) by A5, A3, A4; :: thesis: verum

end;A3: for r being Element of NAT st 0 <= r holds

(M * F) . r = 0.

proof

M * F is V94()
by A2, Th25;
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;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

then A4: SUM (M * F) = (Ser (M * F)) . 0 by A3, SUPINF_2:48;

union (rng F) is Element of S by Th24;

then A5: M . (union (rng F)) = 0. by A1;

(Ser (M * F)) . 0 = (M * F) . 0 by SUPINF_2:def 11;

hence SUM (M * F) = M . (union (rng F)) by A5, A3, A4; :: thesis: verum

then M . {} = 0. by A1;

hence M is zeroed by VALUED_0:def 19; :: thesis: verum