let X be set ; for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X
for n being Nat
for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
let F be Field_Subset of X; for M being Measure of F
for Sets being SetSequence of X
for n being Nat
for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
let M be Measure of F; for Sets being SetSequence of X
for n being Nat
for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
let Sets be SetSequence of X; for n being Nat
for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
let n be Nat; for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
let Cvr be Covering of Sets,F; 0 <= (Volume (M,Cvr)) . n
for k being Element of NAT holds 0 <= (vol (M,(Cvr . n))) . k
then A1:
vol (M,(Cvr . n)) is nonnegative
by SUPINF_2:39;
(Volume (M,Cvr)) . n = SUM (vol (M,(Cvr . n)))
by Def6;
hence
0 <= (Volume (M,Cvr)) . n
by A1, MEASURE6:2; verum