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

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

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

then A8:
Ser (M * Bseq) = M * SSets
by A2, FUNCT_2:12;
defpred S_{1}[ 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_{1}[k] holds

S_{1}[k + 1]

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_{1}[ 0 ]
by FUNCT_2:15;

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

S

proof

assume
n in NAT
; :: thesis: (Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[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 A4: S

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

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

for k being Nat holds S

then (Ser (M * Bseq)) . n1 = (M * (Partial_Union SSets)) . n1 ;

hence (Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n ; :: thesis: verum

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