let X be set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let G, F be sequence of S; :: thesis:
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:
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 MEASURE1:31, XBOOLE_1:2;
then 0. <= M . (F . 0) by VALUED_0:def 19;
hence A5: M . (F . 0) in REAL by A1, XXREAL_0:46, A4; :: thesis:
for x being ExtReal st x in rng (M * G) holds
x <= M . (F . 0)

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

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

end;

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

end;

end;

take (M * F) . 0 ; :: thesis:
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:

end;

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

end;

end;