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

proof

let x be ExtReal; :: thesis: ( x in rng (M * G) implies x <= (M . (F . 0)) - (inf (rng (M * F))) )
A4: dom (M * G) = NAT by FUNCT_2:def 1;
assume x in rng (M * G) ; :: thesis: x <= (M . (F . 0)) - (inf (rng (M * F)))
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 nonnegative 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) )

proof

assume A11: n = 0 ; :: thesis: M . ((F . 0) \ (G . n)) in rng (M * F)
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: verum

end;

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

proof

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

proof

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

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: M . ((F . 0) \ (G . n)) in rng (M * F)
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: verum

end;

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

proof

given k being Nat such that A20: n = k + 1 ; :: thesis: G . n c= F . 0
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: verum

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;
then A26: ((M . (F . 0)) - x) + x = (a - b) + b by A24
.= M . (F . 0) by A23 ;
(inf (rng (M * F))) + x = c + b by A24, A25;
then A27: ((inf (rng (M * F))) + x) - (inf (rng (M * F))) = (b + c) - c by A25
.= 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: verum

end;

then A28: (M . (F . 0)) - (inf (rng (M * F))) is UpperBound of rng (M * G) by XXREAL_2:def 1;
A29: for n being Nat holds G . n c= G . (n + 1) by A2, A3, MEASURE2:13;
for y being UpperBound of rng (M * G) holds (M . (F . 0)) - (inf (rng (M * F))) <= y

proof

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

proof

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

proof

let x be ExtReal; :: thesis: ( x in rng (M * F) implies M . (meet (rng F)) <= x )
A30: dom (M * F) = NAT by FUNCT_2:def 1;
assume x in rng (M * F) ; :: thesis: M . (meet (rng F)) <= x
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: verum

end;

then M . (meet (rng F)) is LowerBound of rng (M * F) by XXREAL_2:def 2;
then A34: M . (meet (rng F)) <= inf (rng (M * F)) by XXREAL_2:def 4;
set Q = union (rng G);
sup (rng (M * G)) = M . (union (rng G)) by A29, MEASURE2:23;
then A35: M . (union (rng G)) <= y by XXREAL_2:def 3;
(M . (F . 0)) - (M . (meet (rng F))) = M . (union (rng G)) by A1, A2, A3, Th7;
then (M . (F . 0)) - (inf (rng (M * F))) <= M . (union (rng G)) by A34, XXREAL_3:37;
hence (M . (F . 0)) - (inf (rng (M * F))) <= y by A35, XXREAL_0:2; :: thesis: verum

end;

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

end;

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