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 () st M is_extension_of m holds

let F be Field_Subset of X; :: thesis: for m being Measure of F st ex M being sigma_Measure of () st M is_extension_of m holds

let m be Measure of F; :: thesis: ( ex M being sigma_Measure of () st M is_extension_of m implies m is completely-additive )
given M being sigma_Measure of () such that A1: M is_extension_of m ; :: thesis:
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 () by ;
reconsider Bseq = Bseq as Sep_Sequence of () ;
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 ; :: thesis: verum
end;
hence m is completely-additive ; :: thesis: verum