@MISC{MEASUR10.MIZ,
  AUTHOR = {Endou, Noboru},
  TITLE = {Product Pre-Measure},
  DAY = {31},
  MONTH = {December},
  YEAR = {2015},
  ADDRESS1 = {National Institute of Technology, Gifu College\\2236-2 Kamimakuwa, Motosu, Gifu, Japan},
  SECTION1 = {Preliminaries},
  SECTION2 = {Family of Semialgebras, Fields and Measures},
  SECTION3 = {Product of Two Measures},
  SUMMARY = {In this article we formalize in Mizar \cite{Mizar:2015}
  product pre-measure on product sets of measurable sets.
  Although there are some approaches to construct product measure
  \cite{Halmos74}, \cite{Bauer:2002}, \cite{Bogachev2007measure}, \cite{FOLLAND},
  \cite{Rao:2004}, we start it from $\sigma$-measure
  because existence of $\sigma$-measure on any semialgebras has
  been proved in \cite{MEASURE9.ABS}.
  In this approach, we use some theorems for integrals.}}

@BOOK{Rao:2004,
  AUTHOR={Rao, M.M.},
  TITLE={Measure Theory and Integration},
  PUBLISHER={Marcel Dekker},
  EDITION={2nd},
  YEAR = {2004}}

@BOOK{Bauer:2002,
  AUTHOR={Heinz Bauer},
  TITLE={Measure and Integration Theory},
  PUBLISHER={Walter de Gruyter Inc.}
  YEAR={2002}}

