Abstract
In this article, we prove the integrability of continuous functions on n-dimensional real normed spaces, using the Mizar formalism. Generalizing selected theorems from the Mizar Mathematical Library, we prove the integrability of continuous real n-variable functions and then, using the correspondence between product-type and tuple-type spaces, we demonstrate the integrability of continuous functions on the desired multidimensional spaces.