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

sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F)))

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

sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F)))

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

sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F)))

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 sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) )

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: sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F)))

set l = (M . (F . 0)) - (inf (rng (M * F)));

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

x <= (M . (F . 0)) - (inf (rng (M * F)))

A29: for n being Nat holds G . n c= G . (n + 1) by A2, A3, MEASURE2:13;

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

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

sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F)))

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

sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F)))

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

sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F)))

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 sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) )

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: sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F)))

set l = (M . (F . 0)) - (inf (rng (M * F)));

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

x <= (M . (F . 0)) - (inf (rng (M * F)))

proof

then A28:
(M . (F . 0)) - (inf (rng (M * F))) 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)) - (inf (rng (M * F))) )

A4: dom (M * G) = NAT by FUNCT_2:def 1;

assume x in rng (M * G) ; :: thesis: x <= (M . (F . 0)) - (inf (rng (M * F)))

then consider n being object such that

A5: n in NAT and

A6: (M * G) . n = x by A4, FUNCT_1:def 3;

M * G is V92() by MEASURE2:1;

then x >= In (0,REAL) by A5, A6, SUPINF_2:39;

then A7: x > -infty by XXREAL_0:2, XXREAL_0:12;

reconsider n = n as Element of NAT by A5;

A8: ( n = 0 implies G . n c= F . 0 ) by A2;

A9: dom (M * F) = NAT by FUNCT_2:def 1;

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

then x <> +infty by A1, A8, A19, MEASURE1:31, NAT_1:6;

then A22: x in REAL by A7, XXREAL_0:14;

reconsider x = x as R_eal by XXREAL_0:def 1;

( M . (F . 0) in REAL & inf (rng (M * F)) in REAL ) by A1, A2, A3, Th9;

then consider a, b, c being Real such that

A23: a = M . (F . 0) and

A24: b = x and

A25: c = inf (rng (M * F)) by A22;

(M . (F . 0)) - x = a - b by A23, A24, SUPINF_2:3;

then A26: ((M . (F . 0)) - x) + x = (a - b) + b by A24, SUPINF_2:1

.= M . (F . 0) by A23 ;

(inf (rng (M * F))) + x = c + b by A24, A25, SUPINF_2:1;

then A27: ((inf (rng (M * F))) + x) - (inf (rng (M * F))) = (b + c) - c by A25, SUPINF_2:3

.= x by A24 ;

(M . (F . 0)) - x = M . ((F . 0) \ (G . n)) by A21, A8, A19, A22, MEASURE1:32, NAT_1:6, XXREAL_0:9;

then inf (rng (M * F)) <= (M . (F . 0)) - x by A10, A12, NAT_1:6, XXREAL_2:3;

then (inf (rng (M * F))) + x <= M . (F . 0) by A26, XXREAL_3:36;

hence x <= (M . (F . 0)) - (inf (rng (M * F))) by A27, XXREAL_3:37; :: thesis: verum

end;A4: dom (M * G) = NAT by FUNCT_2:def 1;

assume x in rng (M * G) ; :: thesis: x <= (M . (F . 0)) - (inf (rng (M * F)))

then consider n being object such that

A5: n in NAT and

A6: (M * G) . n = x by A4, FUNCT_1:def 3;

M * G is V92() by MEASURE2:1;

then x >= In (0,REAL) by A5, A6, SUPINF_2:39;

then A7: x > -infty by XXREAL_0:2, XXREAL_0:12;

reconsider n = n as Element of NAT by A5;

A8: ( n = 0 implies G . n c= F . 0 ) by A2;

A9: dom (M * F) = NAT by FUNCT_2:def 1;

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

proof

A12:
( ex k being Nat st n = k + 1 implies M . ((F . 0) \ (G . n)) in rng (M * F) )
assume A11:
n = 0
; :: thesis: M . ((F . 0) \ (G . n)) in rng (M * F)

M . (F . 0) = (M * F) . 0 by A9, FUNCT_1:12;

hence M . ((F . 0) \ (G . n)) in rng (M * F) by A2, A11, FUNCT_2:4; :: thesis: verum

end;M . (F . 0) = (M * F) . 0 by A9, FUNCT_1:12;

hence M . ((F . 0) \ (G . n)) in rng (M * F) by A2, A11, FUNCT_2:4; :: thesis: verum

proof

A19:
( ex k being Nat st n = k + 1 implies G . n c= F . 0 )
defpred S_{1}[ Nat] means F . $1 c= F . 0;

A13: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

A16: for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A15, A13);

given k being Nat such that A17: n = k + 1 ; :: thesis: M . ((F . 0) \ (G . n)) in rng (M * F)

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A18: M . (F . k) = (M * F) . k by A9, FUNCT_1:12;

(F . 0) \ (G . n) = (F . 0) \ ((F . 0) \ (F . k)) by A3, A17

.= (F . 0) /\ (F . k) by XBOOLE_1:48

.= F . k by A16, XBOOLE_1:28 ;

hence M . ((F . 0) \ (G . n)) in rng (M * F) by A18, FUNCT_2:4; :: thesis: verum

end;A13: for k being Nat st S

S

proof

A15:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A14: F . k c= F . 0 ; :: thesis: S_{1}[k + 1]

F . (k + 1) c= F . k by A3;

hence S_{1}[k + 1]
by A14, XBOOLE_1:1; :: thesis: verum

end;assume A14: F . k c= F . 0 ; :: thesis: S

F . (k + 1) c= F . k by A3;

hence S

A16: for n being Nat holds S

given k being Nat such that A17: n = k + 1 ; :: thesis: M . ((F . 0) \ (G . n)) in rng (M * F)

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A18: M . (F . k) = (M * F) . k by A9, FUNCT_1:12;

(F . 0) \ (G . n) = (F . 0) \ ((F . 0) \ (F . k)) by A3, A17

.= (F . 0) /\ (F . k) by XBOOLE_1:48

.= F . k by A16, XBOOLE_1:28 ;

hence M . ((F . 0) \ (G . n)) in rng (M * F) by A18, FUNCT_2:4; :: thesis: verum

proof

A21:
x = M . (G . n)
by A4, A6, FUNCT_1:12;
given k being Nat such that A20:
n = k + 1
; :: thesis: G . n c= F . 0

reconsider k = k as Element of NAT by ORDINAL1:def 12;

G . n = (F . 0) \ (F . k) by A3, A20;

hence G . n c= F . 0 by 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, A20;

hence G . n c= F . 0 by XBOOLE_1:36; :: thesis: verum

then x <> +infty by A1, A8, A19, MEASURE1:31, NAT_1:6;

then A22: x in REAL by A7, XXREAL_0:14;

reconsider x = x as R_eal by XXREAL_0:def 1;

( M . (F . 0) in REAL & inf (rng (M * F)) in REAL ) by A1, A2, A3, Th9;

then consider a, b, c being Real such that

A23: a = M . (F . 0) and

A24: b = x and

A25: c = inf (rng (M * F)) by A22;

(M . (F . 0)) - x = a - b by A23, A24, SUPINF_2:3;

then A26: ((M . (F . 0)) - x) + x = (a - b) + b by A24, SUPINF_2:1

.= M . (F . 0) by A23 ;

(inf (rng (M * F))) + x = c + b by A24, A25, SUPINF_2:1;

then A27: ((inf (rng (M * F))) + x) - (inf (rng (M * F))) = (b + c) - c by A25, SUPINF_2:3

.= x by A24 ;

(M . (F . 0)) - x = M . ((F . 0) \ (G . n)) by A21, A8, A19, A22, MEASURE1:32, NAT_1:6, XXREAL_0:9;

then inf (rng (M * F)) <= (M . (F . 0)) - x by A10, A12, NAT_1:6, XXREAL_2:3;

then (inf (rng (M * F))) + x <= M . (F . 0) by A26, XXREAL_3:36;

hence x <= (M . (F . 0)) - (inf (rng (M * F))) by A27, XXREAL_3:37; :: thesis: verum

A29: for n being Nat holds G . n c= G . (n + 1) by A2, A3, MEASURE2:13;

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

proof

hence
sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F)))
by A28, XXREAL_2:def 3; :: thesis: verum
let y be UpperBound of rng (M * G); :: thesis: (M . (F . 0)) - (inf (rng (M * F))) <= y

(M . (F . 0)) - (inf (rng (M * F))) <= y

end;(M . (F . 0)) - (inf (rng (M * F))) <= y

proof

hence
(M . (F . 0)) - (inf (rng (M * F))) <= y
; :: thesis: verum
for x being ExtReal st x in rng (M * F) holds

M . (meet (rng F)) <= x

then A34: M . (meet (rng F)) <= inf (rng (M * F)) by XXREAL_2:def 4;

set Q = union (rng G);

sup (rng (M * G)) = M . (union (rng G)) by A29, MEASURE2:23;

then A35: M . (union (rng G)) <= y by XXREAL_2:def 3;

(M . (F . 0)) - (M . (meet (rng F))) = M . (union (rng G)) by A1, A2, A3, Th7;

then (M . (F . 0)) - (inf (rng (M * F))) <= M . (union (rng G)) by A34, XXREAL_3:37;

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

end;M . (meet (rng F)) <= x

proof

then
M . (meet (rng F)) is LowerBound of rng (M * F)
by XXREAL_2:def 2;
let x be ExtReal; :: thesis: ( x in rng (M * F) implies M . (meet (rng F)) <= x )

A30: dom (M * F) = NAT by FUNCT_2:def 1;

assume x in rng (M * F) ; :: thesis: M . (meet (rng F)) <= x

then consider n being object such that

A31: n in NAT and

A32: (M * F) . n = x by A30, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A31;

A33: meet (rng F) c= F . n by FUNCT_2:4, SETFAM_1:3;

x = M . (F . n) by A30, A32, FUNCT_1:12;

hence M . (meet (rng F)) <= x by A33, MEASURE1:31; :: thesis: verum

end;A30: dom (M * F) = NAT by FUNCT_2:def 1;

assume x in rng (M * F) ; :: thesis: M . (meet (rng F)) <= x

then consider n being object such that

A31: n in NAT and

A32: (M * F) . n = x by A30, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A31;

A33: meet (rng F) c= F . n by FUNCT_2:4, SETFAM_1:3;

x = M . (F . n) by A30, A32, FUNCT_1:12;

hence M . (meet (rng F)) <= x by A33, MEASURE1:31; :: thesis: verum

then A34: M . (meet (rng F)) <= inf (rng (M * F)) by XXREAL_2:def 4;

set Q = union (rng G);

sup (rng (M * G)) = M . (union (rng G)) by A29, MEASURE2:23;

then A35: M . (union (rng G)) <= y by XXREAL_2:def 3;

(M . (F . 0)) - (M . (meet (rng F))) = M . (union (rng G)) by A1, A2, A3, Th7;

then (M . (F . 0)) - (inf (rng (M * F))) <= M . (union (rng G)) by A34, XXREAL_3:37;

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