let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being Function of NAT,S st ( for n being Element of NAT holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds
M . (meet (rng F)) = inf (rng (M * F))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for F being Function of NAT,S st ( for n being Element of NAT holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds
M . (meet (rng F)) = inf (rng (M * F))
let M be sigma_Measure of S; :: thesis: for F being Function of NAT,S st ( for n being Element of NAT holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds
M . (meet (rng F)) = inf (rng (M * F))
let F be Function of NAT,S; :: thesis: ( ( for n being Element of NAT holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty implies M . (meet (rng F)) = inf (rng (M * F)) )
assume that
A1: for n being Element of NAT holds F . (n + 1) c= F . n and
A2: M . (F . 0) < +infty ; :: thesis: M . (meet (rng F)) = inf (rng (M * F))
consider G being Function of NAT,S such that
A3: ( G . 0 = {} & ( for n being Element of NAT holds G . (n + 1) = (F . 0) \ (F . n) ) ) by MEASURE2:9;
A4: union (rng G) = (F . 0) \ (meet (rng F)) by A1, A3, Th6;
A5: M . ((F . 0) \ (union (rng G))) = M . (meet (rng F)) by A1, A3, Th7;
A6: for A being Element of S st A = union (rng G) holds
M . (meet (rng F)) = (M . (F . 0)) - (M . A)

proof

let A be Element of S; :: thesis: ( A = union (rng G) implies M . (meet (rng F)) = (M . (F . 0)) - (M . A) )
assume A7: A = union (rng G) ; :: thesis: M . (meet (rng F)) = (M . (F . 0)) - (M . A)
M . ((F . 0) \ (meet (rng F))) <> +infty by A2, MEASURE1:31, XBOOLE_1:36;
then M . A < +infty by A4, A7, XXREAL_0:4;
hence M . (meet (rng F)) = (M . (F . 0)) - (M . A) by A4, A5, A7, MEASURE1:32, XBOOLE_1:36; :: thesis: verum

end;

for n being Element of NAT holds G . n c= G . (n + 1) by A1, A3, MEASURE2:13;
then M . (union (rng G)) = sup (rng (M * G)) by MEASURE2:23;
then M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) by A6;
hence M . (meet (rng F)) = inf (rng (M * F)) by A1, A2, A3, Th13; :: thesis: verum