Formalization of Probability and Random Sampling on a Finite and Discrete Sample Space Using the Mizar Proof Checker. - Kenichi Arai; Nobuaki Kondo; Hiroyuki Okazaki (FCS, 2010)