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 A1: 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) )
set M = (sigma_Meas (C_Meas m)) | (sigma F);
A2: F c= sigma_Field (C_Meas m) by Th20;
then A3: sigma F c= sigma_Field (C_Meas m) by PROB_1:def 9;
then reconsider M = (sigma_Meas (C_Meas m)) | (sigma F) as Function of (sigma F),ExtREAL by FUNCT_2:32;
A4: 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 SS9 = SS as Sep_Sequence of (sigma_Field (C_Meas m)) by A3, FUNCT_2:7;
A5: rng SS c= sigma F by RELAT_1:def 19;
M * SS = (sigma_Meas (C_Meas m)) * ((sigma F) |` SS) by MONOID_1:1
.= (sigma_Meas (C_Meas m)) * SS9 by A5, RELAT_1:94 ;
then A6: SUM (M * SS) = (sigma_Meas (C_Meas m)) . (union (rng SS9)) by MEASURE1:def 6;
union (rng SS) is Element of sigma F by MEASURE1:24;
hence SUM (M * SS) = M . (union (rng SS)) by A6, FUNCT_1:49; :: thesis: verum

end;

M . {} = (sigma_Meas (C_Meas m)) . {} by FUNCT_1:49, PROB_1:4
.= 0 by VALUED_0:def 19 ;
then reconsider M = M as sigma_Measure of (sigma F) by A4, MEASURE1:def 6, MESFUNC5:15, VALUED_0:def 19;
take M ; :: thesis: ( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )
A7: F c= sigma F by PROB_1:def 9;
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 A8: A in F ; :: thesis: M . A = m . A
then reconsider A9 = A as Subset of X ;
M . A = (sigma_Meas (C_Meas m)) . A by A7, A8, FUNCT_1:49
.= (C_Meas m) . A9 by A2, A8, MEASURE4:def 3 ;
hence M . A = m . A by A1, A8, Th18; :: thesis: verum

end;

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