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 () st
( M is_extension_of m & M = (sigma_Meas ()) | () )

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 () st
( M is_extension_of m & M = (sigma_Meas ()) | () )

let m be Measure of F; :: thesis: ( m is completely-additive implies ex M being sigma_Measure of () st
( M is_extension_of m & M = (sigma_Meas ()) | () ) )

assume A1: m is completely-additive ; :: thesis: ex M being sigma_Measure of () st
( M is_extension_of m & M = (sigma_Meas ()) | () )

set M = (sigma_Meas ()) | ();
A2: F c= sigma_Field () by Th20;
then A3: sigma F c= sigma_Field () by PROB_1:def 9;
then reconsider M = (sigma_Meas ()) | () as Function of (),ExtREAL by FUNCT_2:32;
A4: for SS being Sep_Sequence of () holds SUM (M * SS) = M . (union (rng SS))
proof
let SS be Sep_Sequence of (); :: thesis: SUM (M * SS) = M . (union (rng SS))
reconsider SS9 = SS as Sep_Sequence of () by ;
A5: rng SS c= sigma F by RELAT_1:def 19;
M * SS = (sigma_Meas ()) * (() |` SS) by MONOID_1:1
.= (sigma_Meas ()) * SS9 by ;
then A6: SUM (M * SS) = (sigma_Meas ()) . (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 ; :: thesis: verum
end;
M . {} = (sigma_Meas ()) . {} by
.= 0 by VALUED_0:def 19 ;
then reconsider M = M as sigma_Measure of () by ;
take M ; :: thesis: ( M is_extension_of m & M = (sigma_Meas ()) | () )
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 ()) . A by
.= () . A9 by ;
hence M . A = m . A by A1, A8, Th18; :: thesis: verum
end;
hence ( M is_extension_of m & M = (sigma_Meas ()) | () ) ; :: thesis: verum