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

(Volume (M,Cvr)) . n = SUM (vol (M,(Cvr . n))) by Def6;

hence 0 <= (Volume (M,Cvr)) . n by A1, MEASURE6:2; :: thesis: verum

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

then A1:
vol (M,(Cvr . n)) is nonnegative
by SUPINF_2:39;
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;0 <= M . ((Cvr . n) . k) by SUPINF_2:51;

hence 0 <= (vol (M,(Cvr . n))) . k by Def5; :: thesis: verum

(Volume (M,Cvr)) . n = SUM (vol (M,(Cvr . n))) by Def6;

hence 0 <= (Volume (M,Cvr)) . n by A1, MEASURE6:2; :: thesis: verum