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 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 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 st SSets is non-descending holds
lim (M * SSets) = M . (lim SSets)
let SSets be SetSequence of ; :: thesis: ( SSets is non-descending implies lim (M * SSets) = M . (lim SSets) )
assume A0: SSets is non-descending ; :: thesis: lim (M * SSets) = M . (lim SSets)
then X1: @Partial_Union SSets = SSets by PROB_4:20;
then @Partial_Union (@Partial_Diff_Union SSets) = SSets by PROB_3:39;
then A1: Union SSets = Union (@Partial_Diff_Union SSets) by PROB_3:34;

now

let x be set ; :: thesis: ( x in rng (@Partial_Diff_Union SSets) implies x in S )
assume A2: x in rng (@Partial_Diff_Union SSets) ; :: thesis: x in S
rng (@Partial_Diff_Union SSets) c= S by RELAT_1:def 19;
hence x in S by A2; :: 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 PROB_3:41, FUNCT_2:8;
B0: SUM (M * Bseq) = M . (union (rng Bseq)) by MEASURE1:def 11;
reconsider Gseq = Ser (M * Bseq) as ExtREAL_sequence ;
L1: M * Bseq is nonnegative by MEASURE1:54;
for m, n being ext-real number st m in dom Gseq & n in dom Gseq & m <= n holds
Gseq . m <= Gseq . n by L1, MEASURE7:9;
then Gseq is non-decreasing by VALUED_0:def 15;
then ( Gseq is convergent & lim Gseq = sup Gseq ) by RINFSUP2:37;
then A5: lim Gseq = M . (Union SSets) by B0, A1, CARD_3:def 4;
for n being set st n in NAT holds
(Ser (M * Bseq)) . n = (M * (@Partial_Union SSets)) . n

proof

let n be set ; :: thesis: ( n in NAT implies (Ser (M * Bseq)) . n = (M * (@Partial_Union SSets)) . n )
assume n in NAT ; :: thesis: (Ser (M * Bseq)) . n = (M * (@Partial_Union SSets)) . n
then reconsider n1 = n as Element of NAT ;
defpred S₁[ Nat] means (Ser (M * Bseq)) . $1 = (M * (@Partial_Union SSets)) . $1;
(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 P0: S₁[ 0 ] by FUNCT_2:21;
P1: 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 P2: S₁[k] ; :: thesis: S₁[k + 1]
P3: (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 P2, 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 ;
P5: (@Partial_Union (@Partial_Diff_Union SSets)) . k = (@Partial_Union SSets) . k by PROB_3:39;
(@Partial_Diff_Union SSets) . (k + 1) = (SSets . (k + 1)) \ ((Partial_Union SSets) . k) by PROB_3:def 3;
then (Ser (M * Bseq)) . (k + 1) = M . (((Partial_Union (@Partial_Diff_Union SSets)) . k) \/ ((@Partial_Diff_Union SSets) . (k + 1))) by P3, P5, XBOOLE_1:79, MEASURE1:61
.= 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;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(P0, P1);
then (Ser (M * Bseq)) . n1 = (M * (@Partial_Union SSets)) . n1 ;
hence (Ser (M * Bseq)) . n = (M * (@Partial_Union SSets)) . n ; :: thesis: verum

end;

then Ser (M * Bseq) = M * SSets by X1, FUNCT_2:18;
hence lim (M * SSets) = M . (lim SSets) by A5, A0, SETLIM_1:63; :: thesis: verum