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
( M . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real )
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
( M . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real )
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
( M . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real )
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 ( M . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real ) )
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: ( M . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real )
reconsider P = {} as Element of S by PROB_1:4;
M . P <= M . (F . 0) by MEASURE1:31, XBOOLE_1:2;
then 0. <= M . (F . 0) by VALUED_0:def 19;
hence A4: M . (F . 0) is Real by A1, XXREAL_0:46; :: thesis: ( inf (rng (M * F)) is Real & sup (rng (M * G)) is Real )
for x being ext-real number st x in rng (M * G) holds
x <= M . (F . 0)

proof

let x be ext-real number ; :: thesis: ( x in rng (M * G) implies x <= M . (F . 0) )
A5: dom (M * G) = NAT by FUNCT_2:def 1;
assume x in rng (M * G) ; :: thesis: x <= M . (F . 0)
then consider n being set such that
A6: n in NAT and
A7: (M * G) . n = x by A5, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A6;
A8: x = M . (G . n) by A5, A7, FUNCT_1:12;
A9: ( ex k being Nat st n = k + 1 implies x <= M . (F . 0) )

proof

given k being Nat such that A10: 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 A3, A10;
hence x <= M . (F . 0) by A8, MEASURE1:31, XBOOLE_1:36; :: thesis: verum

end;

( n = 0 implies x <= M . (F . 0) ) by A2, A8, MEASURE1:31, XBOOLE_1:2;
hence x <= M . (F . 0) by A9, NAT_1:6; :: thesis: verum

end;

then M . (F . 0) is UpperBound of rng (M * G) by XXREAL_2:def 1;
then A11: sup (rng (M * G)) <= M . (F . 0) by XXREAL_2:def 3;
for x being ext-real number st x in rng (M * F) holds
0. <= x

proof

let x be ext-real number ; :: thesis: ( x in rng (M * F) implies 0. <= x )
A12: dom (M * F) = NAT by FUNCT_2:def 1;
A13: M * F is nonnegative by MEASURE2:1;
assume x in rng (M * F) ; :: thesis: 0. <= x
then ex n being set st
( n in NAT & (M * F) . n = x ) by A12, FUNCT_1:def 3;
hence 0. <= x by A13, SUPINF_2:39; :: thesis: verum

end;

then 0. is LowerBound of rng (M * F) by XXREAL_2:def 2;
then A14: inf (rng (M * F)) >= 0 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 FUNCT_1:12, FUNCT_2:4; :: thesis: verum

end;

then inf (rng (M * F)) <= M . (F . 0) by XXREAL_2:3;
hence inf (rng (M * F)) is Real by A4, A14, XXREAL_0:45; :: thesis: sup (rng (M * G)) is Real
0. <= 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 )
A15: dom (M * G) = NAT by FUNCT_2:def 1;
A16: M * G is nonnegative by MEASURE2:1;
assume x in rng (M * G) ; :: thesis: 0. <= x
then ex n being set st
( n in NAT & (M * G) . n = x ) by A15, FUNCT_1:def 3;
hence 0. <= x by A16, SUPINF_2:39; :: thesis: verum

end;

then A17: 0. <= (M * G) . 0 by FUNCT_2:4;
(M * G) . 0 <= sup (rng (M * G)) by FUNCT_2:4, XXREAL_2:4;
hence 0. <= sup (rng (M * G)) by A17, XXREAL_0:2; :: thesis: verum

end;

hence sup (rng (M * G)) is Real by A4, A11, XXREAL_0:45; :: thesis: verum