let X be non empty set ; :: thesis: for F being Field_Subset of X
for m being Measure of F st m is completely-additive holds
ex M being sigma_Measure of (sigma F) st
( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )
let F be Field_Subset of X; :: thesis: for m being Measure of F st m is completely-additive holds
ex M being sigma_Measure of (sigma F) st
( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )
let m be Measure of F; :: thesis: ( m is completely-additive implies ex M being sigma_Measure of (sigma F) st
( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) ) )
assume B1: m is completely-additive ; :: thesis: ex M being sigma_Measure of (sigma F) st
( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )
B3: F c= sigma_Field (C_Meas m) by Th52;
then B2: ( F c= sigma F & sigma F c= sigma_Field (C_Meas m) ) by PROB_1:def 14;
set M = (sigma_Meas (C_Meas m)) | (sigma F);
reconsider M = (sigma_Meas (C_Meas m)) | (sigma F) as Function of (sigma F),ExtREAL by B2, FUNCT_2:38;
B8: M . {} = (sigma_Meas (C_Meas m)) . {} by PROB_1:42, FUNCT_1:72
.= 0 by VALUED_0:def 19 ;
for SS being Sep_Sequence of (sigma F) holds SUM (M * SS) = M . (union (rng SS))

proof

let SS be Sep_Sequence of (sigma F); :: thesis: SUM (M * SS) = M . (union (rng SS))
reconsider SS' = SS as Sep_Sequence of (sigma_Field (C_Meas m)) by B2, FUNCT_2:9;
B9: rng SS c= sigma F by RELAT_1:def 19;
M * SS = (sigma_Meas (C_Meas m)) * ((sigma F) | SS) by MONOID_1:2
.= (sigma_Meas (C_Meas m)) * SS' by B9, RELAT_1:125 ;
then B11: SUM (M * SS) = (sigma_Meas (C_Meas m)) . (union (rng SS')) by MEASURE1:def 11;
union (rng SS) is Element of sigma F by MEASURE1:53;
hence SUM (M * SS) = M . (union (rng SS)) by B11, FUNCT_1:72; :: thesis: verum

end;

then reconsider M = M as sigma_Measure of (sigma F) by B8, MESFUNC5:21, MEASURE1:def 11, VALUED_0:def 19;
take M ; :: thesis: ( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )
for A being set st A in F holds
M . A = m . A

proof

let A be set ; :: thesis: ( A in F implies M . A = m . A )
assume C1: A in F ; :: thesis: M . A = m . A
then reconsider A' = A as Subset of X ;
M . A = (sigma_Meas (C_Meas m)) . A by B2, C1, FUNCT_1:72
.= (C_Meas m) . A' by B3, C1, MEASURE4:def 4 ;
hence M . A = m . A by C1, B1, Th51b; :: thesis: verum

end;

hence ( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) ) by DDef2; :: thesis: verum