let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for G, F being Function of NAT ,S st M . (F . 0 ) < +infty & G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0 ) \ (F . n) & F . (n + 1) c= F . n ) ) holds
M . (meet (rng F)) = (M . (F . 0 )) - (M . (union (rng G)))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for G, F being Function of NAT ,S st M . (F . 0 ) < +infty & G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0 ) \ (F . n) & F . (n + 1) c= F . n ) ) holds
M . (meet (rng F)) = (M . (F . 0 )) - (M . (union (rng G)))
let M be sigma_Measure of S; :: thesis: for G, F being Function of NAT ,S st M . (F . 0 ) < +infty & G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0 ) \ (F . n) & F . (n + 1) c= F . n ) ) holds
M . (meet (rng F)) = (M . (F . 0 )) - (M . (union (rng G)))
let G, F be Function of NAT ,S; :: thesis: ( M . (F . 0 ) < +infty & G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0 ) \ (F . n) & F . (n + 1) c= F . n ) ) implies M . (meet (rng F)) = (M . (F . 0 )) - (M . (union (rng G))) )
assume A1: ( M . (F . 0 ) < +infty & G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0 ) \ (F . n) & F . (n + 1) c= F . n ) ) ) ; :: thesis: M . (meet (rng F)) = (M . (F . 0 )) - (M . (union (rng G)))
then A2: union (rng G) = (F . 0 ) \ (meet (rng F)) by Th6;
A3: M . ((F . 0 ) \ (union (rng G))) = M . (meet (rng F)) by A1, Th7;
M . ((F . 0 ) \ (meet (rng F))) <> +infty by A1, MEASURE1:62, XBOOLE_1:36;
then M . (union (rng G)) < +infty by A2, XXREAL_0:4;
hence M . (meet (rng F)) = (M . (F . 0 )) - (M . (union (rng G))) by A2, A3, MEASURE1:63, XBOOLE_1:36; :: thesis: verum