let X be set ; :: thesis: for F being Field_Subset of X

for M being Measure of F

for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative

let F be Field_Subset of X; :: thesis: for M being Measure of F

for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative

let M be Measure of F; :: thesis: for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative

let FSets be Set_Sequence of F; :: thesis: vol (M,FSets) is nonnegative

for n being Element of NAT holds 0 <= (vol (M,FSets)) . n

for M being Measure of F

for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative

let F be Field_Subset of X; :: thesis: for M being Measure of F

for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative

let M be Measure of F; :: thesis: for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative

let FSets be Set_Sequence of F; :: thesis: vol (M,FSets) is nonnegative

for n being Element of NAT holds 0 <= (vol (M,FSets)) . n

proof

hence
vol (M,FSets) is nonnegative
by SUPINF_2:39; :: thesis: verum
let n be Element of NAT ; :: thesis: 0 <= (vol (M,FSets)) . n

( (vol (M,FSets)) . n = M . (FSets . n) & {} in F ) by Def5, PROB_1:4;

then M . {} <= (vol (M,FSets)) . n by MEASURE1:8, XBOOLE_1:2;

hence 0 <= (vol (M,FSets)) . n by VALUED_0:def 19; :: thesis: verum

end;( (vol (M,FSets)) . n = M . (FSets . n) & {} in F ) by Def5, PROB_1:4;

then M . {} <= (vol (M,FSets)) . n by MEASURE1:8, XBOOLE_1:2;

hence 0 <= (vol (M,FSets)) . n by VALUED_0:def 19; :: thesis: verum