let X be set ; :: thesis: for F being Field_Subset of X
for M being Measure of F st M is completely-additive holds
for A being set st A in F holds
M . A = (C_Meas M) . A
let F be Field_Subset of X; :: thesis: for M being Measure of F st M is completely-additive holds
for A being set st A in F holds
M . A = (C_Meas M) . A
let M be Measure of F; :: thesis: ( M is completely-additive implies for A being set st A in F holds
M . A = (C_Meas M) . A )
assume A1: M is completely-additive ; :: thesis: for A being set st A in F holds
M . A = (C_Meas M) . A
let A be set ; :: thesis: ( A in F implies M . A = (C_Meas M) . A )
assume A2: A in F ; :: thesis: M . A = (C_Meas M) . A
then reconsider A9 = A as Subset of X ;
for x being ExtReal st x in Svc (M,A9) holds
M . A <= x

proof

let x be ExtReal; :: thesis: ( x in Svc (M,A9) implies M . A <= x )
assume x in Svc (M,A9) ; :: thesis: M . A <= x
then consider Aseq being Covering of A9,F such that
A3: x = SUM (vol (M,Aseq)) by Def7;
consider Bseq being Sep_Sequence of F such that
A4: A = union (rng Bseq) and
A5: for n being Nat holds Bseq . n c= Aseq . n by A2, Th17;
for n being Element of NAT holds (M * Bseq) . n <= (vol (M,Aseq)) . n

proof

let n be Element of NAT ; :: thesis: (M * Bseq) . n <= (vol (M,Aseq)) . n
M . (Bseq . n) <= M . (Aseq . n) by A5, MEASURE1:8;
then (M * Bseq) . n <= M . (Aseq . n) by FUNCT_2:15;
hence (M * Bseq) . n <= (vol (M,Aseq)) . n by Def5; :: thesis: verum

end;

then SUM (M * Bseq) <= SUM (vol (M,Aseq)) by SUPINF_2:43;
hence M . A <= x by A1, A2, A3, A4; :: thesis: verum

end;

then M . A is LowerBound of Svc (M,A9) by XXREAL_2:def 2;
then M . A <= inf (Svc (M,A9)) by XXREAL_2:def 4;
then A6: M . A <= (C_Meas M) . A9 by Def8;
(C_Meas M) . A <= M . A by A2, Th9;
hence M . A = (C_Meas M) . A by A6, XXREAL_0:1; :: thesis: verum