let X be non empty set ; :: thesis: for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being induced_Measure of S,P holds (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S)) is sigma_Measure of (sigma (Field_generated_by S))
let S be semialgebra_of_sets of X; :: thesis: for P being pre-Measure of S
for M being induced_Measure of S,P holds (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S)) is sigma_Measure of (sigma (Field_generated_by S))
let P be pre-Measure of S; :: thesis: for M being induced_Measure of S,P holds (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S)) is sigma_Measure of (sigma (Field_generated_by S))
let M be induced_Measure of S,P; :: thesis: (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S)) is sigma_Measure of (sigma (Field_generated_by S))
M is completely-additive by Th60;
then consider N being sigma_Measure of (sigma (Field_generated_by S)) such that
A1: ( N is_extension_of M & N = (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S)) ) by MEASURE8:33;
thus (sigma_Meas (C_Meas M)) | (sigma (Field_generated_by S)) is sigma_Measure of (sigma (Field_generated_by S)) by A1; :: thesis: verum