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 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: ( 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)

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

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) )

hence inf (rng (M * F)) in REAL by A5, A15, XXREAL_0:45; :: thesis: sup (rng (M * G)) in REAL

In (0,REAL) <= sup (rng (M * G))

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 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: ( 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

then
M . (F . 0) is UpperBound of rng (M * G)
by XXREAL_2:def 1;
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 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) )

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

end;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 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) )

proof

( n = 0 implies x <= M . (F . 0) )
by A2, A9, MEASURE1:31, XBOOLE_1:2;
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 A3, A11;

hence x <= M . (F . 0) by A9, MEASURE1:31, XBOOLE_1:36; :: thesis: verum

end;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: verum

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

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

then
0. is LowerBound of rng (M * F)
by XXREAL_2:def 2;
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 A13, FUNCT_1:def 3;

hence 0. <= x by A14, SUPINF_2:39; :: thesis: verum

end;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 A13, FUNCT_1:def 3;

hence 0. <= x by A14, SUPINF_2:39; :: thesis: verum

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

then
inf (rng (M * F)) <= M . (F . 0)
by XXREAL_2:3;
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;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

hence inf (rng (M * F)) in REAL by A5, A15, XXREAL_0:45; :: thesis: sup (rng (M * G)) in REAL

In (0,REAL) <= sup (rng (M * G))

proof

hence
sup (rng (M * G)) in REAL
by A5, A12, XXREAL_0:45; :: thesis: verum
set x = (M * G) . 0;

for x being R_eal st x in rng (M * G) holds

0. <= x

(M * G) . 0 <= sup (rng (M * G)) by FUNCT_2:4, XXREAL_2:4;

hence In (0,REAL) <= sup (rng (M * G)) by A18, XXREAL_0:2; :: thesis: verum

end;for x being R_eal st x in rng (M * G) holds

0. <= x

proof

then A18:
0. <= (M * G) . 0
by FUNCT_2:4;
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 A16, FUNCT_1:def 3;

hence 0. <= x by A17, SUPINF_2:39; :: thesis: verum

end;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 A16, FUNCT_1:def 3;

hence 0. <= x by A17, SUPINF_2:39; :: thesis: verum

(M * G) . 0 <= sup (rng (M * G)) by FUNCT_2:4, XXREAL_2:4;

hence In (0,REAL) <= sup (rng (M * G)) by A18, XXREAL_0:2; :: thesis: verum