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)
now :: thesis: P . (A \/ B) = (P . A) + (P . B)
per 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;
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;
suppose A4: ( not 0 in A & 0 in B ) ; :: thesis: P . (A \/ B) = (P . A) + (P . B)
then A5: 0 in A \/ B by XBOOLE_0:def 3;
( P . A = 0 & P . B = 1 ) by A4, Lm1;
hence P . (A \/ B) = (P . A) + (P . B) by A5, Lm1; :: thesis: verum
end;
suppose A6: ( not 0 in A & not 0 in B ) ; :: thesis: P . (A \/ B) = (P . A) + (P . B)
then A7: not 0 in A \/ B by XBOOLE_0:def 3;
( P . A = 0 & P . B = 0 ) by A6, Lm1;
hence P . (A \/ B) = (P . A) + (P . B) by A7, Lm1; :: thesis: verum
end;
end;
end;
hence P . (A \/ B) = (P . A) + (P . B) ; :: thesis: verum