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 S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[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 ;
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
.= (M . ((Partial_Union SSets) . k)) + (M . ((Partial_Diff_Union SSets) . (k + 1))) by
.= (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
.= 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: S1[ 0 ] by FUNCT_2:15;
for k being Nat holds S1[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 ;
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 ;
Partial_Union (Partial_Diff_Union SSets) = SSets by ;
then Union SSets = Union (Partial_Diff_Union SSets) by PROB_3:30;
then lim Gseq = M . (Union SSets) by ;
hence lim (M * SSets) = M . (lim SSets) by ; :: thesis: verum