let F be disjoint_valued FinSequence of Family_of_Intervals ; ( Union F in Family_of_Intervals implies pre-Meas . (Union F) = Sum (pre-Meas * F) )
assume
Union F in Family_of_Intervals
; 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
F <> {}
;
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;
verum end; end;