let X be set ; :: thesis: for F being Field_Subset of X
for M being Measure of F
for k being Nat
for FSets being Set_Sequence of F st ( for n being Nat 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 Nat
for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty
let M be Measure of F; :: thesis: for k being Nat
for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty
let k be Nat; :: thesis: for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty
let FSets be Set_Sequence of F; :: thesis: ( ( for n being Nat holds M . (FSets . n) < +infty ) implies M . ((Partial_Union FSets) . k) < +infty )
defpred S1[ Nat] means M . ((Partial_Union FSets) . $1) < +infty ;
assume A1: for n being Nat holds M . (FSets . n) < +infty ; :: thesis: M . ((Partial_Union FSets) . k) < +infty
A2: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
A3: In (0,REAL) <= M . ((Partial_Union FSets) . k) by SUPINF_2:51;
( M . (FSets . (k + 1)) < +infty & In (0,REAL) <= M . (FSets . (k + 1)) ) by A1, SUPINF_2:51;
then A4: M . (FSets . (k + 1)) in REAL by XXREAL_0:10;
assume S1[k] ; :: thesis: S1[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:10;
hence S1[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: S1[ 0 ] by A1;
for k being Nat holds S1[k] from NAT_1:sch 2(A7, A2);
 hence M . ((Partial_Union FSets) . k) < +infty ; :: thesis: verum