In this article, we prove the first mean value theorem for integrals [16]. The formalization of various theorems about the properties of the Lebesgue integral is also presented.
MML identifier: MESFUNC7, version: 7.8.09 4.97.1001