Some authors have formalized the integral in the Mizar Mathematical Library (MML). The first article in a series on the Darboux/Riemann integral was written by Noboru Endou and Artur Korniłowicz: . The Lebesgue integral was formalized a little later  and recently the integral of Riemann-Stieltjes was introduced in the MML by Keiko Narita, Kazuhisa Nakasho and Yasunari Shidama . A presentation of definitions of integrals in other proof assistants or proof checkers (ACL2, COQ, Isabelle/HOL, HOL4, HOL Light, PVS, ProofPower) may be found in  and . Using the Mizar system , we define the Gauge integral (Henstock-Kurzweil) of a real-valued function on a real interval [a, b] (see , , , , ). In the next section we formalize that the Henstock-Kurzweil integral is linear. In the last section, we verified that a real-valued bounded integrable (in sense Darboux/Riemann [6, 7, 8]) function over a interval a, b is Gauge integrable. Note that, in accordance with the possibilities of the MML , we reuse a large part of demonstrations already present in another article. Instead of rewriting the proof already contained in  (MML Version: 5.42.1290), we slightly modified this article in order to use directly the expected results.