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 A' = A as Subset of X ;
for x being ext-real number st x in Svc M,A' holds
M . A <= x

proof

let x be ext-real number ; :: thesis: ( x in Svc M,A' implies M . A <= x )
assume x in Svc M,A' ; :: thesis: M . A <= x
then consider Aseq being Covering of A',F such that
A3: x = SUM (vol M,Aseq) by Def8;
consider Bseq being Sep_Sequence of F such that
A4: ( A = union (rng Bseq) & ( for n being Nat holds Bseq . n c= Aseq . n ) ) by A2, Lem08;
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 A4, MEASURE1:25;
then (M * Bseq) . n <= M . (Aseq . n) by FUNCT_2:21;
hence (M * Bseq) . n <= (vol M,Aseq) . n by Def4; :: thesis: verum

end;

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

end;

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