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