let X be set ; :: thesis: for S being SigmaField of X
for M being Measure of S st ( for F being Sep_Sequence of S holds M . (union (rng F)) <= SUM (M * F) ) holds
M is sigma_Measure of S
let S be SigmaField of X; :: thesis: for M being Measure of S st ( for F being Sep_Sequence of S holds M . (union (rng F)) <= SUM (M * F) ) holds
M is sigma_Measure of S
let M be Measure of S; :: thesis: ( ( for F being Sep_Sequence of S holds M . (union (rng F)) <= SUM (M * F) ) implies M is sigma_Measure of S )
assume A1: for F being Sep_Sequence of S holds M . (union (rng F)) <= SUM (M * F) ; :: thesis: M is sigma_Measure of S
for F being Sep_Sequence of S holds SUM (M * F) = M . (union (rng F))

proof

let F be Sep_Sequence of S; :: thesis: SUM (M * F) = M . (union (rng F))
( M . (union (rng F)) <= SUM (M * F) & SUM (M * F) <= M . (union (rng F)) ) by A1, Th13;
hence SUM (M * F) = M . (union (rng F)) by XXREAL_0:1; :: thesis: verum

end;

hence M is sigma_Measure of S by MEASURE1:def 6; :: thesis: verum