let E be non empty finite set ; :: thesis: for A being Event of E holds prob (A,([#] E)) = prob A
let A be Event of E; :: thesis: prob (A,([#] E)) = prob A
prob ([#] E) = 1 by XCMPLX_1:60;
hence prob (A,([#] E)) = prob A by XBOOLE_1:28; :: thesis: verum