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 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:
reconsider P = {} as Element of S by PROB_1:10;
M . P <= M . (F . 0 ) by MEASURE1:62, XBOOLE_1:2;
then 0. <= M . (F . 0 ) by VALUED_0:def 19;
hence K: M . (F . 0 ) is Real by A1, XXREAL_0:46; :: thesis:
ex x being R_eal st
( x in rng (M * F) & x = M . (F . 0 ) )

proof

A3: dom (M * F) = NAT by FUNCT_2:def 1;
take (M * F) . 0 ; :: thesis:
thus ( (M * F) . 0 in rng (M * F) & (M * F) . 0 = M . (F . 0 ) ) by A3, FUNCT_1:22, FUNCT_2:6; :: thesis:

end;

then A4: inf (rng (M * F)) <= M . (F . 0 ) by XXREAL_2:3;
for x being ext-real number st x in rng (M * F) holds
0. <= x

proof

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

end;

then 0. is LowerBound of rng (M * F) by XXREAL_2:def 2;
then inf (rng (M * F)) >= 0 by XXREAL_2:def 4;
hence inf (rng (M * F)) is Real by A4, K, XXREAL_0:45; :: thesis:
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:
assume A8: x in rng (M * G) ; :: thesis:
A9: dom (M * G) = NAT by FUNCT_2:def 1;
then consider n being set such that
A10: ( n in NAT & (M * G) . n = x ) by A8, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A10;
A11: x = M . (G . n) by A9, A10, FUNCT_1:22;
A12: ( n = 0 implies x <= M . (F . 0 ) ) by A11, A1, MEASURE1:62, XBOOLE_1:2;
( ex k being Nat st n = k + 1 implies x <= M . (F . 0 ) )

proof

given k being Nat such that A13: n = k + 1 ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 13;
G . n = (F . 0 ) \ (F . k) by A1, A13;
hence x <= M . (F . 0 ) by A11, MEASURE1:62, XBOOLE_1:36; :: thesis:

end;

hence x <= M . (F . 0 ) by A12, NAT_1:6; :: thesis:

end;

then A14: M . (F . 0 ) is UpperBound of rng (M * G) by XXREAL_2:def 1;
A15: 0. <= sup (rng (M * G))

proof

A16: for x being R_eal st x in rng (M * G) holds
0. <= x

proof

let x be R_eal; :: thesis:
assume A17: x in rng (M * G) ; :: thesis:
dom (M * G) = NAT by FUNCT_2:def 1;
then A18: ex n being set st
( n in NAT & (M * G) . n = x ) by A17, FUNCT_1:def 5;
M * G is nonnegative by MEASURE2:1;
hence 0. <= x by A18, SUPINF_2:58; :: thesis:

end;

set x = (M * G) . 0 ;
A19: 0. <= (M * G) . 0 by A16, FUNCT_2:6;
(M * G) . 0 <= sup (rng (M * G)) by FUNCT_2:6, XXREAL_2:4;
hence 0. <= sup (rng (M * G)) by A19, XXREAL_0:2; :: thesis:

end;

sup (rng (M * G)) <= M . (F . 0 ) by A14, XXREAL_2:def 3;
hence sup (rng (M * G)) is Real by A15, K, XXREAL_0:45; :: thesis: