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)) - (inf (rng (M * F)));
for x being ExtReal st x in rng (M * G) holds
x <= (M . (F . 0)) - (inf (rng (M * F)))

let x be ExtReal; :: thesis:
A4: dom (M * G) = NAT by FUNCT_2:def 1;
assume x in rng (M * G) ; :: thesis:
then consider n being object such that
A5: n in NAT and
A6: (M * G) . n = x by A4, FUNCT_1:def 3;
M * G is V92() by MEASURE2:1;
then x >= In (0,REAL) by A5, A6, SUPINF_2:39;
then A7: x > -infty by XXREAL_0:2, XXREAL_0:12;
reconsider n = n as Element of NAT by A5;
A8: ( n = 0 implies G . n c= F . 0 ) by A2;
A9: dom (M * F) = NAT by FUNCT_2:def 1;
A10: ( n = 0 implies M . ((F . 0) \ (G . n)) in rng (M * F) )

assume A11: n = 0 ; :: thesis:
M . (F . 0) = (M * F) . 0 by A9, FUNCT_1:12;
hence M . ((F . 0) \ (G . n)) in rng (M * F) by A2, A11, FUNCT_2:4; :: thesis:

end;

A12: ( ex k being Nat st n = k + 1 implies M . ((F . 0) \ (G . n)) in rng (M * F) )

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

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

end;

A15: S₁[ 0 ] ;
A16: for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A13);
given k being Nat such that A17: n = k + 1 ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A18: M . (F . k) = (M * F) . k by A9, FUNCT_1:12;
(F . 0) \ (G . n) = (F . 0) \ ((F . 0) \ (F . k)) by A3, A17
.= (F . 0) /\ (F . k) by XBOOLE_1:48
.= F . k by A16, XBOOLE_1:28 ;
hence M . ((F . 0) \ (G . n)) in rng (M * F) by A18, FUNCT_2:4; :: thesis:

end;

A19: ( ex k being Nat st n = k + 1 implies G . n c= F . 0 )

given k being Nat such that A20: n = k + 1 ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 12;
G . n = (F . 0) \ (F . k) by A3, A20;
hence G . n c= F . 0 by XBOOLE_1:36; :: thesis:

end;

A21: x = M . (G . n) by A4, A6, FUNCT_1:12;
then x <> +infty by A1, A8, A19, MEASURE1:31, NAT_1:6;
then A22: x in REAL by A7, XXREAL_0:14;
reconsider x = x as R_eal by XXREAL_0:def 1;
( M . (F . 0) in REAL & inf (rng (M * F)) in REAL ) by A1, A2, A3, Th9;
then consider a, b, c being Real such that
A23: a = M . (F . 0) and
A24: b = x and
A25: c = inf (rng (M * F)) by A22;
(M . (F . 0)) - x = a - b by A23, A24, SUPINF_2:3;
then A26: ((M . (F . 0)) - x) + x = (a - b) + b by A24, SUPINF_2:1
.= M . (F . 0) by A23 ;
(inf (rng (M * F))) + x = c + b by A24, A25, SUPINF_2:1;
then A27: ((inf (rng (M * F))) + x) - (inf (rng (M * F))) = (b + c) - c by A25, SUPINF_2:3
.= x by A24 ;
(M . (F . 0)) - x = M . ((F . 0) \ (G . n)) by A21, A8, A19, A22, MEASURE1:32, NAT_1:6, XXREAL_0:9;
then inf (rng (M * F)) <= (M . (F . 0)) - x by A10, A12, NAT_1:6, XXREAL_2:3;
then (inf (rng (M * F))) + x <= M . (F . 0) by A26, XXREAL_3:36;
hence x <= (M . (F . 0)) - (inf (rng (M * F))) by A27, XXREAL_3:37; :: thesis:

end;

let y be UpperBound of rng (M * G); :: thesis:
(M . (F . 0)) - (inf (rng (M * F))) <= y

for x being ExtReal st x in rng (M * F) holds
M . (meet (rng F)) <= x

let x be ExtReal; :: thesis:
A30: dom (M * F) = NAT by FUNCT_2:def 1;
assume x in rng (M * F) ; :: thesis:
then consider n being object such that
A31: n in NAT and
A32: (M * F) . n = x by A30, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A31;
A33: meet (rng F) c= F . n by FUNCT_2:4, SETFAM_1:3;
x = M . (F . n) by A30, A32, FUNCT_1:12;
hence M . (meet (rng F)) <= x by A33, MEASURE1:31; :: thesis:

end;

end;

hence (M . (F . 0)) - (inf (rng (M * F))) <= y ; :: thesis:

end;

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