let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S st M is sigma_finite holds
ex F being Set_Sequence of S st
( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S st M is sigma_finite holds
ex F being Set_Sequence of S st
( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X )
let M be sigma_Measure of S; :: thesis: ( M is sigma_finite implies ex F being Set_Sequence of S st
( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X ) )
assume M is sigma_finite ; :: thesis: ex F being Set_Sequence of S st
( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X )
then consider E being Set_Sequence of S such that
A1: ( ( for n being Nat holds M . (E . n) < +infty ) & Union E = X ) ;
defpred S1[ Nat] means (Partial_Union E) . $1 in S;
(Partial_Union E) . 0 = E . 0 by PROB_3:def 2;
then A2: S1[ 0 ] by MEASURE8:def 2;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
A5: E . (k + 1) in S by MEASURE8:def 2;
(Partial_Union E) . (k + 1) = (E . (k + 1)) \/ ((Partial_Union E) . k) by PROB_3:def 2;
hence S1[k + 1] by A4, A5, FINSUB_1:def 1; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A2, A3);
 then reconsider F = Partial_Union E as Set_Sequence of S by MEASURE8:def 2;
A6: F is non-descending by PROB_3:11;
defpred S2[ Nat] means M . (F . $1) < +infty ;
F . 0 = E . 0 by PROB_3:def 2;
then A7: S2[ 0 ] by A1;
A8: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A9: S2[k] ; :: thesis: S2[k + 1]
M . (E . (k + 1)) < +infty by A1;
then A10: (M . (F . k)) + (M . (E . (k + 1))) < +infty by A9, XXREAL_3:16, XXREAL_0:4;
A11: M . (F . (k + 1)) = M . ((F . k) \/ (E . (k + 1))) by PROB_3:def 2;
( F . k in S & E . (k + 1) in S ) by MEASURE8:def 2;
then M . (F . (k + 1)) <= (M . (F . k)) + (M . (E . (k + 1))) by A11, MEASURE1:33;
hence S2[k + 1] by A10, XXREAL_0:2; :: thesis: verum
end;
A12: for n being Nat holds S2[n] from NAT_1:sch 2(A7, A8);
 lim F = Union F by A6, SETLIM_1:63
.= Union E by PROB_3:15 ;
hence ex F being Set_Sequence of S st
( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X ) by A1, A6, A12; :: thesis: verum