let X be set ; :: thesis: for S being SigmaField of X

for M being Measure of S

for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F))

let S be SigmaField of X; :: thesis: for M being Measure of S

for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F))

let M be Measure of S; :: thesis: for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F))

let F be Sep_Sequence of S; :: thesis: SUM (M * F) <= M . (union (rng F))

set T = rng F;

consider G being sequence of S such that

A1: G . 0 = F . 0 and

A2: for n being Nat holds G . (n + 1) = (F . (n + 1)) \/ (G . n) by MEASURE2:4;

{} is Subset of X by XBOOLE_1:2;

then consider H being sequence of (bool X) such that

A3: rng H = {(union (rng F)),{}} and

A4: H . 0 = union (rng F) and

A5: for n being Nat st 0 < n holds

H . n = {} by MEASURE1:19;

rng H c= S

defpred S_{1}[ Nat] means (Ser (M * F)) . $1 = M . (G . $1);

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

A7: for n being Nat holds (G . n) /\ (F . (n + 1)) = {}_{1}[k] holds

S_{1}[k + 1]

then A17: S_{1}[ 0 ]
by A1, A6, FUNCT_1:12;

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

defpred S_{2}[ Nat] means (Ser (M * H)) . $1 = M . (union (rng F));

A19: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]

then A22: S_{2}[ 0 ]
by A4, FUNCT_1:12;

A23: for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A22, A19);

A24: for r being Element of NAT st 1 <= r holds

(M * H) . r = 0.

then SUM (M * H) = (Ser (M * H)) . 1 by A24, SUPINF_2:48;

then SUM (M * H) = M . (union (rng F)) by A23;

hence SUM (M * F) <= M . (union (rng F)) by A30, Th1; :: thesis: verum

for M being Measure of S

for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F))

let S be SigmaField of X; :: thesis: for M being Measure of S

for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F))

let M be Measure of S; :: thesis: for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F))

let F be Sep_Sequence of S; :: thesis: SUM (M * F) <= M . (union (rng F))

set T = rng F;

consider G being sequence of S such that

A1: G . 0 = F . 0 and

A2: for n being Nat holds G . (n + 1) = (F . (n + 1)) \/ (G . n) by MEASURE2:4;

{} is Subset of X by XBOOLE_1:2;

then consider H being sequence of (bool X) such that

A3: rng H = {(union (rng F)),{}} and

A4: H . 0 = union (rng F) and

A5: for n being Nat st 0 < n holds

H . n = {} by MEASURE1:19;

rng H c= S

proof

then reconsider H = H as sequence of S by FUNCT_2:6;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng H or a in S )

assume a in rng H ; :: thesis: a in S

then ( a = union (rng F) or a = {} ) by A3, TARSKI:def 2;

hence a in S by PROB_1:4; :: thesis: verum

end;assume a in rng H ; :: thesis: a in S

then ( a = union (rng F) or a = {} ) by A3, TARSKI:def 2;

hence a in S by PROB_1:4; :: thesis: verum

defpred S

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

A7: for n being Nat holds (G . n) /\ (F . (n + 1)) = {}

proof

A15:
for k being Nat st S
let n be Nat; :: thesis: (G . n) /\ (F . (n + 1)) = {}

A8: for n being Nat

for k being Element of NAT st n < k holds

(G . n) /\ (F . k) = {}

hence (G . n) /\ (F . (n + 1)) = {} by A8; :: thesis: verum

end;A8: for n being Nat

for k being Element of NAT st n < k holds

(G . n) /\ (F . k) = {}

proof

n < n + 1
by NAT_1:13;
defpred S_{2}[ Nat] means for k being Element of NAT st $1 < k holds

(G . $1) /\ (F . k) = {} ;

A9: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]
_{2}[ 0 ]
by PROB_2:def 2, A1, XBOOLE_0:def 7;

thus for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A14, A9); :: thesis: verum

end;(G . $1) /\ (F . k) = {} ;

A9: for n being Nat st S

S

proof

A14:
S
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume A10: for k being Element of NAT st n < k holds

(G . n) /\ (F . k) = {} ; :: thesis: S_{2}[n + 1]

let k be Element of NAT ; :: thesis: ( n + 1 < k implies (G . (n + 1)) /\ (F . k) = {} )

assume A11: n + 1 < k ; :: thesis: (G . (n + 1)) /\ (F . k) = {}

then A12: n < k by NAT_1:13;

F . (n + 1) misses F . k by A11, PROB_2:def 2;

then A13: (F . (n + 1)) /\ (F . k) = {} ;

(G . (n + 1)) /\ (F . k) = ((F . (n + 1)) \/ (G . n)) /\ (F . k) by A2

.= ((F . (n + 1)) /\ (F . k)) \/ ((G . n) /\ (F . k)) by XBOOLE_1:23 ;

hence (G . (n + 1)) /\ (F . k) = {} by A10, A12, A13; :: thesis: verum

end;assume A10: for k being Element of NAT st n < k holds

(G . n) /\ (F . k) = {} ; :: thesis: S

let k be Element of NAT ; :: thesis: ( n + 1 < k implies (G . (n + 1)) /\ (F . k) = {} )

assume A11: n + 1 < k ; :: thesis: (G . (n + 1)) /\ (F . k) = {}

then A12: n < k by NAT_1:13;

F . (n + 1) misses F . k by A11, PROB_2:def 2;

then A13: (F . (n + 1)) /\ (F . k) = {} ;

(G . (n + 1)) /\ (F . k) = ((F . (n + 1)) \/ (G . n)) /\ (F . k) by A2

.= ((F . (n + 1)) /\ (F . k)) \/ ((G . n) /\ (F . k)) by XBOOLE_1:23 ;

hence (G . (n + 1)) /\ (F . k) = {} by A10, A12, A13; :: thesis: verum

thus for n being Nat holds S

hence (G . n) /\ (F . (n + 1)) = {} by A8; :: thesis: verum

S

proof

(Ser (M * F)) . 0 = (M * F) . 0
by SUPINF_2:def 11;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

(G . k) /\ (F . (k + 1)) = {} by A7;

then A16: G . k misses F . (k + 1) ;

assume (Ser (M * F)) . k = M . (G . k) ; :: thesis: S_{1}[k + 1]

then (Ser (M * F)) . (k + 1) = (M . (G . k)) + ((M * F) . (k + 1)) by SUPINF_2:def 11;

then (Ser (M * F)) . (k + 1) = (M . (G . k)) + (M . (F . (k + 1))) by A6, FUNCT_1:12

.= M . ((F . (k + 1)) \/ (G . k)) by A16, MEASURE1:def 3

.= M . (G . (k + 1)) by A2 ;

hence S_{1}[k + 1]
; :: thesis: verum

end;(G . k) /\ (F . (k + 1)) = {} by A7;

then A16: G . k misses F . (k + 1) ;

assume (Ser (M * F)) . k = M . (G . k) ; :: thesis: S

then (Ser (M * F)) . (k + 1) = (M . (G . k)) + ((M * F) . (k + 1)) by SUPINF_2:def 11;

then (Ser (M * F)) . (k + 1) = (M . (G . k)) + (M . (F . (k + 1))) by A6, FUNCT_1:12

.= M . ((F . (k + 1)) \/ (G . k)) by A16, MEASURE1:def 3

.= M . (G . (k + 1)) by A2 ;

hence S

then A17: S

A18: for n being Nat holds S

defpred S

A19: for n being Nat st S

S

proof

( (Ser (M * H)) . 0 = (M * H) . 0 & dom (M * H) = NAT )
by FUNCT_2:def 1, SUPINF_2:def 11;
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

0 <= n by NAT_1:2;

then 0 < n + 1 by NAT_1:13;

then A20: H . (n + 1) = {} by A5;

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

then (M * H) . (n + 1) = M . {} by A20, FUNCT_1:12;

then A21: (M * H) . (n + 1) = 0. by VALUED_0:def 19;

assume (Ser (M * H)) . n = M . (union (rng F)) ; :: thesis: S_{2}[n + 1]

then (Ser (M * H)) . (n + 1) = (M . (union (rng F))) + ((M * H) . (n + 1)) by SUPINF_2:def 11;

hence S_{2}[n + 1]
by A21, XXREAL_3:4; :: thesis: verum

end;0 <= n by NAT_1:2;

then 0 < n + 1 by NAT_1:13;

then A20: H . (n + 1) = {} by A5;

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

then (M * H) . (n + 1) = M . {} by A20, FUNCT_1:12;

then A21: (M * H) . (n + 1) = 0. by VALUED_0:def 19;

assume (Ser (M * H)) . n = M . (union (rng F)) ; :: thesis: S

then (Ser (M * H)) . (n + 1) = (M . (union (rng F))) + ((M * H) . (n + 1)) by SUPINF_2:def 11;

hence S

then A22: S

A23: for n being Nat holds S

A24: for r being Element of NAT st 1 <= r holds

(M * H) . r = 0.

proof

A26:
for n being Nat holds G . n c= union (rng F)
let r be Element of NAT ; :: thesis: ( 1 <= r implies (M * H) . r = 0. )

assume 1 <= r ; :: thesis: (M * H) . r = 0.

then 0 + 1 <= r ;

then 0 < r by NAT_1:13;

then A25: H . r = {} by A5;

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

then (M * H) . r = M . {} by A25, FUNCT_1:12;

hence (M * H) . r = 0. by VALUED_0:def 19; :: thesis: verum

end;assume 1 <= r ; :: thesis: (M * H) . r = 0.

then 0 + 1 <= r ;

then 0 < r by NAT_1:13;

then A25: H . r = {} by A5;

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

then (M * H) . r = M . {} by A25, FUNCT_1:12;

hence (M * H) . r = 0. by VALUED_0:def 19; :: thesis: verum

proof

A30:
for n being Element of NAT holds (Ser (M * F)) . n <= (Ser (M * H)) . n
defpred S_{3}[ Nat] means G . $1 c= union (rng F);

A27: for n being Nat st S_{3}[n] holds

S_{3}[n + 1]
_{3}[ 0 ]
by A1, FUNCT_2:4, ZFMISC_1:74;

thus for n being Nat holds S_{3}[n]
from NAT_1:sch 2(A29, A27); :: thesis: verum

end;A27: for n being Nat st S

S

proof

A29:
S
let n be Nat; :: thesis: ( S_{3}[n] implies S_{3}[n + 1] )

assume A28: G . n c= union (rng F) ; :: thesis: S_{3}[n + 1]

( G . (n + 1) = (F . (n + 1)) \/ (G . n) & F . (n + 1) c= union (rng F) ) by A2, FUNCT_2:4, ZFMISC_1:74;

hence S_{3}[n + 1]
by A28, XBOOLE_1:8; :: thesis: verum

end;assume A28: G . n c= union (rng F) ; :: thesis: S

( G . (n + 1) = (F . (n + 1)) \/ (G . n) & F . (n + 1) c= union (rng F) ) by A2, FUNCT_2:4, ZFMISC_1:74;

hence S

thus for n being Nat holds S

proof

M * H is V92()
by MEASURE1:25;
let n be Element of NAT ; :: thesis: (Ser (M * F)) . n <= (Ser (M * H)) . n

(Ser (M * F)) . n = M . (G . n) by A18;

then (Ser (M * F)) . n <= M . (union (rng F)) by A26, MEASURE1:8;

hence (Ser (M * F)) . n <= (Ser (M * H)) . n by A23; :: thesis: verum

end;(Ser (M * F)) . n = M . (G . n) by A18;

then (Ser (M * F)) . n <= M . (union (rng F)) by A26, MEASURE1:8;

hence (Ser (M * F)) . n <= (Ser (M * H)) . n by A23; :: thesis: verum

then SUM (M * H) = (Ser (M * H)) . 1 by A24, SUPINF_2:48;

then SUM (M * H) = M . (union (rng F)) by A23;

hence SUM (M * F) <= M . (union (rng F)) by A30, Th1; :: thesis: verum