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 Th39;
hence prob A,([#] E) = prob A by XBOOLE_1:28; :: thesis: verum