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

.= 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

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

M . {} =
(sigma_Meas (C_Meas m)) . {}
by FUNCT_1:49, PROB_1:4
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;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

.= 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

hence
( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )
; :: thesis: verum
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;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