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-ascending & M . (SSets . 0) < +infty 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-ascending & M . (SSets . 0) < +infty 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-ascending & M . (SSets . 0) < +infty holds
lim (M * SSets) = M . (lim SSets)
let SSets be SetSequence of S; :: thesis: ( SSets is non-ascending & M . (SSets . 0) < +infty implies lim (M * SSets) = M . (lim SSets) )
assume that
A1: SSets is non-ascending and
A2: M . (SSets . 0) < +infty ; :: thesis: lim (M * SSets) = M . (lim SSets)
A3: M . ((SSets . 0) \ (lim SSets)) >= 0 by SUPINF_2:51;

now :: thesis: for y being object st y in rng ((SSets . 0) (\) SSets) holds
y in S

let y be object ; :: thesis: ( y in rng ((SSets . 0) (\) SSets) implies y in S )
assume y in rng ((SSets . 0) (\) SSets) ; :: thesis: y in S
then consider x being object such that
A4: x in NAT and
A5: ((SSets . 0) (\) SSets) . x = y by FUNCT_2:11;
reconsider x = x as Element of NAT by A4;
(SSets . 0) \ (SSets . x) in S ;
hence y in S by A5, SETLIM_2:def 7; :: thesis: verum

end;

then rng ((SSets . 0) (\) SSets) c= S ;
then reconsider Bseq = (SSets . 0) (\) SSets as SetSequence of S by RELAT_1:def 19;
deffunc H₁( Element of NAT ) -> Element of ExtREAL = (M * SSets) . 0;
consider seq1 being sequence of ExtREAL such that
A6: for n being Element of NAT holds seq1 . n = H₁(n) from FUNCT_2:sch 4();

A7: now :: thesis: for k being Nat holds seq1 . k = ((M * SSets) . k) + ((M * Bseq) . k)

let k be Nat; :: thesis: seq1 . k = ((M * SSets) . k) + ((M * Bseq) . k)
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
A8: k is Element of NAT by ORDINAL1:def 12;
( (SSets . k) \/ ((SSets . 0) \ (SSets . k)) = (SSets . 0) \/ (SSets . k) & SSets . k c= SSets . 0 ) by A1, PROB_1:def 4, XBOOLE_1:39;
then (SSets . k) \/ ((SSets . 0) \ (SSets . k)) = SSets . 0 by XBOOLE_1:12;
then A9: (SSets . k) \/ (Bseq . k) = SSets . 0 by SETLIM_2:def 7;
SSets . k misses (SSets . 0) \ (SSets . k) by XBOOLE_1:79;
then SSets . k misses Bseq . k by SETLIM_2:def 7;
then M . (SSets . 0) = (M . (SSets . k)) + (M . (Bseq . k)) by A9, MEASURE1:30;
then (M * SSets) . 0 = (M . (SSets . k)) + (M . (Bseq . k)) by FUNCT_2:15;
then seq1 . k = (M . (SSets . k)) + (M . (Bseq . k)) by A6, A8;
then seq1 . k = ((M * SSets) . k) + (M . (Bseq . k)) by A8, FUNCT_2:15;
hence seq1 . k = ((M * SSets) . k) + ((M * Bseq) . k) by A8, FUNCT_2:15; :: thesis: verum

end;

M * SSets is non-increasing by A1, Th30;
then A10: M * SSets is convergent by RINFSUP2:36;
rng Bseq c= S ;
then Bseq is sequence of S by FUNCT_2:6;
then A11: M * Bseq is nonnegative by MEASURE2:1;
A12: for n being Nat holds seq1 . n = (M * SSets) . 0

proof

let n be Nat; :: thesis: seq1 . n = (M * SSets) . 0
n is Element of NAT by ORDINAL1:def 12;
hence seq1 . n = (M * SSets) . 0 by A6; :: thesis: verum

end;

A13: rng SSets c= S ;
then SSets is sequence of S by FUNCT_2:6;
then A14: M * SSets is nonnegative by MEASURE2:1;
then A15: -infty < (M * SSets) . 0 by SUPINF_2:51;
(inferior_setsequence SSets) . (0 + 1) c= SSets . 0 by A1, SETLIM_1:50;
then Intersection SSets c= SSets . 0 by A1, SETLIM_1:52;
then lim SSets c= SSets . 0 by A1, SETLIM_1:61;
then A16: (SSets . 0) \/ (lim SSets) = SSets . 0 by XBOOLE_1:12;
Intersection SSets in S by A13, PROB_1:def 6;
then A17: lim SSets in S by A1, SETLIM_1:61;
then A18: (SSets . 0) \ (lim SSets) is Element of S by PROB_1:6;
then M . (((SSets . 0) \ (lim SSets)) \/ (lim SSets)) = (M . ((SSets . 0) \ (lim SSets))) + (M . (lim SSets)) by A17, MEASURE1:30, XBOOLE_1:79;
then A19: M . ((SSets . 0) \/ (lim SSets)) = (M . ((SSets . 0) \ (lim SSets))) + (M . (lim SSets)) by XBOOLE_1:39;
(M * SSets) . 0 < +infty by A2, FUNCT_2:15;
then A20: (M * SSets) . 0 in REAL by A15, XXREAL_0:14;
for n, m being Nat st n <= m holds
Bseq . n c= Bseq . m

proof

let n, m be Nat; :: thesis: ( n <= m implies Bseq . n c= Bseq . m )
assume n <= m ; :: thesis: Bseq . n c= Bseq . m
then SSets . m c= SSets . n by A1, PROB_1:def 4;
then (SSets . 0) \ (SSets . n) c= (SSets . 0) \ (SSets . m) by XBOOLE_1:34;
then Bseq . n c= (SSets . 0) \ (SSets . m) by SETLIM_2:def 7;
hence Bseq . n c= Bseq . m by SETLIM_2:def 7; :: thesis: verum

end;

then A21: Bseq is non-descending by PROB_1:def 5;
then M * Bseq is non-decreasing by Th29;
then M * Bseq is convergent by RINFSUP2:37;
then lim seq1 = (lim (M * Bseq)) + (lim (M * SSets)) by A10, A11, A14, A7, MESFUNC9:11;
then A22: (M * SSets) . 0 = (lim (M * Bseq)) + (lim (M * SSets)) by A20, A12, MESFUNC5:52;
lim (M * Bseq) = M . (lim Bseq) by A21, Th26
.= M . ((SSets . 0) \ (lim SSets)) by A1, SETLIM_1:64, SETLIM_2:86 ;
then A23: (M . ((SSets . 0) \ (lim SSets))) + (M . (lim SSets)) = (lim (M * SSets)) + (M . ((SSets . 0) \ (lim SSets))) by A19, A16, A22, FUNCT_2:15;
A24: M . ((SSets . 0) \ (lim SSets)) <= M . (SSets . 0) by A18, MEASURE1:31, XBOOLE_1:36;
then M . ((SSets . 0) \ (lim SSets)) < +infty by A2, XXREAL_0:2;
then A25: M . (lim SSets) = ((lim (M * SSets)) + (M . ((SSets . 0) \ (lim SSets)))) - (M . ((SSets . 0) \ (lim SSets))) by A3, A23, XXREAL_3:28;
M . ((SSets . 0) \ (lim SSets)) in REAL by A2, A24, A3, XXREAL_0:14;
hence M . (lim SSets) = lim (M * SSets) by A25, XXREAL_3:22; :: thesis: verum