let X be set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let G, F be Function of NAT ,S; :: thesis:
assume that
A1: M . (F . 0 ) < +infty and
A2: G . 0 = {} and
A3: for n being Element of 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 ext-real number st x in rng (M * G) holds
x <= (M . (F . 0 )) - (inf (rng (M * F)))

let x be ext-real number ; :: thesis:
A4: dom (M * G) = NAT by FUNCT_2:def 1;
assume x in rng (M * G) ; :: thesis:
then consider n being set such that
A5: n in NAT and
A6: (M * G) . n = x by A4, FUNCT_1:def 5;
M * G is nonnegative by MEASURE2:1;
then x >= 0 by A5, A6, SUPINF_2:58;
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, XBOOLE_1:2;
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:22;
hence M . ((F . 0 ) \ (G . n)) in rng (M * F) by A2, A11, FUNCT_2:6; :: thesis:

end;

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

defpred S₁[ Element of NAT ] means F . $1 c= F . 0 ;
A14: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

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

end;

end;

given k being Nat such that A17: n = k + 1 ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A18: M . (F . k) = (M * F) . k by A9, FUNCT_1:22;
(F . 0 ) \ (G . n) = (F . 0 ) \ ((F . 0 ) \ (F . k)) by A3, A17
.= (F . 0 ) /\ (F . k) by XBOOLE_1:48
.= F . k by A13, XBOOLE_1:28 ;
hence M . ((F . 0 ) \ (G . n)) in rng (M * F) by A18, FUNCT_2:6; :: 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 13;
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:22;
then x <> +infty by A1, A8, A19, MEASURE1:62, NAT_1:6;
then A22: x is Real by A7, XXREAL_0:14;
reconsider x = x as R_eal by XXREAL_0:def 1;
( M . (F . 0 ) is Real & inf (rng (M * F)) is Real ) by A1, A2, A3, Th11;
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:5;
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:5
.= x by A24 ;
(M . (F . 0 )) - x = M . ((F . 0 ) \ (G . n)) by A21, A8, A19, A22, MEASURE1:63, 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:38;
hence x <= (M . (F . 0 )) - (inf (rng (M * F))) by A27, XXREAL_3:39; :: thesis:

end;

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

for x being ext-real number st x in rng (M * F) holds
M . (meet (rng F)) <= x

let x be ext-real number ; :: thesis:
A30: dom (M * F) = NAT by FUNCT_2:def 1;
assume x in rng (M * F) ; :: thesis:
then consider n being set such that
A31: n in NAT and
A32: (M * F) . n = x by A30, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A31;
A33: meet (rng F) c= F . n by FUNCT_2:6, SETFAM_1:4;
x = M . (F . n) by A30, A32, FUNCT_1:22;
hence M . (meet (rng F)) <= x by A33, MEASURE1:62; :: 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:
reconsider P = {} as Element of S by PROB_1:10;