let X be non empty set ; :: thesis: for F being Field_Subset of X
for m being Measure of F st ex M being sigma_Measure of (sigma F) st M is_extension_of m holds
m is completely-additive
let F be Field_Subset of X; :: thesis: for m being Measure of F st ex M being sigma_Measure of (sigma F) st M is_extension_of m holds
m is completely-additive
let m be Measure of F; :: thesis: ( ex M being sigma_Measure of (sigma F) st M is_extension_of m implies m is completely-additive )
given M being sigma_Measure of (sigma F) such that A1: M is_extension_of m ; :: thesis: m is completely-additive
A2: F c= sigma F by PROB_1:def 9;
for Aseq being Sep_Sequence of F st union (rng Aseq) in F holds
SUM (m * Aseq) = m . (union (rng Aseq))

proof

let Aseq be Sep_Sequence of F; :: thesis: ( union (rng Aseq) in F implies SUM (m * Aseq) = m . (union (rng Aseq)) )
reconsider Bseq = Aseq as sequence of (sigma F) by A2, FUNCT_2:7;
reconsider Bseq = Bseq as Sep_Sequence of (sigma F) ;

A3: now :: thesis: for n being object st n in NAT holds
(M * Bseq) . n = (m * Aseq) . n

let n be object ; :: thesis: ( n in NAT implies (M * Bseq) . n = (m * Aseq) . n )
assume n in NAT ; :: thesis: (M * Bseq) . n = (m * Aseq) . n
then reconsider n9 = n as Element of NAT ;
(M * Bseq) . n = M . (Bseq . n9) by FUNCT_2:15;
then (M * Bseq) . n = m . (Aseq . n9) by A1;
hence (M * Bseq) . n = (m * Aseq) . n by FUNCT_2:15; :: thesis: verum

end;

assume union (rng Aseq) in F ; :: thesis: SUM (m * Aseq) = m . (union (rng Aseq))
then m . (union (rng Aseq)) = M . (union (rng Aseq)) by A1;
then m . (union (rng Aseq)) = SUM (M * Bseq) by MEASURE1:def 6;
hence SUM (m * Aseq) = m . (union (rng Aseq)) by A3, FUNCT_2:12; :: thesis: verum

end;

hence m is completely-additive ; :: thesis: verum