let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S st ex F being Set_Sequence of S st
( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X ) holds
M is sigma_finite
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S st ex F being Set_Sequence of S st
( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X ) holds
M is sigma_finite
let M be sigma_Measure of S; :: 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 ) implies M is sigma_finite )
assume ex F being Set_Sequence of S st
( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X ) ; :: thesis: M is sigma_finite
then consider F being Set_Sequence of S such that
A1: ( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X ) ;
A2: Partial_Union F = F by A1, PROB_4:15;
defpred S₁[ Nat] means (Partial_Diff_Union F) . $1 in S;
(Partial_Diff_Union F) . 0 = F . 0 by PROB_3:def 3;
then A3: S₁[ 0 ] by MEASURE8:def 2;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
A5: (Partial_Union F) . k in S by A2, MEASURE8:def 2;
A6: F . (k + 1) in S by MEASURE8:def 2;
(Partial_Diff_Union F) . (k + 1) = (F . (k + 1)) \ ((Partial_Union F) . k) by PROB_3:def 3;
hence S₁[k + 1] by A5, A6, FINSUB_1:def 3; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
then reconsider E = Partial_Diff_Union F as Set_Sequence of S by MEASURE8:def 2;
defpred S₂[ Nat] means M . (E . $1) < +infty ;
E . 0 = F . 0 by PROB_3:def 3;
then A7: S₂[ 0 ] by A1;
A8: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume S₂[k] ; :: thesis: S₂[k + 1]
A9: ( E . (k + 1) in S & F . (k + 1) in S ) by MEASURE8:def 2;
E . (k + 1) = (F . (k + 1)) \ ((Partial_Union F) . k) by PROB_3:def 3;
then M . (E . (k + 1)) <= M . (F . (k + 1)) by A9, MEASURE1:8, XBOOLE_1:36;
hence S₂[k + 1] by A1, XXREAL_0:2; :: thesis: verum

end;

A10: for n being Nat holds S₂[n] from NAT_1:sch 2(A7, A8);
Union E = Union F by PROB_3:20
.= lim F by A1, SETLIM_1:63 ;
hence M is sigma_finite by A1, A10; :: thesis: verum