let f1, f2 be Measure of (Field_generated_by Family_of_Intervals); :: thesis: ( ( for A being set st A in Field_generated_by Family_of_Intervals holds
for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds
f1 . A = Sum (pre-Meas * F) ) & ( for A being set st A in Field_generated_by Family_of_Intervals holds
for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds
f2 . A = Sum (pre-Meas * F) ) implies f1 = f2 )
assume that
A1: for A being set st A in Field_generated_by Family_of_Intervals holds
for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds
f1 . A = Sum (pre-Meas * F) and
A2: for A being set st A in Field_generated_by Family_of_Intervals holds
for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds
f2 . A = Sum (pre-Meas * F) ; :: thesis: f1 = f2
for A being Element of Field_generated_by Family_of_Intervals holds f1 . A = f2 . A
proof
let A be Element of Field_generated_by Family_of_Intervals; :: thesis: f1 . A = f2 . A
A in Field_generated_by Family_of_Intervals ;
then A in DisUnion Family_of_Intervals by SRINGS_3:22;
then A in { A where A is Subset of REAL : ex F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F } by SRINGS_3:def 3;
then ex E being Subset of REAL st
( A = E & ex F being disjoint_valued FinSequence of Family_of_Intervals st E = Union F ) ;
then consider F being disjoint_valued FinSequence of Family_of_Intervals such that
A3: A = Union F ;
f1 . A = Sum (pre-Meas * F) by A1, A3;
hence f1 . A = f2 . A by A2, A3; :: thesis: verum
end;
hence f1 = f2 by FUNCT_2:def 8; :: thesis: verum