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

( (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A & C . (A /\ (Union seq1)) <= SUM (C * (A (/\) 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)

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

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

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

A21:
for A being Subset of X holds
defpred S_{1}[ 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_{1}[k] holds

S_{1}[k + 1]

_{1}[ 0 ]
;

for k being Nat holds S_{1}[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;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

S

proof

A17:
seq . 0 in sigma_Field C
;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[k + 1]

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;assume A4: S

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 >= ((Ser (C * (A (/\) seq1))) . (k + 1)) + (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

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

then A8:
(Ser (C * (A (/\) seq1))) . k <= (Ser (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1))) . k
by Th23;
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;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

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

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

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

then A20:
Slet 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;( 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

for k being Nat holds S

hence ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A ; :: thesis: verum

( (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A & C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1)) )

proof

then A30:
C . ((union (rng seq)) /\ (Union seq1)) <= SUM (C * ((union (rng seq)) (/\) seq1))
;
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 )

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

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

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;for x being ExtReal st x in rng (Ser (C * (A (/\) seq1))) holds

x <= (C . A) - (C . (A /\ (X \ (union (rng seq)))))

proof

then
(C . A) - (C . (A /\ (X \ (union (rng seq))))) is UpperBound of rng (Ser (C * (A (/\) seq1)))
by XXREAL_2:def 1;
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;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

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

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

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

then
Union seq1 in sigma_Field C
by MEASURE4:def 2;
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;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

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

then A40:
SUM (C * ((union (rng seq)) (/\) seq1)) = sup (Ser (C * seq1))
by FUNCT_2:12;
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;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

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