let F be disjoint_valued FinSequence of Family_of_Intervals ; :: thesis: ( Union F in Family_of_Intervals implies pre-Meas . (Union F) = Sum (pre-Meas * F) )
assume Union F in Family_of_Intervals ; :: thesis: pre-Meas . (Union F) = Sum (pre-Meas * F)
then consider G being disjoint_valued FinSequence of Family_of_Intervals such that
A1: F,G are_fiberwise_equipotent and
A2: for n being Nat st n in dom G holds
( Union (G | n) in Family_of_Intervals & pre-Meas . (Union (G | n)) = Sum (pre-Meas * (G | n)) ) by Th63;
per cases ( F = {} or F <> {} ) ;
suppose A3: F = {} ; :: thesis: pre-Meas . (Union F) = Sum (pre-Meas * F)
then union (rng F) = {} by ZFMISC_1:2;
then ( Union F = {} & {} c= REAL ) by CARD_3:def 4;
then pre-Meas . (Union F) = diameter {} by Th59
.= 0 by MEASURE5:def 6 ;
hence pre-Meas . (Union F) = Sum (pre-Meas * F) by A3, EXTREAL1:7; :: thesis: verum
end;
suppose F <> {} ; :: thesis: pre-Meas . (Union F) = Sum (pre-Meas * F)
then A4: 1 <= len F by FINSEQ_1:20;
A5: ( len F = len G & dom F = dom G ) by A1, RFINSEQ:3;
rng F = rng G by A1, CLASSES1:75;
then Union F = union (rng G) by CARD_3:def 4;
then A6: Union F = Union G by CARD_3:def 4;
A7: G | (len F) = G by A5, FINSEQ_1:58;
len F in dom G by A4, A5, FINSEQ_3:25;
then A8: pre-Meas . (Union G) = Sum (pre-Meas * G) by A7, A2;
A9: ( pre-Meas * G is nonnegative & pre-Meas * F is nonnegative ) by MEASURE9:47;
A10: dom pre-Meas = Family_of_Intervals by FUNCT_2:def 1;
( rng G c= Family_of_Intervals & rng F c= Family_of_Intervals ) ;
hence pre-Meas . (Union F) = Sum (pre-Meas * F) by A6, A8, A9, Th67, A1, A5, A10, CLASSES1:83; :: thesis: verum
end;
end;