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

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

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

then
M . A is LowerBound of Svc (M,A9)
by XXREAL_2:def 2;
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

hence M . A <= x by A1, A2, A3, A4; :: thesis: verum

end;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

then
SUM (M * Bseq) <= SUM (vol (M,Aseq))
by SUPINF_2:43;
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;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

hence M . A <= x by A1, A2, A3, A4; :: thesis: verum

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