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))

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

hence
m is completely-additive
; :: thesis: verum
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) ;

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

assume
union (rng Aseq) in F
; :: thesis: SUM (m * Aseq) = m . (union (rng Aseq))(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 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

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