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

now

let x be set ; :: thesis: ( x in rng (@Partial_Diff_Union SSets) implies x in S )
A3: rng (@Partial_Diff_Union SSets) c= S by RELAT_1:def 19;
assume x in rng (@Partial_Diff_Union SSets) ; :: thesis: x in S
hence x in S by A3; :: thesis: verum

end;

then rng (@Partial_Diff_Union SSets) c= S by TARSKI:def 3;
then reconsider Bseq = @Partial_Diff_Union SSets as Sep_Sequence of S by FUNCT_2:8, PROB_3:41;
for n being set 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 set ; :: thesis: ( n in NAT implies (Ser (M * Bseq)) . n = (M * (@Partial_Union SSets)) . n )
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
A6: ( (@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:39, PROB_3:def 3;
(Ser (M * Bseq)) . (k + 1) = ((Ser (M * Bseq)) . k) + ((M * Bseq) . (k + 1)) by SUPINF_2:63
.= ((M * (@Partial_Union SSets)) . k) + (M . ((@Partial_Diff_Union SSets) . (k + 1))) by A5, FUNCT_2:21
.= (M . ((@Partial_Union SSets) . k)) + (M . ((@Partial_Diff_Union SSets) . (k + 1))) by FUNCT_2:21
.= (M . ((@Partial_Union (@Partial_Diff_Union SSets)) . k)) + (M . ((@Partial_Diff_Union SSets) . (k + 1))) by PROB_3:39 ;
then (Ser (M * Bseq)) . (k + 1) = M . (((Partial_Union (@Partial_Diff_Union SSets)) . k) \/ ((@Partial_Diff_Union SSets) . (k + 1))) by A6, MEASURE1:61, 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:39 ;
hence (Ser (M * Bseq)) . (k + 1) = (M * (@Partial_Union SSets)) . (k + 1) by FUNCT_2:21; :: 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:63
.= M . ((@Partial_Diff_Union SSets) . 0) by FUNCT_2:21
.= M . (SSets . 0) by PROB_3:35
.= M . ((@Partial_Union SSets) . 0) by PROB_3:26 ;
then A7: S₁[ 0 ] by FUNCT_2:21;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A7, A4);
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:18;
reconsider Gseq = Ser (M * Bseq) as ExtREAL_sequence ;
M * Bseq is nonnegative by MEASURE1:54;
then for m, n being ext-real number st m in dom Gseq & n in dom Gseq & m <= n holds
Gseq . m <= Gseq . n by MEASURE7:9;
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 11, RINFSUP2:37;
@Partial_Union (@Partial_Diff_Union SSets) = SSets by A2, PROB_3:39;
then Union SSets = Union (@Partial_Diff_Union SSets) by PROB_3:34;
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