conditional[T:TYPE+,                (IMPORTING measure_integration@subset_algebra_def[T])
            S:sigma_algebra,        (IMPORTING probability_measure[T,S])
            P:probability_measure]: THEORY

BEGIN

   IMPORTING probability_measure[T,S],
             measure_integration@sigma_algebra[T,S]

   A,B:   VAR (S)
   n,i,j: VAR nat
   AA,BB: VAR disjoint_indexed_measurable

   null?(A):bool = P(A) = 0

   P(A,B):probability = IF null?(B) THEN 0 ELSE P(intersection(A,B))/P(B) ENDIF

   conditional_complement: LEMMA
                  P(A,B) * P(B) + P(A,complement(B)) * P(complement(B)) = P(A)

   conditional_partition: LEMMA
           Union(image(BB,fullset[below[n+1]])) = fullset[T] IMPLIES
           P(A) = sigma(0,n, LAMBDA i: P(A, BB(i)) * P(BB(i)))

   bayes_theorem: THEOREM
           NOT null?(B) AND
           Union(image(AA,fullset[below[n+1]])) = fullset[T] IMPLIES
           P(AA(j),B) = P(B,AA(j))*P(AA(j))/
                        sigma(0,n, LAMBDA i: P(B, AA(i)) * P(AA(i)))

END conditional