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 () . (Sets . n) = +infty holds
() . (union (rng Sets)) <= SUM (() * 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 () . (Sets . n) = +infty holds
() . (union (rng Sets)) <= SUM (() * Sets)

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

let Sets be SetSequence of X; :: thesis: ( ex n being Nat st () . (Sets . n) = +infty implies () . (union (rng Sets)) <= SUM (() * Sets) )
assume ex n being Nat st () . (Sets . n) = +infty ; :: thesis: () . (union (rng Sets)) <= SUM (() * 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 ;
dom Sets = NAT by FUNCT_2:def 1;
then ((C_Meas M) * Sets) . N = () . (Sets . N) by FUNCT_1:13;
then SUM (() * Sets) = +infty by ;
hence (C_Meas M) . (union (rng Sets)) <= SUM (() * Sets) by XXREAL_0:3; :: thesis: verum