let X be set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let G, F be sequence of S; :: thesis:
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:
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

let x be ExtReal; :: thesis:
assume A4: x in rng (M * F) ; :: thesis:
( x <> +infty implies (M . (F . 0)) - (sup (rng (M * G))) <= x )

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 A4, FUNCT_1:def 3;
M * F is nonnegative by MEASURE2:1;
then A8: 0. <= x by A6, A7, SUPINF_2:39;
assume A9: x <> +infty ; :: thesis:
reconsider x = x as R_eal by XXREAL_0:def 1;
x <= +infty by XXREAL_0:3;
then x < +infty by A9, XXREAL_0:1;
then A10: x in REAL by A8, XXREAL_0:14, XXREAL_0:46;
( 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 A12, A13;
then A14: ((sup (rng (M * G))) + x) - (sup (rng (M * G))) = (b + c) - c by A13
.= 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))

set k = n + 1;
A17: for n being Nat holds F . n c= F . 0

defpred S₁[ Nat] means F . $1 c= F . 0;
A18: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A19: F . k c= F . 0 ; :: thesis:
F . (k + 1) c= F . k by A3;
hence S₁[k + 1] by A19, XBOOLE_1:1; :: thesis:

end;

end;

then M . (F . n) <= M . (F . 0) by MEASURE1:31;
then A21: M . (F . n) < +infty by A1, XXREAL_0:2;
(M . (F . 0)) - x = (M . (F . 0)) - (M . (F . n)) by A5, A7, FUNCT_1:12
.= M . ((F . 0) \ (F . n)) by A17, A21, MEASURE1:32
.= M . (G . (n + 1)) by A3 ;
then (M . (F . 0)) - x = (M * G) . (n + 1) by A15, FUNCT_1:12;
hence (M . (F . 0)) - x <= sup (rng (M * G)) by FUNCT_2:4, XXREAL_2:4; :: thesis:

end;

(M . (F . 0)) - x = a - b by A11, A12;
then ((M . (F . 0)) - x) + x = (a - b) + b by A12
.= M . (F . 0) by A11 ;
then M . (F . 0) <= (sup (rng (M * G))) + x by A16, XXREAL_3:36;
hence (M . (F . 0)) - (sup (rng (M * G))) <= x by A14, XXREAL_3:37; :: thesis:

end;

hence (M . (F . 0)) - (sup (rng (M * G))) <= x by XXREAL_0:4; :: thesis:

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)))

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 A24, A26;
then A27: ((sup (rng (M * G))) + (inf (rng (M * F)))) - (sup (rng (M * G))) = (c + a) - a by A24
.= inf (rng (M * F)) by A26 ;
let y be LowerBound of rng (M * F); :: thesis:
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 A25, A26;
then ((M . (F . 0)) - (inf (rng (M * F)))) + r = (b - c) + c by A26, A28
.= M . (F . 0) by A25 ;
hence y <= (M . (F . 0)) - (sup (rng (M * G))) by A29, A28, A27, XXREAL_2:def 4; :: thesis:

end;

hence inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G))) by A22, XXREAL_2:def 4; :: thesis: