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
inf (rng (M * 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 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
inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))

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
inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))

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 inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G))) )

assume that
A1: M . (F . 0) < +infty and
A2: G . 0 = {} and
A3: for n being Nat holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; :: thesis: inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))
set l = (M . (F . 0)) - (sup (rng (M * G)));
for x being ExtReal st x in rng (M * F) holds
(M . (F . 0)) - (sup (rng (M * G))) <= x
proof
let x be ExtReal; :: thesis: ( x in rng (M * F) implies (M . (F . 0)) - (sup (rng (M * G))) <= x )
assume A4: x in rng (M * F) ; :: thesis: (M . (F . 0)) - (sup (rng (M * G))) <= x
( x <> +infty implies (M . (F . 0)) - (sup (rng (M * G))) <= x )
proof
A5: dom (M * F) = NAT by FUNCT_2:def 1;
then consider n being object such that
A6: n in NAT and
A7: (M * F) . n = x by ;
M * F is V92() by MEASURE2:1;
then A8: 0. <= x by ;
assume A9: x <> +infty ; :: thesis: (M . (F . 0)) - (sup (rng (M * G))) <= x
reconsider x = x as R_eal by XXREAL_0:def 1;
x <= +infty by XXREAL_0:3;
then x < +infty by ;
then A10: x in REAL by ;
( M . (F . 0) in REAL & sup (rng (M * G)) in REAL ) by A1, A2, A3, Th9;
then consider a, b, c being Real such that
A11: a = M . (F . 0) and
A12: b = x and
A13: c = sup (rng (M * G)) by A10;
(sup (rng (M * G))) + x = c + b by ;
then A14: ((sup (rng (M * G))) + x) - (sup (rng (M * G))) = (b + c) - c by
.= x by A12 ;
reconsider n = n as Element of NAT by A6;
A15: dom (M * G) = NAT by FUNCT_2:def 1;
A16: (M . (F . 0)) - x <= sup (rng (M * G))
proof
set k = n + 1;
A17: for n being Nat holds F . n c= F . 0
proof
defpred S1[ Nat] means F . \$1 c= F . 0;
A18: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A19: F . k c= F . 0 ; :: thesis: S1[k + 1]
F . (k + 1) c= F . k by A3;
hence S1[k + 1] by ; :: thesis: verum
end;
A20: S1[ 0 ] ;
thus for k being Nat holds S1[k] from :: thesis: verum
end;
then M . (F . n) <= M . (F . 0) by MEASURE1:31;
then A21: M . (F . n) < +infty by ;
(M . (F . 0)) - x = (M . (F . 0)) - (M . (F . n)) by
.= M . ((F . 0) \ (F . n)) by
.= M . (G . (n + 1)) by A3 ;
then (M . (F . 0)) - x = (M * G) . (n + 1) by ;
hence (M . (F . 0)) - x <= sup (rng (M * G)) by ; :: thesis: verum
end;
(M . (F . 0)) - x = a - b by ;
then ((M . (F . 0)) - x) + x = (a - b) + b by
.= M . (F . 0) by A11 ;
then M . (F . 0) <= (sup (rng (M * G))) + x by ;
hence (M . (F . 0)) - (sup (rng (M * G))) <= x by ; :: thesis: verum
end;
hence (M . (F . 0)) - (sup (rng (M * G))) <= x by XXREAL_0:4; :: thesis: verum
end;
then A22: (M . (F . 0)) - (sup (rng (M * G))) is LowerBound of rng (M * F) by XXREAL_2:def 2;
for y being LowerBound of rng (M * F) holds y <= (M . (F . 0)) - (sup (rng (M * G)))
proof
A23: inf (rng (M * F)) in REAL by A1, A2, A3, Th9;
( sup (rng (M * G)) in REAL & M . (F . 0) in REAL ) by A1, A2, A3, Th9;
then consider a, b, c being Real such that
A24: a = sup (rng (M * G)) and
A25: b = M . (F . 0) and
A26: c = inf (rng (M * F)) by A23;
(sup (rng (M * G))) + (inf (rng (M * F))) = a + c by ;
then A27: ((sup (rng (M * G))) + (inf (rng (M * F)))) - (sup (rng (M * G))) = (c + a) - a by
.= inf (rng (M * F)) by A26 ;
let y be LowerBound of rng (M * F); :: thesis: y <= (M . (F . 0)) - (sup (rng (M * G)))
consider s, t, r being R_eal such that
s = sup (rng (M * G)) and
t = (M . (F . 0)) - (inf (rng (M * F))) and
A28: r = inf (rng (M * F)) ;
A29: sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) by A1, A2, A3, Th10;
(M . (F . 0)) - (inf (rng (M * F))) = b - c by ;
then ((M . (F . 0)) - (inf (rng (M * F)))) + r = (b - c) + c by
.= M . (F . 0) by A25 ;
hence y <= (M . (F . 0)) - (sup (rng (M * G))) by ; :: thesis: verum
end;
hence inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G))) by ; :: thesis: verum