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)) - (sup (rng (M * 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)) - (sup (rng (M * 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)) - (sup (rng (M * 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)) - (sup (rng (M * G))) )
assume that
A1: M . (F . 0) < +infty and
A2: ( 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)) - (sup (rng (M * G)))
for n being Element of NAT holds G . n c= G . (n + 1) by A2, MEASURE2:15;
then M . (union (rng G)) = sup (rng (M * G)) by MEASURE2:27;
hence M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) by A1, A2, Th8; :: thesis: verum