let X be set ; :: thesis: for C being C_Measure of X
for seq being Sep_Sequence of (sigma_Field C) holds
( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )
let C be C_Measure of X; :: thesis: for seq being Sep_Sequence of (sigma_Field C) holds
( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )
let seq be Sep_Sequence of (sigma_Field C); :: thesis: ( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )
A1: rng seq c= sigma_Field C by RELAT_1:def 19;
then reconsider seq1 = seq as sequence of (bool X) by FUNCT_2:6;
A2: for A being Subset of X
for n being Element of NAT holds ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A

proof

defpred S₁[ Nat] means for A being Subset of X holds C . A >= ((Ser (C * (A (/\) seq1))) . $1) + (C . (A /\ (X \ (union (rng seq)))));
let A be Subset of X; :: thesis: for n being Element of NAT holds ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A
let n be Element of NAT ; :: thesis: ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]

A5: now :: thesis: for A being Subset of X holds C . (A /\ (X \ (seq1 . (k + 1)))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq)))))

let A be Subset of X; :: thesis: C . (A /\ (X \ (seq1 . (k + 1)))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq)))))
A6: C . (A /\ (X \ (seq1 . (k + 1)))) >= ((Ser (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1))) . k) + (C . ((A /\ (X \ (seq1 . (k + 1)))) /\ (X \ (union (rng seq))))) by A4;
for m being Nat st m <= k holds
(C * (A (/\) seq1)) . m <= (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m

proof

let m be Nat; :: thesis: ( m <= k implies (C * (A (/\) seq1)) . m <= (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m )
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
assume m <= k ; :: thesis: (C * (A (/\) seq1)) . m <= (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m
then m < k + 1 by NAT_1:13;
then seq1 . m misses seq1 . (k + 1) by PROB_2:def 2;
then A7: (seq1 . m) /\ (X \ (seq1 . (k + 1))) = seq1 . m by XBOOLE_1:28, XBOOLE_1:86;
((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1) . m = (A /\ (X \ (seq1 . (k + 1)))) /\ (seq1 . m1) by SETLIM_2:def 5
.= A /\ ((seq1 . m) /\ (X \ (seq1 . (k + 1)))) by XBOOLE_1:16 ;
then ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1) . m = (A (/\) seq1) . m1 by A7, SETLIM_2:def 5;
then (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m1 = C . ((A (/\) seq1) . m1) by FUNCT_2:15;
hence (C * (A (/\) seq1)) . m <= (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m by FUNCT_2:15; :: thesis: verum

end;

then A8: (Ser (C * (A (/\) seq1))) . k <= (Ser (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1))) . k by Th23;
seq1 . (k + 1) c= union (rng seq) by FUNCT_2:4, ZFMISC_1:74;
then (X \ (seq1 . (k + 1))) /\ (X \ (union (rng seq))) = X \ (union (rng seq)) by XBOOLE_1:28, XBOOLE_1:34;
then (A /\ (X \ (seq1 . (k + 1)))) /\ (X \ (union (rng seq))) = A /\ (X \ (union (rng seq))) by XBOOLE_1:16;
then ((Ser (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1))) . k) + (C . ((A /\ (X \ (seq1 . (k + 1)))) /\ (X \ (union (rng seq))))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq))))) by A8, XXREAL_3:36;
hence C . (A /\ (X \ (seq1 . (k + 1)))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq))))) by A6, XXREAL_0:2; :: thesis: verum

end;

let A be Subset of X; :: thesis: C . A >= ((Ser (C * (A (/\) seq1))) . (k + 1)) + (C . (A /\ (X \ (union (rng seq)))))
A /\ (X \ (seq1 . (k + 1))) = (A /\ X) \ (seq1 . (k + 1)) by XBOOLE_1:49
.= A \ (seq1 . (k + 1)) by XBOOLE_1:28 ;
then A9: C . (A \ (seq1 . (k + 1))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq))))) by A5;
A10: A \ (seq1 . (k + 1)) c= X \ (seq1 . (k + 1)) by XBOOLE_1:33;
A11: A \/ (A \ (seq1 . (k + 1))) = A by XBOOLE_1:12, XBOOLE_1:36;
( seq1 . (k + 1) in rng seq & A /\ (seq1 . (k + 1)) c= seq1 . (k + 1) ) by FUNCT_2:4, XBOOLE_1:17;
then (C . (A /\ (seq1 . (k + 1)))) + (C . (A \ (seq1 . (k + 1)))) = C . ((A /\ (seq1 . (k + 1))) \/ (A \ (seq1 . (k + 1)))) by A1, A10, MEASURE4:5
.= C . ((A \/ (A \ (seq1 . (k + 1)))) /\ ((seq1 . (k + 1)) \/ (A \ (seq1 . (k + 1))))) by XBOOLE_1:24
.= C . ((A \/ (A \ (seq1 . (k + 1)))) /\ ((seq1 . (k + 1)) \/ A)) by XBOOLE_1:39 ;
then (C . (A /\ (seq1 . (k + 1)))) + (C . (A \ (seq1 . (k + 1)))) = C . A by A11, XBOOLE_1:7, XBOOLE_1:28;
then A12: C . A >= (((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq)))))) + (C . (A /\ (seq1 . (k + 1)))) by A9, XXREAL_3:36;
A13: ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (seq1 . (k + 1)))) = ((Ser (C * (A (/\) seq1))) . k) + (C . ((A (/\) seq1) . (k + 1))) by SETLIM_2:def 5
.= ((Ser (C * (A (/\) seq1))) . k) + ((C * (A (/\) seq1)) . (k + 1)) by FUNCT_2:15
.= (Ser (C * (A (/\) seq1))) . (k + 1) by SUPINF_2:def 11 ;
A14: C is nonnegative by MEASURE4:def 1;
then A15: C * (A (/\) seq1) is nonnegative by MEASURE1:25;
then (C * (A (/\) seq1)) . k >= 0 by SUPINF_2:51;
then A16: (Ser (C * (A (/\) seq1))) . k > -infty by A15, MEASURE7:2;
( C . (A /\ (X \ (union (rng seq)))) > -infty & C . (A /\ (seq1 . (k + 1))) > -infty ) by A14, SUPINF_2:51;
hence C . A >= ((Ser (C * (A (/\) seq1))) . (k + 1)) + (C . (A /\ (X \ (union (rng seq))))) by A16, A12, A13, XXREAL_3:29; :: thesis: verum

end;

A17: seq . 0 in sigma_Field C ;

now :: thesis: for A being Subset of X holds C . A >= ((Ser (C * (A (/\) seq1))) . 0) + (C . (A /\ (X \ (union (rng seq)))))

let A be Subset of X; :: thesis: C . A >= ((Ser (C * (A (/\) seq1))) . 0) + (C . (A /\ (X \ (union (rng seq)))))
( A /\ (seq1 . 0) c= seq1 . 0 & A /\ (X \ (seq1 . 0)) c= X \ (seq1 . 0) ) by XBOOLE_1:17;
then A18: (C . (A /\ (seq1 . 0))) + (C . (A /\ (X \ (seq1 . 0)))) = C . ((A /\ (seq1 . 0)) \/ (A /\ (X \ (seq1 . 0)))) by A17, MEASURE4:5
.= C . ((A /\ (seq1 . 0)) \/ ((A /\ X) \ (seq1 . 0))) by XBOOLE_1:49
.= C . ((A /\ (seq1 . 0)) \/ (A \ (seq1 . 0))) by XBOOLE_1:28
.= C . A by XBOOLE_1:51 ;
seq1 . 0 c= Union seq1 by ABCMIZ_1:1;
then seq . 0 c= union (rng seq) by CARD_3:def 4;
then X \ (union (rng seq)) c= X \ (seq . 0) by XBOOLE_1:34;
then A /\ (X \ (union (rng seq))) c= A /\ (X \ (seq . 0)) by XBOOLE_1:26;
then A19: C . (A /\ (X \ (union (rng seq)))) <= C . (A /\ (X \ (seq . 0))) by MEASURE4:def 1;
(Ser (C * (A (/\) seq1))) . 0 = (C * (A (/\) seq1)) . 0 by SUPINF_2:def 11
.= C . ((A (/\) seq1) . 0) by FUNCT_2:15
.= C . (A /\ (seq1 . 0)) by SETLIM_2:def 5 ;
hence C . A >= ((Ser (C * (A (/\) seq1))) . 0) + (C . (A /\ (X \ (union (rng seq))))) by A18, A19, XXREAL_3:36; :: thesis: verum

end;

then A20: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A20, A3);
hence ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A ; :: thesis: verum

end;

A21: for A being Subset of X holds
( (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A & C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1)) )

proof

let A be Subset of X; :: thesis: ( (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A & C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1)) )
A22: C is nonnegative by MEASURE4:def 1;
then A23: C * (A (/\) seq1) is nonnegative by MEASURE1:25;
A24: C . (A /\ (X \ (union (rng seq)))) > -infty by A22, SUPINF_2:51;
( ( not C . A = +infty or not C . (A /\ (X \ (union (rng seq)))) = +infty ) implies (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A )

proof

assume A25: ( not C . A = +infty or not C . (A /\ (X \ (union (rng seq)))) = +infty ) ; :: thesis: (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A
for x being ExtReal st x in rng (Ser (C * (A (/\) seq1))) holds
x <= (C . A) - (C . (A /\ (X \ (union (rng seq)))))

proof

let x be ExtReal; :: thesis: ( x in rng (Ser (C * (A (/\) seq1))) implies x <= (C . A) - (C . (A /\ (X \ (union (rng seq))))) )
assume x in rng (Ser (C * (A (/\) seq1))) ; :: thesis: x <= (C . A) - (C . (A /\ (X \ (union (rng seq)))))
then consider i being object such that
A26: i in NAT and
A27: (Ser (C * (A (/\) seq1))) . i = x by FUNCT_2:11;
reconsider i = i as Element of NAT by A26;
(C * (A (/\) seq1)) . i >= 0 by A23, SUPINF_2:51;
then A28: x > -infty by A23, A27, MEASURE7:2;
( C . (A /\ (X \ (union (rng seq)))) > -infty & ((Ser (C * (A (/\) seq1))) . i) + (C . (A /\ (X \ (union (rng seq))))) <= C . A ) by A2, A22, SUPINF_2:51;
hence x <= (C . A) - (C . (A /\ (X \ (union (rng seq))))) by A25, A27, A28, XXREAL_3:56; :: thesis: verum

end;

then (C . A) - (C . (A /\ (X \ (union (rng seq))))) is UpperBound of rng (Ser (C * (A (/\) seq1))) by XXREAL_2:def 1;
then A29: SUM (C * (A (/\) seq1)) <= (C . A) - (C . (A /\ (X \ (union (rng seq))))) by XXREAL_2:def 3;
SUM (C * (A (/\) seq1)) >= 0 by A23, MEASURE6:2;
hence (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A by A24, A29, XXREAL_3:55; :: thesis: verum

end;

hence (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A by XXREAL_0:3; :: thesis: C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1))
C . (union (rng (A (/\) seq1))) <= SUM (C * (A (/\) seq1)) by MEASURE4:def 1;
then C . (Union (A (/\) seq1)) <= SUM (C * (A (/\) seq1)) by CARD_3:def 4;
hence C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1)) by SETLIM_2:38; :: thesis: verum

end;

then A30: C . ((union (rng seq)) /\ (Union seq1)) <= SUM (C * ((union (rng seq)) (/\) seq1)) ;
for W, Z being Subset of X st W c= Union seq1 & Z c= X \ (Union seq1) holds
(C . W) + (C . Z) <= C . (W \/ Z)

proof

let W, Z be Subset of X; :: thesis: ( W c= Union seq1 & Z c= X \ (Union seq1) implies (C . W) + (C . Z) <= C . (W \/ Z) )
assume that
A31: W c= Union seq1 and
A32: Z c= X \ (Union seq1) ; :: thesis: (C . W) + (C . Z) <= C . (W \/ Z)
set A = W \/ Z;
A33: (W \/ Z) /\ (X \ (Union seq1)) = Z \/ (W /\ (X \ (Union seq1))) by A32, XBOOLE_1:30;
X \ (Union seq1) misses Union seq1 by XBOOLE_1:79;
then A34: (X \ (Union seq1)) /\ (Union seq1) = {} by XBOOLE_0:def 7;
W /\ (X \ (Union seq1)) c= (Union seq1) /\ (X \ (Union seq1)) by A31, XBOOLE_1:26;
then W /\ (X \ (Union seq1)) = {} by A34;
then A35: C . Z = C . ((W \/ Z) /\ (X \ (union (rng seq)))) by A33, CARD_3:def 4;
Z /\ (Union seq1) c= (X \ (Union seq1)) /\ (Union seq1) by A32, XBOOLE_1:26;
then A36: Z /\ (Union seq1) = {} by A34;
(W \/ Z) /\ (Union seq1) = W \/ (Z /\ (Union seq1)) by A31, XBOOLE_1:30;
then C . W <= SUM (C * ((W \/ Z) (/\) seq1)) by A21, A36;
then A37: (C . W) + (C . Z) <= (SUM (C * ((W \/ Z) (/\) seq1))) + (C . ((W \/ Z) /\ (X \ (union (rng seq))))) by A35, XXREAL_3:36;
(SUM (C * ((W \/ Z) (/\) seq1))) + (C . ((W \/ Z) /\ (X \ (union (rng seq))))) <= C . (W \/ Z) by A21;
hence (C . W) + (C . Z) <= C . (W \/ Z) by A37, XXREAL_0:2; :: thesis: verum

end;

then Union seq1 in sigma_Field C by MEASURE4:def 2;
hence union (rng seq) in sigma_Field C by CARD_3:def 4; :: thesis: C . (union (rng seq)) = Sum (C * seq)
set Sseq = Ser (C * seq1);
union (rng seq) misses X \ (union (rng seq)) by XBOOLE_1:79;
then A38: (union (rng seq)) /\ (X \ (union (rng seq))) = {} by XBOOLE_0:def 7;
C is zeroed by MEASURE4:def 1;
then A39: C . ((union (rng seq)) /\ (X \ (union (rng seq)))) = 0 by A38, VALUED_0:def 19;
for n being object st n in NAT holds
((union (rng seq)) (/\) seq1) . n = seq . n

proof

let n be object ; :: thesis: ( n in NAT implies ((union (rng seq)) (/\) seq1) . n = seq . n )
assume n in NAT ; :: thesis: ((union (rng seq)) (/\) seq1) . n = seq . n
then reconsider n1 = n as Element of NAT ;
seq1 . n1 c= union (rng seq) by FUNCT_2:4, ZFMISC_1:74;
then (union (rng seq)) /\ (seq1 . n1) = seq . n by XBOOLE_1:28;
hence ((union (rng seq)) (/\) seq1) . n = seq . n by SETLIM_2:def 5; :: thesis: verum

end;

then A40: SUM (C * ((union (rng seq)) (/\) seq1)) = sup (Ser (C * seq1)) by FUNCT_2:12;
C is nonnegative by MEASURE4:def 1;
then C * seq1 is nonnegative by MEASURE1:25;
then for m, n being ExtReal st m in dom (Ser (C * seq1)) & n in dom (Ser (C * seq1)) & m <= n holds
(Ser (C * seq1)) . m <= (Ser (C * seq1)) . n by MEASURE7:8;
then Ser (C * seq1) is non-decreasing by VALUED_0:def 15;
then SUM (C * ((union (rng seq)) (/\) seq1)) = lim (Ser (C * seq1)) by A40, RINFSUP2:37;
then A41: SUM (C * ((union (rng seq)) (/\) seq1)) = lim (Partial_Sums (C * seq1)) by Th1;
(SUM (C * ((union (rng seq)) (/\) seq1))) + (C . ((union (rng seq)) /\ (X \ (union (rng seq))))) <= C . (union (rng seq)) by A21;
then ( union (rng seq) = Union seq1 & C . (union (rng seq)) >= Sum (C * seq) ) by A39, A41, CARD_3:def 4, XXREAL_3:4;
hence C . (union (rng seq)) = Sum (C * seq) by A30, A41, XXREAL_0:1; :: thesis: verum