let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-descending holds
lim (M * SSets) = M . (lim SSets)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-descending holds
lim (M * SSets) = M . (lim SSets)
let M be sigma_Measure of S; :: thesis: for SSets being SetSequence of S st SSets is non-descending holds
lim (M * SSets) = M . (lim SSets)
let SSets be SetSequence of S; :: thesis: ( SSets is non-descending implies lim (M * SSets) = M . (lim SSets) )
assume A1: SSets is non-descending ; :: thesis: lim (M * SSets) = M . (lim SSets)
then A2: Partial_Union SSets = SSets by PROB_4:19;
rng (Partial_Diff_Union SSets) c= S ;
then reconsider Bseq = Partial_Diff_Union SSets as Sep_Sequence of S by FUNCT_2:6;
for n being object st n in NAT holds
(Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n

proof

defpred S₁[ Nat] means (Ser (M * Bseq)) . $1 = (M * (Partial_Union SSets)) . $1;
let n be object ; :: thesis: ( n in NAT implies (Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n )
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: ( (Partial_Union (Partial_Diff_Union SSets)) . k = (Partial_Union SSets) . k & (Partial_Diff_Union SSets) . (k + 1) = (SSets . (k + 1)) \ ((Partial_Union SSets) . k) ) by PROB_3:35, PROB_3:def 3;
A6: k in NAT by ORDINAL1:def 12;
(Ser (M * Bseq)) . (k + 1) = ((Ser (M * Bseq)) . k) + ((M * Bseq) . (k + 1)) by SUPINF_2:def 11
.= ((M * (Partial_Union SSets)) . k) + (M . ((Partial_Diff_Union SSets) . (k + 1))) by A4, FUNCT_2:15
.= (M . ((Partial_Union SSets) . k)) + (M . ((Partial_Diff_Union SSets) . (k + 1))) by FUNCT_2:15, A6
.= (M . ((Partial_Union (Partial_Diff_Union SSets)) . k)) + (M . ((Partial_Diff_Union SSets) . (k + 1))) by PROB_3:35 ;
then (Ser (M * Bseq)) . (k + 1) = M . (((Partial_Union (Partial_Diff_Union SSets)) . k) \/ ((Partial_Diff_Union SSets) . (k + 1))) by A5, MEASURE1:30, XBOOLE_1:79
.= M . ((Partial_Union (Partial_Diff_Union SSets)) . (k + 1)) by PROB_3:def 2
.= M . ((Partial_Union SSets) . (k + 1)) by PROB_3:35 ;
hence (Ser (M * Bseq)) . (k + 1) = (M * (Partial_Union SSets)) . (k + 1) by FUNCT_2:15; :: thesis: verum

end;

assume n in NAT ; :: thesis: (Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n
then reconsider n1 = n as Element of NAT ;
(Ser (M * Bseq)) . 0 = (M * Bseq) . 0 by SUPINF_2:def 11
.= M . ((Partial_Diff_Union SSets) . 0) by FUNCT_2:15
.= M . (SSets . 0) by PROB_3:31
.= M . ((Partial_Union SSets) . 0) by PROB_3:22 ;
then A7: S₁[ 0 ] by FUNCT_2:15;
for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A3);
then (Ser (M * Bseq)) . n1 = (M * (Partial_Union SSets)) . n1 ;
hence (Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n ; :: thesis: verum

end;

then A8: Ser (M * Bseq) = M * SSets by A2, FUNCT_2:12;
reconsider Gseq = Ser (M * Bseq) as ExtREAL_sequence ;
M * Bseq is nonnegative by MEASURE1:25;
then for m, n being ExtReal st m in dom Gseq & n in dom Gseq & m <= n holds
Gseq . m <= Gseq . n by MEASURE7:8;
then Gseq is non-decreasing by VALUED_0:def 15;
then A9: ( SUM (M * Bseq) = M . (union (rng Bseq)) & lim Gseq = sup Gseq ) by MEASURE1:def 6, RINFSUP2:37;
Partial_Union (Partial_Diff_Union SSets) = SSets by A2, PROB_3:35;
then Union SSets = Union (Partial_Diff_Union SSets) by PROB_3:30;
then lim Gseq = M . (Union SSets) by A9, CARD_3:def 4;
hence lim (M * SSets) = M . (lim SSets) by A1, A8, SETLIM_1:63; :: thesis: verum