let A, B be Event of Borel_Sets ; :: thesis: ( A misses B implies P . (A \/ B) = (P . A) + (P . B) )

assume A1: A misses B ; :: thesis: P . (A \/ B) = (P . A) + (P . B)

assume A1: A misses B ; :: thesis: P . (A \/ B) = (P . A) + (P . B)

now :: thesis: P . (A \/ B) = (P . A) + (P . B)end;

hence
P . (A \/ B) = (P . A) + (P . B)
; :: thesis: verumper cases
( ( 0 in A & not 0 in B ) or ( not 0 in A & 0 in B ) or ( not 0 in A & not 0 in B ) )
by A1, XBOOLE_0:3;

end;

suppose A2:
( 0 in A & not 0 in B )
; :: thesis: P . (A \/ B) = (P . A) + (P . B)

then A3:
0 in A \/ B
by XBOOLE_0:def 3;

( P . A = 1 & P . B = 0 ) by A2, Lm1;

hence P . (A \/ B) = (P . A) + (P . B) by A3, Lm1; :: thesis: verum

end;( P . A = 1 & P . B = 0 ) by A2, Lm1;

hence P . (A \/ B) = (P . A) + (P . B) by A3, Lm1; :: thesis: verum