let X be set ; :: thesis: for F being Field_Subset of X
for M being Measure of F
for k being natural number
for FSets being Set_Sequence of F st ( for n being natural number holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty
let F be Field_Subset of X; :: thesis: for M being Measure of F
for k being natural number
for FSets being Set_Sequence of F st ( for n being natural number holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty
let M be Measure of F; :: thesis: for k being natural number
for FSets being Set_Sequence of F st ( for n being natural number holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty
let k be natural number ; :: thesis: for FSets being Set_Sequence of F st ( for n being natural number holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty
let FSets be Set_Sequence of F; :: thesis: ( ( for n being natural number holds M . (FSets . n) < +infty ) implies M . ((Partial_Union FSets) . k) < +infty )
defpred S₁[ Nat] means M . ((Partial_Union FSets) . $1) < +infty ;
assume A1: for n being natural number holds M . (FSets . n) < +infty ; :: thesis: M . ((Partial_Union FSets) . k) < +infty

A2: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A3: 0 <= M . ((Partial_Union FSets) . k) by SUPINF_2:70;
( M . (FSets . (k + 1)) < +infty & 0 <= M . (FSets . (k + 1)) ) by A1, SUPINF_2:70;
then A4: M . (FSets . (k + 1)) in REAL by XXREAL_0:10;
assume S₁[k] ; :: thesis: S₁[k + 1]
then M . ((Partial_Union FSets) . k) in REAL by A3, XXREAL_0:10;
then A5: (M . ((Partial_Union FSets) . k)) + (M . (FSets . (k + 1))) in REAL by A4, XREAL_0:def 1;
Partial_Union FSets is Set_Sequence of F by Th15;
then A6: (Partial_Union FSets) . k in F by Def2;
(Partial_Union FSets) . (k + 1) = ((Partial_Union FSets) . k) \/ (FSets . (k + 1)) by PROB_3:def 2;
then M . ((Partial_Union FSets) . (k + 1)) <= (M . ((Partial_Union FSets) . k)) + (M . (FSets . (k + 1))) by A6, MEASURE1:27;
hence S₁[k + 1] by A5, XXREAL_0:9, XXREAL_0:13; :: thesis: verum

end;

(Partial_Union FSets) . 0 = FSets . 0 by PROB_3:def 2;
then A7: S₁[ 0 ] by A1;
for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A2);
hence M . ((Partial_Union FSets) . k) < +infty ; :: thesis: verum