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:
then A2: for n being Element of NAT holds G . n c= G . (n + 1) by MEASURE2:15;
reconsider P = {} as Element of S by PROB_1:10;
set l = (M . (F . 0 )) - (inf (rng (M * F)));
A4: (M . (F . 0 )) - (inf (rng (M * F))) is UpperBound of rng (M * G)

proof

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

proof

let x be ext-real number ; :: thesis:
assume A5: x in rng (M * G) ; :: thesis:
A6: ( dom (M * F) = NAT & dom (M * G) = NAT ) by FUNCT_2:def 1;
then consider n being set such that
A7: ( n in NAT & (M * G) . n = x ) by A5, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A7;
A8: M * G is nonnegative by MEASURE2:1;
A9: x = M . (G . n) by A6, A7, FUNCT_1:22;
A10: ( n = 0 implies G . n c= F . 0 ) by A1, XBOOLE_1:2;
A11: ( ex k being Nat st n = k + 1 implies G . n c= F . 0 )

proof

given k being Nat such that A12: n = k + 1 ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 13;
G . n = (F . 0 ) \ (F . k) by A1, A12;
hence G . n c= F . 0 by XBOOLE_1:36; :: thesis:

end;

A14: x <> +infty by A1, A9, A10, A11, MEASURE1:62, NAT_1:6;
x >= 0 by A7, A8, SUPINF_2:58;
then x > -infty by XXREAL_0:2, XXREAL_0:12;
then A16: x is Real by A14, XXREAL_0:14;
reconsider x = x as R_eal by XXREAL_0:def 1;
A17: inf (rng (M * F)) <= (M . (F . 0 )) - x

proof

A18: (M . (F . 0 )) - x = M . ((F . 0 ) \ (G . n)) by A9, A10, A11, A16, MEASURE1:63, NAT_1:6, XXREAL_0:9;
M . ((F . 0 ) \ (G . n)) in rng (M * F)

proof

A19: ( n = 0 implies M . ((F . 0 ) \ (G . n)) in rng (M * F) )

proof

assume A20: n = 0 ; :: thesis:
M . (F . 0 ) = (M * F) . 0 by A6, FUNCT_1:22;
hence M . ((F . 0 ) \ (G . n)) in rng (M * F) by A1, A20, FUNCT_2:6; :: thesis:

end;

( ex k being Nat st n = k + 1 implies M . ((F . 0 ) \ (G . n)) in rng (M * F) )

proof

given k being Nat such that A21: n = k + 1 ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A22: for n being Element of NAT holds F . n c= F . 0

proof

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

proof

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

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A23, A24); :: thesis:

end;

A26: (F . 0 ) \ (G . n) = (F . 0 ) \ ((F . 0 ) \ (F . k)) by A1, A21
.= (F . 0 ) /\ (F . k) by XBOOLE_1:48
.= F . k by A22, XBOOLE_1:28 ;
M . (F . k) = (M * F) . k by A6, FUNCT_1:22;
hence M . ((F . 0 ) \ (G . n)) in rng (M * F) by A26, FUNCT_2:6; :: thesis:

end;

hence M . ((F . 0 ) \ (G . n)) in rng (M * F) by A19, NAT_1:6; :: thesis:

end;

hence inf (rng (M * F)) <= (M . (F . 0 )) - x by A18, XXREAL_2:3; :: thesis:

end;

A27: M . (F . 0 ) is Real by A1, Th11;
inf (rng (M * F)) is Real by A1, Th11;
then consider a, b, c being Real such that
A29: ( a = M . (F . 0 ) & b = x & c = inf (rng (M * F)) ) by A16, A27;
(M . (F . 0 )) - x = a - b by A29, SUPINF_2:5;
then ((M . (F . 0 )) - x) + x = (a - b) + b by A29, SUPINF_2:1
.= M . (F . 0 ) by A29 ;
then A30: (inf (rng (M * F))) + x <= M . (F . 0 ) by A17, XXREAL_3:38;
(inf (rng (M * F))) + x = c + b by A29, SUPINF_2:1;
then ((inf (rng (M * F))) + x) - (inf (rng (M * F))) = (b + c) - c by A29, SUPINF_2:5
.= x by A29 ;
hence x <= (M . (F . 0 )) - (inf (rng (M * F))) by A30, XXREAL_3:39; :: thesis:

end;

hence (M . (F . 0 )) - (inf (rng (M * F))) is UpperBound of rng (M * G) by XXREAL_2:def 1; :: thesis:

end;

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

proof

let y be UpperBound of rng (M * G); :: thesis:
(M . (F . 0 )) - (inf (rng (M * F))) <= y

proof

set Q = union (rng G);
sup (rng (M * G)) = M . (union (rng G)) by A2, MEASURE2:27;
then A32: M . (union (rng G)) <= y by XXREAL_2:def 3;
(M . (F . 0 )) - (inf (rng (M * F))) <= M . (union (rng G))

proof

A33: (M . (F . 0 )) - (M . (meet (rng F))) = M . (union (rng G)) by A1, Th9;
(M . (F . 0 )) - (inf (rng (M * F))) <= M . (union (rng G))

proof

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

proof

let x be ext-real number ; :: thesis:
assume A34: x in rng (M * F) ; :: thesis:
A35: dom (M * F) = NAT by FUNCT_2:def 1;
then consider n being set such that
A36: ( n in NAT & (M * F) . n = x ) by A34, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A36;
A37: x = M . (F . n) by A35, A36, FUNCT_1:22;
meet (rng F) c= F . n by FUNCT_2:6, SETFAM_1:4;
hence M . (meet (rng F)) <= x by A37, MEASURE1:62; :: thesis:

end;

then M . (meet (rng F)) is LowerBound of rng (M * F) by XXREAL_2:def 2;
then M . (meet (rng F)) <= inf (rng (M * F)) by XXREAL_2:def 4;
hence (M . (F . 0 )) - (inf (rng (M * F))) <= M . (union (rng G)) by A33, XXREAL_3:39; :: thesis:

end;

hence (M . (F . 0 )) - (inf (rng (M * F))) <= M . (union (rng G)) ; :: thesis:

end;

hence (M . (F . 0 )) - (inf (rng (M * F))) <= y by A32, XXREAL_0:2; :: thesis:

end;

hence (M . (F . 0 )) - (inf (rng (M * F))) <= y ; :: thesis:

end;

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