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
proof
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;
then reconsider H = H as sequence of S by FUNCT_2:6;
defpred S1[ 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)) = {}
proof
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) = {}
proof
defpred S2[ Nat] means for k being Element of NAT st $1 < k holds
(G . $1) /\ (F . k) = {} ;
A9: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A10: for k being Element of NAT st n < k holds
(G . n) /\ (F . k) = {} ; :: thesis: S2[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;
A14: S2[ 0 ] by PROB_2:def 2, A1, XBOOLE_0:def 7;
thus for n being Nat holds S2[n] from NAT_1:sch 2(A14, A9); :: thesis: verum
end;
n < n + 1 by NAT_1:13;
hence (G . n) /\ (F . (n + 1)) = {} by A8; :: thesis: verum
end;
A15: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[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: S1[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 S1[k + 1] ; :: thesis: verum
end;
(Ser (M * F)) . 0 = (M * F) . 0 by SUPINF_2:def 11;
then A17: S1[ 0 ] by A1, A6, FUNCT_1:12;
A18: for n being Nat holds S1[n] from NAT_1:sch 2(A17, A15);
 defpred S2[ Nat] means (Ser (M * H)) . $1 = M . (union (rng F));
A19: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[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: S2[n + 1]
then (Ser (M * H)) . (n + 1) = (M . (union (rng F))) + ((M * H) . (n + 1)) by SUPINF_2:def 11;
hence S2[n + 1] by A21, XXREAL_3:4; :: thesis: verum
end;
( (Ser (M * H)) . 0 = (M * H) . 0 & dom (M * H) = NAT ) by FUNCT_2:def 1, SUPINF_2:def 11;
then A22: S2[ 0 ] by A4, FUNCT_1:12;
A23: for n being Nat holds S2[n] from NAT_1:sch 2(A22, A19);
 A24: for r being Element of NAT st 1 <= r holds
(M * H) . r = 0.
proof
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;
A26: for n being Nat holds G . n c= union (rng F)
proof
defpred S3[ Nat] means G . $1 c= union (rng F);
A27: for n being Nat st S3[n] holds
S3[n + 1]
proof
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
assume A28: G . n c= union (rng F) ; :: thesis: S3[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 S3[n + 1] by A28, XBOOLE_1:8; :: thesis: verum
end;
A29: S3[ 0 ] by A1, FUNCT_2:4, ZFMISC_1:74;
thus for n being Nat holds S3[n] from NAT_1:sch 2(A29, A27); :: thesis: verum
end;
A30: for n being Element of NAT holds (Ser (M * F)) . n <= (Ser (M * H)) . n
proof
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;
M * H is nonnegative by MEASURE1:25;
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