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;

then reconsider Bseq = (SSets . 0) (\) SSets as SetSequence of S by RELAT_1:def 19;

deffunc H_{1}( 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_{1}(n)
from FUNCT_2:sch 4();

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

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

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

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

then
rng ((SSets . 0) (\) SSets) c= S
;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;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

then reconsider Bseq = (SSets . 0) (\) SSets as SetSequence of S by RELAT_1:def 19;

deffunc H

consider seq1 being sequence of ExtREAL such that

A6: for n being Element of NAT holds seq1 . n = H

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

M * SSets is non-increasing
by A1, Th30;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;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

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

A13:
rng SSets c= S
;
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;n is Element of NAT by ORDINAL1:def 12;

hence seq1 . n = (M * SSets) . 0 by A6; :: thesis: verum

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

then A21:
Bseq is non-descending
by PROB_1:def 5;
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;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

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