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

set n2 = 1 + 1;
let A, B be Element of S; :: thesis: ( A misses B implies M . (A \/ B) = (M . A) + (M . B) )
assume A1: A misses B ; :: thesis: M . (A \/ B) = (M . A) + (M . B)
A2: ( A in S & B in S ) ;
reconsider A = A, B = B as Subset of X ;
{} is Subset of X by XBOOLE_1:2;
then consider F being Function of NAT,(bool X) such that
A3: rng F = {A,B,{}} and
A4: ( F . 0 = A & F . 1 = B ) and
A5: for n being Element of NAT st 1 < n holds
F . n = {} by Th38;
{} in S by PROB_1:4;
then for x being set st x in {A,B,{}} holds
x in S by A2, ENUMSET1:def 1;
then {A,B,{}} c= S by TARSKI:def 3;
then reconsider F = F as Function of NAT,S by A3, FUNCT_2:6;
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 )
A7: ( n = 0 or n = 1 or 1 < n ) by NAT_1:25;
A8: ( m = 0 or m = 1 or 1 < m ) by NAT_1:25;
A9: ( 1 < n & m = 1 implies F . n misses F . m )

proof

assume that
A10: 1 < n and
m = 1 ; :: thesis: F . n misses F . m
F . n = {} by A5, A10;
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 that
A12: 1 < n and
m = 0 ; :: thesis: F . n misses F . m
F . n = {} by A5, A12;
then (F . n) /\ (F . m) = {} ;
hence F . n misses F . m by XBOOLE_0:def 7; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

assume n <> m ; :: thesis: F . n misses F . m
hence F . n misses F . m by A1, A4, A7, A8, A17, A15, A11, A9, A13; :: 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 A19: 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, A19; :: 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 2;
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 2;
union {A,B,{}} = union {A,B} by Th1;
then A20: union (rng F) = A \/ B by A3, ZFMISC_1:75;
A21: 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. ) )
A22: 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:12; :: 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 A22;
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 A4, A22; :: thesis: verum

end;

set H = M * F;
A23: 0 + 1 = 0 + 1 ;
set y1 = (Ser (M * F)) . 1;
A24: M * F is nonnegative by Th54;
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:44;
then (Ser (M * F)) . (1 + 1) = ((Ser (M * F)) . 1) + 0. by A21
.= (Ser (M * F)) . 1 by XXREAL_3:4
.= ((Ser (M * F)) . 0) + ((M * F) . 1) by A23, SUPINF_2:44
.= (M . A) + (M . B) by A21, SUPINF_2:44 ;
then SUM (M * F) = (M . A) + (M . B) by A21, A24, SUPINF_2:48;
hence M . (A \/ B) = (M . A) + (M . B) by A20, Def11; :: thesis: verum

end;

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