let X be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: for n being Nat
for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
let n be Nat; :: thesis: for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
let Cvr be Covering of Sets,F; :: thesis: 0 <= (Volume (M,Cvr)) . n
for k being Element of NAT holds 0 <= (vol (M,(Cvr . n))) . k
proof
let k be Element of NAT ; :: thesis: 0 <= (vol (M,(Cvr . n))) . k
0 <= M . ((Cvr . n) . k) by SUPINF_2:51;
hence 0 <= (vol (M,(Cvr . n))) . k by Def5; :: thesis: verum
end;
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; :: thesis: verum