let X be set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F)))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F)))

let M be sigma_Measure of S; :: thesis: for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F)))

let G, F be sequence of S; :: thesis: ( M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F))) )

assume that

A1: M . (F . 0) < +infty and

A2: ( G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) ) ; :: thesis: M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F)))

A3: meet (rng F) = (F . 0) \ (union (rng G)) by A2, Th5;

A4: M . ((F . 0) \ (meet (rng F))) = M . (union (rng G)) by A2, Th4;

M . ((F . 0) \ (union (rng G))) <> +infty by A1, MEASURE1:31, XBOOLE_1:36;

then M . (meet (rng F)) < +infty by A3, XXREAL_0:4;

hence M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F))) by A3, A4, MEASURE1:32, XBOOLE_1:36; :: thesis: verum

for M being sigma_Measure of S

for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F)))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F)))

let M be sigma_Measure of S; :: thesis: for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds

M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F)))

let G, F be sequence of S; :: thesis: ( M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F))) )

assume that

A1: M . (F . 0) < +infty and

A2: ( G . 0 = {} & ( for n being Nat holds

( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) ) ; :: thesis: M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F)))

A3: meet (rng F) = (F . 0) \ (union (rng G)) by A2, Th5;

A4: M . ((F . 0) \ (meet (rng F))) = M . (union (rng G)) by A2, Th4;

M . ((F . 0) \ (union (rng G))) <> +infty by A1, MEASURE1:31, XBOOLE_1:36;

then M . (meet (rng F)) < +infty by A3, XXREAL_0:4;

hence M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F))) by A3, A4, MEASURE1:32, XBOOLE_1:36; :: thesis: verum