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))

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

hence
M is sigma_Measure of S
by MEASURE1:def 6; :: thesis: verum
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;( 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