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-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 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 st SSets is non-ascending & M . (SSets . 0 ) < +infty holds
lim (M * SSets) = M . (lim SSets)
let SSets be SetSequence of ; :: 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)

now

let y be set ; :: 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 set such that
B2: ( x in NAT & ((SSets . 0 ) (\) SSets) . x = y ) by FUNCT_2:17;
reconsider x = x as Element of NAT by B2;
(SSets . 0 ) \ (SSets . x) in S ;
hence y in S by B2, SETLIM_2:def 7; :: thesis: verum

end;

then rng ((SSets . 0 ) (\) SSets) c= S by TARSKI:def 3;
then reconsider Bseq = (SSets . 0 ) (\) SSets as SetSequence of by RELAT_1:def 19;
for n, m being Element of NAT st n <= m holds
Bseq . n c= Bseq . m

proof

let n, m be Element of 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 6;
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 A4: Bseq is non-descending by PROB_1:def 7;
then A5: lim (M * Bseq) = M . (lim Bseq) by Th62a
.= M . ((SSets . 0 ) \ (lim SSets)) by A1, SETLIM_1:64, SETLIM_2:86 ;
B3: rng Bseq c= S by RELAT_1:def 19;
B5: rng SSets c= S by RELAT_1:def 19;
then Intersection SSets in S by PROB_1:def 8;
then lim SSets in S by A1, SETLIM_1:61;
then A7: ( lim SSets is Element of S & SSets . 0 is Element of S & (SSets . 0 ) \ (lim SSets) is Element of S ) by PROB_1:44;
then M . (((SSets . 0 ) \ (lim SSets)) \/ (lim SSets)) = (M . ((SSets . 0 ) \ (lim SSets))) + (M . (lim SSets)) by MEASURE1:61, XBOOLE_1:79;
then A8: M . ((SSets . 0 ) \/ (lim SSets)) = (M . ((SSets . 0 ) \ (lim SSets))) + (M . (lim SSets)) by XBOOLE_1:39;
(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 A9: (SSets . 0 ) \/ (lim SSets) = SSets . 0 by XBOOLE_1:12;
( M * Bseq is non-decreasing & M * SSets is non-increasing ) by A4, A1, Lem14, Lem15;
then C1: ( M * Bseq is convergent & M * SSets is convergent ) by RINFSUP2:36, RINFSUP2:37;
deffunc H₁( Element of NAT ) -> Element of ExtREAL = (M * SSets) . 0 ;
consider seq1 being Function of NAT ,ExtREAL such that
B6: for n being Element of NAT holds seq1 . n = H₁(n) from FUNCT_2:sch 4();
( Bseq is Function of NAT ,S & SSets is Function of NAT ,S ) by B3, B5, FUNCT_2:8;
then C2: ( M * Bseq is nonnegative & M * SSets is nonnegative ) by MEASURE2:1;
then ( -infty < (M * SSets) . 0 & (M * SSets) . 0 < +infty ) by A2, SUPINF_2:70, FUNCT_2:21;
then D1: (M * SSets) . 0 in REAL by XXREAL_0:14;
D2: 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 13;
hence seq1 . n = (M * SSets) . 0 by B6; :: thesis: verum

end;

D5: M . ((SSets . 0 ) \ (lim SSets)) <= M . (SSets . 0 ) by A7, MEASURE1:62, XBOOLE_1:36;
D3: ( M . ((SSets . 0 ) \ (lim SSets)) >= 0 & 0 > -infty ) by SUPINF_2:70;
then D4: M . ((SSets . 0 ) \ (lim SSets)) is Real by A2, D5, XXREAL_0:14;
T: M . ((SSets . 0 ) \ (lim SSets)) < +infty by A2, D5, XXREAL_0:2;

now

let k be Nat; :: thesis: seq1 . k = ((M * SSets) . k) + ((M * Bseq) . k)
C3: k is Element of NAT by ORDINAL1:def 13;
SSets . k misses (SSets . 0 ) \ (SSets . k) by XBOOLE_1:79;
then C4: SSets . k misses Bseq . k by C3, SETLIM_2:def 7;
C5: (SSets . k) \/ ((SSets . 0 ) \ (SSets . k)) = (SSets . 0 ) \/ (SSets . k) by XBOOLE_1:39;
SSets . k c= SSets . 0 by A1, C3, PROB_1:def 6;
then (SSets . k) \/ ((SSets . 0 ) \ (SSets . k)) = SSets . 0 by C5, XBOOLE_1:12;
then C6: (SSets . k) \/ (Bseq . k) = SSets . 0 by C3, SETLIM_2:def 7;
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;
( SSets . k1 in S & Bseq . k1 in S ) ;
then M . (SSets . 0 ) = (M . (SSets . k)) + (M . (Bseq . k)) by C6, C4, MEASURE1:61;
then (M * SSets) . 0 = (M . (SSets . k)) + (M . (Bseq . k)) by FUNCT_2:21;
then seq1 . k = (M . (SSets . k)) + (M . (Bseq . k)) by B6, C3;
then seq1 . k = ((M * SSets) . k) + (M . (Bseq . k)) by C3, FUNCT_2:21;
hence seq1 . k = ((M * SSets) . k) + ((M * Bseq) . k) by C3, FUNCT_2:21; :: thesis: verum

end;

then lim seq1 = (lim (M * Bseq)) + (lim (M * SSets)) by C1, C2, MESFUNC9:11;
then (M * SSets) . 0 = (lim (M * Bseq)) + (lim (M * SSets)) by D2, D1, MESFUNC5:58;
then (M . ((SSets . 0 ) \ (lim SSets))) + (M . (lim SSets)) = (lim (M * SSets)) + (M . ((SSets . 0 ) \ (lim SSets))) by A5, A8, A9, FUNCT_2:21;
then M . (lim SSets) = ((lim (M * SSets)) + (M . ((SSets . 0 ) \ (lim SSets)))) - (M . ((SSets . 0 ) \ (lim SSets))) by D3, XXREAL_3:29, T;
hence M . (lim SSets) = lim (M * SSets) by D4, XXREAL_3:22; :: thesis: verum