let M be zeroed V94() 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)

hence M is additive ; :: thesis: verum

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

then
M is additive
;
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

F . m misses F . n

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. ) )

A24: 0 + 1 = 0 + 1 ;

set y1 = (Ser (M * F)) . 1;

A25: M * F is V94() 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;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

for m, n being object st m <> n holds
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 )

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

end;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

A12:
( 1 < n & m = 0 implies F . n misses F . m )
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;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

proof

A14:
( 1 < n & 1 < m implies F . n misses F . m )
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;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

proof

A16:
( n = 1 & 1 < m implies F . n misses F . m )
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;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

proof

A18:
( n = 0 & 1 < m implies F . n misses F . m )
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;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

proof

assume
n <> m
; :: thesis: F . n misses F . m
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;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

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

F . m misses F . n

proof

then reconsider F = F as disjoint_valued sequence of S by PROB_2:def 2;
let m, n be object ; :: thesis: ( m <> n implies F . m misses F . n )

assume A20: m <> n ; :: thesis: F . m misses F . n

end;assume A20: m <> n ; :: thesis: F . m misses F . n

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

set H = M * F;
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)

end;A23: for r being Element of NAT holds (M * F) . r = M . (F . r)

proof

( 1 + 1 <= r implies (M * F) . r = 0. )
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;dom (M * F) = NAT by FUNCT_2:def 1;

hence (M * F) . r = M . (F . r) by FUNCT_1:12; :: thesis: verum

proof

hence
( (M * F) . 0 = M . A & (M * F) . 1 = M . B & ( 1 + 1 <= r implies (M * F) . r = 0. ) )
by A5, A23; :: thesis: verum
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;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

A24: 0 + 1 = 0 + 1 ;

set y1 = (Ser (M * F)) . 1;

A25: M * F is V94() 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

hence M is additive ; :: thesis: verum