let M be zeroed nonnegative Function of S,ExtREAL; :: thesis: ( M is sigma-additive implies M is additive )
assume A1: M is sigma-additive ; :: thesis: M is additive
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 A2: A misses B ; :: thesis: M . (A \/ B) = (M . A) + (M . B)
A3: ( 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 sequence of (bool X) such that
A4: rng F = {A,B,{}} and
A5: ( F . 0 = A & F . 1 = B ) and
A6: for n being Element of NAT st 1 < n holds
F . n = {} by Th17;
{} in S by PROB_1:4;
then for x being object st x in {A,B,{}} holds
x in S by A3, ENUMSET1:def 1;
then {A,B,{}} c= S ;
then reconsider F = F as sequence of S by A4, FUNCT_2:6;
A7: 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 )
A8: ( n = 0 or n = 1 or 1 < n ) by NAT_1:25;
A9: ( m = 0 or m = 1 or 1 < m ) by NAT_1:25;
A10: ( 1 < n & m = 1 implies F . n misses F . m )

proof

assume that
A11: 1 < n and
m = 1 ; :: thesis: F . n misses F . m
F . n = {} by A6, A11;
then (F . n) /\ (F . m) = {} ;
hence F . n misses F . m ; :: thesis: verum

end;

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

proof

assume that
A13: 1 < n and
m = 0 ; :: thesis: F . n misses F . m
F . n = {} by A6, A13;
then (F . n) /\ (F . m) = {} ;
hence F . n misses F . m ; :: thesis: verum

end;

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

proof

assume that
A15: 1 < n and
1 < m ; :: thesis: F . n misses F . m
F . n = {} by A6, A15;
then (F . n) /\ (F . m) = {} ;
hence F . n misses F . m ; :: thesis: verum

end;

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

proof

assume that
n = 1 and
A17: 1 < m ; :: thesis: F . n misses F . m
F . m = {} by A6, A17;
then (F . n) /\ (F . m) = {} ;
hence F . n misses F . m ; :: thesis: verum

end;

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

proof

assume that
n = 0 and
A19: 1 < m ; :: thesis: F . n misses F . m
F . m = {} by A6, A19;
then (F . n) /\ (F . m) = {} ;
hence F . n misses F . m ; :: thesis: verum

end;

assume n <> m ; :: thesis: F . n misses F . m
hence F . n misses F . m by A2, A5, A8, A9, A18, A16, A12, A10, A14; :: thesis: verum

end;

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

proof

let m, n be object ; :: thesis: ( m <> n implies F . m misses F . n )
assume A20: 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 A7, A20; :: 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 ; :: thesis: verum

end;

end;

end;

then reconsider F = F as disjoint_valued sequence of S by PROB_2:def 2;
union {A,B,{}} = union {A,B} by Th1;
then A21: union (rng F) = A \/ B by A4, ZFMISC_1:75;
A22: 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. ) )
A23: 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 A6;
then (M * F) . r = M . {} by A23;
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, A23; :: thesis: verum

end;

set H = M * F;
A24: 0 + 1 = 0 + 1 ;
set y1 = (Ser (M * F)) . 1;
A25: M * F is nonnegative by Th25;
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:def 11;
then (Ser (M * F)) . (1 + 1) = ((Ser (M * F)) . 1) + 0. by A22
.= (Ser (M * F)) . 1 by XXREAL_3:4
.= ((Ser (M * F)) . 0) + ((M * F) . 1) by A24, SUPINF_2:def 11
.= (M . A) + (M . B) by A22, SUPINF_2:def 11 ;
then SUM (M * F) = (M . A) + (M . B) by A22, A25, SUPINF_2:48;
hence M . (A \/ B) = (M . A) + (M . B) by A21, A1; :: thesis: verum

end;

then M is additive ;
hence M is additive ; :: thesis: verum