let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds M is Measure of S
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds M is Measure of S
let M be sigma_Measure of S; :: thesis: M is Measure of S
for A, B being Element of S st A misses B holds
M . (A \/ B) = (M . A) + (M . B)

proof

let A, B be Element of S; :: thesis: ( A misses B implies M . (A \/ B) = (M . A) + (M . B) )
assume A2: A misses B ; :: thesis: M . (A \/ B) = (M . A) + (M . B)
A3: ( A in S & B in S & {} in S ) by PROB_1:10;
A4: {} is Subset of X by XBOOLE_1:2;
reconsider A = A, B = B as Subset of X ;
consider F being Function of NAT ,(bool X) such that
A5: ( rng F = {A,B,{} } & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = {} ) ) by A4, Th38;
F is Function of NAT ,S

proof

{A,B,{} } c= S

proof

for x being set st x in {A,B,{} } holds
x in S by A3, ENUMSET1:def 1;
hence {A,B,{} } c= S by TARSKI:def 3; :: thesis: verum

end;

hence F is Function of NAT ,S by A5, FUNCT_2:8; :: thesis: verum

end;

then reconsider F = F as Function of NAT ,S ;
A6: for n, m being Element of NAT st n <> m holds
F . n misses F . m

proof

let n, m be Element of NAT ; :: thesis: ( n <> m implies F . n misses F . m )
assume A7: n <> m ; :: thesis: F . n misses F . m
A8: ( ( n = 0 or n = 1 or 1 < n ) & ( m = 0 or m = 1 or 1 < m ) ) by NAT_1:26;
A9: ( n = 0 & 1 < m implies F . n misses F . m )

proof

assume ( n = 0 & 1 < m ) ; :: thesis: F . n misses F . m
then ( F . n = A & F . m = {} ) by A5;
then (F . n) /\ (F . m) = {} ;
hence F . n misses F . m by XBOOLE_0:def 7; :: thesis: verum

end;

A10: ( n = 1 & 1 < m implies F . n misses F . m )

proof

assume ( n = 1 & 1 < m ) ; :: thesis: F . n misses F . m
then ( F . n = B & F . m = {} ) by A5;
then (F . n) /\ (F . m) = {} ;
hence F . n misses F . m by XBOOLE_0:def 7; :: thesis: verum

end;

A11: ( 1 < n & m = 0 implies F . n misses F . m )

proof

assume ( 1 < n & m = 0 ) ; :: thesis: F . n misses F . m
then ( F . n = {} & F . m = A ) by A5;
then (F . n) /\ (F . m) = {} ;
hence F . n misses F . m by XBOOLE_0:def 7; :: thesis: verum

end;

A12: ( 1 < n & m = 1 implies F . n misses F . m )

proof

assume ( 1 < n & m = 1 ) ; :: thesis: F . n misses F . m
then ( F . n = {} & F . m = B ) by A5;
then (F . n) /\ (F . m) = {} ;
hence F . n misses F . m by XBOOLE_0:def 7; :: thesis: verum

end;

( 1 < n & 1 < m implies F . n misses F . m )

proof

assume ( 1 < n & 1 < m ) ; :: thesis: F . n misses F . m
then ( F . n = {} & F . m = {} ) by A5;
then (F . n) /\ (F . m) = {} ;
hence F . n misses F . m by XBOOLE_0:def 7; :: thesis: verum

end;

hence F . n misses F . m by A2, A5, A7, A8, A9, A10, A11, A12; :: thesis: verum

end;

for m, n being set st m <> n holds
F . m misses F . n

proof

let m, n be set ; :: thesis: ( m <> n implies F . m misses F . n )
assume A13: m <> n ; :: thesis: F . m misses F . n

per cases ( ( m in NAT & n in NAT ) or not m in NAT or not n in NAT ) ;

suppose ( m in NAT & n in NAT ) ; :: thesis: F . m misses F . n

hence F . m misses F . n by A6, A13; :: thesis: verum

end;

suppose ( not m in NAT or not n in NAT ) ; :: thesis: F . m misses F . n

then ( not m in dom F or not n in dom F ) ;
then ( F . m = {} or F . n = {} ) by FUNCT_1:def 4;
hence F . m misses F . n by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

then reconsider F = F as disjoint_valued Function of NAT ,S by PROB_2:def 3;
A14: union (rng F) = A \/ B

proof

union {A,B,{} } = union {A,B} by Th1;
hence union (rng F) = A \/ B by A5, ZFMISC_1:93; :: thesis: verum

end;

A15: for r being Element of NAT holds
( (M * F) . 0 = M . A & (M * F) . 1 = M . B & ( 1 + 1 <= r implies (M * F) . r = 0. ) )

proof

let r be Element of NAT ; :: thesis: ( (M * F) . 0 = M . A & (M * F) . 1 = M . B & ( 1 + 1 <= r implies (M * F) . r = 0. ) )
A16: for r being Element of NAT holds (M * F) . r = M . (F . r)

proof

let r be Element of NAT ; :: thesis: (M * F) . r = M . (F . r)
dom (M * F) = NAT by FUNCT_2:def 1;
hence (M * F) . r = M . (F . r) by FUNCT_1:22; :: thesis: verum

end;

( 1 + 1 <= r implies (M * F) . r = 0. )

proof

assume 1 + 1 <= r ; :: thesis: (M * F) . r = 0.
then 1 < r by NAT_1:13;
then F . r = {} by A5;
then (M * F) . r = M . {} by A16;
hence (M * F) . r = 0. by VALUED_0:def 19; :: thesis: verum

end;

hence ( (M * F) . 0 = M . A & (M * F) . 1 = M . B & ( 1 + 1 <= r implies (M * F) . r = 0. ) ) by A5, A16; :: thesis: verum

end;

set H = M * F;
A17: M * F is nonnegative by Th54;
A18: 0 + 1 = 0 + 1 ;
set y1 = (Ser (M * F)) . 1;
set n2 = 1 + 1;
reconsider A = A, B = B as Element of S ;
(Ser (M * F)) . (1 + 1) = ((Ser (M * F)) . 1) + ((M * F) . (1 + 1)) by SUPINF_2:63;
then (Ser (M * F)) . (1 + 1) = ((Ser (M * F)) . 1) + 0. by A15
.= (Ser (M * F)) . 1 by XXREAL_3:4
.= ((Ser (M * F)) . 0 ) + ((M * F) . 1) by A18, SUPINF_2:63
.= (M . A) + (M . B) by A15, SUPINF_2:63 ;
then SUM (M * F) = (M . A) + (M . B) by A15, A17, SUPINF_2:67;
hence M . (A \/ B) = (M . A) + (M . B) by A14, Def11; :: thesis: verum

end;

hence M is Measure of S by Def5; :: thesis: verum