let X be set ; :: thesis: for F being Field_Subset of X

for M being Measure of F

for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds

(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

let F be Field_Subset of X; :: thesis: for M being Measure of F

for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds

(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

let M be Measure of F; :: thesis: for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds

(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

let Sets be SetSequence of X; :: thesis: ( ex n being Nat st (C_Meas M) . (Sets . n) = +infty implies (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) )

assume ex n being Nat st (C_Meas M) . (Sets . n) = +infty ; :: thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

then consider N being Nat such that

A1: (C_Meas M) . (Sets . N) = +infty ;

reconsider N = N as Element of NAT by ORDINAL1:def 12;

A2: (C_Meas M) * Sets is nonnegative by Th10, MEASURE1:25;

dom Sets = NAT by FUNCT_2:def 1;

then ((C_Meas M) * Sets) . N = (C_Meas M) . (Sets . N) by FUNCT_1:13;

then SUM ((C_Meas M) * Sets) = +infty by A1, A2, SUPINF_2:45;

hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by XXREAL_0:3; :: thesis: verum

for M being Measure of F

for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds

(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

let F be Field_Subset of X; :: thesis: for M being Measure of F

for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds

(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

let M be Measure of F; :: thesis: for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds

(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

let Sets be SetSequence of X; :: thesis: ( ex n being Nat st (C_Meas M) . (Sets . n) = +infty implies (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) )

assume ex n being Nat st (C_Meas M) . (Sets . n) = +infty ; :: thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

then consider N being Nat such that

A1: (C_Meas M) . (Sets . N) = +infty ;

reconsider N = N as Element of NAT by ORDINAL1:def 12;

A2: (C_Meas M) * Sets is nonnegative by Th10, MEASURE1:25;

dom Sets = NAT by FUNCT_2:def 1;

then ((C_Meas M) * Sets) . N = (C_Meas M) . (Sets . N) by FUNCT_1:13;

then SUM ((C_Meas M) * Sets) = +infty by A1, A2, SUPINF_2:45;

hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by XXREAL_0:3; :: thesis: verum