let X be 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 M = (C_Meas M) | (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 M = (C_Meas M) | (Field_generated_by S)
let P be pre-Measure of S; :: thesis: for M being induced_Measure of S,P holds M = (C_Meas M) | (Field_generated_by S)
let M be induced_Measure of S,P; :: thesis: M = (C_Meas M) | (Field_generated_by S)

now :: thesis: for A being Element of Field_generated_by S holds M . A = ((C_Meas M) | (Field_generated_by S)) . A

let A be Element of Field_generated_by S; :: thesis: M . A = ((C_Meas M) | (Field_generated_by S)) . A
M is completely-additive by MEASURE9:60;
then M . A = (C_Meas M) . A by MEASURE8:18;
hence M . A = ((C_Meas M) | (Field_generated_by S)) . A by FUNCT_1:49; :: thesis: verum

end;

hence M = (C_Meas M) | (Field_generated_by S) by FUNCT_2:def 8; :: thesis: verum