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
( M . (F . 0) in REAL & inf (rng (M * F)) in REAL & sup (rng (M * G)) in REAL )

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
( M . (F . 0) in REAL & inf (rng (M * F)) in REAL & sup (rng (M * G)) in REAL )

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
( M . (F . 0) in REAL & inf (rng (M * F)) in REAL & sup (rng (M * G)) in REAL )

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 ( M . (F . 0) in REAL & inf (rng (M * F)) in REAL & sup (rng (M * G)) in REAL ) )

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: ( M . (F . 0) in REAL & inf (rng (M * F)) in REAL & sup (rng (M * G)) in REAL )
reconsider P = {} as Element of S by PROB_1:4;
A4: 0 in REAL by XREAL_0:def 1;
M . P <= M . (F . 0) by ;
then 0. <= M . (F . 0) by VALUED_0:def 19;
hence A5: M . (F . 0) in REAL by ; :: thesis: ( inf (rng (M * F)) in REAL & sup (rng (M * G)) in REAL )
for x being ExtReal st x in rng (M * G) holds
x <= M . (F . 0)
proof
let x be ExtReal; :: thesis: ( x in rng (M * G) implies x <= M . (F . 0) )
A6: dom (M * G) = NAT by FUNCT_2:def 1;
assume x in rng (M * G) ; :: thesis: x <= M . (F . 0)
then consider n being object such that
A7: n in NAT and
A8: (M * G) . n = x by ;
reconsider n = n as Element of NAT by A7;
A9: x = M . (G . n) by ;
A10: ( ex k being Nat st n = k + 1 implies x <= M . (F . 0) )
proof
given k being Nat such that A11: n = k + 1 ; :: thesis: x <= M . (F . 0)
reconsider k = k as Element of NAT by ORDINAL1:def 12;
G . n = (F . 0) \ (F . k) by ;
hence x <= M . (F . 0) by ; :: thesis: verum
end;
( n = 0 implies x <= M . (F . 0) ) by ;
hence x <= M . (F . 0) by ; :: thesis: verum
end;
then M . (F . 0) is UpperBound of rng (M * G) by XXREAL_2:def 1;
then A12: sup (rng (M * G)) <= M . (F . 0) by XXREAL_2:def 3;
for x being ExtReal st x in rng (M * F) holds
0. <= x
proof
let x be ExtReal; :: thesis: ( x in rng (M * F) implies 0. <= x )
A13: dom (M * F) = NAT by FUNCT_2:def 1;
A14: M * F is V92() by MEASURE2:1;
assume x in rng (M * F) ; :: thesis: 0. <= x
then ex n being object st
( n in NAT & (M * F) . n = x ) by ;
hence 0. <= x by ; :: thesis: verum
end;
then 0. is LowerBound of rng (M * F) by XXREAL_2:def 2;
then A15: inf (rng (M * F)) >= In (0,REAL) by XXREAL_2:def 4;
ex x being R_eal st
( x in rng (M * F) & x = M . (F . 0) )
proof
take (M * F) . 0 ; :: thesis: ( (M * F) . 0 in rng (M * F) & (M * F) . 0 = M . (F . 0) )
dom (M * F) = NAT by FUNCT_2:def 1;
hence ( (M * F) . 0 in rng (M * F) & (M * F) . 0 = M . (F . 0) ) by ; :: thesis: verum
end;
then inf (rng (M * F)) <= M . (F . 0) by XXREAL_2:3;
hence inf (rng (M * F)) in REAL by ; :: thesis: sup (rng (M * G)) in REAL
In (0,REAL) <= sup (rng (M * G))
proof
set x = (M * G) . 0;
for x being R_eal st x in rng (M * G) holds
0. <= x
proof
let x be R_eal; :: thesis: ( x in rng (M * G) implies 0. <= x )
A16: dom (M * G) = NAT by FUNCT_2:def 1;
A17: M * G is V92() by MEASURE2:1;
assume x in rng (M * G) ; :: thesis: 0. <= x
then ex n being object st
( n in NAT & (M * G) . n = x ) by ;
hence 0. <= x by ; :: thesis: verum
end;
then A18: 0. <= (M * G) . 0 by FUNCT_2:4;
(M * G) . 0 <= sup (rng (M * G)) by ;
hence In (0,REAL) <= sup (rng (M * G)) by ; :: thesis: verum
end;
hence sup (rng (M * G)) in REAL by ; :: thesis: verum