let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for G, F being Function of NAT ,S st M . (F . 0 ) < +infty & G . 0 = {} & ( for n being Element of 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 Function of NAT ,S st M . (F . 0 ) < +infty & G . 0 = {} & ( for n being Element of 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 Function of NAT ,S st M . (F . 0 ) < +infty & G . 0 = {} & ( for n being Element of 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 Function of NAT ,S; :: thesis: ( M . (F . 0 ) < +infty & G . 0 = {} & ( for n being Element of 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 A1: ( M . (F . 0 ) < +infty & G . 0 = {} & ( for n being Element of 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)));
A2: (M . (F . 0 )) - (sup (rng (M * G))) is LowerBound of rng (M * F)

proof

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

proof

let x be ext-real number ; :: thesis: ( x in rng (M * F) implies (M . (F . 0 )) - (sup (rng (M * G))) <= x )
assume A3: x in rng (M * F) ; :: thesis: (M . (F . 0 )) - (sup (rng (M * G))) <= x
(M . (F . 0 )) - (sup (rng (M * G))) <= x

proof

( x <> +infty implies (M . (F . 0 )) - (sup (rng (M * G))) <= x )

proof

assume A4: x <> +infty ; :: thesis: (M . (F . 0 )) - (sup (rng (M * G))) <= x
A5: ( dom (M * F) = NAT & dom (M * G) = NAT ) by FUNCT_2:def 1;
then consider n being set such that
A6: ( n in NAT & (M * F) . n = x ) by A3, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A6;
M * F is nonnegative by MEASURE2:1;
then A7: 0. <= x by A6, SUPINF_2:58;
reconsider x = x as R_eal by XXREAL_0:def 1;
A8: (M . (F . 0 )) - x <= sup (rng (M * G))

proof

A9: for n being Element of NAT holds F . n c= F . 0

proof

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

proof

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

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A10, A11); :: thesis: verum

end;

then M . (F . n) <= M . (F . 0 ) by MEASURE1:62;
then A13: M . (F . n) < +infty by A1, XXREAL_0:2;
A14: (M . (F . 0 )) - x = (M . (F . 0 )) - (M . (F . n)) by A5, A6, FUNCT_1:22
.= M . ((F . 0 ) \ (F . n)) by A9, A13, MEASURE1:63
.= M . (G . (n + 1)) by A1 ;
set k = n + 1;
(M . (F . 0 )) - x = (M * G) . (n + 1) by A5, A14, FUNCT_1:22;
hence (M . (F . 0 )) - x <= sup (rng (M * G)) by FUNCT_2:6, XXREAL_2:4; :: thesis: verum

end;

A15: M . (F . 0 ) is Real by A1, Th11;
x <= +infty by XXREAL_0:3;
then x < +infty by A4, XXREAL_0:1;
then A16: x is Real by A7, XXREAL_0:14, XXREAL_0:46;
sup (rng (M * G)) is Real by A1, Th11;
then consider a, b, c being Real such that
A18: ( a = M . (F . 0 ) & b = x & c = sup (rng (M * G)) ) by A15, A16;
(M . (F . 0 )) - x = a - b by A18, SUPINF_2:5;
then ((M . (F . 0 )) - x) + x = (a - b) + b by A18, SUPINF_2:1
.= M . (F . 0 ) by A18 ;
then A19: M . (F . 0 ) <= (sup (rng (M * G))) + x by A8, XXREAL_3:38;
(sup (rng (M * G))) + x = c + b by A18, SUPINF_2:1;
then ((sup (rng (M * G))) + x) - (sup (rng (M * G))) = (b + c) - c by A18, SUPINF_2:5
.= x by A18 ;
hence (M . (F . 0 )) - (sup (rng (M * G))) <= x by A19, XXREAL_3:39; :: thesis: verum

end;

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

end;

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

end;

hence (M . (F . 0 )) - (sup (rng (M * G))) is LowerBound of rng (M * F) by XXREAL_2:def 2; :: thesis: verum

end;

for y being LowerBound of rng (M * F) holds y <= (M . (F . 0 )) - (sup (rng (M * G)))

proof

let y be LowerBound of rng (M * F); :: thesis: y <= (M . (F . 0 )) - (sup (rng (M * G)))
A21: sup (rng (M * G)) = (M . (F . 0 )) - (inf (rng (M * F))) by A1, Th12;
( sup (rng (M * G)) is Real & M . (F . 0 ) is Real & inf (rng (M * F)) is Real ) by A1, Th11;
then consider a, b, c being Real such that
A22: ( a = sup (rng (M * G)) & b = M . (F . 0 ) & c = inf (rng (M * F)) ) ;
consider s, t, r being R_eal such that
A23: ( s = sup (rng (M * G)) & t = (M . (F . 0 )) - (inf (rng (M * F))) & r = inf (rng (M * F)) ) ;
(M . (F . 0 )) - (inf (rng (M * F))) = b - c by A22, SUPINF_2:5;
then A24: ((M . (F . 0 )) - (inf (rng (M * F)))) + r = (b - c) + c by A22, A23, SUPINF_2:1
.= M . (F . 0 ) by A22 ;
(sup (rng (M * G))) + (inf (rng (M * F))) = a + c by A22, SUPINF_2:1;
then ((sup (rng (M * G))) + (inf (rng (M * F)))) - (sup (rng (M * G))) = (c + a) - a by A22, SUPINF_2:5
.= inf (rng (M * F)) by A22 ;
hence y <= (M . (F . 0 )) - (sup (rng (M * G))) by A21, A23, A24, XXREAL_2:def 4; :: thesis: verum

end;

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