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 S_{1}[ 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

then A7: S_{1}[ 0 ]
by A1;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A7, A2);

hence M . ((Partial_Union FSets) . k) < +infty ; :: thesis: verum

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 S

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 S_{1}[k] holds

S_{1}[k + 1]

(Partial_Union FSets) . 0 = FSets . 0
by PROB_3:def 2;S

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[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 S_{1}[k]
; :: thesis: S_{1}[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 S_{1}[k + 1]
by A5, XXREAL_0:9, XXREAL_0:13; :: thesis: verum

end;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 S

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 S

then A7: S

for k being Nat holds S

hence M . ((Partial_Union FSets) . k) < +infty ; :: thesis: verum